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