tracing typeclasses?

Stream: lean4

[Jason Gross]

Google suggests set_option trace.class_instances true, but that's not a thing in Lean4. What's the equivalent?

[Leonardo de Moura]

We have set_option trace.Meta.synthInstance true but it is too verbose. As part of https://github.com/leanprover/lean4/issues/337, we want better error messages that explain why some typeclass resolution failed.

[Jason Gross]

Thanks! That (plus set_option pp.all true) helped me figure out why my coercion wasn't working: I had picked the wrong universe for the output sort when looking for CoeTC _ (Sort _). (Though I guess here in general I should be using coeSort, not coe.)