Three review findings on M2 item 4, none blocking

(Some nil) at an already-(Option T) want reported expect's bare-T
sentence instead of its own: checking the argument against inner's
element type routed a literal nil through expect's "wrap the type in
Option" refusal before Some's own is_nil_lit guard ever ran, and the
advice was nonsense there — the type already is one. The argument is
now checked with no want when it is syntactically nil, which is what a
bare nil resolves against on its own, so it arrives at Some's own
check still dyn and still nil.

no_fallback_slots cannot see the slot unbox_option mints: %dx/%ax are
the pool-ran-dry fallback for a temporary root_plan counted, and a
named local root_plan never counted emits neither mark. The comment
where nil-option.flan and some-nil.flan were added to that list said
otherwise; corrected to say what the check does and does not cover,
and to record that the slot was verified by reading the IR directly
instead — flan.unbox-opt's dyn slot is pushed, flan.as-dyn's is a
plain alloca correctly, since its element is always scalar there.

dyn_offsets falls through Option/Vec/Map with no arm of its own,
correct today only because Check.hidden_dyn refuses a dyn inside any
of them at every storage site first. Commented at the fallthrough,
naming hidden_dyn as the gate and the typed-container view (M2 item 3,
in review now) as the kind of change that could relax it for Vec/Map
without anything here pointing back.

lib/check.ml

@@ -5547,8 +5547,16 @@ and named_call ctx ~want loc name args =
      does. *)
   | "Some" ->
     arity loc name 1 args;
+    let arg = List.hd args in
     let inner = match want with Some (Types.Option t) -> Some t | _ -> None in
-    let a = check ctx ?want:inner (List.hd args) in
+    (* A literal [nil] is refused by this form's own message below, not by
+       [expect]'s bare-T refusal — checking it against [inner] here would
+       let a bare T's "wrap the type in Option" reach the reader even though
+       the type here is already wrapped in one. Checked with no want instead,
+       which is exactly what a bare [nil] resolves against on its own (see
+       [var]'s "nil" arm), so it arrives below still dyn and still nil. *)
+    let ast_nil = match arg.Ast.e with Ast.Var "nil" -> true | _ -> false in
+    let a = check ctx ?want:(if ast_nil then None else inner) arg in
     let a =
       if not (Types.equal a.Tast.ty Types.Dyn) then a
       else if is_nil_lit a then

lib/emit.ml

@@ -451,6 +451,16 @@ and dyn_offsets m (t : Types.t) : int list =
           — which is a run-time question a static descriptor cannot answer.
           Refused in [Check] rather than described wrongly here. *)
        | None -> acc)
+    (* [Types.Option], [Types.Vec] and [Types.Map] fall through here with no
+       arm of their own and answer no offsets, which is correct only because
+       nothing reaches this function holding one with a dyn inside it:
+       [Check.hidden_dyn] refuses that at every global, parameter, return and
+       frame slot first. If that gate is ever relaxed — the typed-container
+       view the M2 queue's item 3 is building is exactly the kind of change
+       that would relax it for [Vec]/[Map] — this arm has to grow alongside
+       it, the way the array and struct arms above already walk their own
+       storage; until then a silent [] here would be an unrooted dyn, not a
+       refusal. *)
     | _ -> acc
   in
   List.sort_uniq compare (go [] 0 t [])

test/test_acceptance.ml

@@ -3773,11 +3773,19 @@ level "1"
         "programs/dyn-struct.flan";
         "programs/dyn-global.flan"; "programs/dyn-boundary.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. *)
+        (* Included for the same reason every dyn program is, though this
+           check cannot see the slot M2 item 4 actually added: [%dx]/[%ax]
+           are the pool-ran-dry fallback for a temporary [root_plan] COUNTED
+           and could not find room for, and [unbox_option]'s fresh slot is a
+           named local [root_plan] never counted at all — a slot outside
+           that pool emits neither mark and this grep is silent about it
+           either way. That slot was checked by reading the IR directly
+           instead: [flan.unbox-opt]'s dyn slot is pushed with
+           [flan_dyn_root_push]; [flan.as-dyn]'s slot is a plain alloca with
+           none, correct because its element type is always scalar there.
+           This row is still worth keeping — it is real evidence about
+           every *other* dyn temporary these two programs mint through the
+           ordinary call-argument and return-value paths. *)
         "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

test/test_flan.ml

@@ -1205,6 +1205,16 @@ let () =
   rejects_check "(Some nil) is refused at compile time"
     "(defn main [] i32 (let [o (Some nil)] 0))"
     ~needle:"(Some nil) cannot be built";
+  (* The same refusal where the argument's own want is already (Option T)'s
+     inner type — a function parameter typed (Option i64), say. [nil] checked
+     against that inner type directly would hit [expect]'s bare-T refusal
+     first ("wrap the type in Option"), which is nonsense here: the type
+     already is one. A regression for the review that found it. *)
+  rejects_check "(Some nil) at an already-Option want gets Some's message, \
+                 not expect's bare-T one"
+    "(defn f [o (Option i64)] i64 (match o (Some v) v None -1))\n\
+     (defn main [] i32 (f (Some nil)))"
+    ~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