`simpa` type mismatch error message could be improved

[kmill]

Description

When doing simpa using e, if the simplified type of e is not defeq to the simplified type of the target, then the error message is obscure, saying that h✝ has a type mismatch.

Context

This came up on Zulip

Steps to Reproduce

Here is an example:

example (p q : Prop) (hp : p ∧ True) : p ∧ q ∧ True := by
  simpa using hp
/-
type mismatch
  h✝
has type
  p : Prop
but is expected to have type
  p ∧ q : Prop
-/

The expected behavior is that the error message explains that the simplified type of hp is p and the simplified target is p ∧ q, and that it doesn't mention the inaccessible variable created by simpa to process the using expression.

Versions

4.8.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.