[Haskell-cafe] Equality constraints in type families

[Tom Schrijvers]

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 at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/