automatic help for diagnosing `erw`

Stream: general

[Scott Morrison]

I would _love_ to have some tactic level help for diagnosing erw. The general problem is that sometimes implicit arguments are not syntactically in the expected form (although definitionally correct), and while rw and simp won't work, erw will. I'd love to be able to see quickly which subexpression(s) is making the difference that causes rw to fail but erw to succeed.

[Scott Morrison]

Can anyone suggest a strategy for achieving this?

[Scott Morrison]

I'm pretty confident I can do the tactic writing required, or at least start, but I'm not sure what I should even try to do.