RFC: simpa? should output information even if failing

Proposal

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
-/

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.

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.

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

Community Feedback

Zulip

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reproducing the supplied MWE and comparing the behavior of simpa? with simp? at this ⊢. Trace the simpa? entry point and its failure path; done means a failing simpa? reports the simplification lemmas it tried, while preserving the existing type-mismatch information.