diff --git a/lib/check.ml b/lib/check.ml
index 982a30a..afba075 100644
--- a/lib/check.ml
+++ b/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
-     does at an (Option T) boundary is the queue's own later item. *)
+     always dyn here: whatever it becomes at a typed want — None at an
+     (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),
diff --git a/lib/emit.ml b/lib/emit.ml
index 560b2cf..a4d05c8 100644
--- a/lib/emit.ml
+++ b/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)
diff --git a/runtime/flan_dyn.c b/runtime/flan_dyn.c
index 2d38d98..2594ed2 100644
--- a/runtime/flan_dyn.c
+++ b/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
diff --git a/runtime/flan_dyn.h b/runtime/flan_dyn.h
index a6f1e1c..60c7208 100644
--- a/runtime/flan_dyn.h
+++ b/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
diff --git a/test/programs/nil-option.flan b/test/programs/nil-option.flan
new file mode 100644
index 0000000..db89e9e
--- /dev/null
+++ b/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 ""))
diff --git a/test/programs/some-nil.flan b/test/programs/some-nil.flan
new file mode 100644
index 0000000..9a7f00e
--- /dev/null
+++ b/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 ""))
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 32559ee..6d1a7e7 100644
--- a/test/test_acceptance.ml
+++ b/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. *)
diff --git a/test/test_flan.ml b/test/test_flan.ml
index bac3efa..9640ab1 100644
--- a/test/test_flan.ml
+++ b/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
diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml
index eb6f3cd..dab72f8 100644
--- a/test/test_sanitize.ml
+++ b/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", [];