Type Inference and Generalization

I've been trying to understand type inference for Hindley-Milner-based languages, and I'm struggling to understand how generalization works. Let's say I have the following program in Haskell:

x :: Int
x = id 1

y :: Char
y = id 'a'

id :: a -> a
id x = x

If the type-checker traverses the program from top to bottom, then from x we can infer that the type of id must generalize Int -> Int, and from y we can infer that id must generalize Char -> Char, but I'm unclear how we can use these constraints without inferring a too-specific type for id.

If we check id first, then we can just instantiate its type in x and y, and use unification. However, if we have recursive or mutually recursive bindings, ensuring that all mentioned top-level bindings are typechecked before the binding itself would lead the type-checker into an infinite loop.

How are these issues resolved?

There are a few things to realize:

First, top level declarations are implicitly let-bound, so your code is equivalent to the following:

let
  x :: Int
  x = id 1

  y :: Char
  y = id 'a'

  id :: a -> a
  id x = x

Secondly, as was mentioned in the comments, Haskell will sort the let statements topologically, nesting them when it can, and any recursive uses are monotyped unless annotated.

Finally, the types of let-variables are generalized at their definition, but specialized at their use. So now we have (something close to):

let
  id :: a -> a
  id x = x
in let
  x :: Int
  x = id 1

  y :: Char
  y = id 'a'

Finally, we need to see that while variable types are generalized at their definition, they are specialized at their use.

So, this is roughly what inference does:

• The checker infers the type $id : \alpha \to \alpha$, then generalizes this to $\forall a \ldotp a \to a$.

• The checker puts $id : \forall a \ldotp a \to a$ into the environment for checking $x$ and $y$

• While checking the definitions of $x$, at the use of $id$,

the type $\forall a \ldotp a \to a$ is instantiated to $\beta \to \beta$, where $\beta$ is a fresh unification variable.

• While checking the definitions of $y$, at the use of $id$,

the type $\forall a \ldotp a \to a$ is instantiated to $\gamma \to \gamma$, where $\gamma$ is a different fresh unification variable.

Because the polymorphic type scheme is instantiated with unique variables at each use, the inference is able proceed without error.

StackExchange Computer Science Q#79234, answer score: 4