A refused if is answered from memory for the same condition, scope and expectation, so a refused or/and chain is checked in linear time

lib/check.ml

@@ -4147,9 +4147,31 @@ let tracked_call loc env name (tr : Shim.track) ret (args : Tast.expr list) =
    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_failed :
+  (Ast.expr * (string * binding) list * Types.t * Loc.diag) list ref = ref []
+
+(* Whether two scopes bind the same names at the same types, which is what a
+   refusal under them can depend on — the slots are fresh on every pass. A
+   memo keyed on less would replay a refusal after a retry changed a type. *)
+let same_scope (a : (string * binding) list) (b : (string * binding) list) =
+  a == b
+  || List.equal
+       (fun (n, (x : binding)) (m, (y : binding)) ->
+          String.equal n m && Types.equal x.bty y.bty)
+       a b
 let truthy_depth = ref 0
 
+(* The same for an [if], keyed on its condition and the expectation:
+   an [if] whose else arm is tried on its own terms first (see [check_if])
+   would otherwise be re-checked, refused, by the trial of every [if] above
+   it — the square of a refused or/and chain's length. *)
+let if_failed :
+  (Loc.t,
+   Ast.expr * ((string * binding) list * Types.t) * Types.t option * Loc.diag)
+    Hashtbl.t =
+  Hashtbl.create 16
+let if_depth = ref 0
+
 
 (* 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
@@ -6000,10 +6022,13 @@ and check_recur ctx ~tail loc args =
    accident. *)
 and check_truthy ctx c =
   match
-    List.find_opt (fun (n, cx, _) -> n == c && cx == ctx) !truthy_failed
+    List.find_opt
+      (fun (n, sc, r, _) -> n == c && r == ctx.ret && same_scope sc ctx.scope)
+      !truthy_failed
   with
-  | Some (_, _, d) -> raise (Loc.Error d)
+  | Some (_, _, _, d) -> raise (Loc.Error d)
   | None ->
+    let scope = ctx.scope in
     incr truthy_depth;
     Fun.protect
       ~finally:(fun () ->
@@ -6012,7 +6037,7 @@ and check_truthy ctx c =
       (fun () ->
          try check_truthy_once ctx c
          with Loc.Error d as ex ->
-           truthy_failed := (c, ctx, d) :: !truthy_failed;
+           truthy_failed := (c, scope, ctx.ret, d) :: !truthy_failed;
            raise ex)
 
 and check_truthy_once ctx c =
@@ -6064,6 +6089,27 @@ and check_truthy_once ctx c =
   | exception Loc.Error _ -> check ctx ~want:Types.Bool c
 
 and check_if ctx ?(tail = false) ?want loc c t e =
+  match
+    List.find_opt
+      (fun (n, (sc, r), w, _) ->
+         n == c && r == ctx.ret && w = want && same_scope sc ctx.scope)
+      (Hashtbl.find_all if_failed c.Ast.loc)
+  with
+  | Some (_, _, _, d) -> raise (Loc.Error d)
+  | None ->
+    let scope = ctx.scope in
+    incr if_depth;
+    Fun.protect
+      ~finally:(fun () ->
+          decr if_depth;
+          if !if_depth = 0 then Hashtbl.reset if_failed)
+      (fun () ->
+         try check_if_once ctx ~tail ?want loc c t e
+         with Loc.Error d as ex ->
+           Hashtbl.add if_failed c.Ast.loc (c, (scope, ctx.ret), want, d);
+           raise ex)
+
+and check_if_once ctx ~tail ?want loc c t e =
   let c = check_truthy ctx c in
   (* Both arms are the tail, and a one-armed [if] counts: [(when c (recur ...))]
      is how nearly every loop is written, and the branch is still the last

test/test_flan.ml

@@ -5691,14 +5691,33 @@ let () =
      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
+   let t0 = Unix.gettimeofday () in
+   match 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 over an i32 fails fast"
+       (Unix.gettimeofday () -. t0 < 3.0);
      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 long or chain refused at its last operand, with nothing expected of it.
+     Each if tries its else arm on its own terms before checking it at bool,
+     and a refused if is answered from memory, so a thousand operands fail
+     at once rather than in the square of that. *)
+  (let deep =
+     "(defn g [x i32] bool (let [b (or "
+     ^ String.concat " " (List.init 1000 (Printf.sprintf "(= x %d)"))
+     ^ " 5)] b))"
+   in
+   (* Timed rather than under [Watchdog.within]: a catch-all inside the
+      checker can swallow the alarm's exception. *)
+   let t0 = Unix.gettimeofday () in
+   match checked deep with
+   | _ -> check "a refused or chain is refused" false
+   | exception Loc.Error { Loc.dmsg; _ } ->
+     check "a refused or chain fails fast" (Unix.gettimeofday () -. t0 < 3.0);
+     check "a refused or chain keeps the one-operand message"
+       (dmsg = "expected bool, found the integer literal 5"));
   (* 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"