fix(library/definitional/projection): error messages for projection generation

src/library/definitional/projection.cpp

@@ -14,30 +14,37 @@ Author: Leonardo de Moura
 
 namespace lean {
 [[ noreturn ]] static void throw_ill_formed(name const & n) {
-    throw exception(sstream() << "error in 'projection' generation, '" << n << "' is an ill-formed inductive datatype");
+    throw exception(sstream() << "error in projection generation, '" << n << "' is an ill-formed inductive datatype");
 }
 
 static pair<unsigned, inductive::intro_rule> get_nparam_intro_rule(environment const & env, name const & n) {
     optional<inductive::inductive_decls> decls = inductive::is_inductive_decl(env, n);
     if (!decls)
-        throw exception(sstream() << "error in 'projection' generation, '" << n << "' is not an inductive datatype");
+        throw exception(sstream() << "error in projection generation, '" << n << "' is not an inductive datatype");
+    optional<unsigned> num_indices = inductive::get_num_indices(env, n);
+    if (num_indices && *num_indices > 0)
+        throw exception(sstream() << "error in projection generation, '"
+                        << n << "' is an indexed inductive datatype family");
     unsigned num_params = std::get<1>(*decls);
     for (auto const & decl : std::get<2>(*decls)) {
         if (inductive::inductive_decl_name(decl) == n) {
             auto intros = inductive::inductive_decl_intros(decl);
             if (length(intros) != 1)
-                throw exception(sstream() << "error in 'projection' generation, '"
-                                << n << "' must have a single constructor");
+                throw exception(sstream() << "error in projection generation, '"
+                                << n << "' does not have a single constructor");
             return mk_pair(num_params, head(intros));
         }
     }
-    optional<unsigned> num_indices = inductive::get_num_indices(env, n);
-    if (num_indices && *num_indices > 0)
-        throw exception(sstream() << "error in 'projection' generation, '"
-                        << n << "' is an indexed inductive datatype family");
     throw_ill_formed(n);
 }
 
+static bool is_prop(expr type) {
+    while (is_pi(type)) {
+        type = binding_body(type);
+    }
+    return is_sort(type) && is_zero(sort_level(type));
+}
+
 environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names) {
     // Given an inductive datatype C A (where A represent parameters)
     //   intro : Pi A (x_1 : B_1[A]) (x_2 : B_2[A, x_1]) ..., C A
@@ -52,6 +59,8 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
     expr intro_type              = inductive::intro_rule_type(intro);
     name rec_name                = inductive::get_elim_name(n);
     declaration ind_decl         = env.get(n);
+    if (env.impredicative() && is_prop(ind_decl.get_type()))
+        throw exception(sstream() << "error in projection generation, '" << n << "' is a proposition");
     declaration rec_decl         = env.get(rec_name);
     level_param_names lvl_params = ind_decl.get_univ_params();
     levels lvls                  = param_names_to_levels(lvl_params);
@@ -77,7 +86,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
     environment new_env = env;
     for (name const & proj_name : proj_names) {
         if (!is_pi(intro_type))
-            throw exception(sstream() << "error in projection '" << proj_name << "' generation, '"
+            throw exception(sstream() << "error generating projection '" << proj_name << "', '"
                             << n << "' does not have sufficient data");
         expr result_type   = binding_domain(intro_type);
         buffer<expr> proj_args;

tests/lean/proj.lean

@@ -0,0 +1,25 @@
+import logic data.nat.basic
+
+inductive vector (T : Type) : nat → Type :=
+  nil {} : vector T nat.zero,
+  cons : T → ∀{n}, vector T n → vector T (nat.succ n)
+
+#projections or
+#projections and
+#projections eq.refl
+#projections eq
+#projections vector
+
+inductive point :=
+mk : nat → nat → point
+
+#projections point :: x y z
+
+#projections point :: x y
+
+#projections point :: x y
+
+inductive funny : nat → Type :=
+mk : Π (a : nat), funny a
+
+#projections funny

tests/lean/proj.lean.expected.out

@@ -0,0 +1,8 @@
+proj.lean:7:0: error: error in projection generation, 'or' does not have a single constructor
+proj.lean:8:0: error: error in projection generation, 'and' is a proposition
+proj.lean:9:0: error: error in projection generation, 'eq.refl' is not an inductive datatype
+proj.lean:10:0: error: error in projection generation, 'eq' is an indexed inductive datatype family
+proj.lean:11:0: error: error in projection generation, 'vector' is an indexed inductive datatype family
+proj.lean:16:0: error: error generating projection 'point.z', 'point' does not have sufficient data
+proj.lean:20:0: error: invalid object declaration, environment already has an object named 'point.x'
+proj.lean:25:0: error: error in projection generation, 'funny' is an indexed inductive datatype family