HList с DataKinds, вид не продвигается

Question

У меня есть этот фрагмент кода, который использует множество расширений GHC:

{-# 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 жалуется, что:

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

Почему я не могу продвинуть HList к виду? Я получаю ту же ошибку, используя GHC 7.8.2 а также 7.11,

Конечно, используя встроенный '[] работает просто отлично

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

Я хочу использовать свой собственный HList вместо '[] потому что фактический HList поддерживает добавление и выглядит так:

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)

РЕДАКТИРОВАТЬ: Основная цель состоит в том, чтобы сделать вывод GHC

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

так что я могу написать

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

Я надеялся, что добавление явного представления для добавления списков на уровне типов поможет мне достичь этого. Есть ли другой способ убедить GHC в вышесказанном?

Answer 1

Теперь я вижу, что вопрос в том, как написать доказательство (All p xs, All p ys) => All p (xs :++: ys), Ответ, по индукции, конечно!

Тип функции, которую мы действительно хотим написать:

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

но у Haskell нет зависимых типов. "Подделка" зависимых типов обычно означает наличие свидетеля, который несет доказательство того, что тип существует. Это делает вещи несколько утомительными, но в настоящее время другого пути нет. У нас уже есть свидетель для списка xs - это точно HList xs, Для ограничений мы будем использовать

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

Тогда мы можем записать импликацию как простую функцию:

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

Таким образом, наш тип становится:

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

Тело функции довольно просто - обратите внимание, как каждый шаблон в allAppend соответствует каждому шаблону в определении :++::

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

Обратное вложение All p (xs :++: ys) => (All p xs, All p ys) тоже держит. На самом деле, определение функции идентично.