From 23af8a4dd3b5c6067a1b8d53359939dc653a1aef Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 15:31:12 +0700 Subject: [PATCH] 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 | 7 ------- lib/check.ml | 31 +++++++++++++++++++++++++++++++ lib/parse.ml | 15 ++++----------- test/programs/dyn-if-truthy.flan | 7 +++++++ test/test_acceptance.ml | 2 +- 5 files changed, 43 insertions(+), 19 deletions(-) diff --git a/TODO.org b/TODO.org index 1584ed26..5d6cf540 100644 --- a/TODO.org +++ b/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 diff --git a/lib/check.ml b/lib/check.ml index 27cd37a2..331e5ca4 100644 --- a/lib/check.ml +++ b/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 diff --git a/lib/parse.ml b/lib/parse.ml index 88b824a5..64d6854f 100644 --- a/lib/parse.ml +++ b/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 diff --git a/test/programs/dyn-if-truthy.flan b/test/programs/dyn-if-truthy.flan index 609447c2..928162fd 100644 --- a/test/programs/dyn-if-truthy.flan +++ b/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))) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 35c127fd..23d96f21 100644 --- a/test/test_acceptance.ml +++ b/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\