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

@@ -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 {

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}))

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))

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}))