Error message when -> fails has the top of the stack as a hypothesis in the context

[dranov]

/-- error:
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  x
x y z : Nat
H : x = y
⊢ z = z
---
error: unsolved goals
x y z : Nat
⊢ x = y → z = z
-/
theorem rrw_intro_fail : ∀ (x y z : Nat), x = y → z = z := by
  move=>x y z ->

I would expect the H to not be there in the error message (it isn't there after the tactic fails), but this is not very important.

[dranov]

There are two problems with this error message:

1. It leaks the implementation details of ->, mentioning the tactic rewrite which the user didn't write themselves;
2. It shows a goal that does not match the user's goal at the error point, but rather a goal that only shows up as an intermediate step in the implementation

To avoid this, we would need to write our own error message rather than rely on the one generated by the tactics used to implement ->.