Haskell and Rank-N polymorphism

Question

What's exactly wrong about the following hypothetical Haskell code? When I compile it in my brain, it should output "1".

foo :: forall a. forall b. forall c. (a -> b) -> c -> Integer -> b
foo f x n = if n > 0 then f True else f x

bar :: forall a. a -> Integer
bar x = 1

main = do
     putStrLn (show (foo bar 1 2))

GHC complains:

$ ghc -XRankNTypes -XScopedTypeVariables poly.hs 

poly.hs:2:28:
     Couldn't match expected type `a' against inferred type `Bool'
       `a' is a rigid type variable bound by
           the type signature for `foo' at poly.hs:1:14
     In the first argument of `f', namely `True'
     In the expression: f True
     In the expression: if n > 0 then f True else f x

poly.hs:2:40:
     Couldn't match expected type `Bool' against inferred type `c'
       `c' is a rigid type variable bound by
            the type signature for `foo' at poly.hs:1:34
     In the first argument of `f', namely `x'
     In the expression: f x
     In the expression: if n > 0 then f True else f x

What does that mean? Isn't it valid Rank-N polymorphism? (Disclaimer: I'm absolutely not a Haskell programmer, but OCaml doesn't support such explicit type signatures.)

Answer 1

You're not actually using rank-N polymorphism in your code.

foo :: forall a. forall b. forall c. (a -> b) -> c -> Integer -> b

This is an ordinary rank-1 type. It reads: forall a,b and c this function can take a function of type a -> b, a value of type c and an Integer and return a value of type b. So it says that it can take a function of type Bool -> Integer or a function of type Integer -> Integer. It does not say that the function has to be polymorphic in its argument. To say that, you need to use:

foo :: forall b. forall c. (forall a. a -> b) -> c -> Integer -> b

Now you're saying that the type of the function needs to be forall a. a -> b, where b is fixed, but a is a newly introduced variable, so the function needs to be polymorphic in its argument.