{-# 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
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
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
'(' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (tp :: k). ShowF f => f tp -> ShowS
showsF f a
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
',' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (tp :: k). ShowF f => f tp -> ShowS
showsF g b
b 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 ( 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|] )
      ])