interaction of GADTs and data families: a bug?

[Sittampalam, Ganesh]

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 think you expect too much. You just don't get type refinement with
type or data families. The function you wrote is similar to this code
that doesn't use families at all:

	fffuuu :: Maybe a -> a -> Int
	fffuuu (Just True) True = 42

and we wouldn't expect that to work because Haskell in general doesn't
have the runtime type match that would be required to handle it.

With GADTs, the specific choice of constructor is what gives you the
type matching functionality.

Cheers,

Ganesh


=============================================================================== 
Please access the attached hyperlink for an important electronic communications disclaimer: 
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html 
===============================================================================