A refusal inside a generic copy names each call that asked for it, a refused generic body is reported once, and a type variable prints with its $

TODO.org

@@ -767,12 +767,6 @@ clause here admits nothing but type predicates. Whether it should take value
 predicates over a length parameter deserves answering deliberately rather than
 falling out of the implementation.
 
-** TODO "In instantiation of" notes
-A refusal inside a copy points at the generic's source with no note naming the
-call site that asked for that type. The data is there — =instantiation_origin=
-exists and the session already uses it — and wiring it into every failure under an
-instantiation is a lane of its own.
-
 ** DONE A program is one compilation, so a generic's body is always visible
 CLOSED: [2026-09-25]
 Odin's and Zig's model: packages are never compiled separately. The cost is build
@@ -1030,15 +1024,6 @@ ignore order, writable access has to alias the real storage. Flexible field orde
 waits for classes deliberately, because a class owns its layout and a =Vector2=
 should not pay for identity and metadata. Not implemented.
 
-** TODO An error in a called generic's body is reported twice
-=(defn g [x $t] u64 (nosuch x))= called once from =main= prints "unknown
-function nosuch" twice at the same place and counts 2 errors — once from the
-abstract pass and once from the instantiation.
-
-** TODO A type variable is printed without its $
-=Types.to_string= prints =Var t= as =t=, so a refusal reads "selection-sort
-expects [t] here, found [3 i32]" where the source wrote =[$t]=.
-
 ** DONE Two refusals suggested something that does not compile
 CLOSED: [2026-09-25]
 =vec-new= and =map-new= with no type no longer say "or give the binding a type";

lib/check.ml

@@ -192,6 +192,12 @@ type env = {
      chain. Odin has no cap of its own to copy, so there was nothing to
      borrow. *)
   mutable chain : (string * Types.t list * Loc.t) list;
+  (* Generics whose abstract pass was refused and recorded, in a whole-file
+     check that goes on after a refusal. A call site still gets a copy's
+     signature, but its body is not checked again: every refusal the abstract
+     pass made would come back from the copy, at the same line, once per type
+     it was called at. *)
+  refused_generics : (string, unit) Hashtbl.t;
   (* Set while a struct, data-case or union field's type is being resolved,
      and only then. It exists for one message: an unknown lowercase name in a
      type slot is told to introduce a type variable with [$name] in the
@@ -240,6 +246,7 @@ let new_env () = {
   subst = [];
   tvpreds = [];
   chain = [];
+  refused_generics = Hashtbl.create 4;
   in_field = false;
   classes = Hashtbl.create 8;
   tracks = Hashtbl.create 16;
@@ -2157,7 +2164,7 @@ let unconstrained env loc op ~needs (t : Types.t) =
     | _ ->
       Loc.failk "check/unconstrained-type-variable" loc
         "%s over the type variable %s: nothing declares %s %s. Write \
-         {:where (%s $%s)} at the head of the body, or take the operation as \
+         {:where (%s %s)} at the head of the body, or take the operation as \
          a parameter, a (Fn [%s %s] ...), and call it here"
         op (Types.to_string t) (Types.to_string t) needs needs
         (Types.to_string t) (Types.to_string t) (Types.to_string t)
@@ -2185,6 +2192,9 @@ let rec mangle_ty (t : Types.t) =
   | Types.CFn (ps, r) ->
     Printf.sprintf "cfn-%s-to-%s"
       (String.concat "-" (List.map mangle_ty ps)) (mangle_ty r)
+  (* Bare, because [Types.to_string] spells a variable with its [$] for the
+     reader and a symbol has no room for one. *)
+  | Types.Var n -> n
   | t -> Types.to_string t
 
 (* ── The runaway instantiation, refused by name rather than by depth ────
@@ -4099,14 +4109,14 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
              | Some (Types.Int k) -> not (Types.signed k)
              | _ -> false) ->
     let t = Option.get want in
-    let gname, _, at = List.nth ctx.env.chain (List.length ctx.env.chain - 1) in
+    (* [instantiate] adds the note naming the call that asked for this copy. *)
+    let gname, _, _ = List.nth ctx.env.chain (List.length ctx.env.chain - 1) in
     let var =
       match List.find_opt (fun (_, u) -> Types.equal u t) ctx.env.subst with
       | Some (v, _) -> Printf.sprintf "$%s = %s" v (Types.to_string t)
       | None -> Types.to_string t
     in
     Loc.failk literal_at_want loc
-      ~notes:[ Loc.note at (Printf.sprintf "%s is instantiated at %s here" gname var) ]
       "%Ld does not fit in %s, which holds no negative number, and %s is called \
        at %s — the body has to work at every type it is called at, so write \
        it with no negative literal, as in (- x %Ld) in place of (+ x %Ld)"
@@ -6548,9 +6558,7 @@ and mixed_refusal : 'a. ctx -> Ast.expr list -> Loc.diag -> 'a =
                           (Printf.sprintf
                              "this array's first element is %s, so every \
                               element is"
-                             (match first.Tast.ty with
+                             (Types.to_string first.Tast.ty)) ] }))
-                              | Types.Var v -> "$" ^ v
-                              | t -> Types.to_string t)) ] }))
       rest;
     raise (Loc.Error d)
 
@@ -11284,11 +11292,39 @@ and instantiate env loc gname vars subst cparams cret =
       env.subst <- saved_subst; env.tyvars <- saved_vars;
       env.tvpreds <- saved_preds; env.chain <- saved_chain
     in
+    if Hashtbl.mem env.refused_generics gname then begin
+      restore ();
+      sym
+    end else
     let tfn =
       match !check_fn_ref env { fn with Ast.name = sym } with
       | tfn -> restore (); tfn
       | exception e ->
         restore ();
+        (* The refusal is inside the generic's source, which says nothing about
+           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 e =
+          match e with
+          | 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
+                   Loc.notes =
+                     d.Loc.notes
+                     @ [ Loc.note loc
+                           (Printf.sprintf "%s is instantiated at %s here"
+                              gname at) ] })
+          | e -> e
+        in
         (* A copy whose body did not check is not a copy. Both entries go back
            out, so a second call at the same types is the same refusal again
            rather than a cache hit on a function that does not exist. *)
@@ -13933,9 +13969,12 @@ let build_program ~keep_going ?tolerate (decls : Ast.decl list) :
     (fun (d : Ast.decl) ->
        match d.Ast.d with
        | Ast.Defn fn when Hashtbl.mem env.gsigs fn.Ast.name ->
-         ignore
+         (match
-           (Loc.caught s (fun () ->
+            Loc.caught s (fun () ->
-              tolerant fn.Ast.name (fun () -> Some (check_generic env fn))))
+              tolerant fn.Ast.name (fun () -> Some (check_generic env fn)))
+          with
+          | None -> Hashtbl.replace env.refused_generics fn.Ast.name ()
+          | Some _ -> ())
        | _ -> ())
     decls;
   let globals =

lib/dev.ml

@@ -669,14 +669,12 @@ let host_loc t name =
    that was written finds nothing in the program, and these are how it gets
    from that name to what the program does hold. *)
 
-(* Its signature as written, [$] and all — [Types.to_string] prints a variable
+(* Its signature as written, [$] and all. *)
-   bare, and [[t]] is not how anyone wrote it. *)
 let generic_signature t name =
   match Hashtbl.find_opt t.session.Session.env.Check.gsigs name with
   | None -> None
-  | Some (vars, params, ret) ->
+  | Some (_, params, ret) ->
-    let dollar = List.map (fun v -> (v, Types.Var ("$" ^ v))) vars in
+    let show ty = Types.to_string ty in
-    let show ty = Types.to_string (Check.subst_ty dollar ty) in
     Some
       (Printf.sprintf "%s [%s] %s" name
          (String.concat " " (List.map show params)) (show ret))

lib/types.ml

@@ -231,7 +231,7 @@ let rec to_string = function
   | CFn (ps, r) ->
     Printf.sprintf "(CFn [%s] %s)"
       (String.concat " " (List.map to_string ps)) (to_string r)
-  | Var n -> n
+  | Var n -> "$" ^ n
   | Dyn -> "dyn"
 
 let is_numeric = function Int _ | Float _ -> true | _ -> false

test/test_acceptance.ml

@@ -3608,7 +3608,7 @@ let () =
        chain of instantiations and not a depth it gave up at. *)
     refuses "an unconstrained operator in a generic body"
       "programs/generic-reject.flan"
-      "nothing declares t numeric?";
+      "nothing declares $t numeric?";
     refuses "an unconstrained operator names the way out"
       "programs/generic-reject.flan" "{:where (numeric? $t)}";
     refuses "a runaway instantiation" "programs/generic-runaway.flan"
@@ -4680,10 +4680,10 @@ level "1"
        the easier of the two to leave open. *)
     refuses "a nested function type does not widen"
       "programs/fn-generic-nested.flan"
-      "hof expects (Fn [(Fn [t] t)] i32) here";
+      "hof expects (Fn [(Fn [$t] $t)] i32) here";
     refuses "and neither does one in return position"
       "programs/fn-generic-nested-return.flan"
-      "call-twice expects (Fn [] (Fn [] t)) here";
+      "call-twice expects (Fn [] (Fn [] $t)) here";
     outputs ~dev:true "an fn capturing by value, dev" "programs/fn-capture.flan"
       fn_capture_out;
 

test/test_flan.ml

@@ -1417,7 +1417,7 @@ let () =
   accepts "all-distinct over a type variable"
     "(defn three [a $t b $t c $t] bool {:where (equal? $t)} (!= a b c))";
   rejects_check "a chain still wants the right predicate"
-    ~needle:"nothing declares t ordered?"
+    ~needle:"nothing declares $t ordered?"
     "(defn between [a $t b $t c $t] bool {:where (equal? $t)} (< a b c))";
   (* One operand and none. Both would have to be [true] whatever they were
      handed, which is a typo carrying a value. *)
@@ -5988,6 +5988,37 @@ let () =
      check "and they are in source order"
        (List.map (fun (d : Loc.diag) -> d.Loc.dloc.Loc.line) ds = [ 1; 2; 3 ]));
 
+  (* A generic whose abstract pass was refused is not checked again at each
+     copy: the refusal is one error, however many types call it, and the
+     caller's own later refusal is still found. *)
+  (match
+     Check.program_all
+       (Parse.program_all
+          (read "(defn g [x $t] u64 (nosuch x))\n\
+                 (defn main [] i32 (g 3) (g true) nope 0)\n"))
+   with
+   | _ -> check "a refused generic body is refused" false
+   | exception Loc.Errors ds ->
+     check "a refused generic body is one error, and its caller's is another"
+       (List.map (fun (d : Loc.diag) -> d.Loc.dloc.Loc.line) ds = [ 1; 2 ]));
+
+  (* A refusal inside a copy names the call that asked for it, and each copy
+     between: the chain walks back to the line the programmer wrote. *)
+  (match
+     checked
+       "(defn show [v $t] () (println v)) \
+        (defn outer [v $t] () (show v)) \
+        (defn main [] i32 (outer main) 0)"
+   with
+   | _ -> check "a copy with no printer is refused" false
+   | exception Loc.Error d ->
+     let notes = List.map (fun (n : Loc.note) -> n.Loc.nmsg) d.Loc.notes in
+     check "a refusal in a copy names both instantiations"
+       (contains d.Loc.dmsg "no printer for"
+        && notes
+           = [ "show is instantiated at $t = (CFn [] i32) here";
+               "outer is instantiated at $t = (CFn [] i32) here" ]));
+
   (* 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
@@ -6046,7 +6077,7 @@ let () =
   accepts "numeric? admits +"
     "(defn add [a $t b $t] $t {:where (numeric? $t)} (+ a b))";
   rejects_check "equal? does not admit <"
-    ~needle:"nothing declares t ordered?"
+    ~needle:"nothing declares $t ordered?"
     "(defn less [a $t b $t] bool {:where (equal? $t)} (< a b))";
   (* The entailments, which are the reason a signature is one predicate long
      rather than two. Every type the language orders is a number or an enum,
@@ -6074,10 +6105,10 @@ let () =
   accepts "integer? admits the shifts"
     "(defn dbl [x $t] $t {:where (integer? $t)} (<< x 1))";
   rejects_check "numeric? does not admit bit-and"
-    ~needle:"nothing declares t integer?"
+    ~needle:"nothing declares $t integer?"
     "(defn low? [x $t] bool {:where (numeric? $t)} (= (bit-and x 1) 1))";
   rejects_check "nor the shifts"
-    ~needle:"nothing declares t integer?"
+    ~needle:"nothing declares $t integer?"
     "(defn dbl [x $t] $t {:where (numeric? $t)} (<< x 1))";
   (* An integer?-bounded caller satisfies a numeric?-bounded callee: the
      entailment carries across generic calls exactly as ordered?-over-equal?