The Coq mailing list

[Julien Tesson <julien.tesson AT lacl.fr>]

Le 28/02/2014 23:05, Matthieu Sozeau a écrit :
>
> 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
Yes, it does, thanks Matthieu.
But I still have trouble while trying to use my class. It seems that the 
transparency works only in one way, not the other. ( e.g. it doesn't unfold 
in the term from the instance  base, only in the term for which we try to 
find an instance). Is it the normal behavior ?

Here is a small example :

================
Require Import Coq.Classes.Init.
Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Classes.Equivalence.

Class Equiv A := equiv: relation A.
Class test A (R:Equiv A).
Typeclasses Transparent Equiv.


(* This instance allows to  guess the relation to use for R from the context  
  *)
Instance equivalence_Equiv A R {Req : Equivalence R} : Equiv A :=R.
Typeclasses Transparent equivalence_Equiv.

Instance T A R {Req : Equivalence R} : test A _.

Goal forall A (R: relation A) {Req : Equivalence R}, test A R.
intros A R Req.
(* but here, the tc resolution fails to unify my R with the 
(equivalence_Equiv A R Req) of the instance T. *)
typeclasses eauto.
Qed.

===============
Cheers,
Julien