Deko-Typ-Ebenenliste mit zusätzlichen Informationen aus der Typ-Level-Map

Question

Ich habe diese heterogene Liste, deren Typ die Typen der darin enthaltenen Werte widerspiegelt. Ich kann durch Überprüfung aller Elemente in Strings umwandeln, dass jede Art erfüllt eine Einschränkung enthalten:

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeApplications #-} 

import GHC.Exts 
import GHC.TypeLits 

import Data.Proxy 

type family AllSatisfy (f :: k -> Constraint) (xs :: [k]) :: Constraint where 
    AllSatisfy f '[] =() 
    AllSatisfy f (x ': xs) = (f x, AllSatisfy f xs) 

data HList (as :: [*]) where 
    HNil :: HList '[] 
    HCons :: a -> HList as -> HList (a ': as) 

type family Keys (xs :: [(a, b)]) :: [a] where 
    Keys '[] = '[] 
    Keys ('(a, b) ': xs) = a ': Keys xs 

type family Values (xs :: [(a, b)]) :: [b] where 
    Values '[] = '[] 
    Values ('(a, b) ': xs) = b ': Values xs 

showHList :: AllSatisfy Show xs => HList xs -> [String] 
showHList HNil = [] 
showHList (HCons x xs) = show x : showHList xs 

Was ich in der Lage sein möchten, wird über eine Typ-Ebene Assoziationsliste einige zusätzliche Informationen zu tun geben, das ist durch die Typen im HList indiziert. Etwas wie:

showWithKey :: forall (keyMap :: [(*, Symbol)]) (b :: Symbol) (rest :: [(*, Symbol)]). 
       (AllSatisfy Show (Keys keyMap) 
       ,AllSatisfy KnownSymbol (Values keyMap) 
       ) => 
       Proxy keyMap -> HList (Keys keyMap) -> [(String, String)] 
showWithKey _ HNil = [] 
showWithKey _ (HCons (x :: a) (xs :: HList as)) = 
    let p = (Proxy @keyMap) :: Proxy ('(a, b) ': rest) 
    in (show x, symbolVal (Proxy @b)) : (showWithKey (Proxy @rest) xs) 

Nun, es ist klar zu sehen, dass, wenn (Keys keyMap) nicht leer ist, dann keyMap, aber GHC kämpft dies herausgefunden:

Could not deduce: keyMap ~ ('(a, b) : rest) 
     from the context: (AllSatisfy Show (Keys keyMap), 
         AllSatisfy KnownSymbol (Values keyMap)) 
     bound by the type signature for: 
        showWithKey :: (AllSatisfy Show (Keys keyMap), 
            AllSatisfy KnownSymbol (Values keyMap)) => 
            Proxy keyMap -> HList (Keys keyMap) -> [(String, String)] 
     or from: Keys keyMap ~ (a : as) 
     bound by a pattern with constructor: 
        HCons :: forall a (as :: [ghc-prim-0.5.0.0:GHC.Types.*]). 
          a -> HList as -> HList (a : as), 
       in an equation for ‘showWithKey’ 
     ‘keyMap’ is a rigid type variable bound by 
     the type signature for: 
      showWithKey :: forall (keyMap :: [(ghc-prim-0.5.0.0:GHC.Types.*, 
              Symbol)]) (b :: Symbol) (rest :: [(ghc-prim-0.5.0.0:GHC.Types.*, 
                       Symbol)]). 
         (AllSatisfy Show (Keys keyMap), 
          AllSatisfy KnownSymbol (Values keyMap)) => 
         Proxy keyMap -> HList (Keys keyMap) -> [(String, String)] 
     Expected type: Proxy ('(a, b) : rest) 
     Actual type: Proxy keyMap 

Wie kann ich das so umschreiben, dass GHC kann Dinge herausfinden?

Answer 1

Nehmen wir einige Hinweise, was user2407038 sagte, ich erstellte eine konkrete Darstellung des depMap Typs und erstellte dann eine Typklasse, um einen nicht-ganz-Singleton-aber-zumindest-kanonischen Wert vom Typ zu beschreiben.

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeApplications #-} 
{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE AllowAmbiguousTypes #-} 

import GHC.Exts 
import GHC.TypeLits 

import Data.Proxy 

type family AllSatisfy (f :: k -> Constraint) (xs :: [k]) :: Constraint where 
    AllSatisfy f '[] =() 
    AllSatisfy f (x ': xs) = (f x, AllSatisfy f xs) 

data HList (as :: [*]) where 
    HNil :: HList '[] 
    HCons :: a -> HList as -> HList (a ': as) 

type family Keys (xs :: [(a, b)]) :: [a] where 
    Keys '[] = '[] 
    Keys ('(a, b) ': xs) = a ': Keys xs 

type family Values (xs :: [(a, b)]) :: [b] where 
    Values '[] = '[] 
    Values ('(a, b) ': xs) = b ': Values xs 

showHList :: AllSatisfy Show xs => HList xs -> [String] 
showHList HNil = [] 
showHList (HCons x xs) = show x : showHList xs 

data SKeyMap :: [(*, Symbol)] -> * where 
    SKeyNil :: SKeyMap '[] 
    SKeyCons :: Proxy a -> Proxy s -> SKeyMap xs -> SKeyMap ('(a, s) ': xs) 

class KnownKeyMap (keyMap :: [(*, Symbol)]) where 
    sKeyMap :: SKeyMap keyMap 


instance KnownKeyMap '[] where 
    sKeyMap = SKeyNil 

instance KnownKeyMap keyMap => KnownKeyMap ('(a, s) ': keyMap) where 
    sKeyMap = SKeyCons Proxy Proxy sKeyMap 

showWithKey' :: forall (keyMap :: [(*, Symbol)]) . 
       (AllSatisfy Show (Keys keyMap) 
       ,AllSatisfy KnownSymbol (Values keyMap) 
       ) => 
       SKeyMap keyMap -> HList (Keys keyMap) -> [(String, String)] 
showWithKey' SKeyNil HNil = [] 
showWithKey' (SKeyCons _ sp skRest) (HCons (x :: a) (xs :: HList as)) = 
    (show x, symbolVal sp) : (showWithKey' skRest xs) 

showWithKey :: forall (keyMap :: [(*, Symbol)]) . 
       (KnownKeyMap keyMap 
       ,AllSatisfy Show (Keys keyMap) 
       ,AllSatisfy KnownSymbol (Values keyMap) 
       ) => 
       HList (Keys keyMap) -> [(String, String)] 
showWithKey = showWithKey' (sKeyMap @keyMap)