Heterogenous list (product) that applies a type

hklist.hs

{-# LANGUAGE PolyKinds, DataKinds, GADTs, TypeOperators, ConstraintKinds, RankNTypes, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}

import Data.Proxy
import Data.Functor.Identity
import GHC.Exts (Constraint)

data HKList :: (k -> *) -> [k] -> * where
  Nil  :: HKList f '[]
  (:*) :: f x -> HKList f xs -> HKList f (x ': xs)
 
-- From constraints
data Dict :: Constraint -> * where
  Dict :: a => Dict a
  
data Dict1 :: (k -> Constraint) -> k -> * where
  Dict1 :: c k => Dict1 c k
  
data Has c a where
  Has :: c a => a -> Has c a
  
type ConstrainedList c = HKList (Has c)

-- from constraints
newtype a :- b = Sub (a => Dict b)

type SList = HKList Proxy

class All c xs where
  dicts :: HKList (Dict1 c) xs
  
instance All c '[] where
  dicts = Nil

instance (All c xs, c x) => All c (x ': xs) where
  dicts = Dict1 :* dicts
  
zipHKList :: (forall k. f k -> g k -> h k) -> HKList f xs -> HKList g xs -> HKList h xs
zipHKList _ Nil Nil = Nil
zipHKList f (x :* xs) (y :* ys) = f x y :* zipHKList f xs ys

allToHas :: All c xs => HKList Identity xs -> HKList (Has c) xs
allToHas xs = zipHKList f dicts xs
  where
    f :: Dict1 c k -> Identity k -> Has c k
    f Dict1 (Identity x) = Has x

hasToAll :: HKList (Has c) xs -> Dict (All c xs)
hasToAll Nil = Dict
hasToAll (Has x :* xs) =
  case hasToAll xs of
    Dict -> Dict