Incorrect inferred type for functions capturing globals with weak type variables

[jfecher]

If a function captures a global variable whose type contains a weak type variable (ie. one that will later be resolved but we do not yet know enough information to assign it a concrete type) the function will incorrectly be inferred to be polymorphic over this weak type variable, even if it is later resolved in the global. Example:

x = 3    // inferred type: Int a
f () = x // inferred type: forall a b. Unit -> Int a can b

This forall a portion is problematic since it will still be polymorphic even if the global is later resolved to a more specific type:

x = 3
f () = x

x + 4u8  // x is now known to be U8
// Type of f is still (forall a b. Unit -> Int a can b)

Attempting to print the type of f via --show-types will actually now show (forall U8 b. (Unit -> U8 can b)) since these forall-quantified variables are never meant to be bound over, but the treatment of them is the same as if they were unbound in the function type.

The correct inferred type of f would be forall b. Unit -> Int a can b with the now free a still referring to the same type variable used by x. There is a similar, common check for closures that close over values to not be polymorphic over the values that they close over, but this does not trigger in this instance since x is global and therefore not captured in the same way other globals are. It does hint that a possible solution may be to try to trigger this check either by enforcing all functions that close over globals with non-function values to be closures, but this may be overkill.