[Haskell-cafe] Type family signatures

Thomas van Noort thomas at cs.ru.nl
Fri Aug 14 11:06:39 EDT 2009


Hello,

I have a question regarding type family signatures. Consider the 
following type family:

   type family Fam a :: *

Then I define a GADT that takes such a value and wraps it:

   data GADT :: * -> * where
     GADT :: a -> Fam a -> GADT (Fam a)

and an accompanying unwrapper:

   unwrap :: GADT (Fam a) -> (a, Fam a)
   unwrap (GADT x y) = (x, y)

When Fam is declared using the first notation,

   type family Fam a :: *

GHC HEAD gives the following error message:

   Main.hs:9:21:
     Couldn't match expected type `a' against inferred type `a1'
       `a' is a rigid type variable bound by
           the type signature for `unwrap' at Main.hs:8:20
       `a1' is a rigid type variable bound by
            the constructor `GADT' at Main.hs:9:8
     In the expression: x
     In the expression: (x, y)
     In the definition of `unwrap': unwrap (GADT x y) = (x, y)

However, when Fam is declared as (moving the a to the other side of the 
:: and changing it into *),

   type family Fam :: * -> *

everything is ok. So, it seems to me that GHC HEAD considers both 
signatures to be really different. However, I do not quite understand 
the semantic difference in my example, other than that Fam needs to be 
fully satisfied in its named type arguments. Note that GHC 6.10.3 does 
not accept the latter signature for Fam since it requires at least one 
index for some reason, that's why I'm using GHC HEAD.

Regards,
Thomas


More information about the Haskell-Cafe mailing list