From 321af0e02b46925002adf0c871fcb705311e6383 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 25 Aug 2025 16:48:23 +0200 Subject: [PATCH] fix: public structures with private field types under the module system (#10109) Fixes #10099 --- src/Lean/Elab/MutualInductive.lean | 29 ++++++----- src/Lean/Elab/Structure.lean | 17 +++++-- src/Lean/Meta/Structure.lean | 79 +++++++++++++++--------------- src/Lean/Parser/Basic.lean | 4 +- tests/pkg/module/Module/Basic.lean | 8 +-- 5 files changed, 77 insertions(+), 60 deletions(-) diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index e4a50df24b..936ae8bc10 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -905,13 +905,16 @@ private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep let numVars := vars.size let numParams := numVars + numExplicitParams let indTypes ← updateParams vars indTypes + -- allow general access to private data for steps that do no elaboration let indTypes ← - if let some univToInfer := univToInfer? then - updateResultingUniverse views numParams (← levelMVarToParam indTypes univToInfer) - else - propagateUniversesToConstructors numParams indTypes - levelMVarToParam indTypes none - checkResultingUniverses views elabs' numParams indTypes + withoutExporting do + if let some univToInfer := univToInfer? then + updateResultingUniverse views numParams (← levelMVarToParam indTypes univToInfer) + else + propagateUniversesToConstructors numParams indTypes + levelMVarToParam indTypes none + withoutExporting do + checkResultingUniverses views elabs' numParams indTypes elabs'.forM fun elab' => elab'.finalizeTermElab let usedLevelNames := collectLevelParamsInInductive indTypes match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with @@ -985,12 +988,14 @@ private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabS Term.withDeclName view0.declName do withRef ref do withExporting (isExporting := !isPrivateName view0.declName) do let res ← mkInductiveDecl vars elabs - mkAuxConstructions (elabs.map (·.view.declName)) - unless view0.isClass do - mkSizeOfInstances view0.declName - IndPredBelow.mkBelow view0.declName - for e in elabs do - mkInjectiveTheorems e.view.declName + -- This might be too coarse, consider reconsidering on construction-by-construction basis + withoutExporting (when := view0.ctors.any (isPrivateName ·.declName)) do + mkAuxConstructions (elabs.map (·.view.declName)) + unless view0.isClass do + mkSizeOfInstances view0.declName + IndPredBelow.mkBelow view0.declName + for e in elabs do + mkInjectiveTheorems e.view.declName for e in elabs do enableRealizationsForConst e.view.declName return res diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 2dadf3e883..e7febcfdcf 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -1036,6 +1036,10 @@ where go (i : Nat) : StructElabM α := do if h : i < views.size then let view := views[i] + -- `withLocalDecl` may need access to private data in case of private fields but we recurse + -- for further fields inside of it, so save and later restore exporting flag + let wasExporting := (← getEnv).isExporting + withoutExporting (when := isPrivateName view.declName) do withRef view.ref do if let some parent := (← get).parents.find? (·.name == view.name) then throwError "Field `{view.name}` has already been declared as a projection for parent `{.ofConstName parent.structName}`" @@ -1050,7 +1054,8 @@ where name := view.name, declName := view.declName, fvar := fieldFVar, default? := default?, binfo := view.binderInfo, paramInfoOverrides, kind := StructFieldKind.newField } - go (i+1) + withExporting (isExporting := wasExporting) do + go (i+1) | none, some (.optParam value) => let type ← inferType value withLocalDecl view.rawName view.binderInfo type fun fieldFVar => do @@ -1058,7 +1063,8 @@ where name := view.name, declName := view.declName, fvar := fieldFVar, default? := default?, binfo := view.binderInfo, paramInfoOverrides, kind := StructFieldKind.newField } - go (i+1) + withExporting (isExporting := wasExporting) do + go (i+1) | none, some (.autoParam _) => throwError "Field `{view.name}` has an auto-param but no type" | some info => @@ -1084,7 +1090,8 @@ where 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 } - go (i+1) + 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" @@ -1098,7 +1105,8 @@ where 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) - go (i+1) + withExporting (isExporting := wasExporting) do + go (i+1) match info.kind with | StructFieldKind.newField => throwError "Field `{view.name}` has already been declared" | StructFieldKind.subobject n @@ -1165,6 +1173,7 @@ private def mkCtorLCtx : StructElabM LocalContext := do Builds a constructor for the type, for adding the inductive type to the environment. -/ private def mkCtor (view : StructView) (r : ElabHeaderResult) (params : Array Expr) : StructElabM Constructor := + withoutExporting (when := isPrivateName view.ctor.declName) do withRef view.ref do let (binders, paramInfoOverrides) ← elabParamInfoUpdates params view.ctor.binders.getArgs unless binders.isEmpty do diff --git a/src/Lean/Meta/Structure.lean b/src/Lean/Meta/Structure.lean index a3a0ae1107..a025ce82b5 100644 --- a/src/Lean/Meta/Structure.lean +++ b/src/Lean/Meta/Structure.lean @@ -80,45 +80,46 @@ def mkProjections (n : Name) (projDecls : Array StructProjDecl) (instImplicit : let mut ctorType := ctorType for h : i in *...projDecls.size do let {ref, projName, paramInfoOverrides} := projDecls[i] - unless ctorType.isForall do - throwErrorAt ref "\ - failed to generate projection '{projName}' for '{.ofConstName n}', \ - not enough constructor fields" - unless paramInfoOverrides.length ≤ params.size do - throwErrorAt ref "\ - failed to generate projection '{projName}' for '{.ofConstName n}', \ - too many structure parameter overrides" - let resultType := ctorType.bindingDomain!.consumeTypeAnnotations - let isProp ← isProp resultType - if isPredicate && !isProp then - throwErrorAt ref "\ - failed to generate projection '{projName}' for the 'Prop'-valued type '{.ofConstName n}', \ - field must be a proof, but it has type\ - {indentExpr resultType}" - let projType := lctx.mkForall projArgs resultType - let projType := projType.inferImplicit indVal.numParams (considerRange := true) - let projType := projType.updateForallBinderInfos paramInfoOverrides - let projVal := lctx.mkLambda projArgs <| Expr.proj n i self - let cval : ConstantVal := { name := projName, levelParams := indVal.levelParams, type := projType } - withRef ref do - if isProp then - let env ← getEnv - addDecl <| - if env.hasUnsafe projType || env.hasUnsafe projVal then - -- Theorems cannot be unsafe, using opaque instead. - Declaration.opaqueDecl { cval with value := projVal, isUnsafe := true } - else - Declaration.thmDecl { cval with value := projVal } - else - let decl ← mkDefinitionValInferringUnsafe projName indVal.levelParams projType projVal ReducibilityHints.abbrev - -- Projections have special compiler support. No need to compile. - addDecl <| Declaration.defnDecl decl - -- Recall: we want instance projections to be in "reducible canonical form" - if !instImplicit then - setReducibleAttribute projName - modifyEnv fun env => addProjectionFnInfo env projName ctorVal.name indVal.numParams i instImplicit - let proj := mkApp (mkAppN (.const projName lvls) params) self - ctorType := ctorType.bindingBody!.instantiate1 proj + ctorType ← withoutExporting (when := isPrivateName projName) do + unless ctorType.isForall do + throwErrorAt ref "\ + failed to generate projection '{projName}' for '{.ofConstName n}', \ + not enough constructor fields" + unless paramInfoOverrides.length ≤ params.size do + throwErrorAt ref "\ + failed to generate projection '{projName}' for '{.ofConstName n}', \ + too many structure parameter overrides" + let resultType := ctorType.bindingDomain!.consumeTypeAnnotations + let isProp ← isProp resultType + if isPredicate && !isProp then + throwErrorAt ref "\ + failed to generate projection '{projName}' for the 'Prop'-valued type '{.ofConstName n}', \ + field must be a proof, but it has type\ + {indentExpr resultType}" + let projType := lctx.mkForall projArgs resultType + let projType := projType.inferImplicit indVal.numParams (considerRange := true) + let projType := projType.updateForallBinderInfos paramInfoOverrides + let projVal := lctx.mkLambda projArgs <| Expr.proj n i self + let cval : ConstantVal := { name := projName, levelParams := indVal.levelParams, type := projType } + withRef ref do + if isProp then + let env ← getEnv + addDecl <| + if env.hasUnsafe projType || env.hasUnsafe projVal then + -- Theorems cannot be unsafe, using opaque instead. + Declaration.opaqueDecl { cval with value := projVal, isUnsafe := true } + else + Declaration.thmDecl { cval with value := projVal } + else + let decl ← mkDefinitionValInferringUnsafe projName indVal.levelParams projType projVal ReducibilityHints.abbrev + -- Projections have special compiler support. No need to compile. + addDecl <| Declaration.defnDecl decl + -- Recall: we want instance projections to be in "reducible canonical form" + if !instImplicit then + setReducibleAttribute projName + modifyEnv fun env => addProjectionFnInfo env projName ctorVal.name indVal.numParams i instImplicit + let proj := mkApp (mkAppN (.const projName lvls) params) self + return ctorType.bindingBody!.instantiate1 proj /-- Checks if the expression is of the form `S.mk x.1 ... x.n` with `n` nonzero diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index c780f38454..024cb8f739 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1013,8 +1013,8 @@ private def tokenFnAux : ParserFn := fun c s => rawStrLitFnAux i c (s.next c i) else let tk := c.tokens.matchPrefix c.inputString i c.endPos.byteIdx <| by - let ⟨⟨{inputString, endPos := ⟨endPos⟩, endPos_valid, ..}, _, _, _⟩⟩ := c - rw [String.endPos] at endPos_valid + have := c.endPos_valid + rw [String.endPos] at this omega identFnAux i tk .anonymous c s diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 6c1041ba44..ff2848cd8e 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -254,16 +254,18 @@ info: theorem f_exp_wfrec.eq_unfold : f_exp_wfrec = fun x x_1 => /-! Private fields should force private ctors. -/ +abbrev Priv := Nat + public structure StructWithPrivateField where - private x : Nat + private x : Priv /-- info: structure StructWithPrivateField : Type number of parameters: 0 fields: - private StructWithPrivateField.x : Nat + private StructWithPrivateField.x : Priv constructor: - private StructWithPrivateField.mk (x : Nat) : StructWithPrivateField + private StructWithPrivateField.mk (x : Priv) : StructWithPrivateField -/ #guard_msgs in #print StructWithPrivateField