Type checking, overview
Heaviliy influenced by Typing
Haskell in Haskell. Differences:
- It is designed to be extensible. (In what dimensions?)
- It performs the dictionary translation.
- The output can also be decorated with inferred types.
Some details remain to be implemented:
- Thorough kind checking (but the type checker is still sound).
- Making use of the superclass relation in context reduction.
- Checking inferred types agains given type signatures (entailment).