chore(library/tactic/cases_tactic): add a bit more information to error message

src/library/tactic/cases_tactic.cpp

@@ -440,9 +440,8 @@ struct cases_tactic_fn {
                 auto s = mk_tactic_state(mvar);
                 throw cases_tactic_exception {
                     tactic::mk_exception([=] () {
-                        return format("cases tactic failed, unsupported equality") + line()
-                            + format("(only equalities between constructors and/or variables are") + line()
-                            + format("supported, try cases on the indices):") + line()
+                        return format("cases tactic failed, unsupported equality between type and constructor indices") + line()
+                            + format("(only equalities between constructors and/or variables are supported, try cases on the indices):") + line()
                             + s.pp_expr(H_type) + line();
                     }, s)
                 };

tests/lean/cases_unsupported_equality.lean

@@ -0,0 +1,6 @@
+inductive foo : ℕ → Type
+| a : foo 0
+| b : ∀ n, foo (n+1)
+
+example (n) (f : ℕ → ℕ) (h : foo (f n)) : true :=
+by cases h

tests/lean/cases_unsupported_equality.lean.expected.out

@@ -0,0 +1,9 @@
+cases_unsupported_equality.lean:6:3: error: cases tactic failed, unsupported equality between type and constructor indices
+(only equalities between constructors and/or variables are supported, try cases on the indices):
+f n = 0
+
+state:
+n : ℕ,
+f : ℕ → ℕ,
+h : foo (f n)
+⊢ f n = 0 → h == foo.a → true