Typeclasses feature request: per-Instance mode

[RalfJung]

Description of the problem

It is fairly common that for a given typeclass, different instances want different Hint Mode: some instances just don't make sense if certain subterms are still an evar. In Iris we are currently working around this by splitting the typeclass into several different typeclasses with different modes, but that is hard to discover, harder to explain and even harder to get right. It would be much easier if we could just restrict some instances to not apply when parts of the goal are still an evar.

This also just came up again for me where I wanted to add some new subrelation instances, but I cannot, since Coq will pick them up in the most inopportune moments. (rewriting seems to do searches of the form subrelation ?r iff, and I really don't want it to pick up my instance as a random superrelation of iff.) This doesn't just cost performance through unnecessary detours during TC search, it actually breaks some of my proofs since these instances have parameters n : nat that Coq cannot infer, and leaves behind for the user to resolve. (This particular problem could possible be resolved by setting a Hint Mode for subrelation -- guessing a random superrelation seems unlikely to ever be useful. But the general case still stands, I think. Also if per-instance modes were a thing I wouldn't have to wait for the Coq standard library to add a mode to subrelation, I could add the new instances today.)

[SkySkimmer]

There would then be 2 ways to interpret Hint Mode:

• instances without a specified mode get the Hint Mode of their class at resolution time
• instances without a specified mode get the Hint Mode of their class at declaration time

The 1st way should be backwards compatible, is there any reason to try to do the 2nd way?

[SkySkimmer]

Actually there may be a 3rd way: at resolution time combine the mode of the class and the mode of the instance somehow
Not sure if that makes any sense though.

[RalfJung]

Combining modes usually means "any one of the modes must apply". So when class and instance have modes, do they get combined or does the instance trump the class? I think I would prefer the latter... otherwise a class with a mode can never have instances that restrict the mode further.

[RalfJung]

I think my intuitive understand would be that the two modes are applied independently:

• first a check is done whether any of the class modes apply. if not, just skip this goal and try to make progress elsewhere.
• then during instance search, for each instance considered its mode is checked.

So, if the instance has no mode, everything behaves as it does now. If instance and class both have modes, then any class mode and the instance mode must apply.

[SkySkimmer]

So it's not possible to have an instance with a mode which is (effectively) less strict than the class mode?

[RalfJung]

Yes I think that's a property one would want. (a) it helps Coq to exclude goals early, before doing any instance selection, and (b) it lets one use the modes to reason globally about the property of this class.

But it is very possible that I am missing a reasonable usecase here. Maybe @robbertkrebbers has thoughts (but he's on vacation currently AFAIK).

[JasonGross]

Duplicate of #14126