Kind refinement in type families with PolyKinds

[Simon Peyton-Jones]

I think the issue is this.  We have
          Strip :: forall k. * -> k

When you say
type instance Strip (Maybe a) = Maybe
GHC infers the kind arguments (as with all hidden argument) to get

          type instance Strip (*->*) (Maybe a) = Maybe

It would be fine to have another type instance like this
type instance Strip (Maybe a) = Int
which would turn into
          type instance Strip * (Maybe a) = Maybe

In all cases, an occurrence of (Strip <kind> <type>) will match one of the "type instances" only if, well, it matches, including the kind.

Does that answer the question.

I would love someone to write some user guidance notes about this kind of thing, perhaps as a new sub-page of
http://www.haskell.org/haskellwiki/GHC/Type_system

Simon


From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-bounces at haskell.org] On Behalf Of José Pedro Magalhães
Sent: 30 October 2012 10:29
To: GHC users
Subject: Kind refinement in type families with PolyKinds

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/20121031/cef1142b/attachment.htm>