The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
Better (?) approach to control typeclass resolution based on whether some arguments are evars
Right now, some of our typeclasses have extra variants called KnownXXX that use Hint Mode to only apply when certain arguments are not evars. This has lead to an explosion in the number of typeclasses.
Maybe a better approach would be to change the way we write some instances, and make sure they can only succeed if some arguments are not evars. I described such a solution at https://gitlab.mpi-sws.org/FP/iris-coq/commit/a9d41b6374f44fd93629f99cfecfea3549baa0b1#note_25278.
One possible concern is that applying such instances should fail as early as possible; if they have other premises, those shouldn't be resolved unless the evar check passes. On the other hand, the KnownXXX classes introduce additional coercions that typeclass resolution will try all the time, which could also be a performance issue.