interaction of GADTs and data families: a bug?
Dan Doel
dan.doel at gmail.com
Thu Apr 15 09:29:18 EDT 2010
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
More information about the Glasgow-haskell-users
mailing list