    {-|
    Description : A 2-tuple with identically parameterized elements
    Copyright   : (c) Galois, Inc 2017-2019

    This module defines a 2-tuple where both elements are parameterized over the
    same existentially quantified parameter.

    -}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    module Data.Parameterized.Pair
      ( Pair(..)
      , fstPair
      , sndPair
      , viewPair
      ) where

    import Data.Kind
    import Data.Parameterized.Classes
    import Data.Parameterized.Some
    import Data.Parameterized.TraversableF

    -- | Like a 2-tuple, but with an existentially quantified parameter that both of
    -- the elements share.
    data Pair (a :: k -> Type) (b :: k -> Type) where
      Pair :: !(a tp) -> !(b tp) -> Pair a b

    instance (TestEquality a, EqF b) => Eq (Pair a b) where
      Pair a tp
    xa b tp
    xb == :: Pair a b -> Pair a b -> Bool
    == Pair a tp
    ya b tp
    yb =
        case a tp -> a tp -> Maybe (tp :~: tp)
    forall (a :: k) (b :: k). a a -> a b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality a tp
    xa a tp
    ya of
          Just tp :~: tp
    Refl -> b tp -> b tp -> Bool
    forall (a :: k). b a -> b a -> Bool
    forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
    eqF b tp
    xb b tp
    b tp
    yb
          Maybe (tp :~: tp)
    Nothing -> Bool
    False

    instance FunctorF (Pair a) where
      fmapF :: forall (f :: k -> *) (g :: k -> *).
    (forall (x :: k). f x -> g x) -> Pair a f -> Pair a g
    fmapF forall (x :: k). f x -> g x
    f (Pair a tp
    x f tp
    y) = a tp -> g tp -> Pair a g
    forall {k} (a :: k -> *) (tp :: k) (b :: k -> *).
    a tp -> b tp -> Pair a b
    Pair a tp
    x (f tp -> g tp
    forall (x :: k). f x -> g x
    f f tp
    y)

    instance FoldableF (Pair a) where
      foldMapF :: forall m (e :: k -> *).
    Monoid m =>
    (forall (s :: k). e s -> m) -> Pair a e -> m
    foldMapF forall (s :: k). e s -> m
    f (Pair a tp
    _ e tp
    y) = e tp -> m
    forall (s :: k). e s -> m
    f e tp
    y
      foldrF :: forall (e :: k -> *) b.
    (forall (s :: k). e s -> b -> b) -> b -> Pair a e -> b
    foldrF forall (s :: k). e s -> b -> b
    f b
    z (Pair a tp
    _ e tp
    y) = e tp -> b -> b
    forall (s :: k). e s -> b -> b
    f e tp
    y b
    z

    -- | Extract the first element of a pair.
    fstPair :: Pair a b -> Some a
    fstPair :: forall {k} (a :: k -> *) (b :: k -> *). Pair a b -> Some a
    fstPair (Pair a tp
    x b tp
    _) = a tp -> Some a
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some a tp
    x

    -- | Extract the second element of a pair.
    sndPair :: Pair a b -> Some b
    sndPair :: forall {k} (a :: k -> *) (b :: k -> *). Pair a b -> Some b
    sndPair (Pair a tp
    _ b tp
    y) = b tp -> Some b
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some b tp
    y

    -- | Project out of Pair.
    viewPair :: (forall tp. a tp -> b tp -> c) -> Pair a b -> c
    viewPair :: forall {k} (a :: k -> *) (b :: k -> *) c.
    (forall (tp :: k). a tp -> b tp -> c) -> Pair a b -> c
    viewPair forall (tp :: k). a tp -> b tp -> c
    f (Pair a tp
    x b tp
    y) = a tp -> b tp -> c
    forall (tp :: k). a tp -> b tp -> c
    f a tp
    x b tp
    y