Rigid types, function types and type declarations mix causes error

Question

I was wondering, I can use type declaration in Haskell pretty much everywhere, but sometimes it leads to a strange result

apply (f :: a -> b) = f

is fine but

apply f = (f :: a -> b)

Couldn't match expected type ‘a1 -> b1’ with actual type ‘p’
‘p’ is a rigid type variable bound by
the inferred type of apply :: p -> a -> b

And that's pretty much it. I know it's a noob question, but I can't find any explanation for this behavior. Could someone elaborate?

I tried googling about this stuff, but search led to nowhere

Answer 1

Sigh, I can understand your confusion. This is rather cumbersome to explain, so I'll simplify a bit below.

In this part

apply (f :: a -> b) = ...

the variable f is a pattern argument, so the type annotation is interpreted as providing the type for that variable. Essentially, here we are saying "let f be any function of type a->b, for some types a and b".

By contrast, in

apply f = (f :: a -> b)

the variable f is an expression, and the type annotation now requires f to have that type. Essentially, we are saying "check that f has type a->b here, and abort otherwise".

However, it gets worse. What are types a and b here? Haskell, in normal circumstances, interprets the whole signature as if it were quantified over all variables. Essentially, we have

apply f = (f :: forall a b . a -> b)

So, we are actually saying "check that f is a polymorphic function from any type to any type". Variables a and b are termed "rigid type variables" which means "these stand for any arbitrary type, and can not be assumed to be a specific type". For example, writing [True, False] :: forall a. [a] raises a type error since the inferred type is [Bool] but the signature says that it must be a list of any type, not just Bool. The error will complain that the rigid a can not be identified with Bool.

This in turn copes with type inference. Type inference sees apply f = and tentatively gives f a type variable f :: p where p is a non-rigid type variable. If the code were apply f = f && True then we need p = Bool, but that's OK because p is not rigid, so we can identify that.

In apply f = (f :: forall a b . a -> b) instead we would need p = forall a b . a -> b but, alas, type inference is complicated and inference algorithms do not normally allow type variables like p to be instantiated to polymorphic types. Hence the type error.

Enough complicated theory. What to do about this, in practice? Here's a few thumb rules.

First, it's a good idea to always provide type annotations to out top-level names:

apply :: (a -> b) -> (a -> b)
apply f = f

There's no need to add more annotations in this case. However, if we really want that, we can:

-- at the beginning of the file:
{-# LANGUAGE ScopedTypeVariables #-}

apply :: forall a b . (a -> b) -> (a -> b)
apply f = (f :: a -> b)

Using that (very common) extension, we ask Haskell to make (f :: a -> b) refer to the a and b defined in the line above. That no longer means (f :: forall a b . a -> b). In GHC 9.* I think the extension is on by default.

Note that this is needed only when our types involve type variables. If we write expression :: Int we never meet such issues.

Personally, I wish Haskell98 (the first version of Haskell) always required forall and never automatically generalized type variables making the quantifications implicit. The current state is a bit weird, but that's the result of 20+ years of research and new extensions added on top of Haskell98 while trying to maintain (some) backward compatibility.