simpa? should output information even if failing

Stream: lean4

[Yaël Dillies]

Consider the following MWE:

-- `Foo`, `Bar`, `Baz` are propeq but non-defeq propositions
def Foo : Prop := True
def Bar : Prop := True ↔ True
def Baz : Prop := (True ↔ True) ↔ True

-- Some bad pair of simp lemmas
@[simp] theorem foo_iff_bar : Foo ↔ Bar := by simp [Foo, Bar]
@[simp] theorem foo_iff_baz : Foo ↔ Baz := by simp [Foo, Baz]

-- `simpa?` won't let me know :(
example (h : Foo) : Baz := by simpa? using h
/-
type mismatch, term
  h
after simplification has type
  Bar : Prop
but is expected to have type
  Baz : Prop
-/

[Yaël Dillies]

This kind of situation, where a simpa doesn't work because I should disable some lemma in the simpa call, is really annoying to debug because simpa? fails instead of telling me what lemmas it tried to use.

[Yaël Dillies]

The only general way to debug this is to do

example (h : Foo) : Baz := by
  have := h
  simp? at this ⊢

which is a painful code transformation to perform

[Yaël Dillies]

Could simpa? output information about which lemmas it used even when it is failing?

[Yaël Dillies]

I've opened a RFC: lean4#7145