From c209cdc8be1e21ded6d57bdcd745f5e29bb73a1d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 6 Jul 2017 15:52:08 +0200
Subject: [PATCH] fix(kernel/inductive/inductive): identify indices modulo whnf

---
 src/kernel/inductive/inductive.cpp      | 22 +++++++---------------
 tests/lean/run/inductive_type_whnf.lean |  3 +++
 2 files changed, 10 insertions(+), 15 deletions(-)
 create mode 100644 tests/lean/run/inductive_type_whnf.lean

diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index f9a536f3f7..0d93c3ebf3 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -286,12 +286,13 @@ struct add_inductive_fn {
     /** \brief Check if the type of datatype is well typed,
         and the number of parameters match the argument num_params.
 
-        This method also populates the fields m_param_consts, m_it_level, m_it_const. */
+        This method also populates the fields m_param_consts, m_elim_info.m_indices, m_it_level, m_it_const. */
     void check_inductive_type() {
         expr t       = m_decl.m_type;
         tc().check(t, m_decl.m_level_params);
         unsigned i    = 0;
         m_it_num_args = 0;
+        t = whnf(t);
         while (is_pi(t)) {
             if (i < m_decl.m_num_params) {
                 expr l = mk_local_for(t);
@@ -299,8 +300,11 @@ struct add_inductive_fn {
                 t = instantiate(binding_body(t), l);
                 i++;
             } else {
-                t = binding_body(t);
+                expr c = mk_local_for(t);
+                m_elim_info.m_indices.push_back(c);
+                t = instantiate(binding_body(t), c);
             }
+            t = whnf(t);
             m_it_num_args++;
         }
         if (i != m_decl.m_num_params)
@@ -530,19 +534,7 @@ struct add_inductive_fn {
 
     /** \brief Populate m_elim_info. */
     void mk_elim_info() {
-        // First, populate the fields, m_C, m_indices, m_major_premise
-        expr t     = m_decl.m_type;
-        unsigned i = 0;
-        while (is_pi(t)) {
-            if (i < m_decl.m_num_params) {
-                t = instantiate(binding_body(t), m_param_consts[i]);
-            } else {
-                expr c = mk_local_for(t);
-                m_elim_info.m_indices.push_back(c);
-                t = instantiate(binding_body(t), c);
-            }
-            i++;
-        }
+        // First, populate the fields m_C and m_major_premise
         m_elim_info.m_major_premise = mk_local(mk_fresh_name(), "n",
                                                mk_app(mk_app(m_it_const, m_param_consts), m_elim_info.m_indices), binder_info());
         expr C_ty = mk_sort(m_elim_level);
diff --git a/tests/lean/run/inductive_type_whnf.lean b/tests/lean/run/inductive_type_whnf.lean
new file mode 100644
index 0000000000..941693e32b
--- /dev/null
+++ b/tests/lean/run/inductive_type_whnf.lean
@@ -0,0 +1,3 @@
+def pred (α : Type) := α → Prop
+
+inductive foo : pred ℕ