diff --git a/TODO.org b/TODO.org
index e9589c05..bc5923fb 100644
--- a/TODO.org
+++ b/TODO.org
@@ -45,6 +45,16 @@ Decided (133): =x?= is a bool; =if x?=, =elif x?=, =while x?= and the rest of an
 make a local Option its payload in the block, in place (not a copy). Assigning an Option
 to it there is refused rather than ending the narrowing; =e? as g= names what a test
 found. Rules out =if let g = x= over a plain name, which is refused toward these.
+** DONE A T is wrapped where a T? is wanted
+CLOSED: [2026-09-26]
+Decided (138), like Swift: one level per boundary, the literal built at T first; not
+inside a container. Rules out implicit unwrapping: a T? where a T is wanted stays refused.
+** DONE A kept when over an Option body flattens one level
+CLOSED: [2026-09-26]
+Decided (140), reversing 125a: a kept =when=, else-less =if=/=elif= or =if let= chain whose
+arm is already a =T?= is a =T?=, and =T= beside =T?= arms is =T?=; a =T??= arm stays =T??=.
+Where =T??= is wanted the arm is Some of it. Rules out telling "no branch matched" apart
+from "a branch gave None" without asking for =T??=.
 ** TODO The stepper does not step inside an optional chain
 =Ast.step_expr= treats a =Chain= as a leaf (its catch-all), so nothing in a chain's
 body gets a step point of its own.
@@ -64,8 +74,8 @@ Option or a dyn holds (130); over any other type, and =_=, it is refused toward
 ** DONE when as a value, and get as a checked lookup
 CLOSED: [2026-09-26]
 Every one-armed =if= (and a =cond= with no =:else=) is a =when=; kept — a =let= value, a
-call's argument, a lambda's return — it is =Option(T)=, nested over an Option body
-(Rust's =bool::then=), and body-or-nil where a dyn is wanted. A =_=-inferred return's
+call's argument, a lambda's return — it is =Option(T)=, and body-or-nil where a dyn is
+wanted. Over an Option body it was nested (Rust's =bool::then=, 125a); 140 reversed that. A =_=-inferred return's
 last form is not kept. =get= over dyn text or vec is nil when out of range; =.field= still traps.
 
 ** NEXT str and String
diff --git a/lib/check.ml b/lib/check.ml
index fc987993..61500504 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -2891,6 +2891,13 @@ let rec bind_ty ?(widen = false) ?(ro = true) subst (pat : Types.t)
     bind_ty ~ro:(m = Types.Const) subst p a
   | Types.Vec p, Types.Vec a
   | Types.Option p, Types.Option a -> inner p a
+  (* A plain value at a [$t?] parameter binds [$t] to its own type, and
+     [expect] wraps it (decision 138). At the top of an argument only, as the
+     widening below: an element of a Vec is never wrapped, so [(Vec $t?)]
+     meets a [(Vec i32)] as a mismatch. *)
+  | Types.Option p, a
+    when widen && (match a with Types.Dyn | Types.Never -> false | _ -> true) ->
+    bind_ty ~widen subst p a
   | Types.Array (n, p), Types.Array (m, a) -> Int64.equal n m && inner p a
   | Types.Map (k, v), Types.Map (k', v') -> inner k k' && inner v v'
   (* Each function type against its own. *)
@@ -3227,6 +3234,14 @@ let rec literal_arith (e : Ast.expr) : int64 option =
    over literals alone. *)
 let lone_literal (e : Ast.expr) = is_literal e || literal_arith e <> None
 
+(* Set for one [check_value] entry: the literal is checked at the Option
+   itself, not wrapped, so a refusal names the Option (decision 138). *)
+let skip_wrap = ref false
+
+(* [None] as written, which has no type until an Option is asked of it. *)
+let is_none_lit (e : Ast.expr) =
+  match e.Ast.e with Ast.Var "None" -> true | _ -> false
+
 (* A value whose type comes only from defaults — a literal, [nil], [(Some 3)],
    arithmetic over literals, a [do] ending in one — so it takes the type of whatever
    meets it. An arm of this kind is checked after the others, at their type,
@@ -3811,6 +3826,12 @@ let lit_admits kind (t : Types.t) =
   | `Box, t -> not (Types.equal t Types.Dyn)
   | _ -> false
 
+(* What a use at [t] says about a literal local: an (Option T) wanted of it
+   says T, since the local is built at T and then wrapped (decision 138), so
+   [let w: i64? = x] makes [x] the i64 [let w: i64 = x] does. *)
+let rec lit_payload (t : Types.t) =
+  match t with Types.Option p -> lit_payload p | t -> t
+
 (* The rounds a session may take before its last guesses are checked as
    they stand. Merging makes two the usual count; the bound only stops a
    pathological program from looping. *)
@@ -5036,7 +5057,7 @@ let no_bare_nil (ops : Tast.expr list) =
       | Some t -> nil_has_no_none nil.Tast.loc t
       | None -> ()
 
-let expect ctx loc ~want (got : Tast.expr) =
+let rec expect ctx loc ~want (got : Tast.expr) =
   match want with
   | None -> got
   | Some w ->
@@ -5105,6 +5126,21 @@ let expect ctx loc ~want (got : Tast.expr) =
       | (Types.Slice (Types.Const, _) | Types.Ptr (Types.Const, _)), _
         when Types.const_widens ~from:got.Tast.ty ~into:w ->
         { got with Tast.ty = w }
+      (* Decision 138, Swift's rule: a T where a (Option T) is wanted is
+         [Some] of it. One level each time — a T? into a T?? is [Some] of the
+         Option, never the Option itself — and the payload goes through this
+         same boundary first, so a T into a T?? is [Some (Some t)] and an i32
+         into an (Option i64) is widened, then wrapped. Never the other way:
+         a T? where a T is wanted is still refused, and a dyn is left to the
+         nil <-> None arms above. When the payload is refused too, the
+         refusal below names the Option, as it did before. *)
+      | Types.Option t, g
+        when (match g with Types.Dyn | Types.Never -> false | _ -> true)
+             && not (Types.fits ~expected:w ~actual:g) ->
+        (match expect ctx loc ~want:(Some t) got with
+         | v when Types.fits ~expected:t ~actual:v.Tast.ty -> mk loc w (Tast.Some_ v)
+         | _ -> got
+         | exception Loc.Error _ -> got)
       | _ -> got
     in
     if Types.fits ~expected:w ~actual:got.Tast.ty then got
@@ -5205,8 +5241,16 @@ let arm_join (a : Types.t) (b : Types.t) =
       match Types.const_join a b with
       | Some j -> Some j
       | None ->
+        (* A T beside a T? meets at the T?, the T wrapped in [Some]
+           (decision 138). Only the plain side moves, and by one level. *)
+        let wraps p u =
+          (match u with Types.Option _ | Types.Unit -> false | _ -> true)
+          && (Types.equal p u || Types.widens_to ~from:u ~into:p)
+        in
         (match a, b with
          | Types.Dyn, _ | _, Types.Dyn -> Some Types.Dyn
+         | Types.Option p, u when wraps p u -> Some a
+         | u, Types.Option p when wraps p u -> Some b
          | _ -> None)
 (* The type two untyped literals meet at: the wider of their own types, and
    an integer beside a float at the float — [(if c 1 2.5)] is an f32, though
@@ -6166,7 +6210,26 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
   ctx.tail <- false;
   let used = ctx.used || List.memq e ctx.kept in
   ctx.used <- false;
+  let skipping = !skip_wrap in
+  skip_wrap := false;
   match e.Ast.e with
+  (* A literal where an (Option T) is wanted is built at T and then wrapped
+     (decision 138): [s = -1] over an [i64?] is [Some] of an i64 -1. It has
+     no type until one is asked of it, so it is asked the payload's, rather
+     than being built at a default and wrapped at the wrong width. *)
+  | Ast.Int _ | Ast.UInt _ | Ast.Float _ | Ast.Byte _ | Ast.Call _ | Ast.Arr (_ :: _)
+    when (match want with Some (Types.Option _) -> not skipping | _ -> false)
+         && (lone_literal e || (match e.Ast.e with Ast.Arr _ -> true | _ -> false)) ->
+    let w = Option.get want in
+    let t = match w with Types.Option t -> t | _ -> assert false in
+    (match trial ctx (fun () -> check ctx ~want:t e) with
+     | Ok v when Types.fits ~expected:t ~actual:v.Tast.ty -> mk loc w (Tast.Some_ v)
+     | Ok v -> expect ctx loc ~want v
+     (* Refused at T: checked again at the Option as it was before 138, so
+        the refusal names what was wanted, [str?], and not only its payload. *)
+     | Error _ ->
+       skip_wrap := true;
+       check ctx ?want e)
   (* A negative literal in a generic body, at an instantiation that made it
      unsigned. The cast the ordinary refusal names would be wrong at every
      other type the function is called at, so the fix is one that needs no
@@ -7019,18 +7082,19 @@ and var ctx ?(qualified = false) loc ~want name =
     | Some ({ blit = Some key; _ } as b)
       when (match ctx.lits, want with
             | Some s, Some t ->
+              let t = lit_payload t in
               s.recording && not !lit_quiet
               && (Types.equal t Types.Dyn
                   || lit_admits (Option.value (lit_kind key) ~default:`Int) t)
             | _ -> false) ->
-      let s = Option.get ctx.lits and t = Option.get want in
+      let s = Option.get ctx.lits and t = lit_payload (Option.get want) in
       let operand = List.memq loc !lit_operand_locs in
       let c = if operand || Types.equal t Types.Dyn then Hint else Up in
       lit_add s key (c, t, loc);
       (try expect ctx loc ~want (mk loc b.bty (Tast.Local b.slot))
        with Loc.Error _ when lit_kind key <> Some `Box && not operand ->
          s.dirty <- true;
-         mk loc t (Tast.Local b.slot))
+         expect ctx loc ~want (mk loc t (Tast.Local b.slot)))
     | Some b ->
       expect ctx loc ~want (local_of loc b)
     (* A local of the enclosing function, in a body that was lifted out of it:
@@ -8628,12 +8692,31 @@ and check_if_once ctx ~tail ~used ?want loc c t e =
          | Some Types.Dyn -> Some Types.Dyn
          | _ -> None
        in
-       let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want:tw t)) in
+       let arm w = branch ctx (fun () -> in_tail (fun () -> check ctx ?want:w t)) in
+       (* At an Option want the arm is asked the payload first, and the chain
+          wraps it; refused there, it is asked the Option itself, which it
+          then is (decision 140). So a T?? wanted of a T? arm is Some of it,
+          and the chain's own None stays the outer one. *)
+       let t, at_payload =
+         match want with
+         | Some (Types.Option _) ->
+           (match trial ctx (fun () -> arm tw) with
+            | Ok t -> t, true
+            | Error d ->
+              (match trial ctx (fun () -> arm want) with
+               | Ok t -> t, false
+               | Error _ -> raise (Loc.Error d)))
+         | _ -> arm tw, false
+       in
        let rest ~used ?want () =
          branch ctx (fun () ->
              ctx.tail <- tail; ctx.used <- used; check ctx ?want e)
        in
        match t.Tast.ty with
+       | ty when at_payload && not (Types.equal ty Types.Never) ->
+         let oty = Option.get want in
+         let e = rest ~used:true ~want:oty () in
+         mk loc oty (Tast.If (c, mk loc oty (Tast.Some_ t), e))
        | Types.Unit ->
          expect ctx loc ~want
            (mk loc Types.Unit (Tast.If (c, t, rest ~used:false ())))
@@ -8643,6 +8726,12 @@ and check_if_once ctx ~tail ~used ?want loc c t e =
        | Types.Dyn ->
          let e = rest ~used:true ~want:Types.Dyn () in
          expect ctx loc ~want (mk loc Types.Dyn (Tast.If (c, t, e)))
+       (* An arm that is already an Option is the chain's value as it is,
+          and [None] when no test holds — one level flattened (decision
+          140): an arm's None and no arm running are one answer. *)
+       | Types.Option _ as o ->
+         let e = rest ~used:true ~want:o () in
+         expect ctx loc ~want (mk loc o (Tast.If (c, t, e)))
        | ty ->
          let oty = Types.Option ty in
          let e = rest ~used:true ~want:oty () in
@@ -8659,14 +8748,33 @@ and check_if_once ctx ~tail ~used ?want loc c t e =
     let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in
     let e = branch ctx (fun () -> in_tail (fun () -> check ctx ?want e)) in
     mk loc t.Tast.ty (Tast.If (c, t, e))
-  | Some e when want = None && adapts t && not (adapts e)
+  | Some e when want = None
+                && ((adapts t && not (adapts e || is_none_lit e))
+                    (* [if c then None else 5]: the else arm decides T, and
+                       None meets it at T? below, as the other order does. *)
+                    || (is_none_lit t && not (is_none_lit e)))
                 && not (and_sentinel e) ->
     (* A literal has no type of its own until something asks, so with no
        expectation the other arm decides: [(if c 4000000 n)] over an i64 [n]
        is an i64, as [(+ 4000000 n)] is. *)
     let e = branch ctx (fun () -> in_tail (fun () -> check ctx e)) in
     let twant = if e.Tast.ty = Types.Never then None else Some e.Tast.ty in
-    let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want:twant t)) in
+    let then_at w = branch ctx (fun () -> in_tail (fun () -> check ctx ?want:w t)) in
+    (* [None] or [Some(1)] beside a plain T: the two meet at T?, the other
+       arm wrapped (decision 138). Tried only once the arm is refused at T,
+       so an arm that fits T is never an Option. *)
+    let t, e =
+      match e.Tast.ty with
+      | Types.Option _ | Types.Dyn | Types.Unit | Types.Never -> then_at twant, e
+      | ety ->
+        (match trial ctx (fun () -> then_at twant) with
+         | Ok t -> t, e
+         | Error _ ->
+           let oty = Types.Option ety in
+           (match trial ctx (fun () -> then_at (Some oty)) with
+            | Ok t -> t, expect ctx e.Tast.loc ~want:(Some oty) e
+            | Error _ -> then_at twant, e))
+    in
     let ty = if e.Tast.ty = Types.Never then t.Tast.ty else e.Tast.ty in
     mk loc ty (Tast.If (c, t, e))
   | Some e ->
@@ -8730,7 +8838,24 @@ and check_if_once ctx ~tail ~used ?want loc c t e =
           | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v)
           | None -> None
         in
-        match at_then () with
+        (* The else arm refused at T and fine at T? — [None], [Some(1)] —
+           and the two meet at T?, the then arm wrapped (decision 138). *)
+        let at_option () =
+          match t.Tast.ty with
+          | Types.Option _ | Types.Dyn | Types.Unit -> None
+          | ty ->
+            let oty = Types.Option ty in
+            (match
+               trial ctx (fun () ->
+                   branch ctx (fun () -> in_tail (fun () -> check ctx ~want:oty e)))
+             with
+             | Ok v when Types.equal v.Tast.ty oty -> Some (oty, v)
+             | _ -> None)
+        in
+        (* Only where the arms met nowhere else, so nothing that met before
+           meets differently: a dyn else arm still meets at dyn. *)
+        match
+          (match at_then () with
         | Ok v ->
           (match opened_dyn ~box:(to_dyn ctx) v with
            | Some box -> Some (Types.Dyn, box)
@@ -8757,7 +8882,10 @@ and check_if_once ctx ~tail ~used ?want loc c t e =
               | Some r -> Some r
               | None ->
                 Some (t.Tast.ty, expect ctx v.Tast.loc ~want:(Some t.Tast.ty) v))
-           | Error _ -> None)
+           | Error _ -> None))
+        with
+        | None -> at_option ()
+        | j -> j
     in
     match joined with
     | Some (j, v) ->
@@ -8846,9 +8974,9 @@ and check_if_once ctx ~tail ~used ?want loc c t e =
    branch evaluates to. Kept — a [let]'s value, an argument, a return, or
    anything else with a type wanted of it — it answers (Option T): [Some] of
    the branch when the test held and [None] when it did not. A branch that
-   is already an Option is not flattened: the answer is (Option (Option T)),
-   Rust's [bool::then], so [None] from the branch and a failed test stay two
-   answers.
+   is already an Option is that Option, flattened one level (decision 140,
+   Kotlin's [?.] rather than Rust's [bool::then]): [None] from the branch and
+   a failed test are one answer. A (Option (Option T)) branch stays one.
 
    Dyn has no Option. Where a dyn is wanted, or the branch is a dyn, a false
    test answers nil and a true one the branch's value — one absence, as a
@@ -8868,17 +8996,26 @@ and check_when ctx ~used ?want loc c
   | Some Types.Dyn ->
     let t = branch_at ~want:Types.Dyn () in
     mk loc Types.Dyn (Tast.If (c, t, nil ()))
-  | Some (Types.Option inner) ->
-    let t = branch_at ~want:inner () in
-    let oty = Types.Option inner in
-    let some = if t.Tast.ty = Types.Never then t else mk loc oty (Tast.Some_ t) in
-    mk loc oty (Tast.If (c, some, mk loc oty Tast.None_))
+  | Some (Types.Option inner as oty) ->
+    (* The payload first, wrapped; refused there, the Option itself, which
+       the branch then is (decision 140). *)
+    let t =
+      match trial ctx (fun () -> branch_at ~want:inner ()) with
+      | Ok t -> if t.Tast.ty = Types.Never then t else mk loc oty (Tast.Some_ t)
+      | Error d ->
+        (match trial ctx (fun () -> branch_at ~want:oty ()) with
+         | Ok t -> if t.Tast.ty = Types.Never then t else expect ctx loc ~want:(Some oty) t
+         | Error _ -> raise (Loc.Error d))
+    in
+    mk loc oty (Tast.If (c, t, mk loc oty Tast.None_))
   | None when not used -> stmt (branch_at ())
   | _ ->
     let t = branch_at () in
     if valueless t then stmt t
     else if Types.equal t.Tast.ty Types.Dyn then
       expect ctx loc ~want (mk loc Types.Dyn (Tast.If (c, t, nil ())))
+    else if (match t.Tast.ty with Types.Option _ -> true | _ -> false) then
+      expect ctx loc ~want (mk loc t.Tast.ty (Tast.If (c, t, mk loc t.Tast.ty Tast.None_)))
     else
       let oty = Types.Option t.Tast.ty in
       expect ctx loc ~want
@@ -9800,11 +9937,38 @@ and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) =
     | _ -> ty
   in
   let is_nil = match v.Ast.e with Ast.Var "nil" -> true | _ -> false in
+  (* Quietly: what [v] is on its own terms is not a use of a literal local
+     inside it — [[x]] read with no want would pin x at its guess, and the
+     annotation's want below is the use that says what x is. *)
+  let own_ty () =
+    let was = !lit_quiet in
+    lit_quiet := true;
+    Fun.protect ~finally:(fun () -> lit_quiet := was) (fun () ->
+        probe ctx loc (fun () -> (check ctx v).Tast.ty))
+  in
   if ty <> Types.Dyn && not is_nil
-     && probe ctx loc (fun () -> (check ctx v).Tast.ty) = Some Types.Dyn
+     && own_ty () = Some Types.Dyn
      (* A keyword naming one of an enum's members is that member at the
         enum's type, not a dyn: [let d: Dir = :north]. *)
      && not (match ty, v.Ast.e with Types.Enum _, Ast.Kw _ -> true | _ -> false)
+     (* An array literal that is a dyn vector only because its elements do
+        not agree among themselves — [[1, None]] — is built at the annotation
+        when every element fits it, as [x: [2 i32?] = [1, None]] (decision
+        138). Nothing is converted: the literal is built at T. *)
+     && not (let rec holds_option = function
+                | Types.Option _ -> true
+                | Types.Array (_, t) | Types.Slice (_, t) -> holds_option t
+                | _ -> false
+              in
+              let rec elems_option = function
+                | Types.Array (_, t) | Types.Slice (_, t) -> holds_option t
+                | Types.Option t -> elems_option t
+                | _ -> false
+              in
+              match v.Ast.e with
+              | Ast.Arr _ when elems_option ty ->
+                probe ctx loc (fun () -> ignore (check ctx ~want:ty v)) <> None
+              | _ -> false)
   then begin
     let tn = tyname loc ty in
     let numeric = match ty with Types.Int _ | Types.Float _ -> true | _ -> false in
@@ -9960,7 +10124,7 @@ and check_array_gen ctx ~want loc dims f =
        ~element:(fun idxs -> mk loc elem (Tast.CallPtr (fv, idxs))))
 
 and check_match ctx ?(tail = false) ?(used = false) ?(stmt = false) ?(opt = false)
-    ?opt_rest ?want loc scrutinee arms =
+    ?(flat = false) ?opt_rest ?want loc scrutinee arms =
   (* [stmt] is an [if let] with no else: a statement, Unit whatever its arm
      answers, as a one-armed [if] is when nothing keeps it. [opt] is one that
      is kept: its arm answers [Some], and the arm with no body [None]. *)
@@ -9969,7 +10133,11 @@ and check_match ctx ?(tail = false) ?(used = false) ?(stmt = false) ?(opt = fals
   let want0 = want in
   let want =
     if stmt then None
-    else if opt then (match want with Some (Types.Option i) -> Some i | _ -> None)
+    else if opt then
+      (match want with
+       | Some (Types.Option _) when flat -> want
+       | Some (Types.Option i) -> Some i
+       | _ -> None)
     else want
   in
   let s = check ctx scrutinee in
@@ -10337,8 +10505,24 @@ and check_match ctx ?(tail = false) ?(used = false) ?(stmt = false) ?(opt = fals
     let idx = List.mapi (fun i r -> (i, r)) resolved in
     if !want <> None then idx
     else
-      List.filter (fun (_, r) -> not (literal_arm r)) idx
-      @ List.filter (fun (_, r) -> literal_arm r) idx
+      let typed = List.filter (fun (_, r) -> not (literal_arm r)) idx in
+      (* A bare [None] that would be checked first has nothing to take its
+         type from and was always refused; it goes after the others, so it
+         meets their T at T? (decision 138). Only the leading ones move, so
+         no order that checked before changes. *)
+      let none_arm (_, ((a : Ast.arm), _, _)) =
+        match List.rev a.Ast.body with last :: _ -> is_none_lit last | [] -> false
+      in
+      let rec lead acc = function
+        | x :: rest when none_arm x -> lead (x :: acc) rest
+        | rest -> (List.rev acc, rest)
+      in
+      let nones, typed =
+        match lead [] typed with
+        | _ :: _ as nones, rest when List.length nones < List.length idx -> nones, rest
+        | _ -> [], typed
+      in
+      typed @ List.filter (fun (_, r) -> literal_arm r) idx @ nones
   in
   let checked =
     map_lr
@@ -10403,6 +10587,19 @@ and check_match ctx ?(tail = false) ?(used = false) ?(stmt = false) ?(opt = fals
                         (head, (ctx.scope, ctx.ret), w, d);
                       Error d)
                in
+               (* Where it would be refused: an arm fine at T? — [None],
+                  [Some(1)] — meets a T join at T? (decision 138), and
+                  [arm_join] wraps the arms before it. *)
+               let refused () =
+                 let fallback () = at !want () in
+                 match w with
+                 | Types.Option _ | Types.Dyn | Types.Unit -> fallback ()
+                 | _ ->
+                   let oty = Types.Option w in
+                   (match trial ctx (at (Some oty)) with
+                    | Ok b when Types.equal b.Tast.ty oty -> b
+                    | _ -> fallback ())
+               in
                match at_join () with
                | Ok b ->
                  (match opened_dyn ~box:(to_dyn ctx) b with
@@ -10418,10 +10615,10 @@ and check_match ctx ?(tail = false) ?(used = false) ?(stmt = false) ?(opt = fals
                   with
                   | Ok b -> b
                   | Error own when String.equal own.Loc.kind not_kept ->
-                    at !want ()
+                    refused ()
                   | Error own when is_mismatch d && not (is_mismatch own) ->
                     at None ()
-                  | Error _ -> at !want ())
+                  | Error _ -> refused ())
              else block ctx ?want:!want a.Ast.aloc a.Ast.body
            in
            let body =
@@ -10539,6 +10736,14 @@ and check_match ctx ?(tail = false) ?(used = false) ?(stmt = false) ?(opt = fals
             match r with
             | Some e -> e
             | None -> rt a.Ast.aloc Types.Dyn "flan_dyn_nil" [])
+      (* Already an Option: the whole, one level flattened (decision 140). *)
+      | Some (Types.Option _ as o) when flat || want0 = None ->
+        opt_result := Some o;
+        let r = rest ~used:true ~want:o () in
+        fill Fun.id (fun a ->
+            match r with
+            | Some e -> e
+            | None -> mk a.Ast.aloc o Tast.None_)
       | Some t ->
         let oty = Types.Option t in
         opt_result := Some oty;
@@ -10701,9 +10906,22 @@ and check_if_let ctx ~tail ~used ?want loc scrutinee (arm : Ast.arm) els =
                   ctx.tail <- tail; ctx.used <- used; check ctx ?want e))
            els
        in
+       (* The arm at the payload first, as [check_when] asks it; refused
+          there, at the Option itself (decision 140). *)
+       let go ~flat () =
+         check_match ctx ~tail ~used:true ~opt:true ~flat ?opt_rest ?want loc scrutinee
+           [ arm; wild [] ]
+       in
        expect ctx loc ~want
-         (check_match ctx ~tail ~used:true ~opt:true ?opt_rest ?want loc scrutinee
-            [ arm; wild [] ]))
+         (match want with
+          | Some (Types.Option _) ->
+            (match trial ctx (go ~flat:false) with
+             | Ok r -> r
+             | Error d ->
+               (match trial ctx (go ~flat:true) with
+                | Ok r -> r
+                | Error _ -> raise (Loc.Error d)))
+          | _ -> go ~flat:false ()))
   | Some e ->
     check_match ctx ~tail ~used ?want loc scrutinee [ arm; wild [ e ] ]
   | None ->
@@ -16732,6 +16950,12 @@ and generic_call ctx ~want loc name vars pats pret args =
             call with no type variables in it. *)
          | _ ->
            (match subst_ty !subst pat, a.Tast.ty with
+            (* A plain value at a [$t?] parameter, which [bind_ty] bound
+               through the Option: wrapped now that $t is known (decision
+               138). *)
+            | Types.Option _ as o, at
+              when (match at with Types.Option _ | Types.Dyn | Types.Never -> false | _ -> true) ->
+              expect ctx a.Tast.loc ~want:(Some o) a
             | Types.Fn (ps, r), Types.CFn (ps', r') ->
               if Types.equal (Types.Fn (ps, r)) (Types.Fn (ps', r')) then
                 mk a.Tast.loc (Types.Fn (ps, r))
@@ -17696,7 +17920,9 @@ let builtins : (string * string * string) list =
     (* Option *)
     ("Some", "Some [T] (Option T)",
      "Wraps a value as a present Option. None is the other half, and is \
-      written as a name rather than as a call.");
+      written as a name rather than as a call. Where an (Option T) is \
+      expected a T is wrapped with no Some written, one level at a time; an \
+      Option is never unwrapped that way.");
 
     (* the host primitives *)
     ("bytes", "bytes [str Allocator?] [u8]",
diff --git a/spec-syntax.md b/spec-syntax.md
index 4299e0e1..7c85a91f 100644
--- a/spec-syntax.md
+++ b/spec-syntax.md
@@ -244,6 +244,16 @@ Each item: the proposal, then the reason in one line.
     holds — `a?.f(x)`, `a?[i]`, `a?.b.c`. A result that is already an Option
     is not wrapped again, so `a?.b?.c` is one Option. A rest with no value
     makes the whole a statement. `~o1` is a fresh name no reader produces.
+  - A `T` where a `T?` is wanted is `Some` of it (decision 138): an
+    assignment, a `let` with a type, an argument, a return, a struct field, an
+    array or `Vec` element, and an `if` or `match` arm beside an Option arm.
+    A literal is built at `T` first, so `s = -1` over an `i64?` is `Some(-1)`
+    at i64. One level at a time: a `T` into a `T??` is `Some(Some(t))`, a `T?`
+    into a `T??` is `Some` of it. A `$t` meeting `$u?` binds `$u` to `T`.
+    Never inside a container (`Vec(i32)` is not a `Vec(i32?)`), and never the
+    other way: a `T?` where a `T` is wanted still needs `!`, `??`, `x?` or
+    `as`. A kept chain whose arms are a `T` and a `T?` is a `T?` (decision
+    140, under `when c`). **Built.**
 - **Casts and type-taking builtins are calls:** `i32(x)`, `vec-new(u8)`,
   `max-value(u8)`, `the([3 f32], [1 2 3.5])`. A pointer cast is the type
   called: `Ptr(Color)(p)` reads `((Ptr Color) p)`. **Built.**
@@ -307,7 +317,13 @@ Each item: the proposal, then the reason in one line.
   A `when` whose value is kept (a `let`'s value, an argument, a return) gives
   `Some(a)` when `c` holds and `None` when it does not; where a `dyn` is
   wanted, `a` or `nil`. As a statement it gives nothing. An `if`/`elif` chain
-  with no `else` is the same when kept: `None` when no test holds. **Built.**
+  with no `else` is the same when kept: `None` when no test holds. When `a`
+  is already an Option it is not wrapped again (decision 140): `when c then
+  o` over an `i32?` is an `i32?`, `None` when `c` fails or `o` is `None`, and
+  a chain mixing `T` and `T?` arms is a `T?`. One level only: an arm that is
+  a `T??` gives a `T??`. Where an Option of the arm's type is wanted, as a
+  `T??` over a `T?` arm, the arm is `Some` of its value and a failed test is
+  the outer `None`. `if let` with no `else` follows the same rule. **Built.**
 - **`if let P = v`** plus a block reads as `(if-let [P v] then)`; `elif` and
   `else` follow as for `if`, the rest of the chain being the `if-let`'s else.
   `elif let P = v` is a further `if-let` nested in that else.
diff --git a/test/programs/autowrap.fln b/test/programs/autowrap.fln
new file mode 100644
index 00000000..a63a82a6
--- /dev/null
+++ b/test/programs/autowrap.fln
@@ -0,0 +1,148 @@
+;; A T where a T? is wanted is Some of it (decision 138): each position,
+;; a literal built at the payload's type, nested Options, generics, and the
+;; arms of an if, a match and a kept chain.
+
+struct P
+  a: i64?
+  b: i32?
+
+fn show(o: i32?) -> i32 = o ?? -9
+
+fn back(b: bool, x: i32) -> i32?
+  if b
+    return x
+  None
+
+fn pick(b: bool, x: i32) -> i32?
+  if b then x else None
+
+fn pick2(b: bool, x: i32) -> i32?
+  if b then None else x
+
+fn two(o: Option(i32?)) -> str
+  match o
+    Some(i) -> if i? then "some some" else "some none"
+    None -> "none"
+
+fn first(o: $u?) -> $u = o!
+
+fn wrap(x: $t) -> $t? = x
+
+;; A generic body's own $t handed to a $u? parameter.
+fn through(x: $t) -> $t = first(x)
+
+;; A None arm first takes its type from the arms after it.
+fn arms(k: i32, x: i32) -> i32?
+  match k
+    5 -> None
+    4 -> x
+    _ -> 0
+
+fn big(x: i64?) -> i64 = x ?? 0
+
+;; A T?? is wanted, so each arm is Some of its value and the chain's None is
+;; the outer one.
+fn chain(a: bool, b: bool, opt: i32?) -> Option(i32?)
+  if a
+    1
+  elif b
+    opt
+
+;; Nothing wanted: a T arm beside a T? arm makes the chain a T?, flattened
+;; one level (decision 140).
+fn flat(a: bool, b: bool, opt: i32?) -> i32?
+  let r =
+    if a
+      1
+    elif b
+      opt
+  r
+
+fn main()
+  ;; assignment, and a literal at the payload's width
+  let s: i64? = None
+  s = -1
+  println(s ?? 0)
+  ;; a let with an annotation, from a literal, a name and arithmetic
+  let x: i32 = 4
+  let a: i32? = x + 1
+  let w: i64? = x
+  let f: f64? = 2
+  println(a ?? 0, w ?? 0, f ?? 0.0)
+  ;; an argument and a return value
+  println(show(7), back(true, 8) ?? -1, back(false, 8) ?? -1)
+  ;; a struct field
+  let p = P{.a 3 .b x}
+  println(p.a ?? 0, p.b ?? 0)
+  p.b = 7
+  println(p.b ?? 0)
+  ;; an array and a Vec element
+  let xs: [3 i32?] = [1, None, x]
+  println(xs[0] ?? 0, xs[1] ?? 0, xs[2] ?? 0)
+  xs[1] = 5
+  println(xs[1] ?? 0)
+  let v: Vec(i32?) = vec-new(i32?)
+  push(v, 6)
+  push(v, None)
+  println(length(v), v[0] ?? 0, v[1] ?? 0)
+  ;; the arms of an if and a match
+  println(pick(true, 2) ?? -1, pick(false, 2) ?? -1, pick2(true, 2) ?? -1, pick2(false, 2) ?? -1)
+  let m = match x
+    4 -> x
+    _ -> None
+  println(m ?? 0)
+  println(arms(5, 3) ?? -1, arms(4, 3) ?? -1, arms(1, 3) ?? -1)
+  ;; nested: a T into a T?? is Some(Some(t)), a T? is Some of it
+  let nn: Option(i32?) = 5
+  let none: i32? = None
+  let nn2: Option(i32?) = none
+  println(two(nn), two(nn2))
+  ;; kept chains over T and T? arms
+  println(two(chain(true, false, none)), two(chain(false, true, none)), two(chain(false, false, none)))
+  println(flat(true, false, none) ?? -1, flat(false, true, Some(6)) ?? -1, flat(false, true, none) ?? -1, flat(false, false, none) ?? -1)
+  let kk =
+    if x > 9
+      none
+    elif x > 1
+      1
+  println(kk ?? -1)
+  ;; generics
+  println(first(9), first(Some(8)), wrap(3) ?? 0, through(5))
+  ;; a literal local takes the payload's type from an Option use, as it
+  ;; takes T from a T use: each pair prints the same
+  let la = 4
+  let wa: i64? = la
+  let lb = 4
+  let wb: i64 = lb
+  println(la * 1000000000, lb * 1000000000, wa ?? 0, wb)
+  let lc = 4
+  println(big(lc), lc * 1000000000)
+  let lf = 7
+  let wf: f64? = lf
+  let lg = 7
+  let wg: f64 = lg
+  println(lf / 2, lg / 2, wf ?? 0.0, wg)
+  let lu = 200
+  let wu: u8? = lu
+  let lv = 200
+  let wv: u8 = lv
+  println(wu ?? 0, wv)
+  ;; and from a typed array's element, with or without an Option
+  let la2 = 3
+  let xa: [1 i64] = [la2]
+  let lb2 = 3
+  let xb: [2 i64?] = [lb2, None]
+  println(la2 * 1000000000, lb2 * 1000000000, xa[0], xb[0] ?? 0)
+  ;; None first in an if, as in a match
+  let e1 = if x > 1 then None else 5
+  let e2 = if x > 1 then 5 else None
+  println(e1 ?? -1, e2 ?? -1)
+  ;; an Option around an array of Options
+  let ao: [2 i32?]? = [1, None]
+  let ai = ao!
+  println(ai[0] ?? 0, ai[1] ?? 0)
+  ;; a narrowed name still takes a payload value
+  let o: i32? = Some(1)
+  if o?
+    o = 10
+    println(o)
diff --git a/test/programs/if-let-kept.fln b/test/programs/if-let-kept.fln
index 0fb4714c..bf27e7c1 100644
--- a/test/programs/if-let-kept.fln
+++ b/test/programs/if-let-kept.fln
@@ -21,6 +21,28 @@ fn early(a: Option(i32)) -> Option(i32)
   elif true
     3
 
+;; An arm that is already an Option is the whole, flattened (decision 140).
+fn flat(a: Option(i32), o: Option(i32)) -> Option(i32)
+  if let Some(x) = a then o
+
+;; An Option of it wanted: the arm is Some of its value, and no match is the
+;; outer None.
+fn nest(a: Option(i32), o: Option(i32)) -> Option(Option(i32))
+  if let Some(x) = a then o
+
+fn level(oo: Option(Option(i32)))
+  match oo
+    Some(o) -> if o? then println(o) else println("some none")
+    None -> println("none")
+
+fn flat_chain(a: Option(i32), k: i32)
+  let r =
+    if let Some(x) = a
+      x
+    elif k > 0
+      None
+  show(r)
+
 fn dyn_only(a: Option(i32)) -> dyn
   if let Some(x) = a then x
 
@@ -40,6 +62,15 @@ fn main()
   show(lead(1, None))
   show(early(None))
   show(early(Some(1)))
+  show(flat(Some(1), Some(4)))
+  show(flat(Some(1), None))
+  show(flat(None, Some(4)))
+  level(nest(Some(1), Some(4)))
+  level(nest(Some(1), None))
+  level(nest(None, Some(4)))
+  flat_chain(Some(3), 0)
+  flat_chain(None, 1)
+  flat_chain(None, 0)
   println(dyn_only(Some(5)))
   println(dyn_only(None))
   ;; As a statement it is unchanged.
diff --git a/test/programs/when-value.flan b/test/programs/when-value.flan
index c1c907b4..ce3ecb23 100644
--- a/test/programs/when-value.flan
+++ b/test/programs/when-value.flan
@@ -1,7 +1,8 @@
 ;;;; A when whose value is kept answers an Option: Some of its body when the
 ;;;; test holds, None when it does not. As a statement it answers nothing.
 ;;;; Where a dyn is wanted it answers the body or nil, since dyn has no
-;;;; Option. A body that is already an Option is not flattened.
+;;;; Option. A body that is already an Option is that Option, flattened one
+;;;; level (decision 140), unless an Option of it is what is wanted.
 
 (defn show [o (Option i32)] ()
   (match o (Some v) (println v) None (println "none")))
@@ -9,10 +10,13 @@
 ;; Returned: the return type is the want.
 (defn half [n i32] (Option i32) (when (= 0 (% n 2)) (/ n 2)))
 
-;; Nested, as Rust's bool::then: None from the body stays apart from a
-;; failed test.
+;; An (Option (Option i32)) is wanted, so the body is Some of it and the
+;; failed test is the outer None.
 (defn wrap [c bool o (Option i32)] (Option (Option i32)) (when c o))
 
+;; Flattened: None from the body and a failed test are one answer.
+(defn flat [c bool o (Option i32)] (Option i32) (when c o))
+
 (defn level [oo (Option (Option i32))] ()
   (match oo
     (Some o) (match o (Some v) (println v) None (println "some none"))
@@ -45,6 +49,12 @@
   (level (wrap true (Some 1)))
   (level (wrap true None))
   (level (wrap false (Some 1)))
+  (show (flat true (Some 4)))
+  (show (flat true None))
+  (show (flat false (Some 4)))
+  (let [o (the (Option i32) (Some 8))
+        f (when true o)]
+    (show f))
   (println (dyn-when true))
   (println (dyn-when nil))
   (show (early None))
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 6cb47fec..caa407e8 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -2226,8 +2226,8 @@ let () =
       dyn_if_truthy_out;
     (* A kept when is an Option; get is a checked lookup; if let. *)
     let when_value_out =
-      "5\nnone\n42\nnone\n9\n1\nsome none\nnone\n5\nnil\n3\nnone\n6\nnone\n20\nnone\n2\n\
-       a\nnil\ncond stmt\nran\nend\n"
+      "5\nnone\n42\nnone\n9\n1\nsome none\nnone\n4\nnone\nnone\n8\n5\nnil\n3\nnone\n6\nnone\n\
+       20\nnone\n2\na\nnil\ncond stmt\nran\nend\n"
     in
     outputs "when as a value" "programs/when-value.flan" when_value_out;
     outputs ~opt:"-O0" "when as a value, -O0" "programs/when-value.flan" when_value_out;
@@ -2246,7 +2246,8 @@ let () =
       "5\n100\n0\n9\n1\n20\n100\n0\n1\n7\nabsent\nnorth\n6\n-1\n-2\n14\nwhen block\n"
     in
     let if_let_kept_out =
-      "1\n4\nnone\n6\nnone\n9\n2\nnone\n3\nnone\n5\nnil\n7\n"
+      "1\n4\nnone\n6\nnone\n9\n2\nnone\n3\nnone\n4\nnone\nnone\n4\nsome none\nnone\n\
+       3\nnone\nnone\n5\nnil\n7\n"
     in
     outputs "a kept if let chain" "programs/if-let-kept.fln" if_let_kept_out;
     outputs ~opt:"-O0" "a kept if let chain, -O0" "programs/if-let-kept.fln" if_let_kept_out;
@@ -2274,6 +2275,11 @@ let () =
          outputs ~opt:"-O0" (path ^ ", -O0") ("programs/" ^ path) want;
          outputs ~x86:true (path ^ ", --x86") ("programs/" ^ path) want)
       [ ("optionals.fln", optionals_out); ("optionals-dyn.fln", optionals_dyn_out);
+        (* A T where a T? is wanted is Some of it (decision 138). *)
+        ("autowrap.fln",
+         "-1\n5 4 2\n7 8 -1\n3 4\n7\n1 0 4\n5\n2 6 0\n2 -1 -1 2\n4\n-1 3 0\n\
+          some some some none\nsome some some none none\n1 6 -1 -1\n1\n9 8 3 5\n\
+          4000000000 4000000000 4 4\n4 4000000000\n3.5 3.5 7 7\n200 200\n3000000000 3000000000 3 3\n-1 5\n1 0\n10\n");
         (* x? tests and narrows, e? as g names what it found (decision 133). *)
         ("presence.fln", "true false true\n6\n-1\n3\n101 209 0\n11\n42\n2\nabsent\n6\nfalse true\n3\n6\n15\n"); ("presence-dyn.fln", "true false\n103 209 0\nno pet\nann\n3 2\n") ];
     (* The pipe (decision 137): chains, multi-line, qualified, dyn, and the
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 9154491e..8aa8f4e5 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -8482,6 +8482,26 @@ let () =
   parse_rejects "_ in a defgeneric's return slot"
     ~needle:"defgeneric's methods each have their own"
     "(defgeneric area [s] _)";
+  (* Decision 138: a T is wrapped where a T? is wanted, and never the other
+     way. The program half is programs/autowrap.fln. *)
+  accepts "a T is Some of it at a T?" "(defn f [] (Option i64) -1)\n(defn main [] ())";
+  rejects_check "a T? is not unwrapped at a T" ~needle:"expected i32, found (Option i32)"
+    "(defn f [o (Option i32)] i32 o)\n(defn main [] ())";
+  rejects_check "a T? argument is not unwrapped" ~needle:"expected i32, found (Option i32)"
+    "(defn g [x i32] i32 x)\n(defn f [o (Option i32)] i32 (g o))\n(defn main [] ())";
+  rejects_check "a payload that does not fit is refused at the Option"
+    ~needle:"expected (Option i32), found str"
+    "(defn f [] (Option i32) \"no\")\n(defn main [] ())";
+  rejects_check "a literal that does not fit is refused at the Option"
+    ~needle:"expected (Option str), found the integer literal 5"
+    "(defn f [] (Option str) 5)\n(defn main [] ())";
+  rejects_check "a narrowing is not wrapped" ~needle:"expected (Option i32), found i64"
+    "(defn f [x i64] (Option i32) x)\n(defn main [] ())";
+  rejects_check "no wrap inside a container" ~needle:"expected (Vec (Option i32)), found (Vec i32)"
+    "(defn f [v (Vec i32)] (Vec (Option i32)) v)\n(defn main [] ())";
+  rejects_check "a narrowed name still refuses an Option"
+    ~needle:"it cannot be given an Option here"
+    "(defn main [] () (let [o (the (Option i32) (Some 1))] (when (? o) (set o (Some 2)))))";
   (* A plain name binds what an Option or a dyn holds; over anything else
      it cannot fail, and is refused toward let. The program half is
      programs/if-let.flan and programs/optionals.fln. *)
diff --git a/test/test_syntax.ml b/test/test_syntax.ml
index 4b69b8c3..af8de176 100644
--- a/test/test_syntax.ml
+++ b/test/test_syntax.ml
@@ -1528,7 +1528,7 @@ let () =
   refused "addr-taken.fln"
     "fn clear(p: Ptr(i32?))\n  deref(p) = None\n\nfn main()\n  let x: i32? = Some(1)\n\
      \  let p = addr(x)\n  if x?\n    clear(p)\n    println(x + 1)\n"
-    [ "expected Option(i32)" ];
+    [ "+ takes numbers, found Option(i32)" ];
   refused "capital-local.fln" "fn main()\n  let X: i32? = Some(1)\n  println(X?)\n"
     [ "To test the local X, give it a lowercase name, as in x?" ];
   checks "addr-taken-test.fln"