On 18 May 2013 11:16, TP <
paratribulations@free.fr> wrote:
<snip>
>
> However, I have not managed to make the version with forall work. Below, the
> first occurrence of forall is ok, but the three following yield error.
>
> ----------------------------
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE StandaloneDeriving #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE ExplicitForAll #-}
>
> data Gender = Male | Female
> data Person :: Gender -> * where
> Dead :: forall (a :: Gender). Person a
> Alive :: { name :: String
> , weight :: Float
> , father :: forall (a :: Gender). Person a } -> forall (b ::
> Gender). Person b
The foralls should be in front of all the data constructor parameters, like with the
Dead constructor, since you want to quantify a and b over the whole type signature:
data Person :: Gender -> * where
Dead :: forall (a :: Gender). Person a
Alive :: forall (a :: Gender) (b :: Gender).
{ name :: String
, weight :: Float
, father :: Person a } -> Person b
> deriving instance Show (forall (a :: Gender). Person a)
Again, you should quantify over Show as well:
deriving instance forall (a :: Gender). Show (Person a)
Note that all of this would work even without explicit quantification since you
have already specified that Person accepts an argument of kind Gender. In other
words, this works as expected:
data Person :: Gender -> * where
Dead :: Person a
Alive :: { name :: String
, weight :: Float
, father :: Person b } -> Person a
deriving instance Show (Person a)
You also probably want father :: Person Male, since a father cannot be Female
(presumably!).