From b51b7d0a53f62df17662e13643c43f3907b67f9f Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Fri, 25 Sep 2026 16:20:08 +0700
Subject: [PATCH] A refusal in a prelude generic's body stands at the call that
 asked for the copy, with the prelude's line as a note

---
 lib/check.ml      | 34 ++++++++++++++++++++++++++--------
 test/test_flan.ml | 31 +++++++++++++++++++++++++++++++
 2 files changed, 57 insertions(+), 8 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index 8b6df651..d69941fc 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -12049,16 +12049,34 @@ and instantiate env loc gname vars subst cparams cret =
            which call asked for this copy; the note names it. Nested copies
            each add their own, so the notes walk the chain back to the call
            the programmer wrote. *)
+        let at () =
+          String.concat ", "
+            (List.map
+               (fun v -> Printf.sprintf "$%s = %s" v
+                   (Types.to_string (List.assoc v subst)))
+               vars)
+        in
+        let in_prelude (l : Loc.t) = String.equal l.Loc.file Prelude.file in
         let e =
           match e with
+          (* A prelude generic's body is source nobody at this call wrote, and
+             an editor cannot jump to it. The refusal moves to the call that
+             asked for the copy, and the prelude's line comes along as a
+             note. *)
+          | Loc.Error d when in_prelude d.Loc.dloc && not (in_prelude loc) ->
+            Loc.Error
+              (Loc.sort_notes
+                 { d with
+                   Loc.dloc = loc;
+                   dmsg =
+                     Printf.sprintf "%s cannot be made at %s. In its body: %s"
+                       gname (at ()) d.Loc.dmsg;
+                   notes =
+                     d.Loc.notes
+                     @ [ Loc.note d.Loc.dloc
+                           (Printf.sprintf "in %s's body, in the prelude" gname) ];
+                   expansion = None })
           | Loc.Error d when d.Loc.dloc <> loc ->
-            let at =
-              String.concat ", "
-                (List.map
-                   (fun v -> Printf.sprintf "$%s = %s" v
-                       (Types.to_string (List.assoc v subst)))
-                   vars)
-            in
             Loc.Error
               (Loc.sort_notes
                  { d with
@@ -12066,7 +12084,7 @@ and instantiate env loc gname vars subst cparams cret =
                      d.Loc.notes
                      @ [ Loc.note loc
                            (Printf.sprintf "%s is instantiated at %s here"
-                              gname at) ] })
+                              gname (at ())) ] })
           | e -> e
         in
         (* A copy whose body did not check is not a copy. Both entries go back
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 9d0ad68d..1ab6d401 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -6017,6 +6017,37 @@ let () =
            = [ "show is instantiated at $t = (CFn [] i32) here";
                "outer is instantiated at $t = (CFn [] i32) here" ]));
 
+  (* A copy that cannot be built at a closure's type: the zeroed value in the
+     body is refused there, and the call that asked is named. *)
+  (match
+     checked
+       "(defn blank [x $t] $t (let [z (the $t (zeroed))] z)) \
+        (defn use-it [f (Fn [i32] i32)] i32 (blank f) 0)"
+   with
+   | _ -> check "a zeroed closure in a copy is refused" false
+   | exception Loc.Error d ->
+     check "a copy at a closure type names the call that asked"
+       (List.exists
+          (fun (n : Loc.note) ->
+             contains n.Loc.nmsg "blank is instantiated at $t = (Fn [i32] i32) here")
+          d.Loc.notes));
+
+  (* A prelude generic's body is nobody's source at the call: the refusal is
+     at the call, and the prelude's line is a note. *)
+  (match
+     checked
+       "(defn keep [g (Vec u8)] bool true) \
+        (defn use-it [xs [(Vec u8)]] i32 (length (filter xs keep)))"
+   with
+   | _ -> check "a prelude copy that cannot be built is refused" false
+   | exception Loc.Error d ->
+     check "a prelude copy's refusal is at the user's call"
+       (d.Loc.dloc.Loc.file <> Prelude.file
+        && contains d.Loc.dmsg "filter cannot be made at $t = (Vec u8)"
+        && List.exists
+             (fun (n : Loc.note) -> n.Loc.nloc.Loc.file = Prelude.file)
+             d.Loc.notes));
+
   (* The parser resynchronises on a top-level form, so two bad declarations are
      two errors rather than one. *)
   (match Parse.program_all (read "(defn a)\n(defn b)\n") with