Free type variables in Hindley-Milner type inference

Question

I'm trying to understand how generalization works in H-M type inference. In order to generalize a function, we:

• Collect all the free type variables in the type of the function body,
• Subtract away any type variables that appear free in the type environment,
• And whatever is leftover can be generalized into a type scheme

The middle bullet is the one I'm having trouble with. In particular, I don't understand how it's possible for there to be any free type variables in the type environment. When we create a type scheme, we close over its free type variables, so the resulting scheme shouldn't have any free type variables. Thus, since none of the schemes in a type environment should have free type variables, how could the type environment itself have any free type variables?

Perhaps someone could give me a simple example program in OCaml or Haskell in which the type environment has a free type variable during type inference?

Answer 1

I found a good explanation and example in a paper called "Let Should not be Generalised":

A central feature of the Hindley-Milner system is that let-bound definitions are generalised. For example, consider the slightly artificial definition:

let f x = let g y = (x,y) in ...

The definition for g is typed in an environment in which x :: a, and the inferred type for g is ∀b.b → (a, b). This type is polymorphic in b, but not in a, because the latter is free in the type environment at the definition of g. This side condition, that g should be generalised only over variables that are not free in the type environment, is the only tricky point in the entire Hindley-Milner type system.