module Singleraeh.Tuple where

import Singleraeh.Demote
import Data.Kind ( Type )

data SUnit (unit :: ()) where SUnit :: SUnit '()

demoteSUnit :: SUnit unit -> ()
demoteSUnit :: forall (unit :: ()). SUnit unit -> ()
demoteSUnit SUnit unit
SUnit = ()

instance Demotable SUnit where
    type Demote SUnit = ()
    demote :: forall (k1 :: ()). SUnit k1 -> Demote SUnit
demote = SUnit k1 -> ()
SUnit k1 -> Demote SUnit
forall (unit :: ()). SUnit unit -> ()
demoteSUnit

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)

instance (Demotable sa, Demotable sb) => Demotable (STuple2 sa sb) where
    type Demote (STuple2 sa sb) = (Demote sa, Demote sb)
    demote :: forall (k1 :: (a, b)). STuple2 sa sb k1 -> Demote (STuple2 sa sb)
demote = (forall (a :: a). sa a -> Demote sa)
-> (forall (b :: b). sb b -> Demote sb)
-> STuple2 sa sb k1
-> (Demote sa, Demote sb)
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 sa a -> Demote sa
forall (a :: a). sa a -> Demote sa
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote sb b -> Demote sb
forall (b :: b). sb b -> Demote sb
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote