Unbound type variables are not always unbound

[Innf107]

Minimal example

Running the following code in the repl reports type f : * -> *. Applying f to an argument shows that both * refer to the same type variable, which is therefore clearly not unbound and should be displayed as e.g. a -> a instead.

f = \x ->
    y : *
    y = x
    y

The code should arguably not compile at all, since * is bound in the type of y but escapes its scope when it is unified with the type of x.

[ayazhafiz]

For future implementors of this bug fix: probably what we want to do here is check after introduction of a def, are all wildcards generalized? In this case, we should see that after introducing y, the annotation * is not generalized because its type would be at a lower rank. If the wildcard is not generalized, issue a warning and say that this is really a type a for some a.