Sound and improved treatment of polymorphism and type variables

[LPTK]

We should not generalize non-function values, which is unsound in the presence of mutation.

Also, it would be good to handle all 'a variables as rigid and have a different ?a syntax for flexible ones.

Also, we should be able to refer to the same variables across type annotations in a given def. So we should store type variables in the typing context, not just in an inner map of typeType2.