The same mistake was wearing two faces, and neither named the fix

($u x) was an unknown function in the same body where (vec-new $u) was an
unbound type variable, because the cast arm did not take the sigil clause
type_named took. It takes it now, so one mistake has one story.

And the story was a rule rather than an answer: "only a defn signature can"
is what to say when nothing is in scope to name — a struct field, a global —
but inside a signature that introduces $t, the name that was meant is almost
always t. It names them. Which names those are comes from tyvars abstractly
and from subst inside an instantiation, because a body is checked under both
and reading one would answer the same mistake two ways in a single run.

FIX.org

@@ -4768,9 +4768,12 @@ Broken and fixed: [(vec-new $t)], [(vec-new $t a)], [(map-new $k $v)],
 Size and alignment come from the copy: the i32 instantiation of [sorted] emits
 flan_vec_init with 4/4 and the f64 one with 8/8, and flan_dev_reg_note_vec
 with 4 and 8. The abstract pass holds [Var t] and is never emitted — emit.ml
-has no layout for a Var and would die if it were. Instantiated at dyn the copy
+has no layout for a Var and would die if it were.
-takes flan_dyn_vec_new and flan_dyn_push with the roots pushed, because the
+
-substitution happens before the element type is looked at.
+The dyn question does not arise: a generic is not instantiated at dyn at all
+any more, and the refusal says to reach for the dyn side instead. So no copy
+of one of these bodies can reach the dyn container, and the branch in vec-new
+that picks it is unreachable from here.
 
 test/programs/generic-alloc.flan is the motivating program end to end;
 x86 matches LLVM on it.
@@ -4779,12 +4782,26 @@ docs/SPIKE-GENERICS.md already specified this — "Both spellings are accepted
 at a use" — so the doc was right and check.ml was the divergence. No doc
 change; the tests are what now hold the claim up.
 
-Left: (vec-new $t a) instantiated at dyn is refused — "(vec-new dyn) takes no
+Two diagnostics came with it, because the fix left the same mistake wearing
-allocator" — and the refusal lands on the generic body, at the line that wrote
+two faces. [($u x)] was an unknown function where [(vec-new $u)] in the same
-[$t a], not at the call site that chose dyn. That is right as a decision and
+body was an unbound variable, so the cast arm took the sigil clause too. And
-thin as a message: the source says [$t] and the message says [dyn] with
+the unbound-sigil message said "write the concrete type here" in a signature
-nothing between them. Naming the instantiation would need the substitution
+that introduces one: it names the variables that *are* bound now, read from
-threaded into it; not done here.
+[tyvars] abstractly and from [subst] inside an instantiation, so one run does
+not answer the same mistake two ways. Where none is in scope — a struct field,
+a global — it is still the rule, because there is no answer to give.
 
-Also left: docs/SPIKE-GENERICS.md still lists map-new, zeroed and the casts
+Found while widening the cast arm and left alone: a *declared name* may carry
-under "Mechanical" as remaining work. They landed.
+the sigil. [(defn $foo [x i32] i32 ...)] is accepted and [($foo 3)] calls it;
+so is [(defstruct $S [a i32])], and [($S 3)] constructs one — though the type
+[$S] cannot be written anywhere, so nothing can hold the result but a let.
+The character is reserved in every type position and in no name, so the cast
+arm declines a name a binding, a struct or a defn already claims rather than
+assume it is a type. That is one decline per table a name can be declared in,
+and the arm sits above every one of them: [ordinary_call] and, last in
+[named_call], [positional_struct]. Refusing the sigil in a declared name
+would close it properly; that is a decision about the spelling and not this
+lane's to make.
+
+Left: docs/SPIKE-GENERICS.md still lists map-new, zeroed and the casts under
+"Mechanical" as remaining work. They landed.

lib/check.ml

@@ -1039,12 +1039,34 @@ and resolve_name env ~seen loc n =
   | None ->
   if List.mem bare env.tyvars then Types.Var bare
   else if n <> bare then
-    (* A sigil somewhere that is not a [defn] signature: a struct field, a
+    (* A sigil on a name nothing binds. Two different mistakes wear the same
-       global, a [let] annotation. There is nowhere for it to bind, so it is
+       spelling, and which one it is turns on whether any variable is in scope
-       the error rather than a variable with no scope. *)
+       at all. Where none is — a struct field, a global, a [let] annotation —
+       there is nowhere for a variable to bind and the fix is a concrete type.
+       Where some are, the name is almost always a variable that was
+       introduced once and spelled differently the second time, and the fix is
+       one of the names that *is* bound. Naming them is the difference between
+       a rule and an answer.
+
+       Which names those are is read from [tyvars] during the abstract pass and
+       from [subst] inside an instantiation, because the instantiation clears
+       the first and fills the second — and a body is checked under both, so
+       reading only one of them would answer the same mistake two ways in a
+       single run. *)
+    (match (match env.tyvars with [] -> List.map fst env.subst | vs -> vs) with
+     | [] ->
        Loc.failk "check/unbound-type-variable" loc
          "%s introduces a type variable, and only a defn signature can — write \
           the concrete type here" n
+     | [ v ] ->
+       Loc.failk "check/unbound-type-variable" loc
+         "nothing binds the type variable %s — this signature introduces %s, \
+          so write %s here, or a concrete type" n v v
+     | vars ->
+       Loc.failk "check/unbound-type-variable" loc
+         "nothing binds the type variable %s — this signature introduces %s, \
+          so write one of those here, or a concrete type"
+         n (String.concat " and " vars))
   else
   match Types.ikind_of_name n with
   | Some k -> Types.Int k
@@ -8030,8 +8052,27 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      concrete target, so the copy casts to a real type and the emitter sees
      nothing unusual. During the abstract pass the target is [Var t] and the
      [where] clause is what says the cast means anything at all: a cast
-     produces a number, so [numeric?] is what admits it. *)
+     produces a number, so [numeric?] is what admits it.
-  | _ when tyvar_in_scope ctx.env name && List.length args = 1 ->
+
+     A sigil on a name nothing binds comes here too, for the reason
+     [type_named] takes one: the character is only ever written where a type
+     goes, so [resolve_name] gets to say that a variable has no binding site
+     outside a defn signature. Otherwise [($u x)] would be an unknown function
+     in the same body where [(vec-new $u)] is an unbound variable — one
+     mistake told two ways.
+
+     Only where nothing else claims the name, though. Nothing stops a defn, a
+     struct or a binding from carrying the character, and a call to one is a
+     call and not a type: this arm sits above the arms that would have found
+     it — [ordinary_call] and, last of all, [positional_struct] — so it has to
+     decline first, once per table a name can be declared in. *)
+  | _ when (tyvar_in_scope ctx.env name
+            || (name <> tyvar_bare name
+                && lookup ctx name = None
+                && not (Hashtbl.mem ctx.env.structs name)
+                && not (Hashtbl.mem ctx.env.fns name)
+                && not (Hashtbl.mem ctx.env.gsigs name)))
+           && List.length args = 1 ->
     let target = resolve_name ctx.env ~seen:[] loc name in
     unconstrained ctx.env loc ("a cast to " ^ name) ~needs:"numeric?" target;
     let a = check ctx (List.hd args) in

test/test_flan.ml

@@ -5675,10 +5675,23 @@ let () =
     ~needle:"nothing here says what (vec-new) is a Vec of"
     "(defn f [x $t] i32 (do x (let [v (vec-new)] (free v) 0)))";
   (* And a sigil on a name nothing binds is answered as the unbound variable
-     it is, rather than as a missing element type. *)
+     it is, rather than as a missing element type — with the names that *are*
+     bound, because inside a signature that introduces one the mistake is
+     nearly always the second spelling of the first. *)
   rejects_check "vec-new over a sigil that names no variable in scope"
-    ~needle:"only a defn signature can"
+    ~needle:"this signature introduces t, so write t here"
     "(defn f [x $t] i32 (do x (let [v (vec-new $u)] (free v) 0)))";
+  rejects_check "and a cast over one tells the same story"
+    ~needle:"this signature introduces t, so write t here"
+    "(defn f [x i32  d $t] $t {:where (numeric? $t)} (do d ($u x)))";
+  rejects_check "two variables in scope are both named"
+    ~needle:"introduces t and u, so write one of those"
+    "(defn f [a $t  b $u] i32 (do a b (let [v (vec-new $w)] (free v) 0)))";
+  (* Where no variable is in scope there is none to name, and the answer is
+     the rule: a sigil binds, and only a defn signature is a binding site. *)
+  rejects_check "a sigil in a struct field, where nothing can bind one"
+    ~needle:"only a defn signature can"
+    "(defstruct S [v $t])";
 
   (* ── The builtin table against the arms it describes ──────────────
      [Check.builtins] is what the editor's C-c C-v and M-. read for a name no