interaction of GADTs and data families: a bug?
simonpj at microsoft.com
Fri Apr 16 01:58:56 EDT 2010
| > My intention was to use a GADT as data family instance (hence, I
| > wrote it in GADT style and it was accepted as such). Can't GADTs be
| > used as data family instances?
| I'm not aware of any restriction there, but that's not the issue here.
| You were trying to choose between different top-level types (which
| happen to be instances of the same family) by their constructors. GADTs
| allow you to choose between different constructors of the *same*
| top-level type.
| If DataFam Bool had multiple constructors, you could choose between them
| in fffuuuu. But fffuuuu would have to have type DataFam Bool -> Bool ->
| Int (as is necessary with your originally posted code).
Ganesh and Dan are exactly right. You can certainly have a data family instance that it itself a GADT:
data family T a b
data instance T Int b where
Foo :: T Int Bool
Bar :: T Int Char
data instance T Char b where ....
And indeed matching on a (T Int b) can refine the b:
f :: T Int b -> b
f Foo = True
f Bra = 'c'
But (T Int b) and (T Char b) are distinct data types, and do not share constructors.
More information about the Glasgow-haskell-users