fix: bug at inductive datatype resulting universe inference

src/Lean/Elab/Inductive.lean

@@ -321,9 +321,11 @@ unless (r.isParam) $
   throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly";
 us ← collectUniverses r rOffset numParams indTypes;
 let rNew := Level.mkNaryMax us.toList;
+let updateLevel (e : Expr) : Expr := e.replaceLevel fun u => if u == tmpIndParam then some rNew else none;
 pure $ indTypes.map fun indType =>
-  let type := indType.type.replaceLevel fun u => if u == tmpIndParam then some rNew else none;
-  { indType with type := type }
+  let type := updateLevel indType.type;
+  let ctors := indType.ctors.map fun ctor => { ctor with type := updateLevel ctor.type };
+  { indType with type := type, ctors := ctors }
 
 private def traceIndTypes (indTypes : List InductiveType) : TermElabM Unit :=
 indTypes.forM fun indType =>

tests/lean/run/new_inductive.lean

@@ -19,7 +19,7 @@ end
 
 #print bla
 
-inductive Term (α : Type) (β : Type) : Type
+inductive Term (α : Type) (β : Type)
 | var : α → bla (Term α β) (fun _ => Term α β) 10 → Term α β
 | foo (p : Nat → myPair (Term α β) (myList $ Term α β)) (n : β) : myList (myList $ Term α β) → Term α β
 
@@ -33,9 +33,9 @@ inductive arrow (α β : Type)
 | mk (s : Nat → myPair α β) : arrow α β
 
 mutual
-inductive tst1 : Type
+inductive tst1
 | mk : (arrow (myPair tst2 Bool) tst2) → tst1
-inductive tst2 : Type
+inductive tst2
 | mk : tst1 → tst2
 end
 
@@ -66,10 +66,15 @@ end Rbnode
 def Rbtree (α : Type u) (lt : α → α → Prop) : Type u :=
 {t : Rbnode α // t.WellFormed lt }
 
-inductive Trie : Type
+inductive Trie
 | Empty : Trie
 | mk    : Char → Rbnode (myPair Char Trie) → Trie
 
 #print Trie.rec
 #print Trie.noConfusion
 end test
+
+inductive Foo
+| mk : List Foo → Foo
+
+#check Foo