Hi all,

I have encoded a type family such that:

type family F a :: * -> *

and a function (I know it is complicated, but I think the problem is self explanatory):

hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a (c,a)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c

hyloPara d g h = g . fmap (hyloPara d g h) . h

it all works fine.

However, if I change the declaration to (changed F d c for the "supposedly equivalent" F a (c,a)):

hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a (c,a)) => d -> (F a (c,a) -> c) -> (a -> F d a) -> a -> c

and I get

Occurs check: cannot construct the infinite type: c = (c, a)

When generalising the type(s) for `hyloPara'

This really messes up my notions on equality constraints, is it the expected behavior? It would be essential for me to provide this definition.

Thanks,

hugo