HList with DataKinds, kind not promotable

Question

I have this code snippet which uses a plethora of GHC extensions:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.Exts (Constraint)

data HList :: [*] -> * where
    Nil  :: HList '[]
    Cons :: a -> HList l -> HList (a ': l)

type family All (p :: * -> Constraint) (xs :: HList [*]) :: Constraint where
    All p Nil = ()
    All p (Cons x xs) = (p x, All p xs)

GHC complains that:

 ‘HList’ of kind ‘[*] -> *’ is not promotable
    In the kind ‘HList [*]’

Why can't I promote HList to a kind? I get the same error using GHC 7.8.2 and 7.11.

Of course, using the builtin '[] works just fine:

type family All (p :: * -> Constraint) (xs :: [*]) :: Constraint where
    All p '[]       = ()
    All p (x ': xs) = (p x, All p xs)

I want to use my own HList instead of '[] because the actual HList supports appending and looks like this:

type family (:++:) (xs :: [*]) (ys :: [*]) where
    '[] :++:  ys = ys
     xs :++: '[] = xs
    (x ': xs) :++: ys = x ': (xs :++: ys)

data HList :: [*] -> * where
    Nil  :: HList '[]
    Cons :: a -> HList l -> HList (a ': l)
    App  :: Hlist a -> HList b -> HList (a :++: b)

EDIT: The main goal is to have GHC infer

(All p xs, All p ys) ==> All p (xs :++: ys)

so that I can write

data Dict :: Constraint -> * where
    Dict :: c => Dict c

witness :: Dict (All p xs) -> Dict (All p ys) -> Dict (All p (xs :++: ys))
witness Dict Dict = Dict

I had hoped that adding an explicit representation for appending type-level lists would help me achieve this. Is there another way to convince GHC of the above?

Answer 1

I see now that the question is how to write a proof of (All p xs, All p ys) => All p (xs :++: ys). The answer is, by induction, of course!

The type of the function we really want to write is

allAppend :: (p :: Constraint) -> (xs :: [*]) -> (ys :: [*]) 
          -> (All p xs, All p ys) -> All p (xs :++: ys)

but Haskell doesn't have dependent types. "Faking" dependent types usually means having a witness that carries a proof that a type exists. This makes things somewhat tedious, but currently there is no other way. We already have a witness for a list xs - it is precisely HList xs. For constraints, we will use

data Dict p where Dict :: p => Dict p

Then we can write implication as a simple function:

type (==>) a b = Dict a -> Dict b 

So our type becomes:

allAppend :: Proxy p -> HList xs -> HList ys 
          -> (All p xs, All p ys) ==> (All p (xs :++: ys))

The body of the function is quite straightforward - note how each pattern in allAppend matches each pattern in the definition of :++::

allAppend _ Nil _  Dict = Dict  
allAppend _ _  Nil Dict = Dict 
allAppend p (Cons _ xs) ys@(Cons _ _) Dict = 
  case allAppend p xs ys Dict of Dict -> Dict 

The opposite entailment All p (xs :++: ys) => (All p xs, All p ys) also holds. In fact, the function definition is identical.