From de65af831856ccc827ee7e8ebafb1ee6e1745a00 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 24 Feb 2026 18:30:12 -0800 Subject: [PATCH] feat: overriding binder kinds of parameters in `inductive` constructors (#12603) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a feature where `inductive` constructors can override the binder kinds of the type's parameters, like in #9480 for `structure`. For example, it's possible to make `x` explicit in the constructor `Eq.refl`, rather than implicit: ```lean inductive Eq {α : Type u} (x : α) : α → Prop where | refl (x) : Eq x x ``` In the Prelude, this is currently accomplished by taking advantage of auto-promotion of indices to parameters. **Breaking change.** Inductive types with a constructor that starts with typeless binders may need to be rewritten, e.g. changing `(x)` to `(x : _)` if there is a `variable` with that name or if it is meant to shadow one of the inductive type's parameters. --- src/Init/Core.lean | 4 +- src/Lean/Elab/Inductive.lean | 4 +- src/Lean/Elab/MutualInductive.lean | 45 ++++++++- src/Lean/Elab/Structure.lean | 42 ++------- src/Std/Data/DHashMap/Raw.lean | 30 +++--- tests/lean/run/inductiveBinderUpdates.lean | 102 +++++++++++++++++++++ tests/lean/run/structBinderUpdates.lean | 4 +- 7 files changed, 175 insertions(+), 56 deletions(-) create mode 100644 tests/lean/run/inductiveBinderUpdates.lean diff --git a/src/Init/Core.lean b/src/Init/Core.lean index f9dd92b1f8..67ba3a75a1 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1339,10 +1339,10 @@ transitive and contains `r`. `TransGen r a z` if and only if there exists a sequ -/ inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α → Prop /-- If `r a b`, then `TransGen r a b`. This is the base case of the transitive closure. -/ - | single {a b} : r a b → TransGen r a b + | single {a b : α} : r a b → TransGen r a b /-- If `TransGen r a b` and `r b c`, then `TransGen r a c`. This is the inductive case of the transitive closure. -/ - | tail {a b c} : TransGen r a b → r b c → TransGen r a c + | tail {a b c : α} : TransGen r a b → r b c → TransGen r a c /-- The transitive closure is transitive. -/ theorem Relation.TransGen.trans {α : Sort u} {r : α → α → Prop} {a b c} : diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 59d39b4dd3..28a282d91e 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -207,7 +207,8 @@ private def elabCtors (indFVars : Array Expr) (params : Array Expr) (r : ElabHea let indFamily ← isInductiveFamily params.size indFVar r.view.ctors.toList.mapM fun ctorView => withoutExporting (when := isPrivateName ctorView.declName) do - Term.withAutoBoundImplicit <| Term.elabBinders ctorView.binders.getArgs fun ctorParams => + let (binders, paramInfoOverrides) ← elabParamInfoUpdates params ctorView.binders.getArgs (fun _ => pure true) + Term.withAutoBoundImplicit <| Term.elabBinders binders fun ctorParams => withRef ctorView.ref do let elabCtorType : TermElabM Expr := do match ctorView.type? with @@ -263,6 +264,7 @@ private def elabCtors (indFVars : Array Expr) (params : Array Expr) (r : ElabHea let type ← mkForallFVars (extraCtorParams ++ ctorParams) type let type ← reorderCtorArgs type let type ← mkForallFVars params type + let type := type.updateForallBinderInfos (params |>.map (fun param => paramInfoOverrides[param]?.map Prod.snd) |>.toList) trace[Elab.inductive] "{ctorView.declName} : {type}" return { name := ctorView.declName, type } where diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 520db70060..98cc6198d6 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -421,6 +421,47 @@ private def instantiateMVarsAtInductive (indType : InductiveType) : TermElabM In let ctors ← indType.ctors.mapM fun ctor => return { ctor with type := (← instantiateMVars ctor.type) } return { indType with type, ctors } +open Parser.Term in +private def typelessBinder? : Syntax → Option (Array Ident × BinderInfo) + | `(bracketedBinderF|($ids:ident*)) => some (ids, .default) + | `(bracketedBinderF|{$ids:ident*}) => some (ids, .implicit) + | `(bracketedBinderF|⦃$ids:ident*⦄) => some (ids, .strictImplicit) + | `(bracketedBinderF|[$id:ident]) => some (#[id], .instImplicit) + | _ => none + +/-- +Takes a binder list and interprets the prefix to see if any could be construed to be binder info updates. +Returns the binder list without these updates along with the new binder infos for these parameters. + +- `params` are the parameters appearing in the header +- `binders` is the binder list to process +- `maybeParam` should return true for every local that could be a parameter + (for example, in structures we check that the ids don't refer to previously defined fields) +-/ +def elabParamInfoUpdates + [Monad m] [MonadError m] [MonadLCtx m] [MonadLiftT TermElabM m] + (params : Array Expr) (binders : Array Syntax) + (maybeParam : FVarId → m Bool) : + m (Array Syntax × ExprMap (Syntax × BinderInfo)) := do + let mut overrides : ExprMap (Syntax × BinderInfo) := {} + for i in *...binders.size do + match typelessBinder? binders[i]! with + | none => return (binders.extract i, overrides) + | some (ids, bi) => + let lctx ← getLCtx + let decls := ids.filterMap fun id => lctx.findFromUserName? id.getId + let decls ← decls.filterM fun decl => maybeParam decl.fvarId + if decls.size != ids.size then + -- Then either these are for a new variables or the binder isn't only for parameters + return (binders.extract i, overrides) + for decl in decls, id in ids do + Term.addTermInfo' id decl.toExpr + unless params.contains decl.toExpr do + throwErrorAt id m!"Only parameters appearing in the declaration header may have their binders kinds be overridden" + ++ .hint' "If this is not intended to be an override, use a binder with a type: for example, `(x : _)`" + overrides := overrides.insert decl.toExpr (id, bi) + return (#[], overrides) + section IndexPromotion /-! ## Index-to-parameter promotion @@ -1134,8 +1175,8 @@ private def withUsed {α} (elabs : Array InductiveElabStep2) (vars : Array Expr) private def updateParams (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (List InductiveType) := indTypes.mapM fun indType => do let type ← mkForallFVars vars indType.type - let ctors ← indType.ctors.mapM fun ctor => do - let ctorType ← withExplicitToImplicit vars (mkForallFVars vars ctor.type) + let ctors ← withExplicitToImplicit vars <| indType.ctors.mapM fun ctor => do + let ctorType ← mkForallFVars vars ctor.type return { ctor with type := ctorType } return { indType with type, ctors } diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index f5bd25a1f4..4629a6efad 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -958,45 +958,17 @@ private def solveParentMVars (e : Expr) : StructElabM Expr := do discard <| MVarId.checkedAssign mvar parentInfo.fvar return e -open Parser.Term in -private def typelessBinder? : Syntax → Option ((Array Ident) × BinderInfo) - | `(bracketedBinderF|($ids:ident*)) => some (ids, .default) - | `(bracketedBinderF|{$ids:ident*}) => some (ids, .implicit) - | `(bracketedBinderF|⦃$ids:ident*⦄) => some (ids, .strictImplicit) - | `(bracketedBinderF|[$id:ident]) => some (#[id], .instImplicit) - | _ => none - -/-- -Takes a binder list and interprets the prefix to see if any could be construed to be binder info updates. -Returns the binder list without these updates along with the new binder infos for these parameters. --/ -private def elabParamInfoUpdates (structParams : Array Expr) (binders : Array Syntax) : StructElabM (Array Syntax × ExprMap (Syntax × BinderInfo)) := do - let mut overrides : ExprMap (Syntax × BinderInfo) := {} - for i in *...binders.size do - match typelessBinder? binders[i]! with - | none => return (binders.extract i, overrides) - | some (ids, bi) => - let lctx ← getLCtx - let decls := ids.filterMap fun id => lctx.findFromUserName? id.getId - -- Filter out all fields. We assume the remaining fvars are the possible parameters. - let decls ← decls.filterM fun decl => return (← findFieldInfoByFVarId? decl.fvarId).isNone - if decls.size != ids.size then - -- Then either these are for a new variables or the binder isn't only for parameters - return (binders.extract i, overrides) - for decl in decls, id in ids do - Term.addTermInfo' id decl.toExpr - unless structParams.contains decl.toExpr do - throwErrorAt id m!"Only parameters appearing in the declaration header may have their binders kinds be overridden" - ++ .hint' "If this is not intended to be an override, use a binder with a type: for example, `(x : _)`" - overrides := overrides.insert decl.toExpr (id, bi) - return (#[], overrides) +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 withoutExporting (when := view.modifiers.isPrivate) do let state ← get let binders := view.binders.getArgs - let (binders, paramInfoOverrides) ← elabParamInfoUpdates structParams binders + 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 => @@ -1085,7 +1057,7 @@ where 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) ← elabParamInfoUpdates structParams view.binders.getArgs + 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}" @@ -1182,7 +1154,7 @@ 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 := withoutExporting (when := isPrivateName view.ctor.declName) do withRef view.ref do - let (binders, paramInfoOverrides) ← elabParamInfoUpdates params view.ctor.binders.getArgs + let (binders, paramInfoOverrides) ← elabParamInfoUpdates params view.ctor.binders.getArgs (fun _ => pure true) 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}" diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index d3a5363700..73019c4bc7 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -677,45 +677,45 @@ inductive WF : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable -- we can write down `DHashMap.map` and `DHashMap.filterMap` in `AdditionalOperations.lean` -- without requiring these proofs just to invoke the operations. /-- Internal implementation detail of the hash map -/ - | wf {α β} [BEq α] [Hashable α] {m : Raw α β} : 0 < m.buckets.size → + | wf {α β : _} [BEq α] [Hashable α] {m : Raw α β} : 0 < m.buckets.size → (∀ [EquivBEq α] [LawfulHashable α], Raw.WFImp m) → WF m /-- Internal implementation detail of the hash map -/ - | emptyWithCapacity₀ {α β} [BEq α] [Hashable α] {c} : WF (Raw₀.emptyWithCapacity c : Raw₀ α β).1 + | emptyWithCapacity₀ {α β : _} [BEq α] [Hashable α] {c} : WF (Raw₀.emptyWithCapacity c : Raw₀ α β).1 /-- Internal implementation detail of the hash map -/ - | insert₀ {α β} [BEq α] [Hashable α] {m : Raw α β} {h a b} : WF m → WF (Raw₀.insert ⟨m, h⟩ a b).1 + | insert₀ {α β : _} [BEq α] [Hashable α] {m : Raw α β} {h a b} : WF m → WF (Raw₀.insert ⟨m, h⟩ a b).1 /-- Internal implementation detail of the hash map -/ - | containsThenInsert₀ {α β} [BEq α] [Hashable α] {m : Raw α β} {h a b} : + | containsThenInsert₀ {α β : _} [BEq α] [Hashable α] {m : Raw α β} {h a b} : WF m → WF (Raw₀.containsThenInsert ⟨m, h⟩ a b).2.1 /-- Internal implementation detail of the hash map -/ - | containsThenInsertIfNew₀ {α β} [BEq α] [Hashable α] {m : Raw α β} {h a b} : + | containsThenInsertIfNew₀ {α β : _} [BEq α] [Hashable α] {m : Raw α β} {h a b} : WF m → WF (Raw₀.containsThenInsertIfNew ⟨m, h⟩ a b).2.1 /-- Internal implementation detail of the hash map -/ - | erase₀ {α β} [BEq α] [Hashable α] {m : Raw α β} {h a} : WF m → WF (Raw₀.erase ⟨m, h⟩ a).1 + | erase₀ {α β : _} [BEq α] [Hashable α] {m : Raw α β} {h a} : WF m → WF (Raw₀.erase ⟨m, h⟩ a).1 /-- Internal implementation detail of the hash map -/ - | insertIfNew₀ {α β} [BEq α] [Hashable α] {m : Raw α β} {h a b} : + | insertIfNew₀ {α β : _} [BEq α] [Hashable α] {m : Raw α β} {h a b} : WF m → WF (Raw₀.insertIfNew ⟨m, h⟩ a b).1 /-- Internal implementation detail of the hash map -/ - | getThenInsertIfNew?₀ {α β} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {h a b} : + | getThenInsertIfNew?₀ {α β : _} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {h a b} : WF m → WF (Raw₀.getThenInsertIfNew? ⟨m, h⟩ a b).2.1 /-- Internal implementation detail of the hash map -/ - | filter₀ {α β} [BEq α] [Hashable α] {m : Raw α β} {h f} : WF m → WF (Raw₀.filter f ⟨m, h⟩).1 + | filter₀ {α β : _} [BEq α] [Hashable α] {m : Raw α β} {h f} : WF m → WF (Raw₀.filter f ⟨m, h⟩).1 /-- Internal implementation detail of the hash map -/ - | constGetThenInsertIfNew?₀ {α β} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a b} : + | constGetThenInsertIfNew?₀ {α β : _} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a b} : WF m → WF (Raw₀.Const.getThenInsertIfNew? ⟨m, h⟩ a b).2.1 /-- Internal implementation detail of the hash map -/ - | modify₀ {α β} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {h a} {f : β a → β a} : + | modify₀ {α β : _} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {h a} {f : β a → β a} : WF m → WF (Raw₀.modify ⟨m, h⟩ a f).1 /-- Internal implementation detail of the hash map -/ - | constModify₀ {α} {β : Type v} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a} {f : β → β} : + | constModify₀ {α : _} {β : Type v} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a} {f : β → β} : WF m → WF (Raw₀.Const.modify ⟨m, h⟩ a f).1 /-- Internal implementation detail of the hash map -/ - | alter₀ {α β} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {h a} + | alter₀ {α β : _} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {h a} {f : Option (β a) → Option (β a)} : WF m → WF (Raw₀.alter ⟨m, h⟩ a f).1 /-- Internal implementation detail of the hash map -/ - | constAlter₀ {α} {β : Type v} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a} + | constAlter₀ {α : _} {β : Type v} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a} {f : Option β → Option β} : WF m → WF (Raw₀.Const.alter ⟨m, h⟩ a f).1 /-- Internal implementation detail of the hash map -/ - | inter₀ {α β} [BEq α] [Hashable α] {m₁ m₂ : Raw α β} {h₁ h₂} : WF m₁ → WF m₂ → WF (Raw₀.inter ⟨m₁, h₁⟩ ⟨m₂, h₂⟩).1 + | inter₀ {α β : _} [BEq α] [Hashable α] {m₁ m₂ : Raw α β} {h₁ h₂} : WF m₁ → WF m₂ → WF (Raw₀.inter ⟨m₁, h₁⟩ ⟨m₂, h₂⟩).1 -- TODO: this needs to be deprecated, but there is a bootstrapping issue. -- @[deprecated WF.emptyWithCapacity₀ (since := "2025-03-12")] diff --git a/tests/lean/run/inductiveBinderUpdates.lean b/tests/lean/run/inductiveBinderUpdates.lean new file mode 100644 index 0000000000..7e74d1bc04 --- /dev/null +++ b/tests/lean/run/inductiveBinderUpdates.lean @@ -0,0 +1,102 @@ +/-! +# Tests of `inductive` parameter binder updates + +See also `structBinderUpdates.lean`. +-/ + +/-! +By default parameters are implicit. +-/ +inductive Eq1 {α : Type u} (x : α) : α → Prop where + | rfl : Eq1 x x +/-- info: Eq1.rfl.{u} {α : Type u} {x : α} : Eq1 x x -/ +#guard_msgs in #check Eq1.rfl + +/-! +Can override explicitness of the parameter for the constructor. +-/ +inductive Eq2 {α : Type u} (x : α) : α → Prop where + | rfl (x) : Eq2 x x +/-- info: Eq2.rfl.{u} {α : Type u} (x : α) : Eq2 x x -/ +#guard_msgs in #check Eq2.rfl + +/-! +Can override multiple parameter binders simultaneously. +-/ +inductive Eq3 {α : Type u} (x : α) : α → Prop where + | rfl (α x) : Eq3 x x +/-- info: Eq3.rfl.{u} (α : Type u) (x : α) : Eq3 x x -/ +#guard_msgs in #check Eq3.rfl + +/-! +There is no constraint on which parameter is overridden. +-/ +inductive Eq4 {α : Type u} (x : α) : α → Prop where + | rfl (α) : Eq4 x x +/-- info: Eq4.rfl.{u} (α : Type u) {x : α} : Eq4 x x -/ +#guard_msgs in #check Eq4.rfl + +/-! +Cannot override binders for parameters from from `variable`. +-/ +/-- +error: Only parameters appearing in the declaration header may have their binders kinds be overridden + +Hint: If this is not intended to be an override, use a binder with a type: for example, `(x : _)` +-/ +#guard_msgs in +variable {α : Type u} (x : α) in +inductive Eq5 : α → Prop where + | rfl (x) : Eq5 x x + +/-! +Test of the a header parameter shadowing a `variable` parameter that's still included as a parameter. +-/ +variable {α : Type u} (x : α) in +inductive Eq6 (x : α) : α → Prop where + | rfl (x) : Eq6 x (clear% x; x) +/-- info: Eq6.rfl.{u} {α : Type u} {x : α} (x✝ : α) : Eq6 x x✝ x -/ +#guard_msgs in #check Eq6.rfl + +/-! +The `(x)` syntax also can be used as a binder, if it's not shadowing a local variable. +-/ +variable {α : Type u} in +inductive Eq7 : α → α → Prop where + | rfl (x) : Eq7 x x +/-- info: Eq7.rfl.{u} {α : Type u} (x : α) : Eq7 x x -/ +#guard_msgs in #check Eq7.rfl + +/-! +Example of non-binder update. +-/ +inductive I1 : Nat → Nat → Type where + | mk (a b) : I1 a b +/-- info: I1.mk (a b : Nat) : I1 a b -/ +#guard_msgs in #check I1.mk + +/-! +Cannot mix binder updates with defining new fields. +When this happens, it assumes they're all new fields. +-/ +/-- +error: Mismatched inductive type parameter in + I2 a b +The provided argument + a +is not definitionally equal to the expected parameter + a✝ + +Note: The value of parameter `a✝` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. +-/ +#guard_msgs in +inductive I2 (a : Nat) : Nat → Type where + | mk (a b) : I2 a b + +/-! +Can mix binder updates with defining new fields if they're done in separate binders. +-/ +inductive I2' (a : Nat) : Nat → Type where + | mk (a) (b) : I2' a b +/-- info: I2'.mk (a b : Nat) : I2' a b -/ +#guard_msgs in #check I2'.mk diff --git a/tests/lean/run/structBinderUpdates.lean b/tests/lean/run/structBinderUpdates.lean index 00a6774274..89c9beeaae 100644 --- a/tests/lean/run/structBinderUpdates.lean +++ b/tests/lean/run/structBinderUpdates.lean @@ -1,5 +1,7 @@ /-! -# Tests of structure parameter binder updates +# Tests of `structure` parameter binder updates + +See also `inductiveBinderUpdates.lean`. -/ /-!