max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: public structures with private field types under the module system (#10109)

Browse source 
Fixes #10099
This commit is contained in:
Sebastian Ullrich 2025-08-25 16:48:23 +02:00 • committed by GitHub
parent 1718ca21cd
commit 321af0e02b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 77 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/Lean/Elab/MutualInductive.lean
View file

@ -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

17
src/Lean/Elab/Structure.lean
View file

@ -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

79
src/Lean/Meta/Structure.lean
View file

@ -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

4
src/Lean/Parser/Basic.lean
View file

@ -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

8
tests/pkg/module/Module/Basic.lean
View file

@ -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