Feature Request: per-hint Hint Mode

[andres-erbsen]

Description of the problem

I have a typeclass for which most instances are keyed by all parameters, except in sections where I prove lemmas about arbitrary instances of that typeclass I want the instance in the context to be used for typeclass resolution when the parameters are not known. I've been setting Local Hint Mode in that section as a workaround, but that applies to all Required instances, so I don't expect it to keep working out as I want.

Coq Version

8.13.1

@mattam82 ?

[mattam82]

I don't expect it to keep working out as I want.

Why is that? It seems to me that adding a local hint mode saying that in the section you want a more relaxed mode to get the default instances is the right thing to do. Also, the pattern annotation on a Hint is already a more precise information than a mode.

[JasonGross]

After chatting on coq-call with Matthieu, there are the following three use-cases:

1. It's annoying to break a long list of Existing Instances ... into a bunch of Hint Extern is annoying, and it'd be nice to have a compact syntax.
2. I think context variables cannot be blocked on Hint Extern patterns, though it's possible I'm misremembering
3. I'm not sure about this one, but it seems like there might be subtle differences in behavior about when constraints are considered "stuck" and what happens when they are, with regard to wanting some instances to be considered stuck rather than failing to apply? I'm not completely sure about this one, though, it might not be coherent.

[JasonGross]

More use cases:

---

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.)

Originally posted by @RalfJung in #17945

[JasonGross]

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.

Originally posted by @RalfJung in #17945 (comment)

@RalfJung you speak of "the instance mode", but shouldn't we permit multiple disjunctive instance modes?

[RalfJung]

Yeah I guess allowing multiple per-instance modes would be a natural generalization. It might make the syntax harder to figure out though.

[JasonGross]

Why not use the same syntax as the current Hint Mode? If you declare multiple per-instance modes for the same instance, they are treated disjunctively

[RalfJung]

I was thinking the mode would be somehow part of the Instance vernacular. If it's a separate vernacular then yeah that would work easily. I guess it could be an attribute but then it should also be easy to just have the attribute applied multiple times.