The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

  That’s a bug, but a very uneasy one due to the difference between 
metavariables
and existential variables (seems to be today’s theme…). In short, the Req
argument is treated as a dependent meta variable after unification with the
goal but the unifier (apply’s unifier) throws an error in this case (because 
before, you couldn’t have dependent goals). I can fix it for type class 
unification
in the trunk (and 8.5 and maybe the next 8.4pl too). In the new engine, this 
problem is solved.

Best,
— Matthieu

On 1 mars 2014, at 17:06, Julien Tesson 
<julien.tesson AT lacl.fr>
 wrote:

> 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
>