How is the scope of a nested universal quantifier determined (higher-rank types)?

Question

Originally I assumed the scope of a nested universal quantifier on the LHS of a function type can be determined purely syntactical, i.e. everything inside the parenthesis of (forall a. a -> b) -> Bool is within the same scope. However, this assumption is wrong:

{-# LANGUAGE RankNTypes #-}

fun :: (forall a. [a] -> b) -> Bool
fun _ = undefined

arg :: c -> c
arg _ = undefined

r = fun arg -- type variable a would escape its scope

This makes sense, because in fun b must be chosen before a and thus be fixed or independent of a. During unification the argument type c -> c would force b's instantiation with [a0] though.

So maybe scoping at the type level rather resembles that of functions at the term level, where the result value is clearly not part of the function's scope. In other words if b weren't the codomain of the function type, the type checker would pass. Unfortunately, I couldn't come up with an annotation that supports my reasoning.

A more restrictive way would be to disallow the instantiation of rigid type variables with any flexible one of the same annotation during unification. Both ways seem legitimate to me, but how does this actually work in Haskell?

Answer 1

Non-quantified type variables are implicitly quantified at the top-level. Your types are equivalent to

fun :: forall b . (forall a. [a] -> b) -> Bool
arg :: forall c . c -> c

Hence, the scope of b is the whole type.

You can think of each forall'ed variable as a kind of implicit additional type argument the function receives. I think you understand that, in a signature like

foo :: Int -> (String -> Bool) -> Char

the Int value is chosen by the caller of foo, while the String value is chosen by foo when (and if) it calls the function passed as a second argument.

In the same spirit,

fun :: forall b. (forall a. [a] -> b) -> Bool

means that b is chosen by the caller of fun, while a is chosen by fun itself.

The caller can indeed pass the b type explicitly using TypeAnnotations and write

fun @Int :: (forall a. [a] -> Int) -> Bool

After that, an argument of type forall a. [a] -> Int must be apssed, and length fits such polymorphic type.

fun @Int length :: Bool

Since this is the call site for fun we don't get to see where the "type argument" a is passed. That indeed can only be found in the definition of fun.

Well, it turns out that it's not really possible to define a fun which that type that makes a meaningful call to its argument (length, above). It would be if we had a slightly different signature like this:

fun :: forall b. Eq b => (forall a. [a] -> b) -> Bool
fun f = f @Int [1,2,3] /= f @Bool [True, False]

Here we can see that f (to be bound to length by the call) is called twice at two distinct types. This produces two values of type b that can then be compared to produce the final Bool.