perf: fuse fvar substitution into instantiateMVars

src/Lean/Elab/PreDefinition/Basic.lean

@@ -11,6 +11,7 @@ public import Lean.Util.NumApps
 public import Lean.Meta.Eqns
 public import Lean.Elab.RecAppSyntax
 public import Lean.Elab.DefView
+import Lean.Meta.InstMVarsAll
 
 public section
 
@@ -48,7 +49,7 @@ Applies `Lean.instantiateMVars` to the types of values of each predefinition.
 -/
 def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
   preDefs.mapM fun preDef => do
-    pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) }
+    pure { preDef with type := (← instantiateAllMVars preDef.type), value := (← instantiateAllMVars preDef.value) }
 
 /--
 Applies `Lean.Elab.Term.levelMVarToParam` to the types of each predefinition.

src/Lean/Meta/InstMVarsAll.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+module
+
+prelude
+public import Lean.Meta.Basic
+
+namespace Lean.Meta
+
+@[extern "lean_instantiate_expr_mvars_original"]
+private opaque instantiateMVarsOriginalImp (mctx : MetavarContext) (e : Expr) :
+  MetavarContext × Expr
+
+@[extern "lean_instantiate_expr_mvars_all"]
+private opaque instantiateAllMVarsImp (mctx : MetavarContext) (e : Expr) :
+  MetavarContext × Expr
+
+@[extern "lean_instantiate_expr_mvars_all_sharing"]
+private opaque instantiateAllMVarsSharingImp (mctx : MetavarContext) (e : Expr) :
+  MetavarContext × Expr
+
+/-- The original single-pass `instantiateMVars` implementation, exposed for benchmarking
+    independently of which implementation is the default. -/
+public def instantiateMVarsOriginal (e : Expr) : MetaM Expr := do
+  if !e.hasMVar then return e
+  let (mctx, eNew) := instantiateMVarsOriginalImp (← getMCtx) e
+  modifyMCtx fun _ => mctx; return eNew
+
+/-- Like `instantiateMVars` but uses a fused two-pass approach.
+    Pass 1 resolves direct mvar assignments with write-back.
+    Pass 2 resolves delayed assignments with a fused fvar substitution,
+    avoiding separate `replace_fvars` calls. Preserves sharing using
+    a flat cache with lazy staleness detection via persistent scope
+    generation snapshots. -/
+public def instantiateAllMVars (e : Expr) : MetaM Expr := do
+  if !e.hasMVar then return e
+  let (mctx, eNew) := instantiateAllMVarsImp (← getMCtx) e
+  modifyMCtx fun _ => mctx; return eNew
+
+/-- Alias for `instantiateAllMVars`. -/
+public def instantiateAllMVarsSharing (e : Expr) : MetaM Expr := do
+  if !e.hasMVar then return e
+  let (mctx, eNew) := instantiateAllMVarsSharingImp (← getMCtx) e
+  modifyMCtx fun _ => mctx; return eNew
+
+end Lean.Meta

src/Lean/MetavarContext.lean

@@ -400,6 +400,12 @@ def MetavarContext.getDelayedMVarAssignmentCore? (mctx : MetavarContext) (mvarId
 def MetavarContext.getDelayedMVarAssignmentExp (mctx : MetavarContext) (mvarId : MVarId) : Option DelayedMetavarAssignment :=
   mctx.dAssignment.find? mvarId
 
+@[export lean_delayed_mvar_assignment_fvars]
+def DelayedMetavarAssignment.fvarsExp (d : DelayedMetavarAssignment) : Array Expr := d.fvars
+
+@[export lean_delayed_mvar_assignment_mvar_id_pending]
+def DelayedMetavarAssignment.mvarIdPendingExp (d : DelayedMetavarAssignment) : MVarId := d.mvarIdPending
+
 def getDelayedMVarAssignment? [Monad m] [MonadMCtx m] (mvarId : MVarId) : m (Option DelayedMetavarAssignment) :=
   return (← getMCtx).getDelayedMVarAssignmentCore? mvarId
 
@@ -1483,6 +1489,24 @@ def levelMVarToParam (mctx : MetavarContext) (alreadyUsedPred : Name → Bool) (
 def getExprAssignmentDomain (mctx : MetavarContext) : Array MVarId :=
   mctx.eAssignment.foldl (init := #[]) fun a mvarId _ => Array.push a mvarId
 
+/--
+Abstract the given fvars from an unassigned mvar by creating a delayed-assigned mvar.
+Returns `(mctx', result)` where `result` has the fvars replaced by `values`.
+This can be used when encountering an unassigned mvar with an active fvar
+substitution.
+-/
+@[export lean_abstract_mvar_fvars]
+def abstractMVarFVars (mctx : MetavarContext) (mvarId : MVarId) (fvars : Array Expr) (values : Array Expr) : MetavarContext × Expr :=
+  match mctx.decls.find? mvarId with
+  | none => (mctx, mkMVar mvarId)
+  | some _mvarDecl =>
+    let ngen : NameGenerator := { namePrefix := `_noUpdate, idx := mctx.mvarCounter }
+    let ctx : MkBinding.Context := { quotContext := `_root_, preserveOrder := false }
+    let state : MkBinding.State := { mctx, nextMacroScope := 0, ngen }
+    match (MkBinding.elimMVarDeps fvars (mkMVar mvarId) ctx).run state with
+    | .ok e s => (s.mctx, Expr.replaceFVars e fvars values)
+    | .error _ s => (s.mctx, mkMVar mvarId)
+
 end MetavarContext
 
 namespace MVarId

src/kernel/CMakeLists.txt

@@ -19,4 +19,5 @@ add_library(
   inductive.cpp
   trace.cpp
   instantiate_mvars.cpp
+  instantiate_mvars_all.cpp
 )

src/kernel/instantiate_mvars.cpp

@@ -100,6 +100,8 @@ extern "C" LEAN_EXPORT object * lean_instantiate_level_mvars(object * m, object
 
 extern "C" object * lean_get_mvar_assignment(obj_arg mctx, obj_arg mid);
 extern "C" object * lean_get_delayed_mvar_assignment(obj_arg mctx, obj_arg mid);
+extern "C" object * lean_delayed_mvar_assignment_fvars(obj_arg d);
+extern "C" object * lean_delayed_mvar_assignment_mvar_id_pending(obj_arg d);
 extern "C" object * lean_assign_mvar(obj_arg mctx, obj_arg mid, obj_arg val);
 typedef object_ref delayed_assignment;
 
@@ -116,6 +118,14 @@ option_ref<delayed_assignment> get_delayed_mvar_assignment(metavar_ctx & mctx, n
     return option_ref<delayed_assignment>(lean_get_delayed_mvar_assignment(mctx.to_obj_arg(), mid.to_obj_arg()));
 }
 
+array_ref<expr> delayed_assignment_fvars(delayed_assignment const & d) {
+    return array_ref<expr>(lean_delayed_mvar_assignment_fvars(d.to_obj_arg()));
+}
+
+name delayed_assignment_mvar_id_pending(delayed_assignment const & d) {
+    return name(lean_delayed_mvar_assignment_mvar_id_pending(d.to_obj_arg()));
+}
+
 expr replace_fvars(expr const & e, array_ref<expr> const & fvars, expr const * rev_args) {
     size_t sz = fvars.size();
     if (sz == 0)
@@ -290,8 +300,8 @@ class instantiate_mvars_fn {
             metavariables, we replace the free variables `fvars` in `newVal` with the first
             `fvars.size` elements of `args`.
             */
-            array_ref<expr> fvars(cnstr_get(d.get_val().raw(), 0), true);
-            name mid_pending(cnstr_get(d.get_val().raw(), 1), true);
+            array_ref<expr> fvars = delayed_assignment_fvars(d.get_val());
+            name mid_pending = delayed_assignment_mvar_id_pending(d.get_val());
             if (fvars.size() > get_app_num_args(e)) {
                 /*
                 We don't have sufficient arguments for instantiating the free variables `fvars`.
@@ -362,12 +372,19 @@ class instantiate_mvars_fn {
     expr operator()(expr const & e) { return visit(e); }
 };
 
-extern "C" LEAN_EXPORT object * lean_instantiate_expr_mvars(object * m, object * e) {
+/* The original single-pass implementation, exposed for benchmarking. */
+extern "C" LEAN_EXPORT object * lean_instantiate_expr_mvars_original(object * m, object * e) {
     metavar_ctx mctx(m);
     expr e_new = instantiate_mvars_fn(mctx)(expr(e));
     object * r = alloc_cnstr(0, 2, 0);
     cnstr_set(r, 0, mctx.steal());
     cnstr_set(r, 1, e_new.steal());
     return r;
 }
+
+extern "C" LEAN_EXPORT object * lean_instantiate_expr_mvars_all_sharing(object * m, object * e);
+
+extern "C" LEAN_EXPORT object * lean_instantiate_expr_mvars(object * m, object * e) {
+    return lean_instantiate_expr_mvars_all_sharing(m, e);
+}
 }