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.)