    {-# LANGUAGE AllowAmbiguousTypes    #-}
    {-# LANGUAGE ConstraintKinds        #-}
    {-# LANGUAGE FlexibleContexts       #-}
    {-# LANGUAGE FlexibleInstances      #-}
    {-# LANGUAGE FunctionalDependencies #-}
    {-# LANGUAGE GADTs                  #-}
    {-# LANGUAGE ScopedTypeVariables    #-}
    {-# LANGUAGE TupleSections          #-}
    {-# LANGUAGE TypeApplications       #-}
    {-# LANGUAGE TypeFamilies           #-}
    {-# LANGUAGE TypeInType             #-}
    {-# LANGUAGE TypeOperators          #-}
    {-# LANGUAGE UndecidableInstances   #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Generics.Product.Internal.HList
    -- Copyright   :  (C) 2020 Csongor Kiss
    -- License     :  BSD3
    -- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Derive an isomorphism between a product type and a flat HList.
    --
    -----------------------------------------------------------------------------

    module Data.Generics.Product.Internal.HList
      ( GIsList(..)
      , IndexList (..)
      , HList (..)
      , type (++)
      , Elem
      , ListTuple (..)
      , TupleToList
      ) where

    import GHC.TypeLits

    import Data.Kind    (Type)
    import GHC.Generics
    import Data.Profunctor.Indexed
    import Data.Generics.Internal.Profunctor.Lens
    import Data.Generics.Internal.Profunctor.Iso

    data HList (as :: [Type]) where
      Nil :: HList '[]
      (:>) :: a -> HList as -> HList (a ': as)

    infixr 5 :>

    type family ((as :: [k]) ++ (bs :: [k])) :: [k] where
      '[]       ++ bs = bs
      (a ': as) ++ bs = a ': as ++ bs

    instance Semigroup (HList '[]) where
      HList '[]
    _ <> :: HList '[] -> HList '[] -> HList '[]
    <> HList '[]
    _ = HList '[]
    Nil

    instance Monoid (HList '[]) where
      mempty :: HList '[]
    mempty  = HList '[]
    Nil
      mappend :: HList '[] -> HList '[] -> HList '[]
    mappend HList '[]
    _ HList '[]
    _ = HList '[]
    Nil

    instance (Semigroup a, Semigroup (HList as)) => Semigroup (HList (a ': as)) where
      (a
    x :> HList as
    xs) <> :: HList (a : as) -> HList (a : as) -> HList (a : as)
    <> (a
    y :> HList as
    ys) = (a
    a
    x a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    a
    y) a -> HList as -> HList (a : as)
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> (HList as
    HList as
    xs HList as -> HList as -> HList as
    forall a. Semigroup a => a -> a -> a
    <> HList as
    HList as
    ys)

    instance (Monoid a, Monoid (HList as)) => Monoid (HList (a ': as)) where
      mempty :: HList (a : as)
    mempty = a
    forall a. Monoid a => a
    mempty a -> HList as -> HList (a : as)
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList as
    forall a. Monoid a => a
    mempty
      mappend :: HList (a : as) -> HList (a : as) -> HList (a : as)
    mappend (a
    x :> HList as
    xs) (a
    y :> HList as
    ys) = a -> a -> a
    forall a. Monoid a => a -> a -> a
    mappend a
    a
    x a
    a
    y a -> HList as -> HList (a : as)
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList as -> HList as -> HList as
    forall a. Monoid a => a -> a -> a
    mappend HList as
    HList as
    xs HList as
    HList as
    ys

    class Elem (as :: [(k, Type)]) (key :: k) (i :: Nat) a | as key -> i a
    instance {-# OVERLAPPING #-} pos ~ 0 => Elem (a ': xs) key pos a
    instance (Elem xs key i a, pos ~ (i + 1)) => Elem (x ': xs) key pos a

    class GIsList
      (f :: Type -> Type)
      (g :: Type -> Type)
      (as :: [Type])
      (bs :: [Type]) | f -> as, g -> bs, bs f -> g, as g -> f where

      glist :: Iso (f x) (g x) (HList as) (HList bs)

    instance
      ( GIsList l l' as as'
      , GIsList r r' bs bs'
      , Appending as bs cs as' bs' cs'
      , cs ~ (as ++ bs)
      , cs' ~ (as' ++ bs')
      ) => GIsList (l :*: r) (l' :*: r') cs cs' where

      glist :: forall x. Iso ((:*:) l r x) ((:*:) l' r' x) (HList cs) (HList cs')
    glist = p i (l x, r x) (l' x, r' x) -> p i ((:*:) l r x) ((:*:) l' r' x)
    forall (a :: * -> *) (b :: * -> *) x (a' :: * -> *) (b' :: * -> *)
           (p :: * -> * -> * -> *) i.
    Profunctor p =>
    p i (a x, b x) (a' x, b' x) -> p i ((:*:) a b x) ((:*:) a' b' x)
    prodIso (p i (l x, r x) (l' x, r' x) -> p i ((:*:) l r x) ((:*:) l' r' x))
    -> (p i (HList cs) (HList cs') -> p i (l x, r x) (l' x, r' x))
    -> p i (HList cs) (HList cs')
    -> p i ((:*:) l r x) ((:*:) l' r' x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Iso (l x) (l' x) (HList as) (HList as')
    -> Iso (r x) (r' x) (HList bs) (HList bs')
    -> Iso
         (l x, r x) (l' x, r' x) (HList as, HList bs) (HList as', HList bs')
    forall s t a b s' t' a' b'.
    Iso s t a b
    -> Iso s' t' a' b' -> Iso (s, s') (t, t') (a, a') (b, b')
    pairing p i (HList as) (HList as') -> p i (l x) (l' x)
    forall x. Iso (l x) (l' x) (HList as) (HList as')
    forall (f :: * -> *) (g :: * -> *) (as :: [*]) (bs :: [*]) x.
    GIsList f g as bs =>
    Iso (f x) (g x) (HList as) (HList bs)
    Iso (l x) (l' x) (HList as) (HList as')
    glist p i (HList bs) (HList bs') -> p i (r x) (r' x)
    forall x. Iso (r x) (r' x) (HList bs) (HList bs')
    forall (f :: * -> *) (g :: * -> *) (as :: [*]) (bs :: [*]) x.
    GIsList f g as bs =>
    Iso (f x) (g x) (HList as) (HList bs)
    Iso (r x) (r' x) (HList bs) (HList bs')
    glist (p i (HList as, HList bs) (HList as', HList bs')
     -> p i (l x, r x) (l' x, r' x))
    -> (p i (HList cs) (HList cs')
        -> p i (HList as, HList bs) (HList as', HList bs'))
    -> p i (HList cs) (HList cs')
    -> p i (l x, r x) (l' x, r' x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i (HList cs) (HList cs')
    -> p i (HList as, HList bs) (HList as', HList bs')
    forall (as :: [*]) (bs :: [*]) (cs :: [*]) (as' :: [*])
           (bs' :: [*]) (cs' :: [*]).
    Appending as bs cs as' bs' cs' =>
    Iso
      (HList as, HList bs) (HList as', HList bs') (HList cs) (HList cs')
    Iso
      (HList as, HList bs) (HList as', HList bs') (HList cs) (HList cs')
    appending
      {-# INLINE glist #-}

    instance GIsList f g as bs => GIsList (M1 t meta f) (M1 t meta g) as bs where
      glist :: forall x. Iso (M1 t meta f x) (M1 t meta g x) (HList as) (HList bs)
    glist = p i (f x) (g x) -> p i (M1 t meta f x) (M1 t meta g x)
    forall i1 (c :: Meta) (f :: * -> *) p1 (g :: * -> *)
           (p2 :: * -> * -> * -> *) i2.
    Profunctor p2 =>
    p2 i2 (f p1) (g p1) -> p2 i2 (M1 i1 c f p1) (M1 i1 c g p1)
    mIso (p i (f x) (g x) -> p i (M1 t meta f x) (M1 t meta g x))
    -> (p i (HList as) (HList bs) -> p i (f x) (g x))
    -> p i (HList as) (HList bs)
    -> p i (M1 t meta f x) (M1 t meta g x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i (HList as) (HList bs) -> p i (f x) (g x)
    forall x. Iso (f x) (g x) (HList as) (HList bs)
    forall (f :: * -> *) (g :: * -> *) (as :: [*]) (bs :: [*]) x.
    GIsList f g as bs =>
    Iso (f x) (g x) (HList as) (HList bs)
    glist
      {-# INLINE glist #-}

    instance GIsList (Rec0 a) (Rec0 b) '[a] '[b] where
      glist :: forall x. Iso (Rec0 a x) (Rec0 b x) (HList '[a]) (HList '[b])
    glist = p i a b -> p i (K1 R a x) (K1 R b x)
    forall r a p1 b (p2 :: * -> * -> * -> *) i.
    Profunctor p2 =>
    p2 i a b -> p2 i (K1 r a p1) (K1 r b p1)
    kIso (p i a b -> p i (K1 R a x) (K1 R b x))
    -> (p i (HList '[a]) (HList '[b]) -> p i a b)
    -> p i (HList '[a]) (HList '[b])
    -> p i (K1 R a x) (K1 R b x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i (HList '[a]) (HList '[b]) -> p i a b
    forall a b (p :: * -> * -> * -> *) i.
    Profunctor p =>
    p i (HList '[a]) (HList '[b]) -> p i a b
    singleton
      {-# INLINE glist #-}

    instance GIsList U1 U1 '[] '[] where
      glist :: forall x. Iso (U1 x) (U1 x) (HList '[]) (HList '[])
    glist = (U1 x -> HList '[])
    -> (HList '[] -> U1 x) -> Iso (U1 x) (U1 x) (HList '[]) (HList '[])
    forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
    iso (HList '[] -> U1 x -> HList '[]
    forall a b. a -> b -> a
    const HList '[]
    Nil) (U1 x -> HList '[] -> U1 x
    forall a b. a -> b -> a
    const U1 x
    forall k (p :: k). U1 p
    U1)
      {-# INLINE glist #-}

    --------------------------------------------------------------------------------
    -- | as ++ bs === cs
    class Appending as bs cs as' bs' cs'
      | as bs cs cs'   -> as' bs'
      , as' bs' cs cs' -> as bs
      , as bs          -> cs
      , as' bs'        -> cs'
      where
      appending :: Iso (HList as, HList bs) (HList as', HList bs') (HList cs) (HList cs')

    -- | [] ++ bs === bs
    instance Appending '[] bs bs '[] bs' bs' where
      appending :: Iso
      (HList '[], HList bs) (HList '[], HList bs') (HList bs) (HList bs')
    appending = ((HList '[], HList bs) -> HList bs)
    -> (HList bs' -> (HList '[], HList bs'))
    -> Iso
         (HList '[], HList bs) (HList '[], HList bs') (HList bs) (HList bs')
    forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
    iso (HList '[], HList bs) -> HList bs
    forall a b. (a, b) -> b
    snd (HList '[]
    Nil,)

    -- | (a : as) ++ bs === (a : cs)
    instance
      Appending as bs cs as' bs' cs' -- as ++ bs == cs
      => Appending (a ': as) bs (a ': cs) (a' ': as') bs' (a' ': cs') where
      appending :: Iso
      (HList (a : as), HList bs)
      (HList (a' : as'), HList bs')
      (HList (a : cs))
      (HList (a' : cs'))
    appending
        = Iso
      (HList (a : as)) (HList (a' : as')) (a, HList as) (a', HList as')
    -> Iso (HList bs) (HList bs') (HList bs) (HList bs')
    -> Iso
         (HList (a : as), HList bs)
         (HList (a' : as'), HList bs')
         ((a, HList as), HList bs)
         ((a', HList as'), HList bs')
    forall s t a b s' t' a' b'.
    Iso s t a b
    -> Iso s' t' a' b' -> Iso (s, s') (t, t') (a, a') (b, b')
    pairing (Iso
      (a', HList as') (a, HList as) (HList (a' : as')) (HList (a : as))
    -> Iso
         (HList (a : as)) (HList (a' : as')) (a, HList as) (a', HList as')
    forall s t a b. Iso s t a b -> Iso b a t s
    fromIso p i (HList (a' : as')) (HList (a : as))
    -> p i (a', HList as') (a, HList as)
    forall a (as :: [*]) b (bs :: [*]) (p :: * -> * -> * -> *) i.
    Profunctor p =>
    p i (HList (a : as)) (HList (b : bs))
    -> p i (a, HList as) (b, HList bs)
    Iso
      (a', HList as') (a, HList as) (HList (a' : as')) (HList (a : as))
    consing) p i (HList bs) (HList bs') -> p i (HList bs) (HList bs')
    forall a. a -> a
    Iso (HList bs) (HList bs') (HList bs) (HList bs')
    id -- ((a, as), bs)
        (p i ((a, HList as), HList bs) ((a', HList as'), HList bs')
     -> p i (HList (a : as), HList bs) (HList (a' : as'), HList bs'))
    -> (p i (HList (a : cs)) (HList (a' : cs'))
        -> p i ((a, HList as), HList bs) ((a', HList as'), HList bs'))
    -> p i (HList (a : cs)) (HList (a' : cs'))
    -> p i (HList (a : as), HList bs) (HList (a' : as'), HList bs')
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i (a, (HList as, HList bs)) (a', (HList as', HList bs'))
    -> p i ((a, HList as), HList bs) ((a', HList as'), HList bs')
    forall a b c a' b' c' (p :: * -> * -> * -> *) i.
    Profunctor p =>
    p i (a, (b, c)) (a', (b', c')) -> p i ((a, b), c) ((a', b'), c')
    assoc3                       -- (a, (as, bs))
        (p i (a, (HList as, HList bs)) (a', (HList as', HList bs'))
     -> p i ((a, HList as), HList bs) ((a', HList as'), HList bs'))
    -> (p i (HList (a : cs)) (HList (a' : cs'))
        -> p i (a, (HList as, HList bs)) (a', (HList as', HList bs')))
    -> p i (HList (a : cs)) (HList (a' : cs'))
    -> p i ((a, HList as), HList bs) ((a', HList as'), HList bs')
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Iso a a' a a'
    -> Iso
         (HList as, HList bs) (HList as', HList bs') (HList cs) (HList cs')
    -> Iso
         (a, (HList as, HList bs))
         (a', (HList as', HList bs'))
         (a, HList cs)
         (a', HList cs')
    forall s t a b s' t' a' b'.
    Iso s t a b
    -> Iso s' t' a' b' -> Iso (s, s') (t, t') (a, a') (b, b')
    pairing p i a a' -> p i a a'
    forall a. a -> a
    Iso a a' a a'
    id p i (HList cs) (HList cs')
    -> p i (HList as, HList bs) (HList as', HList bs')
    forall (as :: [*]) (bs :: [*]) (cs :: [*]) (as' :: [*])
           (bs' :: [*]) (cs' :: [*]).
    Appending as bs cs as' bs' cs' =>
    Iso
      (HList as, HList bs) (HList as', HList bs') (HList cs) (HList cs')
    Iso
      (HList as, HList bs) (HList as', HList bs') (HList cs) (HList cs')
    appending         -- (a, cs)
        (p i (a, HList cs) (a', HList cs')
     -> p i (a, (HList as, HList bs)) (a', (HList as', HList bs')))
    -> (p i (HList (a : cs)) (HList (a' : cs'))
        -> p i (a, HList cs) (a', HList cs'))
    -> p i (HList (a : cs)) (HList (a' : cs'))
    -> p i (a, (HList as, HList bs)) (a', (HList as', HList bs'))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i (HList (a : cs)) (HList (a' : cs'))
    -> p i (a, HList cs) (a', HList cs')
    forall a (as :: [*]) b (bs :: [*]) (p :: * -> * -> * -> *) i.
    Profunctor p =>
    p i (HList (a : as)) (HList (b : bs))
    -> p i (a, HList as) (b, HList bs)
    consing                      -- (a : cs)

    singleton :: Iso a b (HList '[a]) (HList '[ b])
    singleton :: forall a b (p :: * -> * -> * -> *) i.
    Profunctor p =>
    p i (HList '[a]) (HList '[b]) -> p i a b
    singleton = (a -> HList '[a])
    -> (HList '[b] -> b) -> Iso a b (HList '[a]) (HList '[b])
    forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
    iso (a -> HList '[] -> HList '[a]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil) (\(a
    x :> HList as
    _) -> b
    a
    x)

    consing :: Iso (a, HList as) (b, HList bs) (HList (a ': as)) (HList (b ': bs))
    consing :: forall a (as :: [*]) b (bs :: [*]) (p :: * -> * -> * -> *) i.
    Profunctor p =>
    p i (HList (a : as)) (HList (b : bs))
    -> p i (a, HList as) (b, HList bs)
    consing = ((a, HList as) -> HList (a : as))
    -> (HList (b : bs) -> (b, HList bs))
    -> Iso
         (a, HList as) (b, HList bs) (HList (a : as)) (HList (b : bs))
    forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
    iso (\(a
    x, HList as
    xs) -> a
    x a -> HList as -> HList (a : as)
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList as
    xs) (\(a
    x :> HList as
    xs) -> (b
    a
    x, HList bs
    HList as
    xs))

    --------------------------------------------------------------------------------
    class IndexList (i :: Nat) as bs a b | i as -> a, i bs -> b, i as b -> bs, i bs a -> as where
      point :: Lens (HList as) (HList bs) a b

    instance {-# OVERLAPPING #-}
      ( as ~ (a ': as')
      , bs ~ (b ': as')
      ) => IndexList 0 as bs a b where
      point :: Lens (HList as) (HList bs) a b
    point = (HList as -> (HList as', a))
    -> ((HList as', b) -> HList bs) -> Lens (HList as) (HList bs) a b
    forall s c a b t. (s -> (c, a)) -> ((c, b) -> t) -> Lens s t a b
    lens (\(a
    x :> HList as
    xs) -> (HList as'
    HList as
    xs, a
    a
    x)) (\(HList as'
    xs, b
    x') -> b
    x' b -> HList as' -> HList (b : as')
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList as'
    xs)
      {-# INLINE point #-}

    instance
      ( IndexList (n - 1) as' bs' a b
      , as ~ (x ': as')
      , bs ~ (x ': bs')
      ) => IndexList n as bs a b where
      point :: Lens (HList as) (HList bs) a b
    point = Iso (x, HList bs') (x, HList as') (HList bs) (HList as)
    -> Iso (HList as) (HList bs) (x, HList as') (x, HList bs')
    forall s t a b. Iso s t a b -> Iso b a t s
    fromIso p i (HList bs) (HList as) -> p i (x, HList bs') (x, HList as')
    p i (HList (x : bs')) (HList (x : as'))
    -> p i (x, HList bs') (x, HList as')
    forall a (as :: [*]) b (bs :: [*]) (p :: * -> * -> * -> *) i.
    Profunctor p =>
    p i (HList (a : as)) (HList (b : bs))
    -> p i (a, HList as) (b, HList bs)
    Iso (x, HList bs') (x, HList as') (HList bs) (HList as)
    consing (p i (x, HList as') (x, HList bs') -> p i (HList as) (HList bs))
    -> (p i a b -> p i (x, HList as') (x, HList bs'))
    -> p i a b
    -> p i (HList as) (HList bs)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i (HList as') (HList bs') -> p i (x, HList as') (x, HList bs')
    forall i a b c. p i a b -> p i (c, a) (c, b)
    forall (p :: * -> * -> * -> *) i a b c.
    Strong p =>
    p i a b -> p i (c, a) (c, b)
    second' (p i (HList as') (HList bs') -> p i (x, HList as') (x, HList bs'))
    -> (p i a b -> p i (HList as') (HList bs'))
    -> p i a b
    -> p i (x, HList as') (x, HList bs')
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall (i :: Nat) (as :: [*]) (bs :: [*]) a b.
    IndexList i as bs a b =>
    Lens (HList as) (HList bs) a b
    point @(n-1)
      {-# INLINE point #-}

    --------------------------------------------------------------------------------
    -- * Convert tuples to/from HLists

    class ListTuple (tuple :: Type) (tuple' :: Type) (as :: [Type]) (bs :: [Type]) | as -> tuple, bs -> tuple' where
      tupled :: Iso (HList as) (HList bs) tuple tuple'
      tupled = (HList as -> tuple)
    -> (tuple' -> HList bs) -> Iso (HList as) (HList bs) tuple tuple'
    forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
    iso (forall tuple tuple' (as :: [*]) (bs :: [*]).
    ListTuple tuple tuple' as bs =>
    HList as -> tuple
    listToTuple @tuple @tuple' @as @bs) (forall tuple tuple' (as :: [*]) (bs :: [*]).
    ListTuple tuple tuple' as bs =>
    tuple' -> HList bs
    tupleToList @tuple @tuple' @as @bs)
      {-# INLINE tupled #-}

      tupleToList :: tuple' -> HList bs
      listToTuple :: HList as -> tuple

    instance ListTuple () () '[] '[]
      where
      tupleToList :: () -> HList '[]
    tupleToList ()
    _ = HList '[]
    Nil
      listToTuple :: HList '[] -> ()
    listToTuple HList '[]
    _ = ()

    instance ListTuple a a' '[a] '[a'] where
      tupleToList :: a' -> HList '[a']
    tupleToList a'
    a
        = a'
    a a' -> HList '[] -> HList '[a']
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a] -> a
    listToTuple (a
    a :> HList as
    Nil)
        = a
    a
    a

    instance ListTuple
      (a1, b1) (a2, b2)
      [a1, b1] [a2, b2]
      where
      tupleToList :: (a2, b2) -> HList '[a2, b2]
    tupleToList (a2
    a, b2
    b)
        = a2
    a a2 -> HList '[b2] -> HList '[a2, b2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2 -> HList '[] -> HList '[b2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1] -> (a1, b1)
    listToTuple (a
    a :> a
    b :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b)

    instance ListTuple
      (a1, b1, c1) (a2, b2, c2)
      [a1, b1, c1] [a2, b2, c2]
      where
      tupleToList :: (a2, b2, c2) -> HList '[a2, b2, c2]
    tupleToList (a2
    a, b2
    b, c2
    c)
        = a2
    a a2 -> HList '[b2, c2] -> HList '[a2, b2, c2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2 -> HList '[c2] -> HList '[b2, c2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2 -> HList '[] -> HList '[c2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1] -> (a1, b1, c1)
    listToTuple (a
    a :> a
    b :> a
    c :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c)

    instance ListTuple
      (a1, b1, c1, d1) (a2, b2, c2, d2)
      [a1, b1, c1, d1] [a2, b2, c2, d2]
      where
      tupleToList :: (a2, b2, c2, d2) -> HList '[a2, b2, c2, d2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d)
        = a2
    a a2 -> HList '[b2, c2, d2] -> HList '[a2, b2, c2, d2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2 -> HList '[c2, d2] -> HList '[b2, c2, d2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2 -> HList '[d2] -> HList '[c2, d2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2 -> HList '[] -> HList '[d2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1] -> (a1, b1, c1, d1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d)

    instance ListTuple
      (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2)
      [a1, b1, c1, d1, e1] [a2, b2, c2, d2, e2]
      where
      tupleToList :: (a2, b2, c2, d2, e2) -> HList '[a2, b2, c2, d2, e2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e)
        = a2
    a a2 -> HList '[b2, c2, d2, e2] -> HList '[a2, b2, c2, d2, e2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2 -> HList '[c2, d2, e2] -> HList '[b2, c2, d2, e2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2 -> HList '[d2, e2] -> HList '[c2, d2, e2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2 -> HList '[e2] -> HList '[d2, e2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2 -> HList '[] -> HList '[e2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1] -> (a1, b1, c1, d1, e1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2)
      [a1, b1, c1, d1, e1, f1] [a2, b2, c2, d2, e2, f2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2) -> HList '[a2, b2, c2, d2, e2, f2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f)
        = a2
    a a2
    -> HList '[b2, c2, d2, e2, f2] -> HList '[a2, b2, c2, d2, e2, f2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2 -> HList '[c2, d2, e2, f2] -> HList '[b2, c2, d2, e2, f2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2 -> HList '[d2, e2, f2] -> HList '[c2, d2, e2, f2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2 -> HList '[e2, f2] -> HList '[d2, e2, f2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2 -> HList '[f2] -> HList '[e2, f2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2 -> HList '[] -> HList '[f2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1, f1] -> (a1, b1, c1, d1, e1, f1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1) (a2, b2, c2, d2, e2, f2, g2)
      [a1, b1, c1, d1, e1, f1, g1] [a2, b2, c2, d2, e2, f2, g2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2) -> HList '[a2, b2, c2, d2, e2, f2, g2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g)
        = a2
    a a2
    -> HList '[b2, c2, d2, e2, f2, g2]
    -> HList '[a2, b2, c2, d2, e2, f2, g2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList '[c2, d2, e2, f2, g2] -> HList '[b2, c2, d2, e2, f2, g2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2 -> HList '[d2, e2, f2, g2] -> HList '[c2, d2, e2, f2, g2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2 -> HList '[e2, f2, g2] -> HList '[d2, e2, f2, g2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2 -> HList '[f2, g2] -> HList '[e2, f2, g2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2 -> HList '[g2] -> HList '[f2, g2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2 -> HList '[] -> HList '[g2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1, f1, g1] -> (a1, b1, c1, d1, e1, f1, g1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1) (a2, b2, c2, d2, e2, f2, g2, h2)
      [a1, b1, c1, d1, e1, f1, g1, h1] [a2, b2, c2, d2, e2, f2, g2, h2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2)
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h)
        = a2
    a a2
    -> HList '[b2, c2, d2, e2, f2, g2, h2]
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList '[c2, d2, e2, f2, g2, h2]
    -> HList '[b2, c2, d2, e2, f2, g2, h2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList '[d2, e2, f2, g2, h2] -> HList '[c2, d2, e2, f2, g2, h2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2 -> HList '[e2, f2, g2, h2] -> HList '[d2, e2, f2, g2, h2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2 -> HList '[f2, g2, h2] -> HList '[e2, f2, g2, h2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2 -> HList '[g2, h2] -> HList '[f2, g2, h2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2 -> HList '[h2] -> HList '[g2, h2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2 -> HList '[] -> HList '[h2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1, f1, g1, h1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1, j1) (a2, b2, c2, d2, e2, f2, g2, h2, j2)
      [a1, b1, c1, d1, e1, f1, g1, h1, j1] [a2, b2, c2, d2, e2, f2, g2, h2, j2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2, j2)
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h, j2
    j)
        = a2
    a a2
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2]
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList '[c2, d2, e2, f2, g2, h2, j2]
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList '[d2, e2, f2, g2, h2, j2]
    -> HList '[c2, d2, e2, f2, g2, h2, j2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2
    -> HList '[e2, f2, g2, h2, j2] -> HList '[d2, e2, f2, g2, h2, j2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2 -> HList '[f2, g2, h2, j2] -> HList '[e2, f2, g2, h2, j2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2 -> HList '[g2, h2, j2] -> HList '[f2, g2, h2, j2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2 -> HList '[h2, j2] -> HList '[g2, h2, j2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2 -> HList '[j2] -> HList '[h2, j2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> j2
    j j2 -> HList '[] -> HList '[j2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1, f1, g1, h1, j1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1, j1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> a
    j :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h, j1
    a
    j)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2)
      [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2)
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h, j2
    j, k2
    k)
        = a2
    a a2
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2]
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2]
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList '[d2, e2, f2, g2, h2, j2, k2]
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2
    -> HList '[e2, f2, g2, h2, j2, k2]
    -> HList '[d2, e2, f2, g2, h2, j2, k2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2
    -> HList '[f2, g2, h2, j2, k2] -> HList '[e2, f2, g2, h2, j2, k2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2 -> HList '[g2, h2, j2, k2] -> HList '[f2, g2, h2, j2, k2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2 -> HList '[h2, j2, k2] -> HList '[g2, h2, j2, k2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2 -> HList '[j2, k2] -> HList '[h2, j2, k2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> j2
    j j2 -> HList '[k2] -> HList '[j2, k2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> k2
    k k2 -> HList '[] -> HList '[k2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1, f1, g1, h1, j1, k1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> a
    j :> a
    k :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h, j1
    a
    j, k1
    a
    k)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2)
      [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2)
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h, j2
    j, k2
    k, l2
    l)
        = a2
    a a2
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2]
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2]
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2]
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2
    -> HList '[e2, f2, g2, h2, j2, k2, l2]
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2
    -> HList '[f2, g2, h2, j2, k2, l2]
    -> HList '[e2, f2, g2, h2, j2, k2, l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2
    -> HList '[g2, h2, j2, k2, l2] -> HList '[f2, g2, h2, j2, k2, l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2 -> HList '[h2, j2, k2, l2] -> HList '[g2, h2, j2, k2, l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2 -> HList '[j2, k2, l2] -> HList '[h2, j2, k2, l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> j2
    j j2 -> HList '[k2, l2] -> HList '[j2, k2, l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> k2
    k k2 -> HList '[l2] -> HList '[k2, l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> l2
    l l2 -> HList '[] -> HList '[l2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> a
    j :> a
    k :> a
    l :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h, j1
    a
    j, k1
    a
    k, l1
    a
    l)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2)
      [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2)
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h, j2
    j, k2
    k, l2
    l, m2
    m)
        = a2
    a a2
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2]
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2]
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2]
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2]
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2
    -> HList '[f2, g2, h2, j2, k2, l2, m2]
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2
    -> HList '[g2, h2, j2, k2, l2, m2]
    -> HList '[f2, g2, h2, j2, k2, l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2
    -> HList '[h2, j2, k2, l2, m2] -> HList '[g2, h2, j2, k2, l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2 -> HList '[j2, k2, l2, m2] -> HList '[h2, j2, k2, l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> j2
    j j2 -> HList '[k2, l2, m2] -> HList '[j2, k2, l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> k2
    k k2 -> HList '[l2, m2] -> HList '[k2, l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> l2
    l l2 -> HList '[m2] -> HList '[l2, m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> m2
    m m2 -> HList '[] -> HList '[m2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> a
    j :> a
    k :> a
    l :> a
    m :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h, j1
    a
    j, k1
    a
    k, l1
    a
    l, m1
    a
    m)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2)
      [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2)
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h, j2
    j, k2
    k, l2
    l, m2
    m, n2
    n)
        = a2
    a a2
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2]
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2]
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2]
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2]
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2]
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2
    -> HList '[g2, h2, j2, k2, l2, m2, n2]
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2
    -> HList '[h2, j2, k2, l2, m2, n2]
    -> HList '[g2, h2, j2, k2, l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2
    -> HList '[j2, k2, l2, m2, n2] -> HList '[h2, j2, k2, l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> j2
    j j2 -> HList '[k2, l2, m2, n2] -> HList '[j2, k2, l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> k2
    k k2 -> HList '[l2, m2, n2] -> HList '[k2, l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> l2
    l l2 -> HList '[m2, n2] -> HList '[l2, m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> m2
    m m2 -> HList '[n2] -> HList '[m2, n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> n2
    n n2 -> HList '[] -> HList '[n2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> a
    j :> a
    k :> a
    l :> a
    m :> a
    n :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h, j1
    a
    j, k1
    a
    k, l1
    a
    l, m1
    a
    m, n1
    a
    n)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2)
      [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2)
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h, j2
    j, k2
    k, l2
    l, m2
    m, n2
    n, o2
    o)
        = a2
    a a2
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
    -> HList '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2, o2]
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2
    -> HList '[g2, h2, j2, k2, l2, m2, n2, o2]
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2
    -> HList '[h2, j2, k2, l2, m2, n2, o2]
    -> HList '[g2, h2, j2, k2, l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2
    -> HList '[j2, k2, l2, m2, n2, o2]
    -> HList '[h2, j2, k2, l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> j2
    j j2
    -> HList '[k2, l2, m2, n2, o2] -> HList '[j2, k2, l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> k2
    k k2 -> HList '[l2, m2, n2, o2] -> HList '[k2, l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> l2
    l l2 -> HList '[m2, n2, o2] -> HList '[l2, m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> m2
    m m2 -> HList '[n2, o2] -> HList '[m2, n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> n2
    n n2 -> HList '[o2] -> HList '[n2, o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> o2
    o o2 -> HList '[] -> HList '[o2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> a
    j :> a
    k :> a
    l :> a
    m :> a
    n :> a
    o :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h, j1
    a
    j, k1
    a
    k, l1
    a
    l, m1
    a
    m, n1
    a
    n, o1
    a
    o)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2)
      [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2)
    -> HList
         '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h, j2
    j, k2
    k, l2
    l, m2
    m, n2
    n, o2
    o, p2
    p)
        = a2
    a a2
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    -> HList
         '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    -> HList '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2
    -> HList '[g2, h2, j2, k2, l2, m2, n2, o2, p2]
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2
    -> HList '[h2, j2, k2, l2, m2, n2, o2, p2]
    -> HList '[g2, h2, j2, k2, l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2
    -> HList '[j2, k2, l2, m2, n2, o2, p2]
    -> HList '[h2, j2, k2, l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> j2
    j j2
    -> HList '[k2, l2, m2, n2, o2, p2]
    -> HList '[j2, k2, l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> k2
    k k2
    -> HList '[l2, m2, n2, o2, p2] -> HList '[k2, l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> l2
    l l2 -> HList '[m2, n2, o2, p2] -> HList '[l2, m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> m2
    m m2 -> HList '[n2, o2, p2] -> HList '[m2, n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> n2
    n n2 -> HList '[o2, p2] -> HList '[n2, o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> o2
    o o2 -> HList '[p2] -> HList '[o2, p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> p2
    p p2 -> HList '[] -> HList '[p2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList '[a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> a
    j :> a
    k :> a
    l :> a
    m :> a
    n :> a
    o :> a
    p :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h, j1
    a
    j, k1
    a
    k, l1
    a
    l, m1
    a
    m, n1
    a
    n, o1
    a
    o, p1
    a
    p)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2)
      [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2)
    -> HList
         '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h, j2
    j, k2
    k, l2
    l, m2
    m, n2
    n, o2
    o, p2
    p, q2
    q)
        = a2
    a a2
    -> HList
         '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    -> HList
         '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    -> HList
         '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    -> HList '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2
    -> HList '[g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2
    -> HList '[h2, j2, k2, l2, m2, n2, o2, p2, q2]
    -> HList '[g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2
    -> HList '[j2, k2, l2, m2, n2, o2, p2, q2]
    -> HList '[h2, j2, k2, l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> j2
    j j2
    -> HList '[k2, l2, m2, n2, o2, p2, q2]
    -> HList '[j2, k2, l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> k2
    k k2
    -> HList '[l2, m2, n2, o2, p2, q2]
    -> HList '[k2, l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> l2
    l l2
    -> HList '[m2, n2, o2, p2, q2] -> HList '[l2, m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> m2
    m m2 -> HList '[n2, o2, p2, q2] -> HList '[m2, n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> n2
    n n2 -> HList '[o2, p2, q2] -> HList '[n2, o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> o2
    o o2 -> HList '[p2, q2] -> HList '[o2, p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> p2
    p p2 -> HList '[q2] -> HList '[p2, q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> q2
    q q2 -> HList '[] -> HList '[q2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList
      '[a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> a
    j :> a
    k :> a
    l :> a
    m :> a
    n :> a
    o :> a
    p :> a
    q :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h, j1
    a
    j, k1
    a
    k, l1
    a
    l, m1
    a
    m, n1
    a
    n, o1
    a
    o, p1
    a
    p, q1
    a
    q)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2)
      [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2,
     r2)
    -> HList
         '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2,
           r2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h, j2
    j, k2
    k, l2
    l, m2
    m, n2
    n, o2
    o, p2
    p, q2
    q, r2
    r)
        = a2
    a a2
    -> HList
         '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    -> HList
         '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2,
           r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList
         '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    -> HList
         '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    -> HList
         '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    -> HList '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2
    -> HList '[g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2
    -> HList '[h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    -> HList '[g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2
    -> HList '[j2, k2, l2, m2, n2, o2, p2, q2, r2]
    -> HList '[h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> j2
    j j2
    -> HList '[k2, l2, m2, n2, o2, p2, q2, r2]
    -> HList '[j2, k2, l2, m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> k2
    k k2
    -> HList '[l2, m2, n2, o2, p2, q2, r2]
    -> HList '[k2, l2, m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> l2
    l l2
    -> HList '[m2, n2, o2, p2, q2, r2]
    -> HList '[l2, m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> m2
    m m2
    -> HList '[n2, o2, p2, q2, r2] -> HList '[m2, n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> n2
    n n2 -> HList '[o2, p2, q2, r2] -> HList '[n2, o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> o2
    o o2 -> HList '[p2, q2, r2] -> HList '[o2, p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> p2
    p p2 -> HList '[q2, r2] -> HList '[p2, q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> q2
    q q2 -> HList '[r2] -> HList '[q2, r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> r2
    r r2 -> HList '[] -> HList '[r2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList
      '[a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1,
        r1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1,
        r1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> a
    j :> a
    k :> a
    l :> a
    m :> a
    n :> a
    o :> a
    p :> a
    q :> a
    r :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h, j1
    a
    j, k1
    a
    k, l1
    a
    l, m1
    a
    m, n1
    a
    n, o1
    a
    o, p1
    a
    p, q1
    a
    q, r1
    a
    r)

    instance ListTuple
      (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2)
      [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
      where
      tupleToList :: (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2,
     r2, s2)
    -> HList
         '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2,
           r2, s2]
    tupleToList (a2
    a, b2
    b, c2
    c, d2
    d, e2
    e, f2
    f, g2
    g, h2
    h, j2
    j, k2
    k, l2
    l, m2
    m, n2
    n, o2
    o, p2
    p, q2
    q, r2
    r, s2
    s)
        = a2
    a a2
    -> HList
         '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2,
           s2]
    -> HList
         '[a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2,
           r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> b2
    b b2
    -> HList
         '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    -> HList
         '[b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2,
           s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> c2
    c c2
    -> HList
         '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    -> HList
         '[c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> d2
    dd2
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    -> HList
         '[d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> e2
    e e2
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    -> HList '[e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> f2
    f f2
    -> HList '[g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    -> HList '[f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> g2
    g g2
    -> HList '[h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    -> HList '[g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> h2
    h h2
    -> HList '[j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    -> HList '[h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> j2
    j j2
    -> HList '[k2, l2, m2, n2, o2, p2, q2, r2, s2]
    -> HList '[j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> k2
    k k2
    -> HList '[l2, m2, n2, o2, p2, q2, r2, s2]
    -> HList '[k2, l2, m2, n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> l2
    l l2
    -> HList '[m2, n2, o2, p2, q2, r2, s2]
    -> HList '[l2, m2, n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> m2
    m m2
    -> HList '[n2, o2, p2, q2, r2, s2]
    -> HList '[m2, n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> n2
    n n2
    -> HList '[o2, p2, q2, r2, s2] -> HList '[n2, o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> o2
    o o2 -> HList '[p2, q2, r2, s2] -> HList '[o2, p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> p2
    p p2 -> HList '[q2, r2, s2] -> HList '[p2, q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> q2
    q q2 -> HList '[r2, s2] -> HList '[q2, r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> r2
    r r2 -> HList '[s2] -> HList '[r2, s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> s2
    s s2 -> HList '[] -> HList '[s2]
    forall a (as :: [*]). a -> HList as -> HList (a : as)
    :> HList '[]
    Nil
      listToTuple :: HList
      '[a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1,
        r1, s1]
    -> (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1,
        r1, s1)
    listToTuple (a
    a :> a
    b :> a
    c :> a
    d :> a
    e :> a
    f :> a
    g :> a
    h :> a
    j :> a
    k :> a
    l :> a
    m :> a
    n :> a
    o :> a
    p :> a
    q :> a
    r :> a
    s :> HList as
    Nil)
        = (a1
    a
    a, b1
    a
    b, c1
    a
    c, d1
    a
    d, e1
    a
    e, f1
    a
    f, g1
    a
    g, h1
    a
    h, j1
    a
    j, k1
    a
    k, l1
    a
    l, m1
    a
    m, n1
    a
    n, o1
    a
    o, p1
    a
    p, q1
    a
    q, r1
    a
    r, s1
    a
    s)

    type family TupleToList a where
      TupleToList () = '[]
      TupleToList (a, b) = '[a, b]
      TupleToList (a, b, c) = '[a, b, c]
      TupleToList (a, b, c, d) = '[a, b, c, d]
      TupleToList (a, b, c, d, e) = '[a, b, c, d, e]
      TupleToList (a, b, c, d, e, f) = '[a, b, c, d, e, f]
      TupleToList (a, b, c, d, e, f, g) = '[a, b, c, d, e, f, g]
      TupleToList (a, b, c, d, e, f, g, h) = '[a, b, c, d, e, f, g, h]
      TupleToList (a, b, c, d, e, f, g, h, j) = '[a, b, c, d, e, f, g, h, j]
      TupleToList (a, b, c, d, e, f, g, h, j, k) = '[a, b, c, d, e, f, g, h, j, k]
      TupleToList (a, b, c, d, e, f, g, h, j, k, l) = '[a, b, c, d, e, f, g, h, j, k, l]
      TupleToList (a, b, c, d, e, f, g, h, j, k, l, m) = '[a, b, c, d, e, f, g, h, j, k, l, m]
      TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n) = '[a, b, c, d, e, f, g, h, j, k, l, m, n]
      TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o]
      TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p]
      TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q]
      TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r]
      TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s]
      TupleToList a = '[a]