fix(library/tactic/inversion_tactic): check whether eliminator can only eliminate to Prop

fixes #571

src/library/tactic/inversion_tactic.cpp

@@ -379,10 +379,16 @@ class inversion_tac {
         name const & I_name = const_name(I);
         expr g_type         = g.get_type();
         expr cases_on;
+        level g_lvl  = sort_level(m_tc.ensure_type(g_type).first);
         if (m_cases_on_decl.get_num_univ_params() != m_I_decl.get_num_univ_params()) {
-            level g_lvl  = sort_level(m_tc.ensure_type(g_type).first);
             cases_on     = mk_constant({I_name, "cases_on"}, cons(g_lvl, const_levels(I)));
         } else {
+            if (!is_zero(g_lvl)) {
+                if (m_throw_tactic_exception)
+                    throw tactic_exception(sstream() << "invalid 'cases' tactic, '" << const_name(I) << "' can only eliminate to Prop");
+                else
+                    throw inversion_exception();
+            }
             cases_on     = mk_constant({I_name, "cases_on"}, const_levels(I));
         }
         // add params

tests/lean/571.lean

@@ -0,0 +1,7 @@
+open nat
+variables (P : ℕ → Prop)
+
+example (H : ∃n, P n) : ℕ :=
+begin
+  cases H with n p,
+end

tests/lean/571.lean.expected.out

@@ -0,0 +1,13 @@
+571.lean:6:2: error:invalid 'cases' tactic, 'Exists' can only eliminate to Prop
+proof state:
+P : ℕ → Prop,
+H : ∃ (n : ℕ), P n
+⊢ ℕ
+571.lean:7:0: error: don't know how to synthesize placeholder
+P : ℕ → Prop,
+H : ∃ (n : ℕ), P n
+⊢ ℕ
+571.lean:7:0: error: failed to add declaration '14.1' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (P : …) (H : …),
+    ?M_1