Coq: limiting (typeclass) hint usage

[andres-erbsen]

Currently typeclass instances follow require, making it essentially impossible to control the time taken by typeclass resolution as triggered by setoid_rewrite and such. As it seems that making Require not pull in instances would require a lot of changes, perhaps it would be possible to build a more lightweight mechanism to run a command with limited typeclass instances. For example, consider the following tactical

with_instances instancelist tac where instancelist has type list {T : Type & T} that could be called like with_instances [Proper_map] (setoid_rewrite fst_pair).

[Zimmi48]

I think everyone would support changing the behavior of Require to make it not pull in instances / hints. If that's too much for compatibility reasons, then we should have a lighter Require as proposed by @JasonGross.

Some other related improvement would be the ability to separate instances in several hint databases (currently they are all in typeclass_instances). I know that at least @CohenCyril would support this.

Finally, I'm interesting to learn more about your proposal as I do not understand it currently. Can you give an example of how you would use it in context?

[ppedrot]

For the record, there is an option Loose Hint Behavior that accepts a string flag "Lax" (the default), "Warn" or "Strict" to change the behaviour of hints w.r.t. mere requiring. I'd recommend turning it strict for your needs.