module Singleraeh.Tuple where

import Singleraeh.Demote
import Data.Kind ( Type, Constraint )

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

class SingTuple2 (cl :: lk -> Constraint) (cr :: rk -> Constraint) (sl :: lk -> Type) (sr :: rk -> Type) (lr :: (lk, rk)) where
    singTuple2'
        :: (forall l. cl l => sl l)
        -> (forall r. cr r => sr r)
        -> STuple2 sl sr lr

singTuple2
    :: forall cl cr sl sr lr. SingTuple2 cl cr sl sr lr
    => (forall l. cl l => sl l)
    -> (forall r. cr r => sr r)
    -> STuple2 sl sr lr
singTuple2 :: forall {a} {b} (cl :: a -> Constraint) (cr :: b -> Constraint)
       (sl :: a -> Type) (sr :: b -> Type) (lr :: (a, b)).
SingTuple2 cl cr sl sr lr =>
(forall (l :: a). cl l => sl l)
-> (forall (r :: b). cr r => sr r) -> STuple2 sl sr lr
singTuple2 = forall {a} {b} (cl :: a -> Constraint) (cr :: b -> Constraint)
       (sl :: a -> Type) (sr :: b -> Type) (lr :: (a, b)).
SingTuple2 cl cr sl sr lr =>
(forall (l :: a). cl l => sl l)
-> (forall (r :: b). cr r => sr r) -> STuple2 sl sr lr
singTuple2' @_ @_ @cl @cr

instance (cl l, cr r) => SingTuple2 cl cr sl sr '(l, r) where
    singTuple2' :: (forall (l :: k). cl l => sl l)
-> (forall (r :: k). cr r => sr r) -> STuple2 sl sr '(l, r)
singTuple2' forall (l :: k). cl l => sl l
sl forall (r :: k). cr r => sr r
sr = sl l -> sr r -> STuple2 sl sr '(l, r)
forall {a} {b} (sa :: a -> Type) (a :: a) (sb :: b -> Type)
       (b :: b).
sa a -> sb b -> STuple2 sa sb '(a, b)
STuple2 sl l
forall (l :: k). cl l => sl l
sl sr r
forall (r :: k). cr r => sr r
sr

type STuple3 :: (a -> Type) -> (b -> Type) -> (c -> Type) -> (a, b, c) -> Type
data STuple3 sa sb sc abc where
    STuple3 :: sa a -> sb b -> sc c -> STuple3 sa sb sc '(a, b, c)

demoteSTuple3
    :: forall da db dc sa sb sc abc
    .  (forall a. sa a -> da)
    -> (forall b. sb b -> db)
    -> (forall c. sc c -> dc)
    -> STuple3 sa sb sc abc
    -> (da, db, dc)
demoteSTuple3 :: forall {a} {b} {c} da db dc (sa :: a -> Type) (sb :: b -> Type)
       (sc :: c -> Type) (abc :: (a, b, c)).
(forall (a :: a). sa a -> da)
-> (forall (b :: b). sb b -> db)
-> (forall (c :: c). sc c -> dc)
-> STuple3 sa sb sc abc
-> (da, db, dc)
demoteSTuple3 forall (a :: a). sa a -> da
demoteSA forall (b :: b). sb b -> db
demoteSB forall (c :: c). sc c -> dc
demoteSC (STuple3 sa a
sa sb b
sb sc c
sc) =
    (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, sc c -> dc
forall (c :: c). sc c -> dc
demoteSC sc c
sc)

instance (Demotable sa, Demotable sb, Demotable sc)
  => Demotable (STuple3 sa sb sc) where
    type Demote (STuple3 sa sb sc) = (Demote sa, Demote sb, Demote sc)
    demote :: forall (k1 :: (a, b, c)).
STuple3 sa sb sc k1 -> Demote (STuple3 sa sb sc)
demote = (forall (a :: a). sa a -> Demote sa)
-> (forall (b :: b). sb b -> Demote sb)
-> (forall (c :: c). sc c -> Demote sc)
-> STuple3 sa sb sc k1
-> (Demote sa, Demote sb, Demote sc)
forall {a} {b} {c} da db dc (sa :: a -> Type) (sb :: b -> Type)
       (sc :: c -> Type) (abc :: (a, b, c)).
(forall (a :: a). sa a -> da)
-> (forall (b :: b). sb b -> db)
-> (forall (c :: c). sc c -> dc)
-> STuple3 sa sb sc abc
-> (da, db, dc)
demoteSTuple3 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 sc c -> Demote sc
forall (c :: c). sc c -> Demote sc
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote

class SingTuple3 (ca :: ak -> Constraint) (cb :: bk -> Constraint) (cc :: ck -> Constraint) (sa :: ak -> Type) (sb :: bk -> Type) (sc :: ck -> Type) (abc :: (ak, bk, ck)) where
    singTuple3'
        :: (forall a. ca a => sa a)
        -> (forall b. cb b => sb b)
        -> (forall c. cc c => sc c)
        -> STuple3 sa sb sc abc

singTuple3
    :: forall ca cb cc sa sb sc abc. SingTuple3 ca cb cc sa sb sc abc
    => (forall a. ca a => sa a)
    -> (forall b. cb b => sb b)
    -> (forall c. cc c => sc c)
    -> STuple3 sa sb sc abc
singTuple3 :: forall {a} {b} {c} (ca :: a -> Constraint) (cb :: b -> Constraint)
       (cc :: c -> Constraint) (sa :: a -> Type) (sb :: b -> Type)
       (sc :: c -> Type) (abc :: (a, b, c)).
SingTuple3 ca cb cc sa sb sc abc =>
(forall (a :: a). ca a => sa a)
-> (forall (b :: b). cb b => sb b)
-> (forall (c :: c). cc c => sc c)
-> STuple3 sa sb sc abc
singTuple3 = forall {a} {b} {c} (ca :: a -> Constraint) (cb :: b -> Constraint)
       (cc :: c -> Constraint) (sa :: a -> Type) (sb :: b -> Type)
       (sc :: c -> Type) (abc :: (a, b, c)).
SingTuple3 ca cb cc sa sb sc abc =>
(forall (a :: a). ca a => sa a)
-> (forall (b :: b). cb b => sb b)
-> (forall (c :: c). cc c => sc c)
-> STuple3 sa sb sc abc
singTuple3' @_ @_ @_ @ca @cb @cc

instance (ca a, cb b, cc c) => SingTuple3 ca cb cc sa sb sc '(a, b, c) where
    singTuple3' :: (forall (a :: k). ca a => sa a)
-> (forall (b :: k). cb b => sb b)
-> (forall (c :: k). cc c => sc c)
-> STuple3 sa sb sc '(a, b, c)
singTuple3' forall (a :: k). ca a => sa a
sa forall (b :: k). cb b => sb b
sb forall (c :: k). cc c => sc c
sc = sa a -> sb b -> sc c -> STuple3 sa sb sc '(a, b, c)
forall {a} {b} {c} (sa :: a -> Type) (a :: a) (sb :: b -> Type)
       (b :: b) (sc :: c -> Type) (c :: c).
sa a -> sb b -> sc c -> STuple3 sa sb sc '(a, b, c)
STuple3 sa a
forall (a :: k). ca a => sa a
sa sb b
forall (b :: k). cb b => sb b
sb sc c
forall (c :: k). cc c => sc c
sc