interaction of GADTs and data families: a bug?

[Simon Peyton-Jones]

| > 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.

Simon