
25 Apr
2013
25 Apr
'13
12:29 p.m.
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.