The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

On Friday, February 28, 2014, Julien Tesson <julien.tesson AT lacl.fr> wrote:
> > So, just to better understand what's in going on there, is it just typeclasses that are opaque  for the unification during the instance search or is it the same for all terms ?
> > Is there some documentation on this somewhere ?
> One should always read the documentation *before* asking such question, sorry.
> I just notice that the answer is almost in section 19.6.5 (http://coq.inria.fr/refman/Reference-Manual022.html#sec678).
> So if I understood right the documentation, The command for making term transparent or opaque works on any term.
>
> But the default status of a given term is not clear to me. I guess it depends on some black magic made by some great magician in such a way that most of the time, we don't have to care about it. I'm I right ?
>

Yes, that's the spirit. All defs are transparent except constants corresponding to the types of a definitional (one field, no curly braces) Class definition. E.g. Projections are transparent by default. The problem is that regular unification (outside tc resolution) will gladly unfold these definitional type-class constants, ignoring the transparency status, which is a bit of an abstraction leak. Iow, the typeclass system maintains its own transparency info.

Hope that clears up any remaining confusion,

-- Matthieu

--