From 7794f06f00b8145c6e010aec895061267e8ec43b Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Mon, 21 Sep 2026 10:08:31 +0700 Subject: [PATCH] The same mistake was wearing two faces, and neither named the fix MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ($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 | 39 +++++++++++++++++++++++--------- lib/check.ml | 57 ++++++++++++++++++++++++++++++++++++++++------- test/test_flan.ml | 17 ++++++++++++-- 3 files changed, 92 insertions(+), 21 deletions(-) diff --git a/FIX.org b/FIX.org index 7cbde82..3d89077 100644 --- a/FIX.org +++ b/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 -takes flan_dyn_vec_new and flan_dyn_push with the roots pushed, because the -substitution happens before the element type is looked at. +has no layout for a Var and would die if it were. + +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 -allocator" — and the refusal lands on the generic body, at the line that wrote -[$t a], not at the call site that chose dyn. That is right as a decision and -thin as a message: the source says [$t] and the message says [dyn] with -nothing between them. Naming the instantiation would need the substitution -threaded into it; not done here. +Two diagnostics came with it, because the fix left the same mistake wearing +two faces. [($u x)] was an unknown function where [(vec-new $u)] in the same +body was an unbound variable, so the cast arm took the sigil clause too. And +the unbound-sigil message said "write the concrete type here" in a signature +that introduces one: it names the variables that *are* bound now, read from +[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 -under "Mechanical" as remaining work. They landed. +Found while widening the cast arm and left alone: a *declared name* may carry +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. diff --git a/lib/check.ml b/lib/check.ml index 619095b..1e81d34 100644 --- a/lib/check.ml +++ b/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 - global, a [let] annotation. There is nowhere for it to bind, so it is - the error rather than a variable with no scope. *) - Loc.failk "check/unbound-type-variable" loc - "%s introduces a type variable, and only a defn signature can — write \ - the concrete type here" n + (* A sigil on a name nothing binds. Two different mistakes wear the same + spelling, and which one it is turns on whether any variable is in 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. *) - | _ when tyvar_in_scope ctx.env name && List.length args = 1 -> + produces a number, so [numeric?] is what admits it. + + 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 diff --git a/test/test_flan.ml b/test/test_flan.ml index e7a6c86..e6f55dc 100644 --- a/test/test_flan.ml +++ b/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