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. *)