Code unexpectedly accepted by GHC/GHCi

Question

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?

Answer 1

Briefly put, the type of x gets generalized by let. This is a key step in the Hindley-Milner type inference algorithm.

Concretely, 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 Nothing. Using (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.