[Haskell-cafe] same function's type accepted in top level, but rejected in where clause

5 Jul 2013

      Hi all,

I came across an interesting type checker error, a function is
accepted in top level, but rejected by type checker when moved to
`where ...` clause.

I moved required code to a new module for demonstration purposes:

    module Bug where

    fix :: (a -> a) -> a
    fix f = let x = f x in x

    data Fix f = Fix (f (Fix f))

    unFix :: Fix f -> f (Fix f)
    unFix (Fix a) = a

    data ListF a l = NilF | ConsF a l

    instance Functor (ListF a) where
        fmap _ NilF        = NilF
        fmap f (ConsF a l) = ConsF a (f l)

    fold :: Functor f => (f a -> a) -> Fix f -> a
    fold f a = f (fmap (fold f) (unFix a {- f (Fix f) -}))

    unfold :: Functor f => (a -> f a) -> a -> Fix f
    unfold f a = Fix (fmap (unfold f) (f a))

Now, after this code, type checker accept this function:

    iterateListF :: (a -> a) -> a -> Fix (ListF a)
    iterateListF fn e = unfold (foldFn fn) e

    foldFn :: (a -> a) -> a -> ListF a a
    foldFn fn a = ConsF a (fn a)

But rejects this:

    iterateListF :: (a -> a) -> a -> Fix (ListF a)
    iterateListF fn e = unfold f e
      where
        f :: a -> ListF a a
        f a = ConsF a (fn a)

With error:

    bug.hs:27:20:
        Couldn't match expected type `a1' with actual type `a'
          `a1' is a rigid type variable bound by
               the type signature for f :: a1 -> ListF a1 a1 at bug.hs:26:10
          `a' is a rigid type variable bound by
              the type signature for
                iterateListF :: (a -> a) -> a -> Fix (ListF a)
              at bug.hs:23:17
        In the return type of a call of `fn'
        In the second argument of `ConsF', namely `(fn a)'
        In the expression: ConsF a (fn a)

Changing type variables in type of `f` to `x` fails with this error:

    bug.hs:28:20:
        Couldn't match expected type `x' with actual type `a'
          `x' is a rigid type variable bound by
              the type signature for f :: x -> ListF x x at bug.hs:27:10
          `a' is a rigid type variable bound by
              the type signature for
                iterateListF :: (a -> a) -> a -> Fix (ListF a)
              at bug.hs:24:17
        In the return type of a call of `fn'
        In the second argument of `ConsF', namely `(fn a)'
        In the expression: ConsF a (fn a)
    Failed, modules loaded: none.

.. and this is strange because error message describes function as it
is before changing `a` to `x`.

Any ideas why this definition rejected? Is this a bug in GHC?

---
Ömer Sinan Ağacan
http://osa1.net