let's remove the field in a different PR

src/Init/Internal/Order/Basic.lean

@@ -488,7 +488,6 @@ instance instCCPOPProd [CCPO α] [CCPO β] : CCPO (α ×' β) where
   csup c := ⟨CCPO.csup (PProd.chain.fst c), CCPO.csup (PProd.chain.snd c)⟩
   csup_spec := by
     intro ⟨a, b⟩ c hchain
-    try dsimp -- TODO(kmill) remove
     constructor
     next =>
       intro ⟨h₁, h₂⟩ ⟨a', b'⟩ cab

src/Lean/Elab/Print.lean

@@ -86,8 +86,9 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
   let env ← getEnv
   let kind := if isClass env id then "class" else "structure"
   let header ← mkHeader' kind id levelParams type isUnsafe (sig := false)
+  let levels := levelParams.map Level.param
   liftTermElabM <| forallTelescope (← getConstInfo id).type fun params _ =>
-    let s := Expr.const id (levelParams.map .param)
+    let s := Expr.const id levels
     withLocalDeclD `self (mkAppN s params) fun self => do
       let mut m : MessageData := header
       -- Signature
@@ -100,15 +101,12 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
       unless parents.isEmpty do
         m := m ++ Format.line ++ "parents:"
         for parent in parents do
-          let ptype ← inferType (mkApp (mkAppN (.const parent.projFn (levelParams.map .param)) params) self)
+          let ptype ← inferType (mkApp (mkAppN (.const parent.projFn levels) params) self)
           m := m ++ indentD m!"{.ofConstName parent.projFn (fullNames := true)} : {ptype}"
       -- Fields
-      -- Collect params in a map for default value processing
-      let paramMap : NameMap Expr ← params.foldlM (init := {}) fun paramMap param => do
-        pure <| paramMap.insert (← param.fvarId!.getUserName) param
       -- Collect autoParam tactics, which are all on the flat constructor:
       let flatCtorName := mkFlatCtorOfStructCtorName ctor
-      let flatCtorInfo ← try getConstInfo flatCtorName catch _ => getConstInfo (id ++ `_flat_ctor) -- TODO(kmill): remove catch
+      let flatCtorInfo ← getConstInfo flatCtorName
       let autoParams : NameMap Syntax ← forallTelescope flatCtorInfo.type fun args _ =>
         args[numParams:].foldlM (init := {}) fun set arg => do
           let decl ← arg.fvarId!.getDecl
@@ -136,9 +134,7 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
               let stx : TSyntax ``Parser.Tactic.tacticSeq := ⟨stx⟩
               pure m!" := by{indentD stx}"
             else if let some defFn := getEffectiveDefaultFnForField? env id field then
-              let cinfo ← getConstInfo defFn
-              let defValue ← instantiateValueLevelParams cinfo (levelParams.map .param)
-              if let some val ← processDefaultValue paramMap fieldMap defValue then
+              if let some (_, val) ← instantiateStructDefaultValueFn? defFn levels params (pure ∘ fieldMap.find?) then
                 pure m!" :={indentExpr val}"
               else
                 pure m!" := <error>"
@@ -157,24 +153,6 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
       -- Omit proofs; the delaborator enables `pp.proofs` for non-constant proofs, but we don't want this for default values
       withOptions (fun opts => opts.set pp.proofs.name false) do
         logInfo m
-where
-  processDefaultValue (paramMap : NameMap Expr) (fieldValues : NameMap Expr) : Expr → MetaM (Option Expr)
-  | .lam n d b c => do
-    if c.isExplicit then
-      let some val := fieldValues.find? n | return none
-      if ← isDefEq (← inferType val) d then
-        processDefaultValue paramMap fieldValues (b.instantiate1 val)
-      else
-        return none
-    else
-      let some param := paramMap.find? n | return none
-      if ← isDefEq (← inferType param) d then
-        processDefaultValue paramMap fieldValues (b.instantiate1 param)
-      else
-        return none
-  | e =>
-    let_expr id _ a := e | return some e
-    return some a
 
 private def printIdCore (id : Name) : CommandElabM Unit := do
   let env ← getEnv

src/Lean/Elab/StructInst.lean

@@ -399,7 +399,7 @@ The `structureType?` is the expected type of the structure instance.
 -/
 private def mkCtorHeader (ctorVal : ConstructorVal) (structureType? : Option Expr) : TermElabM CtorHeaderResult := do
   let flatCtorName := mkFlatCtorOfStructCtorName ctorVal.name
-  let cinfo ← try getConstInfo flatCtorName catch _ => getConstInfo (ctorVal.induct ++ `_flat_ctor) -- TODO(kmill): remove catch
+  let cinfo ← getConstInfo flatCtorName
   let us ← mkFreshLevelMVars ctorVal.levelParams.length
   let mut type ← instantiateTypeLevelParams cinfo.toConstantVal us
   let mut params : Array Expr := #[]
@@ -726,36 +726,13 @@ After default values are resolved, then the one that is added to the environment
 as an `_inherited_default` auxiliary function is normalized; we don't do those normalizations here.
 -/
 private partial def getFieldDefaultValue? (fieldName : Name) : StructInstM (NameSet × Option Expr) := do
-  match getEffectiveDefaultFnForField? (← getEnv) (← read).structName fieldName with
-  | none => return ({}, none)
-  | some defaultFn =>
-    trace[Elab.struct] "default fn for '{fieldName}' is '{.ofConstName defaultFn}'"
-    let cinfo ← getConstInfo defaultFn
-    let us := (← read).levels
-    go? {} <| (← instantiateValueLevelParams cinfo us).beta (← read).params
-where
-  logFailure : StructInstM (NameSet × Option Expr) := do
-    logError m!"default value for field '{fieldName}' of structure '{.ofConstName (← read).structName}' could not be instantiated, ignoring"
-    return ({}, none)
-  go? (usedFields : NameSet) (e : Expr) : StructInstM (NameSet × Option Expr) := do
-    match e with
-    | Expr.lam n d b c =>
-      if c.isExplicit then
-        let some val := (← get).fieldMap.find? n
-          | trace[Elab.struct] "default value error: no value for field '{n}'"
-            logFailure
-        let valType ← inferType val
-        if (← isDefEq valType d) then
-          go? (usedFields.insert n) (b.instantiate1 val)
-        else
-          trace[Elab.struct] "default value error: {← mkHasTypeButIsExpectedMsg valType d}"
-          logFailure
-      else
-        trace[Elab.struct] "default value error: unexpected implicit argument{indentExpr e}"
-        logFailure
-    | e =>
-      let_expr id _ a := e | return (usedFields, some e)
-      return (usedFields, some a)
+  let some defFn := getEffectiveDefaultFnForField? (← getEnv) (← read).structName fieldName
+    | return ({}, none)
+  let fieldMap := (← get).fieldMap
+  let some (fields, val) ← instantiateStructDefaultValueFn? defFn (← read).levels (← read).params (pure ∘ fieldMap.find?)
+    | logError m!"default value for field '{fieldName}' of structure '{.ofConstName (← read).structName}' could not be instantiated, ignoring"
+      return ({}, none)
+  return (fields, val)
 
 /--
 Auxiliary type for `synthDefaultFields`
@@ -935,7 +912,7 @@ where
     let ctor := getStructureCtor (← getEnv) parentName
     unless params.size == ctor.numParams do return .done e
     let flatCtorName := mkFlatCtorOfStructCtorName ctor.name
-    let cinfo ← try getConstInfo flatCtorName catch _ => getConstInfo (ctor.induct ++ `_flat_ctor) -- TODO(kmill): remove catch
+    let cinfo ← getConstInfo flatCtorName
     let ctorVal ← instantiateValueLevelParams cinfo us
     let fieldArgs := parentFields.map fieldMap.find!
     let e' := (ctorVal.beta params).beta fieldArgs

src/Lean/Elab/Structure.lean

@@ -529,46 +529,25 @@ private def fieldFromMsg (info : StructFieldInfo) : MessageData :=
     m!"field '{info.name}'"
 
 /--
-Instantiates default value for field `fieldName` set at structure `structName`.
-The arguments for the `_default` auxiliary function are provided by `fieldMap`.
+Instantiates default value for field `fieldName` set at structure `structName`, using the field fvars in the `StructFieldInfo`s.
 After default values are resolved, then the one that is added to the environment
-as an `_inherited_default` auxiliary function is normalized; we don't do those normalizations here.
+as an `_inherited_default` auxiliary function is normalized;
+we don't do those normalizations here, since that could be wasted effort if this default isn't chosen.
 -/
-private partial def getFieldDefaultValue? (structName : Name) (paramMap : NameMap Expr) (fieldName : Name) : StructElabM (Option Expr) := do
-  match getDefaultFnForField? (← getEnv) structName fieldName with
-  | none => return none
-  | some defaultFn =>
-    let cinfo ← getConstInfo defaultFn
-    let us ← mkFreshLevelMVarsFor cinfo
-    go? (← instantiateValueLevelParams cinfo us)
-where
-  failed : MetaM (Option Expr) := do
-    logWarning m!"ignoring default value for field '{fieldName}' defined at '{.ofConstName structName}'"
-    return none
+private partial def getFieldDefaultValue? (structName : Name) (params : Array Expr) (fieldName : Name) : StructElabM (Option Expr) := do
+  let some defFn := getDefaultFnForField? (← getEnv) structName fieldName
+    | return none
+  let fieldVal? (n : Name) : StructElabM (Option Expr) := do
+    let some info ← findFieldInfo? n | return none
+    return info.fvar
+  let some (_, val) ← instantiateStructDefaultValueFn? defFn none params fieldVal?
+    | logWarning m!"default value for field '{fieldName}' of structure '{.ofConstName structName}' could not be instantiated, ignoring"
+      return none
+  return val
 
-  go? (e : Expr) : StructElabM (Option Expr) := do
-    match e with
-    | Expr.lam n d b c =>
-      if c.isExplicit then
-        let some info ← findFieldInfo? n | failed
-        let valType ← inferType info.fvar
-        if (← isDefEq valType d) then
-          go? (b.instantiate1 info.fvar)
-        else
-          failed
-      else
-        let some param := paramMap.find? n | return none
-        if ← isDefEq (← inferType param) d then
-          go? (b.instantiate1 param)
-        else
-          failed
-    | e =>
-      let r := if e.isAppOfArity ``id 2 then e.appArg! else e
-      return some (← reduceFieldProjs r)
-
-private def getFieldDefault? (structName : Name) (paramMap : NameMap Expr) (fieldName : Name) :
+private def getFieldDefault? (structName : Name) (params : Array Expr) (fieldName : Name) :
     StructElabM (Option StructFieldDefault) := do
-  if let some val ← getFieldDefaultValue? structName (paramMap : NameMap Expr) fieldName then
+  if let some val ← getFieldDefaultValue? structName params fieldName then
     -- Important: we use `getFieldDefaultValue?` because we want default value definitions, not *inherited* ones, to properly handle diamonds
     trace[Elab.structure] "found default value for '{fieldName}' from '{.ofConstName structName}'{indentExpr val}"
     return StructFieldDefault.optParam val
@@ -593,7 +572,7 @@ Adds `fieldName` of type `fieldType` from structure `structName`.
 See `withStructFields` for meanings of other arguments.
 -/
 private partial def withStructField (view : StructView) (sourceStructNames : List Name) (inSubobject? : Option Expr)
-    (structName : Name) (paramMap : NameMap Expr) (fieldName : Name) (fieldType : Expr)
+    (structName : Name) (params : Array Expr) (fieldName : Name) (fieldType : Expr)
     (k : Expr → StructElabM α) : StructElabM α := do
   trace[Elab.structure] "withStructField '{.ofConstName structName}', field '{fieldName}'"
   let fieldType ← instantiateMVars fieldType
@@ -612,7 +591,7 @@ private partial def withStructField (view : StructView) (sourceStructNames : Lis
     let existingFieldType ← inferType existingField.fvar
     unless (← isDefEq fieldType existingFieldType) do
       throwError "field type mismatch, field '{fieldName}' from parent '{.ofConstName structName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}"
-    if let some d ← getFieldDefault? structName paramMap fieldName then
+    if let some d ← getFieldDefault? structName params fieldName then
       addFieldInheritedDefault fieldName structName d
     k existingField.fvar
   else
@@ -639,7 +618,7 @@ private partial def withStructField (view : StructView) (sourceStructNames : Lis
         binfo := fieldInfo.binderInfo
         projFn? := fieldInfo.projFn
       }
-      if let some d ← getFieldDefault? structName paramMap fieldName then
+      if let some d ← getFieldDefault? structName params fieldName then
         addFieldInheritedDefault fieldName structName d
       k fieldFVar
 
@@ -652,7 +631,7 @@ Does not add a parent field for the structure itself; that is done by `withStruc
 - the continuation `k` is run with a constructor expression for this structure
 -/
 private partial def withStructFields (view : StructView) (sourceStructNames : List Name)
-    (structType : Expr) (inSubobject? : Option Expr) (paramMap : NameMap Expr)
+    (structType : Expr) (inSubobject? : Option Expr)
     (k : Expr → StructElabM α) : StructElabM α := do
   let structName ← getStructureName structType
   let .const _ us := structType.getAppFn | unreachable!
@@ -688,7 +667,7 @@ private partial def withStructFields (view : StructView) (sourceStructNames : Li
       let fieldName := fields[i]
       let fieldMVar := fieldMVars[i]!
       let fieldType ← inferType fieldMVar
-      withStructField view sourceStructNames inSubobject? structName paramMap fieldName fieldType fun fieldFVar => do
+      withStructField view sourceStructNames inSubobject? structName params fieldName fieldType fun fieldFVar => do
         fieldMVar.mvarId!.assign fieldFVar
         goFields (i + 1)
     else
@@ -739,14 +718,7 @@ private partial def withStruct (view : StructView) (sourceStructNames : List Nam
 
     let allFields := getStructureFieldsFlattened env structName (includeSubobjectFields := false)
     let withStructFields' (kind : StructFieldKind) (inSubobject? : Option Expr) (k : StructFieldInfo → StructElabM α) : StructElabM α := do
-      -- Create a parameter map for default value processing
-      let info ← getConstInfoInduct structName
-      let paramMap : NameMap Expr ← forallTelescope info.type fun xs _ => do
-        let mut paramMap := {}
-        for param in params, x in xs do
-          paramMap := paramMap.insert (← x.fvarId!.getUserName) param
-        return paramMap
-      withStructFields view sourceStructNames structType inSubobject? paramMap fun structVal => do
+      withStructFields view sourceStructNames structType inSubobject? fun structVal => do
         if let some _ ← findFieldInfo? structFieldName then
           throwErrorAt projRef "field '{structFieldName}' has already been declared\n\n\
             The 'toParent : P' syntax can be used to adjust the name for the parent projection"
@@ -755,7 +727,7 @@ private partial def withStruct (view : StructView) (sourceStructNames : List Nam
         -- which for inherited fields might not have been seen yet.
         -- Note: duplication is ok for now. We use a stable sort later.
         for fieldName in allFields do
-          if let some d ← getFieldDefault? structName paramMap fieldName then
+          if let some d ← getFieldDefault? structName params fieldName then
             addFieldInheritedDefault fieldName structName d
         withLetDecl rawStructFieldName structType structVal fun structFVar => do
           let info : StructFieldInfo := {
@@ -1227,8 +1199,8 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
         fieldName  := info.name
         projFn     := info.declName
         binderInfo := info.binfo
-        autoParam? := if let some (.autoParam tactic) := info.resolvedDefault? then some tactic else none
         subobject? := if let .subobject parentName := info.kind then parentName else none
+        autoParam? := none -- deprecated field
       }
     else
       return none

src/Lean/Meta/Structure.lean

@@ -181,4 +181,42 @@ def etaStructReduce (e : Expr) (p : Name → Bool) : MetaM Expr := do
     else
       return .continue)
 
+/--
+Instantiates the default value given by the default value function `defaultFn`.
+- `defaultFn` is the default value function returned by `Lean.getEffectiveDefaultFnForField?` or `Lean.getDefaultFnForField?`.
+- `levels?` is the list of levels to use, and otherwise the levels are inferred.
+- `params` is the list of structure parameters. These are assumed to be correct for the given levels.
+- `fieldVal?` is a function for getting fields for values, if they exist.
+
+If successful, returns a set of fields used and the resulting default value.
+Success is expected. Callers should do metacontext backtracking themselves if needed.
+-/
+partial def instantiateStructDefaultValueFn?
+    [Monad m] [MonadEnv m] [MonadError m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
+    (defaultFn : Name) (levels? : Option (List Level)) (params : Array Expr)
+    (fieldVal? : Name → m (Option Expr)) : m (Option (NameSet × Expr)) := do
+  let cinfo ← getConstInfo defaultFn
+  let us ← levels?.getDM (mkFreshLevelMVarsFor cinfo)
+  assert! us.length == cinfo.levelParams.length
+  let mut val ← liftMetaM <| instantiateValueLevelParams cinfo us
+  for param in params do
+    let .lam _ t b _ := val | return none
+    -- If no levels given, need to unify to solve for level mvars.
+    if levels?.isNone then
+      unless (← isDefEq (← inferType param) t) do return none
+    val := b.instantiate1 param
+  go? {} val
+where
+  go? (usedFields : NameSet) (e : Expr) : m (Option (NameSet × Expr)) := do
+    match e with
+    | .lam n d b _ =>
+      let some val ← fieldVal? n | return none
+      if (← isDefEq (← inferType val) d) then
+        go? (usedFields.insert n) (b.instantiate1 val)
+      else
+        return none
+    | e =>
+      let_expr id _ a := e | return some (usedFields, e)
+      return some (usedFields, a)
+
 end Lean.Meta

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -9,6 +9,7 @@ import Lean.PrettyPrinter.Delaborator.Basic
 import Lean.PrettyPrinter.Delaborator.SubExpr
 import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
 import Lean.Meta.CoeAttr
+import Lean.Meta.Structure
 
 namespace Lean.PrettyPrinter.Delaborator
 open Lean.Meta
@@ -556,8 +557,7 @@ def delabDelayedAssignedMVar : Delab := whenNotPPOption getPPMVarsDelayed do
     delabMVarAux decl.mvarIdPending
 
 private partial def collectStructFields
-    (structName : Name)
-    (paramMap : NameMap Expr)
+    (structName : Name) (levels : List Level) (params : Array Expr)
     (fields : Array (TSyntax ``Parser.Term.structInstField))
     (fieldValues : NameMap Expr)
     (s : ConstructorVal) :
@@ -575,14 +575,13 @@ private partial def collectStructFields
         if ← getPPOption getPPStructureInstancesFlatten then
           if let some s' ← isConstructorApp? (← getExpr) then
             if s'.induct == parentName then
-              let (fieldValues, fields) ← collectStructFields structName paramMap fields fieldValues s'
+              let (fieldValues, fields) ← collectStructFields structName levels params fields fieldValues s'
               return (i + 1, fieldValues, fields)
-      /- Does it have the default value, and should it be omitted? -/
+      /- Does this field have a default value? and if so, can we omit the field? -/
       unless ← getPPOption getPPStructureInstancesDefaults do
         if let some defFn := getEffectiveDefaultFnForField? (← getEnv) structName fieldName then
-          let cinfo ← getConstInfo defFn
-          let defValue := cinfo.instantiateValueLevelParams! (← mkFreshLevelMVarsFor cinfo)
-          if let some defValue ← withNewMCtxDepth <| processDefaultValue paramMap fieldValues defValue then
+          -- Use `withNewMCtxDepth` to prevent delaborator from solving metavariables.
+          if let some (_, defValue) ← withNewMCtxDepth <| instantiateStructDefaultValueFn? defFn levels params (pure ∘ fieldValues.find?) then
             if ← withReducible <| withNewMCtxDepth <| isDefEq defValue (← getExpr) then
               -- Default value matches, skip the field.
               return (i + 1, fieldValues, fields)
@@ -596,24 +595,6 @@ private partial def collectStructFields
       let field ← `(structInstField|$fieldId:ident := $value)
       return (i + 1, fieldValues, fields.push field))
   return (fieldValues, fields)
-where
-  processDefaultValue (paramMap : NameMap Expr) (fieldValues : NameMap Expr) : Expr → MetaM (Option Expr)
-  | .lam n d b c => do
-    if c.isExplicit then
-      let some val := fieldValues.find? n | return none
-      if ← isDefEq (← inferType val) d then
-        processDefaultValue paramMap fieldValues (b.instantiate1 val)
-      else
-        return none
-    else
-      let some param := paramMap.find? n | return none
-      if ← isDefEq (← inferType param) d then
-        processDefaultValue paramMap fieldValues (b.instantiate1 param)
-      else
-        return none
-  | e =>
-    let_expr id _ a := e | return some e
-    return some a
 
 /--
 Delaborate structure constructor applications using structure instance notation or anonymous constructor notation.
@@ -663,14 +644,10 @@ def delabStructureInstance : Delab := do
     If `pp.structureInstances.flatten` is true (and `pp.explicit` is false or the subobject has no parameters)
     then subobjects are flattened.
     -/
-    -- For default value handling, we need to create a map of type parameter names to expressions.
+    let .const _ levels := (← getExpr).getAppFn | failure
     let args := (← getExpr).getAppArgs
-    let paramMap : NameMap Expr ← forallTelescope s.type fun xs _ => do
-      let mut paramMap := {}
-      for param in args[:s.numParams], x in xs do
-        paramMap := paramMap.insert (← x.fvarId!.getUserName) param
-      return paramMap
-    let (_, fields) ← collectStructFields s.induct paramMap #[] {} s
+    let params := args[0:s.numParams]
+    let (_, fields) ← collectStructFields s.induct levels params #[] {} s
     let tyStx? : Option Term ← withType do
       if ← getPPOption getPPStructureInstanceType then delab else pure none
     `({ $fields,* $[: $tyStx?]? })

src/Lean/Structure.lean

@@ -27,8 +27,7 @@ structure StructureFieldInfo where
   subobject? : Option Name
   /-- The binder info for the field from the `structure` definition. -/
   binderInfo : BinderInfo
-  /-- If set, the field is an autoparam (a field declared using `fld := by ...` syntax).
-  The expression evaluates to a tactic `Syntax` object. Generally this is an `Expr.const` expression. -/
+  /-- Deprecated. -/
   autoParam? : Option Expr := none
   deriving Inhabited, Repr