From fea941817df3f2fab018985691cb6be45248c2d1 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 8 Mar 2026 12:44:28 -0700 Subject: [PATCH 1/3] feat: mutually dependent `structure` default values, and self-dependence checking This PR changes the way default field values are elaborated in the `structure`/`class` commands so that they have all the fields in context. This allows the field defaults to be dependent on one another, which is already allowed for default values for inherited fields. Additionally, there is now an error that's logged if a field default depends on itself. Such fields will never be applicable. This fixes a bug reported by Aaron Liu [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/default.20structure.20values.20can.20depend.20on.20themselves/near/578014370) --- src/Lean/Elab/Structure.lean | 254 +++++++++--------- tests/elab/struct3.lean | 13 + tests/elab/structureElab.lean | 79 +++++- tests/elab_fail/struct1.lean | 12 +- tests/elab_fail/struct1.lean.out.expected | 11 +- .../structDefValueOverride.lean.out.expected | 2 +- 6 files changed, 234 insertions(+), 137 deletions(-) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 7ccc9bffd3ba..502757e4684f 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -167,6 +167,8 @@ structure StructFieldInfo where binfo : BinderInfo /-- Overrides for the parameters' binder infos when making the projections. The first component is a ref for the binder. -/ paramInfoOverrides : ExprMap (Syntax × BinderInfo) := {} + /-- Number of binders for the field's type, used for elaborating the default value for the field (if present). -/ + numBinders : Nat := 0 /-- Structure names that are responsible for this field being here. - Empty if the field is a `newField`. @@ -947,72 +949,63 @@ However, now `α` does not know its relationship to `toMagma`. This was not robust, since in diamond inheritance `α` only remembered *one* of its parents in this indirect way. -/ -private def solveParentMVars (e : Expr) : StructElabM Expr := do - let env ← getEnv - Term.synthesizeSyntheticMVars (postpone := .yes) +private def solveParentMVars (e : Expr) : StructElabM Unit := do let mvars ← getMVarsNoDelayed e - for mvar in mvars do - unless ← mvar.isAssigned do - let decl ← mvar.getDecl - if decl.kind.isNatural then - if let .const name .. := (← whnf decl.type).getAppFn then - if isStructure env name then - if let some parentInfo ← findParentFieldInfo? name then - if ← isDefEq (← mvar.getType) (← inferType parentInfo.fvar) then - discard <| MVarId.checkedAssign mvar parentInfo.fvar - return e + unless mvars.isEmpty do + Term.synthesizeSyntheticMVars (postpone := .yes) + for mvar in mvars do + unless ← mvar.isAssigned do + let decl ← mvar.getDecl + if decl.kind.isNatural then + withLCtx decl.lctx decl.localInstances do + if let .const name .. := (← whnf decl.type).getAppFn then + if let some parentInfo ← findParentFieldInfo? name then + if ← isDefEq (← mvar.getType) (← inferType parentInfo.fvar) then + discard <| MVarId.checkedAssign mvar parentInfo.fvar private def elabParamInfoUpdatesForField (structParams : Array Expr) (binders : Array Syntax) : StructElabM (Array Syntax × ExprMap (Syntax × BinderInfo)) := do elabParamInfoUpdates structParams binders -- Filter out all fields. We assume the remaining fvars are the possible parameters. (fun fvarId => return (← findFieldInfoByFVarId? fvarId).isNone) -private def elabFieldTypeValue (structParams : Array Expr) (view : StructFieldView) : - StructElabM (Option Expr × ExprMap (Syntax × BinderInfo) × Option StructFieldDefault) := do +/-- +Elaborates the field's type, returning +1. the type +2. the parameter binder info overrides +3. the number of binders for the type +-/ +private def elabFieldType (structParams : Array Expr) (view : StructFieldView) : + StructElabM (Expr × ExprMap (Syntax × BinderInfo) × Nat) := do withoutExporting (when := view.modifiers.isPrivate) do let state ← get let binders := view.binders.getArgs let (binders, paramInfoOverrides) ← elabParamInfoUpdatesForField structParams binders - Term.withAutoBoundImplicit <| Term.withAutoBoundImplicitForbiddenPred (fun n => view.name == n) <| Term.elabBinders binders fun params => do - match view.type? with - | none => - match view.default? with - | none => return (none, paramInfoOverrides, none) - | some (.optParam valStx) => - Term.synthesizeSyntheticMVarsNoPostponing - let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true)) - let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none - let value ← runStructElabM (init := state) <| solveParentMVars value - registerFailedToInferFieldType view.name (← inferType value) view.nameId - registerFailedToInferDefaultValue view.name value valStx - let value ← mkLambdaFVars params value - return (none, paramInfoOverrides, StructFieldDefault.optParam value) - | some (.autoParam tacticStx) => - throwErrorAt tacticStx "Invalid field declaration: Type must be provided when auto-param tactic is used" - | some typeStx => - let type ← Term.elabType typeStx - let type ← runStructElabM (init := state) <| solveParentMVars type - registerFailedToInferFieldType view.name type typeStx - Term.synthesizeSyntheticMVarsNoPostponing - let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true)) - match view.default? with + Term.withAutoBoundImplicit <| Term.withAutoBoundImplicitForbiddenPred (fun n => view.name == n) <| + Term.elabBinders binders fun params => do + let type ← + match view.type? with + | some typeStx => + let type ← Term.elabType typeStx + runStructElabM (init := state) <| solveParentMVars type + registerFailedToInferFieldType view.name type typeStx + pure type | none => - let type ← mkForallFVars params type - return (type, paramInfoOverrides, none) - | some (.optParam valStx) => - let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type - let value ← runStructElabM (init := state) <| solveParentMVars value - registerFailedToInferDefaultValue view.name value valStx - Term.synthesizeSyntheticMVarsNoPostponing - let type ← mkForallFVars params type - let value ← mkLambdaFVars params value - return (type, paramInfoOverrides, StructFieldDefault.optParam value) - | some (.autoParam tacticStx) => - let name := mkAutoParamFnOfProjFn view.declName - discard <| Term.declareTacticSyntax tacticStx name - let type ← mkForallFVars params type - return (type, paramInfoOverrides, StructFieldDefault.autoParam <| .const name []) + let type ← mkFreshTypeMVar + registerFailedToInferFieldType view.name type view.nameId + pure type + Term.synthesizeSyntheticMVarsNoPostponing + let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true)) + let type ← mkForallFVars params type + return (type, paramInfoOverrides, params.size) + +private def throwExistingDefaultValue (name : Name) : StructElabM α := + throwError "A default value for field `{name}` has already been set for this structure" +/-- +Elaborates the types of the fields. + +Default values are elaborated later, once the full local context has been created. +-/ private partial def withFields (structParams : Array Expr) (views : Array StructFieldView) (k : StructElabM α) : StructElabM α := do go 0 where @@ -1028,68 +1021,23 @@ where throwError "Field `{view.name}` has already been declared as a projection for parent `{.ofConstName parent.structName}`" match ← findFieldInfo? view.name with | none => - let (type?, paramInfoOverrides, default?) ← elabFieldTypeValue structParams view - match type?, default? with - | none, none => throwError "Invalid field: Type expected" - | some type, _ => - withLocalDecl view.rawName view.binderInfo type fun fieldFVar => do - addFieldInfo { ref := view.nameId, sourceStructNames := [], - name := view.name, declName := view.declName, fvar := fieldFVar, default? := default?, - binfo := view.binderInfo, paramInfoOverrides, - kind := StructFieldKind.newField } - withExporting (isExporting := wasExporting) do - go (i+1) - | none, some (.optParam value) => - let type ← inferType value - withLocalDecl view.rawName view.binderInfo type fun fieldFVar => do - addFieldInfo { ref := view.nameId, sourceStructNames := [], - name := view.name, declName := view.declName, fvar := fieldFVar, default? := default?, - binfo := view.binderInfo, paramInfoOverrides, - kind := StructFieldKind.newField } - withExporting (isExporting := wasExporting) do - go (i+1) - | none, some (.autoParam _) => - throwError "Field `{view.name}` has an auto-param but no type" + let (type, paramInfoOverrides, numBinders) ← elabFieldType structParams view + /- + Currently, having autoParams with binders is accepted for new fields. + This code is a possibility in case it should be an error. + (However, we could also arrange for the tactic to enter `numBinders` automatically!) + -- if numBinders > 0 && view.default? matches some (.autoParam ..) then + -- throwErrorAt view.binders "Invalid field: Unexpected binders for field `{view.name}` when setting auto-param tactic" + -/ + withLocalDecl view.rawName view.binderInfo type fun fieldFVar => do + addFieldInfo { ref := view.nameId, sourceStructNames := [], + name := view.name, declName := view.declName, + numBinders, fvar := fieldFVar, default? := none, + binfo := view.binderInfo, paramInfoOverrides, + kind := StructFieldKind.newField } + withExporting (isExporting := wasExporting) do + go (i+1) | some info => - let updateDefaultValue : StructElabM α := do - match view.default? with - | none => throwError "Field `{view.name}` has already been declared in a parent structure" - | some (.optParam valStx) => - if let some type := view.type? then - throwErrorAt type "Omit the type of field `{view.name}` to set its default value" - else - if info.default?.isSome then - throwError "A new default value for field `{view.name}` has already been set in this structure" - let mut valStx := valStx - let (binders, paramInfoOverrides) ← elabParamInfoUpdatesForField structParams view.binders.getArgs - unless paramInfoOverrides.isEmpty do - let params := MessageData.joinSep (paramInfoOverrides.toList.map (m!"{·.1}")) ", " - throwError "Cannot override structure parameter binder kinds when overriding the default value: {params}" - if binders.size > 0 then - valStx ← `(fun $binders* => $valStx:term) - let fvarType ← inferType info.fvar - let value ← Term.elabTermEnsuringType valStx fvarType - registerFailedToInferDefaultValue view.name value valStx - pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref } - if let some projFn := info.projFn? then Term.addTermInfo' view.ref (← mkConstWithLevelParams projFn) - replaceFieldInfo { info with ref := view.nameId, default? := StructFieldDefault.optParam value } - withExporting (isExporting := wasExporting) do - go (i+1) - | some (.autoParam tacticStx) => - if let some type := view.type? then - throwErrorAt type "Omit the type of field `{view.name}` to set its auto-param tactic" - else - if info.default?.isSome then - throwError "A new default value for field `{view.name}` has already been set in this structure" - if view.binders.getArgs.size > 0 then - throwErrorAt view.binders "Invalid field: Unexpected binders when setting auto-param tactic for inherited field" - let name := mkAutoParamFnOfProjFn view.declName - discard <| Term.declareTacticSyntax tacticStx name - replaceFieldInfo { info with ref := view.nameId, default? := StructFieldDefault.autoParam (.const name []) } - pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref } - if let some projFn := info.projFn? then Term.addTermInfo' view.ref (← mkConstWithLevelParams projFn) - withExporting (isExporting := wasExporting) do - go (i+1) match info.kind with | StructFieldKind.newField => throwError "Field `{view.name}` has already been declared" | StructFieldKind.subobject n @@ -1103,10 +1051,72 @@ where throwError m!"Field `{view.name}` has already been declared as a projection for an indirect parent structure `{.ofConstName n}`" ++ .note m!"This projection was inherited from {inheritanceMsg}" | StructFieldKind.copiedField - | StructFieldKind.fromSubobject => updateDefaultValue + | StructFieldKind.fromSubobject => + match view.default? with + | none => throwError "Field `{view.name}` has already been declared in a parent structure" + | some default => + -- Prepare the default value for later elaboration by `elabStructFieldDefaults`. + if let some projFn := info.projFn? then Term.addTermInfo' view.ref (← mkConstWithLevelParams projFn) + pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref } + match default with + | .optParam _ => + let (_, paramInfoOverrides) ← elabParamInfoUpdatesForField structParams view.binders.getArgs + unless paramInfoOverrides.isEmpty do + let params := MessageData.joinSep (paramInfoOverrides.toList.map (m!"{·.1}")) ", " + throwError "Cannot override structure parameter binder kinds when overriding the default value: {params}" + withExporting (isExporting := wasExporting) do + go (i+1) + | .autoParam _ => + if let some type := view.type? then + throwErrorAt type "Invalid field: Uexpected type for field `{view.name}` when setting auto-param tactic for inherited field" + unless view.binders.getArgs.isEmpty do + throwErrorAt view.binders "Invalid field: Unexpected binders for field `{view.name}` when setting auto-param tactic for inherited field" + withExporting (isExporting := wasExporting) do + go (i+1) else k +/-- +Elaborates the field defaults, with all the fields in scope. + +The behavior is slightly different between new fields and inherited fields: +- New fields: We re-enter the binders elaborated in `elabFieldType`, then elaborate the value. +- Inherited fields: We wrap the value in `fun` syntax to make use of the binders, then elaborate that. + +For inherited fields, we have already checked +-/ +private def elabStructFieldDefaults (views : Array StructFieldView) : StructElabM Unit := do + for view in views do + if let some defaultView := view.default? then + withoutExporting (when := isPrivateName view.declName) do + withRef view.ref do + let some info ← findFieldInfo? view.name | unreachable! + if info.default?.isSome then + throwExistingDefaultValue info.name + match defaultView with + | .optParam valStx => + let type ← inferType info.fvar + let value ← + if info.kind.isFromSubobject then + let mut valStx := valStx + if let some fieldType := view.type? then + valStx ← `(($valStx:term : $fieldType:term)) + let binders := view.binders.getArgs + if binders.size > 0 then + valStx ← `(fun $binders* => $valStx:term) + Term.elabTermEnsuringType valStx type + else + forallBoundedTelescope type info.numBinders fun xs type => do + let value ← Term.elabTermEnsuringType valStx type + mkLambdaFVars xs value + solveParentMVars value + registerFailedToInferDefaultValue view.name value valStx + replaceFieldInfo { info with default? := StructFieldDefault.optParam value } + | .autoParam tacticStx => + let name := mkAutoParamFnOfProjFn view.declName + discard <| Term.declareTacticSyntax tacticStx name + replaceFieldInfo { info with default? := StructFieldDefault.autoParam (.const name []) } + private def collectUsedFVars (lctx : LocalContext) (localInsts : LocalInstances) (fieldInfos : Array StructFieldInfo) : StateRefT CollectFVars.State MetaM Unit := do withLCtx lctx localInsts do @@ -1345,18 +1355,19 @@ private def addDefaults (levelParams : List Name) (params : Array Expr) (replace let parentFVarIds := fieldInfos |>.filter (·.kind.isParent) |>.map (·.fvar.fvarId!) let fields := fieldInfos |>.filter (!·.kind.isParent) withLCtx lctx (← getLocalInstances) do - let addDefault (declName : Name) (value : Expr) : StructElabM Unit := do + let addDefault (thisFieldInfo : StructFieldInfo) (declName : Name) (value : Expr) : StructElabM Unit := do let value ← instantiateMVars value -- If there are mvars, `checkDefaults` already logged an error. unless value.hasMVar || value.hasSyntheticSorry do - /- The identity function is used as "marker". -/ - let value ← mkId value let value ← zetaDeltaFVars value parentFVarIds - let value ← fields.foldrM (init := value) fun fieldInfo val => do + /- The identity function is used as "marker". -/ + let value ← fields.foldrM (init := ← mkId value) fun fieldInfo val => do let decl ← fieldInfo.fvar.fvarId!.getDecl let type ← zetaDeltaFVars decl.type parentFVarIds let val' := val.abstract #[fieldInfo.fvar] if val'.hasLooseBVar 0 then + if fieldInfo.fvar == thisFieldInfo.fvar then + logErrorAt thisFieldInfo.ref m!"Default value for field `{thisFieldInfo.name}` will never be applied since it contains the field itself:{indentExpr value}" return .lam decl.userName type val' .default else return val @@ -1372,9 +1383,9 @@ private def addDefaults (levelParams : List Name) (params : Array Expr) (replace for fieldInfo in fieldInfos do if let some (.optParam value) := fieldInfo.default? then withoutExporting (when := isPrivateName fieldInfo.declName) do - addDefault (mkDefaultFnOfProjFn fieldInfo.declName) value + addDefault fieldInfo (mkDefaultFnOfProjFn fieldInfo.declName) value else if let some (.optParam value) := fieldInfo.resolvedDefault? then - addDefault (mkInheritedDefaultFnOfProjFn fieldInfo.declName) value + addDefault fieldInfo (mkInheritedDefaultFnOfProjFn fieldInfo.declName) value /-- Given `type` of the form `forall ... (source : A), B`, return `forall ... [source : A], B`. @@ -1511,6 +1522,7 @@ def elabStructureCommand : InductiveElabDescr where withParents view rs r.indFVar do withFields params view.fields do withRef view.ref do + elabStructFieldDefaults view.fields Term.synthesizeSyntheticMVarsNoPostponing resolveFieldDefaults view.declName let state ← get diff --git a/tests/elab/struct3.lean b/tests/elab/struct3.lean index c547a806d3b1..864fce91a607 100644 --- a/tests/elab/struct3.lean +++ b/tests/elab/struct3.lean @@ -20,3 +20,16 @@ class Monad4 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, seq f x := Bind2.bind f fun y => Functor.map y (x ()) seqLeft x y := Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a seqRight x y := Bind2.bind x fun _ => y () + +/-! +Can provide type signatures when setting defaults of inherited fields. +-/ +class Monad5 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind2 m where + map {α β} (f : α → β) (x : m α) : m β := + Bind2.bind x (pure ∘ f) + seq {α β} (f : m (α → β)) (x : Unit -> m α) : m β := + Bind2.bind f fun y => Functor.map y (x ()) + seqLeft {α β} (x : m α) (y : Unit → m β) := + Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a + seqRight {α β} (x : m α) (y : Unit → m β) := + Bind2.bind x fun _ => y () diff --git a/tests/elab/structureElab.lean b/tests/elab/structureElab.lean index 0a49f85cc3f6..8e9f57398834 100644 --- a/tests/elab/structureElab.lean +++ b/tests/elab/structureElab.lean @@ -449,41 +449,108 @@ structure S4 extends S2, S3 end TestO2 +namespace TestOptParam + +/-! +All fields are in scope when elaborating default values. +-/ +structure Loop where + x : Nat := y + y : Nat := x + deriving Repr + +/-- info: { x := 1, y := 1 } -/ +#guard_msgs in #eval { x := 1 : Loop } +/-- info: { x := 2, y := 2 } -/ +#guard_msgs in #eval { y := 2 : Loop } +/-- info: { x := 1, y := 2 } -/ +#guard_msgs in #eval { x := 1, y := 2 : Loop } + +/-! +Testing a loop that goes through the parent structure. +-/ +structure Base where + x : Nat + y : Nat := x + deriving Repr +structure Loop2 extends Base where + x := y + deriving Repr +/-- info: { toBase := { x := 1, y := 1 } } -/ +#guard_msgs in #eval { x := 1 : Loop2 } +/-- info: { toBase := { x := 2, y := 2 } } -/ +#guard_msgs in #eval { y := 2 : Loop2 } + +/-! +Restating the type of an inherited field is OK +-/ +structure RestateType extends Base where + x : Nat := 1 + deriving Repr +/-- info: { toBase := { x := 1, y := 1 } } -/ +#guard_msgs in #eval { : RestateType } + +/-! +Restating the type of an inherited field is a valid +way to change the binder names. +-/ +structure A (m : Type → Type) where + map (f : α → β) : m α → m β +structure A' extends A List where + map {α β} (g : α → β) (xs : List α) : List β := List.map g xs + +/-- info: A'.mk (A.mk fun {α β} g xs => List.map g xs) : A' -/ +#guard_msgs in #check { : A'} + +/-- +error: Default value for field `x` will never be applied since it contains the field itself: + x + 1 +-/ +#guard_msgs in +structure InapplicableDefault where + x : Nat := x + 1 + +end TestOptParam + /-! Some failures from unsupported autoparams -/ namespace TestFail1 -/-- error: Invalid field declaration: Type must be provided when auto-param tactic is used -/ +/-- error: Failed to infer type of field `x` -/ #guard_msgs in structure F1 where x := by exact 0 structure F2 where x (n : Nat) : Nat -/-- error: Omit the type of field `x` to set its auto-param tactic -/ +/-- +error: Invalid field: Uexpected type for field `x` when setting auto-param tactic for inherited field +-/ #guard_msgs in structure F3 extends F2 where x : Nat → Nat := by exact 0 -/-- error: Invalid field: Unexpected binders when setting auto-param tactic for inherited field -/ +/-- +error: Invalid field: Unexpected binders for field `x` when setting auto-param tactic for inherited field +-/ #guard_msgs in structure F4 extends F2 where x (n : Nat) := by exact 0 -/-- error: A new default value for field `x` has already been set in this structure -/ +/-- error: A default value for field `x` has already been set for this structure -/ #guard_msgs in structure F5 extends F2 where x := by exact 0 x := by exact 0 -/-- error: A new default value for field `x` has already been set in this structure -/ +/-- error: A default value for field `x` has already been set for this structure -/ #guard_msgs in structure F6 extends F2 where x := id x := by exact 0 -/-- error: A new default value for field `x` has already been set in this structure -/ +/-- error: A default value for field `x` has already been set for this structure -/ #guard_msgs in structure F7 extends F2 where x := by exact 0 diff --git a/tests/elab_fail/struct1.lean b/tests/elab_fail/struct1.lean index 95fd8c9c2d53..a3568fab514f 100644 --- a/tests/elab_fail/struct1.lean +++ b/tests/elab_fail/struct1.lean @@ -36,22 +36,22 @@ structure S' extends A Nat where (x := true) -- error type mismatch structure S extends A Nat where -(x : Bool := true) -- error omit type +(x : Bool := true) -- error type mismatch structure S'' where (x : Nat := true) -- error type mismatch -private structure S where +private structure Spriv where private mk :: (x : Nat) -private structure S where +private structure Spriv where protected mk :: (x : Nat) -private structure S where +private structure Spriv where protected (x : Nat) -private structure S where +private structure Spriv where mk2 :: (x : Nat) -#check S +#check Spriv #check S.mk2 diff --git a/tests/elab_fail/struct1.lean.out.expected b/tests/elab_fail/struct1.lean.out.expected index 7032d3761fc7..e4da83a2fce8 100644 --- a/tests/elab_fail/struct1.lean.out.expected +++ b/tests/elab_fail/struct1.lean.out.expected @@ -21,7 +21,12 @@ has type Bool but is expected to have type Nat -struct1.lean:39:5-39:9: error: Omit the type of field `x` to set its default value +struct1.lean:39:1-39:2: error: Type mismatch + true +has type + Bool +but is expected to have type + Nat struct1.lean:42:12-42:16: error: Type mismatch true has type @@ -34,5 +39,5 @@ Hint: Remove `private` modifier from constructor p̵r̵i̵v̵a̵t̵e̵ ̵mk :: struct1.lean:48:0-48:15: error: Constructor cannot be `protected` because this structure is `private` struct1.lean:51:0-51:19: error: Field cannot be marked `protected` because this structure is `private` -S : Type -S.mk2 (x : Nat) : S +Spriv : Type +struct1.lean:57:7-57:12: error(lean.unknownIdentifier): Unknown constant `S.mk2` diff --git a/tests/elab_fail/structDefValueOverride.lean.out.expected b/tests/elab_fail/structDefValueOverride.lean.out.expected index ef2bd4f2ffa3..ba00cfc6cfb3 100644 --- a/tests/elab_fail/structDefValueOverride.lean.out.expected +++ b/tests/elab_fail/structDefValueOverride.lean.out.expected @@ -1 +1 @@ -structDefValueOverride.lean:6:2-6:3: error: A new default value for field `x` has already been set in this structure +structDefValueOverride.lean:6:2-6:3: error: A default value for field `x` has already been set for this structure From 32be33be06de1d1b9ee33dfc0a3373e2ddacccd3 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 8 Mar 2026 16:05:55 -0700 Subject: [PATCH 2/3] remove dependencies from local context --- src/Lean/Elab/Structure.lean | 9 +++-- tests/elab/structureElab.lean | 34 ++++++++++++++++--- .../mvarAtDefaultValue.lean.out.expected | 2 -- 3 files changed, 37 insertions(+), 8 deletions(-) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 502757e4684f..64c8ac62b480 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -1083,7 +1083,7 @@ The behavior is slightly different between new fields and inherited fields: - New fields: We re-enter the binders elaborated in `elabFieldType`, then elaborate the value. - Inherited fields: We wrap the value in `fun` syntax to make use of the binders, then elaborate that. -For inherited fields, we have already checked +For inherited fields, we have already done checks that the binders and types are suitable. -/ private def elabStructFieldDefaults (views : Array StructFieldView) : StructElabM Unit := do for view in views do @@ -1096,8 +1096,12 @@ private def elabStructFieldDefaults (views : Array StructFieldView) : StructElab match defaultView with | .optParam valStx => let type ← inferType info.fvar - let value ← + -- Prevent default values from being able to refer to the field itself, + -- since such recursive default values cannot be applied. + let fieldDeps ← collectForwardDeps #[info.fvar] (preserveOrder := false) + let value ← withErasedFVars (fieldDeps.map (·.fvarId!)) do if info.kind.isFromSubobject then + -- Inherited field. Use `fun` to elaborate binders. let mut valStx := valStx if let some fieldType := view.type? then valStx ← `(($valStx:term : $fieldType:term)) @@ -1106,6 +1110,7 @@ private def elabStructFieldDefaults (views : Array StructFieldView) : StructElab valStx ← `(fun $binders* => $valStx:term) Term.elabTermEnsuringType valStx type else + -- New field. Use the pre-elaborated binders. forallBoundedTelescope type info.numBinders fun xs type => do let value ← Term.elabTermEnsuringType valStx type mkLambdaFVars xs value diff --git a/tests/elab/structureElab.lean b/tests/elab/structureElab.lean index 8e9f57398834..b9d69c76067b 100644 --- a/tests/elab/structureElab.lean +++ b/tests/elab/structureElab.lean @@ -502,14 +502,40 @@ structure A' extends A List where /-- info: A'.mk (A.mk fun {α β} g xs => List.map g xs) : A' -/ #guard_msgs in #check { : A'} -/-- -error: Default value for field `x` will never be applied since it contains the field itself: - x + 1 +/-! +Default values cannot refer to the field. -/ +/-- error: Unknown identifier `x` -/ #guard_msgs in -structure InapplicableDefault where +structure InapplicableDefault1 where x : Nat := x + 1 +/-! +Default values can refer to later fields. +-/ +structure ApplicableDefault2 where + x : Nat := y + 1 + y : Fin 2 + +/-! +Default values cannot refer to later fields if they depend on the field. +-/ +/-- error: Unknown identifier `y` -/ +#guard_msgs in +structure InpplicableDefault3 where + x : Nat := y + 1 + y : Fin x + +/-! +Default values cannot refer to the field, even for inherited fields. +-/ +structure Base2 where + x : Nat +/-- error: Unknown identifier `x` -/ +#guard_msgs in +structure InapplicableDefault2 extends Base2 where + x := x + end TestOptParam /-! diff --git a/tests/elab_fail/mvarAtDefaultValue.lean.out.expected b/tests/elab_fail/mvarAtDefaultValue.lean.out.expected index 8a312701e066..2746fb1b4f05 100644 --- a/tests/elab_fail/mvarAtDefaultValue.lean.out.expected +++ b/tests/elab_fail/mvarAtDefaultValue.lean.out.expected @@ -1,6 +1,4 @@ mvarAtDefaultValue.lean:5:7-5:8: error: Failed to infer default value for field `x` mvarAtDefaultValue.lean:8:7-8:8: error: don't know how to synthesize placeholder context: -x : Nat -toA : A := ⋯ ⊢ Nat From ad8fa9c419295a223024e24ac43743ef67eca41d Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 8 Mar 2026 16:12:04 -0700 Subject: [PATCH 3/3] remove cycle check --- src/Lean/Elab/Structure.lean | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 64c8ac62b480..531fe04444e7 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -1360,19 +1360,18 @@ private def addDefaults (levelParams : List Name) (params : Array Expr) (replace let parentFVarIds := fieldInfos |>.filter (·.kind.isParent) |>.map (·.fvar.fvarId!) let fields := fieldInfos |>.filter (!·.kind.isParent) withLCtx lctx (← getLocalInstances) do - let addDefault (thisFieldInfo : StructFieldInfo) (declName : Name) (value : Expr) : StructElabM Unit := do + let addDefault (declName : Name) (value : Expr) : StructElabM Unit := do let value ← instantiateMVars value -- If there are mvars, `checkDefaults` already logged an error. unless value.hasMVar || value.hasSyntheticSorry do - let value ← zetaDeltaFVars value parentFVarIds /- The identity function is used as "marker". -/ - let value ← fields.foldrM (init := ← mkId value) fun fieldInfo val => do + let value ← mkId value + let value ← zetaDeltaFVars value parentFVarIds + let value ← fields.foldrM (init := value) fun fieldInfo val => do let decl ← fieldInfo.fvar.fvarId!.getDecl let type ← zetaDeltaFVars decl.type parentFVarIds let val' := val.abstract #[fieldInfo.fvar] if val'.hasLooseBVar 0 then - if fieldInfo.fvar == thisFieldInfo.fvar then - logErrorAt thisFieldInfo.ref m!"Default value for field `{thisFieldInfo.name}` will never be applied since it contains the field itself:{indentExpr value}" return .lam decl.userName type val' .default else return val @@ -1388,9 +1387,9 @@ private def addDefaults (levelParams : List Name) (params : Array Expr) (replace for fieldInfo in fieldInfos do if let some (.optParam value) := fieldInfo.default? then withoutExporting (when := isPrivateName fieldInfo.declName) do - addDefault fieldInfo (mkDefaultFnOfProjFn fieldInfo.declName) value + addDefault (mkDefaultFnOfProjFn fieldInfo.declName) value else if let some (.optParam value) := fieldInfo.resolvedDefault? then - addDefault fieldInfo (mkInheritedDefaultFnOfProjFn fieldInfo.declName) value + addDefault (mkInheritedDefaultFnOfProjFn fieldInfo.declName) value /-- Given `type` of the form `forall ... (source : A), B`, return `forall ... [source : A], B`.