The Coq mailing list

[Victor Porton <porton AT narod.ru>]

15.11.2011, 14:08, "Matthieu Sozeau" 
<matthieu.sozeau AT gmail.com>:
> Le 15 nov. 2011 à 00:07, Victor Porton a écrit :
>
>> The following does not verify, because in some reason Coq does not do a 
>> coercion from Derived to Base.
>>
>> Maybe it is an intended behavior but for me it seems like a conceptual 
>> error in Coq type classes.
>
> Well, maybe you should read about typeclasses in Haskell and Coq to 
> understand why they're
> implemented like this. In case you think "base" is declared a coercion, the 
> manual will
> inform you that it is not the case, "base" is simply declared as an 
> instance, of type
> [Derived -> Base]. You can declare it as a coercion yourself if you like.

Thus I probably misunderstand the Reference Manual.

From the page 363 of Reference Manual 8.3.pl2:

Coq < Class PreOrder (A : Type) (R : relation A) :=
Coq < { PreOrder_Reflexive :> Reflexive A R ;
Coq < PreOrder_Transitive :> Transitive A R }.
The syntax :> indicates that each PreOrder can be seen as a Reflexive 
relation. So each
time a reflexive relation is needed, a preorder can be used instead. This is 
very similar to the coercion
mechanism of Structure declarations. The implementation simply declares each 
projection as an
instance.

Why this does not work as I expect, that is automatically creating coercion 
from Derived to Base?

-- 
Victor Porton - http://portonvictor.org