{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
  ScopedTypeVariables, UndecidableInstances, QuasiQuotes, TypeFamilies,
  GADTs, TypeOperators, Rank2Types #-}

{- |

Module      :  Type.Yoko.MFun
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

An enrichment of "Type.Yoko.Fun" where functions must be of kind @* -> * -> *@;
the first parameter is a mediator and the second is (as expected by
"Type.Yoko.Fun") the type at which the function is to be instantiated.

-}

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




-- | mediator-functions can be mapped across an 'RM' type/value.
newtype RMMap u fn m c = RMMap (NT u (fn m))

{- | mediator-functions can also modify the mediator; e.g.

@
  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 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)




-- | A @FromAt@ function is applicable only at the specified mediator and type;
-- crucially @type instance MApp (FromAt m) n = 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