diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 61d372630f94..baf808e2a847 100644
--- a/src/Lean/CoreM.lean
+++ b/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.
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 2972577e308a..2356370d0a76 100644
--- a/src/Lean/Elab/Command.lean
+++ b/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
diff --git a/src/runtime/apply.cpp b/src/runtime/apply.cpp
index cb24a9b364cb..2205a5830fc5 100644
--- a/src/runtime/apply.cpp
+++ b/src/runtime/apply.cpp
@@ -890,12 +890,21 @@ if (arity == fixed + n) {
   lean_dec_ref(f);
   return r;
 } else if (arity < fixed + n) {
-  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
-  for (unsigned i = 0; i < fixed; i++) { lean_inc(fx(i)); args[i] = fx(i); }
-  for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
-  obj * new_f = FNN(f)(args);
-  lean_dec_ref(f);
-  return lean_apply_n(new_f, n+fixed-arity, &as[arity-fixed]);
+  unsigned m = arity - fixed;
+  obj * new_f;
+  if (arity > LEAN_CLOSURE_MAX_ARGS) {
+    // `f`'s code takes its arguments as an array
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
+    for (unsigned i = 0; i < fixed; i++) { lean_inc(fx(i)); args[i] = fx(i); }
+    for (unsigned i = 0; i < m; i++) args[fixed+i] = as[i];
+    new_f = FNN(f)(args);
+    lean_dec_ref(f);
+  } else {
+    // `f`'s code takes `arity` separate arguments, so it must not be invoked through `FNN`;
+    // `lean_apply_n` dispatches on `m` and consumes `f`.
+    new_f = lean_apply_n(f, m, as);
+  }
+  return lean_apply_n(new_f, n - m, &as[m]);
 } else {
   return fix_args(f, n, as);
 }