Hi,

suppose that there is following data family:

> data family D a
> data instance D Int = DInt Int
> data instance D Bool = DBool Bool

it is not possible to match on constructors from different instances:

> -- type error
> a :: D a -> a
> a (DInt x) = x
> a (DBool x) = x

however, following works:

> data G :: * -> * where
> GInt :: G Int
> GBool :: G Bool
>
> b :: G a -> D a -> a
> b GInt (DInt x) = x
> b GBool (DBool x) = x

The reason why second example works is equality constraints (a ~ Int) and (a ~ Bool) introduced by GADT's constructors, I suppose.

I'm curious - why data families constructors (such as DInt and DBool) doesn't imply such constraints while typechecking pattern matching?

Thanks.