[Haskell-cafe] pattern matching on data families constructors

[Francesco Mazzoli]

At Fri, 26 Apr 2013 00:20:36 +0400,
Alexey Egorov wrote:
> Yes, my question is about why different instances are different types even if
> they have the same type constructor (D).
> I'm just find it confusing that using GADTs trick it is possible to match on
> different constructors.

See it this way: the two ‘D’s (the GADTs and the data family one) are both type
functions, taking a type and giving you back another type.

In standard Haskell all such type functions return instances of the same data
type (with a set of data constructors you can pattern match on), much like the
‘D’ of the GADTs.  With type/data families the situation changes, and the
returned type can be different depending on the provided type, which is what’s
happening here.

Now the thing you want to do is ultimately write your ‘a’, which as you said
relies on type coercions, but this fact (the ‘GADTs trick’) has nothing to do
with the fact that type families will relate types to different data types.

Francesco