From 6cf22b32aac7ec4e899e7b73416c6cb2089fc345 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 23 Jul 2025 09:33:34 -0700 Subject: [PATCH] feat: custom `structure` constructors can update binder kinds of parameters (#9480) This PR adds a feature where `structure` constructors can override the inferred binder kinds of the type's parameters. In the following, the `(p)` binder on `toLp` causes `p` to be an explicit parameter to `WithLp.toLp`: ```lean structure WithLp (p : Nat) (V : Type) where toLp (p) :: ofLp : V ``` This reflects the syntax of the feature added in #7742 for overriding binder kinds of structure projections. Similarly, only those parameters in the header of the `structure` may be updated; it is an error to try to update binder kinds of parameters included via `variable`. Closes #9072. Fixes a possible bug from stale caches when creating the type of the constructor. --- src/Lean/Elab/Structure.lean | 15 ++++-- src/Lean/Parser/Command.lean | 2 +- tests/lean/run/structBinderUpdates.lean | 65 +++++++++++++++++++++++++ 3 files changed, 78 insertions(+), 4 deletions(-) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 0de1fb587e..3592151988 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -197,8 +197,10 @@ private def defaultCtorName := `mk /- The structure constructor syntax is ``` -leading_parser try (declModifiers >> ident >> " :: ") +def structCtor := leading_parser + declModifiers true >> ident >> many Term.bracketedBinder >> " :: " ``` +and `structStx[4]` is `optional (" where " >> optional structCtor >> structFields)`. -/ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) (forcePrivate : Bool) : TermElabM CtorView := do @@ -229,9 +231,11 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc let name := ctor[1].getId let declName := structDeclName ++ name let declName ← applyVisibility ctorModifiers.visibility declName + -- `binders` is type parameter binder overrides; this will be validated when the constructor is created in `Structure.mkCtor`. + let binders := ctor[2] addDocString' declName ctorModifiers.docString? addDeclarationRangesFromSyntax declName ctor[1] - pure { ref := ctor[1], declId := ctor[1], modifiers := ctorModifiers, declName } + pure { ref := ctor[1], declId := ctor[1], modifiers := ctorModifiers, declName, binders } /-- ``` @@ -1112,18 +1116,23 @@ Builds a constructor for the type, for adding the inductive type to the environm -/ private def mkCtor (view : StructView) (r : ElabHeaderResult) (params : Array Expr) : StructElabM Constructor := withRef view.ref do + let (binders, paramInfoOverrides) ← elabParamInfoUpdates params view.ctor.binders.getArgs + unless binders.isEmpty do + throwErrorAt (mkNullNode binders) "Expecting binders that update binder kinds of type parameters." + trace[Elab.structure] "constructor param overrides {view.ctor.binders}" let lctx ← mkCtorLCtx let type ← instantiateMVars <| mkAppN r.indFVar params let fieldInfos := (← get).fields let fieldCtorFVars := fieldInfos |>.filter (·.kind.isInCtor) |>.map (·.fvar) let type := lctx.mkForall fieldCtorFVars type - withLCtx lctx {} do + withFreshCache <| withLCtx lctx {} do trace[Elab.structure] "constructor type before reductions:{indentExpr type}" let type ← fieldNormalizeExpr type trace[Elab.structure] "constructor type after reductions:{indentExpr type}" let type ← mkForallFVars params type let type ← instantiateMVars type let type := type.inferImplicit params.size true + let type := type.updateForallBinderInfos <| params.toList.map fun e => paramInfoOverrides[e]?.map Prod.snd trace[Elab.structure] "full constructor type:{indentExpr type}" pure { name := view.ctor.declName, type } diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 8086a4282b..68dc62be0a 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -223,7 +223,7 @@ def structFields := leading_parser structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder) def structCtor := leading_parser - atomic (ppIndent (declModifiers true >> ident >> " :: ")) + atomic (ppIndent (declModifiers true >> ident >> many (ppSpace >> Term.bracketedBinder) >> " :: ")) def structureTk := leading_parser "structure " def classTk := leading_parser diff --git a/tests/lean/run/structBinderUpdates.lean b/tests/lean/run/structBinderUpdates.lean index 9b90269707..3e3f8a2a43 100644 --- a/tests/lean/run/structBinderUpdates.lean +++ b/tests/lean/run/structBinderUpdates.lean @@ -134,3 +134,68 @@ class C (α : Type) where β : Type f (α β) : β end Ex6 + +/-! +## Constructor updates +-/ + +/-! +Comparing natural constructor binder kinds to the updated ones. +-/ +namespace ExC1 + +structure WithLp (p : Nat) (V : Type) where toLp :: + ofLp : V + +/-- info: constructor ExC1.WithLp.toLp : {p : Nat} → {V : Type} → V → WithLp p V -/ +#guard_msgs in #print WithLp.toLp + +structure WithLp' (p : Nat) (V : Type) where toLp (p) :: + ofLp : V + +/-- info: constructor ExC1.WithLp'.toLp : (p : Nat) → {V : Type} → V → WithLp' p V -/ +#guard_msgs in #print WithLp'.toLp +end ExC1 + +/-! +Checking errors +-/ +namespace ExC2 + +/-- error: Expecting binders that update binder kinds of type parameters. -/ +#guard_msgs in +structure WithLp (p : Nat) (V : Type) where toLp (p : _) :: + ofLp : V + +variable (n : Nat) + +/-- +error: only parameters appearing in the declaration header may have their binders kinds be overridden + +If this is not intended to be an override, use a binder with a type, for example '(x : _)'. +-/ +#guard_msgs in +structure WithLp (p : Nat) (V : Type) where toLp (n) :: + ofLp : V + +/-! +Even if `n` is used by `ofLp`, the restriction is still in place. +Motivation 1: the fields themselves have the same restriction, so it's for consistency. +Motivation 2: we should be able to tell whether the param binder update is legit without looking at all the fields. +Motivation 3: the constructor type is constructed before we know which `variable`s will be included. That would take participation of MutualInductive. +-/ +/-- +error: only parameters appearing in the declaration header may have their binders kinds be overridden + +If this is not intended to be an override, use a binder with a type, for example '(x : _)'. +-/ +#guard_msgs in +structure WithLp (p : Nat) (V : Type) where toLp (n) :: + ofLp : Fin n → V + +/-- error: Expecting binders that update binder kinds of type parameters. -/ +#guard_msgs in +structure WithLp (p : Nat) (V : Type) where toLp (m : Int) :: + ofLp : V + +end ExC2