Hi Hugo,
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.
I think you've uncovered a bug in the type checker. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case: F x y ~ F u v <=> F x ~ F u /\ y ~ v So if we apply that to F d c ~ F a (c,a) we get: F d ~ F a /\ c ~ (c,a) where the latter clearly is an occurs-check error, i.e. there's no finite type c such that c = (c,a). So the error in the second version is justified. There should have been one in the latter, but the type checker failed to do the decomposition: a bug. What instances do you have for F? Are they such that F d c ~ F a (c,a) can hold? By the way, for your function, you don't need equations in your type signature. This will do: hyloPara :: Functor (F d) => d -> (F d c -> c) -> (a -> F d a) -> a -> c Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/