perf: faster isProof major in reduceRec

src/Lean/Meta/InferType.lean

@@ -595,7 +595,8 @@ partial def isTypeFormerType (type : Expr) : MetaM Bool := do
 Returns `true` iff `type` is `Prop` or `As → Prop`.
 -/
 partial def isPropFormerType (type : Expr) : MetaM Bool := do
-  return (← typeFormerTypeLevel type) == .some .zero
+  let some l ← typeFormerTypeLevel type | return false
+  return l.isAlwaysZero
 
 /--
 Returns `true` iff `e : Sort _` or `e : (forall As, Sort _)`.

src/Lean/Meta/WHNF.lean

@@ -239,6 +239,21 @@ private def cleanupNatOffsetMajor (e : Expr) : MetaM Expr := do
   else
     return mkNatSucc (mkNatAdd e (toExpr (k - 1)))
 
+/-- Checks whether a recursor major is a proof. If `isProofQuick` fails, rather than run `isProp (← inferType major)`, we infer the sort of the major using the recursor's info. -/
+private def isMajorProof (recVal : RecursorVal) (recLvls : List Level) (major : Expr) : MetaM Bool := do
+  match ← isProofQuick major with
+    | .true => pure true
+    | .false => pure false
+    | .undef =>
+      withTraceNodeBefore `Meta.whnf (fun _ => return m!"isMajorProof {major}") do
+      let indInfo ← getConstVal recVal.getMajorInduct
+      /- If the type doesn't have large elimination, it must be a proof.
+         TODO once the `isImpredicative` field exists in `inductiveVal`s, use that to cover more cases here. -/
+      if indInfo.levelParams.length = recLvls.length then
+        return true
+      let lvls := recLvls.tail!
+      isPropFormerType (← instantiateTypeLevelParams indInfo lvls)
+
 /-- Auxiliary function for reducing recursor applications. -/
 private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : Array Expr) (failK : Unit → MetaM α) (successK : Expr → MetaM α) : MetaM α :=
   let majorIdx := recVal.getMajorIdx
@@ -250,7 +265,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A
       -- We use this trick because we abstract nested proofs occurring in definitions.
       -- Alternative design: do not abstract nested proofs used to justify well-founded recursion.
       withTransparency .all <| whnf major
-    else if !(← isProof major) then
+    else if !(← isMajorProof recVal recLvls major) then
       whnf major
     else
       pure major

stage0/src/stdlib_flags.h

@@ -1,6 +1,6 @@
 #include "util/options.h"
 
-// [ ] Check box to force CI to test stage 2 and run update-stage0 on PR merge
+// [X] Check box to force CI to test stage 2 and run update-stage0 on PR merge
 // (any other change to this file will do the same; ALL changes should be made to the stage0/ copy)
 
 namespace lean {

tests/elab/16108.lean

@@ -0,0 +1,13 @@
+/-!
+`decide` on bounded quantifiers must not need more recursion depth per element than before
+#15371. Checking whether the major premise of `Decidable.rec` is a proof used to infer the type of
+the unreduced instance, which gains a β-redex at every step of `Nat.decidableBallLT`. At the
+deepest step, that inference added depth proportional to the bound.
+-/
+
+example : ∀ i, i < 100 → i + 0 = i := by decide
+
+example : ∀ i : Fin 100, i.val + 0 = i.val := by decide
+
+-- Before #15371, the default `maxRecDepth` sufficed up to a bound of 165.
+example : ∀ i, i < 150 → i + 0 = i := by decide