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.