Kind refinement in type families with PolyKinds

[José Pedro Magalhães]

Hi all,

I'm wondering why the following does not work:

{-# LANGUAGE DataKinds          #-}
> {-# LANGUAGE PolyKinds          #-}
> {-# LANGUAGE KindSignatures     #-}
> {-# LANGUAGE TypeFamilies       #-}
> {-# LANGUAGE GADTs              #-}
> {-# LANGUAGE TypeOperators      #-}
>
> module Bug where
>
> -- Type equality
> data a :=: b where Refl :: a :=: a
>
> -- Applying a type to a list of arguments
> type family Apply (t :: k) (ts :: [*]) :: *
> type instance Apply t             '[]       = t
> type instance Apply (f :: * -> *) (t ': ts) = f t
>
> -- Stripping a type from all its arguments
> type family Strip (t :: *) :: k
> type instance Strip (Maybe a) = Maybe
>
> -- Reapplying a stripped type is the identity
> x :: Apply (Strip (Maybe a)) (a ': '[]) :=: Maybe a
> x = Refl
>

If I ask GHCi for the kind of `Strip (Maybe Int)`, I get `k`, whereas I
would expect `* -> *`.
That explains why the `Apply` type family is not reduced further.

I understand that this might be related to GADTs not being allowed to
refine kinds;
the following datatype fails to compile with the error "`D1' cannot be
GADT-like
in its *kind* arguments":

data DStrip :: k -> * where
>   D1 :: DStrip Maybe
>

But then, shouldn't the type instance for `Strip` above trigger the same
error?


Thanks,
Pedro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20121030/3f4a7c6f/attachment.htm>