MetaCoq is missing Hint Opaque

[Janno]

MetaCoq adds many typeclass instances for commonly used classes such as Equivalence, Reflexive, PreOrder, etc. Unfortunately almost all of them are on hint transparent terms which means there is a very noticeable cost from failing unification attempts when calling reflexivity and other standard tactics.

While porting to 8.18 I noticed that the number of instances has almost doubled and with it the cost of (failing) calls to reflexivity in our development. It's hard to get exact numbers since the version bump changes other things but I estimate that the extra instances account for an overall slowdown between 2 and 4% in our development although there are (usually smaller) files where it accounts for double digit percentage points.

AFAICT there isn't a way to import sub libraries such as template-coq without also getting all these instances automatically.

I recommend adopting the usual policy of never declaring instances on terms whose head is hint transparent.

[rlepigre]

We now have a more detailed data point on this: we actually got a 10% speedup overall (on our whole Coq development) by removing all imports of MetaCoq, which we only really relied on for lens generation (we now use elpi instead).

We are however still interested in getting this fixed, because we might need to use MetaCoq again in the future, and other projects would certainly benefit as well.

[mattam82]

You could maybe use selective imports using the new import categories, but indeed we will fix this.