The topic of Section 7.12.5 of the GHC Users Guide is higher rank polymorphism. There are some example valid types, among others:
f4 :: Int -> (forall a.a->a)
Now I wonder what this type means. I think it is the same as:
f4' :: forall a. Int -> a -> a
If this is so, can we generally mentally move forall like the above (that appears right of the rightmost arrow) to the left assuming that no type variable with the same name occurs in the rest of the type (but this could be dealt with renaming, simply)?
For example, the following would still be correct, wouldn't it:
f5 :: Int -> (forall a. (forall b. b -> a) -> a)
f5' :: forall a. Int -> (forall b. b -> a) -> a
Would be thankful for an insightful answer.
Background: In this talk about lenses by SPJ, we have:
type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
and then, when you compose them, you have such a lens type in the result. Therefore I just wanted to know whether my intuition is correct, that the forall in the result doesn't really matter - it just appears "accidentally" because of the type synonym. Otherwise, there must be some difference between the types for f4, f4'and f5, f5' above I would want to learn about.
Here is a ghci session:
Prelude> let f5 :: Int -> (forall a. (forall b. b -> a) -> a); f5 i f = f i
Prelude> :t f5
f5 :: Int -> (forall b. b -> a) -> a
Prelude>
Looks like GHC agrees with me, at least in this case .....