- A+

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.

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.