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?
id
will be type checked, and given a polymorphic type, beforex
andy
are type checked. This might find mutually recursive loops. If some binding in the loop is explicitly annotated, that's exploited to break the loop (the annotation is at first assumed, the other bindings are type checked, and finally the annotated binding are type checked last). If there's a loop without annotations, then generalization is only performed last: this might reject some well-typed programs. $\endgroup$ – chi Jul 23 '17 at 13:11let id1 :: a -> a ; id1 x = id2 x ; id2 y = const y (id1 True, id1 ())
type checks only becauseid1
is annotated, hence it is assumed to be polymorphic. I have not put this into an answer since it might be too much Haskell-specific -- one might use a different strategy. $\endgroup$ – chi Jul 23 '17 at 14:31