Try out Coq-style type classes

[gmalecha]

This is potentially a very interesting alternative approach to representing type classes, especially when coupled with the latest modular types code. It might make reasoning about structures such as monads and logics in full generality much easier.

• The reason that this is a question is that it will increase the term size by quite a bit. This could affect performance, but only trying it out will tell.

[gmalecha]

@jesper-bengtson this might be an interesting thing to look at for Charge.