Topic: tracing typeclasses?
Jason Gross (Mar 12 2021 at 19:57):
set_option trace.class_instances true, but that's not a thing in Lean4. What's the equivalent?
Leonardo de Moura (Mar 12 2021 at 20:32):
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 (Mar 12 2021 at 20:40):
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
Last updated: May 07 2021 at 13:21 UTC