We want to be able to infer each term definition group independantly
from start to finish (elaboration -> solving -> substitution) without
needing to share the type variable seed between groups, so this
algorithm can scale up to multiple modules.

For that, we need to add a step after substitution - generalize the
term definition. We do this by adding a new kind of type:

> TypeScheme [TypeVar] Type

which closes over all of the type variables in the type.
Consider it similar to a type level lambda that takes types as
arguments and returns a type which replaces all type variables with
the respective type arguments.

This simplifies the code because we no longer to distinguish between
Monomorphic and Polymorphic types, and we only need one Constraint:
Equality.

Where we used InstanceOf before, we use Equality. If the type on the
right is a type scheme, we will instantiate it during constraint solving.
When we encounter a constraint of the form:

> Equality t1 (TypeScheme typevars t2)

We instantiate t2 with fresh arguments replacing the typevars, like we
did with InstanceOf.

After we finish solving, producing a substitution, and subtituting the
type variables with their respective types in the substitution, we
generalize the type of each term definition and close over the type
variables.

So for example this term definition:

> id x = x

Will have this type after the substitution:

> TypeApp (->) (TypeVar "t1") (TypeVar "t1")

and after the generalization it will have the type:

> TypeScheme ["a"] (TypeApp (->) (TypeVar "a") (TypeVar "a"))

Which will be represented syntactically as:

> id : forall a. a -> a

The State seem to reset on interrupt, using IORef guarantees that it
will stay the same.

We want this because we want function to be able to refer to
themselves, and in a strict language a value refering to itself is
just an infinite loop so we do not allow that.