When omitting "forall" are they really inserted before the statement automatically?

Question

A lot of articles and books say that forall is explicitly added before the statement if it's not specified. For example

check :: (forall a. [a] -> Int) -> [b] -> [c] -> Bool

is actually

check :: forall b. forall c. (forall a. [a] -> Int) -> [b] -> [c] -> Bool

I have some problems with this because since Haskell uses currying I would imagine that the final signature would look like:

check :: (forall a. [a] -> Int) -> forall b. [b] -> forall c. [c] -> Bool

With added parens for clarity:

check :: (forall a. [a] -> Int) -> (forall b. [b] -> (forall c. [c] -> Bool))

And in this case the version with forall keywords before the expression seems to just be a shortcut for the convenience.

Am I right?

Answer 1

The nice thing about Haskell is that you can actually look at the intermediate language with the quantifiers explicit by passing -ddump-simpl to the compiler. As Tarmil pointed out, in System Fc rearranging the outer universal quantifiers in this function are semantically identical.

-- surface language
check :: (forall a. [a] -> Int) -> [b] -> [c] -> Bool
check = undefined

app1 = check undefined
app2 = check undefined undefined
app3 = check undefined undefined undefined

Translates to:

-- core language
check :: forall b c. (forall a. [a] -> Int) -> [b] -> [c] -> Bool
check = \ (@ b) (@ c) -> (undefined)

app1 :: forall b c. [b] -> [c] -> Bool
app1 = \ (@ b) (@ c) -> check (\ (@ a) -> undefined)

app2 :: forall c. [c] -> Bool
app2 = \ (@ c) -> check (\ (@ a) -> undefined) (undefined)

app3 :: Bool
app3 = check (\ (@ a) -> undefined) (undefined) (undefined)