Type classes

A general issue to collect discussion and decisions on supporting type classes. Discussion so far has been along the following lines:

- Introduction of a new, typed language between parsing and PureLang. Type inference would produce this by annotating an untyped AST (perhaps even one targeted directly by parsing). This language would need a semantics, permitting verification of compilation of type classes and extension of our end-to-end theorem.
- Type classes would be compiled using a [standard dictionary construction](https://dl.acm.org/doi/pdf/10.1145/227699.227700). PureLang etc. would therefore need some sort of record/dictionary support.

Many outstanding questions remain. For example, desired features (Haskell 98 type classes, or more?).

Usage of this new typed AST (TAST) brings other possibilities too.
- A typed equational theory over TAST to simplify verification of intra-TAST transformations.
- Introduction of a copy of GHC's core in between TAST and PureLang, i.e. compilation of TAST -> Core -> PureLang. We could then attempt to port various intra-Core optimisations from GHC.