I ran into problems when I tryed doing some of
the Conor's talk at ICFP 2012 in Haskell with
DataKinds and PolyKinds extension, using GHC 7.4.1.

I am wondering whether this is a bug in GHC 7.4.1
(maybe fixed in GHC 7.6.x? haven't tried since
I haven't installed 7.6.x yet), or a limitation of
datatype promotion itself. The problem happens when
I try to use promoted list datatype.

Here is a code that illustrates this problem:

> {-# LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures #-}
>
> data GList x i j where
>   GNil   :: GList x i i
>   GCons  :: x i j  -> GList x j k
>                    -> GList x i k
> 
> 
> append :: GList x i j  -> GList x j k
>                        -> GList x i k
> append GNil            ys  = ys
> append (  GCons x xs)  ys  =
>           GCons x (append xs ys)


Instantiating to a plain regular list works

> data Elem a i j where
>   MkElem :: a -> Elem a () ()
> 
> type List' a = GList (Elem a) () ()
> 
> nil' = GNil {-"~"-} :: List' a
> 
> cons' :: a -> List' a -> List' a
> cons' = GCons . MkElem

Instantiating to a length indexed list works

> data Nat = Z | S Nat
> 
> data ElemV a i j where
>   MkElemV :: a -> ElemV a (S n) n
> 
> type Vec a n = GList (ElemV a) n Z
> 
> vNil = GNil {-"~"-} :: Vec a Z
> 
> vCons :: a -> Vec a n -> Vec a (S n)
> vCons = GCons . MkElemV

Good, then let's do some more things with DataKinds.

Promoting Bool works as well as Nat.

> data RelB :: Bool -> Bool -> * where
>   MkRelB :: RelB b b
> 
> l1 = GCons MkRelB GNil

But, I have some problems with promoting [Bool] !!!

> data RelBL :: [Bool] -> [Bool] -> * where
>   MkRelBL :: RelBL bs bs

I can only with mono-kinded list structure.
Below is a momomorphization of GList.

> data MyList (x :: [Bool] -> [Bool] -> *) i j where
>   MyNil   :: MyList x i i
>   MyCons  :: x i j  -> MyList x j k
>                     -> MyList x i k
> 
> l3 = MyCons MkRelBL MyNil

However when I try to do this with the poly-kinded GList,
I get a kind error. Is this a bug of GHC 7.4.1 or is this
a limitation of DataKind extension?

> l4 = GCons MkRelBL GNil

tmp.lhs:74:22:
    Couldn't match kind `BOX' against `*'
    Kind incompatibility when matching types:
      k0 :: BOX
      [Bool] :: *
    In the second argument of `GCons', namely `GNil'
    In the expression: GCons MkRelBL GNil