From b153f325b8f2da34793be9af3e3204f7b1a9164a Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 10:04:23 +0700 Subject: [PATCH 1/8] A declared name that starts with $ is refused where it is declared --- TODO.org | 12 ++++----- lib/parse.ml | 64 ++++++++++++++++++++++++++++++++--------------- test/test_flan.ml | 20 +++++++++++++++ 3 files changed, 70 insertions(+), 26 deletions(-) diff --git a/TODO.org b/TODO.org index a76e8535..72b62a22 100644 --- a/TODO.org +++ b/TODO.org @@ -598,12 +598,12 @@ back to the call site. Costs about 2µs a call. Rules out putting a =loc= field on the wire, and rules out structural matching of the expansion against the arguments, which can pick the wrong one of two equal subtrees. -** NEXT A declared name may carry the $ sigil -Decided 2026-09-25: refuse =$= at the start of any declared name; the refusal says =$= marks a type variable. -=(defn $foo [x i32] i32 ...)= is accepted and =($foo 3)= calls it; so is -=(defstruct $S [a i32])=, whose type can then be written nowhere. The character is -reserved in every type position and in no name. Refusing it in a declared name -would close it properly, and that is a decision about the spelling. +** DONE A declared name may carry the $ sigil +CLOSED: [2026-09-25] +A name that starts with =$= is refused where it is declared — every top-level +form, a struct or union field, an enum member, a data case and a =let= name — +saying =$= marks a type variable and naming the bare spelling. A parameter was +already refused, as a type in a name slot. * Checker diff --git a/lib/parse.ml b/lib/parse.ml index 48129474..c54c47d3 100644 --- a/lib/parse.ml +++ b/lib/parse.ml @@ -14,6 +14,22 @@ let sym (f : Form.t) = | Sym s -> s | _ -> fail f "expected a name, found %s" (Form.to_string f) +(* A name something declares. [$] opens a type variable in every type + position, so a declared name that starts with one could be written at its + definition and at a call and nowhere a type goes — [(defstruct $S ...)] is a + type no signature can name. Refused at the declaration, where the fix is. *) +let no_sigil (f : Form.t) = + match f.v with + | Sym s when String.length s > 1 && s.[0] = '$' -> + let bare = String.sub s 1 (String.length s - 1) in + Loc.failk "parse/sigil-in-name" f.loc + "%s cannot be declared: a name does not start with $, which marks a \ + type variable, as in [x $t]. Name it %s" + s bare + | _ -> () + +let dname (f : Form.t) = no_sigil f; sym f + (* Names for the temporaries this file mints — the value is bound once and everything that needs it reads *that*, so a destructuring pattern over a call calls it once and a short-circuit operand is evaluated once. [~] is a @@ -122,7 +138,7 @@ let rec fields (f : Form.t) (items : Form.t list) : Ast.field list = | [] -> [] | name :: ty :: rest -> no_pattern name; - { Ast.fname = sym name; fty = texpr ty; floc = name.loc } :: fields f rest + { Ast.fname = dname name; fty = texpr ty; floc = name.loc } :: fields f rest | [ odd ] -> Loc.fail odd.loc "field %s has no type — these come in name/type pairs" (Form.to_string odd) @@ -879,7 +895,9 @@ and temp (p : Form.t) (v : Ast.expr) : Ast.expr * Ast.binding = name is what it always was. *) and destructure (p : Form.t) (v : Ast.expr) : Ast.binding list = match p.v with - | Sym name -> [ { Ast.bname = name; bty = None; bval = v; bloc = p.loc } ] + | Sym name -> + no_sigil p; + [ { Ast.bname = name; bty = None; bval = v; bloc = p.loc } ] (* The value goes into a temporary first, so it is evaluated once however many names the pattern binds, and so that [(let [{:keys [p]} p] ...)] reads the old [p] rather than the one it is in the middle of rebinding. *) @@ -1290,17 +1308,17 @@ let rec decl (f : Form.t) : Ast.decl = | List ({ v = Sym "defalias"; _ } :: args) -> (match args with - | [ n; t ] -> mk (Ast.Defalias (sym n, texpr t)) + | [ n; t ] -> mk (Ast.Defalias (dname n, texpr t)) | _ -> fail f "defalias is (defalias Name Type)") | List ({ v = Sym "defstruct"; _ } :: args) -> (match args with - | [ n; { v = Vec fs; _ } ] -> mk (Ast.Defstruct (sym n, fields f fs)) + | [ n; { v = Vec fs; _ } ] -> mk (Ast.Defstruct (dname n, fields f fs)) | _ -> fail f "defstruct is (defstruct Name [field Type ...])") | List ({ v = Sym "defdata"; _ } :: args) -> (match args with - | [ n; { v = Vec vs; _ } ] -> mk (Ast.Defdata (sym n, List.map variant vs)) + | [ n; { v = Vec vs; _ } ] -> mk (Ast.Defdata (dname n, List.map variant vs)) | _ -> fail f "defdata is (defdata Name [(Case [field Type ...]) ...])") (* C's union: one storage, as many ways of reading it as there are members. @@ -1343,7 +1361,7 @@ let rec decl (f : Form.t) : Ast.decl = [member Type ...]). This reads as a tagged sum — write \ (defdata Name [(Case [field Type ...]) ...])") ms; - mk (Ast.Defunion (sym n, fields f ms)) + mk (Ast.Defunion (dname n, fields f ms)) | _ -> fail f "defunion is (defunion Name [member Type ...])") (* The slot after the parameters is unconditionally the return type. It used @@ -1437,7 +1455,7 @@ let rec decl (f : Form.t) : Ast.decl = (Form.to_string ret) in let fwhere, body = constraints body in - mk (Ast.Defn { Ast.name = sym n; params = []; praw = Some (pitems ps); + mk (Ast.Defn { Ast.name = dname n; params = []; praw = Some (pitems ps); ret = Some rty; fwhere; fbody = body_of body; nloc = n.loc; fprivate }) | _ -> @@ -1463,7 +1481,7 @@ let rec decl (f : Form.t) : Ast.decl = (match args with | [ n; { v = Vec slots; _ } ] -> mk (Ast.Defclass - (sym n, + (dname n, List.map (fun (s : Form.t) -> match s.v with @@ -1493,7 +1511,7 @@ let rec decl (f : Form.t) : Ast.decl = when if generic then body = [] else body <> [] -> mk ((if generic then (fun fn -> Ast.Defgeneric fn) else fun fn -> Ast.Defmulti fn) - { Ast.name = sym n; params = dyn_params which ps; praw = None; + { Ast.name = dname n; params = dyn_params which ps; praw = None; ret = Some (texpr ret); fwhere = []; fbody = body_of body; nloc = n.loc; fprivate = Ast.Exported }) | _ -> fail f "%s" usage) @@ -1539,11 +1557,11 @@ let rec decl (f : Form.t) : Ast.decl = | { v = Str csym; _ } :: rest -> (match List.rev rest with | [ n; { v = Form.Vec ps; _ } ] -> - mk (mkd { Ast.name = sym n; params = fields f ps; praw = None; + mk (mkd { Ast.name = dname n; params = fields f ps; praw = None; ret = None; fwhere = []; fbody = []; nloc = n.loc; fprivate = Ast.Exported } csym) | [ n; { v = Form.Vec ps; _ }; r ] -> - mk (mkd { Ast.name = sym n; params = fields f ps; praw = None; + mk (mkd { Ast.name = dname n; params = fields f ps; praw = None; ret = Some (texpr r); fwhere = []; fbody = []; nloc = n.loc; fprivate = Ast.Exported } csym) | _ -> fail f "%s" usage) @@ -1566,7 +1584,7 @@ let rec decl (f : Form.t) : Ast.decl = | List ({ v = Sym "defenum"; _ } :: args) -> (match args with | [ n; { v = Form.Vec ms; _ } ] -> - let ename = sym n in + let ename = dname n in (* An enum member is an [i32] at run time. [Shim] lowers the type to int32_t for C's benefit and [Check] builds every member as a [Tast.Int (v, I32)] -- but the reader hands this pass an [int64], so @@ -1613,7 +1631,8 @@ let rec decl (f : Form.t) : Ast.decl = refusals here and below can be made; neither reaches the AST. *) let rec members next = function | [] -> [] - | { v = Form.Sym m; loc } :: { v = Form.Int k; _ } :: rest -> + | ({ v = Form.Sym m; loc } as mf) :: { v = Form.Int k; _ } :: rest -> + no_sigil mf; (* The [let] is load-bearing rather than tidiness. OCaml leaves the evaluation order of [::]'s two operands unspecified and in practice takes the tail first, so an inlined [fits ... k] would @@ -1626,7 +1645,8 @@ let rec decl (f : Form.t) : Ast.decl = i32 by the time it is incremented, so the sum cannot overflow. *) let k = fits m loc ~explicit:true k in (m, k, true, loc) :: members (Int64.add k 1L) rest - | { v = Form.Sym m; loc } :: rest -> + | ({ v = Form.Sym m; loc } as mf) :: rest -> + no_sigil mf; let next = fits m loc ~explicit:false next in (m, next, false, loc) :: members (Int64.add next 1L) rest | bad :: _ -> @@ -1690,11 +1710,11 @@ let rec decl (f : Form.t) : Ast.decl = (match args with | [ n; t ] -> let ty, init = defvar3 t in - mk (Ast.Defvar (sym n, Some ty, init, kind)) + mk (Ast.Defvar (dname n, Some ty, init, kind)) | [ n; t; { v = Sym "uninit"; _ } ] -> - mk (Ast.Defvar (sym n, Some (texpr t), Ast.Uninit, kind)) + mk (Ast.Defvar (dname n, Some (texpr t), Ast.Uninit, kind)) | [ n; t; v ] -> - mk (Ast.Defvar (sym n, Some (texpr t), Ast.Init (expr v), kind)) + mk (Ast.Defvar (dname n, Some (texpr t), Ast.Init (expr v), kind)) | _ -> fail f "%s is (%s name Type value?) or (%s name value) — a third element \ @@ -1733,8 +1753,8 @@ let rec decl (f : Form.t) : Ast.decl = | List ({ v = Sym "defconst"; _ } :: args) -> (match args with - | [ n; v ] -> mk (Ast.Defconst (sym n, None, expr v)) - | [ n; t; v ] -> mk (Ast.Defconst (sym n, Some (texpr t), expr v)) + | [ n; v ] -> mk (Ast.Defconst (dname n, None, expr v)) + | [ n; t; v ] -> mk (Ast.Defconst (dname n, Some (texpr t), expr v)) | _ -> fail f "defconst is (defconst name Type? value)") (* A macro is an ordinary function, and this is where it becomes one: @@ -1764,7 +1784,7 @@ let rec decl (f : Form.t) : Ast.decl = let sg = Expand.params_of ps in let form_t = { Ast.t = Ast.Tname "Form"; tloc = f.loc } in mk (Ast.Defn - { Ast.name = sym n; + { Ast.name = dname n; (* A name the reader cannot produce -- [~] opens an unquote, so no symbol read out of a source file holds one -- which is what keeps the compiler's own parameter out of the way of @@ -1844,6 +1864,10 @@ and macro_body (sg : Expand.msig) (body : Form.t list) : Ast.expr list = [ call loc0 (s loc0 "let" :: Form.make (Form.Vec items) loc0 :: body) ] and variant (f : Form.t) : Ast.variant = + (match f.v with + | Sym _ -> no_sigil f + | List (n :: _) -> no_sigil n + | _ -> ()); match f.v with | Sym n -> { Ast.vname = n; vfields = []; vloc = f.loc } | List [ { v = Sym n; _ }; { v = Vec fs; _ } ] -> diff --git a/test/test_flan.ml b/test/test_flan.ml index d39a06df..26ef0703 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -6323,6 +6323,26 @@ let () = (defn main [] () (add2 1 2))" []; + (* ── A declared name does not start with $ ─────────────────────── *) + (* $ marks a type variable in every type position, so a name that starts + with one could not be written where a type goes. *) + let sigil what src = + parse_rejects ("a declared name with a $: " ^ what) src + ~needle:"a name does not start with $, which marks a type variable" + in + sigil "defn" "(defn $foo [x i32] i32 (+ x 1))"; + sigil "defstruct" "(defstruct $S [a i32])"; + sigil "a struct field" "(defstruct S [$a i32])"; + sigil "defenum" "(defenum $E [A B])"; + sigil "an enum member" "(defenum E [A $B])"; + sigil "defonce" "(defonce $g i32 0)"; + sigil "defconst" "(defconst $k 3)"; + sigil "defdata case" "(defdata D [($C [a i32])])"; + sigil "defmacro" "(defmacro $m [x] x)"; + sigil "a let binding" "(defn f [] i32 (let [$y 1] y))"; + parse_rejects "the $ refusal names the bare spelling" + "(defn $foo [x i32] i32 x)" ~needle:"Name it foo"; + (* ── The acceptance program checks end to end ──────────────────── *) accepts "calc-me.flan type checks" (In_channel.with_open_bin "../calc-me.flan" In_channel.input_all); From 4a292b5a73c99bf3f205ac220cdb69864bd20a04 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 10:07:22 +0700 Subject: [PATCH 2/8] f64-inf, f64-nan, f32-inf and f32-nan are constants the compiler supplies --- TODO.org | 19 +++++++++++++------ lib/check.ml | 25 +++++++++++++++++++++++-- lib/prelude.ml | 6 +++--- test/programs/limits.flan | 10 ++++++++++ test/test_acceptance.ml | 4 +++- 5 files changed, 52 insertions(+), 12 deletions(-) diff --git a/TODO.org b/TODO.org index 72b62a22..779108ac 100644 --- a/TODO.org +++ b/TODO.org @@ -138,12 +138,19 @@ big-endian bytes, which is how the hex literal reads. Two and not one with a wider operand because the intrinsic takes a single repeated byte: the byte fill is one instruction and the four-byte pattern is a loop on both backends. -** NEXT There is no literal for an infinity or a NaN -Decided 2026-09-25: four constants the compiler supplies, =f64-inf=, =f64-nan=, =f32-inf=, =f32-nan=, beside =f64-max= and the rest. Negative infinity is =(- f64-inf)=. Rules out Clojure's =##Inf= reader literal. -=lib/reader.ml= has no literal for either, and =float_repr= prints =inf= and =nan= -as words the reader will not read back. =(/ 1.0 0.0)= is the only route to an -infinity, and the constant folder is integers only, so it cannot be a =defconst=. -Closing it needs a reader literal or a float-capable folding pass. +** DONE There is no literal for an infinity or a NaN +CLOSED: [2026-09-25] +=f64-inf=, =f64-nan=, =f32-inf= and =f32-nan= are names the checker supplies +(=Check.special_float=), reached only after every local, global and function has +missed, so a program's own binding of one wins. Negative infinity is +=(- 0.0 f64-inf)=: the decision wrote =(- f64-inf)=, and there is no unary minus. +Rules out Clojure's =##Inf= reader literal. + +** TODO (!= x x) is false for a NaN +=!== on floats is LLVM's ordered =one= on both backends (=lib/emit.ml= =fcmp_op=, +=lib/x86.ml= =float_cc=), so =(!= f64-nan f64-nan)= is =false= where C, Odin and +IEEE 754 say =true=; =(not (= x x))= is the only NaN test that works. Changing it +to =une= is a decision about what =!== means. ** DONE A u64 constant above 2^63 cannot be written in decimal CLOSED: [2026-09-25] diff --git a/lib/check.ml b/lib/check.ml index 64e43869..a54b3ad6 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1598,6 +1598,17 @@ let defvar_neither env loc ~form gname n ~values ~cases = asked "is this name declared at all", so a global that is itself a defonce still undecided belongs on it: what it resolves to is the next pass's question, not this one's. *) +(* The infinities and NaNs, which the reader has no literal for and the + integer-only constant folder cannot compute, so the compiler supplies them + beside the prelude's f64-max and the rest. Negative infinity is + [(- f64-inf)]. *) +let special_float = function + | "f64-inf" -> Some (Float.infinity, Types.F64) + | "f64-nan" -> Some (Float.nan, Types.F64) + | "f32-inf" -> Some (Float.infinity, Types.F32) + | "f32-nan" -> Some (Float.nan, Types.F32) + | _ -> None + (* Case name -> the data type it belongs to, read off the declarations rather than out of [env.cases]: this runs inside [collect], which has registered the data type *names* by here but not resolved their cases, so the table @@ -1689,7 +1700,9 @@ let settle_defvars env (decls : Ast.decl list) : Ast.decl list = end else begin (match t.Ast.t with - | Ast.Tname s when not (List.mem s (Lazy.force values)) -> + | Ast.Tname s + when not (List.mem s (Lazy.force values)) + && special_float s = None -> defvar_neither env t.Ast.tloc ~form n s ~values:(Lazy.force values) ~cases:(Lazy.force cases) | _ -> ()); @@ -1982,6 +1995,7 @@ let mk loc ty e : Tast.expr = { Tast.e; ty; loc } let unit_at loc = mk loc Types.Unit Tast.Unit + (* The environment for a lifted body, built once its own body has been checked and [caught] is therefore final. spec-memory.md's case 2, and the whole of its machinery. @@ -3928,7 +3942,14 @@ and var ctx ?(qualified = false) loc ~want name = expect ctx loc ~want (mk loc (Types.CFn (params, ret)) (Tast.FnAddr (Tast.Fnval name))) - | None -> unknown_name ctx loc name) + | None -> + (* The float constants no literal can write, reached only once + every table above has missed, so a program's own binding of + one of these names is the one it gets. *) + match special_float name with + | Some (x, k) -> + expect ctx loc ~want (mk loc (Types.Float k) (Tast.Float (x, k))) + | None -> unknown_name ctx loc name) (* What remains of spec-memory.md's ownership section after the repeals of 2026-09-18 is the allocator's side alone: the region rule decides where a diff --git a/lib/prelude.ml b/lib/prelude.ml index 29dbfe74..dee1d391 100644 --- a/lib/prelude.ml +++ b/lib/prelude.ml @@ -713,9 +713,9 @@ let source = {flan| ;; ;; Every decimal below is the shortest one that round-trips to the exact value ;; intended, and each is pinned against an independent derivation in -;; test/programs/limits.flan rather than trusted. There is no infinity or NaN -;; constant, and there cannot be one written down: the reader has no literal -;; for either. (/ 1.0 0.0) is the only way to reach an infinity today. +;; test/programs/limits.flan rather than trusted. The infinities and NaNs, +;; f64-inf, f64-nan, f32-inf and f32-nan, are not here: no literal writes one, +;; so the checker supplies them (Check.special_float). (defconst f32-max f32 3.4028234663852886e38) (defconst f64-max f64 1.7976931348623157e308) (defconst f32-min-positive f32 1.1754943508222875e-38) diff --git a/test/programs/limits.flan b/test/programs/limits.flan index 6c430826..bd284465 100644 --- a/test/programs/limits.flan +++ b/test/programs/limits.flan @@ -118,4 +118,14 @@ (< (- (f32 0.0) f32-max) (- (f32 0.0) f32-min-positive))) (say "f64's least value negates its greatest" (< (- 0.0 f64-max) (- 0.0 f64-min-positive))) + + ;; The infinities and NaNs, which no literal writes. Each infinity is the + ;; overflow of its type's greatest value, negated it is below the least + ;; finite one, and a NaN is the one value not equal to itself. + (say "f64-inf" (= f64-inf (* f64-max 2.0))) + (say "f32-inf" (= f32-inf (* f32-max (f32 2.0)))) + (say "f64-inf negated" (< (- 0.0 f64-inf) (- 0.0 f64-max))) + (say "f32-inf negated" (< (- (f32 0.0) f32-inf) (- (f32 0.0) f32-max))) + (say "f64-nan" (not (= f64-nan f64-nan))) + (say "f32-nan" (not (= f32-nan f32-nan))) 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index eb357e3b..92894d95 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -5283,7 +5283,9 @@ level "1" f32-max is the last finite f32 ok\n\ f64-max is the last finite f64 ok\n\ f32's least value negates its greatest ok\n\ - f64's least value negates its greatest ok\n" + f64's least value negates its greatest ok\n\ + f64-inf ok\nf32-inf ok\nf64-inf negated ok\nf32-inf negated ok\n\ + f64-nan ok\nf32-nan ok\n" in outputs "type limits" "programs/limits.flan" limits_out; outputs ~opt:"-O0" "type limits, -O0" "programs/limits.flan" limits_out; From d006a8b4807b3236907cc0b9fd0ceb41457af224 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 10:14:24 +0700 Subject: [PATCH 3/8] An array literal's first element types the rest, constant arithmetic folds at a bounded type variable, and a pointer or a plain union takes a byte fill --- TODO.org | 38 +++++----- lib/check.ml | 100 ++++++++++++++++++------- test/programs/array-first-element.flan | 14 ++++ test/programs/fill-ptr-union.flan | 18 +++++ test/programs/generic-fold.flan | 11 +++ test/test_acceptance.ml | 20 +++++ test/test_flan.ml | 33 +++++--- 7 files changed, 179 insertions(+), 55 deletions(-) create mode 100644 test/programs/array-first-element.flan create mode 100644 test/programs/fill-ptr-union.flan create mode 100644 test/programs/generic-fold.flan diff --git a/TODO.org b/TODO.org index 779108ac..a9614cdd 100644 --- a/TODO.org +++ b/TODO.org @@ -659,19 +659,20 @@ it would entail =ordered?= and =equal?= and not =numeric?=, so the cast rule becomes a disjunction and the refusal has to name whichever the reader meant. Each part of that is a decision and the author has not been asked. -** NEXT The Ptr and union arms of the fill boundary are relaxable -Decided 2026-09-25: relax both. A =Ptr= may be byte-filled, a poisoned pointer being the useful case, and an untagged union is filled over its whole size. -What may be byte-filled is numbers, and structs and fixed arrays of numbers. -A =Ptr= is refused so the rule stays one sentence, and an untagged union -because the walk goes over a struct's fields rather than a union's members. -Both are named in the decision as the arms to relax first if it is reopened, -and a poisoned pointer is arguably the useful case. +** DONE The Ptr and union arms of the fill boundary are relaxable +CLOSED: [2026-09-25] +A =Ptr= may be byte-filled, and an untagged union is filled over its whole +size when every member may be, its members walked as a struct's fields are; a +union with a =dyn= member is refused naming the =dyn=. Everything else the rule +refused it still refuses. -** NEXT A compound constant expression at a bounded type variable -Decided 2026-09-25: fold constant integer arithmetic before the bounded-variable literal check, so =(+ x (+ 1 2))= is accepted where =(+ x 3)= is. -=(+ x (+ 1 2))= at a bounded variable is refused where =(+ x 3)= works — the -literal arm admits a bare constant and nothing folds the compound first. -Walk-backable, so it waits until a body actually wants it. +** DONE A compound constant expression at a bounded type variable +CLOSED: [2026-09-25] +Integer arithmetic over literals alone (=Check.literal_arith=) is folded to the +literal it computes wherever a type variable is wanted, so =(+ x (+ 1 2))= is +admitted exactly where =(+ x 3)= is. A defconst's name does not fold, since it +has a type of its own. The instantiation checks the form unfolded, at its +concrete type. ** DONE Generics by monomorphisation, checked abstractly, with where predicates CLOSED: [2026-09-13] @@ -896,13 +897,12 @@ ordinary expressions and the builtin reads the type back out of one type an expression cannot hold, such as =(Fn [i32] ())=, is parsed as =Ast.TypeArg=. Rules out a type expression anywhere else in expression position. -** NEXT An array literal cannot say it is [f32] -Decided 2026-09-25: the first element's type carries to the rest, so =[(f32 1.0) 2.5]= is an =[f32]=; that is refused today and is a bug. No =1.0f= suffix for now. -A float literal defaults to =f64=, an array literal has no context, and a =let= -has no annotation. Same shape as =(vec-new [u8])= and probably the same fix. -Not the same fix: a bracket literal has no argument to put a type in. Decision: -how a literal names its element type — a spelling of its own, or a =let= -annotation. +** DONE An array literal cannot say it is [f32] +CLOSED: [2026-09-25] +With nothing outside an array literal naming its element type, the first +element's type is the want for the rest, so =[(f32 1.0) 2.5]= is a =[2 f32]=. A +refusal of a later element carries a note at the first saying it set the type. +Rules out a =1.0f= suffix for now. ** NEXT A let binding takes no type annotation Decided 2026-09-25: =(the T expr)=, Common Lisp's special operator, gives any expression its want; checked at compile time like any other want, and it compiles to nothing. =let= is unchanged. On a =dyn= operand it is refused, naming the cast. The refusals that say "annotate the binding" — =None=, an empty =[]=, and =(zeroed)=/=(filled)=/=(dead-beef)= with no want — suggest it instead, because today their suggestion cannot compile. diff --git a/lib/check.ml b/lib/check.ml index a54b3ad6..678c19db 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1082,29 +1082,30 @@ let rec no_zeroed_fn loc what (t : Types.t) = - [string] and a slice. Two words, the second of which is a length every bounds check believes. A filled length is a bounds check that passes and an access that does not. - - [Ptr]. Not walked by the collector, and a poisoned pointer is arguably - the useful case — but it is still a value every [deref] in the language - trusts, and admitting it would make the rule "plain data, except one - kind of address". Kept out so the rule is one sentence. This is the arm - to relax first if the question is reopened. - [bool]. The one refusal that is about the backends rather than the runtime: a bool is a byte here and an [i1] to LLVM, which reads the low bit, where x86 compares the whole byte against zero. 0xDE is false on one and true on the other, and byte-identical behaviour across the two backends is the property this feature is pinned on. - - an enum, a data type, a union, an [(Option T)], a function value. Each + - an enum, a data type, an [(Option T)], a function value. Each carries a tag or a case index that something later reads as a small number with a meaning, and a filled one names a case that does not exist. Floats are in: every bit pattern is a float, NaNs included, and both - backends move one as bytes. *) + backends move one as bytes. So is a [Ptr], which the collector does not + walk and whose poisoned value is the useful case, and an untagged union + whose members are all admitted, filled over its whole size. *) let rec unfillable env seen (t : Types.t) : Types.t option = match t with - | Types.Int _ | Types.Float _ -> None + | Types.Int _ | Types.Float _ | Types.Ptr _ -> None | Types.Array (_, e) -> unfillable env seen e | Types.Named n when not (List.mem n seen) -> - (match Hashtbl.find_opt env.structs n with + (match + match Hashtbl.find_opt env.structs n with + | Some s -> Some s + | None -> Hashtbl.find_opt env.unions n + with | Some s -> List.fold_left (fun acc (fl : Tast.field) -> @@ -1112,9 +1113,8 @@ let rec unfillable env seen (t : Types.t) : Types.t option = | Some _ -> acc | None -> unfillable env (n :: seen) fl.Tast.fty) None s.Tast.fields - (* A data type or a union, which are the two [Named] things that are not - in [structs]. Both overlay their members, so the type itself is what - the refusal names. *) + (* A data type, the one [Named] thing in neither table: its tag names a + case, so the type itself is what the refusal names. *) | None -> Some t) | _ -> Some t @@ -1995,6 +1995,30 @@ let mk loc ty e : Tast.expr = { Tast.e; ty; loc } let unit_at loc = mk loc Types.Unit Tast.Unit +(* Integer arithmetic over literals alone, folded. Unlike [const_int] no name + is read: a defconst has a type of its own, and only an untyped constant may + stand at a type variable. *) +let rec literal_arith (e : Ast.expr) : int64 option = + match e.Ast.e with + | Ast.Int n -> Some n + | Ast.Call ({ Ast.e = Ast.Var op; _ }, x :: y :: rest) -> + let step a b = + match op with + | "+" -> Some (Int64.add a b) + | "-" -> Some (Int64.sub a b) + | "*" -> Some (Int64.mul a b) + | "/" when b <> 0L -> Some (Int64.div a b) + | "%" when b <> 0L && rest = [] -> Some (Int64.rem a b) + | _ -> None + in + List.fold_left + (fun acc e -> + match acc, literal_arith e with + | Some a, Some b -> step a b + | _ -> None) + (literal_arith x) (y :: rest) + | _ -> None + (* The environment for a lifted body, built once its own body has been checked and [caught] is therefore final. spec-memory.md's case 2, and the whole of @@ -3597,6 +3621,14 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr = | Ast.ArrayFill (dims, v) -> check_array_fill ctx ~want loc dims v | Ast.ArrayGen (dims, f) -> check_array_gen ctx ~want loc dims f | Ast.Match (scrutinee, arms) -> check_match ctx ~tail ?want loc scrutinee arms + (* Constant integer arithmetic where a type variable is wanted is folded to + the literal it computes first, so [(+ x (+ 1 2))] is admitted wherever + [(+ x 3)] is. The instantiation re-checks the form unfolded, at a concrete + type, where the ordinary arithmetic is fine. *) + | Ast.Call ({ Ast.e = Ast.Var ("+" | "-" | "*" | "/" | "%"); _ }, _) + when (match want with Some (Types.Var _) -> true | _ -> false) + && literal_arith e <> None -> + int_literal loc ~want ~preds:ctx.env.tvpreds (Option.get (literal_arith e)) | Ast.Call (head, args) -> check_call ctx ~want loc head args | Ast.Unwrap (Ast.Usome, v) -> (* Unwrap Some, else early-return None from the enclosing function, so the @@ -5426,7 +5458,34 @@ and check_arr ctx ~want loc items = | Some (Types.Slice t) -> Some t | _ -> None in - let items = map_lr (fun i -> check ctx ?want:elem_want i) items in + (* With nothing outside saying what the elements are, the first one says: + [[(f32 1.0) 2.5]] is an [[2 f32]], its [2.5] checked at [f32] the way it + would be at an [f32] parameter. *) + let items = + match elem_want, items with + | Some _, _ | None, [] -> map_lr (fun i -> check ctx ?want:elem_want i) items + | None, first :: rest -> + let first = check ctx first in + let want = + match first.Tast.ty with Types.Never -> None | t -> Some t + in + (* A refusal of the element itself says where its type came from. *) + let one (i : Ast.expr) = + try check ctx ?want i with + | Loc.Error d when d.Loc.dloc = i.Ast.loc && want <> None -> + raise + (Loc.Error + { d with + Loc.notes = + d.Loc.notes + @ [ Loc.note first.Tast.loc + (Printf.sprintf + "this array's first element is %s, so every \ + element is" + (Types.to_string first.Tast.ty)) ] }) + in + first :: map_lr one rest + in let n = Int64.of_int (List.length items) in let elem = match elem_want, items with @@ -7160,8 +7219,8 @@ and named_call ?(qualified = false) ctx ~want loc name args = | Some bad -> Loc.failk "check/fill-not-plain-data" loc "%s writes raw bytes over %s, and %s is not plain data — %s. \ - Fill only numbers, and structs and fixed arrays built out of \ - them" + Fill only numbers and pointers, and structs, unions and fixed \ + arrays built out of them" name (Types.to_string ty) (if Types.equal bad ty then "it" else Types.to_string bad) (match bad with @@ -7173,8 +7232,6 @@ and named_call ?(qualified = false) ctx ~want loc name args = a filled header frees a wild address" | Types.String | Types.Slice _ -> "it is a pointer and a length every bounds check believes" - | Types.Ptr _ -> - "it is an address every deref trusts" | Types.Bool -> "a bool is an i1 to LLVM and a whole byte to the x86 backend, \ so a filled one would not even agree with itself across the \ @@ -7188,15 +7245,6 @@ and named_call ?(qualified = false) ctx ~want loc name args = | Types.Named n when Hashtbl.mem ctx.env.datas n -> "it carries a tag that names a case, and no byte pattern \ names a real one" - | Types.Named n when Hashtbl.mem ctx.env.unions n -> - (* Untagged, per [env.unions]'s own note — so the reason is - not a tag. It is that a union's members overlay, and this - rule walks a struct's fields rather than a union's members: - nothing here has shown they are all plain data, and a - member that is not would be filled through the one that - is. *) - "a union's members overlay, and this rule does not walk them \ - — so nothing here has shown that every member is plain data" | Types.Enum _ -> "an enum's values are the members it declared, and no byte \ pattern is one of them" diff --git a/test/programs/array-first-element.flan b/test/programs/array-first-element.flan new file mode 100644 index 00000000..a667a60a --- /dev/null +++ b/test/programs/array-first-element.flan @@ -0,0 +1,14 @@ +;;;; An array literal with nothing outside it saying what its elements are +;;;; takes that from its first element: [(f32 1.0) 2.5] is a [2 f32], and the +;;;; 2.5 is an f32 literal rather than an f64 refused for not being one. +(defn sum3 [a [3 f32]] f32 (+ (at a 0) (at a 1) (at a 2))) + +(defn main [] i32 + (let [a [(f32 1.0) 2.5 3.25] + b [(i64 1) 2 3] + c [(u8 1) 255]] + (println (length a)) + (println (sum3 a)) + (println (+ (at b 1) (i64 9000000000))) + (println (at c 1))) + 0) diff --git a/test/programs/fill-ptr-union.flan b/test/programs/fill-ptr-union.flan new file mode 100644 index 00000000..5e9d2d73 --- /dev/null +++ b/test/programs/fill-ptr-union.flan @@ -0,0 +1,18 @@ +;;;; A pointer and an untagged union take a byte fill. The union is filled +;;;; over its whole size, so its widest member reads back every byte; the +;;;; pointer is read back through a union that overlays it with a u64, since +;;;; there is no other way to see an address as a number. +(defunion U [a u32 b [8 u8]]) +(defunion W [p (Ptr i32) n u64]) + +(defn main [] i32 + (let [u (array 1 U)] + (set u (filled 0xAB)) + (println (.a (at u 0))) ; 2880154539 + (println (at (.b (at u 0)) 7))) ; 171 + (let [w (array 1 W)] + (set (.p (at w 0)) (dead-beef)) + (println (.n (at w 0))) ; 17275436393656397278 + (set (at w 0) (filled 0x01)) + (println (.n (at w 0)))) ; 72340172838076673 + 0) diff --git a/test/programs/generic-fold.flan b/test/programs/generic-fold.flan new file mode 100644 index 00000000..cddcedb9 --- /dev/null +++ b/test/programs/generic-fold.flan @@ -0,0 +1,11 @@ +;;;; Constant integer arithmetic stands where a bounded type variable is +;;;; wanted, as the single literal it folds to would. +(defn f [x $t] t {:where (numeric? $t)} (+ x (* 2 (+ 1 2)))) +(defn g [x $t] t {:where (integer? $t)} (- x (% 7 4))) + +(defn main [] i32 + (println (f 4)) ; 10 + (println (f (u8 250))) ; 0, u8 arithmetic wrapping + (println (f 1.5)) ; 7.5 + (println (g (i64 10))) ; 7 + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 92894d95..45947b76 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -529,6 +529,26 @@ let () = outputs "a u64 constant in decimal" "programs/u64-decimal.flan" u64_out; outputs ~x86:true "a u64 constant in decimal, x86" "programs/u64-decimal.flan" u64_out; + (* Constant arithmetic folds before a bounded variable checks it. *) + let fold_out = "10\n0\n7.5\n7\n" in + outputs "constant arithmetic at a bounded variable" + "programs/generic-fold.flan" fold_out; + outputs ~x86:true "constant arithmetic at a bounded variable, x86" + "programs/generic-fold.flan" fold_out; + (* A pointer and an untagged union take a byte fill. *) + let fpu_out = + "2880154539\n171\n17275436393656397278\n72340172838076673\n" in + outputs "a pointer and a union filled" "programs/fill-ptr-union.flan" + fpu_out; + outputs ~x86:true "a pointer and a union filled, x86" + "programs/fill-ptr-union.flan" fpu_out; + (* An array literal takes its element type from its first element when + nothing outside it names one. *) + let first_out = "3\n6.75\n9000000002\n255\n" in + outputs "an array literal's first element types the rest" + "programs/array-first-element.flan" first_out; + outputs ~x86:true "an array literal's first element types the rest, x86" + "programs/array-first-element.flan" first_out; (* into. The count of pulls is the assertion a unit test cannot make: one pass, one call per element per stage it reaches, and no intermediate collection anywhere. The two show lines either side of it are the same diff --git a/test/test_flan.ml b/test/test_flan.ml index 26ef0703..6da7418c 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -2852,10 +2852,9 @@ let () = rejects_check "a string cannot be filled" "(defn f [] () (let [s \"hi\"] (set s (filled 0xFF))))" ~needle:"a length every bounds check believes"; - rejects_check "a pointer field cannot be filled" + accepts "a pointer field may be filled" "(defstruct S [p (Ptr i32)]) \ - (defn f [] () (let [s (S {})] (set s (filled 0xFF))))" - ~needle:"an address every deref trusts"; + (defn f [] () (let [s (S {})] (set s (filled 0xFF))))"; (* The one refusal that is about the two backends rather than the runtime: LLVM reads a bool's low bit and x86 compares the whole byte, so 0xDE is false on one and true on the other. Byte-identical behaviour across the @@ -2864,15 +2863,17 @@ let () = rejects_check "a bool cannot be filled" "(defn f [] () (let [b false] (set b (filled 0xFF))))" ~needle:"would not even agree with itself"; - (* Each of the tagged and address-carrying types names its own reason. They - shared one "it carries a tag that names a case" line until review caught - that it was false for two of them — a union is untagged (env.unions is - "the untagged unions") and a function value is a code pointer, not a - tag. Pinned per type so the reasons cannot quietly re-merge. *) - rejects_check "a union cannot be filled, and not because of a tag" + (* An untagged union is filled over its whole size when every member may be + filled, and refused for the member that may not. *) + accepts "a union of numbers may be filled" "(defunion U [a i32 b f64]) \ + (defn f [] () (let [u (U {})] (set u (dead-beef))))"; + rejects_check "a union with a dyn member cannot be filled" + "(defunion U [a i32 d dyn]) \ (defn f [] () (let [u (U {})] (set u (dead-beef))))" - ~needle:"a union's members overlay"; + ~needle:"a root pointing at nothing"; + (* Each of the tagged and address-carrying types names its own reason, so + the reasons cannot quietly merge into one that is false for some. *) rejects_check "a function value cannot be filled" "(defn g [] ()) (defn f [] () (let [h g] (set h (dead-beef))))" ~needle:"it is a code address"; @@ -6343,6 +6344,18 @@ let () = parse_rejects "the $ refusal names the bare spelling" "(defn $foo [x i32] i32 x)" ~needle:"Name it foo"; + (* ── An array literal's first element types the rest ───────────── *) + accepts "an f32 array literal from its first element" + "(defn main [] i32 (let [a [(f32 1.0) 2.5]] (i32 (length a))))"; + (match checked "(defn main [] i32 (let [a [(u8 1) 256]] 0))" with + | _ -> check "an element that does not fit the first element's type" false + | exception Loc.Error d -> + check "the refusal says the first element set the type" + (List.exists + (fun (n : Loc.note) -> + contains n.Loc.nmsg "this array's first element is u8") + d.Loc.notes)); + (* ── The acceptance program checks end to end ──────────────────── *) accepts "calc-me.flan type checks" (In_channel.with_open_bin "../calc-me.flan" In_channel.input_all); From dd160aa31b06b3d5065326a5edab3e04509b9d6f Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 10:19:09 +0700 Subject: [PATCH 4/8] A return computes its value before it runs its defers --- TODO.org | 12 ++++++------ docs/BUILT.md | 3 ++- lib/check.ml | 34 +++++++++++++++++++++++++++------ test/programs/return-defer.flan | 32 +++++++++++++++++++++++++++++++ test/test_acceptance.ml | 8 ++++++++ web/index.html | 7 ++++--- 6 files changed, 80 insertions(+), 16 deletions(-) create mode 100644 test/programs/return-defer.flan diff --git a/TODO.org b/TODO.org index a9614cdd..6ab697d9 100644 --- a/TODO.org +++ b/TODO.org @@ -339,12 +339,12 @@ a =defer= in one always registers. A loop body and a branch are still refused by name: =defer= is a compile-time construct with the cleanup copied into every exit path, so "maybe registered" is not expressible. -** TODO A return runs its defers before it computes its value -=(return v)= is lowered as =Do (defers @ [Return v])= (=lib/check.ml= near 3474), -so a defer that changes what =v= reads changes the answer, and =(return x)= and -falling off the end with =x= disagree. All backends agree with each other. The -value is computed first and the defers run after, the order Odin, Go and Zig -use. +** DONE A return runs its defers before it computes its value +CLOSED: [2026-09-25] +=(return v)= computes =v= into a slot, then runs the defers registered so far, +then returns the slot — the order falling off the end already had, and Odin's, Go's +and Zig's. One lowering in =Check=, so every backend has it. A value of type +=Never= is still returned directly, since nothing after it runs. ** DONE edn reads into a struct and answers a dynamic value CLOSED: [2026-09-17] diff --git a/docs/BUILT.md b/docs/BUILT.md index 930c83da..c3dbc372 100644 --- a/docs/BUILT.md +++ b/docs/BUILT.md @@ -19,7 +19,8 @@ assignable, which makes the generated step its only writer. **Amended** by the s **`defer`** is recognised in `check_fn` and nowhere else, because that is the only place that knows a form is at the top level of a function body. Each one is checked in place, then registered on the context; it emits nothing where it stands. Function exit runs them innermost-first, and an explicit `return` runs the ones registered *above* it — a defer -written below a return has not executed yet and must not fire. A trap runs none of them, which follows from the +written below a return has not executed yet and must not fire. Both compute the returned value into a slot first and +run the defers after it, Odin's, Go's and Zig's order, so a defer that changes a returned local does not change the answer. A trap runs none of them, which follows from the bounds-check shape (`noreturn` then `unreachable`) rather than being a separate decision. **Amended** once a bounds failure became a signal: an *answered* one leaves through the unwind path and runs them like any other transfer, an unanswered one still runs none. See "An index out of range is a condition" at the foot of this file. diff --git a/lib/check.ml b/lib/check.ml index 678c19db..2ddd068d 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -3535,12 +3535,34 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr = None | Some v -> Some (check ctx ~want:ctx.ret v) in - (* Whatever has been deferred *so far* runs first: a defer written below - this return has not executed yet and must not fire. *) - let r = mk loc Types.Never (Tast.Return v) in - (match ctx.defers with - | [] -> r - | ds -> mk loc Types.Never (Tast.Do (ds @ [ r ]))) + (* The value is computed first, then whatever has been deferred *so far* + runs, then the function returns — the order the fall-off-the-end path + in [check_fn] has, so [(return x)] and a last form [x] agree. A defer + written below this return has not executed yet and must not fire. *) + (match ctx.defers, v with + | [], _ -> mk loc Types.Never (Tast.Return v) + | ds, Some (value : Tast.expr) + when not (Types.equal value.Tast.ty Types.Never + || Types.equal value.Tast.ty Types.Unit) -> + let s = fresh_slot ctx value.Tast.ty in + let r = + mk loc Types.Never + (Tast.Return (Some (mk loc value.Tast.ty (Tast.Local s)))) + in + mk loc Types.Never (Tast.Let ([ (s, value) ], ds @ [ r ])) + (* A unit value has nothing to keep, and is still evaluated first. *) + | ds, Some value when Types.equal value.Tast.ty Types.Unit -> + mk loc Types.Never + (Tast.Do + ((value :: ds) + @ [ mk loc Types.Never (Tast.Return (Some (unit_at loc))) ])) + (* A value that never arrives is computed first too, and the defers + after it are unreachable: a trap runs none, and a transfer out of it + runs the function's [fdefers]. *) + | _, Some _ -> mk loc Types.Never (Tast.Return v) + | ds, None -> + mk loc Types.Never + (Tast.Do (ds @ [ mk loc Types.Never (Tast.Return None) ]))) (* (set (at target i) x) against a dyn target — a dyn vec from (vec-new dyn), or a typed container's own view (M2 item 3) — is a call and not a place: [flan_dyn_set_at] tag-checks [x]'s dyn tag against what the vec diff --git a/test/programs/return-defer.flan b/test/programs/return-defer.flan new file mode 100644 index 00000000..0909169b --- /dev/null +++ b/test/programs/return-defer.flan @@ -0,0 +1,32 @@ +;;;; A return computes its value first and then runs the defers registered +;;;; so far, so (return x) and a last form x answer the same thing even when +;;;; a defer changes x. +(defstruct P [a i32 b i32]) + +(defn early [] i32 + (let [x 1] + (defer (set x 2)) + (return x))) + +(defn fall [] i32 + (let [x 1] + (defer (set x 2)) + x)) + +(defn agg [flag bool] P + (let [p (P {.a 1 .b 1})] + (defer (set p (P {.a 9 .b 9})) (println "deferred")) + (when flag (return p)) + (P {.a 5 .b 5}))) + +(defn unit [] () + (defer (println "second")) + (return (println "first"))) + +(defn main [] i32 + (println (early)) ; 1 + (println (fall)) ; 1 + (println (.a (agg true))) ; deferred, then 1 + (println (.a (agg false))) ; deferred, then 5 + (unit) ; first, then second + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 45947b76..2a1c6a28 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -529,6 +529,14 @@ let () = outputs "a u64 constant in decimal" "programs/u64-decimal.flan" u64_out; outputs ~x86:true "a u64 constant in decimal, x86" "programs/u64-decimal.flan" u64_out; + (* A return computes its value before it runs the defers. *) + let rd_out = "1\n1\ndeferred\n1\ndeferred\n5\nfirst\nsecond\n" in + outputs "a return computes its value before its defers" + "programs/return-defer.flan" rd_out; + outputs ~opt:"-O0" "a return computes its value before its defers, -O0" + "programs/return-defer.flan" rd_out; + outputs ~x86:true "a return computes its value before its defers, x86" + "programs/return-defer.flan" rd_out; (* Constant arithmetic folds before a bounded variable checks it. *) let fold_out = "10\n0\n7.5\n7\n" in outputs "constant arithmetic at a bounded variable" diff --git a/web/index.html b/web/index.html index 791be8c7..7584f36e 100644 --- a/web/index.html +++ b/web/index.html @@ -1107,9 +1107,10 @@ not found

defer

-

A defer runs at function exit, innermost first. An explicit -return runs the ones registered above it — a defer written below a return -has not executed yet and must not fire.

+

A defer runs at function exit, innermost first, after the value the +function returns has been computed. An explicit return runs the ones +registered above it — a defer written below a return has not executed yet and must +not fire.

(defn work [n i32] i32
   (defer (println "second"))

From 6c9635cd53188e1f33c4801533d1f7bcef37ba89 Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 10:26:03 +0700
Subject: [PATCH 5/8] A wide literal is refused for its range as an enum
 member, names the u64 cast where a dyn is wanted, and comes back wide from a
 macro

---
 TODO.org          | 20 +++++++++++++++++---
 lib/check.ml      |  6 ++++++
 lib/expand.ml     | 30 ++++++++++++++++++++++++++----
 lib/parse.ml      | 10 ++++++++++
 test/test_flan.ml | 19 +++++++++++++++++++
 5 files changed, 78 insertions(+), 7 deletions(-)

diff --git a/TODO.org b/TODO.org
index 6ab697d9..c94d08a4 100644
--- a/TODO.org
+++ b/TODO.org
@@ -161,9 +161,23 @@ in the spelling it was written in. Hex with the top bit set was accepted as a
 negative at any integer type before this; it is refused now too. A negative
 decimal is still a =u64= bit pattern. A cast's integer literal that does not fit
 =i32= is checked at the cast's type; one that fits keeps the =i32= default, so
-=(u32 -1)= still means what it did. A wide literal that passes through a macro
-comes back as an ordinary =Int=, because the macro side's =Form= has one integer
-case. Rules out a second integer case in the prelude's =Form=.
+=(u32 -1)= still means what it did. A wide literal passed to a macro as an
+argument comes back wide: it crosses as an =Int= with a token in the unused
+second payload word (=Expand.wides=). Rules out a second integer case in the
+prelude's =Form=.
+
+** DONE A wide literal's follow-ups: an enum member, a dyn want, a macro
+CLOSED: [2026-09-25]
+=(defenum E [A 0xFFFFFFFFFFFFFFFF])= gets the enum range refusal in the spelling
+written. A wide literal where a =dyn= is wanted names =(u64 ...)= and says the dyn
+holds it as the i64 with the same bits. A wide literal passed through a macro is
+refused or accepted exactly as it would be unexpanded.
+
+** TODO A wide literal written inside a quasiquote comes back as an i64
+=(defmacro w [] `(+ 1 0xFFFFFFFFFFFFFFFF))= expands to =(+ 1 -1)= and prints 0:
+=Expand.quote= builds =(Form.Int {.i ...})= from the pattern, and a Form built in
+Flan has no way to carry the token an argument crosses with. At a =u64= want the
+pattern is the right value, so a refusal would break the one reading that works.
 
 ** DONE {.row .col} binds same-named locals
 CLOSED: [2026-09-20]
diff --git a/lib/check.ml b/lib/check.ml
index 2ddd068d..40a65e3c 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -3846,6 +3846,12 @@ and wide_literal loc ~want n s =
       "%s does not fit in i32, the type an integer literal takes when nothing \
        says otherwise — write (u64 %s) for a u64"
       s s
+  | Some Types.Dyn ->
+    Loc.failk literal_at_want loc
+      "expected dyn, found the integer literal %s, which only a u64 holds — a \
+       dyn integer is an i64. Write (u64 %s) for the u64, which a dyn holds as \
+       the i64 with the same bits, %Ld"
+      s s n
   | Some other ->
     Loc.failk literal_at_want loc
       "expected %s, found the integer literal %s, which only a u64 holds"
diff --git a/lib/expand.ml b/lib/expand.ml
index 98bbfe94..8ecc3754 100644
--- a/lib/expand.ml
+++ b/lib/expand.ml
@@ -78,6 +78,19 @@ let tag_of_int = function
 
 type sites = (Dynload.addr, Loc.t) Hashtbl.t
 
+(* ── A wide literal's round trip ───────────────────────────────────
+   A macro's [Form] has one integer case, so a literal at or above 2^63 crosses
+   as its bit pattern in [Int]'s payload. What marks it as wide is the second
+   payload word, which [Int] does not use and which a macro that passes the
+   form through copies along with the rest of its 24 bytes: [write] puts a
+   token there naming the literal's spelling in this table, and [unmarshal]
+   turns a node carrying one back into the [UInt] that went in. An [Int] the
+   macro built itself has no token, and is the [Int] it says it is. One table
+   per call, as [sites] is. *)
+let wide_mark = 0x5749444500000000L
+
+let wides : (int64, int64 * string) Hashtbl.t ref = ref (Hashtbl.create 1)
+
 (* Into an existing 24 bytes, which is what an argument array needs: the macro
    takes a [Form] slice, and a slice is contiguous elements and not an array of
    pointers — so this writes *into* memory the caller took, and every caller
@@ -114,9 +127,13 @@ let rec write (sites : sites) p (f : Form.t) =
   | Form.Kw s -> str TKw s
   | Form.Str s -> str TStr s
   | Form.Int i -> tag TInt; Dynload.poke_i64 p payload i
-  (* A macro's Form has one integer case, so a wide literal crosses as its
-     pattern and comes back as an ordinary [Int]. *)
-  | Form.UInt (i, _) -> tag TInt; Dynload.poke_i64 p payload i
+  (* Crosses as an [Int] carrying a token; see [wides]. *)
+  | Form.UInt (i, text) ->
+    tag TInt;
+    Dynload.poke_i64 p payload i;
+    let token = Int64.logor wide_mark (Int64.of_int (Hashtbl.length !wides)) in
+    Hashtbl.replace !wides token (i, text);
+    Dynload.poke_i64 p len_off token
   | Form.Float x -> tag TFloat; Dynload.poke_f64 p payload x
   | Form.Byte b -> tag TByte; Dynload.poke_i32 p payload (Int32.of_int b)
   | Form.List xs -> seq TList xs
@@ -167,7 +184,11 @@ let rec unmarshal ~(sites : sites) ~loc (p : Dynload.addr) : Form.t =
       unmarshal ~sites ~loc (Nativeint.add b (Nativeint.of_int (i * form_size))))
   in
   match tag_of_int (Dynload.peek_i32 p 0) with
-  | TInt -> Form.make (Form.Int (Dynload.peek_i64 p payload)) loc
+  | TInt ->
+    let i = Dynload.peek_i64 p payload in
+    (match Hashtbl.find_opt !wides (Dynload.peek_i64 p len_off) with
+     | Some (w, text) when Int64.equal w i -> Form.make (Form.UInt (i, text)) loc
+     | _ -> Form.make (Form.Int i) loc)
   | TFloat -> Form.make (Form.Float (Dynload.peek_f64 p payload)) loc
   | TByte ->
     Form.make (Form.Byte (Int32.to_int (Dynload.peek_i32 p payload) land 0xff)) loc
@@ -191,6 +212,7 @@ let call ~loc (fn : Dynload.addr) (args : Form.t list) : Form.t =
      handed to a second allocation while the table still holds it, and the
      table is dropped the moment this returns either way. *)
   let sites : sites = Hashtbl.create 8 in
+  wides := Hashtbl.create 1;
   let a = Dynload.take (max (n * form_size) 1) in
   List.iteri
     (fun i x -> write sites (Nativeint.add a (Nativeint.of_int (i * form_size))) x)
diff --git a/lib/parse.ml b/lib/parse.ml
index c54c47d3..931caf4d 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -1645,6 +1645,16 @@ let rec decl (f : Form.t) : Ast.decl =
               i32 by the time it is incremented, so the sum cannot overflow. *)
            let k = fits m loc ~explicit:true k in
            (m, k, true, loc) :: members (Int64.add k 1L) rest
+         (* At or above 2^63, so its [int64] is a bit pattern and not the
+            number written; refused in the spelling it was written in. *)
+         | ({ v = Form.Sym m; _ } as mf) :: { v = Form.UInt (_, text); loc = vloc }
+           :: _ ->
+           no_sigil mf;
+           Loc.failk "parse/enum-value-out-of-range" vloc
+             "the member %s of %s is %s, which does not fit i32 — an enum's \
+              members run from -2147483648 to 2147483647. Give %s a value in \
+              that range, or use a defconst"
+             m ename text m
          | ({ v = Form.Sym m; loc } as mf) :: rest ->
            no_sigil mf;
            let next = fits m loc ~explicit:false next in
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 6da7418c..758848c1 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -6356,6 +6356,25 @@ let () =
              contains n.Loc.nmsg "this array's first element is u8")
           d.Loc.notes));
 
+  (* ── A wide literal's follow-ups ──────────────────────────────── *)
+  parse_rejects "a wide enum member is refused for its range"
+    "(defenum E [A 0xFFFFFFFFFFFFFFFF B])"
+    ~needle:"the member A of E is 0xFFFFFFFFFFFFFFFF, which does not fit i32";
+  rejects_check "a wide literal in a dyn global names the u64 cast"
+    "(defonce big 0xFFFFFFFFFFFFFFFF)"
+    ~needle:"Write (u64 0xFFFFFFFFFFFFFFFF) for the u64";
+  accepts "the cast the dyn refusal names compiles"
+    "(defonce big (u64 0xFFFFFFFFFFFFFFFF))";
+  (* A macro's Form has one integer case; the literal comes back wide all the
+     same, and is refused where it would have been refused unexpanded. *)
+  rejects_check "a wide literal through a macro is still wide"
+    "(defmacro idm [x] x) \
+     (defn f [] i32 (+ 1 (idm 0xFFFFFFFFFFFFFFFF)))"
+    ~needle:"0xFFFFFFFFFFFFFFFF does not fit in i32";
+  accepts "a wide literal through a macro is still a u64"
+    "(defmacro idm [x] x) \
+     (defn f [] u64 (idm 18446744073709551615))";
+
   (* ── The acceptance program checks end to end ──────────────────── *)
   accepts "calc-me.flan type checks"
     (In_channel.with_open_bin "../calc-me.flan" In_channel.input_all);

From 83b244475a9a0af788715f76926a744e3d1b8e08 Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 10:30:52 +0700
Subject: [PATCH 6/8] A refusal that suggests a fix suggests one that compiles,
 for vec-new, map-new and a near miss that is a value

---
 TODO.org          |  8 ++++++++
 lib/check.ml      | 34 ++++++++++++++++++++++++++++++----
 test/test_flan.ml | 22 ++++++++++++++++++++++
 3 files changed, 60 insertions(+), 4 deletions(-)

diff --git a/TODO.org b/TODO.org
index c94d08a4..2c65948b 100644
--- a/TODO.org
+++ b/TODO.org
@@ -1034,6 +1034,14 @@ should not pay for identity and metadata. Not implemented.
 function nosuch" twice at the same place and counts 2 errors — once from the
 abstract pass and once from the instantiation.
 
+** 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";
+they name the type arguments alone, and =(the T expr)= joins them when it lands.
+An unknown call whose near miss is a value — =(context-allocator)= against
+=context/allocator=, or a global — says the name is a value written without
+parentheses, and names no call at all when the call had arguments.
+
 * Backends
 
 ** DONE The x86 backend tracks LLVM at -O0
diff --git a/lib/check.ml b/lib/check.ml
index 40a65e3c..34c05c4d 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -6751,7 +6751,7 @@ and vec_new_elem ctx ~want loc args =
      | _ ->
        fail loc
          "nothing here says what (vec-new) is a Vec of — write the element \
-          type, as (vec-new i32), or give the binding a type")
+          type, as (vec-new i32)")
 
 (* A type written as an argument to vec-new or map-new, read back out of the
    expression Parse made of it. Only the shapes that cannot be a value there:
@@ -6817,18 +6817,18 @@ and map_new_types ctx ~want loc args =
   | a :: _ when type_of_expr a <> None ->
     fail loc
       "(map-new) names a key and no value — write both, as (map-new string \
-       i32), or give the binding a type"
+       i32)"
   | { Ast.e = Ast.Var k; _ } :: rest when is_type k && rest = [] ->
     fail loc
       "(map-new %s) names a key and no value — write both, as (map-new %s \
-       i32), or give the binding a type" k k
+       i32)" k k
   | _ ->
     (match want with
      | Some (Types.Map (k, v)) -> k, v, args
      | _ ->
        fail loc
          "nothing here says what (map-new) maps — write the key and value \
-          types, as (map-new string i32), or give the binding a type")
+          types, as (map-new string i32)")
 
 (* The element type, or the reason this is not a Vec. *)
 and vec_elem loc what (t : Types.t) =
@@ -9219,7 +9219,33 @@ and ordinary_call ctx ~want loc name args =
           | Some _ as m -> m
           | None -> if capitalised then near_miss ctx.env name else None
         in
+        (* A near miss that names a value rather than a function is still the
+           near miss, but [(m)] would be refused in its turn, so the sentence
+           says how that name is written instead. *)
+        let callable m =
+          let fn_ty = function
+            | Types.Fn _ | Types.CFn _ | Types.Dyn -> true
+            | _ -> false
+          in
+          match lookup ctx m with
+          | Some b -> fn_ty b.bty
+          | None ->
+            match Hashtbl.find_opt ctx.env.globals m with
+            | Some (ty, _) -> fn_ty ty
+            | None ->
+              not (List.mem m [ "true"; "false"; "nil"; "None";
+                                "context/allocator"; "context/temp" ])
+        in
         match guess with
+        | Some m when not (callable m) ->
+          if args = [] then
+            Loc.failk "check/unknown-function" loc
+              "unknown function %s — did you mean %s? It is a value and not a \
+               function, so it is written without parentheses" name m
+          else
+            Loc.failk "check/unknown-function" loc
+              "unknown function %s. The nearest name, %s, is a value and not a \
+               function" name m
         | Some m ->
           Loc.failk "check/unknown-function" loc
             "unknown function %s — did you mean %s?" name m
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 758848c1..b24cb9f6 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -6375,6 +6375,28 @@ let () =
     "(defmacro idm [x] x) \
      (defn f [] u64 (idm 18446744073709551615))";
 
+  (* ── Suggestions that compile ─────────────────────────────────── *)
+  (* A let binding has no type slot, so the refusal names only the spelling
+     that works. *)
+  rejects_check "vec-new with no element type names only the type argument"
+    "(defn f [] i32 (let [v (vec-new)] 0))"
+    ~needle:"as (vec-new i32)";
+  (match checked "(defn f [] i32 (let [m (map-new)] 0))" with
+   | _ -> check "map-new with no types is refused" false
+   | exception Loc.Error d ->
+     check "map-new's refusal does not suggest a binding type"
+       (not (contains d.Loc.dmsg "binding")));
+  (* The near miss is a value, and is suggested without the parentheses that
+     would make it a refused call. *)
+  rejects_check "a near miss that is a value says it is written bare"
+    "(defn f [] i32 (let [a (context-allocator)] 0))"
+    ~needle:"did you mean context/allocator? It is a value and not a function";
+  accepts "the bare spelling that refusal names compiles"
+    "(defn f [] i32 (let [a context/allocator] 0))";
+  rejects_check "a near miss that is a function keeps the plain suggestion"
+    "(defn foo [] i32 1) (defn f [] i32 (fooo))"
+    ~needle:"did you mean foo?";
+
   (* ── The acceptance program checks end to end ──────────────────── *)
   accepts "calc-me.flan type checks"
     (In_channel.with_open_bin "../calc-me.flan" In_channel.input_all);

From 222dc0ae90ff141d565297ca38fc3351ecffcfde Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 10:37:43 +0700
Subject: [PATCH 7/8] A loop, dotimes, match, macro, class or generic binding
 that starts with $ is refused too

---
 TODO.org          | 7 ++++---
 lib/parse.ml      | 9 +++++----
 test/test_flan.ml | 7 +++++++
 3 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/TODO.org b/TODO.org
index 2c65948b..07921c14 100644
--- a/TODO.org
+++ b/TODO.org
@@ -622,9 +622,10 @@ arguments, which can pick the wrong one of two equal subtrees.
 ** DONE A declared name may carry the $ sigil
 CLOSED: [2026-09-25]
 A name that starts with =$= is refused where it is declared — every top-level
-form, a struct or union field, an enum member, a data case and a =let= name —
-saying =$= marks a type variable and naming the bare spelling. A parameter was
-already refused, as a type in a name slot.
+form, a struct or union field, an enum member, a data case, a class slot, and a
+=let=, =loop=, =dotimes=, =match=, macro or generic binding — saying =$= marks a
+type variable and naming the bare spelling. A =defn= parameter was already
+refused, as a type in a name slot.
 
 * Checker
 
diff --git a/lib/parse.ml b/lib/parse.ml
index 931caf4d..1f626ec4 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -177,6 +177,7 @@ and dyn_params which (items : Form.t list) : Ast.field list =
     (fun (it : Form.t) ->
        match it.v with
        | Sym s ->
+         no_sigil it;
          { Ast.fname = s;
            fty = { Ast.t = Ast.Tname "dyn"; tloc = it.loc };
            floc = it.loc }
@@ -554,7 +555,7 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
            { Ast.dstart = Some start; dstop = stop; dstep = Some step }
          | _ -> assert false
        in
-       mk (Ast.Dotimes (lbl, sym n, b, body_of body))
+       mk (Ast.Dotimes (lbl, dname n, b, body_of body))
      | _ ->
        fail f
          "dotimes is (dotimes [name stop] body ...), \
@@ -800,7 +801,7 @@ and loop_bindings f (items : Form.t list) : (string * Ast.expr) list =
     | [] -> []
     | name :: value :: rest ->
       no_pattern name;
-      (sym name, expr value) :: go rest
+      (dname name, expr value) :: go rest
     | [ odd ] ->
       Loc.fail odd.loc
         "binding %s has no value — loop takes name/value pairs"
@@ -1237,7 +1238,7 @@ and pattern (f : Form.t) : Ast.pattern =
       member member
   | List ({ v = Sym ctor; _ } :: binds) ->
     List.iter no_pattern binds;
-    Ast.Pctor (ctor, List.map sym binds)
+    Ast.Pctor (ctor, List.map dname binds)
   | _ -> fail f "expected a pattern, found %s" (Form.to_string f)
 
 (* ── The third element of a defonce or a def ───────────────────────────
@@ -1485,7 +1486,7 @@ let rec decl (f : Form.t) : Ast.decl =
               List.map
                 (fun (s : Form.t) ->
                    match s.v with
-                   | Sym name -> (name, s.loc)
+                   | Sym name -> no_sigil s; (name, s.loc)
                    | _ ->
                      fail s
                        "a class slot is a name — its value is dyn, so there \
diff --git a/test/test_flan.ml b/test/test_flan.ml
index b24cb9f6..72e259af 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -6341,6 +6341,13 @@ let () =
   sigil "defdata case" "(defdata D [($C [a i32])])";
   sigil "defmacro" "(defmacro $m [x] x)";
   sigil "a let binding" "(defn f [] i32 (let [$y 1] y))";
+  sigil "a dotimes counter" "(defn f [] () (dotimes [$i 3] (println i)))";
+  sigil "a loop binding" "(defn f [] i32 (loop [$i 0] i))";
+  sigil "a match bind"
+    "(defdata D [(C [a i32])]) (defn f [d D] i32 (match d (D.C $x) x))";
+  sigil "a macro parameter" "(defmacro m [$x] x)";
+  sigil "a class slot" "(defclass K [$s])";
+  sigil "a generic's parameter" "(defgeneric area [$s] f64)";
   parse_rejects "the $ refusal names the bare spelling"
     "(defn $foo [x i32] i32 x)" ~needle:"Name it foo";
 

From 2f3544e7f5082a61ebae4addf624a86f4e4295c3 Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 10:53:52 +0700
Subject: [PATCH 8/8] Code after a return emits nothing, a wide element names
 the u64 array, and $ is refused in fn, handler, :keys and & binders

---
 TODO.org                        |  8 ++++++--
 lib/check.ml                    | 31 +++++++++++++++++++++++++++++++
 lib/emit.ml                     |  5 +++++
 lib/parse.ml                    | 14 +++++++++-----
 test/programs/return-defer.flan | 15 +++++++++++++++
 test/test_acceptance.ml         |  3 ++-
 test/test_flan.ml               | 16 ++++++++++++++++
 7 files changed, 84 insertions(+), 8 deletions(-)

diff --git a/TODO.org b/TODO.org
index 3b48464f..5c04b881 100644
--- a/TODO.org
+++ b/TODO.org
@@ -358,7 +358,10 @@ CLOSED: [2026-09-25]
 =(return v)= computes =v= into a slot, then runs the defers registered so far,
 then returns the slot — the order falling off the end already had, and Odin's, Go's
 and Zig's. One lowering in =Check=, so every backend has it. A value of type
-=Never= is still returned directly, since nothing after it runs.
+=Never= is still returned directly, since nothing after it runs. The LLVM
+emitter emits nothing after a terminator (=Emit.value= answers =poison= once the
+block is closed); a bounds check in dead code used to reopen the block and
+reference an operand it never wrote.
 
 ** DONE edn reads into a struct and answers a dynamic value
 CLOSED: [2026-09-17]
@@ -625,7 +628,8 @@ arguments, which can pick the wrong one of two equal subtrees.
 CLOSED: [2026-09-25]
 A name that starts with =$= is refused where it is declared — every top-level
 form, a struct or union field, an enum member, a data case, a class slot, and a
-=let=, =loop=, =dotimes=, =match=, macro or generic binding — saying =$= marks a
+=let=, =:keys=, =&=, =loop=, =dotimes=, =match=, =fn=, handler clause, macro or
+generic binding — saying =$= marks a
 type variable and naming the bare spelling. A =defn= parameter was already
 refused, as a type in a name slot.
 
diff --git a/lib/check.ml b/lib/check.ml
index e7e43c83..c005ef73 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -5484,12 +5484,34 @@ and check_arr ctx ~want loc items =
     match elem_want, items with
     | Some _, _ | None, [] -> map_lr (fun i -> check ctx ?want:elem_want i) items
     | None, first :: rest ->
+      let first_ast = first in
       let first = check ctx first in
       let want =
         match first.Tast.ty with Types.Never -> None | t -> Some t
       in
       (* A refusal of the element itself says where its type came from. *)
       let one (i : Ast.expr) =
+        (match i.Ast.e, want with
+         | Ast.UInt (_, text), Some (Types.Int k) when k <> Types.U64 ->
+           let first_src =
+             match first_ast.Ast.e with
+             | Ast.Int _ | Ast.Byte _ -> Some (spell_arg "" first_ast)
+             | _ -> None
+           in
+           Loc.failk literal_at_want i.Ast.loc
+             ~notes:
+               [ Loc.note first.Tast.loc
+                   (Printf.sprintf
+                      "this array's first element is %s, so every element is"
+                      (Types.ikind_name k)) ]
+             "%s does not fit in %s, and only a u64 holds it%s" text
+             (Types.ikind_name k)
+             (match first_src with
+              | Some f ->
+                Printf.sprintf " — write the first element as (u64 %s) for an \
+                                array of u64" f
+              | None -> " — make the first element a u64 for an array of u64")
+         | _ -> ());
         try check ctx ?want i with
         | Loc.Error d when d.Loc.dloc = i.Ast.loc && want <> None ->
           raise
@@ -11015,8 +11037,17 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn =
      run them — it is [noreturn] and then [unreachable] — and that is the same
      rule the bounds checks already follow. *)
   let body =
+    let ends_never =
+      match List.rev body with
+      | (last : Tast.expr) :: _ -> Types.equal last.Tast.ty Types.Never
+      | [] -> false
+    in
     match ctx.defers with
     | [] -> body
+    (* A body that never falls off the end — its last form a [return], say —
+       has no fall-off path to put the defers on, and a copy of them there is
+       code after a terminator. *)
+    | _ when ends_never -> body
     | ds when Types.equal ret Types.Unit -> body @ ds
     | ds ->
       (* The result is computed before the defers run and returned after, so it
diff --git a/lib/emit.ml b/lib/emit.ml
index 08aff1c6..f0f75d57 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -1950,6 +1950,11 @@ let fcmp_op = function
    a child -- the branch at the end of an [if], the store of a [set] -- are
    attributed to the parent and not to whatever ran last inside it. *)
 let rec value f (e : Tast.expr) : string =
+  (* Code after a terminator — past a [return], a [break] or a trap — is never
+     reached and is not emitted: a form in it that opens blocks of its own, a
+     bounds check say, would reopen the dead block and branch on operands
+     [ins] never wrote. Nothing reads the answer. *)
+  if not f.live then "poison" else
   let v =
     match f.dsub with
     | None -> value_at f e
diff --git a/lib/parse.ml b/lib/parse.ml
index 1f626ec4..c380830b 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -535,7 +535,7 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
     (match args with
      | { v = Vec ps; _ } :: body ->
        List.iter no_pattern ps;
-       mk (Ast.Fn (List.map sym ps, body_of body))
+       mk (Ast.Fn (List.map dname ps, body_of body))
      | _ -> fail f "fn is (fn [param ...] body ...)")
 
   (* One, two or three bounds. The stop is always the last one written, so the
@@ -620,8 +620,10 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
     in
     let clause (c : Form.t) =
       match c.Form.v with
-      | Form.List (ty :: { v = Form.Vec [ { v = Form.Sym n; _ } ]; _ } :: cbody)
+      | Form.List (ty :: { v = Form.Vec [ ({ v = Form.Sym n; _ } as nf) ]; _ }
+                   :: cbody)
         when cbody <> [] ->
+        no_sigil nf;
         { Ast.hty = texpr ty; hname = n; hbody = List.map expr cbody;
           hloc = c.Form.loc }
       | _ ->
@@ -650,8 +652,10 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
     in
     let clause (c : Form.t) =
       match c.Form.v with
-      | Form.List (ty :: { v = Form.Vec [ { v = Form.Sym n; _ } ]; _ } :: cbody)
+      | Form.List (ty :: { v = Form.Vec [ ({ v = Form.Sym n; _ } as nf) ]; _ }
+                   :: cbody)
         when cbody <> [] ->
+        no_sigil nf;
         { Ast.hty = texpr ty; hname = n; hbody = List.map expr cbody;
           hloc = c.Form.loc }
       | _ -> fail c "a handler-case clause is (Type [name] body ...)"
@@ -965,7 +969,7 @@ and dmap (p : Form.t) (t : Ast.expr) (items : Form.t list) : Ast.binding list =
         | (n : Form.t) :: more ->
           let name =
             match n.v with
-            | Sym s -> s
+            | Sym s -> no_sigil n; s
             | _ ->
               Loc.fail n.loc
                 ":keys binds field names, and %s is not one — a nested pattern \
@@ -1051,7 +1055,7 @@ and dvec (p : Form.t) (t : Ast.expr) (items : Form.t list) : Ast.binding list =
          is a local and outlives the body that reads it. Nothing new. *)
       let name =
         match r.v with
-        | Sym s -> s
+        | Sym s -> no_sigil r; s
         | _ ->
           Loc.fail r.loc
             "& binds one name for the tail, and %s is not one — the tail is a \
diff --git a/test/programs/return-defer.flan b/test/programs/return-defer.flan
index 0909169b..0b51f6ee 100644
--- a/test/programs/return-defer.flan
+++ b/test/programs/return-defer.flan
@@ -23,10 +23,25 @@
   (defer (println "second"))
   (return (println "first")))
 
+(defn arr [] [3 i32]
+  (let [a [1 2 3]]
+    (defer (set (at a 0) 9))
+    (return a)))
+
+;;;; Code after a return is never reached, and a bounds check in it is not
+;;;; emitted as though it were.
+(defn dead [] i32
+  (let [a [1 2 3]]
+    (return 7)
+    (at a 0)))
+
 (defn main [] i32
   (println (early))              ; 1
   (println (fall))               ; 1
   (println (.a (agg true)))      ; deferred, then 1
   (println (.a (agg false)))     ; deferred, then 5
   (unit)                         ; first, then second
+  (let [r (arr)]
+    (println (at r 0) (at r 1) (at r 2)))   ; 1 2 3
+  (println (dead))               ; 7
   0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 8a00ad0a..6afb0bc7 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -530,7 +530,8 @@ let () =
     outputs ~x86:true "a u64 constant in decimal, x86"
       "programs/u64-decimal.flan" u64_out;
     (* A return computes its value before it runs the defers. *)
-    let rd_out = "1\n1\ndeferred\n1\ndeferred\n5\nfirst\nsecond\n" in
+    let rd_out =
+      "1\n1\ndeferred\n1\ndeferred\n5\nfirst\nsecond\n1 2 3\n7\n" in
     outputs "a return computes its value before its defers"
       "programs/return-defer.flan" rd_out;
     outputs ~opt:"-O0" "a return computes its value before its defers, -O0"
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 72e259af..d7857883 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -6348,6 +6348,16 @@ let () =
   sigil "a macro parameter" "(defmacro m [$x] x)";
   sigil "a class slot" "(defclass K [$s])";
   sigil "a generic's parameter" "(defgeneric area [$s] f64)";
+  sigil "an fn parameter" "(defn f [] i32 (let [g (fn [$a] $a)] 0))";
+  sigil "a handler-case binder"
+    "(defstruct E [n i32]) \
+     (defn f [] i32 (handler-case 1 [(E [$c] 2)]))";
+  sigil "a handler-bind binder"
+    "(defstruct E [n i32]) \
+     (defn f [] i32 (handler-bind [(E [$c] (println 1))] 1))";
+  sigil "a :keys name"
+    "(defstruct P [a i32]) (defn f [p P] i32 (let [{:keys [$a]} p] a))";
+  sigil "a & tail" "(defn f [xs [3 i32]] i32 (let [[a & $r] xs] a))";
   parse_rejects "the $ refusal names the bare spelling"
     "(defn $foo [x i32] i32 x)" ~needle:"Name it foo";
 
@@ -6382,6 +6392,12 @@ let () =
     "(defmacro idm [x] x) \
      (defn f [] u64 (idm 18446744073709551615))";
 
+  rejects_check "a wide element after a narrow first names the u64 array"
+    "(defn main [] i32 (let [a [1 18446744073709551615]] 0))"
+    ~needle:"write the first element as (u64 1) for an array of u64";
+  accepts "the u64 array that refusal names compiles"
+    "(defn main [] i32 (let [a [(u64 1) 18446744073709551615]] 0))";
+
   (* ── Suggestions that compile ─────────────────────────────────── *)
   (* A let binding has no type slot, so the refusal names only the spelling
      that works. *)