diff --git a/TODO.org b/TODO.org index 5d6cf540..b0d30b34 100644 --- a/TODO.org +++ b/TODO.org @@ -848,14 +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 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 -subtree rather than the leaf, which is exponential in nested =not= depth on a -program that does not type-check. Moot for anything that compiles; only the -daemon's half-typed recompiles could feel it. A cheaper retry was tried and -shelved because it changes which literal gets the nicer message. - ** DONE and's last operand gets a misdirected caret CLOSED: [2026-09-25] Already fixed by 3672da2, which blames the arm that is not a compiler temp; the diff --git a/lib/check.ml b/lib/check.ml index 331e5ca4..252cafba 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -4091,6 +4091,14 @@ let tracked_call loc env name (tr : Shim.track) ret (args : Tast.expr list) = (* Every expression goes through here, and [check_value] is the one that knows the forms. What this adds is [refuse_owned_copy], asked of whatever came back unless the form was checked as the target of a place. *) + +(* The conditions [check_truthy] has refused, each with the body it was + checked in and its diagnostic, for as long as the outermost call is on the + stack — see [check_truthy]. Physical identity on both, since a generic's + body is the same syntax checked again at another type. *) +let truthy_failed : (Ast.expr * ctx * Loc.diag) list ref = ref [] +let truthy_depth = ref 0 + let rec check ctx ?want (e : Ast.expr) : Tast.expr = let place = ctx.place_ok in ctx.place_ok <- false; @@ -5887,12 +5895,12 @@ and check_recur ctx ~tail loc args = literals gets the nicer message, not just the speed. The cost that buys is real: nested [not] on a program that does not type-check re-runs this whole function once per level of nesting inside the level above it, - which is exponential in how deep the nesting goes — moot for a program - that compiles, since neither retry ever fires, and moot for ordinary - nesting depths, but visible within a second or so around twenty levels - of a [not] wrapped in a [not] wrapped in .... The dev daemon is the one - caller that could feel this, recompiling a half-typed form on every - edit; nobody has hit it in practice and it is not fixed here. + which would be exponential in how deep the nesting goes. What keeps it + linear is [truthy_failed]: a condition this function has already refused, + in the same body, is refused again with the same diagnostic rather than + re-checked, so a retry re-walks its subtree once and stops at the first + condition below it that was settled. The message is the one the first + pass produced, so no message changes. Keywords are a separate, deliberate loss rather than a bug: a bare [:kw] used to be checked here with [want:Types.Bool] from the start, so @@ -5907,6 +5915,23 @@ and check_recur ctx ~tail loc args = test_flan.ml pins the new answer down so it is not lost again by accident. *) and check_truthy ctx c = + match + List.find_opt (fun (n, cx, _) -> n == c && cx == ctx) !truthy_failed + with + | Some (_, _, d) -> raise (Loc.Error d) + | None -> + incr truthy_depth; + Fun.protect + ~finally:(fun () -> + decr truthy_depth; + if !truthy_depth = 0 then truthy_failed := []) + (fun () -> + try check_truthy_once ctx c + with Loc.Error d as ex -> + truthy_failed := (c, ctx, d) :: !truthy_failed; + raise ex) + +and check_truthy_once ctx c = let loc = c.Ast.loc in match check ctx c with | c0 when c0.Tast.ty = Types.Dyn -> diff --git a/test/test_flan.ml b/test/test_flan.ml index 24cfbe01..131f7ab5 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -5682,6 +5682,23 @@ let () = rejects_check "and offers no comparison at all for a type that has none" "(defstruct P [x i32]) (defn f [] i32 (let [p (P {.x 1})] (if p 1 0)))" ~needle:"a condition is a bool or a dyn, and this is P"; + (* A deep nest of not over a condition that is refused. Each level retries + the level below it for its message, and a refusal already settled is + answered from memory, so two hundred levels fail at once — re-walking + each subtree doubled the work per level. The message is the innermost + condition's, as it is at one level. *) + (let deep = + let rec nest k e = if k = 0 then e else nest (k - 1) ("(not " ^ e ^ ")") in + "(defn g [x i32] bool " ^ nest 200 "x" ^ ")" + in + match Watchdog.within 5 (fun () -> checked deep) with + | _ -> check "a deep not nest over an i32 is refused" false + | exception Watchdog.Timeout -> + check "a deep not nest over an i32 fails fast" false + | exception Loc.Error { Loc.dmsg; _ } -> + check "a deep not nest keeps the one-level message" + (dmsg = "a condition is a bool or a dyn, and this is i32 — test it, as \ + (!= x 0)")); (* A literal still names itself: that message knows something the rule does not, so the re-check's answer is kept wherever it is more specific. *) rejects_check "a literal condition keeps its own message"