interaction of GADTs and data families: a bug?

Simon Peyton-Jones simonpj at
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 mailing list