From 1842bb5476406a8e9d916a26cbaf3069c3255791 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 21 May 2026 09:53:33 -0700
Subject: [PATCH] feat: improve performance of structure instance notation
 elaboration (#13760)

This PR improves elaboration performance for structure instance notation
with large numbers of fields. It also uses beta-reducing substitution
for structure parameters, which is already the case for structure
fields.

It substitutes field values into types when they are needed, avoiding
quadratic runtime complexity.
---
 src/Lean/Elab/StructInst.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 5c576ccbe5..a8d89a2528 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -414,6 +414,7 @@ private def mkCtorHeader (ctorVal : ConstructorVal) (structureType? : Option Exp
   for _ in *...ctorVal.numParams do
     let .forallE _ d b bi := type
       | throwError "unexpected constructor type"
+    let d := d.instantiateBetaRevRange 0 params.size params
     let param ←
       if bi.isInstImplicit then
         let mvar ← mkFreshExprMVar d .synthetic
@@ -422,7 +423,8 @@ private def mkCtorHeader (ctorVal : ConstructorVal) (structureType? : Option Exp
       else
         mkFreshExprMVar d
     params := params.push param
-    type := b.instantiate1 param
+    type := b
+  type := type.instantiateBetaRevRange 0 params.size params
   let structType := mkAppN (.const ctorVal.induct us) params
   if let some structureType := structureType? then
     discard <| isDefEq structureType structType
@@ -611,7 +613,8 @@ private structure StructInstContext where
   fieldViews : ExpandedFields
 
 private structure StructInstState where
-  /-- The type of the flat constructor with applied parameters and applied fields. -/
+  /-- Initially the type of the flat constructor after applying parameters. After each field, we
+  replace it with its body. May have bvars; needs to be instantiated with `fields`. -/
   type : Expr
   /-- A set of the structure name and all its parents. -/
   structNameSet : NameSet := {}
@@ -721,7 +724,7 @@ private def normalizeExpr (e : Expr) (zetaDeltaImpl : Bool := true) : StructInst
 private def addStructFieldAux (fieldName : Name) (e : Expr) : StructInstM Unit := do
   trace[Elab.structInst] "field {fieldName} := {.nestD e}"
   modify fun s => { s with
-    type := s.type.bindingBody!.instantiateBetaRevRange 0 1 #[e]
+    type := s.type.bindingBody!
     fields := s.fields.push e
     fieldMap := s.fieldMap.insert fieldName e
   }
@@ -1141,6 +1144,8 @@ private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : B
 private partial def loop : StructInstM Expr := withViewRef do
   let type := (← get).type
   if let .forallE fieldName fieldType _ binfo := type then
+    let fields := (← get).fields
+    let fieldType := fieldType.instantiateBetaRevRange 0 fields.size fields
     if let some fieldValue := (← get).fieldMap.find? fieldName then
       -- This is a field that was added by `addParentInstanceFields`
       trace[Elab.structInst] "processing inferred field `{fieldName}` : {fieldType}\ninferred value:{inlineExprTrailing fieldValue}"