[#14970] perf: give currRecDepth its own ReaderT layer in CoreM

batteries/Batteries/Lean/LawfulMonad.lean

@@ -31,7 +31,7 @@ instance : LawfulMonad BaseIO := inferInstanceAs <| LawfulMonad (ST _)
 instance : LawfulMonad IO := inferInstanceAs <| LawfulMonad (EIO _)
 
 instance : LawfulMonad CoreM :=
-  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ (EIO Exception))
+  inferInstanceAs <| LawfulMonad (ReaderT _ <| ReaderT _ <| StateRefT' _ _ (EIO Exception))
 instance : LawfulMonad MetaM :=
   inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ CoreM)
 instance : LawfulMonad TermElabM :=

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-08-27
+leanprover/lean4-pr-releases:pr-release-14970-08499f9

mathlib4/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean

@@ -142,7 +142,8 @@ Note: It is expensive to create two new `IO.Ref`s for every `MetaM` operation,
   -- mstate.modify fun s => { cache := s.cache }
   -- cstate.modify fun s => { env := s.env, cache := s.cache, ngen := s.ngen }
   let mctx := { keyedConfig := Config.toConfigWithKey { transparency := .reducible } }
-  match ← (((act name constInfo) mctx mstate) cctx cstate).toBaseIO with
+  -- `0` is the initial recursion depth of `CoreM`'s recursion-depth reader layer
+  match ← (((act name constInfo) mctx mstate) cctx 0 cstate).toBaseIO with
   | .ok a =>
     return a.foldl (fun t (val, entries) =>
       entries.foldl (fun t (key, entry) => t.push key (entry, val)) t) tree

mathlib4/Mathlib/Tactic/ClickSuggestions/SectionState.lean

@@ -79,8 +79,8 @@ where
 def SectionState.insertResult (s : SectionState α) (res : Result α)
     (isDup : α → α → MetaM Bool) : MetaM (SectionState α) := do
   let { results, errors } := s
-  let results ← fun c₁ c₂ c₃ c₄ ↦
-    (res.insertInArray results isDup c₁ c₂ c₃ c₄).catchExceptions fun ex ↦ do
+  let results ← fun c₁ c₂ c₃ c₄ c₅ ↦
+    (res.insertInArray results isDup c₁ c₂ c₃ c₄ c₅).catchExceptions fun ex ↦ do
     if let .internal id _ := ex then
       if id == interruptExceptionId then
         return default