Judgemental equality underapproximation

Stream: Type theory

[Martin Dvořák]

Afaik Lean 4 underapproximates judgemental equality from the specific type theory.
Are there any negative consequences of it in practice?
Does anybody have a realistic example of a proof that won't compile even tho it could (would in theory)?

[Aaron Liu]

lean4#3213

[Aaron Liu]

It has been annoying to me once or twice

[Martin Dvořák]

Do you a have a real-life example that motivated your MWE?

[Aaron Liu]

I was using obtain to create data (I know, bad idea) and these were the kind of terms it produced