rw failing due to missing typeclass

Stream: lean4

[Ruben Van de Velde]

#new members > (a ⊔ b) ⊓ c ≤ a ⊔ (b ⊓ c) @ 💬 is another case of the dreaded "Tactic rewrite failed: Did not find an occurrence of the pattern" error when the pattern is clearly there, due to a missing typeclass. I know by now that I can figure out what's wrong by explicitly specifying arguments until the error changes to "failed to synthesize", but it still would be great to have a better error message by default. Is anyone working on this?

[Aaron Liu]

This might be possible I have an idea

[Kyle Miller]

lean4#7172 is an experiment from earlier this year, but I haven't had much of a chance to test it out and I got busy with other things in the meantime. Example output is here: #lean4 dev > Misleading error message on type mismatch @ 💬

I'd be happy to hear about any other ideas to address this.