Opaque vs Hint/Typeclasses Opaque

Question

Does Opaque foo indeed subsume Typeclasses Opaque foo , as you’d expect?

Background

I’m revising this code:

Global Typeclasses Opaque foo.
Global Opaque foo.

If I swap these statements, Typeclasses Opaque gives “Cannot coerce to_subst to an evaluable reference.”
For “Ideal Coq”, that means Typeclasses Opaque is redundant, but I’ve learned we don’t have that yet, so it’d be good to know for sure. Docs for either Opaque, Typeclasses Opaque and Hint Opaque say little except document that Opaque isn’t really opaque:

Opaque has also an effect on the conversion algorithm of Coq, telling it to delay the unfolding of a constant as much as possible when Coq has to check the conversion (see Section Conversion rules) of two distinct applied constants.

We also have a couple of issues on Opaque, which is why I’m especially uncertain.

AFAIK, yes.

Typeclasses Opaque foo is a unification hint that will prevent unification occurring during typeclass search when checking which instances to apply from unfolding foo.

I don’t know the exact effects of Opaque (there are IIRC still some ways to unfold such terms), but from what I recall it does at least affect all unification.

1 Like