feat: missing whnf at checkParamsAndResultType

src/Lean/Elab/Inductive.lean

@@ -127,12 +127,13 @@ private partial def checkParamsAndResultType (type firstType : Expr) (numParams
     forallTelescopeCompatible type firstType numParams fun _ type firstType =>
     forallTelescopeReducing type fun _ type =>
     forallTelescopeReducing firstType fun _ firstType => do
-    match type with
-    | Expr.sort .. =>
-      unless (← isDefEq firstType type) do
-        throwError "resulting universe mismatch, given{indentExpr type}\nexpected type{indentExpr firstType}"
-    | _ =>
-      throwError "unexpected inductive resulting type"
+      let type ← whnfD type
+      match type with
+      | Expr.sort .. =>
+        unless (← isDefEq firstType type) do
+          throwError "resulting universe mismatch, given{indentExpr type}\nexpected type{indentExpr firstType}"
+      | _ =>
+        throwError "unexpected inductive resulting type"
   catch
     | Exception.error ref msg => throw (Exception.error ref m!"invalid mutually inductive types, {msg}")
     | ex => throw ex

tests/lean/run/ind_whnf2.lean

@@ -0,0 +1,13 @@
+def Set (α : Type u) : Type u := α → id Prop
+
+mutual
+  inductive Even : id (Set Nat)
+  | zero : Even 0
+  | succ : Odd n → Even n
+
+  inductive Odd : Set Nat
+  | succ : Even n → Odd n
+end
+
+#print Even
+#print Odd