    {-# LANGUAGE CPP #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE FlexibleContexts #-}

    -- | A GADT HList implementation
    --
    -- There exist other implementations of HList on hackage, but none seem to
    -- be reliably maintained.
    module Data.HList.HList
      ( HList(..)
      , Append
      , hAppend
      , HInit(..)
    ) where

    import Prelude hiding (reverse)

    import Data.Kind (Type)
    import Data.Monoid (Monoid, mappend, mempty)
    import Data.Semigroup

    import Data.Proxy

    data HList :: [Type] -> Type where
      HNil :: HList '[]
      (:+:) :: x -> HList xs -> HList (x ': xs)
      -- TCons :: x -> HList xs -> HList (Cons x xs)
      -- TNull :: HList Null

    infixr 5 :+:

    instance Show (HList '[]) where
      show :: HList '[] -> String
    show HList '[]
    _ = String
    "HNil"

    instance (Show a, Show (HList b)) => Show (HList (a ': b)) where
      show :: HList (a : b) -> String
    show (x
    x :+: HList xs
    y) = String
    "(" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ x -> String
    forall a. Show a => a -> String
    show x
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ":+:" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ HList xs -> String
    forall a. Show a => a -> String
    show HList xs
    y String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

    instance Semigroup (HList '[]) where
      HList '[]
    _ <> :: HList '[] -> HList '[] -> HList '[]
    <> HList '[]
    _ = HList '[]
    HNil
    instance (Semigroup x, Semigroup (HList xs))
          => Semigroup (HList (x ': xs))
      where
        (x
    x1 :+: HList xs
    xs1) <> :: HList (x : xs) -> HList (x : xs) -> HList (x : xs)
    <> (x
    x2 :+: HList xs
    xs2) = (x
    x
    x1 x -> x -> x
    forall a. Semigroup a => a -> a -> a
    <> x
    x
    x2) x -> HList xs -> HList (x : xs)
    forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
    :+: (HList xs
    HList xs
    xs1 HList xs -> HList xs -> HList xs
    forall a. Semigroup a => a -> a -> a
    <> HList xs
    HList xs
    xs2)

    instance Monoid (HList '[]) where
      mempty :: HList '[]
    mempty = HList '[]
    HNil
      mappend :: HList '[] -> HList '[] -> HList '[]
    mappend = HList '[] -> HList '[] -> HList '[]
    forall a. Semigroup a => a -> a -> a
    (<>)
    instance (Semigroup x, Monoid x, Semigroup (HList xs), Monoid (HList xs))
          => Monoid (HList (x ': xs))
      where
        mempty :: HList (x : xs)
    mempty = x
    forall a. Monoid a => a
    mempty x -> HList xs -> HList (x : xs)
    forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
    :+: HList xs
    forall a. Monoid a => a
    mempty
        mappend :: HList (x : xs) -> HList (x : xs) -> HList (x : xs)
    mappend = HList (x : xs) -> HList (x : xs) -> HList (x : xs)
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance Eq (HList '[]) where
      HList '[]
    HNil == :: HList '[] -> HList '[] -> Bool
    == HList '[]
    HNil = Bool
    True
      HList '[]
    HNil /= :: HList '[] -> HList '[] -> Bool
    /= HList '[]
    HNil = Bool
    False

    instance (Eq x, Eq (HList xs))
          => Eq (HList (x ': xs))
      where
        x
    x1 :+: HList xs
    xr1 == :: HList (x : xs) -> HList (x : xs) -> Bool
    == x
    x2 :+: HList xs
    xr2 = x
    x1x -> x -> Bool
    forall a. Eq a => a -> a -> Bool
    ==x
    x
    x2 Bool -> Bool -> Bool
    && HList xs
    xr1HList xs -> HList xs -> Bool
    forall a. Eq a => a -> a -> Bool
    ==HList xs
    HList xs
    xr2
        x
    x1 :+: HList xs
    xr1 /= :: HList (x : xs) -> HList (x : xs) -> Bool
    /= x
    x2 :+: HList xs
    xr2 = x
    x1x -> x -> Bool
    forall a. Eq a => a -> a -> Bool
    /=x
    x
    x2 Bool -> Bool -> Bool
    || HList xs
    xr1HList xs -> HList xs -> Bool
    forall a. Eq a => a -> a -> Bool
    /=HList xs
    HList xs
    xr2

    -- cannot use the closed variant because of ghc-7.8.4.
    -- (was not investigated more closely; there simply
    --  is some syntax error for code which works fine with ghc-7.10.)
    type family Append (l1::[Type]) (l2::[Type]) :: [Type]
    type instance Append '[] l2 = l2
    type instance Append (car1 ': cdr2) l2 = car1 ': Append cdr2 l2

    hAppend :: HList ts1 -> HList ts2 -> HList (Append ts1 ts2)
    hAppend :: forall (ts1 :: [*]) (ts2 :: [*]).
    HList ts1 -> HList ts2 -> HList (Append ts1 ts2)
    hAppend HList ts1
    HNil HList ts2
    l = HList ts2
    HList (Append ts1 ts2)
    l
    hAppend (x
    x:+:HList xs
    xs) HList ts2
    l = x
    x x -> HList (Append xs ts2) -> HList (x : Append xs ts2)
    forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
    :+: HList xs -> HList ts2 -> HList (Append xs ts2)
    forall (ts1 :: [*]) (ts2 :: [*]).
    HList ts1 -> HList ts2 -> HList (Append ts1 ts2)
    hAppend HList xs
    xs HList ts2
    l

    class HInit (l1 :: [Type]) where
      hInit :: forall l2 . Proxy l2 -> HList (Append l1 l2) -> HList l1
      hSplit :: forall l2 . HList (Append l1 l2) -> (HList l1, HList l2)

    instance HInit '[] where
      hInit :: forall (l2 :: [*]). Proxy l2 -> HList (Append '[] l2) -> HList '[]
    hInit Proxy l2
    _ HList (Append '[] l2)
    _ = HList '[]
    HNil
      hSplit :: forall (l2 :: [*]). HList (Append '[] l2) -> (HList '[], HList l2)
    hSplit HList (Append '[] l2)
    l = (HList '[]
    HNil, HList l2
    HList (Append '[] l2)
    l)
    instance HInit l1 => HInit (x ': l1) where
      hInit :: forall (l2 :: [*]).
    Proxy l2 -> HList (Append (x : l1) l2) -> HList (x : l1)
    hInit Proxy l2
    p (x
    x :+: HList xs
    xs)  = x
    x
    x x -> HList l1 -> HList (x : l1)
    forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
    :+: Proxy l2 -> HList (Append l1 l2) -> HList l1
    forall (l2 :: [*]). Proxy l2 -> HList (Append l1 l2) -> HList l1
    forall (l1 :: [*]) (l2 :: [*]).
    HInit l1 =>
    Proxy l2 -> HList (Append l1 l2) -> HList l1
    hInit Proxy l2
    p HList xs
    HList (Append l1 l2)
    xs
    #if !MIN_VERSION_base(4,9,0)
      hInit _ _           = error "cannot happen" -- see ghc trac #3927
    #endif
      hSplit :: forall (l2 :: [*]).
    HList (Append (x : l1) l2) -> (HList (x : l1), HList l2)
    hSplit (x
    x :+: HList xs
    xs) = let (HList l1
    l1, HList l2
    l2) = HList (Append l1 l2) -> (HList l1, HList l2)
    forall (l1 :: [*]) (l2 :: [*]).
    HInit l1 =>
    HList (Append l1 l2) -> (HList l1, HList l2)
    forall (l2 :: [*]). HList (Append l1 l2) -> (HList l1, HList l2)
    hSplit HList xs
    HList (Append l1 l2)
    xs
                           in (x
    x
    x x -> HList l1 -> HList (x : l1)
    forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
    :+: HList l1
    l1, HList l2
    l2)
    #if !MIN_VERSION_base(4,9,0)
      hSplit _          = error "cannot happen"
    #endif