diff --git a/TODO.org b/TODO.org
index 045ac539..9ca06d9c 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]
@@ -154,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]
@@ -332,12 +353,15 @@ 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. 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]
@@ -600,12 +624,14 @@ 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, a class slot, and 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.
 
 * Checker
 
@@ -654,19 +680,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]
@@ -895,13 +922,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.
@@ -1019,6 +1045,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/docs/BUILT.md b/docs/BUILT.md
index fdd0dc3a..02803ee5 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 10140620..e5106991 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -1078,29 +1078,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) ->
@@ -1108,9 +1109,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
 
@@ -1594,6 +1594,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
@@ -1685,7 +1696,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)
             | _ -> ());
@@ -1978,6 +1991,31 @@ 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
    its machinery.
@@ -3488,12 +3526,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
@@ -3574,6 +3634,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
@@ -3769,6 +3837,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"
@@ -3919,7 +3993,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
@@ -5396,7 +5477,56 @@ 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_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
+            (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
@@ -6634,7 +6764,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:
@@ -6700,18 +6830,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) =
@@ -7130,8 +7260,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
@@ -7143,8 +7273,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 \
@@ -7158,15 +7286,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"
@@ -9114,7 +9233,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
@@ -10893,8 +11038,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 0af38526..9b3ba1c3 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/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 48129474..c380830b 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)
@@ -161,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 }
@@ -518,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
@@ -538,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 ...), \
@@ -603,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 }
       | _ ->
@@ -633,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 ...)"
@@ -784,7 +805,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"
@@ -879,7 +900,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. *)
@@ -946,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 \
@@ -1032,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 \
@@ -1219,7 +1242,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 ───────────────────────────
@@ -1290,17 +1313,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 +1366,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 +1460,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,11 +1486,11 @@ 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
-                   | 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 \
@@ -1493,7 +1516,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 +1562,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 +1589,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 +1636,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 +1650,18 @@ 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 ->
+         (* 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
            (m, next, false, loc) :: members (Int64.add next 1L) rest
          | bad :: _ ->
@@ -1690,11 +1725,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 +1768,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 +1799,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 +1879,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/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/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/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/programs/return-defer.flan b/test/programs/return-defer.flan
new file mode 100644
index 00000000..0b51f6ee
--- /dev/null
+++ b/test/programs/return-defer.flan
@@ -0,0 +1,47 @@
+;;;; 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 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 d89aed51..6ced8956 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -529,6 +529,35 @@ 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\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"
+      "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"
+      "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
@@ -5409,7 +5438,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;
diff --git a/test/test_flan.ml b/test/test_flan.ml
index d39a06df..d7857883 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";
@@ -6323,6 +6324,102 @@ 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))";
+  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)";
+  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";
+
+  (* ── 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));
+
+  (* ── 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))";
+
+  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. *)
+  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);
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</code></pre>
 
 <h2 id="defer">defer</h2>
 
-<p>A <code>defer</code> runs at function exit, innermost first. An explicit
-<code>return</code> runs the ones registered above it — a defer written below a return
-has not executed yet and must not fire.</p>
+<p>A <code>defer</code> runs at function exit, innermost first, after the value the
+function returns has been computed. An explicit <code>return</code> runs the ones
+registered above it — a defer written below a return has not executed yet and must
+not fire.</p>
 
 <pre><code>(defn work [n i32] i32
   (defer (println "second"))