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

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

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

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