CSC448: Type Checking Revisited: Let Polymorphism II [122/133]

However, we must be careful about binding type variables that are used elsewhere when we introduce type schemes.

fun f x =>
  let y = x 
  in y (head y)
        

First assign fresh type variables:

f : 'a -> 'b
x : 'a
        

Then we see that y is bound to x : 'a, so we might naively say that y has type scheme forall ['a] 'a.

Unfortunately, this generalisation is not sound.

The type inference must check that type variables do not occur freely in the context before generalising them in this way. In this case, the type variable 'a appears freely in the context because x has that type.