Why does this function fail to typecheck?

Question

During a lecture on functional programming we saw the following Haskell function:

f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z x) + (z y)

It is expected that this function will fail to typecheck. However, the reason why this happens was not explained. When trying it out in GHCI I got the following output:

Prelude> :l test [1 of 1] Compiling Main             ( test.hs,
interpreted )

test.hs:2:35:
    Couldn't match expected type `a' with actual type `Bool'
      `a' is a rigid type variable bound by
          the type signature for f :: Bool -> Int -> (a -> Int) -> Int
          at test.hs:1:6
    Relevant bindings include
      z :: a -> Int (bound at test.hs:2:7)
      f :: Bool -> Int -> (a -> Int) -> Int (bound at test.hs:2:1)
    In the first argument of `z', namely `x'
    In the first argument of `(+)', namely `(z x)' Failed, modules loaded: none.

Why does this happen?

Answer 1

f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z x) + (z y)

The type signature asserts that our function z is polymorphic in its first argument. It takes a value of any type a and returns an Int. However, the scoping of the type variable a also means that it must be the same type a at all uses. a cannot be instantiated to different types at the same use site. This is "rank 1 polymoprhism".

You can read the type as really:

f :: forall a. Bool -> Int -> (a -> Int) -> Int

So:

z (x :: Bool) + z (y :: Int)

is invalid, as a is constrained to two different, independant types.

A language extension allows us to change the scope of a so that it can be instantiated to a polymorphic variable -- i.e. to hold different types at the same use site, including to have polymorphic function types:

Prelude> :set -XRankNTypes

Prelude> let f :: Bool -> Int -> (forall a . a -> Int) -> Int 
             f x y z = if x then y + y else (z x) + (z y)

Now the type a doesn't have global scope, and individual instantiations can vary. This lets us write the "more polymorphic" function f and use it:

Prelude> f True 7 (const 1)
14

So that's how cool higher rank polymorphism is. More code reuse.

Answer 2

That is simply not how simple parametric polymorphism works. The function z is polymorphic in the signature of the function, but in the body its only monomorphic.

When type-checking the definition the type checker infers a monomorphic type for the type variable a to use throughout the definition of the function. Your f however tries to call z with two different types, and thus the type checker infers two conflicting types for a.