Stream: Coq users

Topic: Debugging typeclass resolution not selecting an instance


view this post on Zulip Armaël Guéneau (Nov 08 2020 at 12:24):

I have a scenario where typeclass resolution does not consider the instance I want as matching the goal. (If I remove all instances except the one I want, then typeclass resolution fails.)
Manually simple applying the instance works, however. The class has no declared Hint Modes.
How do I debug this?

view this post on Zulip Armaël Guéneau (Nov 08 2020 at 12:34):

Aaaaa, nevermind, problem solved: I apparently forgot to register the instance properly...

view this post on Zulip Matthieu Sozeau (Nov 08 2020 at 16:57):

Otherwise Set Typeclassed Debug Verbosity 2 would have led you to see that the instance was not even used


Last updated: Feb 01 2023 at 13:03 UTC