Formalize Haskell Type Classes as a Theory Graph
Choose a logical framework, e.g., LF, and formalize (a simple fragment of) Haskell in it.
Then use that theory as a meta-theory for a theory graph containing the standard type classes. This includes in particular the various kinds of Monad classes and their implementations
There are multiple variants of Monad, some related by include, some by view. Interestingly, because Haskell is a programming language, the Monad laws are often spelt out in a formal system. That can lead to confusion, and a clean theory would be very helpful.