From d4ae4da2226c326ec564ef9181cb85c8c5b60d48 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Jul 2020 16:17:54 -0700
Subject: [PATCH] feat: check given constructor resulting type

---
 src/Lean/Elab/Inductive.lean            | 6 +++++-
 tests/lean/inductive1.lean              | 8 ++++++++
 tests/lean/inductive1.lean.expected.out | 4 ++++
 3 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 4b72613b0b..2acdeb2a8f 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -203,7 +203,11 @@ r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getAr
       pure indFVar
     | some ctorType => do {
       type ← Term.elabTerm ctorType none;
-      -- TODO: check whether resulting type is indFVar
+      resultingType ← getResultingType ref type;
+      unless (resultingType.getAppFn == indFVar) $
+        Term.throwError ref ("unexpected constructor resulting type" ++ indentExpr resultingType);
+      unlessM (Term.isType ref resultingType) $
+        Term.throwError ref ("unexpected constructor resulting type, type expected" ++ indentExpr resultingType);
       pure type
     };
   type ← Term.mkForall ref ctorParams type;
diff --git a/tests/lean/inductive1.lean b/tests/lean/inductive1.lean
index 656d36d597..3acfe1030d 100644
--- a/tests/lean/inductive1.lean
+++ b/tests/lean/inductive1.lean
@@ -98,3 +98,11 @@ end
 inductive T1 : Nat → Type
 | z1 : T1 0
 | z2 -- constructor resulting type must be specified in inductive family declaration
+
+
+-- Test12
+inductive T1 : Nat → Type
+| z1 : T1 -- unexpected constructor resulting type
+
+inductive T1 : Nat → Type
+| z1 : Nat -- unexpected constructor resulting type
diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out
index 0927717760..65fe30abe4 100644
--- a/tests/lean/inductive1.lean.expected.out
+++ b/tests/lean/inductive1.lean.expected.out
@@ -22,3 +22,7 @@ inductive1.lean:82:10: error: invalid use of attributes in inductive declaration
 inductive1.lean:85:0: error: invalid 'private' constructor in a 'private' inductive datatype
 inductive1.lean:93:7: error: invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes
 inductive1.lean:100:0: error: constructor resulting type must be specified in inductive family declaration
+inductive1.lean:105:0: error: unexpected constructor resulting type, type expected
+  T1
+inductive1.lean:108:0: error: unexpected constructor resulting type
+  Nat