Stream: Coq users

Topic: Retroactively add Typeclasses Unique Instances


view this post on Zulip Thibaut Pérami (Mar 13 2024 at 18:22):

Hello, I'm dealing with increasingly complex type classes searches, and undecipherable error messages, but nearly all the typeclasses I use could have the Typeclasses Unique Instances flag. I suppose this would reduce the backtracking and therefore make typeclass search failure faster and more debuggable. The problem is that some of those type classes are defined in other library. Can I change this flag retroactively for a specific Class, or even better, just in a Section?

view this post on Zulip Gaëtan Gilbert (Mar 13 2024 at 18:26):

Can I change this flag retroactively for a specific Class, or even better, just in a Section?

no

I guess you could wrap them, something like

Class A := ...

Set Typeclasses Unique Instances.
Class UniqueA := uniqueA : A.
Instance mkUniqueA (x:A) : UniqueA := x.

Last updated: Jun 13 2024 at 19:02 UTC