## Kind refinement in type families with PolyKinds

2012-10-30 10:28:54 GMT

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

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users <at> haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users