experiment with Hint Constants Opaque in typeclass search about coq-hott

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