A condition check_truthy has already refused is refused again from memory, so a retry through nested not is linear and keeps its message

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

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

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"