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