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