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

[Pablo Nogueira]

> I myselft  don't understand why GHCi doesn't accept the type it
>  infered as an explicit signature ...

I think it has to do with the following:

Looking at the type errors, they seem to indicate that the type
checker is being general and does not assume the |From| and |To|
"relations" are between
a type |t| and (s (t x) x)| but, in general, between |t| and |s (t' x) x|.

Given that

from   :: (From a1 c1 x) => a1 x -> c1 x
 to     :: (To   a2 c2 y) => c2 y -> a2 y
bimap  :: Bifunctor s => (t1 -> t3) -> (t2 -> t4) -> s t1 t2 -> s t3 t4

During type checking the following equations spring up:

c2 y   = s t3 t4
c1 x   =  s t1 t2
t2       = x
t4       = y
t1       = a1 x
t3       = a2 y

That'd give the same type as that inferred, but somehow new variables
|a11| and |a12| appear.

>  caused by a lack of functional dependencies.
>  class From a c x | a -> c where
> class To a c y | c -> a where
> ... hushes GHCi. The question now is, of course, if the new
>  dependencies are too restrictive for your problem.

They are of little avail given the instances I define:

 instance Bifunctor s => From (Fix s) (s (Fix s x)) x where
     from = out

 instance Bifunctor s => To (Fix s) (s (Fix s y)) y where
     to   = In