I don't understand why this code should pass type-checking:
foo :: (Maybe a, Maybe b) foo = let x = Nothing in (x,x)
Since each component is bound to the same variable
x, I would expect that the most general type for this expression to be
(Maybe a, Maybe a). I get the same results if I use a
where instead of a
let. Am I missing something?
Briefly put, the type of
x gets generalized by
let. This is a key step in the Hindley-Milner type inference algorithm.
let x = Nothing initially assigns
x the type
Maybe t, where
t is a fresh type variable. Then, the type gets generalized, universally quantifying all its type variables (technically: except those in use elsewhere, but here we only have
t). This causes
x :: forall t. Maybe t. Note that this is exactly the same type as
Nothing :: forall t. Maybe t.
Hence, each time we use
x in our code, that refers to a potentially different type
Maybe t, much like
(x, x) gets the same type as
(Nothing, Nothing) for this reason.
Instead, lambdas do not feature the same generalization step. By comparison
(/x -> (x, x)) Nothing "only" has type
forall t. (Maybe t, Maybe t), where both components are forced to be of the same type. Here
x is again assigned type
Maybe t, with
t fresh, but it is not generalized. Then
(x, x) is assigned type
(Maybe t, Maybe t). Only at the top-level we generalize adding
forall t, but at that point is too late to obtain a heterogeneous pair.