reducible instances

Stream: lean4

[Jason Gross]

Is there a way to get the failed to synthesize instance message to print after all the inline/reducible things have been unfolded?

[Mario Carneiro]

I don't think that's how it works. Typeclass inference unfolds reducibles while attempting to unify the typeclass subgoal with an instance, it doesn't do a two pass thing where it first eagerly unfolds reducibles then does typeclass inference

[Mario Carneiro]

Probably if you want this behavior it would be an explicit thing, i.e. you could do apply_instance <|> dsimp reducible >> fail "failed to synthesize instance" or whatever the lean 4 equivalent of that is