The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 15 nov. 2011 à 16:29, Victor Porton a écrit :

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

Did you read what you just quoted there? " The implementation simply declares 
each projection as an 
instance." "This is very similar to the coercion mechanism of Structure 
declarations." meaning it is not
_the same_, but _similar_. If you write 
[@n
 derived] you are bypassing the instance resolution, if you 
wrote 
[@n
 _], it would infer the chain of "coercions" [base derived]: e.g:

Definition test (derived: Derived) := @n _.
Set Printing All.
Print test.
>> test = fun derived : Derived => @n (@base derived)
     : Derived -> nat

 One is not supposed to use @n 1
-- Matthieu