<HTML><BODY><p>Hi,</p><p>suppose that there is following data family:</p><p>> data family D a<br>> data instance D Int = DInt Int<br>> data instance D Bool = DBool Bool</p><p>it is not possible to match on constructors from different instances:</p><p>> -- type error<br>> a :: D a -> a<br>> a (DInt x) = x<br>> a (DBool x) = x</p><p>however, following works:</p><p>> data G :: * -> * where<br>> GInt :: G Int<br>> GBool :: G Bool<br>><br>> b :: G a -> D a -> a<br>> b GInt (DInt x) = x<br>> b GBool (DBool x) = x</p><p>The reason why second example works is equality constraints (a ~ Int) and (a ~ Bool) introduced by GADT's constructors, I suppose.</p><p>I'm curious - why data families constructors (such as DInt and DBool) doesn't imply such constraints while typechecking pattern matching?</p><p>Thanks.</p></BODY></HTML>