The Coq mailing list

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

-- Matthieu