perf: give currRecDepth its own ReaderT layer in CoreM

This PR stops the recursion-depth guard from rebuilding `Core.Context` on every recursive step. Roughly 96% of `Core.Context` reconstructions exist only to bump the depth counter, and each one paid a reference count increment per pointer field.

`withReader` can never reuse the `Context` record, so keeping `currRecDepth` there made every `withIncRecDepth` rebuild it. As its own reader layer the depth is just an extra argument, so a recursion step neither allocates nor touches a reference count. The layer sits inside the `Context` reader so that a bare `read` still resolves to `Context`, and `CoreM.run` gains an initial-depth parameter so nested command elaboration keeps inheriting its caller's depth.

Note this changes `CoreM`'s arity, which is externally observable in LCNF output.

Author: Kha

src/Lean/CoreM.lean

@@ -220,7 +220,6 @@ structure Context where
   /-- Auxiliary datastructure for converting `String.Pos` into Line/Column number. -/
   fileMap        : FileMap
   options        : Options := {}
-  currRecDepth   : Nat := 0
   maxRecDepth    : Nat := 1000
   ref            : Syntax := Syntax.missing
   currNamespace  : Name := Name.anonymous
@@ -252,8 +251,12 @@ The main features it provides are:
 - environment state
 - Lean options context
 - the current open namespace
+- the current recursion depth, as its own reader layer rather than a `Context` field: `withReader`
+  cannot reuse the `Context` record, so keeping the depth there made every recursion step rebuild
+  `Context` and pay one reference count increment per pointer field. The layer sits *inside* the
+  `Context` reader so that a bare `read` still resolves to `Context`.
 -/
-abbrev CoreM := ReaderT Context <| StateRefT State (EIO Exception)
+abbrev CoreM := ReaderT Context <| ReaderT Nat <| StateRefT State (EIO Exception)
 
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
@@ -306,8 +309,8 @@ instance : MonadDeclNameGenerator CoreM where
   setDeclNGen ngen := modify fun s => { s with auxDeclNGen := ngen }
 
 instance : MonadRecDepth CoreM where
-  withRecDepth d x := withReader (fun ctx => { ctx with currRecDepth := d }) x
-  getRecDepth := return (← read).currRecDepth
+  withRecDepth d x := fun ctx => withTheReader Nat (fun _ => d) (x ctx)
+  getRecDepth := fun _ => readThe Nat
   getMaxRecDepth := return (← read).maxRecDepth
 
 instance : MonadResolveName CoreM where
@@ -427,11 +430,13 @@ that are conditionally inaccessible, depending on the current value of the `tact
 def mkFreshUserName (n : Name) : CoreM Name :=
   mkFreshNameImp n
 
-@[inline] def CoreM.run (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State) :=
-  ((withConsistentCtx x) ctx).run s
+@[inline] def CoreM.run (x : CoreM α) (ctx : Context) (s : State) (recDepth : Nat := 0) :
+    EIO Exception (α × State) :=
+  (((withConsistentCtx x) ctx) recDepth).run s
 
-@[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
-  Prod.fst <$> x.run ctx s
+@[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) (recDepth : Nat := 0) :
+    EIO Exception α :=
+  Prod.fst <$> x.run ctx s recDepth
 
 /--
 Run a `CoreM` monad in IO.

src/Lean/Elab/Command.lean

@@ -267,7 +267,6 @@ private def runCore (x : CoreM α) : CommandElabM α := do
   let coreCtx : Core.Context := {
     fileName           := ctx.fileName
     fileMap            := ctx.fileMap
-    currRecDepth       := ctx.currRecDepth
     maxRecDepth        := s.maxRecDepth
     ref                := ctx.ref
     currNamespace      := scope.currNamespace
@@ -288,7 +287,7 @@ private def runCore (x : CoreM α) : CommandElabM α := do
     infoState.lazyAssignment := s.infoState.lazyAssignment
     traceState := s.traceState
     snapshotTasks := s.snapshotTasks
-  }
+  } (recDepth := ctx.currRecDepth)
   let (ea, coreS) ← liftM x
   modify fun s => { s with
     env                      := coreS.env
@@ -1096,7 +1095,7 @@ private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) :
     cmd.run {
       fileName := ctx.fileName
       fileMap := ctx.fileMap
-      currRecDepth := ctx.currRecDepth
+      currRecDepth := (← MonadRecDepth.getRecDepth)
       currMacroScope := ctx.currMacroScope
       ref := ctx.ref
       snap? := none