An arm is checked at the other arm's type first and meets it at the join only when refused there, so every program master accepts keeps its type and value while arms still meet in either order

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]

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
-        | 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. *)
+        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 ->
-             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
+            match
               trial ctx (fun () ->
                   branch ctx (fun () ->
                       in_tail (fun () -> check ctx ~want:t.Tast.ty e)))
             with
-           | Error d
-             when is_mismatch d && not (is_mismatch own) ->
-             let v = alone () in
-             (match arm_join t.Tast.ty v.Tast.ty 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 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 () ->
+                 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
+           | 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 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
+               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 ->
-                 (* 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) ->
+                  | 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

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

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)

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";

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\