{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Data.Container.Poly where

--import Prologue hiding (Ixed, Indexed, Simple)
--import           Data.TypeLevel.List (In)
--import Data.Typeable
--import GHC.Prim
--import Type.Bool
import qualified Data.Container.Opts as Mods
--import           Data.Container.Mods (FilterMutable, filterMutable)



--type family AppendLst a lst where AppendLst a '[]       = '[a]
--                                  AppendLst a (l ': ls) = l ': AppendLst a ls



--------------------

--type family CmpLst (lst :: [k]) (lst' :: [k']) :: [Bool] where
--            CmpLst (l ': ls)    (l  ': ls')     = (True  ': CmpLst ls ls')
--            CmpLst (l ': ls)    (l' ': ls')     = (False ': CmpLst ls ls')
--            CmpLst '[]          '[]             = '[]

--type family LstIn (lst :: [*]) (lst' :: [*]) :: [Bool] where
--            LstIn (l ': ls) lst = In l lst ': LstIn ls (Remove l lst)
--            LstIn ls        '[] = '[]
--            LstIn '[]       lst = '[]


--type family   Remove (a :: k) (cont :: c) :: c
--type instance Remove (a :: k) ((t ': ts) :: [k]) = If (a :== t) ts (t ': Remove a ts)
--type instance Remove (a :: k) '[]                = '[]


--type family ModsOf (inst :: k) cont :: [*]

--data InstMods (inst :: k) (mods :: [Bool]) = InstMods
--data InstMods2 (inst :: k) (mods :: [Bool]) (cont :: *) = InstMods2
--data InstModsX (inst :: k) (query :: [*]) (mods :: [Bool]) (cont :: *) = InstModsX








--newtype Tagged t a = Tagged { fromTag :: a } deriving (Show)

--tagged :: Proxy t -> a -> Tagged t a
--tagged _ = Tagged

--type family FillData (layout :: [*]) datas where FillData (t ': ts) datas = (GetData t datas, FillData ts datas)
--                                                 FillData '[]       datas = ()

--type family GetData (tag :: *) datas where GetData tag (Tagged tag  a, ds) = a
--                                           GetData tag (Tagged tag' a, ds) = GetData tag ds

--type family   TaggedCont (tags :: [*]) a
--type instance TaggedCont '[]       ()     = ()
--type instance TaggedCont (t ': ts) (a,as) = (Tagged t a, TaggedCont ts as)

--class Taggable tags cont where
--    taggedCont :: Proxy tags -> cont -> TaggedCont tags cont

--instance {-# OVERLAPPABLE #-}                   Taggable '[]       ()     where taggedCont _ _ = ()
--instance {-# OVERLAPPABLE #-} Taggable ts as => Taggable (t ': ts) (a,as) where taggedCont _ (a,as) = (Tagged a, taggedCont (Proxy :: Proxy ts) as)

--class                                                                          DataFillable (layout :: [*]) datas where fillData :: Proxy layout -> datas -> FillData layout datas
--instance {-# OVERLAPPABLE #-} (DataGettable t datas, DataFillable ts datas) => DataFillable (t ': ts) datas where fillData _ ds = (getData (Proxy :: Proxy t) ds, fillData (Proxy :: Proxy ts) ds)
--instance {-# OVERLAPPABLE #-}                                                  DataFillable '[]       datas where fillData _ _  = ()

--class                                                                                                    DataGettable tag datas               where getData :: Proxy tag -> datas -> GetData tag datas
--instance {-# OVERLAPPABLE #-}                                                                            DataGettable tag (Tagged tag  a, ds) where getData _ = fromTag . fst
--instance {-# OVERLAPPABLE #-} (DataGettable tag ds, GetData tag (Tagged tag' a, ds) ~ GetData tag ds) => DataGettable tag (Tagged tag' a, ds) where getData t = getData t . snd



--type family   MappedByTag tag a l
--type instance MappedByTag t a ()                 = ()
--type instance MappedByTag t a (Tagged t' a', ls) = If (t :== t') (Tagged t  a , MappedByTag t a ls)
--                                                                 (Tagged t' a', MappedByTag t a ls)

--class                                                                                                                       MapByTag  t a b l       | t l -> a where mapByTag  :: Proxy t -> (a -> b) -> l -> MappedByTag t b l
--class                                                                                                                       MapByTag' t a b l                  where mapByTag' :: Proxy t -> (a -> b) -> l -> MappedByTag t b l
--instance {-# OVERLAPPABLE #-} (MapByTag' t a b l, a ~ a')                                                                => MapByTag  t a b (Tagged t  a', l ) where mapByTag  t f (Tagged a, l) = (Tagged $ f a, mapByTag' t f l)
--instance {-# OVERLAPPABLE #-} (MapByTag  t a b l, MappedByTag t b (Tagged t' a', l) ~ (Tagged t' a', MappedByTag t b l)) => MapByTag  t a b (Tagged t' a', l ) where mapByTag  t f (ta      , l) = (ta          , mapByTag  t f l)
--instance {-# OVERLAPPABLE #-} (MapByTag' t a b l, a ~ a')                                                                => MapByTag' t a b (Tagged t  a', l ) where mapByTag' t f (Tagged a, l) = (Tagged $ f a, mapByTag' t f l)
--instance {-# OVERLAPPABLE #-} (MapByTag' t a b l, MappedByTag t b (Tagged t' a', l) ~ (Tagged t' a', MappedByTag t b l)) => MapByTag' t a b (Tagged t' a', l ) where mapByTag' t f (ta      , l) = (ta          , mapByTag' t f l)
--instance                                                                                                                    MapByTag' t a b ()                 where mapByTag' _ _ _ = ()




--type I = InstMods2
--type I2X = InstModsX

--type family UpdateQuery instMods guery where
--    UpdateQuery (InstModsX inst q m cont) q'= InstModsX inst q' (LstIn (ModsOf inst cont) q') cont





--rebaseSpecX :: InstModsX inst q mods cont -> InstModsX inst' q (LstIn (ModsOf inst' cont) q) cont
--rebaseSpecX _ = InstModsX

--polySpecX :: InstModsX inst q mods cont -> InstModsX inst q (LstIn (ModsOf inst cont') q) cont'
--polySpecX _ = InstModsX
----type family Rebase mods base where Rebase (InstMods2 inst mods old) new = InstMods2 inst mods new

--type family InstQuery (inst :: * -> Constraint) :: [*]

--query :: InstModsX inst q mods cont -> Proxy q
--query _ = Proxy







--optBuilder :: a -> OptBuilderBase a
--optBuilder = OptBuilder

--type OptBuilderBase = OptBuilder '[]



--newtype OptBuilder (opts :: [*]) a = OptBuilder a deriving (Functor)

--class FuncBuilder f a | a -> f where
--    buildFunc :: f -> a

--class FuncTrans opts f a | a opts -> f where
--    transFunc :: OptBuilder opts f -> a

--instance {-# OVERLAPPABLE #-} (f ~ a, g ~ b)             => FuncBuilder (f -> g)            (a -> b)            where buildFunc = id
--instance {-# OVERLAPPABLE #-} (t ~ (f -> g), opts ~ '[]) => FuncBuilder (f -> g)            (OptBuilder opts t) where buildFunc = OptBuilder

--instance                            (opts ~ opts', f ~ f')       => FuncTrans opts f  (OptBuilder opts' f') where transFunc = id
--instance                          (f ~ (Proxy opts -> a -> b))   => FuncTrans opts f  (a -> b)              where transFunc (OptBuilder f) = f Proxy





--extendOptBuilder :: Proxy opt -> Proxy opts' -> OptBuilder opts a -> OptBuilder (opt ': (Concat opts' opts)) a
--extendOptBuilder _ _ (OptBuilder a) = OptBuilder a




----------------





--type family Selected (b :: [Bool]) (lst :: [*]) :: [*] where
--    Selected ('True  ': b) (l ': ls) = l ': Selected b ls
--    Selected ('False ': b) (l ': ls) =      Selected b ls
--    Selected '[]           lst       =      '[]
--    Selected s             lst       =      '[]



--data Query (q :: [*]) (m :: [Bool]) = Query


--data NA = NA
--data Info (idx :: *) (el :: *) (cls :: k) (cont :: *) = Info

--type family InfoIdx  i where InfoIdx  (Info idx el cls cont) = idx
--type family InfoEl   i where InfoEl   (Info idx el cls cont) = el
--type family InfoCls  i where InfoCls  (Info idx el cls cont) = cls
--type family InfoCont i where InfoCont (Info idx el cls cont) = cont

--type RawInfo           = Info NA  NA
--type IxedInfo   idx    = Info idx NA
--type ElInfo         el = Info NA  el
--type IxedElInfo idx el = Info idx el



--type family ElementOf        cont
--type family IndexOf      el  cont
--type family HomoIndexOf (m :: * -> *) :: *
--type family ElementByIx idx cont
--type family IxType      idx

--type IndexOf' cont = IndexOf (ElementOf cont) cont

---- === Results ===



--type family SelTags (info :: *) (s :: [Bool]) where SelTags (Info idx el cls cont) s = QueryData (Info idx el cls (DataStoreOf cont)) (Selected s (FilterMutable (ModsOf cls cont)))









--type IxedData cls idx = If (IxedMode cls :== Single) idx [idx]

--type family QueryData (info :: *) (query :: [*]) :: * where
--    QueryData info '[]       = ()
--    QueryData info (q ': qs) = (ModData q info, QueryData info qs)

--type family   ModData mod info
--type instance ModData Mods.Ixed (Info idx el cls cont) = IxedData cls (
--    If (idx :== NA) (
--        --If (el :== NA)
--            (IndexOf' cont)
--          --  (IndexOf el cont)
--    ) idx
-- )





--type ComputeSelection (cls :: k) (cont :: *) (q :: [*]) = LstIn (ModsOf cls cont) q
--type AssumeQuery i q s = QueryData (DataStoreInfo i) (FilterMutable q) ~ SelTags i s




--runModsF :: ComputeSelection cls cont q ~ s => (Proxy (q :: [*])) -> (Query q s -> Info idx el cls cont -> sig) -> sig
--runModsF _ f = f Query Info


--runModsF' = flip runModsF



--type family ContainerOf a
--class HasContainer a where
--    container :: Lens' a (ContainerOf a)

--type family DataStoreOf a

--class HasDataStore a where
--    dataStore :: Lens' a (DataStoreOf a)

--class HasDataStore a => IsDataStore a where
--    fromDataStore :: DataStoreOf a -> a



--type family InfoSelection i q where InfoSelection   (Info idx el cls cont) q = ComputeSelection cls cont q
--type family DataStoreInfo i   where DataStoreInfo   (Info idx el cls cont)   = Info idx el cls (DataStoreOf cont)



--type family InfoInst info q m :: Constraint where
--    InfoInst (Info NA  NA cls cont) q m = cls        cont m q (ComputeSelection cls cont q)
--    InfoInst (Info NA  el cls cont) q m = cls     el cont m q (ComputeSelection cls cont q)
--    InfoInst (Info idx NA cls cont) q m = cls idx    cont m q (ComputeSelection cls cont q)
--    InfoInst (Info idx el cls cont) q m = cls idx el cont m q (ComputeSelection cls cont q)






------






--type family Ixed (op :: k) :: k where Ixed (cls q (m ::  * -> *) :: * -> Constraint) = cls (AppendLst Mods.Ixed q) m
--                                      Ixed (cls q    :: (* -> *) -> * -> Constraint) = cls (AppendLst Mods.Ixed q)



--type family Unchecked (op :: k) :: k where Unchecked (cls q (m ::  * -> *) :: * -> Constraint) = cls (AppendLst Mods.Unchecked q) m
--                                           Unchecked (cls q    :: (* -> *) -> * -> Constraint) = cls (AppendLst Mods.Unchecked q)








type family Ixed (op :: k) :: k where
    Ixed (op (ms :: [*]) (ps :: [*]))               = op (Mods.Ixed ': ms) ps
    Ixed (op (ms :: [*]) (ps :: [*]) (m :: * -> *)) = op (Mods.Ixed ': ms) ps m

---- === Concatenation ===








--type family IxedMode (a :: k) :: IxedType

--data IxedType = Multi
--              | Single
--              deriving (Show)



----type family ClassOf (a :: *) :: k

----------------------------------







--newtype NestedFunctor m n a = NestedFunctor { fromNestedFunctor :: m (n a)} deriving (Show)
--instance (Functor m, Functor n) => Functor (NestedFunctor m n) where fmap f = NestedFunctor . (fmap $ fmap f) . fromNestedFunctor


--nested :: (Functor m, Functor n) => Lens a b c d -> (c -> m (n d)) -> (a -> m (n b))
--nested l f = fromNestedFunctor . l (fmap NestedFunctor f)





--data Result d r = Result d r deriving (Show, Functor)

---- Result utils

--simple' = Result ()
--res     = Result . (,())
--resM    = return .: res
--simpleM = return . simple'

--withResData :: (d -> (out, d')) -> Result d r -> (out, Result d' r)
--withResData f (Result d r) = (out, Result d' r) where
--  (out, d') = f d

--withResData_ :: (d -> d') -> Result d r -> Result d' r
--withResData_ = flattenMod withResData

--splitResData :: Result (d,ds) r -> (d, Result ds r)
--splitResData = withResData id

--flattenMod :: Functor f => (f ((), a) -> b -> (x, c)) -> f a -> b -> c
--flattenMod f = snd .: (f . fmap ((),))



----type Unique lst = Reverse (Unique' lst '[])
--type Unique lst = (Unique2' lst)

--type family Unique' (lst :: [*]) (reg :: [*]) where
--  Unique' '[]       reg = reg
--  Unique' (l ': ls) reg = Unique' ls (If (l `In` reg) reg (l ': reg))

--type family Unique2' (lst :: [*]) where
--  Unique2' '[]       = '[]
--  Unique2' (l ': ls) = l ': Unique2' (Remove l ls)




--uniqueProxy :: Proxy a -> Proxy (Unique a)
--uniqueProxy _ = Proxy






--newtype Flipped t a b = Flipped { fromFlipped :: t b a } deriving Show

--instance Functor (Flipped Result r) where fmap f (Flipped (Result d r)) = Flipped (Result (f d) r)


--withFlipped f = fromFlipped . f . Flipped



--foo f (info :: Proxy (cls :: k)) (q :: Proxy (q :: [*])) (tc :: cont) = out where
--    tc2 = runModsF' f (uniqueProxy q) tc
--    tc3 = withFlipped (fmap $ taggedCont (Proxy :: Proxy (Selected (ComputeSelection cls cont q) (FilterMutable (ModsOf cls cont))) )) <$> tc2
--    out = tc3

----bar :: OpCtx ExpandableInfo2 q m t => Proxy q -> t -> m (Result (MyResult ExpandableInfo2 q t) t)
--bar f info q t = out where
--    q'    = filterMutable q
--    cont  = view container t
--    tgdr  = foo f info q cont
--    tgdr' = (fmap . fmap) (\c -> t & container .~ c) tgdr
--    out   = withFlipped (fmap (fillData q')) <$> tgdr'


--barTx f (cls :: Proxy (cls :: k)) (q :: Proxy (q :: [*])) (t :: t) = withFlipped (fmap (fillData (filterMutable q))) <$> nested container tgdr t where
--    tgdr c  = withFlipped (fmap $ taggedCont (Proxy :: Proxy (Selected (ComputeSelection cls (ContainerOf t) q) (FilterMutable (ModsOf cls (ContainerOf t)))) )) <$> f (uniqueProxy q) c


--barTy f (cls :: Proxy (cls :: k)) (q :: Proxy (q :: [*])) (t :: t) = withFlipped (fmap (fillData (filterMutable q))) <$> tgdr (view container t) where
--    tgdr c  = withFlipped (fmap $ taggedCont (Proxy :: Proxy (Selected (ComputeSelection cls (ContainerOf t) q) (FilterMutable (ModsOf cls (ContainerOf t)))) )) <$> f (uniqueProxy q) c

----bar2z f (cls :: Proxy (cls :: k)) (q :: Proxy (q :: [*])) (t :: t) = withFlipped (fmap (fillData (filterMutable q))) <$> tgdr (view container t) where
----    tgdr c  = withFlipped (fmap $ taggedCont (Proxy :: Proxy (Selected (ComputeSelection cls (ContainerOf t) q) (FilterMutable (ModsOf cls (ContainerOf t)))) )) <$> f (uniqueProxy q) c



--type family AssumeRtupConv q t :: Constraint where AssumeRtupConv q t = If' (Mods.FilterMutable q :== '[]) (AsRTup t ~ (t,())) ()

--type family OpCtx info q m t where OpCtx (Info idx el cls) q m t = ((Functor m,
--                                               HasContainer t,
--                                               DataFillable
--                                                 (FilterMutable q)
--                                                 (TaggedCont
--                                                    (Selected
--                                                       (LstIn
--                                                          (ModsOf cls (ContainerOf t)) q)
--                                                       (FilterMutable
--                                                          (ModsOf cls (ContainerOf t))))
--                                                    (QueryData
--                                                       (Info idx el cls (DataStoreOf t))
--                                                       (Selected
--                                                          (LstIn
--                                                             (ModsOf cls (ContainerOf t))
--                                                             (Unique q))
--                                                          (FilterMutable
--                                                             (ModsOf
--                                                                cls (ContainerOf t)))))),
--                                               Taggable
--                                                 (Selected
--                                                    (LstIn
--                                                       (ModsOf cls (ContainerOf t)) q)
--                                                    (FilterMutable
--                                                       (ModsOf cls (ContainerOf t))))
--                                                 (QueryData
--                                                    (Info idx el cls (DataStoreOf t))
--                                                    (Selected
--                                                       (LstIn
--                                                          (ModsOf cls (ContainerOf t))
--                                                          (Unique q))
--                                                       (FilterMutable
--                                                          (ModsOf
--                                                             cls (ContainerOf t))))),
--                                               QueryData
--                                                 (Info idx el cls (DataStoreOf t))
--                                                 (FilterMutable (Unique q))
--                                               ~ QueryData
--                                                   (Info idx el cls (DataStoreOf t))
--                                                   (Selected
--                                                      (LstIn
--                                                         (ModsOf cls (ContainerOf t))
--                                                         (Unique q))
--                                                      (FilterMutable
--                                                         (ModsOf cls (ContainerOf t)))),
--                                               QueryData
--                                                 (Info idx el cls (DataStoreOf t))
--                                                 (FilterMutable q)
--                                               ~ FillData
--                                                   (FilterMutable q)
--                                                   (TaggedCont
--                                                      (Selected
--                                                         (LstIn
--                                                            (ModsOf cls (ContainerOf t))
--                                                            q)
--                                                         (FilterMutable
--                                                            (ModsOf
--                                                               cls (ContainerOf t))))
--                                                      (QueryData
--                                                         (Info idx el cls (DataStoreOf t))
--                                                         (Selected
--                                                            (LstIn
--                                                               (ModsOf
--                                                                  cls (ContainerOf t))
--                                                               (Unique q))
--                                                            (FilterMutable
--                                                               (ModsOf
--                                                                  cls
--                                                                  (ContainerOf t))))))),

--                                                                  -- manual
--                                                                  Functor m,
--                                                                  AssumeRtupConv q t,
--                                                                  IsContainer t,
--                                                                  InfoInst (Info idx el cls (ContainerOf t)) (Unique q) m,
--                                                                  DataStoreOf (ContainerOf t) ~ DataStoreOf t,
--                                                                  (QueryData (Info idx el cls (DataStoreOf t)) (FilterMutable q) ~ QueryData (Info idx el cls (DataStoreOf t)) (FilterMutable q)))


--type family TransCheck q info info' t where
--    TransCheck q (Info idx el cls) info' t = (FillData
--                        (FilterMutable q)
--                        (TaggedCont
--                           (Selected
--                              (LstIn (ModsOf cls (ContainerOf t)) q)
--                              (FilterMutable (ModsOf cls (ContainerOf t))))
--                           (QueryData
--                              (Info idx el cls (DataStoreOf t))
--                              (Selected
--                                 (LstIn
--                                    (ModsOf cls (ContainerOf t))
--                                    (Unique q))
--                                 (FilterMutable (ModsOf cls (ContainerOf t))))))
--                      ~ QueryData
--                          (info' (DataStoreOf t)) (FilterMutable q))






----type family Test (a :: k) where Test a = (If a :== (t1,t2)) True True


----type family Match

--class IsTuple a (is :: Bool) | a -> is

--instance {-# OVERLAPPABLE #-} is ~ False => IsTuple a is
--instance                                    IsTuple () True
--instance                                    IsTuple (t1,t2) True
--instance                                    IsTuple (t1,t2,t3) True
--instance                                    IsTuple (t1,t2,t3,t4) True
--instance                                    IsTuple (t1,t2,t3,t4,t5) True
--instance                                    IsTuple (t1,t2,t3,t4,t5,t6) True
--instance                                    IsTuple (t1,t2,t3,t4,t5,t6,t7) True
--instance                                    IsTuple (t1,t2,t3,t4,t5,t6,t7,t8) True
--instance                                    IsTuple (t1,t2,t3,t4,t5,t6,t7,t8,t9) True

---- FIXME [WD]: below ToTupCtx* refer to need of AssumeRtupConv function, which adds special case context when we are returning only single value from Rtuple (t,())
---- It is not seen properly byGHC though
----type family ToTupCtx a :: Constraint where
----  ToTupCtx (t,()) = (AsRTup t ~ (t,()))
----  ToTupCtx t      = ()

----type family ToTupCtx2 a :: Constraint where
----  ToTupCtx2 (t1,t2) = ()
----  ToTupCtx2 (t1,t2,t3) = ()
----  ToTupCtx2 (t1,t2,t3,t4) = ()
----  ToTupCtx2 (t1,t2,t3,t4,t5) = ()
----  ToTupCtx2 (t1,t2,t3,t4,t5,t6) = ()
----  ToTupCtx2 (t1,t2,t3,t4,t5,t6,t7) = ()
----  ToTupCtx2 (t1,t2,t3,t4,t5,t6,t7,t8) = ()
----  ToTupCtx2 (t1,t2,t3,t4,t5,t6,t7,t8,t9) = ()
----  ToTupCtx2 t = (AsRTup t ~ (t,()))

--  ---- Utils

--type family   AsTup a
--type instance AsTup () = ()
--type instance AsTup (t1,()) = t1
--type instance AsTup (t1,(t2,())) = (t1,t2)
--type instance AsTup (t1,(t2,(t3,()))) = (t1,t2,t3)
--type instance AsTup (t1,(t2,(t3,(t4,())))) = (t1,t2,t3,t4)
--type instance AsTup (t1,(t2,(t3,(t4,(t5,()))))) = (t1,t2,t3,t4,t5)
--type instance AsTup (t1,(t2,(t3,(t4,(t5,(t6,())))))) = (t1,t2,t3,t4,t5,t6)
--type instance AsTup (t1,(t2,(t3,(t4,(t5,(t6,(t7,()))))))) = (t1,t2,t3,t4,t5,t6,t7)
--type instance AsTup (t1,(t2,(t3,(t4,(t5,(t6,(t7,(t8,())))))))) = (t1,t2,t3,t4,t5,t6,t7,t8)
--type instance AsTup (t1,(t2,(t3,(t4,(t5,(t6,(t7,(t8,(t9,()))))))))) = (t1,t2,t3,t4,t5,t6,t7,t8,t9)

--type family   AsRTup a where
--    AsRTup () = ()
--    AsRTup (t1,t2) = (t1,(t2,()))
--    AsRTup (t1,t2,t3) = (t1,(t2,(t3,())))
--    AsRTup (t1,t2,t3,t4) = (t1,(t2,(t3,(t4,()))))
--    AsRTup (t1,t2,t3,t4,t5) = (t1,(t2,(t3,(t4,(t5,())))))
--    AsRTup (t1,t2,t3,t4,t5,t6) = (t1,(t2,(t3,(t4,(t5,(t6,()))))))
--    AsRTup (t1,t2,t3,t4,t5,t6,t7) = (t1,(t2,(t3,(t4,(t5,(t6,(t7,())))))))
--    AsRTup (t1,t2,t3,t4,t5,t6,t7,t8) = (t1,(t2,(t3,(t4,(t5,(t6,(t7,(t8,()))))))))
--    AsRTup (t1,t2,t3,t4,t5,t6,t7,t8,t9) = (t1,(t2,(t3,(t4,(t5,(t6,(t7,(t8,(t9,())))))))))
--    AsRTup a = (a,())


--class    a ~ AsRTup (AsTup a) => ToTup a  where toTup :: a -> AsTup a
--instance ToTup () where toTup _ = ()
--instance AsRTup t1 ~ (t1,()) => ToTup (t1,()) where toTup (t1,()) = t1
--instance ToTup (t1,(t2,())) where toTup (t1,(t2,())) = (t1,t2)
--instance ToTup (t1,(t2,(t3,()))) where toTup (t1,(t2,(t3,()))) = (t1,t2,t3)
--instance ToTup (t1,(t2,(t3,(t4,())))) where toTup (t1,(t2,(t3,(t4,())))) = (t1,t2,t3,t4)
--instance ToTup (t1,(t2,(t3,(t4,(t5,()))))) where toTup (t1,(t2,(t3,(t4,(t5,()))))) = (t1,t2,t3,t4,t5)
--instance ToTup (t1,(t2,(t3,(t4,(t5,(t6,())))))) where toTup (t1,(t2,(t3,(t4,(t5,(t6,())))))) = (t1,t2,t3,t4,t5,t6)
--instance ToTup (t1,(t2,(t3,(t4,(t5,(t6,(t7,()))))))) where toTup (t1,(t2,(t3,(t4,(t5,(t6,(t7,()))))))) = (t1,t2,t3,t4,t5,t6,t7)
--instance ToTup (t1,(t2,(t3,(t4,(t5,(t6,(t7,(t8,())))))))) where toTup (t1,(t2,(t3,(t4,(t5,(t6,(t7,(t8,())))))))) = (t1,t2,t3,t4,t5,t6,t7,t8)
--instance ToTup (t1,(t2,(t3,(t4,(t5,(t6,(t7,(t8,(t9,()))))))))) where toTup (t1,(t2,(t3,(t4,(t5,(t6,(t7,(t8,(t9,()))))))))) = (t1,t2,t3,t4,t5,t6,t7,t8,t9)

--type SimpleRes a = AsRTup a ~ (a, ())








type Simple (t :: [*] -> [*] -> k) = t '[] '[]