fix: inductive elaboration should keep track of universe level parameters created in binders (#5814)

Refactors `inductive` elaborator to keep track of universe level
parameters created during elaboration of `variable`s and binders. This
fixes an issue in Mathlib where its `Type*` elaborator can result in
unexpected universe levels.

For example, in
```lean4
variable {F : Type*}
inductive I1 (A B : Type*) (x : F) : Type
```
before this change the signature would be
```
I1.{u_1, u_2} {F : Type u_1} (A : Type u_1) (B : Type u_2) (x : F) : Type
```
but now it is
```
I1.{u_1, u_2, u_3} {F : Type u_1} (A : Type u_2) (B : Type u_3) (x : F) : Type
```
Fixes this for the `axiom` elaborator too.

Adds more accurate universe level validation for mutual inductives.

Breaking change: removes `Lean.Elab.Command.expandDeclId`. Use
`Lean.Elab.Term.expandDeclId` from within `runCommandElabM`.

src/Lean/Elab/Command.lean

@@ -711,15 +711,6 @@ def addUnivLevel (idStx : Syntax) : CommandElabM Unit := withRef idStx do
   else
     modifyScope fun scope => { scope with levelNames := id :: scope.levelNames }
 
-def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM ExpandDeclIdResult := do
-  let currNamespace ← getCurrNamespace
-  let currLevelNames ← getLevelNames
-  let r ← Elab.expandDeclId currNamespace currLevelNames declId modifiers
-  for id in (← (← getScope).varDecls.flatMapM getBracketedBinderIds) do
-    if id == r.shortName then
-      throwError "invalid declaration name '{r.shortName}', there is a section variable with the same name"
-  return r
-
 end Elab.Command
 
 open Elab Command MonadRecDepth

src/Lean/Elab/Declaration.lean

@@ -102,14 +102,16 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   -- leading_parser "axiom " >> declId >> declSig
   let declId             := stx[1]
   let (binders, typeStx) := expandDeclSig stx[2]
-  let scopeLevelNames ← getLevelNames
-  let ⟨_, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName modifiers.stx stx
-  runTermElabM fun vars =>
+  runTermElabM fun vars => do
+    let scopeLevelNames ← Term.getLevelNames
+    let ⟨shortName, declName, allUserLevelNames⟩ ← Term.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
+    addDeclarationRanges declName modifiers.stx stx
+    Term.withAutoBoundImplicitForbiddenPred (fun n => shortName == n) do
     Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
       let type ← Term.elabType typeStx
       Term.synthesizeSyntheticMVarsNoPostponing
+      let xs ← Term.addAutoBoundImplicits xs
       let type ← instantiateMVars type
       let type ← mkForallFVars xs type
       let type ← mkForallFVars vars type (usedOnly := true)
@@ -135,63 +137,6 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
           compileDecl decl
         Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
 
-/-
-leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
-leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
--/
-private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
-  checkValidInductiveModifier modifiers
-  let (binders, type?) := expandOptDeclSig decl[2]
-  let declId           := decl[1]
-  let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName modifiers.stx decl
-  let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
-    -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
-    let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
-    if let some leadingDocComment := ctor[0].getOptional? then
-      if ctorModifiers.docString?.isSome then
-        logErrorAt leadingDocComment "duplicate doc string"
-      ctorModifiers := { ctorModifiers with docString? := TSyntax.getDocString ⟨leadingDocComment⟩ }
-    if ctorModifiers.isPrivate && modifiers.isPrivate then
-      throwError "invalid 'private' constructor in a 'private' inductive datatype"
-    if ctorModifiers.isProtected && modifiers.isPrivate then
-      throwError "invalid 'protected' constructor in a 'private' inductive datatype"
-    checkValidCtorModifier ctorModifiers
-    let ctorName := ctor.getIdAt 3
-    let ctorName := declName ++ ctorName
-    let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers.visibility ctorName
-    let (binders, type?) := expandOptDeclSig ctor[4]
-    addDocString' ctorName ctorModifiers.docString?
-    addAuxDeclarationRanges ctorName ctor ctor[3]
-    return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
-  let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
-    return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
-  let classes ← liftCoreM <| getOptDerivingClasses decl[6]
-  if decl[3][0].isToken ":=" then
-    -- https://github.com/leanprover/lean4/issues/5236
-    withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
-      "'inductive ... :=' has been deprecated in favor of 'inductive ... where'."
-  return {
-    ref             := decl
-    shortDeclName   := name
-    derivingClasses := classes
-    declId, modifiers, declName, levelNames
-    binders, type?, ctors
-    computedFields
-  }
-
-private def classInductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView :=
-  inductiveSyntaxToView modifiers decl
-
-def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  let v ← inductiveSyntaxToView modifiers stx
-  elabInductiveViews #[v]
-
-def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  let modifiers := modifiers.addAttr { name := `class }
-  let v ← classInductiveSyntaxToView modifiers stx
-  elabInductiveViews #[v]
-
 /--
 Macro that expands a declaration with a complex name into an explicit `namespace` block.
 Implementing this step as a macro means that reuse checking is handled by `elabCommand`.
@@ -230,19 +175,6 @@ def elabDeclaration : CommandElab := fun stx => do
     else
       throwError "unexpected declaration"
 
-/-- Return true if all elements of the mutual-block are inductive declarations. -/
-private def isMutualInductive (stx : Syntax) : Bool :=
-  stx[1].getArgs.all fun elem =>
-    let decl     := elem[1]
-    let declKind := decl.getKind
-    declKind == `Lean.Parser.Command.inductive
-
-private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
-  let views ← elems.mapM fun stx => do
-     let modifiers ← elabModifiers ⟨stx[0]⟩
-     inductiveSyntaxToView modifiers stx[1]
-  elabInductiveViews views
-
 /-- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/
 private def isMutualDef (stx : Syntax) : Bool :=
   stx[1].getArgs.all fun elem =>

src/Lean/Elab/Inductive.lean

@@ -18,6 +18,7 @@ import Lean.Elab.ComputedFields
 import Lean.Elab.DefView
 import Lean.Elab.DeclUtil
 import Lean.Elab.Deriving.Basic
+import Lean.Elab.DeclarationRange
 
 namespace Lean.Elab.Command
 open Meta
@@ -79,10 +80,56 @@ structure ElabHeaderResult where
   view       : InductiveView
   lctx       : LocalContext
   localInsts : LocalInstances
+  levelNames : List Name
   params     : Array Expr
   type       : Expr
   deriving Inhabited
 
+/-
+leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
+leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
+-/
+private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : TermElabM InductiveView := do
+  checkValidInductiveModifier modifiers
+  let (binders, type?) := expandOptDeclSig decl[2]
+  let declId           := decl[1]
+  let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
+  addDeclarationRanges declName modifiers.stx decl
+  let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
+    -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
+    let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
+    if let some leadingDocComment := ctor[0].getOptional? then
+      if ctorModifiers.docString?.isSome then
+        logErrorAt leadingDocComment "duplicate doc string"
+      ctorModifiers := { ctorModifiers with docString? := TSyntax.getDocString ⟨leadingDocComment⟩ }
+    if ctorModifiers.isPrivate && modifiers.isPrivate then
+      throwError "invalid 'private' constructor in a 'private' inductive datatype"
+    if ctorModifiers.isProtected && modifiers.isPrivate then
+      throwError "invalid 'protected' constructor in a 'private' inductive datatype"
+    checkValidCtorModifier ctorModifiers
+    let ctorName := ctor.getIdAt 3
+    let ctorName := declName ++ ctorName
+    let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers.visibility ctorName
+    let (binders, type?) := expandOptDeclSig ctor[4]
+    addDocString' ctorName ctorModifiers.docString?
+    addAuxDeclarationRanges ctorName ctor ctor[3]
+    return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
+  let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
+    return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
+  let classes ← getOptDerivingClasses decl[6]
+  if decl[3][0].isToken ":=" then
+    -- https://github.com/leanprover/lean4/issues/5236
+    withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
+      "'inductive ... :=' has been deprecated in favor of 'inductive ... where'."
+  return {
+    ref             := decl
+    shortDeclName   := name
+    derivingClasses := classes
+    declId, modifiers, declName, levelNames
+    binders, type?, ctors
+    computedFields
+  }
+
 private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) :=
   Term.withAutoBoundImplicitForbiddenPred (fun n => views.any (·.shortDeclName == n)) do
     if h : i < views.size then
@@ -94,7 +141,8 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc :
           let type := mkSort u
           Term.synthesizeSyntheticMVarsNoPostponing
           Term.addAutoBoundImplicits' params type fun params type => do
-            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
+            let levelNames ← Term.getLevelNames
+            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view }
         | some typeStx =>
           let (type, _) ← Term.withAutoBoundImplicit do
             let type ← Term.elabType typeStx
@@ -105,7 +153,8 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc :
             return (← mkForallFVars indices type, indices.size)
           Term.addAutoBoundImplicits' params type fun params type => do
             trace[Elab.inductive] "header params: {params}, type: {type}"
-            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
+            let levelNames ← Term.getLevelNames
+            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view }
       elabHeaderAux views (i+1) acc
     else
       return acc
@@ -123,13 +172,20 @@ private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit := do
     unless r.view.modifiers.isUnsafe == isUnsafe do
       throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
 
-private def checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
+private def InductiveView.checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
   if views.size > 1 then
     let levelNames := views[0]!.levelNames
     for view in views do
       unless view.levelNames == levelNames do
         throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
 
+private def ElabHeaderResult.checkLevelNames (rs : Array ElabHeaderResult) : TermElabM Unit := do
+  if rs.size > 1 then
+    let levelNames := rs[0]!.levelNames
+    for r in rs do
+      unless r.levelNames == levelNames do
+        throwErrorAt r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
+
 private def mkTypeFor (r : ElabHeaderResult) : TermElabM Expr := do
   withLCtx r.lctx r.localInsts do
     mkForallFVars r.params r.type
@@ -791,12 +847,15 @@ private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array Ind
 private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := Term.withoutSavingRecAppSyntax do
   let view0 := views[0]!
   let scopeLevelNames ← Term.getLevelNames
-  checkLevelNames views
+  InductiveView.checkLevelNames views
   let allUserLevelNames := view0.levelNames
   let isUnsafe          := view0.modifiers.isUnsafe
   withRef view0.ref <| Term.withLevelNames allUserLevelNames do
     let rs ← elabHeader views
     Term.synthesizeSyntheticMVarsNoPostponing
+    ElabHeaderResult.checkLevelNames rs
+    let allUserLevelNames := rs[0]!.levelNames
+    trace[Elab.inductive] "level names: {allUserLevelNames}"
     withInductiveLocalDecls rs fun params indFVars => do
       trace[Elab.inductive] "indFVars: {indFVars}"
       let mut indTypesArray := #[]
@@ -888,19 +947,55 @@ private def applyComputedFields (indViews : Array InductiveView) : CommandElabM
   liftTermElabM do Term.withDeclName indViews[0]!.declName do
     ComputedFields.setComputedFields computedFields
 
-def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
+def elabInductiveViews (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := do
   let view0 := views[0]!
   let ref := view0.ref
-  runTermElabM fun vars => Term.withDeclName view0.declName do withRef ref do
+  Term.withDeclName view0.declName do withRef ref do
     mkInductiveDecl vars views
     mkSizeOfInstances view0.declName
     Lean.Meta.IndPredBelow.mkBelow view0.declName
     for view in views do
       mkInjectiveTheorems view.declName
+
+def elabInductiveViewsPostprocessing (views : Array InductiveView) : CommandElabM Unit := do
+  let view0 := views[0]!
+  let ref := view0.ref
   applyComputedFields views -- NOTE: any generated code before this line is invalid
   applyDerivingHandlers views
   runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do
     for view in views do
       Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
 
+def elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Unit := do
+  let vs ← runTermElabM fun vars => do
+    let vs ← inductives.mapM fun (modifiers, stx) => inductiveSyntaxToView modifiers stx
+    elabInductiveViews vars vs
+    pure vs
+  elabInductiveViewsPostprocessing vs
+
+def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  elabInductives #[(modifiers, stx)]
+
+def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  let modifiers := modifiers.addAttr { name := `class }
+  elabInductive modifiers stx
+
+/--
+Returns true if all elements of the `mutual` block (`Lean.Parser.Command.mutual`) are inductive declarations.
+-/
+def isMutualInductive (stx : Syntax) : Bool :=
+  stx[1].getArgs.all fun elem =>
+    let decl     := elem[1]
+    let declKind := decl.getKind
+    declKind == `Lean.Parser.Command.inductive
+
+/--
+Elaborates a `mutual` block satisfying `Lean.Elab.Command.isMutualInductive`.
+-/
+def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
+  let inductives ← elems.mapM fun stx => do
+    let modifiers ← elabModifiers ⟨stx[0]⟩
+    pure (modifiers, stx[1])
+  elabInductives inductives
+
 end Lean.Elab.Command

tests/lean/run/inductive_typestar.lean

@@ -0,0 +1,44 @@
+import Lean
+
+/-!
+# `inductive` and the mathlib `Type*` notation
+
+The `inductive` command interacts badly with `Type*`.
+Universe parameters that came from the `variable` command were forgotten,
+leading to parameters coming from the binder list shadowing them.
+-/
+
+elab "Type*" : term => do
+  let u ← Lean.Meta.mkFreshLevelMVar
+  Lean.Elab.Term.levelMVarToParam (.sort (.succ u))
+
+section
+variable {F : Type*}
+
+/-!
+There should be three distinct level parameters.
+-/
+inductive I1 (A B : Type*) (x : F) : Type
+/-- info: I1.{u_1, u_2, u_3} {F : Type u_1} (A : Type u_2) (B : Type u_3) (x : F) : Type -/
+#guard_msgs in #check I1
+
+/-!
+This was also a problem for `axiom`.
+-/
+axiom ax1 (A B : Type*) (x : F) : Type
+/-- info: ax1.{u_1, u_2, u_3} {F : Type u_1} (A : Type u_2) (B : Type u_3) (x : F) : Type -/
+#guard_msgs in #check ax1
+end
+
+/-!
+Regression test: `axiom` shouldn't report "unused univeres levels" from `variable`s.
+-/
+section
+variable (X : Type u)
+axiom ax2 : Nat
+end
+section
+variable (X : Type*)
+axiom ax3 : Nat
+axiom ax4 (α : Sort _) : α
+end