From 3d1f682144ce6dfabd317e1511ee82fe14459ad7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Oct 2021 13:08:43 -0700
Subject: [PATCH] feat: missing `whnf` at `checkParamsAndResultType`

---
 src/Lean/Elab/Inductive.lean  | 13 +++++++------
 tests/lean/run/ind_whnf2.lean | 13 +++++++++++++
 2 files changed, 20 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/ind_whnf2.lean

diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 1b4a7769fc..13b80894dc 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/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
diff --git a/tests/lean/run/ind_whnf2.lean b/tests/lean/run/ind_whnf2.lean
new file mode 100644
index 0000000000..43ab6f4f5b
--- /dev/null
+++ b/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