feat: check universe parameters in mutually recursive inductive declaration

src/Lean/Elab/Inductive.lean

@@ -59,6 +59,11 @@ rs.forM fun r => unless (r.params.size == numParams) $
   Term.throwError r.view.ref "invalid inductive type, number of parameters mismatch in mutually inductive datatype";
 pure numParams
 
+private def checkLevelNames (rs : Array ElabHeaderResult) : TermElabM Unit := do
+let levelNames := (rs.get! 0).view.levelNames;
+rs.forM fun r => unless (r.view.levelNames == levelNames) $
+  Term.throwError r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatype"
+
 private def mkTypeFor (r : ElabHeaderResult) : TermElabM Expr := do
 Term.withLocalContext r.lctx r.localInsts do
   Term.mkForall r.view.ref r.params r.type
@@ -128,6 +133,7 @@ private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHead
 rs ← elabHeaderAux views 0 #[];
 when (rs.size > 1) do {
   numParams ← checkNumParams rs;
+  checkLevelNames rs;
   checkHeaders rs numParams 0 none
 };
 pure rs

tests/lean/inductive1.lean

@@ -49,3 +49,13 @@ inductive T1 (b : Bool) (x : Nat)  : Type
 inductive T2 (b : Bool) {x : Nat} : Type -- binder annotation mismatch at 'x'
 
 end
+
+
+-- Test7
+mutual
+
+inductive T1.{w1} (b : Bool) (x : Nat) : Type
+
+inductive T2.{w2} (b : Bool) (x : Nat) : Type -- universe parameter mismatch
+
+end

tests/lean/inductive1.lean.expected.out

@@ -13,3 +13,4 @@ expected type
   Nat
 inductive1.lean:40:0: error: invalid inductive type, number of parameters mismatch in mutually inductive datatype
 inductive1.lean:49:0: error: invalid mutually inductive type, binder annotation mismatch at parameter 'x'
+inductive1.lean:59:0: error: invalid inductive type, universe parameters mismatch in mutually inductive datatype