[Haskell-cafe] A type signature inferred by GHCi that is rejected when written explicitly

Pablo Nogueira pablo at babel.ls.fi.upm.es
Mon Jul 7 11:07:17 EDT 2008

I find this interesting,

GHCi accepts a function |dmap| which I show below and infers its type,
but if I annotate the function with the inferred type, GHCi's
type-checker rejects it.

I'm trying to generalise the datatype-generic dmap:

< dmap :: Bifunctor s => (a -> b) -> Fix s a -> Fix s b
< dmap f = In . bimap (dmap f) f . out

> data Fix s a = In { out :: s (Fix s a) a  }
> class Bifunctor s where
>     bimap :: (a -> c) -> (b -> d) -> s a b -> s c d

The idea is that recursive types are represented by their
(lamba-lifted) functors, eg:

> data ListF b a = NilF | ConsF a b

> instance Bifunctor ListF where
>   bimap f g NilF           =  NilF
>   bimap f g (ConsF a b)    =  ConsF (g a) (f b)

I now define two classes:

> class From a c x where
>     from :: a x -> c x
> class To a c y where
>     to :: c y -> a y

And a generic |gmap| which given the map for |c| and a mapping for |x|
delivers the map for |a|:

> type GMap t x y = (x -> y) -> t x -> t y
> gmap :: (From a c x, To a c y) => GMap c x y -> GMap a x y
> gmap gmc gmx = to . gmc gmx . from

I want to write |dmap| as a special case of |gmap|, but I can't even
get there. If I write

> dmap f = to . bimap (dmap f) f . from

GHCi infers it has type (up to renaming):

(From a1 (s (a1 x)) x,  Bifunctor s,  To  a2 (s (a2 y)) y) => (x -> y)
-> a1 x -> a2 y

But if I cut and paste the type into the code I get type errors:

   Could not deduce (From a1 (s1 (a11 x)) x) ...
    Could not deduce (From a11 (s1 (a11 x)) x, To a21 (s1 (a21 y)) y) ...
    Could not deduce (From a1 (s1 (a11 x)) x) ...


More information about the Haskell-Cafe mailing list