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?
fun x -> .... (fun y -> e) ..... If the type of
e, will you generalize over it? $\endgroup$
letexpressions, but I think you're probably right that inference of a nested
letcould encounter free type variables in the type environment. I will investigate that. Thank you. $\endgroup$
letis the thing to look at, not functions. You lead me astray when you wrote "In order to generalize a function, we ..." :-) $\endgroup$