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: [EMAIL PROTECTED]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
