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.

Answer 3

Even

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

wouldn't typecheck (as was pointed out in the comments), and generate the same error, because Haskell infers least general types for expressions, and your type is more general than the inferred. As "A Gentle Introduction to Haskell" puts it,

An expression's or function's principal type is the least general type that, intuitively, "contains all instances of the expression".

If you specify a type explicitly, Haskell assumes you did that for a reason, and insists on matching the inferred type to the given type.

For the expression above the inferred type is (Num t) => Bool -> t -> (t -> t) -> t, so when matching the types, it sees that you gave Int for y and the type of z becomes (Int -> Int). Which is less general than (a -> Int). But you insisted on having an a there (not an Int) — a rigid type variable. In other words, your function f can only accept functions of type Int -> Int, but you are insisting that it may be given any function :: a -> Int, including :: String -> Int etc. (as @augustsson points out in the comments). Your declared type is too broad.

Similarly, if you had just one (z x) it would match with the given type of x and arrive at the narrower than declared type (Bool -> Int) for the z function. And yet again complain about a rigid type variable.

In effect, you declared the type (Num t) => Bool -> t -> (t1 -> t) -> t but it really is (Num t) => Bool -> t -> (t -> t) -> t. It is a different type.