Haskell type inference

Question

Why doesn't the following piece of code compile in Haskell?

g :: (a->a) -> (Char, Bool)
g f = (f 'z', f True)

As I understand it, Haskell tries to infer the most general type and then check that my type is inferred from the Haskell inferred type. And in this case, an unresolvable system of constraints is obtained: f is applied to 'z', so f is of type Char -> *. But in this case, f is applied to True, so f must be of type Bool -> * , but Char and Bool are not unified. But why, in case I explicitly specified the type, Haskell simply cannot check that I guessed right? After all the type specified by me approaches under function.

Answer 1

Your type signature is shorthand for

f :: ∀ a . (a -> a) -> (Char, Bool)

(∀ can also be written – and read – forall).

What that means is, anybody calling your function gets to pick a type a, and then use the instantiation for that type. For example, they could select a ~ String or a ~ Double or whatever.

What you seem to be trying to express is instead

f :: (∀ a . a -> a) -> (Char, Bool)

saying the function f itself has to be polymorphic. Well, you can say that, it just requires the extensions

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

on top of your source file.

Do note however that there is only one reasonable function with the signature ∀ a . a -> a, namely id.