From 2f5c7d0465c8038f039192760e9adc6c9d8250e0 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 23 Nov 2024 20:22:39 -0800 Subject: [PATCH] fix: structures with copied parents can now use other parents as instances (#6175) This PR fixes a bug with the `structure`/`class` command where if there are parents that are not represented as subobjects but which used other parents as instances, then there would be a kernel error. Closes #2611. Note: there is still the limitation that parents that are not represented as subobjects do not themselves provide instances to other parents. --- src/Lean/Elab/Structure.lean | 123 ++++++++++++++++++++--------------- tests/lean/run/2611.lean | 50 ++++++++++++++ 2 files changed, 121 insertions(+), 52 deletions(-) create mode 100644 tests/lean/run/2611.lean diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 1eecec16d4a1..557a8b22991f 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -285,7 +285,7 @@ private def findExistingField? (infos : Array StructFieldInfo) (parentStructName return some fieldName return none -private partial def processSubfields (structDeclName : Name) (parentFVar : Expr) (parentStructName : Name) (subfieldNames : Array Name) +private def processSubfields (structDeclName : Name) (parentFVar : Expr) (parentStructName : Name) (subfieldNames : Array Name) (infos : Array StructFieldInfo) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := go 0 infos where @@ -506,7 +506,7 @@ private partial def mkToParentName (parentStructName : Name) (p : Name → Bool) if p curr then curr else go (i+1) go 1 -private partial def withParents (view : StructView) (rs : Array ElabHeaderResult) (indFVar : Expr) +private def withParents (view : StructView) (rs : Array ElabHeaderResult) (indFVar : Expr) (k : Array StructFieldInfo → Array StructParentInfo → TermElabM α) : TermElabM α := do go 0 #[] #[] where @@ -775,57 +775,81 @@ private def setSourceInstImplicit (type : Expr) : Expr := /-- Creates a projection function to a non-subobject parent. -/ -private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (parentStructName : Name) (parentType : Expr) : MetaM StructureParentInfo := do +private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (source : Expr) (parentStructName : Name) (parentType : Expr) : MetaM StructureParentInfo := do let isProp ← Meta.isProp parentType let env ← getEnv let structName := view.declName let sourceFieldNames := getStructureFieldsFlattened env structName - let structType := mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default + let mut declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType)) + if view.isClass && isClass env parentStructName then + declType := setSourceInstImplicit declType + declType := declType.inferImplicit params.size true + let rec copyFields (parentType : Expr) : MetaM Expr := do + let Expr.const parentStructName us ← pure parentType.getAppFn | unreachable! + let parentCtor := getStructureCtor env parentStructName + let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs + for fieldName in getStructureFields env parentStructName do + if sourceFieldNames.contains fieldName then + let fieldVal ← mkProjection source fieldName + result := mkApp result fieldVal + else + -- fieldInfo must be a field of `parentStructName` + let some fieldInfo := getFieldInfo? env parentStructName fieldName | unreachable! + if fieldInfo.subobject?.isNone then throwError "failed to build coercion to parent structure" + let resultType ← whnfD (← inferType result) + unless resultType.isForall do throwError "failed to build coercion to parent structure, unexpected type{indentExpr resultType}" + let fieldVal ← copyFields resultType.bindingDomain! + result := mkApp result fieldVal + return result + let declVal ← instantiateMVars (← mkLambdaFVars params (← mkLambdaFVars #[source] (← copyFields parentType))) + let declName := structName ++ mkToParentName (← getStructureName parentType) fun n => !env.contains (structName ++ n) + -- Logic from `mk_projections`: prop-valued projections are theorems (or at least opaque) + let cval : ConstantVal := { name := declName, levelParams, type := declType } + if isProp then + addDecl <| + if view.modifiers.isUnsafe then + -- Theorems cannot be unsafe. + Declaration.opaqueDecl { cval with value := declVal, isUnsafe := true } + else + Declaration.thmDecl { cval with value := declVal } + else + addAndCompile <| Declaration.defnDecl { cval with + value := declVal + hints := ReducibilityHints.abbrev + safety := if view.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe + } + -- Logic from `mk_projections`: non-instance-implicits that aren't props become reducible. + -- (Instances will get instance reducibility in `Lean.Elab.Command.addParentInstances`.) + if !binfo.isInstImplicit && !(← Meta.isProp parentType) then + setReducibleAttribute declName + return { structName := parentStructName, subobject := false, projFn := declName } + +private def mkRemainingProjections (levelParams : List Name) (params : Array Expr) (view : StructView) + (parents : Array StructParentInfo) (fieldInfos : Array StructFieldInfo) : TermElabM (Array StructureParentInfo) := do + let structType := mkAppN (Lean.mkConst view.declName (levelParams.map mkLevelParam)) params withLocalDeclD `self structType fun source => do - let mut declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType)) - if view.isClass && isClass env parentStructName then - declType := setSourceInstImplicit declType - declType := declType.inferImplicit params.size true - let rec copyFields (parentType : Expr) : MetaM Expr := do - let Expr.const parentStructName us ← pure parentType.getAppFn | unreachable! - let parentCtor := getStructureCtor env parentStructName - let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs - for fieldName in getStructureFields env parentStructName do - if sourceFieldNames.contains fieldName then - let fieldVal ← mkProjection source fieldName - result := mkApp result fieldVal + /- + Remark: copied parents might still be referring to the fvars of other parents. We need to replace these fvars with projection constants. + For subobject parents, this has already been done by `mkProjections`. + https://github.com/leanprover/lean4/issues/2611 + -/ + let mut parentInfos := #[] + let mut parentFVarToConst : ExprMap Expr := {} + for h : i in [0:parents.size] do + let parent := parents[i] + let parentInfo : StructureParentInfo ← (do + if parent.subobject then + let some info := fieldInfos.find? (·.kind == .subobject parent.structName) | unreachable! + pure { structName := parent.structName, subobject := true, projFn := info.declName } else - -- fieldInfo must be a field of `parentStructName` - let some fieldInfo := getFieldInfo? env parentStructName fieldName | unreachable! - if fieldInfo.subobject?.isNone then throwError "failed to build coercion to parent structure" - let resultType ← whnfD (← inferType result) - unless resultType.isForall do throwError "failed to build coercion to parent structure, unexpected type{indentExpr resultType}" - let fieldVal ← copyFields resultType.bindingDomain! - result := mkApp result fieldVal - return result - let declVal ← instantiateMVars (← mkLambdaFVars params (← mkLambdaFVars #[source] (← copyFields parentType))) - let declName := structName ++ mkToParentName (← getStructureName parentType) fun n => !env.contains (structName ++ n) - -- Logic from `mk_projections`: prop-valued projections are theorems (or at least opaque) - let cval : ConstantVal := { name := declName, levelParams, type := declType } - if isProp then - addDecl <| - if view.modifiers.isUnsafe then - -- Theorems cannot be unsafe. - Declaration.opaqueDecl { cval with value := declVal, isUnsafe := true } - else - Declaration.thmDecl { cval with value := declVal } - else - addAndCompile <| Declaration.defnDecl { cval with - value := declVal - hints := ReducibilityHints.abbrev - safety := if view.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe - } - -- Logic from `mk_projections`: non-instance-implicits that aren't props become reducible. - -- (Instances will get instance reducibility in `Lean.Elab.Command.addParentInstances`.) - if !binfo.isInstImplicit && !(← Meta.isProp parentType) then - setReducibleAttribute declName - return { structName := parentStructName, subobject := false, projFn := declName } + let parent_type := (← instantiateMVars parent.type).replace fun e => parentFVarToConst[e]? + mkCoercionToCopiedParent levelParams params view source parent.structName parent_type) + parentInfos := parentInfos.push parentInfo + if let some fvar := parent.fvar? then + parentFVarToConst := parentFVarToConst.insert fvar <| + mkApp (mkAppN (.const parentInfo.projFn (levelParams.map mkLevelParam)) params) source + pure parentInfos /-- Precomputes the structure's resolution order. @@ -887,12 +911,7 @@ def elabStructureCommand : InductiveElabDescr where if (← getEnv).contains field.declName then Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true) finalize := fun levelParams params replaceIndFVars => do - let parentInfos ← parents.mapM fun parent => do - if parent.subobject then - let some info := fieldInfos.find? (·.kind == .subobject parent.structName) | unreachable! - pure { structName := parent.structName, subobject := true, projFn := info.declName } - else - mkCoercionToCopiedParent levelParams params view parent.structName parent.type + let parentInfos ← mkRemainingProjections levelParams params view parents fieldInfos setStructureParents view.declName parentInfos checkResolutionOrder view.declName if view.isClass then diff --git a/tests/lean/run/2611.lean b/tests/lean/run/2611.lean new file mode 100644 index 000000000000..254925e9a23f --- /dev/null +++ b/tests/lean/run/2611.lean @@ -0,0 +1,50 @@ +/-! +# Structure copied parents should be able to refer to other parents as instances +Issue: https://github.com/leanprover/lean4/issues/2611 +-/ + +/-! +Example that worked before the fixes for 2611. The projection `D.toC` refers to `D.toA` for the `A` instance. +This is a natural consequence to the way subobject projection functions are added by `mkProjections`. +-/ +class A +class C [A] +class D extends A, C + +/-! +This example did not work. Since `C` provides a `B` field, it's a copied parent. +Now there is a step where the fvar for the `A` instance is replaced by the `D.toA` constant. +-/ +namespace Ex2 +class A +class B +class C [A] extends B +class D extends A, B, C +end Ex2 + +/-! +A test that this still works even when there are parameters on the structure. +-/ +namespace Ex3 +class A where + x : Nat +class B [A] where + x : Nat +class C (α : Type) extends A, B where + y : α +/-- info: Ex3.C.toB {α : Type} [self : C α] : @B (@C.toA α self) -/ +#guard_msgs in set_option pp.explicit true in #check C.toB +end Ex3 + +/-! +A test that this still works even when there are parameters on the parents. +-/ +namespace Ex4 +class A (n : Nat) where + x : Nat +class B (n : Nat) [A n] where + x : Nat +class C extends A 3, B 3 +/-- info: Ex4.C.toB [self : C] : @B (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@C.toA self) -/ +#guard_msgs in set_option pp.explicit true in #check C.toB +end Ex4