module Type.Yoko.MFun where
import Type.Yoko.TSTSS
import Type.Yoko.Type
import Type.Yoko.Universe
import Type.Yoko.Natural
import Type.Yoko.Fun
import Data.Yoko.Generic
newtype RMMap u fn m c = RMMap (NT u (fn m))
type family MApp (fn :: * -> * -> *) m
type instance Dom (RMMap u fn m) c = RM m c
type instance Rng (RMMap u fn m) c = RM (MApp fn m) c
type instance MApp (RMMap u fn) m = MApp fn m
instance (t ::: u, t ::: Domain (fn m), Wrapper (fn m),
Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med (MApp fn m) t
) => R t ::: Domain (RMMap u fn m) where
inhabits = AppBy $ \(RMMap fns) ->
R . apply (fns `appNTF` inhabitsFor [qP|t|]) . unR
instance (Rep t ::: Domain (RMMap u fn m), Generic t
) => N t ::: Domain (RMMap u fn m) where
inhabits = AppBy $ \(RMMap fn) -> obj . apply (RMMap fn) . rep
instance D a ::: Domain (RMMap u fn m) where inhabits = AppBy $ \_ -> D . unD
instance U ::: Domain (RMMap u fn m) where inhabits = AppBy $ \_ _ -> U
instance (Functor f, c ::: Domain (RMMap u fn m)
) => F f c ::: Domain (RMMap u fn m) where
inhabits = AppBy $ \(RMMap fn) -> F . fmap (apply (RMMap fn)) . unF
instance (c ::: Domain (RMMap u fn m), d ::: Domain (RMMap u fn m),
FunctorTSTSS ff) => FF ff c d ::: Domain (RMMap u fn m) where
inhabits = AppBy $ \(RMMap fn) -> FF .
fmapTSTSS (apply (RMMap fn)) (apply (RMMap fn)) . unFF
instance (c ::: Domain (RMMap u fn m)) => M i c ::: Domain (RMMap u fn m) where
inhabits = AppBy $ \(RMMap fn) -> M . apply (RMMap fn) . unM
type instance DomF (RMMap u fn m) = RM m
type instance RngF (RMMap u fn m) = RM (MApp fn m)
newtype FromAt m n a = FromAt {toAt :: Med n a -> Med m a}
type instance Unwrap (FromAt m n) a = Med n a -> Med m a
instance Wrapper (FromAt m n) where wrap = FromAt; unwrap (FromAt x) = x
type instance Dom (FromAt m n) t = Med n t
type instance Rng (FromAt m n) t = Med m t
instance a ::: Domain (FromAt m n) where inhabits = AppBy toAt
type instance MApp (FromAt m) n = m