feat(kernel/inductive): mark parameters, type formers and indices as implicit parameters in the elimination rule

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/inductive/inductive.cpp

@@ -622,9 +622,15 @@ struct add_inductive_fn {
         expr C_app   = mk_app(info.m_C, info.m_indices);
         if (m_dep_elim)
             C_app = mk_app(C_app, info.m_major_premise);
-        expr elim_ty = Pi(info.m_indices, Pi(info.m_major_premise, C_app));
+
+        expr elim_ty = Pi(info.m_major_premise, C_app);
+        unsigned i = info.m_indices.size();
+        while (i > 0) {
+            --i;
+            elim_ty = Pi(info.m_indices[i], elim_ty, mk_implicit_binder_info());
+        }
         // abstract all introduction rules
-        unsigned i = get_num_its();
+        i = get_num_its();
         while (i > 0) {
             --i;
             unsigned j = m_elim_info[i].m_minor_premises.size();
@@ -637,9 +643,13 @@ struct add_inductive_fn {
         i = get_num_its();
         while (i > 0) {
             --i;
-            elim_ty = Pi(m_elim_info[i].m_C, elim_ty);
+            elim_ty = Pi(m_elim_info[i].m_C, elim_ty, mk_implicit_binder_info());
+        }
+        i = m_param_consts.size();
+        while (i > 0) {
+            --i;
+            elim_ty = Pi(m_param_consts[i], elim_ty, mk_implicit_binder_info());
         }
-        elim_ty = Pi(m_param_consts, elim_ty);
         m_env = m_env.add(check(m_env, mk_var_decl(get_elim_name(d), get_elim_level_param_names(), elim_ty)));
     }
 

tests/lean/run/e14.lean

@@ -0,0 +1,34 @@
+inductive nat : Type :=
+| zero : nat
+| succ : nat → nat
+
+inductive list (A : Type) : Type :=
+| nil  : list A
+| cons : A → list A → list A
+
+check nil
+check nil.{1}
+check @nil.{1} nat
+check @nil nat
+
+check cons zero nil
+
+inductive vector (A : Type) : nat → Type :=
+| vnil  : vector A zero
+| vcons : forall {n : nat}, A → vector A n → vector A (succ n)
+
+check vcons zero vnil
+variable n : nat
+check vcons n vnil
+
+check vector_rec
+
+definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
+:= vector_rec (@nil A) (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v
+
+coercion vector_to_list
+
+variable f : forall {A : Type}, list A → nat
+
+check f (cons zero nil)
+check f (vcons zero vnil)