module Data.Type.Witness.Specific.Pair where

import Data.Type.Witness.General.Order
import Data.Type.Witness.General.Representative
import Data.Type.Witness.General.WitnessConstraint
import Import

-- | a witness for pairs of witnesses
type PairType :: (k -> Type) -> (k -> Type) -> (k -> Type)
data PairType w1 w2 t =
    MkPairType (w1 t)
               (w2 t)

instance (Representative w1, Representative w2) => Representative (PairType w1 w2) where
    getRepWitness :: Subrepresentative (PairType w1 w2) (PairType w1 w2)
getRepWitness (MkPairType w1 a
w1 w2 a
w2) =
        case (forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness w1 a
w1, forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness w2 a
w2) of
            (Dict (Is w1 a)
Dict, Dict (Is w2 a)
Dict) -> forall (a :: Constraint). a => Dict a
Dict

instance (Is w1 t, Is w2 t) => Is (PairType w1 w2) t where
    representative :: PairType w1 w2 t
representative = forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w1 t -> w2 t -> PairType w1 w2 t
MkPairType forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative

-- | left-biased
instance TestEquality w1 => TestEquality (PairType w1 w2) where
    testEquality :: forall (a :: k) (b :: k).
PairType w1 w2 a -> PairType w1 w2 b -> Maybe (a :~: b)
testEquality (MkPairType w1 a
a1 w2 a
_) (MkPairType w1 b
b1 w2 b
_) = forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w1 a
a1 w1 b
b1

-- | left-biased
instance TestOrder w1 => TestOrder (PairType w1 w2) where
    testCompare :: forall (a :: k) (b :: k).
PairType w1 w2 a -> PairType w1 w2 b -> WOrdering a b
testCompare (MkPairType w1 a
a1 w2 a
_) (MkPairType w1 b
b1 w2 b
_) = forall k (w :: k -> Type) (a :: k) (b :: k).
TestOrder w =>
w a -> w b -> WOrdering a b
testCompare w1 a
a1 w1 b
b1

-- | right-biased
instance WitnessConstraint c w2 => WitnessConstraint c (PairType w1 w2) where
    witnessConstraint :: forall (t :: k). PairType w1 w2 t -> Dict (c t)
witnessConstraint (MkPairType w1 t
_ w2 t
w2) = forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k).
WitnessConstraint c w =>
w t -> Dict (c t)
witnessConstraint w2 t
w2