module Singleraeh.Tuple where

import Data.Kind ( Type )

type STuple2 :: (a -> Type) -> (b -> Type) -> (a, b) -> Type
data STuple2 sa sb ab where
    STuple2 :: sa a -> sb b -> STuple2 sa sb '(a, b)

demoteSTuple2
    :: forall da db sa sb ab
    .  (forall a. sa a -> da)
    -> (forall b. sb b -> db)
    -> STuple2 sa sb ab
    -> (da, db)
demoteSTuple2 :: forall {a} {b} da db (sa :: a -> Type) (sb :: b -> Type)
       (ab :: (a, b)).
(forall (a :: a). sa a -> da)
-> (forall (b :: b). sb b -> db) -> STuple2 sa sb ab -> (da, db)
demoteSTuple2 forall (a :: a). sa a -> da
demoteSA forall (b :: b). sb b -> db
demoteSB (STuple2 sa a
sa sb b
sb) = (sa a -> da
forall (a :: a). sa a -> da
demoteSA sa a
sa, sb b -> db
forall (b :: b). sb b -> db
demoteSB sb b
sb)