# Free type variables in Hindley-Milner type inference

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?

• I am not sure what you're asking, but perhaps it would help to think about nested functions: fun x -> .... (fun y -> e) ..... If the type of x appears in e, will you generalize over it? Jan 25, 2023 at 15:36
• Generalization only occurs for let expressions, but I think you're probably right that inference of a nested let could encounter free type variables in the type environment. I will investigate that. Thank you. Jan 25, 2023 at 15:52
• Yes, let is the thing to look at, not functions. You lead me astray when you wrote "In order to generalize a function, we ..." :-) Jan 25, 2023 at 15:56

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.