On Fri, Aug 14, 2009 at 11:06 AM, Thomas van Noort<tho...@cs.ru.nl> wrote: > 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)
This is because type families are not injective. Nothing stops you from defining two instances such as, type instance Fam Int = Bool type instance Fam Char = Bool in which case a value of type GADT Bool is ambiguous. Does it contain an Int or a Char? > 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. A type family with no index is equivalent to a type synonym. But in answer to your question, these signatures are very different. Consider these families. type family Foo a b :: * type family Bar a :: * -> * Foo is indexed by two parameters, but Bar is only indexed by one. type instance Foo A B = X type instance Foo A C = X -- Foo a b ~ Foo a c does not imply b ~ c type instance Bar A = [] -- Bar a b ~ Bar a c does imply b ~ c Bar returns a type constructor, so it can be used anywhere a type constructor of kind * -> * can be used. foo :: (Functor (Foo a)) => ... -- invalid bar :: (Functor (Bar a)) => ... -- valid -- Dave Menendez <d...@zednenem.com> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe