fix(library/blast/forward/ematch): keep using ematching on implicit arguments

Ematching module should only ignore type classes (i.e., instance
implicit) and subsingletons (which includes propositions).

src/library/blast/forward/ematch.cpp

@@ -308,7 +308,7 @@ struct ematch_fn {
             lean_assert(length(*pinfos) == t_args.size());
             for (unsigned i = 0; i < t_args.size(); i++) {
                 param_info const & pinfo = head(*pinfos);
-                if (!pinfo.is_inst_implicit() && !pinfo.is_implicit() && !pinfo.is_subsingleton()) {
+                if (!pinfo.is_inst_implicit() && !pinfo.is_subsingleton()) {
                     /* We only match explicit arguments that are *not* subsingletons */
                     s = cons(entry(get_eq_name(), Match, p_args[i], t_args[i]), s);
                 } else {

tests/lean/run/blast_ematch_heq3.lean

@@ -0,0 +1,24 @@
+import data.nat
+open nat
+
+constant tuple.{l} : Type.{l} → nat → Type.{l}
+constant nil {A : Type} : tuple A 0
+
+constant append {A : Type} {n m : nat} : tuple A n → tuple A m → tuple A (n + m)
+infix ` ++ ` := append
+axiom append_assoc {A : Type} {n₁ n₂ n₃ : nat} (v₁ : tuple A n₁) (v₂ : tuple A n₂) (v₃ : tuple A n₃) :
+  (v₁ ++ v₂) ++ v₃ == v₁ ++ (v₂ ++ v₃)
+attribute append_assoc [simp]
+
+variables {A : Type}
+variables {p m n q : nat}
+variables {xs : tuple A m}
+variables {ys : tuple A n}
+variables {zs : tuple A p}
+variables {ws : tuple A q}
+
+example : p = m + n  → zs == xs ++ ys →  zs ++ ws == xs ++ (ys ++ ws) :=
+by inst_simp
+
+example : p = n + m  → zs == xs ++ ys →  zs ++ ws == xs ++ (ys ++ ws) :=
+by inst_simp