[Haskell-cafe] pattern matching on data families constructors

[Francesco Mazzoli]

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