    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeFamilies #-}

    module Data.Parameterized.DataKind
      ( PairRepr(..), Fst, Snd, fst, snd
      ) where

    import           Data.Parameterized.Classes
    import qualified Data.Parameterized.TH.GADT as TH

    import           Data.Kind
    import           Prelude hiding ( fst, snd )

    data PairRepr (f :: k1 -> Type) (g :: k2 -> Type) (p :: (k1, k2)) where
      PairRepr :: f a -> g b -> PairRepr f g '(a, b)

    type family Fst (pair :: (k1, k2)) where
      Fst '(a, _) = a
    type family Snd (pair :: (k1, k2)) where
      Snd '(_, b) = b

    fst :: PairRepr f g p -> f (Fst p)
    fst :: forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> *) (p :: (k1, k2)).
    PairRepr f g p -> f (Fst p)
    fst (PairRepr f a
    a g b
    _) = f a
    f (Fst p)
    a

    snd :: PairRepr f g p -> g (Snd p)
    snd :: forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> *) (p :: (k1, k2)).
    PairRepr f g p -> g (Snd p)
    snd (PairRepr f a
    _ g b
    b) = g b
    g (Snd p)
    b

    $(return [])

    instance ( ShowF f, ShowF g ) => Show (PairRepr f g p) where
      show :: PairRepr f g p -> String
    show (PairRepr f a
    a g b
    b) = Char -> ShowS
    showChar Char
    '(' ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f a -> ShowS
    forall {k} (f :: k -> *) (tp :: k). ShowF f => f tp -> ShowS
    showsF f a
    a ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> ShowS
    showChar Char
    ',' ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . g b -> ShowS
    forall {k} (f :: k -> *) (tp :: k). ShowF f => f tp -> ShowS
    showsF g b
    b ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ String
    ")"
    instance ( ShowF f, ShowF g ) => ShowF (PairRepr f g)

    deriving instance ( Eq (f a), Eq (g b) ) => Eq (PairRepr f g '(a, b))
    instance ( EqF f, EqF g ) => EqF (PairRepr f g) where
      eqF :: forall (a :: (k1, k2)). PairRepr f g a -> PairRepr f g a -> Bool
    eqF (PairRepr f a
    a1 g b
    b1) (PairRepr f a
    a2 g b
    b2) =
        f a -> f a -> Bool
    forall (a :: k1). f a -> f a -> Bool
    forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
    eqF f a
    a1 f a
    f a
    a2 Bool -> Bool -> Bool
    && g b -> g b -> Bool
    forall (a :: k2). g a -> g a -> Bool
    forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
    eqF g b
    b1 g b
    g b
    b2
    instance ( TestEquality f, TestEquality g ) => TestEquality (PairRepr f g) where
      testEquality :: forall (a :: (k1, k2)) (b :: (k1, k2)).
    PairRepr f g a -> PairRepr f g b -> Maybe (a :~: b)
    testEquality =
        $(TH.structuralTypeEquality [t|PairRepr|]
          [
            ( TH.DataArg 0 `TH.TypeApp` TH.AnyType, [|testEquality|] )
          , ( TH.DataArg 1 `TH.TypeApp` TH.AnyType, [|testEquality|] )
          ])

    deriving instance ( Ord (f a), Ord (g b) ) => Ord (PairRepr f g '(a, b))
    instance ( OrdF f, OrdF g ) => OrdF (PairRepr f g) where
      compareF :: forall (x :: (k1, k2)) (y :: (k1, k2)).
    PairRepr f g x -> PairRepr f g y -> OrderingF x y
    compareF =
        $(TH.structuralTypeOrd [t|PairRepr|]
          [ ( TH.DataArg 0 `TH.TypeApp` TH.AnyType, [|compareF|] )
          , ( TH.DataArg 1 `TH.TypeApp` TH.AnyType, [|compareF|] )
          ])