The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Hi all,
I have the following problem :
I have  introduced a hierarchy of universes such as:
=================================
Definition Universal                 := Type.
Definition Concept       : Universal := Type.
Definition Association   : Universal := Type.

Definition PT  : Concept   := Type.
Definition PD  : PT        := Type.
Definition ED  : PT        := Type.
...
=================================
Then, I create some type classes :
=================================

Class BinaryRel {A B:PT} : Association  := {
                     BinaryRel_arg1   : A;
                     BinaryRel_arg2   : B;
                     BinaryRel_struct : A->B->Prop}.

Class OccurIn `{@BinaryRel PRO R} : Association := { }.

Class Endocarditis `{@BinaryRel Disease Endocardium} : Association := {
                     Endocarditis_arity : SelectArity Disease (card_1 
Disease) }.

Instance BR1 : @BinaryRel Disease Endocardium :={
                     BinaryRel_arg1          := d1;  (* with Parameter 
d1 : Disease. *)
                     BinaryRel_arg2          := En1; (* with Parameter 
En1 : Endocardium.*)
                     BinaryRel_struct d1 En1 := True}.

Parameter End1 : @Endocarditis BR1.
Parameter End2 : @OccurIn BR1. (* <- error *)

=================================
And I obtain the following error message :

Error: The term "BR1" has type "BinaryRel" while it is expected to have 
type "BinaryRel".
=================================

while there are coercion paths between respective implicit arguments :

[u20] : Disease >-> PRO
[r5] : Endocardium >-> R

Is anyone has an explanation?
Thanks in advance,
Cheers,
Richard

--
And the wounded skies above say
it's much too much too late.
Well, maybe we should all be praying for time.

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard