A bool arm and a dyn arm of an if meet at dyn with the bool boxed, so (or false (box "s")) answers "s"

TODO.org

@@ -848,13 +848,6 @@ CLOSED: [2026-09-20]
 typed conditions stay strict =bool=. =and= and =or= hand back the operand that
 decided them, Clojure's rule, through a desugaring that evaluates each test once.
 
-** NEXT A bool arm and a dyn arm joining as dyn
-Decided 2026-09-25: they join as =dyn=, the =bool= boxed — Clojure's rule, so =(or false (box "s"))= answers ="s"=.
-With both arms of a desugared =and=/=or= holding real values, a non-bool =dyn= on
-the losing side meets the strict =bool= boundary and traps —
-=(or false (box "s"))= is the case. Whether a =bool= arm and a =dyn= arm should
-join as =dyn= is the author's call and is not settled.
-
 ** NEXT A truthiness failure re-runs the whole failing subtree
 Decided 2026-09-25: fix it without changing any message — the retry reuses what the first pass settled for each subtree (memoised by node), so nested =not= is linear. Test with a deep nest that must fail fast and with the existing message tests unchanged.
 The retry exists to keep a refused literal's message unchanged and re-runs the

lib/check.ml

@@ -5998,6 +5998,34 @@ and check_if ctx ?(tail = false) ?want loc c t e =
       want = None
       && (match t.Tast.ty with Types.Slice _ | Types.Ptr _ -> true | _ -> false)
     in
+    (* A bool arm and a dyn arm meet at dyn, the bool boxed — Clojure's rule,
+       so (or false (box "s")) answers "s" rather than unboxing the string at
+       bool and trapping. The other order already met at dyn, the then arm
+       deciding. So after a bool then arm the else arm is checked on its own
+       terms first, since checking it at bool is what unboxes it, and kept
+       when it is a bool or a dyn. Anything else is abandoned and checked at
+       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. *)
+    let own_else =
+      if want = None && t.Tast.ty = Types.Bool then
+        match
+          trial ctx (fun () ->
+              let v = branch ctx (fun () -> in_tail (fun () -> check ctx e)) in
+              match v.Tast.ty with
+              | Types.Bool | Types.Dyn | Types.Never -> v
+              | _ -> raise (Loc.Error (Loc.diag v.Tast.loc "not bool or dyn")))
+        with
+        | Ok v -> Some v
+        | Error _ -> None
+      else None
+    in
+    let t =
+      match own_else with
+      | Some v when v.Tast.ty = Types.Dyn ->
+        expect ctx t.Tast.loc ~want:(Some Types.Dyn) t
+      | _ -> t
+    in
     let ewant =
       match want with
       | Some _ -> want
@@ -6019,6 +6047,9 @@ and check_if ctx ?(tail = false) ?want loc c t e =
        location; and with an expectation in hand both arms are checked against
        it rather than against each other, so nothing here runs. *)
     let e =
+      match own_else with
+      | Some v -> v
+      | None ->
       match branch ctx (fun () -> in_tail (fun () -> check ctx ?want:ewant e)) with
       | v -> v
       | exception Loc.Error d

lib/parse.ml

@@ -1182,17 +1182,10 @@ and cond f (args : Form.t list) : Ast.expr =
    [f.loc] would blame the enclosing (and ...) for whichever operand is
    actually wrong.
 
-   What answering the operand costs, for both forms alike: the two arms are
-   now both real values, so mixing a dyn operand with a typed bool one makes
-   check_if unify them, and the then arm decides. A non-bool dyn value on
-   the losing side then meets the strict bool boundary at run time —
-   (or false (box "s")) and (and (box nil) some-bool) both trap, verified on
-   this tree. Each form used to be safe in exactly one of those directions,
-   because the sentinel it answered was a bool literal that boxed to fit
-   whatever the real branch was; neither is now, and they are at least
-   symmetric about it. Making bool and dyn arms join as dyn is a check_if
-   question, noted in TODO.org, "A bool arm and a dyn arm joining as dyn",
-   and not decided here.
+   The two arms are both real values, so mixing a dyn operand with a typed
+   bool one makes check_if unify them: a bool arm and a dyn arm meet at dyn
+   with the bool boxed, whichever side each is on, so (or false (box "s"))
+   answers "s" and (and (box nil) some-bool) answers nil.
 
    One known wart, measured rather than guessed, and left alone deliberately.
    In a want-free position — [(println (and true true (vec-new i32)))] — the

test/programs/dyn-if-truthy.flan

@@ -92,6 +92,13 @@
   ;; used to trap trying to unbox "x" as a strict bool.
   (println (or (box nil) (box "x")))
   (println (or (box 5) (box "unreached")))
+  ;; A typed bool operand beside a dyn one: the two meet at dyn, the bool
+  ;; boxed, so the dyn one comes back whichever side of the if it lands on.
+  (println (or false (box "s")))
+  (println (or (= 1 2) (box nil)))
+  (println (and (box nil) (= 1 1)))
+  (println (and true (box "y")))
+  (println (or true (box "unreached")))
 
   ;; One operand is that operand, whatever it is -- no test, no sentinel.
   (println (and (box nil)))

test/test_acceptance.ml

@@ -1928,7 +1928,7 @@ let () =
     let dyn_if_truthy_out =
       "falsey\nfalsey\ntruthy\ntruthy\ntruthy\ntruthy\ntruthy\ntruthy\ntruthy\n\
        truthy\ntruthy\ntruthy\nwhen 0 ran\nwhen empty-string ran\nb\nb\n\
-       :kw\nfalse\nnil\n\n0\nfalse\nx\n5\n\
+       :kw\nfalse\nnil\n\n0\nfalse\nx\n5\ns\nnil\nnil\ny\ntrue\n\
        nil\n\nnil\n0\ntrue\nfalse\n\
        nil\nand-reached\n2\n7\nor-reached\n1\n\
        and-decider\nnil\nor-decider\n9\n\