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?