Why am I getting this error when I try to write the type definition of a local function in Haskell?

Question

This my definition of the function any'

any' :: (t -> Bool) -> [t] -> Bool
any' f = foldl' step False
       where step :: Bool -> t -> Bool
             step b x | f x       = True
                      | otherwise = b

I get this error when loading in hugs:

ERROR "folds.hs":65 - Inferred type is not general enough
*** Expression    : step
*** Expected type : Bool -> a -> Bool
*** Inferred type : Bool -> _7 -> Bool

... and this in ghci:

folds.hs:65:27:
    Couldn't match expected type `t' with actual type `t1'
      `t' is a rigid type variable bound by
          the type signature for any' :: (t -> Bool) -> [t] -> Bool
          at folds.hs:62:9
      `t1' is a rigid type variable bound by
           the type signature for step :: Bool -> t1 -> Bool at folds.hs:64:22
    In the first argument of `f', namely `x'
    In the expression: f x
    In a stmt of a pattern guard for
                   an equation for `step':
      f x

When I remove the type definition of step It works fine, so my question is... There is a way to correctly write that type definition or am I dealing with one of those situations where local functions can't be explicitly typed?

Answer 1

The t in the signature

where step :: Bool -> t -> Bool

is not the same t as that occurring in the signature of any'. Instead, it is interpreted as a fresh type variable which is local to the step signature.

In other words, your code is actually equivalent to

any' :: (t -> Bool) -> [t] -> Bool
any' f = foldl' step False
   where step :: Bool -> a -> Bool          -- t renamed to a
         step b x | f x       = True
                  | otherwise = b

and the compiler then complains because step claims in its signature to be applicable to any type a while f requires a t.

A possible fix is removing the step signature. In this case the compiler will infer the right type on its own. This is not entirely pleasant from the programmer's point of view, since the compiler now will not check that the step signature really is the one which the programmer intended.

Another fix, as suggested in the comments, is to enable a Haskell extension which allows us to write our type.

{-# LANGUAGE ScopedTypeVariables #-}
import Data.List

any' :: forall t. (t -> Bool) -> [t] -> Bool
any' f = foldl' step False
       where step :: Bool -> t -> Bool
             step b x | f x       = True
                      | otherwise = b

Here the explicit quantifier forall t tells the compiler that the t occurring inside the definition of any' is really the same t, and not a fresh type variable.

Answer 2

You need the scoped type variables extension, otherwise the compiler sees the second t as another new polymorphic type variable, rather than the same t as in the main type declaration.

The clue that this is happening is in the message Couldn't match expected type 't' with actual type 't1'. Clearly ghci has renamed the second t t1, because it doesn't consider them the same.

You can use ScopedTypeVariables and an explicit forall to bring the t into scope for the inner function.

{-# LANGUAGE ScopedTypeVariables #-}

any' :: forall t.(t -> Bool) -> [t] -> Bool
any' f = foldl' step False
       where step :: Bool -> t -> Bool
             step b x | f x       = True
                      | otherwise = b