{-# LANGUAGE GADTs, DataKinds, TypeOperators, FlexibleContexts, FlexibleInstances #-}
data HList ty where
Nil :: HList '[]
(:>) :: h -> HList t -> HList (h ': t)
infixr 5 :>
instance Show (HList '[]) where
show _ = "[]"
instance (Show h, Show (HList t)) => Show (HList (h ': t)) where
show (h :> t) = let '[':s = show t in
"[" ++ show h ++ (if s == "]" then s else " :> " ++ s)
data Elem tys ty where
EZ :: Elem (x ': xs) x
ES :: Elem xs x -> Elem (y ': xs) x
get :: Elem tys ty -> HList tys -> ty
get EZ (h :> _) = h
get (ES elems) (_ :> t) = get elems t
main = do
let myList = True :> [1,2,3,4] :> () :> ('c' :> [1,2] :> Nil) :> 42 :> Nil
print myList
putStrLn "----"
print $ get EZ myList
print $ get (ES (ES (ES EZ))) myList
