Kind refinement in type families with PolyKinds
José Pedro Magalhães
jpm at cs.uu.nl
Tue Oct 30 11:28:54 CET 2012
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>
More information about the Glasgow-haskell-users
mailing list