{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}          -- Enabled by default apparently
{-# LANGUAGE TypeOperators #-}  -- Enabled by default apparently
{-# LANGUAGE TypeFamilies #-}


data HList :: (* -> *) -> [*] -> * where
  HNil :: HList f '[]
  HCons :: f t -> HList f ts -> HList f (t':ts)


-- Example hlists
-- a = HCons 3 HNil




---------------------------------------------------------------------------  

-- data Hlist :: [*] -> * where
--   HNil :: Hlist '[]
--   HCons :: t -> Hlist ts -> Hlist (t : ts)

-- data Member :: a -> [*] -> * where 
--   First :: Member x (y:l)
--   Next :: Member x l -> Member x (y:l)

-- hd :: Hlist (t ': ts) -> t  
-- hd (HCons x _) = x

-- tl :: Hlist (t ': ts) -> Hlist ts
-- tl (HCons _ xs) = xs

-- len :: Hlist ts -> Int
-- len HNil = 0
-- len (HCons _ xs) = 1 + (len xs)

-- type family (++) (l1 :: [*]) (l2 :: [*]) where
--   '[] ++ y = y
--   (x':xs) ++ y = x':(xs ++ y)

-- cat :: Hlist ts1 -> Hlist ts2 -> Hlist (ts1 ++ ts2)  
-- cat HNil y = y
-- cat (HCons x xs) y = HCons x (cat xs y)




-- -- Example hlists
-- a = HCons 3 HNil 
-- b = HCons 3 (HCons True HNil)
-- -- λ> a
-- -- a :: Hlist '[Integer]
-- -- λ> b
-- -- b :: Hlist '[Integer, Bool]
-- -- λ> tl a
-- --
-- -- tl a :: Hlist '[]
-- -- λ> tl b
-- -- tl b :: Hlist '[Bool]
-- -- λ> hd a
-- -- 3
-- -- λ> hd (tl b)
-- -- True
-- -- λ> hd $ tl (tl b)  -- Error
-- --
-- -- λ> cat b b
-- -- cat b b :: Hlist '[Integer, Bool, Integer, Bool]