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.