diff --git a/TODO.org b/TODO.org
index 32899497..1a23c947 100644
--- a/TODO.org
+++ b/TODO.org
@@ -64,8 +64,9 @@ use-directed inference.
 
 ** DONE An if's or match's arms meet at one join, whichever is written first
 CLOSED: [2026-09-25]
-Lossless widening, const, and dyn beside anything, the same for =_= exits.
-Rules out the first arm deciding the type the others are checked at.
+Each arm is asked the other's type first; only a refusal meets at the join
+(lossless widening, const, dyn beside a dyn value), the same for =_= exits.
+Rules out the first arm's type refusing a wider second arm.
 
 ** DONE def, defonce and defconst are the three forms
 CLOSED: [2026-09-20]
diff --git a/lib/check.ml b/lib/check.ml
index 47b9586c..fcae594f 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -3000,6 +3000,23 @@ 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
 
+(* 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,
+   and never decides a join. *)
+let rec adapts (e : Ast.expr) =
+  lone_literal e
+  || (match e.Ast.e with
+      | Ast.Var "nil" -> true
+      | Ast.Call ({ Ast.e = Ast.Var "Some"; _ }, [ x ]) -> adapts x
+      | Ast.Call ({ Ast.e = Ast.Var ("+" | "-" | "*" | "/" | "%"); _ },
+                  (_ :: _ as xs)) ->
+        List.for_all adapts xs
+      | Ast.Do (_ :: _ as xs) | Ast.Let (_, (_ :: _ as xs)) ->
+        adapts (List.hd (List.rev xs))
+      | Ast.If (_, a, Some b) -> adapts a && adapts b
+      | _ -> false)
+
 
 (* The environment for a lifted body, built once its own body has been checked
    and [caught] is therefore final. spec-memory.md's case 2, and the whole of
@@ -5324,6 +5341,28 @@ let if_failed :
   Hashtbl.create 16
 let if_depth = ref 0
 
+(* An arm refused at the other arm's type, keyed the same way: the arm is
+   then checked on its own terms, and an [if] above it that checks it again
+   — its own trial, then for real — finds the refusal here rather than
+   walking the arm to it once more, which in a chain nested in else arms
+   would be twice per level. Cleared for each program. *)
+let arm_failed :
+  (Loc.t,
+   Ast.expr * ((string * binding) list * Types.t) * Types.t * Loc.diag)
+    Hashtbl.t =
+  Hashtbl.create 16
+
+(* A dyn value opened at a typed want: the box, and the want it was opened
+   at. Two arms that meet this way meet at dyn — the typed one is boxed, not
+   the dyn one opened — whichever is written first. *)
+let not_kept = "check/arm-not-kept"
+
+let opened_dyn (v : Tast.expr) =
+  match v.Tast.e with
+  | Tast.Prim (Tast.Rt ("flan_dyn_need_i64" | "flan_dyn_need_f64"), [ inner ])
+    when Types.equal inner.Tast.ty Types.Dyn -> Some inner
+  | _ -> None
+
 
 (* A Vec or a Map parameter is a copy of the caller's header — Odin's rule —
    so growing it reallocates a block only this function's copy points at, and
@@ -5724,7 +5763,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
       (match ctx.in_frames with Some n -> n | None -> assert false)
 
   | Ast.Return v when ctx.ret == infer_ret ->
-    let lit = match v with Some x -> lone_literal x | None -> false in
+    let lit = match v with Some x -> adapts x | None -> false in
     let v = Option.map (check ctx) v in
     infer_seen :=
       (match v with
@@ -7431,7 +7470,7 @@ and check_if_once ctx ~tail ?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 && lone_literal t && not (lone_literal e)
+  | Some e when want = None && adapts t && not (adapts 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]
@@ -7461,43 +7500,75 @@ and check_if_once ctx ~tail ?want loc c t e =
        bool as before, for that path's messages. A chain whose arms all fit
        is checked once; a refused one re-checks each level below the refusal
        once more, the square of its depth. *)
-    (* The else arm on its own terms, when nothing is wanted: the two arms
-       meet at [arm_join], so the order they are written in decides nothing,
-       and both are brought to the join as checked — the arm is never checked
-       twice, which in a chain of ifs would be twice per level. *)
+    (* The else arm at the then arm's type first, as it always was: a value
+       that takes its type from what is asked of it — [(+ b 1)] beside an
+       i64, [nil] beside an Option — is asked the then arm's. Only when that
+       is refused as a mismatch is it checked on its own terms, and the two
+       meet at [arm_join], so [(if c x32 y64)] is the i64 [(if c y64 x32)]
+       is. A dyn opened at the then arm's type is not a meeting: the two
+       meet at dyn, as they do the other way round. The arm is checked once
+       each way at most, and a refusal at the then arm's type is kept
+       ([arm_failed]) for the ifs above that check it again. *)
     let joined =
       if want <> None || free_join || t.Tast.ty = Types.Never
          || t.Tast.ty = Types.Bool || and_sentinel e || lone_literal e
       then None
       else
         let alone () = branch ctx (fun () -> in_tail (fun () -> check ctx e)) in
-        match trial ctx alone with
+        let key = (ctx.scope, ctx.ret) in
+        let at_then () =
+          match
+            List.find_opt
+              (fun (n, (sc, r), w, _) ->
+                 n == e && r == ctx.ret && Types.equal w t.Tast.ty
+                 && same_scope sc ctx.scope)
+              (Hashtbl.find_all arm_failed e.Ast.loc)
+          with
+          | Some (_, _, _, d) -> Error d
+          | None ->
+            match
+              trial ctx (fun () ->
+                  branch ctx (fun () ->
+                      in_tail (fun () -> check ctx ~want:t.Tast.ty e)))
+            with
+            | Ok v -> Ok v
+            | Error d ->
+              Hashtbl.add arm_failed e.Ast.loc (e, key, t.Tast.ty, d);
+              Error d
+        in
+        let meet v =
+          match arm_join t.Tast.ty v.Tast.ty with
+          | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v)
+          | None -> None
+        in
+        match at_then () with
         | Ok v ->
-          (match arm_join t.Tast.ty v.Tast.ty with
-           | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v)
-           (* No join: the refusal [if] gives its else arm. *)
-           | None ->
-             Some (t.Tast.ty, expect ctx v.Tast.loc ~want:(Some t.Tast.ty) v))
-        | Error own ->
-          (* Refused on its own terms. The then arm's type may be what it
-             needed — [nil], a bare struct — and it is checked at it below,
-             whose refusal is then the one said. Only when that refusal is a
-             mismatch and the arm's own is not — an unknown name, say — is
-             the arm's own error the real one, so nothing is invented about a
-             type it was never going to have. *)
+          (match opened_dyn v with
+           | Some box -> Some (Types.Dyn, box)
+           | None -> Some (t.Tast.ty, v))
+        | Error _ when adapts e -> None
+        | Error d ->
+          (* A mismatch, or a dyn the then arm's type could not open: the
+             arm on its own terms meets the then arm. Anything else refused
+             it at the then arm's type, and that refusal is said. *)
           (match
              trial ctx (fun () ->
-                 branch ctx (fun () ->
-                     in_tail (fun () -> check ctx ~want:t.Tast.ty e)))
+                 let v = alone () in
+                 if is_mismatch d || Types.equal v.Tast.ty Types.Dyn then v
+                 else raise (Loc.Error (Loc.diag ~kind:not_kept v.Tast.loc "")))
            with
-           | Error d
-             when is_mismatch d && not (is_mismatch own) ->
+           | Ok v -> meet v
+           | Error own when String.equal own.Loc.kind not_kept -> None
+           (* Refused on its own terms too, and not as a mismatch — an
+              unknown name, say: that is the real error, and nothing is said
+              about a type the arm was never going to have. *)
+           | Error own when is_mismatch d && not (is_mismatch own) ->
              let v = alone () in
-             (match arm_join t.Tast.ty v.Tast.ty with
-              | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v)
+             (match meet v with
+              | Some r -> Some r
               | None ->
                 Some (t.Tast.ty, expect ctx v.Tast.loc ~want:(Some t.Tast.ty) v))
-           | _ -> None)
+           | Error _ -> None)
     in
     match joined with
     | Some (j, v) ->
@@ -8928,7 +8999,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
      the others, as an [if]'s literal arm does. The order is only the order
      they are checked in; they are put back in source order below. *)
   let literal_arm ((a : Ast.arm), _, _) =
-    match List.rev a.Ast.body with last :: _ -> lone_literal last | [] -> false
+    match List.rev a.Ast.body with last :: _ -> adapts last | [] -> false
   in
   (* Every arm a literal: they meet at the wider of their own types, as an
      [if]'s two do. *)
@@ -9002,19 +9073,47 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
            let arm = (a, ctor, binds) in
            let body =
              if free && !want <> None && not (literal_arm arm) then
+               (* As an [if]'s else arm: at the join so far first, on its
+                  own terms only when that is refused as a mismatch. *)
                let at w () = block ctx ?want:w a.Ast.aloc a.Ast.body in
-               match trial ctx (at None) with
-               | Ok b -> b
-               | Error own ->
-                 (* Refused on its own terms: the join may be what it
-                    needed, and its refusal at the join is then the one
-                    said — unless that refusal is a mismatch and the arm's
-                    own is not, when the arm's own error is the real one. *)
-                 (match trial ctx (at !want) with
-                  | Error d
-                    when is_mismatch d && not (is_mismatch own) ->
+               let w = Option.get !want in
+               let head = List.hd a.Ast.body in
+               let at_join () =
+                 match
+                   List.find_opt
+                     (fun (n, (sc, r), w', _) ->
+                        n == head && r == ctx.ret && Types.equal w' w
+                        && same_scope sc ctx.scope)
+                     (Hashtbl.find_all arm_failed head.Ast.loc)
+                 with
+                 | Some (_, _, _, d) -> Error d
+                 | None ->
+                   (match trial ctx (at (Some w)) with
+                    | Ok b -> Ok b
+                    | Error d ->
+                      Hashtbl.add arm_failed head.Ast.loc
+                        (head, (ctx.scope, ctx.ret), w, d);
+                      Error d)
+               in
+               match at_join () with
+               | Ok b ->
+                 (match opened_dyn b with
+                  | Some box -> want := Some Types.Dyn; box
+                  | None -> b)
+               | Error d ->
+                 (match
+                    trial ctx (fun () ->
+                        let b = at None () in
+                        if is_mismatch d || Types.equal b.Tast.ty Types.Dyn then b
+                        else
+                          raise (Loc.Error (Loc.diag ~kind:not_kept b.Tast.loc "")))
+                  with
+                  | Ok b -> b
+                  | Error own when String.equal own.Loc.kind not_kept ->
+                    at !want ()
+                  | Error own when is_mismatch d && not (is_mismatch own) ->
                     at None ()
-                  | _ -> at !want ())
+                  | Error _ -> at !want ())
              else block ctx ?want:!want a.Ast.aloc a.Ast.body
            in
            (if body.Tast.ty <> Types.Never then
@@ -13928,6 +14027,21 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
        type, so [(+ x 1)] over a dyn x goes on building an i64 one. *)
     else if dyn_ok && not (needs_want y) then begin
       let a = check ctx ?want x in
+      (* y at [a]'s type first, and on its own terms only if that is
+         refused: checking it both ways every time made a chain of these
+         nested in their second operands twice as slow per level. A dyn
+         opened at [a]'s type is seen for what it was. *)
+      let at_a =
+        if a.Tast.ty = Types.Dyn then None
+        else
+          match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
+          | Ok b' -> Some (Ok b')
+          | Error d -> Some (Error d)
+      in
+      match at_a with
+      | Some (Ok b') ->
+        (match opened_dyn b' with Some box -> a, box | None -> a, b')
+      | _ ->
       let b = check ctx y in
       (* Nothing dyn about this pair after all, so it is put back the way the
          typed path built it. Re-checking only when the types actually differ
@@ -13949,7 +14063,11 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
          that has to move. Nothing is checked a third time — the own-terms [b]
          already in hand is the answer. *)
       else
-        (match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
+        (match
+           match at_a with
+           | Some (Error d) -> Error d
+           | _ -> trial ctx (fun () -> check ctx ~want:a.Tast.ty y)
+         with
          | Ok b' -> a, b'
          | Error d ->
            (match
@@ -15524,7 +15642,7 @@ and read_return env (fn : Ast.fn) params =
   let last =
     match List.rev tf.Tast.body, List.rev fn.Ast.fbody with
     | (x : Tast.expr) :: _, (a : Ast.expr) :: _ ->
-      [ (x.Tast.ty, x.Tast.loc, lone_literal a) ]
+      [ (x.Tast.ty, x.Tast.loc, adapts a) ]
     | (x : Tast.expr) :: _, [] -> [ (x.Tast.ty, x.Tast.loc, false) ]
     | [], _ -> []
   in
@@ -16837,6 +16955,7 @@ let shadow_prelude (prelude : Ast.decl list) (decls : Ast.decl list) =
 let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) :
   Tast.program * env * string list =
   let env = new_env () in
+  Hashtbl.reset arm_failed;
   (* ── A declaration left as it was compiled ───────────────────────────
      A dev session installs a function whose signature changed, and a
      caller compiled against the old one is still in the running program and
diff --git a/spec-syntax.md b/spec-syntax.md
index ffd35efc..53f4fe3d 100644
--- a/spec-syntax.md
+++ b/spec-syntax.md
@@ -55,10 +55,11 @@ warns about; the new syntax must not inherit it.
 **The return type is inferred when omitted.** Body-local only, as
 `docs/SPIKE-INFERENCE.md` ("The cheap first step" and "Verdict") scopes it:
 - the return type is the body's type; a `dyn` body gives `dyn`; the exits (the
-  last form and each `return`) meet exactly as an `if`'s or `match`'s arms do, through one
-  join and in any order: lossless widening, the read-only side of a const
-  difference, `dyn` beside anything; a literal takes the other exits' type
-  and what `if` refuses is refused; no value gives `()`.
+  last form and each `return`) meet exactly as an `if`'s or `match`'s arms do,
+  in any order: each is asked the others' type first, so a literal, `nil` or
+  arithmetic takes it; only arms that are refused that way meet at the join
+  (lossless widening, the read-only side of a const difference, `dyn` beside
+  a genuinely dyn value); what `if` refuses is refused; no value gives `()`.
 - it reads only the function's own body, never a call site.
 - a self-recursive or mutually recursive function must write its return type.
   Refuse by name, naming the whole cycle. The corpus has 17 self-recursive
diff --git a/test/programs/arm-want.flan b/test/programs/arm-want.flan
new file mode 100644
index 00000000..58cf9dce
--- /dev/null
+++ b/test/programs/arm-want.flan
@@ -0,0 +1,25 @@
+;;;; An arm is checked at the other arm's type first: arithmetic in a
+;;;; narrower arm is done at the wider type, not done narrow and widened, and
+;;;; nil beside an Option is None, whichever arm comes first.
+
+(defn wd [c bool a i64 b i32] i64 (let [v (if c a (+ b 1))] v))
+(defn wd2 [c bool a i64 b i32] i64 (if c a (+ b 1)))
+(defn wd4 [c bool a i64 b i32] i64 (let [v (if c a (* b b))] v))
+(defn wd5 [o (Option i32) a i64 b i32] i64 (let [v (match o (Some q) a None (+ b 1))] v))
+(defn wd6 [c bool a f64 b i32] f64 (let [v (if c a (/ b 2))] v))
+(defn wd7 [c bool a i64 b i32] _ (when c (return a)) (+ b 1))
+
+(defn n1 [c bool p (Option i64)] i64 (let [v (if c nil p)] (match v (Some q) q None -1)))
+(defn n2 [o (Option i32) p (Option i64)] i64
+  (let [v (match o None nil (Some z) p)] (match v (Some q) q None -1)))
+
+(defn main [] i32
+  (println (wd false 0 2147483647))
+  (println (wd2 false 0 2147483647))
+  (println (wd4 false 0 100000))
+  (println (wd5 None 0 2147483647))
+  (println (wd6 false 0.0 3))
+  (println (wd7 false 0 2147483647))
+  (println (n1 false (Some 5)) (n1 true (Some 5)))
+  (println (n2 (Some 1) (Some 5)) (n2 None (Some 5)))
+  0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 72cb2fe5..cb0e7202 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -590,6 +590,14 @@ let () =
       "programs/return-defer.flan" rd_out;
     outputs ~x86:true "a return computes its value before its defers, x86"
       "programs/return-defer.flan" rd_out;
+    (* An arm is checked at the other arm's type first. *)
+    let aw_out =
+      "2147483648\n2147483648\n10000000000\n2147483648\n1.5\n2147483648\n\
+       5 -1\n5 -1\n"
+    in
+    outputs "an arm takes the other arm's type" "programs/arm-want.flan" aw_out;
+    outputs ~x86:true "an arm takes the other arm's type, x86"
+      "programs/arm-want.flan" aw_out;
     (* A generic copy made during an abandoned trial keeps what it lifted. *)
     outputs "a trial's generic copy keeps its lambda and its message printer"
       "programs/trial-generic.flan" "42\n21\n";
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 02fe3813..da911778 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -7984,7 +7984,8 @@ let () =
      check "a match arm of another type is refused at its value"
        (dloc.Loc.col = 87 && contains dmsg "expected i8, found string"));
   (* Nested arms that meet at a wider type are checked once each, not once
-     per level above them. *)
+     per level above them — when the else arm fits the then arm's type, and
+     when it is wider, so that every level's first attempt is refused. *)
   (let nest kind depth =
      let rec go k e =
        if k = 0 then e
@@ -7993,7 +7994,10 @@ let () =
            (match kind with
             | `If -> Printf.sprintf "(if c a (+ (idg b) (i32 %s)))" e
             | `Match ->
-              Printf.sprintf "(match o (Some q) a None (+ (idg b) (i32 %s)))" e)
+              Printf.sprintf "(match o (Some q) a None (+ (idg b) (i32 %s)))" e
+            | `If_wider -> Printf.sprintf "(if c b (+ a (i64 %s)))" e
+            | `Match_wider ->
+              Printf.sprintf "(match o (Some q) b None (+ a (i64 %s)))" e)
      in
      go depth "(i32 b)"
    in
@@ -8021,7 +8025,45 @@ let () =
         | exception Loc.Error { Loc.dmsg; _ } ->
           check (what ^ " twenty deep checks: " ^ dmsg) false)
      [ (`If, "[c bool a i64 b i32]", "an if");
-       (`Match, "[o (Option i32) a i64 b i32]", "a match") ]);
+       (`Match, "[o (Option i32) a i64 b i32]", "a match");
+       (`If_wider, "[c bool a i64 b i32]", "an if whose else arm is wider");
+       (`Match_wider, "[o (Option i32) a i64 b i32]",
+        "a match whose last arm is wider") ]);
+  (* An arm is asked the other arm's type first, so a value that takes its
+     type from what is asked — nil, (Some 3), arithmetic — gets it, and the
+     two meet the same way whichever is written first. *)
+  (let reads_as_top what src name want =
+     let got =
+       match checked src with
+       | p ->
+         (match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = name) p.Tast.fns with
+          | Some f -> Dev.signature_of_fn f
+          | None -> "missing")
+       | exception Loc.Error { Loc.dmsg = m; _ } -> "refused: " ^ m
+     in
+     if got <> want then begin
+       incr failures;
+       Printf.printf "FAIL  %s\n        got: %s\n     wanted: %s\n" what got want
+     end
+   in
+  List.iter
+    (fun (what, sg, body, want) ->
+       reads_as_top what ("(defn f " ^ sg ^ " _ " ^ body ^ ")\n(defn main [] ())") "f" want)
+    [ ("nil beside an Option", "[c bool p (Option i64)]", "(if c p nil)",
+       "f [bool (Option i64)] (Option i64)");
+      ("nil first beside an Option", "[c bool p (Option i64)]", "(if c nil p)",
+       "f [bool (Option i64)] (Option i64)");
+      ("(Some 3) beside an Option", "[c bool p (Option i64)]", "(if c p (Some 3))",
+       "f [bool (Option i64)] (Option i64)");
+      ("float arithmetic beside an f32", "[c bool p f32]", "(if c p (* 2.0 3.0))",
+       "f [bool f32] f32");
+      ("a do ending in a literal beside a u8", "[c bool p u8]",
+       "(if c p (do (println 1) 7))", "f [bool u8] u8");
+      ("a match's nil arm first", "[o (Option i32) p (Option i64)]",
+       "(match o None nil (Some z) p)", "f [(Option i32) (Option i64)] (Option i64)") ]);
+  rejects_check "nil beside a string, as before"
+    ~needle:"string"
+    "(defn f [c bool s string] string (let [v (if c s nil)] v))\n(defn main [] ())";
   rejects_check "an else arm's own error is the one reported"
     ~needle:"unknown function nope2"
     "(defn g [c bool a i32 b i64] i64 (let [v (if c a (+ b (nope2 1)))] v))\n\