experiment with Hint Constants Opaque in typeclass search

[jdchristensen]

In #1779, @JasonGross suggested that typeclass search could be made faster and more predictable by having constants opaque by default and manually marked to unfold when that is appropriate. It would be interesting for someone to experiment with this. You start by putting

#[export] Hint Constants Opaque: typeclass_instances. (* all unfoldable constants have to be declared as such explicitly*)

somewhere near the start of Overture.v. Then various files in the library will fail to build, so you add necessary hints to fix those places. For example, Jason suggested:

#[export] Hint Mode IsTrunc ! ! : typeclass_instances. (* if the level and type both have some known structure, we can proceed *)
#[export] Hint Mode IsTrunc - + : typeclass_instances. (* if the type is fully known we can use tc to infer the level *)
#[export] Hint Mode IsEquiv - - + : typeclass_instances. (* only infer equivalence if the function is known; - - ! would also be fine if we want to infer IsEquiv id without needing the types to be known *)
#[export] Hint Mode Equiv + + : typeclass_instances. (* only infer Equiv if both types are fully known *)

But many others will be needed.

Jason had other guidance as well:

Roughly the universal trick is "set up typeclass search such that for every typeclass problem, there is at most one 'right' answer; the 'right' answer should be obvious to the coder just looking at the goal; try to get Coq to consider only the 'right' answer" (Hint Mode and Hint Opaque are useful for this last part). Relaxations of this rule are permissible, but introduce slowness exponential in the nesting depth, so make exceptions sparingly, ideally with bounded depth (Hint Cut ... : typeclass_instances can help with this), and make make sure to order the instance priorities in a way that cuts the search short as early as possible.

Basically, if you're designing something to be solved by typeclasses, you should be able to run the full resolution in your head, including paths that fail, for all the goals you care about; if you can't, you're probably expecting magic that you will pay for in performance.

I guess one trick for helping with performance is doing Hint Constants Opaque : typeclass_instances at the outset, and then only doing Hint Transparent foo : typeclass_instances when you're sure. (And probably you want to pair #[export] Hint Transparent with #[export] Hint Unfold; if you're allowing tc to see through the constant, you very likely have no business depending on it being folded.) (And even better to use an idiom like #[local] Hint Transparent foo : typeclass_instances. #[export] Instance : TheClass foo := _. so that you don't pollute conversion problems with unfolding foo when really you only need to unfold it for one particular instance.)

Set Typeclasses Debug Verbosity 2. Set Debug "tactic-unification,unification". Set Printing All. is absolutely essential to debugging failures then, though, since often it won't be clear why tc isn't considering some instance when it seems to you like it should.

[JasonGross]

Then various files in the library will fail to build, so you add necessary hints to fix those places. For example, Jason suggested:

#[export] Hint Mode IsTrunc ! ! : typeclass_instances. (* if the level and type both have some known structure, we can proceed *)
#[export] Hint Mode IsTrunc - + : typeclass_instances. (* if the type is fully known we can use tc to infer the level *)
#[export] Hint Mode IsEquiv - - + : typeclass_instances. (* only infer equivalence if the function is known; - - ! would also be fine if we want to infer IsEquiv id without needing the types to be known *)
#[export] Hint Mode Equiv + + : typeclass_instances. (* only infer Equiv if both types are fully known *)

But many others will be needed.

Ah, these suggestions are not to fix the problems caused by Hint Constants Opaque, but to further (and orthogonally) constrain typeclass search. Instead the problems caused by Hint Constants Opaque need to be fixed by Hint Transparent some_particular_constant : typeclass_instances.

[jdchristensen]

Thanks for clarifying. So here's one approach:

Phase 1: add Hint Constants Opaque; see what breaks; add Hint Transparent as needed.

Phase 2: add Hint Mode to add additional constraints based on what makes sense for various typeclasses, and make sure things still build.

As you make changes, check the build time and make sure you haven't caused a slowdown.

I guess phase 2 can be done without doing phase 1, and might be less work.

[jdchristensen]

More tips about phase 1 from @JasonGross:

Roughly the rule of thumb is that you need to mark transparent any definition whose truncatedness you want tc to infer, but for which no trunc instance is declared. (For example, if you want to use instances of IsTrunc _ { a : A & ... } interchangably with instances of IsTrunc _ (hfiber ...)). There are a couple of exceptions, though I expect them to be quite rare for IsTrunc. One example is that if you prove forall (A : Type) (ls : list A), IsHProp (nil = ls) and then want to automatically infer forall (A B : Type) (f : A -> B) (ls : list B), IsHProp (map f nil = ls), you'll need to declare map transparent. I wouldn't be all that surprised if none of the truncation instances broke.