nil <-> None at (Option T) boundaries, and (Some nil) unconstructible — M2 queue item 4

Both directions of the boundary go through expect, the way every other
dyn crossing does. A dyn's tag decides which case an (Option T) becomes
on the way in; an Option's own tag decides nil or a boxed payload on the
way out. box_option/unbox_option build the same If-over-a-tag shape get
and map-remove already build for the same reason, reading an Option's
tag and payload with the raw Field access Render's structural printer
already uses — nothing new for either backend to lower. A literal
Some/None skips the runtime check entirely, since the checker already
knows which case it is.

A bare T has no None to become. The literal nil the checker can see is
refused right there, at compile time, in expect itself — the author's
decision to do both halves rather than settle for the runtime trap
alone. Everything one step removed from the syntax — a dyn that only
turns out to be nil once the program runs — reaches flan_dyn_need_i64's
existing DynType trap, unchanged; there is no dataflow in this checker
for it to be otherwise (see "Ownership tracking repealed").

(Some nil) is refused the same way: the literal at compile time, with a
message saying why nil and None would collide; a dyn that turns out to
be nil only at run time through the new flan_dyn_need_not_nil, which
traps by the same route flan_dyn_need_i64 does.

(Option (Option T)) does not cross either direction — boxing Some of an
inner None would box it as nil, indistinguishable from the outer None,
the same ambiguity (Some nil) is refused for. The type itself stays
legal on the typed side; only the crossing does not exist for it.

(Option dyn) needs no case of its own in the boundary code — the
payload is already dyn, so box_option/unbox_option treat it as the
identity — but it is not yet a value a program can hold anywhere. The
per-type-descriptor pass (M2 item 2) refuses it at every storage site
today, the same way it refuses (Vec dyn), because a struct's dyn fields
are marked by byte offsets and (Option dyn)'s payload has none. Item 4
does not lift that gate; it only makes the boundary already correct for
the day items 2/3 do.

expect grew a ctx parameter to build the fresh slot the two new
crossings need — every call site threaded through, one context
mismatch caught and fixed in check_fn's tail-expression case along the
way. var's None case grew a direct Dyn arm: None at a dyn want is nil
outright, with nothing to build.

nil-option.flan carries the crossings that succeed and ends on the
bare-T trap; some-nil.flan is (Some nil)'s run-time half, kept in its
own file the way dyn-boundary.flan is one trap per program. Both are
in no_fallback_slots and test_sanitize.ml: the new dyn temporary
unbox_option's tag test mints is rooted, and reads its Option's tag and
payload through ASan clean, --sanitize matching the unsanitized run
byte for byte.

lib/check.ml

@@ -1470,6 +1470,12 @@ let box loc (e : Tast.expr) : Tast.expr =
       ". The dyn container at this milestone is the runtime's own, from \
        (vec-new dyn); a typed container has a representation the dyn runtime \
        cannot walk"
+  (* [Option] is on this list in name only: [expect] intercepts it before
+     [box] ever sees one — [box_option] is the real answer, M2 item 4 — so
+     this arm only fires for a direct caller that hands [box] an Option
+     itself, and none does today. Left refused rather than removed, so a
+     caller that starts doing that gets a sentence instead of a silent
+     mis-lowering. *)
   | Types.Named _ | Types.Enum _ | Types.Option _ | Types.Ptr _
   | Types.Alloc | Types.Fn _ | Types.Var _ ->
     no_dyn_yet loc ~into:true e.Tast.ty ""
@@ -1500,7 +1506,95 @@ let unbox loc (want : Types.t) (e : Tast.expr) : Tast.expr =
           then "f64" else "i64"))
   | _ -> no_dyn_yet loc ~into:false want ""
 
-let expect loc ~want (got : Tast.expr) =
+(* nil is written [nil] and nothing else produces it, so this is the whole of
+   "the checker can see a nil reaching here" — a name, not a dataflow fact.
+   There is no propagation through a [let] or a call in this checker (see
+   "Ownership tracking repealed" — flow analysis was removed on purpose), so a
+   [nil] bound to a name and used later is exactly the case the runtime trap
+   below exists for. That is the intended split, not a gap: the syntax a
+   reader can see is refused where they are looking at it, and everything one
+   step removed from the syntax is caught when the program runs. *)
+let is_nil_lit (e : Tast.expr) =
+  match e.Tast.e with
+  | Tast.Prim (Tast.Rt "flan_dyn_nil", []) -> true
+  | _ -> false
+
+(* ── nil <-> None at (Option T) ────────────────────────────────────────────
+
+   The dyn absence and the typed one are the same absence at the one boundary
+   where both are meaningful, M2 item 4. Both directions build the same
+   [If]-over-a-tag shape [get] and [map-remove] already build (check.ml
+   4780-4900): the tag says which of [Some]/[None] it is, and the payload,
+   when there is one, crosses the scalar boundary [box]/[unbox] already own.
+
+   (Option (Option T)) does not cross either direction. Boxing [Some] of an
+   inner [None] would box that [None] as nil — the same nil an outer [None]
+   becomes — which is exactly the ambiguity [(Some nil)] is refused for one
+   level down; unboxing has the mirror problem, one dyn absence asked to tell
+   two levels of it apart. The type stays legal on the typed side (it is
+   already constructible: nothing here refuses it), only the crossing does
+   not exist for it.
+
+   (Option dyn) needs no case of its own. Its payload is already dyn, so
+   boxing it is the identity and unboxing it is the identity; the only thing
+   that has to hold is that the payload is never nil, which is [(Some nil)]'s
+   refusal below, not this boundary's. *)
+let box_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr =
+  match t with
+  | Types.Option inner ->
+    Loc.failk "check/option-nested-dyn" loc
+      "(Option (Option %s)) does not cross into dyn — boxing Some of an \
+       inner None would box it as nil, the same nil an outer None becomes, \
+       which is the ambiguity (Some nil) is refused for"
+      (Types.to_string inner)
+  | _ ->
+    (* A literal [Some]/[None] built right here skips the runtime check: the
+       checker already knows which case it is, so there is nothing to test at
+       run time and the conversion is free on both backends. *)
+    match got.Tast.e with
+    | Tast.None_ -> rt loc Types.Dyn "flan_dyn_nil" []
+    | Tast.Some_ x -> if Types.equal t Types.Dyn then x else box loc x
+    | _ ->
+      let s = fresh_slot ctx (Types.Option t) in
+      let sv = mk loc (Types.Option t) (Tast.Local s) in
+      let tag = mk loc (Types.Int Types.I8) (Tast.Field (sv, 0)) in
+      let is_some =
+        mk loc Types.Bool
+          (Tast.Prim (Tast.Ne,
+                      [ tag; mk loc (Types.Int Types.I8) (Tast.Int (0L, Types.I8)) ]))
+      in
+      let payload = mk loc t (Tast.Field (sv, 1)) in
+      let some_dyn = if Types.equal t Types.Dyn then payload else box loc payload in
+      let none_dyn = rt loc Types.Dyn "flan_dyn_nil" [] in
+      mk loc Types.Dyn
+        (Tast.Let ([ (s, got) ],
+                   [ mk loc Types.Dyn (Tast.If (is_some, some_dyn, none_dyn)) ]))
+
+let unbox_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr =
+  let oty = Types.Option t in
+  match t with
+  | Types.Option inner ->
+    Loc.failk "check/option-nested-dyn" loc
+      "(Option (Option %s)) does not cross from dyn — a dyn value is nil or \
+       it is not, one absence, and that cannot tell None from Some None apart"
+      (Types.to_string inner)
+  | _ when is_nil_lit got -> mk loc oty Tast.None_
+  | _ ->
+    let s = fresh_slot ctx Types.Dyn in
+    let sv = mk loc Types.Dyn (Tast.Local s) in
+    let not_nil =
+      mk loc Types.Bool
+        (Tast.Prim (Tast.Eq,
+                    [ rt loc (Types.Int Types.I32) "flan_dyn_is_nil" [ sv ];
+                      mk loc (Types.Int Types.I32) (Tast.Int (0L, Types.I32)) ]))
+    in
+    let none = mk loc oty Tast.None_ in
+    let payload = if Types.equal t Types.Dyn then sv else unbox loc t sv in
+    let some = mk loc oty (Tast.Some_ payload) in
+    mk loc oty
+      (Tast.Let ([ (s, got) ], [ mk loc oty (Tast.If (not_nil, some, none)) ]))
+
+let expect ctx loc ~want (got : Tast.expr) =
   match want with
   | None -> got
   | Some w ->
@@ -1511,7 +1605,18 @@ let expect loc ~want (got : Tast.expr) =
     let got =
       match w, got.Tast.ty with
       | Types.Dyn, Types.Dyn -> got
+      | Types.Dyn, Types.Option t -> box_option ctx loc t got
       | Types.Dyn, _ -> box loc got
+      | Types.Option t, Types.Dyn -> unbox_option ctx loc t got
+      (* A bare T has no None to become, and this nil is one the checker can
+         actually see — the literal, written right where the mismatch is.
+         Refused here, at the offending line, instead of waiting for the
+         runtime trap [unbox] would otherwise reach for two arms down. *)
+      | w, Types.Dyn when is_nil_lit got ->
+        fail loc
+          "nil has no None to become at %s — nil only converts to (Option T) \
+           or to dyn itself; wrap the type in Option, or keep the value dyn"
+          (Types.to_string w)
       | _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got
       | _, Types.Dyn -> unbox loc w got
       | _ -> got
@@ -1862,7 +1967,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
       | _ -> Types.F64
     in
     mk loc (Types.Float k) (Tast.Float (x, k))
-  | Ast.Str s -> expect loc ~want (mk loc Types.String (Tast.Str s))
+  | Ast.Str s -> expect ctx loc ~want (mk loc Types.String (Tast.Str s))
   | Ast.Kw k ->
     (* Two keywords in one spelling, told apart by the expectation. Where an
        enum type is expected, :space resolves at compile time against its
@@ -1883,7 +1988,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
             (String.concat " "
                (List.map (fun (m, _) -> ":" ^ m) members)))
      | Some Types.Dyn | None ->
-       expect loc ~want
+       expect ctx loc ~want
          (rt loc Types.Dyn "flan_dyn_kw" [ mk loc Types.String (Tast.Str k) ])
      | Some other ->
        fail loc
@@ -1907,7 +2012,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
                check ctx ~want:Types.Dyn v ])
         kvs
     in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Dyn
          (Tast.Let ([ (m, rt loc Types.Dyn "flan_dyn_map_new" []) ],
                     sets @ [ mval ])))
@@ -1933,7 +2038,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
     in
     (* No latch: a [while] has nothing to run between the body and the test, so
        a [continue] can branch straight at the condition. *)
-    expect loc ~want (mk loc Types.Unit (Tast.While (c, body, [])))
+    expect ctx loc ~want (mk loc Types.Unit (Tast.While (c, body, [])))
   (* [Never], as [exit] and [return] are: nothing after one of these runs, and
      an [if] arm that ends in a break does not have to agree with the other. *)
   (* (loop [x 0 acc 1] body ...) — a loop that answers with the value of its
@@ -1976,7 +2081,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
   | Ast.Set (p, v) ->
     let p, pty = check_place ctx loc p in
     let v = check ctx ~want:pty v in
-    expect loc ~want (mk loc Types.Unit (Tast.Set (p, v)))
+    expect ctx loc ~want (mk loc Types.Unit (Tast.Set (p, v)))
   | Ast.Field (target, name) ->
     let target, sname = struct_target ctx target in
     let s = Option.get (fields_named ctx.env sname) in
@@ -1986,7 +2091,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
          "%s has no field %s" sname name
      | Some i ->
        let fty = (List.nth s.Tast.fields i).Tast.fty in
-       expect loc ~want (mk loc fty (Tast.Field (target, i))))
+       expect ctx loc ~want (mk loc fty (Tast.Field (target, i))))
   | Ast.Struct (name, kvs) -> check_struct ctx ~want loc name kvs
   (* A bracket literal where a dyn is wanted is the runtime's own vec, built
      where it stands — the same lowering the map literal gets, and what makes
@@ -2011,7 +2116,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
      value, which is what a declared array with no initialiser gets. *)
   | Ast.ArrayOf t ->
     let ty = resolve ctx.env t in
-    expect loc ~want (mk loc ty (Tast.Zero ty))
+    expect ctx loc ~want (mk loc ty (Tast.Zero ty))
   | Ast.Match (scrutinee, arms) -> check_match ctx ~tail ?want loc scrutinee arms
   | Ast.Call (head, args) -> check_call ctx ~want loc head args
   | Ast.Unwrap (Ast.Usome, v) ->
@@ -2022,7 +2127,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
        let v = check ctx v in
        (match v.Tast.ty with
         | Types.Option t ->
-          expect loc ~want (mk loc t (Tast.UnwrapSome v))
+          expect ctx loc ~want (mk loc t (Tast.UnwrapSome v))
         | other ->
           fail loc "some takes an (Option T), found %s" (Types.to_string other))
      | other ->
@@ -2075,7 +2180,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
       | Ast.Ssignal -> (Types.Unit, Tast.Ssignal)
       | Ast.Serror -> (Types.Never, Tast.Serror)
     in
-    expect loc ~want (mk loc ty (Tast.Signal (kind, type_id name, c)))
+    expect ctx loc ~want (mk loc ty (Tast.Signal (kind, type_id name, c)))
 
   | Ast.HandlerBind (clauses, body) -> check_handler_bind ctx ?want loc clauses body
   | Ast.HandlerCase (body, clauses) -> check_handler_case ctx ?want loc body clauses
@@ -2123,7 +2228,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
       mk loc Types.Never
         (Tast.InvokeRestart (type_id name, name, locals, sg, type_id sg, loc))
     in
-    expect loc ~want
+    expect ctx loc ~want
       (if binds = [] then invoke
        else mk loc Types.Never (Tast.Let (binds, [ invoke ])))
 
@@ -2198,17 +2303,22 @@ and in_range loc k n =
 and var ctx loc ~want name =
   match name with
   | "true" | "false" ->
-    expect loc ~want (mk loc Types.Bool (Tast.Bool (name = "true")))
+    expect ctx loc ~want (mk loc Types.Bool (Tast.Bool (name = "true")))
   (* The dyn absence value, written down. It arrived with maps — (get m k) on
      a key the map does not hold answers it — and this is its producer, so a
      program can store one, compare against one, and put one in a map. It is
-     always dyn: at a typed want it refuses through [expect], and what a nil
+     always dyn here: whatever it becomes at a typed want — None at an
-     does at an (Option T) boundary is the queue's own later item. *)
+     (Option T), a refusal at a bare T — is [expect]'s boundary logic, M2
+     item 4. *)
   | "nil" ->
-    expect loc ~want (rt loc Types.Dyn "flan_dyn_nil" [])
+    expect ctx loc ~want (rt loc Types.Dyn "flan_dyn_nil" [])
   | "None" ->
     (match want with
      | Some (Types.Option t) -> mk loc (Types.Option t) Tast.None_
+     (* The mirror of [nil] becoming [None]: at a dyn want, None *is* nil,
+        with nothing to build and nothing to check — there is only one dyn
+        absence and this is it, not an (Option T) that then gets boxed. *)
+     | Some Types.Dyn -> rt loc Types.Dyn "flan_dyn_nil" []
      | Some other when other <> Types.Never ->
        fail loc "expected %s, found None" (Types.to_string other)
      | _ ->
@@ -2221,19 +2331,19 @@ and var ctx loc ~want name =
      variables at run time rather than extra parameters — see docs/BUILT.md for why
      the literal reading of "calling convention" is deferred. *)
   | "context/allocator" ->
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Alloc (Tast.Prim (Tast.Rt "flan_context_allocator", [])))
   | "context/temp" ->
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Alloc (Tast.Prim (Tast.Rt "flan_context_temp", [])))
   | _ ->
     match lookup ctx name with
     | Some b ->
-      expect loc ~want (mk loc b.bty (Tast.Local b.slot))
+      expect ctx loc ~want (mk loc b.bty (Tast.Local b.slot))
     | None ->
       match Hashtbl.find_opt ctx.env.globals name with
       | Some (ty, _) ->
-        expect loc ~want (mk loc ty (Tast.Global name))
+        expect ctx loc ~want (mk loc ty (Tast.Global name))
       | None ->
         match Hashtbl.find_opt ctx.env.cases name with
         (* A case with no fields is a whole value on its own, so it is written
@@ -2247,7 +2357,7 @@ and var ctx loc ~want name =
               "%s has fields, so it needs them — write (%s {.%s ...})"
               name name
               (List.hd c.Tast.vfields).Tast.fname;
-          expect loc ~want
+          expect ctx loc ~want
             (mk loc (Types.Named dname)
                (Tast.MakeCase (dname, c.Tast.vname, [])))
         | Some (dname, c) ->
@@ -2273,7 +2383,7 @@ and var ctx loc ~want name =
                   function value: a Flan function's signature ends with the \
                   transfer channel and a C one does not. Wrap it in a defn \
                   and pass that" name;
-             expect loc ~want
+             expect ctx loc ~want
                (mk loc (Types.Fn (params, ret)) (Tast.FnAddr (Tast.Fnval name)))
            | None -> captured ctx loc name;
          Loc.failk "check/unknown-name" loc "unknown name %s" name)
@@ -2298,7 +2408,7 @@ and block ctx ?want ?(defer_ok = false) loc body =
   match body with
   (* Withdrawn here too. An empty body has no last form to be the tail, so
      leaving the permission set would hand it to whatever is checked next. *)
-  | [] -> ctx.tail <- false; expect loc ~want (unit_at loc)
+  | [] -> ctx.tail <- false; expect ctx loc ~want (unit_at loc)
   | _ ->
     (* A block's tail is its last form and nothing else. Callers that must not
        pass one on need do nothing: [check] withdrew it before they were
@@ -2378,7 +2488,7 @@ and check_fn ctx ~want loc (params : string list) body =
     match List.rev fbody with
     | [] -> fbody
     | last :: rest ->
-      List.rev (expect last.Tast.loc ~want:(Some ret) last :: rest)
+      List.rev (expect fctx last.Tast.loc ~want:(Some ret) last :: rest)
   in
   (* Named after the function it was written in and numbered within it, which
      is the handler clause's rule and is stable for the same reason: a
@@ -2408,7 +2518,7 @@ and check_fn ctx ~want loc (params : string list) body =
       ret; body = fbody; fdefers = [];
       fparent = Some ctx.owner; floc = loc }
     :: ctx.env.lifted;
-  expect loc ~want
+  expect ctx loc ~want
     (mk loc (Types.Fn (pts, ret)) (Tast.FnAddr (Tast.Fnval fname)))
 
 (* A handler runs where the *signal* was, not where it was established, so it
@@ -2531,7 +2641,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
       go body)
   in
   ctx.in_frames <- saved;
-  expect loc ~want (mk loc ty (Tast.Handled (frames, body)))
+  expect ctx loc ~want (mk loc ty (Tast.Handled (frames, body)))
 
 (* (restart-case BODY (name [] BODY-1) ...) — spec-conditions.md §3 and §6.
 
@@ -2926,7 +3036,7 @@ and check_dotimes ctx ~want loc label name count body =
        rest of the body — so [i] would never advance and the loop would hang.
        That is the whole reason [Tast.While] carries a third list. *)
     let loop = mk loc Types.Unit (Tast.While (cond, body, [ step ])) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Unit (Tast.Let ([ (i, zero); (limit, count) ], [ loop ]))))
 
 (* ── (loop [...] ...) and (recur ...) ───────────────────────────────────
@@ -3001,9 +3111,9 @@ and check_loop ctx ?want loc bs body =
     in
     let loop = mk loc Types.Unit (Tast.While (yes, inner, [])) in
     match result with
-    | None -> expect loc ~want (mk loc ty (Tast.Let (binds, [ loop ])))
+    | None -> expect ctx loc ~want (mk loc ty (Tast.Let (binds, [ loop ])))
     | Some r ->
-      expect loc ~want
+      expect ctx loc ~want
         (mk loc ty
            (Tast.Let (binds @ [ (r, mk loc ty (Tast.Zero ty)) ],
                       [ loop; mk loc ty (Tast.Local r) ]))))
@@ -3075,7 +3185,7 @@ and check_if ctx ?(tail = false) ?want loc c t e =
     (* A one-armed if produces Unit whatever the branch evaluates to: there is
        no value on the missing side. `when` desugars to this. *)
     let t = branch ctx (fun () -> in_tail (fun () -> check ctx t)) in
-    expect loc ~want (mk loc Types.Unit (Tast.If (c, t, unit_at loc)))
+    expect ctx loc ~want (mk loc Types.Unit (Tast.If (c, t, unit_at loc)))
   | Some e ->
     let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in
     (* With no expectation the then-branch supplies one for the else-branch,
@@ -3187,7 +3297,7 @@ and check_struct ctx ~want loc name kvs =
            | None -> mk loc f.Tast.fty (Tast.Zero f.Tast.fty))
         s.Tast.fields
     in
-    expect loc ~want (mk loc (Types.Named name) (Tast.Make (name, fields)))
+    expect ctx loc ~want (mk loc (Types.Named name) (Tast.Make (name, fields)))
 
 (* [(U {.member v})] — an untagged union value.
 
@@ -3239,14 +3349,14 @@ and check_union ctx ~want loc name kvs =
   match kvs with
   (* The two-member case left above, so this sees one or none. *)
   | _ :: _ :: _ -> assert false
-  | [] -> expect loc ~want (mk loc (Types.Named name) (Tast.Zero (Types.Named name)))
+  | [] -> expect ctx loc ~want (mk loc (Types.Named name) (Tast.Zero (Types.Named name)))
   | [ (k, v) ] ->
     let i = Option.get (Tast.field_index u k) in
     let fty = (List.nth u.Tast.fields i).Tast.fty in
     let v = check ctx ~want:fty v in
     let slot = fresh_slot ctx (Types.Named name) in
     let here = mk loc (Types.Named name) (Tast.Local slot) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc (Types.Named name)
          (Tast.Let
             ([ (slot, mk loc (Types.Named name) (Tast.Zero (Types.Named name))) ],
@@ -3294,7 +3404,7 @@ and check_case ctx ~want loc dname (c : Tast.variant) kvs =
          | None -> mk loc f.Tast.fty (Tast.Zero f.Tast.fty))
       c.Tast.vfields
   in
-  expect loc ~want
+  expect ctx loc ~want
     (mk loc (Types.Named dname) (Tast.MakeCase (dname, c.Tast.vname, fields)))
 
 and check_arr ctx ~want loc items =
@@ -3325,7 +3435,7 @@ and check_arr ctx ~want loc items =
    | _ -> ());
   (* [n T] and [T] are distinct in type and in ownership (spec-memory.md), so
      an array literal does not satisfy a slice expectation. *)
-  expect loc ~want (mk loc (Types.Array (n, elem)) (Tast.Arr items))
+  expect ctx loc ~want (mk loc (Types.Array (n, elem)) (Tast.Arr items))
 
 and check_match ctx ?(tail = false) ?want loc scrutinee arms =
   let s = check ctx scrutinee in
@@ -3645,7 +3755,7 @@ and call_value ctx ~want loc (callee : Tast.expr) args =
         (if List.length params = 1 then "" else "s")
         (List.length args);
     let args = map2_lr (fun p a -> check ctx ~want:p a) params args in
-    expect loc ~want (mk loc ret (Tast.CallPtr (callee, args)))
+    expect ctx loc ~want (mk loc ret (Tast.CallPtr (callee, args)))
   | other ->
     fail loc "this is a %s and not a function, so it cannot be called"
       (Types.to_string other)
@@ -3711,7 +3821,7 @@ and fold_left_prim ctx ~want loc name p ok what args =
       (mk loc ty (Tast.Prim (p, [ a; b ])))
       rest
   in
-  expect loc ~want acc
+  expect ctx loc ~want acc
   end
 
 (* The dyn lowering of a fold: one call per operator application, left to
@@ -3742,7 +3852,7 @@ and dyn_fold ctx ~want loc name first rest =
     List.fold_left (fun acc arg -> apply acc (check ctx ~want:Types.Dyn arg))
       acc rest
   in
-  expect loc ~want acc
+  expect ctx loc ~want acc
 
 (* ── Allocation failure, spec-memory.md ────────────────────────────────
    No allocating operation returns an error and none can fail silently. When
@@ -4012,7 +4122,7 @@ and vec_at ctx loc (target : Tast.expr) (idx : Ast.expr list) =
    wrote down, so each one needs a line in [builtins] further down this file.
    A new arm without an entry fails the build — test_flan reads both. *)
 and named_call ctx ~want loc name args =
-  let prim p ty args = expect loc ~want (mk loc ty (Tast.Prim (p, args))) in
+  let prim p ty args = expect ctx loc ~want (mk loc ty (Tast.Prim (p, args))) in
   match name with
   (* ── arithmetic and comparison ─────────────────────────────────── *)
   | "+" | "-" | "*" | "/" ->
@@ -4069,7 +4179,7 @@ and named_call ctx ~want loc name args =
         if String.equal name "!=" then mk loc Types.Bool (Tast.Prim (Tast.Not, [ cmp ]))
         else cmp
       in
-      expect loc ~want r
+      expect ctx loc ~want r
     end else begin
     (* [=] and [!=] admit types [<] does not. A handle is one: a pair of
        numbers in one word and where being the same entity is the question the
@@ -4168,7 +4278,7 @@ and named_call ctx ~want loc name args =
       mk loc ty (Tast.Let ([ (sa, a); (sb, b) ],
                            [ mk loc ty (Tast.If (test, la, lb)) ]))
     in
-    expect loc ~want
+    expect ctx loc ~want
       (List.fold_left (fun acc arg -> pick acc (check ctx ~want:ty arg))
          (pick a b) rest)
   (* (zeroed) is the all-bytes-zero value of whatever it is being stored into,
@@ -4263,7 +4373,7 @@ and named_call ctx ~want loc name args =
        allocator that does exist"
   | "heap-allocator" ->
     arity loc name 0 args;
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Alloc (Tast.Prim (Tast.Rt "flan_heap_allocator", [])))
   (* The capacity is explicit and there is no growing backing store: an arena
      whose size is decided by the program is one a program can reason about,
@@ -4272,14 +4382,14 @@ and named_call ctx ~want loc name args =
   | "arena-new" ->
     arity loc name 1 args;
     let cap = check ctx ~want:(Types.Int Types.I64) (List.hd args) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Alloc (Tast.Prim (Tast.Rt "flan_arena_new", [ cap ])))
   (* Hands the pages back, which [free-all] deliberately does not — see
      docs/BUILT.md, "free-all is retain-capacity". *)
   | "arena-destroy" ->
     arity loc name 1 args;
     let a = check ctx ~want:Types.Alloc (List.hd args) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Unit (Tast.Prim (Tast.Rt "flan_arena_destroy", [ a ])))
   (* One of spec-memory.md's two release points. It takes the source location
      as a string so that an allocator with no region to release names the site
@@ -4287,7 +4397,7 @@ and named_call ctx ~want loc name args =
   | "free-all" ->
     arity loc name 1 args;
     let a = check ctx ~want:Types.Alloc (List.hd args) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Unit
          (Tast.Prim (Tast.Rt "flan_alloc_free_all", [ a; here loc ])))
   (* The capability set, read off the allocator value. Odin asks its procedure
@@ -4296,7 +4406,7 @@ and named_call ctx ~want loc name args =
   | "can-free?" ->
     arity loc name 1 args;
     let a = check ctx ~want:Types.Alloc (List.hd args) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Bool
          (Tast.Prim (Tast.Ne,
                      [ mk loc (Types.Int Types.I8)
@@ -4305,7 +4415,7 @@ and named_call ctx ~want loc name args =
   | "can-free-all?" ->
     arity loc name 1 args;
     let a = check ctx ~want:Types.Alloc (List.hd args) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Bool
          (Tast.Prim (Tast.Ne,
                      [ mk loc (Types.Int Types.I8)
@@ -4317,7 +4427,7 @@ and named_call ctx ~want loc name args =
   | "alloc-epoch" ->
     arity loc name 1 args;
     let a = check ctx ~want:Types.Alloc (List.hd args) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc (Types.Int Types.I64)
          (Tast.Prim (Tast.Rt "flan_alloc_epoch", [ a ])))
   (* The allocator's identity — its address — which is what the condition's
@@ -4326,7 +4436,7 @@ and named_call ctx ~want loc name args =
   | "alloc-id" ->
     arity loc name 1 args;
     let a = check ctx ~want:Types.Alloc (List.hd args) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Rt "flan_alloc_id", [ a ])))
   (* A ceiling on live bytes, 0 for none. spec-memory.md's retry restart is
      answerable only by a handler that can make the *same* request succeed, and
@@ -4338,7 +4448,7 @@ and named_call ctx ~want loc name args =
   | "alloc-budget" ->
     arity loc name 1 args;
     let a = check ctx ~want:Types.Alloc (List.hd args) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc (Types.Int Types.I64)
          (Tast.Prim (Tast.Rt "flan_alloc_budget", [ a ])))
   | "set-alloc-budget" ->
@@ -4347,7 +4457,7 @@ and named_call ctx ~want loc name args =
      | [ a; n ] ->
        let a = check ctx ~want:Types.Alloc a in
        let n = check ctx ~want:(Types.Int Types.I64) n in
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc Types.Unit (Tast.Prim (Tast.Rt "flan_alloc_set_budget", [ a; n ])))
      | _ -> assert false)
   (* "Did you forget to free" is an allocator-tier question and this is the
@@ -4355,7 +4465,7 @@ and named_call ctx ~want loc name args =
   | "alloc-live-blocks" ->
     arity loc name 1 args;
     let a = check ctx ~want:Types.Alloc (List.hd args) in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc (Types.Int Types.I64)
          (Tast.Prim (Tast.Rt "flan_alloc_live_blocks", [ a ])))
   (* (with-allocator A BODY...). It rebinds and releases nothing: not at the
@@ -4382,7 +4492,7 @@ and named_call ctx ~want loc name args =
              in
              go body)
        in
-       expect loc ~want (mk loc ty (Tast.WithAlloc (a, body))))
+       expect ctx loc ~want (mk loc ty (Tast.WithAlloc (a, body))))
 
   (* ── (Vec T), spec-memory.md ───────────────────────────────────── *)
   (* Every one of these is a named call over a type-erased runtime, with
@@ -4416,7 +4526,7 @@ and named_call ctx ~want loc name args =
           "(vec-new dyn) takes no allocator — the dyn container's storage is \
            the dyn runtime's, which is what lets the collector find the values \
            inside it";
-      expect loc ~want (rt loc Types.Dyn "flan_dyn_vec_new" [])
+      expect ctx loc ~want (rt loc Types.Dyn "flan_dyn_vec_new" [])
     end else begin
     let a = allocator_arg ctx loc args in
     let v = fresh_slot ctx (Types.Vec elem) in
@@ -4425,7 +4535,7 @@ and named_call ctx ~want loc name args =
         [ mk loc (Types.Vec elem) (Tast.Local v); a; i64_at loc 0L;
           size_of loc elem; align_of loc elem; here loc ]
     in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc (Types.Vec elem)
          (Tast.Let ([ (v, mk loc (Types.Vec elem) (Tast.Zero (Types.Vec elem))) ],
                     [ with_note loc (alloc_guard ctx loc attempt)
@@ -4448,7 +4558,7 @@ and named_call ctx ~want loc name args =
           retry restart exist for an allocator the *program* named, and here
           there is none to name. *)
        if target.Tast.ty = Types.Dyn then
-         expect loc ~want
+         expect ctx loc ~want
            (rt loc Types.Unit "flan_dyn_push"
               [ target; check ctx ~want:Types.Dyn x ])
        else begin
@@ -4467,7 +4577,7 @@ and named_call ctx ~want loc name args =
           an unmoved block costs a probe and an overwrite with the same
           numbers. This is the insert per allocation NEXT.md settles on, and
           the settled answer to what it costs is "measure a real program". *)
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc Types.Unit
             (Tast.Let ([ (e, x) ],
                        [ region_check ctx.env loc target
@@ -4490,7 +4600,7 @@ and named_call ctx ~want loc name args =
        if (match target.Tast.ty with
            | Types.Map (k, _) -> deferred_key ctx.env loc "reserve" k
            | _ -> false) then
-         expect loc ~want (mk loc Types.Unit Tast.Unit)
+         expect ctx loc ~want (mk loc Types.Unit Tast.Unit)
        else
        let attempt, note =
          match target.Tast.ty with
@@ -4511,7 +4621,7 @@ and named_call ctx ~want loc name args =
            reg_note loc "flan_dev_reg_note_vec" target
              [ size_of loc elem ] elem
        in
-       expect loc ~want
+       expect ctx loc ~want
          (region_check ctx.env loc target
             (with_note loc (alloc_guard ctx loc attempt) note))
      | _ -> assert false)
@@ -4540,7 +4650,7 @@ and named_call ctx ~want loc name args =
            [ target; addr_of loc (mk loc (Types.Slice elem) (Tast.Local out));
              lo; hi; size_of loc elem; here loc ]
        in
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc (Types.Slice elem)
             (Tast.Let ([ (out, mk loc (Types.Slice elem)
                                  (Tast.Zero (Types.Slice elem))) ],
@@ -4590,11 +4700,11 @@ and named_call ctx ~want loc name args =
           elements own, in one operation and with no per-element teardown"
          (Types.to_string target.Tast.ty)
      | Types.Vec elem ->
-       expect loc ~want
+       expect ctx loc ~want
          (rt loc Types.Unit "flan_vec_free"
             [ target; size_of loc elem; align_of loc elem; here loc ])
      | Types.Map (k, v) ->
-       expect loc ~want
+       expect ctx loc ~want
          (rt loc Types.Unit "flan_map_free"
             [ target; size_of loc k; size_of loc v; here loc ])
      | other ->
@@ -4655,7 +4765,7 @@ and named_call ctx ~want loc name args =
              the value a (map-new) starts from, so everything written around
              the clone still checks against the type it will have. *)
           let mty = Types.Map (k, v) in
-          expect loc ~want (mk loc mty (Tast.Zero mty))
+          expect ctx loc ~want (mk loc mty (Tast.Zero mty))
         | Types.Map (k, v) ->
           let mty = Types.Map (k, v) in
           let hash, _ = key_fns ctx.env loc k in
@@ -4665,7 +4775,7 @@ and named_call ctx ~want loc name args =
               [ mk loc mty (Tast.Local d); target; a;
                 size_of loc k; size_of loc v; hash; here loc ]
           in
-          expect loc ~want
+          expect ctx loc ~want
             (mk loc mty
                (Tast.Let ([ (d, mk loc mty (Tast.Zero mty)) ],
                           [ with_note loc (alloc_guard ctx loc attempt)
@@ -4681,7 +4791,7 @@ and named_call ctx ~want loc name args =
               [ mk loc (Types.Vec elem) (Tast.Local d); target; a;
                 size_of loc elem; align_of loc elem; here loc ]
           in
-          expect loc ~want
+          expect ctx loc ~want
             (mk loc (Types.Vec elem)
                (Tast.Let ([ (d, mk loc (Types.Vec elem)
                                   (Tast.Zero (Types.Vec elem))) ],
@@ -4714,7 +4824,7 @@ and named_call ctx ~want loc name args =
         [ mk loc mty (Tast.Local m); a; size_of loc k; size_of loc v;
           here loc ]
     in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc mty
          (Tast.Let ([ (m, mk loc mty (Tast.Zero mty)) ],
                     [ with_note loc (alloc_guard ctx loc attempt)
@@ -4736,7 +4846,7 @@ and named_call ctx ~want loc name args =
           a dyn vec is: the runtime owns the storage, so there is no guard, no
           restart and no region check. An equal key's value is replaced. *)
        if target.Tast.ty = Types.Dyn then
-         expect loc ~want
+         expect ctx loc ~want
            (rt loc Types.Unit "flan_dyn_map_set"
               [ target; check ctx ~want:Types.Dyn k;
                 check ctx ~want:Types.Dyn v ])
@@ -4748,7 +4858,7 @@ and named_call ctx ~want loc name args =
           and a borrow still a borrow — and the node itself is a unit no-op,
           thrown away with the rest of the abstract pass. *)
        if deferred_key ctx.env loc "put" kt then
-         expect loc ~want (mk loc Types.Unit Tast.Unit)
+         expect ctx loc ~want (mk loc Types.Unit Tast.Unit)
        else
        (* Both are bound before the loop, so that a [retry] re-attempts the
           allocation and not the expressions that produced the key and the
@@ -4761,7 +4871,7 @@ and named_call ctx ~want loc name args =
              addr_of loc (mk loc vt (Tast.Local vs));
              size_of loc kt; size_of loc vt; hash; eq; here loc ]
        in
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc Types.Unit
             (Tast.Let ([ (ks, k); (vs, v) ],
                        [ region_check ctx.env loc target
@@ -4788,7 +4898,7 @@ and named_call ctx ~want loc name args =
           and (contains? m k) is the question to ask when nil might also be
           stored under the key. *)
        if target.Tast.ty = Types.Dyn then
-         expect loc ~want
+         expect ctx loc ~want
            (rt loc Types.Dyn "flan_dyn_map_get"
               [ target; check ctx ~want:Types.Dyn k ])
        else begin
@@ -4798,7 +4908,7 @@ and named_call ctx ~want loc name args =
           form answers an (Option V), and the abstract pass still has to
           type-check whatever the body does with the answer. *)
        if deferred_key ctx.env loc "get" kt then
-         expect loc ~want (mk loc (Types.Option vt) Tast.None_)
+         expect ctx loc ~want (mk loc (Types.Option vt) Tast.None_)
        else
        let hash, eq = key_fns ctx.env loc kt in
        let ks = fresh_slot ctx kt in
@@ -4822,7 +4932,7 @@ and named_call ctx ~want loc name args =
                        [ found;
                          mk loc (Types.Int Types.I8) (Tast.Int (0L, Types.I8)) ]))
        in
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc oty
             (Tast.Let ([ (ks, k);
                          (out, mk loc vt (Tast.Zero vt)) ],
@@ -4840,7 +4950,7 @@ and named_call ctx ~want loc name args =
        let s = check ctx s in
        (match s.Tast.ty with
         | Types.String | Types.Slice (Types.Int Types.U8) ->
-          expect loc ~want (rt loc Types.Dyn "flan_dyn_kw" [ s ])
+          expect ctx loc ~want (rt loc Types.Dyn "flan_dyn_kw" [ s ])
         | other ->
           fail loc "keyword takes a string or a [u8], found %s"
             (Types.to_string other))
@@ -4870,7 +4980,7 @@ and named_call ctx ~want loc name args =
           the abstract pass still has to check whatever the body does with the
           answer. *)
        if deferred_key ctx.env loc "map-remove" kt then
-         expect loc ~want (mk loc (Types.Option vt) Tast.None_)
+         expect ctx loc ~want (mk loc (Types.Option vt) Tast.None_)
        else
        let hash, eq = key_fns ctx.env loc kt in
        let ks = fresh_slot ctx kt in
@@ -4892,7 +5002,7 @@ and named_call ctx ~want loc name args =
                        [ found;
                          mk loc (Types.Int Types.I8) (Tast.Int (0L, Types.I8)) ]))
        in
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc oty
             (Tast.Let ([ (ks, k);
                          (out, mk loc vt (Tast.Zero vt)) ],
@@ -4933,7 +5043,7 @@ and named_call ctx ~want loc name args =
          rt loc (Types.Int Types.I8) "flan_map_next"
            [ target; cur; k; v; size_of loc kt; size_of loc vt; here loc ]
        in
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc Types.Bool
             (Tast.Prim
                (Tast.Ne,
@@ -4956,7 +5066,7 @@ and named_call ctx ~want loc name args =
           comparison does, because a presence test is overwhelmingly an if's
           condition. *)
        if target.Tast.ty = Types.Dyn then
-         expect loc ~want
+         expect ctx loc ~want
            (unbox loc Types.Bool
               (rt loc Types.Dyn "flan_dyn_map_contains"
                  [ target; check ctx ~want:Types.Dyn k ]))
@@ -4966,7 +5076,7 @@ and named_call ctx ~want loc name args =
        (* Deferred, and the placeholder is a [bool] — the form a condition
           wants, so the condition around it still has to check. *)
        if deferred_key ctx.env loc "has-key?" kt then
-         expect loc ~want (mk loc Types.Bool (Tast.Bool false))
+         expect ctx loc ~want (mk loc Types.Bool (Tast.Bool false))
        else
        let hash, eq = key_fns ctx.env loc kt in
        let ks = fresh_slot ctx kt in
@@ -4975,7 +5085,7 @@ and named_call ctx ~want loc name args =
            [ target; addr_of loc (mk loc kt (Tast.Local ks));
              size_of loc kt; size_of loc vt; hash; eq; here loc ]
        in
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc Types.Bool
             (Tast.Let ([ (ks, k) ],
                        [ mk loc Types.Bool
@@ -5044,11 +5154,11 @@ and named_call ctx ~want loc name args =
           a wart. [want] is a fallback only, and nothing depends on it. *)
        (match args with
         | [ _; { Ast.e = Ast.Var "string"; _ } ] ->
-          expect loc ~want (as_string ())
+          expect ctx loc ~want (as_string ())
         | _ ->
           (match want with
            | Some Types.String -> as_string ()
-           | _ -> expect loc ~want (as_bytes ())))
+           | _ -> expect ctx loc ~want (as_bytes ())))
      | _ ->
        fail loc
          "embed is (embed \"path\") for a [u8], or (embed \"path\" string)")
@@ -5106,7 +5216,7 @@ and named_call ctx ~want loc name args =
                    mk loc (Types.Slice (Types.Int Types.U8)) (Tast.Str data) ])))
         entries
     in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc (Types.Array (Int64.of_int (List.length entries), ety))
          (Tast.Arr elems))
 
@@ -5159,7 +5269,7 @@ and named_call ctx ~want loc name args =
            try_ (rt loc (Types.Int Types.I8) "flan_slurp_into"
                    [ vv (); psv (); size_of loc u8; here loc ]) ]
        in
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc vt
             (Tast.Let
                ([ (ps, path);
@@ -5192,7 +5302,7 @@ and named_call ctx ~want loc name args =
        (* Both operands are bound before the loop so that a retry re-attempts
           the write and not the expressions that produced it — the same rule
           alloc_guard states for push. *)
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc Types.Unit
             (Tast.Let ([ (ps, path); (ds, data) ],
                        [ file_guard ctx loc ~path_slot:ps ~op:1 steps ])))
@@ -5229,7 +5339,7 @@ and named_call ctx ~want loc name args =
       [ try_ (rt loc (Types.Int Types.I8) sym
                 [ mk loc Types.String (Tast.Local ps) ]) ]
     in
-    expect loc ~want
+    expect ctx loc ~want
       (mk loc Types.Unit
          (Tast.Let ([ (ps, path) ],
                     [ file_guard ctx loc ~path_slot:ps ~op steps ])))
@@ -5256,7 +5366,7 @@ and named_call ctx ~want loc name args =
                    [ mk loc Types.String (Tast.Local ps);
                      mk loc Types.String (Tast.Local ds) ]) ]
        in
-       expect loc ~want
+       expect ctx loc ~want
          (mk loc Types.Unit
             (Tast.Let ([ (ps, from_); (ds, to_) ],
                        [ file_guard ctx loc ~path_slot:ps ~op:3 steps ])))
@@ -5277,12 +5387,12 @@ and named_call ctx ~want loc name args =
        prim Tast.Len index_ty [ a ]
      | Types.Vec _ ->
        let n = rt loc (Types.Int Types.I64) "flan_vec_len" [ a; here loc ] in
-       expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
+       expect ctx loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
      (* Extended rather than given a name of its own, for the reason [at] and
         [len] were extended over Vec: one question, one word. *)
      | Types.Map _ ->
        let n = rt loc (Types.Int Types.I64) "flan_map_len" [ a; here loc ] in
-       expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
+       expect ctx loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
      (* A dyn length is an i32 like every other length here, not a dyn holding
         one. [len] is what an index loop compares against, and handing back a
         boxed number would make [(< i (len xs))] a dyn comparison and a pair of
@@ -5290,7 +5400,7 @@ and named_call ctx ~want loc name args =
         once and narrowed the way the Vec's i64 above is. *)
      | Types.Dyn ->
        let n = unbox loc (Types.Int Types.I64) (rt loc Types.Dyn "flan_dyn_len" [ a ]) in
-       expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
+       expect ctx loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
      | other ->
        fail loc
          "len takes an array, a slice, a string, a Vec or a Map, found %s"
@@ -5302,7 +5412,7 @@ and named_call ctx ~want loc name args =
        (match target.Tast.ty with
         | Types.Vec _ ->
           let p, elem = vec_at ctx loc target idx in
-          expect loc ~want (mk loc elem (Tast.Deref p))
+          expect ctx loc ~want (mk loc elem (Tast.Deref p))
         (* One index, because a dyn container is one dimension: the nested
            [(at grid r c)] spelling walks a type the compiler can see through,
            and here it cannot. [(at (at g r) c)] is the spelling that works and
@@ -5310,7 +5420,7 @@ and named_call ctx ~want loc name args =
         | Types.Dyn ->
           (match idx with
            | [ i ] ->
-             expect loc ~want
+             expect ctx loc ~want
                (rt loc Types.Dyn "flan_dyn_at" [ target; check ctx ~want:Types.Dyn i ])
            | _ ->
              fail loc
@@ -5417,21 +5527,39 @@ and named_call ctx ~want loc name args =
           or (deref p)"
      | Some p ->
        let p, ty = check_place ctx a.Ast.loc p in
-       expect loc ~want (mk loc (Types.Ptr ty) (Tast.Addr p)))
+       expect ctx loc ~want (mk loc (Types.Ptr ty) (Tast.Addr p)))
   | "deref" ->
     arity loc name 1 args;
     let a = check ctx (List.hd args) in
     (match a.Tast.ty with
-     | Types.Ptr t -> expect loc ~want (mk loc t (Tast.Deref a))
+     | Types.Ptr t -> expect ctx loc ~want (mk loc t (Tast.Deref a))
      | other -> fail loc "deref takes a (Ptr T), found %s"
                   (Types.to_string other))
 
   (* ── Option ────────────────────────────────────────────────────── *)
+  (* (Some nil) cannot be built. Some marks a value present; nil is dyn's own
+     way of saying absent; a present absence is what would make nil and None
+     the same case of an (Option dyn) and break nil <-> None at the boundary
+     in both directions. Refused here at the literal, which the checker can
+     see the same way it sees any other [nil]; a dyn value that only turns
+     out to be nil once the program runs is caught by the runtime guard on
+     the value instead, named for what it refuses rather than just that it
+     does. *)
   | "Some" ->
     arity loc name 1 args;
     let inner = match want with Some (Types.Option t) -> Some t | _ -> None in
     let a = check ctx ?want:inner (List.hd args) in
-    expect loc ~want (mk loc (Types.Option a.Tast.ty) (Tast.Some_ a))
+    let a =
+      if not (Types.equal a.Tast.ty Types.Dyn) then a
+      else if is_nil_lit a then
+        Loc.failk "check/some-nil" loc
+          "(Some nil) cannot be built — Some marks a value present, and nil \
+           is dyn's own absence, so a present nil would make nil and None \
+           the same case of an (Option dyn), which nil <-> None at the \
+           boundary depends on staying apart. Use None instead"
+      else rt loc Types.Dyn "flan_dyn_need_not_nil" [ a ]
+    in
+    expect ctx loc ~want (mk loc (Types.Option a.Tast.ty) (Tast.Some_ a))
 
   (* ── the milestone-2 host primitives (plan.org) ────────────────── *)
   | "bytes" ->
@@ -5490,12 +5618,12 @@ and named_call ctx ~want loc name args =
     prim Tast.BytesToI64 (Types.Int Types.I64) [ byte_slice ctx (List.hd args) ]
   | "f64->bytes" ->
     arity loc name 1 args;
-    expect loc ~want
+    expect ctx loc ~want
       (to_bytes ctx loc Tast.F64ToBytes
          (check ctx ~want:(Types.Float Types.F64) (List.hd args)))
   | "i64->bytes" ->
     arity loc name 1 args;
-    expect loc ~want
+    expect ctx loc ~want
       (to_bytes ctx loc Tast.I64ToBytes
          (check ctx ~want:(Types.Int Types.I64) (List.hd args)))
   | "write-stdout" ->
@@ -5623,7 +5751,7 @@ and named_call ctx ~want loc name args =
         ]
       else []
     in
-    expect loc ~want (mk loc Types.Unit (Tast.Do (parts @ nl)))
+    expect ctx loc ~want (mk loc Types.Unit (Tast.Do (parts @ nl)))
   | "exit" ->
     arity loc name 1 args;
     prim Tast.Exit Types.Never [ check ctx ~want:index_ty (List.hd args) ]
@@ -5736,7 +5864,7 @@ and named_call ctx ~want loc name args =
           (if List.length params = 1 then "" else "s")
           (List.length args);
       let args = map2_lr (fun p a -> check ctx ~want:p a) params args in
-      expect loc ~want (mk loc ret (Tast.Call (name, args)))
+      expect ctx loc ~want (mk loc ret (Tast.Call (name, args)))
     | None ->
       if Hashtbl.mem ctx.env.datas name then
         fail loc
@@ -5847,11 +5975,11 @@ and generic_call ctx ~want loc name vars pats pret args =
                 name p.Ast.pname p.Ast.pvar (Types.to_string t) p.Ast.pname
             | _ -> ())
          gfn.Ast.fwhere);
-    expect loc ~want (mk loc cret (Tast.Call (name, targs)))
+    expect ctx loc ~want (mk loc cret (Tast.Call (name, targs)))
   end
   else
     let sym = instantiate ctx.env loc name vars !subst cparams cret in
-    expect loc ~want (mk loc cret (Tast.Call (sym, targs)))
+    expect ctx loc ~want (mk loc cret (Tast.Call (sym, targs)))
 
 (* Cache or generate, Odin's loop. The key is the whole concrete signature
    compared pairwise with [Types.equal] — [are_types_identical] — so calling
@@ -7916,7 +8044,7 @@ let expressions env (es : (Types.t option * Ast.expr) list) :
     List.rev
       (List.fold_left
          (fun acc (want, (e : Ast.expr)) ->
-            expect e.Ast.loc ~want (check ctx ?want e) :: acc)
+            expect ctx e.Ast.loc ~want (check ctx ?want e) :: acc)
          [] es)
   in
   (ts, Array.of_list (List.rev ctx.slot_tys),

lib/emit.ml

@@ -3372,6 +3372,11 @@ declare void @flan_dyn_print(i64)
 declare i64 @flan_dyn_need_i64(i64)
 declare double @flan_dyn_need_f64(i64)
 declare i32 @flan_dyn_need_bool(i64)
+; nil <-> None at an (Option T) boundary, and (Some nil)'s run-time half —
+; M2 queue item 4, check.ml's [box_option]/[unbox_option] and the [Some]
+; builtin.
+declare i32 @flan_dyn_is_nil(i64)
+declare i64 @flan_dyn_need_not_nil(i64)
 declare void @flan_dyn_root_push(ptr)
 declare void @flan_dyn_root_push_desc(ptr, ptr)
 declare void @flan_dyn_root_pop(i64)

runtime/flan_dyn.c

@@ -1003,6 +1003,24 @@ uint8_t flan_dyn_need_bool(flan_dyn v) {
   return (uint8_t)(dyn_payload(v) ? 1 : 0);
 }
 
+/* nil <-> None at an (Option T) boundary. Cannot trap — every dyn value
+ * answers this one way or the other. */
+int32_t flan_dyn_is_nil(flan_dyn v) {
+  return flan_dyn_tag(v) == FLAN_DYN_TAG_NIL ? 1 : 0;
+}
+
+/* (Some nil)'s run-time half: a dyn value the checker could not see was nil
+ * at compile time, reaching Some anyway. [op] is "some" rather than a Flan
+ * spelling of the call, matching how every other dyn trap here names the
+ * operation that refused. */
+flan_dyn flan_dyn_need_not_nil(flan_dyn v) {
+  if (flan_dyn_tag(v) == FLAN_DYN_TAG_NIL)
+    trap1(TYPE_TRAP, "some",
+          "Some cannot hold nil -- nil and None would become the same case "
+          "of an (Option dyn)", v);
+  return v;
+}
+
 /* ── Arithmetic ────────────────────────────────────────────────────────
  *
  * Two ints answer an int; anything else numeric answers a float. The promotion

runtime/flan_dyn.h

@@ -135,6 +135,16 @@ int64_t flan_dyn_need_i64(flan_dyn v);
 double  flan_dyn_need_f64(flan_dyn v);
 uint8_t flan_dyn_need_bool(flan_dyn v);
 
+/* nil <-> None at an (Option T) boundary, and (Some nil)'s refusal — M2 item
+ * 4. [flan_dyn_is_nil] is the tag test the boundary's runtime half needs and
+ * does not want to build out of [flan_dyn_tag] and a comparison at every call
+ * site; it answers 1 for nil and 0 for every other tag, and cannot trap.
+ * [flan_dyn_need_not_nil] is the other half: it answers [v] unchanged when
+ * [v] is not nil, and traps when it is — the run-time case of (Some nil),
+ * for a dyn value that is not known to be nil until the program runs. */
+int32_t  flan_dyn_is_nil(flan_dyn v);
+flan_dyn flan_dyn_need_not_nil(flan_dyn v);
+
 /* ── The collector ─────────────────────────────────────────────────────
  *
  * Mark-sweep, precise, and never moving. [flan_gc_init] is idempotent, and the

test/programs/nil-option.flan

@@ -0,0 +1,53 @@
+;;;; nil <-> None at (Option T) boundaries -- M2 queue item 4.
+;;;;
+;;;; nil is dyn's own absence and None is (Option T)'s; this is the boundary
+;;;; where the checker decides they are the same absence. [absent] and
+;;;; [opt-of] take it in at the two annotated sites that are not a function
+;;;; argument -- a global's declared type and a return type; [via-param]
+;;;; takes it in at the third, a parameter. [as-dyn] is the other direction:
+;;;; a written (Option i64) crossing into dyn becomes nil or the boxed
+;;;; payload. [box-it]/[unbox-opt] round-trip a value through both crossings.
+;;;;
+;;;; The last line is the trap: a dyn that is nil only once the program runs,
+;;;; reaching a bare i64. The literal [nil] two lines above it would have been
+;;;; refused at compile time instead -- see test_flan.ml and
+;;;; test_acceptance.ml's "nil at a bare T, compile time" row for that half.
+
+(defvar absent (Option i64) nil)
+
+(defn opt-of [flag bool] (Option i64)
+  (if flag (Some 7) nil))
+
+(defn via-param [o (Option i64)] i64
+  (match o (Some v) v None -1))
+
+(defn as-dyn [o (Option i64)] dyn o)
+
+(defn box-it [x i64] dyn x)
+(defn unbox-opt [d dyn] (Option i64) d)
+
+(defn maybe-nil [flag bool] dyn (if flag 5 nil))
+(defn take-i64 [n i64] i64 n)
+
+(defn show [o (Option i64)] ()
+  (print (match o (Some v) v None -1)) (println ""))
+
+(defn main [] ()
+  ;; nil -> None, at a global's declared type, a return type and a parameter.
+  (show absent)                                       ; -1
+  (show (opt-of true))                                ; 7
+  (show (opt-of false))                                ; -1
+  (print (via-param nil)) (println "")                 ; -1
+  (print (via-param (Some 3))) (println "")             ; 3
+
+  ;; None -> nil, crossing into dyn; Some x -> the boxed x.
+  (print (= (as-dyn None) nil)) (println "")            ; true
+  (print (as-dyn (Some 9))) (println "")                ; 9
+
+  ;; A value round-tripped through both crossings: typed -> dyn -> (Option T).
+  (show (unbox-opt (box-it 42)))                        ; 42
+
+  ;; The trap: a dyn that turns out to be nil only when the program runs,
+  ;; reaching a bare i64. flan_dyn_need_i64 owns the wording.
+  (print (take-i64 (maybe-nil false)))
+  (println ""))

test/programs/some-nil.flan

@@ -0,0 +1,14 @@
+;;;; (Some nil), the run-time half -- M2 queue item 4.
+;;;;
+;;;; The literal (Some nil) is refused at compile time (test_flan.ml). This is
+;;;; the other half: a dyn value the checker cannot see is nil until the
+;;;; program runs, reaching Some anyway. flan_dyn_need_not_nil owns the
+;;;; wording, the same way flan_dyn_need_i64 owns dyn-boundary.flan's.
+
+(defn maybe-nil [flag bool] dyn (if flag 5 nil))
+
+(defn main [] ()
+  (print (match (Some (maybe-nil true)) (Some x) x None -1))
+  (println "")                                          ; 5
+  (print (match (Some (maybe-nil false)) (Some x) x None -1))
+  (println ""))

test/test_acceptance.ml

@@ -3633,6 +3633,72 @@ level "1"
        exit status alone would not have shown. *)
     dyn_boundary ~x86:true ();
 
+    (* nil <-> None at (Option T) boundaries, and (Some nil) -- M2 queue item
+       4. [nil-option] carries the successful crossings: nil becoming None at
+       a global's declared type, a return type and a parameter; None becoming
+       nil crossing into dyn; and a value round-tripped through both
+       crossings via box-it/unbox-opt. Its last line is the trap named in
+       FIX.org's own words for the item -- a dyn that is nil only once the
+       program runs, reaching a bare i64 -- and the runtime owns the wording,
+       exactly as [dyn_boundary] above asserts on flan_dyn_need_i64's. The
+       literal [nil] that would have been refused two lines earlier instead
+       is test_flan.ml's row, not this one's: a program with it in does not
+       compile, so there is nothing here to run.
+
+       [some-nil] is the other trap this item adds, kept in its own file for
+       the reason [dyn_boundary] is one file per trap: one program, one
+       ending. (Some nil) written as a literal is also test_flan.ml's row;
+       this is the value the checker could not see was nil until the branch
+       that produces it ran. *)
+    let nil_option_out = "-1\n7\n-1\n-1\n3\ntrue\n9\n42\n" in
+    let nil_option ?opt ?x86 () =
+      let exe = compile ?opt ?x86 "programs/nil-option.flan" in
+      let code, text = run exe None in
+      let name =
+        "nil <-> None: the crossings, and the bare-T trap"
+        ^ (match opt with Some o -> ", " ^ o | None -> "")
+        ^ (match x86 with Some true -> ", --x86" | _ -> "")
+      in
+      if code <> 134
+         || not (contains text nil_option_out)
+         || not (contains text "int was wanted")
+      then begin
+        incr failures;
+        Printf.printf
+          "FAIL  %s\n        got: %S (exit %d)\n     wanted: %S then a trap \
+           (exit 134)\n"
+          name text code nil_option_out
+      end;
+      (try Sys.remove exe with Sys_error _ -> ())
+    in
+    nil_option ();
+    nil_option ~opt:"-O0" ();
+    nil_option ~x86:true ();
+    let some_nil_out = "5\n" in
+    let some_nil ?opt ?x86 () =
+      let exe = compile ?opt ?x86 "programs/some-nil.flan" in
+      let code, text = run exe None in
+      let name =
+        "(Some nil): the run-time trap"
+        ^ (match opt with Some o -> ", " ^ o | None -> "")
+        ^ (match x86 with Some true -> ", --x86" | _ -> "")
+      in
+      if code <> 134
+         || not (contains text some_nil_out)
+         || not (contains text "Some cannot hold nil")
+      then begin
+        incr failures;
+        Printf.printf
+          "FAIL  %s\n        got: %S (exit %d)\n     wanted: %S then a trap \
+           (exit 134)\n"
+          name text code some_nil_out
+      end;
+      (try Sys.remove exe with Sys_error _ -> ())
+    in
+    some_nil ();
+    some_nil ~opt:"-O0" ();
+    some_nil ~x86:true ();
+
     (* The root count, which is the part of this feature the runs above cannot
        check — and the reason has outlived the stub it was first written
        about. flan_dyn.c's trigger has a one-megabyte floor, and not one
@@ -3706,7 +3772,13 @@ level "1"
       [ "programs/dyn-basic.flan"; "programs/dyn-vec.flan";
         "programs/dyn-struct.flan";
         "programs/dyn-global.flan"; "programs/dyn-boundary.flan";
-        "programs/dyn-defer.flan" ];
+        "programs/dyn-defer.flan";
+        (* [unbox_option] binds the dyn it is testing to a fresh slot before
+           reading its tag twice, and that slot is the one new place M2 item
+           4 mints a dyn temporary the collector has to find — the same
+           question this list already asks of every other dyn-producing
+           boundary. *)
+        "programs/nil-option.flan"; "programs/some-nil.flan" ];
     (* And that the defer program still runs and still runs its defer: the
        count being right is not much use if the transfer path broke getting
        there. 1005 is the defer, 6 is the value the restart produced. *)

test/test_flan.ml

@@ -1166,9 +1166,78 @@ let () =
      for a key a map does not hold. It is always dyn. *)
   accepts "nil is a dyn literal"
     "(defn main [] i32 (let [n nil] (if (= n nil) 0 1)))";
-  rejects_check "nil at a typed want"
+  (* Superseded by the M2 item 4 boundary below: a literal [nil] at a bare
+     typed want is now refused by name, at compile time, rather than by the
+     generic dyn-boundary message — see "nil at a bare T is refused at
+     compile time" further down. *)
+
+  (* ── nil <-> None at (Option T), M2 queue item 4 ──────────────────
+     nil and None are the same absence at the one boundary where both are
+     meaningful. The three sites a dyn can be unboxed at own nil's half of
+     it too: a parameter, a return type and a global's declared type. *)
+  accepts "nil becomes None at a return type"
+    "(defn f [] (Option i64) nil)\n\
+     (defn main [] i32 (match (f) (Some _) 1 None 0))";
+  accepts "nil becomes None at a parameter"
+    "(defn h [o (Option i64)] i32 (match o (Some _) 1 None 0))\n\
+     (defn main [] i32 (h nil))";
+  accepts "nil becomes None at a global's declared type"
+    "(defvar ov (Option i64) nil)\n\
+     (defn main [] i32 (match ov (Some _) 1 None 0))";
+  (* The other direction: None crossing into dyn is nil, and a program can
+     compare the result the same way it compares any other nil. *)
+  accepts "None becomes nil crossing into dyn"
+    "(defn g [] dyn None)\n\
+     (defn main [] i32 (if (= (g) nil) 0 1))";
+  (* A bare T has no None to become. This nil is the one the checker can see
+     — the literal, right where the mismatch is — so it is refused here
+     rather than waiting for the run-time trap the same mismatch reaches for
+     one call deeper (dyn-not-visibly-nil case, test_acceptance.ml). *)
+  rejects_check "nil at a bare T is refused at compile time"
     "(defn take [n i32] i32 n)\n(defn main [] i32 (take nil))"
-    ~needle:"does not cross into a written type";
+    ~needle:"nil has no None to become";
+  rejects_check "nil at a bare T is refused at compile time, return position"
+    "(defn f [] i64 nil)\n(defn main [] i32 0)"
+    ~needle:"nil has no None to become";
+  (* (Some nil) would make nil and None the same case of an (Option dyn), so
+     it cannot be built — refused at compile time when the argument is the
+     literal nil, which is exactly what "the checker can see" means here. *)
+  rejects_check "(Some nil) is refused at compile time"
+    "(defn main [] i32 (let [o (Some nil)] 0))"
+    ~needle:"(Some nil) cannot be built";
+  (* (Option (Option T)) is legal on the typed side — nothing above refuses
+     the type — but boxing its Some of an inner None would box that None as
+     nil, indistinguishable from the outer None, so the crossing into dyn
+     does not exist for it. *)
+  rejects_check "(Option (Option T)) does not cross into dyn"
+    "(defn f [] (Option (Option i64)) None)\n\
+     (defn g [] dyn (f))\n\
+     (defn main [] i32 0)"
+    ~needle:"does not cross into dyn";
+  (* (Option dyn): the payload is already dyn, so [box_option]/[unbox_option]
+     treat it as the identity — no [box]/[unbox] call, just the tag test —
+     and the only thing that has to hold is that the payload is never nil,
+     which is (Some nil)'s refusal above and not this boundary's.
+
+     That is what the code does; it is not yet what a program can hold. A
+     value of type (Option dyn) is refused wherever it would need a GC root
+     — global, parameter, return or local slot — by the *separate*,
+     pre-existing per-type-descriptor pass (M2 item 2): the collector marks a
+     struct's dyn fields by their byte offsets, and (Option dyn)'s payload
+     has none, the same reason (Vec dyn) and (Map K dyn) are refused today.
+     Item 4 does not lift that gate; it only makes sure the boundary is
+     already correct for the day items 2/3 do. The refusal below is that
+     gate, not a nil-boundary message — proof the two are not tangled. *)
+  rejects_check "(Option dyn) is a legal type but not yet a storable value"
+    "(defn k [] (Option dyn) None)\n(defn main [] i32 0)"
+    ~needle:"no descriptor can find";
+  (* A full round trip through the boundary: a typed i64 boxed into dyn at
+     one annotated site, then read back as an (Option i64) at another. *)
+  accepts "a value round-trips through dyn and (Option T)"
+    "(defn box-it [x i64] dyn x)\n\
+     (defn unbox-opt [d dyn] (Option i64) d)\n\
+     (defn main [] i32\n\
+    \  (match (unbox-opt (box-it 42)) (Some x) (if (= x 42) 0 1) None 1))";
 
   (* The map operations ride the words the typed map already owns: get, put,
      len, has-key? — one question, one word, on both sides. has-key? on a

test/test_sanitize.ml

@@ -202,6 +202,17 @@ let corpus =
        amount of reading the offsets can. *)
     "programs/dyn-struct.flan", [];
     "programs/dyn-map.flan", [];
+    (* nil <-> None at (Option T), M2 queue item 4: an Option's tag is read
+       with a raw [Field] the surface language never writes (check.ml's
+       [box_option]/[unbox_option], the same access Render's structural
+       printer uses), so this is where a wrong tag offset or a wrong
+       direction of the comparison shows up as a read past the struct rather
+       than as a wrong answer. Both trap, by design — [nil-option] on a bare
+       T meeting a dyn nil, [some-nil] on (Some nil) built from a value the
+       checker could not see was nil — and the two-sided check above is what
+       ASan's build being asked to trap the same way the plain build does. *)
+    "programs/nil-option.flan", [];
+    "programs/some-nil.flan", [];
     "../spike/x86/p13-dyn-collect.flan", [];
     "programs/sand-headless.flan", [];
     "programs/signedness.flan", [];