Typing rules for TypeClassLang

**Define inductive typing (elaboration) rules for TypeClassLang**

These effectively describe valid annotations for an untyped TypeClassLang program - ill-typed programs are those without any valid annotations. This requires a declarative specification of how to resolve overloading.

We should carefully design exactly what the type annotations are: they should not be required for all sub-expressions, and must be sufficient to make dictionary construction "easy". In other words, when we specify the semantics of TypeClassLang via dictionary construction, a well-annotated input program should provide all the information on exactly which dictionaries to construct where - there should be no duplication of overloading resolution in the specification of the typing rules and semantics.

Some further considerations are below.

## Types and kinds

TypeClassLang types must extend those of PureLang to incorporate type class constraints (the "context").
TypeClassLang must also have a kind system, (e.g. to consider `Functor`). We will use Haskell's simple `*` kind and `->` kind
constructor.

- Contexts may contain only typeclasses applied to single type variables
(i.e. not `Eq [a]`, but `Eq a` fine).
- Data type declarations may incorporate class constraints; ML-style exceptions remain monomorphic. For example:
```haskell
data Eq a => Set a = NilSet | ConsSet a (Set a)
```
This introduces type constructor `Set :: * -> *`, and constructors `NilSet :: ∀a. Set a` and `ConsSet :: ∀a. Eq a => ...`.
Note how the `Eq a` context is only applied where it is required, i.e. where `a` appears in the arguments of the constructor.
- Partial application is a key feature of kinds - our formalisation should not be overly arity-aware.

## Type classes

### Declarations

- Note that top-level definitions can be used in default operations - type classes exist at the same top-level scope.
- The hierarchy of superclasses must be acyclic.
- All overloading used within the class/instance declaration itself must appear in the context (or in method contexts, below)
- Methods can have their own context (!) as long as they don't constrain the type variable of the class declaration. For example:
```haskell
class C a where
m :: Show b => a -> b
```
- Method names must be unique

### Instances

- Each instance must define a minimal set of methods described by the class declaration, or it is invalid.
- Instance resolution must be deterministic: for any given call-site, there must be only one instance which matches.
Haskell permits overlapping instance declarations, but forbids a call-site which causes ambiguity. We might prefer to check for ambiguity at declaration time.
- "ambiguous types" are also an issue:
"a type `∀u. cx => t` where a type variable in `u` occurs in `cx` but not in `t`", e.g.
```haskell
let x = read "..." in show x
-- show :: ∀a. Show a => a -> String
-- read :: ∀a. Read a => String -> a
```