The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

This chapter presents a quick reference of the commands related to
type classes. For an actual introduction to type classes, there is a
description of the system [127] and the literature on type classes in
Haskell which also applies.


[127]
Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. In TPHOLs’08, 
2008.

http://scholar.google.com/scholar?q=Matthieu+Sozeau+and+Nicolas+Oury.+First-Class+Type+Classes.&hl=en&btnG=Search&as_sdt=1%2C9&as_sdtp=on

http://mattam.org/research/publications/First-Class_Type_Classes.pdf

"A newly declared class is automatically translated into a record type
having the index types as parameters and the same members. When the
user declares a new instance of such a type class, the system creates
a record object of the type of the corresponding class."

"Indeed, class methods are encoded, in the final proof term, as
applications of some projection of a record object representing the
instance"