interaction of GADTs and data families: a bug?

[Dan Doel]

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