At Thu, 25 Apr 2013 20:29:16 +0400, Alexey Egorov wrote:
I'm curious - why data families constructors (such as DInt and DBool) doesn't imply such constraints while typechecking pattern matching?
I think you are misunderstanding what data families do. ‘DInt :: DInt -> D Int’ and ‘DBool :: DBool -> D Bool’ are two data constructors for *different* data types (namely, ‘D Int’ and ‘D Bool’). The type family ‘D :: * -> *’ relates types to said distinct data types. On the other hand the type constructor ‘D :: * -> *’ parametrises a *single* data type over another type—the fact that the parameter can be constrained depending on the data constructor doesn’t really matter here. Would you expect this to work?
newtype DInt a = DInt a newtype DBool a = DBool a
type family D a type instance D Int = DInt Int type instance D Bool = DBool Bool
a :: D a -> a a (DInt x) = x a (DBool x) = x
Francesco