Haskell and Rank-N Polymorphism

Question

What exactly is wrong with 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 fxn = if n > 0 then f True else fx 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 fx 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: fx In the expression: if n > 0 then f True else fx 

What does it mean? Isn't this a valid N-rank polymorphism? (Disclaimer: I'm absolutely not a Haskell programmer, but OCaml does not support such explicit types of signatures.)

Answer 1

In fact, you are not using rank-N polymorphism in your code.

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

This is a common type of rank-1. He reads: forall a, b and c this function can take a function of type a -> b , a value of type c and Integer and return a value of type b . Therefore, he says that he can execute a function of type Bool -> Integer or a function of type Integer -> Integer . He does not say that a function should be polymorphic in its argument. To say this, you need to use:

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

Now you say that the type of the function should be forall a. a -> b forall a. a -> b , where b fixed, but a is the new variable introduced, so the function must be polymorphic in its argument.