From 6246fae32c834f49549ebfa23b5d3ab323410977 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 21 May 2014 16:29:25 -0700
Subject: [PATCH] fix(kernel/inductive): inductive datatype declaration
 validation bug pointed out by Cody Roux

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/inductive/inductive.cpp | 30 +++++++++++++++++++++++++++++-
 tests/lua/ind1.lua                 |  7 +++++--
 tests/lua/ind5.lua                 | 23 +++++++++++++++++++++++
 tests/lua/ind_ex.lua               |  2 +-
 4 files changed, 58 insertions(+), 4 deletions(-)
 create mode 100644 tests/lua/ind5.lua

diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index c240f1857..1f8f3cf5d 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -414,10 +414,38 @@ struct add_inductive_fn {
         updt_type_checker();
     }
 
+    /** \brief Return true if type formers C in the recursors can only map to Type.{0} */
+    bool elim_only_at_universe_zero() {
+        if (!m_env.impredicative() || !is_zero(m_it_levels[0])) {
+            // If Type.{0} is not impredicative or the resultant inductive datatype is not in Type.{0},
+            // then the recursor may return Type.{l} where l is a universe level parameter.
+            return false;
+        }
+        if (get_num_its() > 1 || length(inductive_decl_intros(head(m_decls))) != 1) {
+            // If we have more than one introduction rule, then yes, the type formers can only
+            // map to Type.{0}
+            return true;
+        }
+        // We have only one introduction rule, the final check is, the type of each argument
+        // that is not a parameter must live in Type.{0}.
+        auto ir    = head(inductive_decl_intros(head(m_decls)));
+        expr t     = intro_rule_type(ir);
+        unsigned i = 0;
+        while (is_pi(t)) {
+            if (i >= m_num_params) {
+                expr s = m_tc.ensure_sort(m_tc.infer(binding_domain(t)));
+                if (!is_zero(sort_level(s)))
+                    return true;
+            }
+            t = instantiate(binding_body(t), mk_local_for(t));
+            i++;
+        }
+        return false;
+    }
 
     /** \brief Initialize m_elim_level. */
     void mk_elim_level() {
-        if (m_env.impredicative() && is_zero(m_it_levels[0]) && (get_num_its() > 1 || length(inductive_decl_intros(head(m_decls))) != 1)) {
+        if (elim_only_at_universe_zero()) {
             // environment is impredicative, datatype maps to Bool/Prop, we have more than one introduction rule.
             m_elim_level = mk_level_zero();
         } else {
diff --git a/tests/lua/ind1.lua b/tests/lua/ind1.lua
index f5212c38b..e8d4d3687 100644
--- a/tests/lua/ind1.lua
+++ b/tests/lua/ind1.lua
@@ -95,7 +95,7 @@ env = add_inductive(env,
                     "eq", {l}, 2, Pi({{A, U_l}, {a, A}, {b, A}}, Bool),
                     "refl", Pi({{A, U_l}, {a, A}}, eq_l(A, a, a)))
 display_type(env, Const("eq_rec", {v, u}))
-display_type(env, Const("exists_rec", {v, u}))
+display_type(env, Const("exists_rec", {u}))
 display_type(env, Const("list_rec", {v, u}))
 display_type(env, Const("Even_rec"))
 display_type(env, Const("Odd_rec"))
@@ -129,8 +129,11 @@ assert(tc:is_def_eq(length(cons_nat(zero, nil_nat)), succ(zero)))
 assert(tc:is_def_eq(length(cons_nat(zero, cons_nat(zero, nil_nat))), succ(succ(zero))))
 
 -- Martin-Lof style identity type
+local env  = hott_environment()
 local Id_l = Const("Id", {l})
+env = env:add_global_level("u")
+env = env:add_global_level("v")
 env = add_inductive(env,
-                    "Id", {l}, 1, Pi({{A, U_l}, {a, A}, {b, A}}, Bool),
+                    "Id", {l}, 1, Pi({{A, U_l}, {a, A}, {b, A}}, U_l),
                     "Id_refl", Pi({{A, U_l, true}, {b, A}}, Id_l(A, b, b)))
 display_type(env, Const("Id_rec", {v, u}))
diff --git a/tests/lua/ind5.lua b/tests/lua/ind5.lua
new file mode 100644
index 000000000..047fb0d72
--- /dev/null
+++ b/tests/lua/ind5.lua
@@ -0,0 +1,23 @@
+function display_type(env, t)
+   print(tostring(t) .. " : " .. tostring(env:normalize(env:type_check(t))))
+end
+
+local A          = Local("A", Bool)
+local env        = environment()
+local retraction = Const("retraction")
+
+env = add_inductive(env,
+                    "retraction", Bool,
+                    "inj", Pi(A, retraction))
+
+local u = global_univ("u")
+env = env:add_global_level("u")
+local a = Local("a", Bool)
+local r = Local("r", retraction)
+
+local rec = Const("retraction_rec")
+display_type(env, rec)
+local proj = Fun(r, rec(Bool, Fun(a, a), r))
+local inj  = Const("inj")
+
+assert(not pcall(function() display_type(env, Fun(a, proj(inj(a)))) end))
diff --git a/tests/lua/ind_ex.lua b/tests/lua/ind_ex.lua
index d96ac0672..a103cedb4 100644
--- a/tests/lua/ind_ex.lua
+++ b/tests/lua/ind_ex.lua
@@ -13,4 +13,4 @@ function display_type(env, t)
    print(tostring(t) .. " : " .. tostring(type_checker(env):check(t)))
 end
 
-display_type(env, Const("inhabited_rec", {1, 1}))
+display_type(env, Const("inhabited_rec", {1}))