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