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

[David McBride]

If you remove the type signature from f in the where clause it will
work.  The reason is because the type signature listed there, the a is
a different a than in the top level signature.  If you change it from
a to x, it says it should be the a that you can't seem to specify.

If you add the pragma ScopedTypeVariables to your file, it works the
way you would assume.  However you will have to change the toplevel
signature to iterateListF :: forall a. (a -> a) -> a -> Fix (ListF a)
in order to make it work (added the forall a.).

On Fri, Jul 5, 2013 at 4:35 PM, Ömer Sinan Ağacan <omeragacan at gmail.com> wrote:
> 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe