Fixes #109 by tracking which define type parameters are robust

[colin-mcd]

Specifically, this change implements the following:

• Modifies the context to keep track of which define type params should be robust
• When we type-check a global UsVar, we already create a new type vars to solve for each type param in its definition. Now for each of those type params that is robust, we add the constraint that the new type var must be solved to a robust type too.
• To determine which type params must be robust in a definition, we collect all robust constraints introduced by its body and then mark each type var/param as robust if it is a free var in any of the robust-constrained types.

We can talk about this tomorrow if it's unclear in any way

[davidweichiang]

Edge case:

data MyBool a = MyFalse | MyTrue;
define double = \x. (x, case x of MyFalse -> False | MyTrue -> True); -- error
--define double = \x. (x, x); -- no error
define b : MyBool (() -> ()) = MyTrue;
double b

I would perfectly fine with just not allowing a datatype to ignore a type parameter.

[davidweichiang]

Three possible outcomes: (1) make the first line an error (2) first line is okay, both definitions of double are errors (3) first line is okay, both definitions of double are okay

[davidweichiang]

Cf. #75 for the change that caused the 2nd definition of double to become allowed.

All in all, I think I mildly lean towards (3). Type inference is supposed to find the most general type and \forall a . MyBool a is more general than \forall a robust . MyBool a.

[davidweichiang]

I'll go ahead and merge this, too, to make the merge with #118 easier.