Type checking with RankNTypes in Haskell

Question

I'm trying to understand RankNTypes in Haskell and found this example:

check :: Eq b => (forall a. [a] -> b) -> [c] -> [d] -> Bool
check f l1 l2 = f l1 == f l2

(If my understanding is correct, this is equivalent to check :: forall b c d. Eq b => (forall a. [a] -> b) -> [c] -> [d] -> Bool.)

Ok, so far so good. Now, if the explicit forall a is removed, GHC produces the following errors:

Could not deduce (c ~ a)
from the context (Eq b)
[…]
Could not deduce (d ~ a)
from the context (Eq b)
[…]

When removing the nested forall, the type signature becomes

check :: forall a b c d. Eq b => ([a] -> b) -> [c] -> [d] -> Bool

It is easy to see why this fails type checking since l1 and l2 should have type [a] for us to pass them to f, but why isn't this the case when specifying f's type as (forall a. [a] ->b)? Is the fact that a is only bound inside the parens the full answer? I.e. the type checker will accept

[c] -> b ~ (forall a. [a] -> b)
[d] -> b ~ (forall a. [a] -> b)

(edit: Fixed. Thanks, Boyd!)

since a function of type (forall a. a -> b) can take any list?

Answer 1

When f = \xs -> ... is written with the explicit Rank2 quantification forall a. [a] -> b you can view this as a new function

f = Λa -> \xs -> ...

where Λ is a special lambda that takes a type argument to determine which specific type a it will use in the body of the function. This type argument is applied each time the function is called, just like how normal lambda bindings are applied on each call. This is how GHC handles forall internally.

In the explicitly forall'd version, f can be applied to different type arguments each time it is called so a can resolve to a different type each time, once for c and once for d.

In the version without the inner forall, this type application for a happens only once, when check is called. So every time f is called it must use the same a. Of course this fails since f is called on lists of different types.

Answer 2

It is easy to see why this fails type checking since l1 and l2 should have type [a] for us to pass them to f, but why isn't this the case when specifying f's type as (forall a. [a] ->b)?

Because the type (forall a. [a] -> B) can be unified with [C] -> B and (separately) [D] -> B. However, the type [A] -> B cannot be unified with either [C] -> B or [D] -> B.

Is the fact that a is only bound inside the parens the full answer?

Basically. You have to choose a particular type for each type variable when you are "inside" a forall scope, but outside you can use the forall multiple times and choose a different particular type each time you do.

I.e. the type checker will accept

[c] ~ (forall a. a -> b)
[d] ~ (forall a. a -> b)

since a function of type (forall a. a -> b) can take any list?

Careful. You seem to have lost some "[]" characters there. Also, you are not quite getting the unification correct. The type checker will accept both:

[C] -> B ~ (forall a. [a] -> B)
[D] -> B ~ (forall a. [a] -> B)

It will not accept either:

[C] -> B ~ [A] -> B
[D] -> B ~ [A] -> B