The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 13 Oct 2012 15:30:28 +0200,
Richard Dapoigny 
<richard.dapoigny AT univ-savoie.fr>
 a écrit :

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

First thing to do in this condition is to activate printing of implicit
arguments. I often set the printing of all low level contents.

For the rest, I did not try your code, as you defined stuff in your
comments and didn't wanted to play in understanding what should be
declared as parameters.


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