On Thursday 15 April 2010 8:10:42 am Sebastian Fischer wrote:
Dear GHC experts,
Certain behaviour when using
{-# LANGUAGE GADTs, TypeFamilies #-}
surprises me. The following is accepted by GHC 6.12.1:
data GADT a where BoolGADT :: GADT Bool
foo :: GADT a -> a -> Int foo BoolGADT True = 42
But the following is not:
data family DataFam a data instance DataFam Bool where BoolDataFam :: DataFam Bool
fffuuuu :: DataFam a -> a -> Int fffuuuu BoolDataFam True = 42
GHC 6.12.1 throws the following error (GHC 6.10.4 panics):
Couldn't match expected type `a' against inferred type `Bool' `a' is a rigid type variable bound by the type signature for `fffuuuu' at gadtDataFam.hs:13:19 In the pattern: BoolDataFam In the definition of `fffuuuu': fffuuuu BoolDataFam True = 42
I expect that `fffuuuu` should be accepted just like `foo`. Do I expect too much?
I don't really see how your example could be expected to work. I can only conclude that DataFam Bool is not a GADT, it's an ADT written with GADT syntax. Data/type families allow for definition of a family of types by case analysis on one or more indices. To define functions polymorphic in those indices, one must first do case analysis on those indices (via classes or a separate GADT parameter), or work at a specific index. Presumably one can do the following: data family Fam a :: * -> * data instance Fam Bool :: * -> * where BoolInt :: Fam Bool Int where Fam Bool a is itself a GADT with index a. But we can also write an instance: data instance Fam Int a = CInt a a which can also be written: data instance Fam Int a where CInt :: a -> a -> Fam Int a but the specificity of Int comes not from CInt being a GADT constructor, but because we are specifying what the type Fam Int is. And we cannot expect to define a function: foo :: Fam a b -> Int foo (CInt x y) = 32 foo BoolInt = 42 simply because type/data families do not work that way. The index of the family needs to be known before we can know which constructors we are able to match against. We could, however, write: foo :: Fam Bool b -> b foo BoolInt = 42 which shows that once we know that we are working with Fam Bool b, matching can refine b. I haven't used this feature yet, so perhaps an expert will correct me. But that is my interpretation of the situation. -- Dan