.
>
> On a side note, if we consider typeclasses as predicates on types, then (especially with the extensions enabled) the type system looks extremely like a obfuscated logic programming language.With existential types it even starts to look like a first-order thereom prover.
> At present we can easily express different flavors of conjunction, but expressing disjunction is hard. And that's why the Prelude can cause problems here.
>
>

See
http://www.cse.chalmers.se/~hallgren/Papers/wm01.html

It gets even more fun with GADTs and, particularly, type families, which are explicitly designed with type level proofs in mind

-- Don