Haskell type inference

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.

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.

Remember that in standard Haskell types (without using more advanced features that require extensions), type variables represent a choice the caller of the function gets to make. The implementation of the function has to work whatever choice is made for the type variable.

So this type signature:

g :: (a->a) -> (Char, Bool)

says that the caller can pick any type a they like, and then provide a function with type a -> a (for their choice of a), and g will give them back a (Char, Bool) pair. In particular, it would be valid for a caller to pick, say, Int for a and then provide (+1) as an Int -> Int function argument.

Your implementation is this:

g f = (f 'z', f True)

This implementation is not compatible with the type you gave for g. In particular, when given (+1) as an Int -> Int function, you would be trying to compute ('z' + 1, True + 1), which is obviously ill-typed.

There is in fact no type at all that could be chosen for a where an a -> a function could be applied to both the Char 'z' and the Bool True. You were right in your initial assessment that no simple Haskell type could be inferred for your function at all.

Stepping into more advanced territory, with the extension RankNTypes it is possible to give a different type to your implementation of g (note that this type will never be inferred, you have to give it explicitly if you want it):

{-# LANGUAGE RankNTypes #-}

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

Here, because of the forall a. nested inside the argument type, the caller doesn't get to choose a. Instead the caller is required to pass a polymorphic function that works for any a, because the implementation of g gets to choose a, and it can make a different choice every time it uses the function.

These two modes of use of polymorphism are very different, and it's important not to get them confused. Without extensions, you're always using the "caller gets to choose" system.