content: {-# LANGUAGE CPP #-}
  {-# OPTIONS_HADDOCK not-home #-}
  module Control.Effect.Carrier.Internal.Compose where
  
  import Control.Applicative
  import Control.Monad
  import qualified Control.Monad.Fail as Fail
  import Control.Monad.Trans
  import Control.Monad.Trans.Identity
  import Control.Monad.Fix
  import Control.Effect.Internal
  import Control.Effect.Internal.Derive
  import Control.Effect.Internal.Utils
  import Control.Monad.Trans.Control
  
  import Unsafe.Coerce
  
  -- | Composition of monad/carrier transformers.
  newtype ComposeT t (u :: (Type -> Type) -> Type -> Type) m a = ComposeT {
      getComposeT :: t (u m) a
    }
    deriving ( Functor, Applicative, Monad
             , Alternative, MonadPlus
             , MonadFix, MonadFail, MonadIO
             , MonadThrow, MonadCatch, MonadMask
             , MonadBase b, MonadBaseControl b
             , Carrier
             )
  
  instance ( MonadTrans t
           , MonadTrans u
           , forall m. Monad m => Monad (u m)
           )
        => MonadTrans (ComposeT t u) where
    lift m = ComposeT (lift (lift m))
    {-# INLINEABLE lift #-}
  
  instance ( MonadTransControl t
           , MonadTransControl u
           , forall m. Monad m => Monad (u m)
           )
        => MonadTransControl (ComposeT t u) where
    type StT (ComposeT t u) a = StT u (StT t a)
  
    liftWith main = ComposeT $
      liftWith $ \lowerT ->
      liftWith $ \lowerU ->
      main (lowerU . lowerT .# getComposeT)
    {-# INLINEABLE liftWith #-}
  
    restoreT m = ComposeT (restoreT (restoreT m))
    {-# INLINEABLE restoreT #-}
  
  -- | Composition of a list of carrier transformers.
  --
  -- This is useful when you have multiple interpretations whose
  -- carriers you'd like to treat as one larger object, such that
  -- 'lift' lifts past all those carriers.
  --
  -- For example:
  --
  -- @
  -- data Counter m a where
  --   Probe :: Counter m Int
  --
  -- type CounterC = 'CompositionC'
  --   '[ 'Control.Effect.ReinterpretSimpleC' Counter '['Control.Effect.State.State' Int]
  --    , 'Control.Effect.State.StateC' Int
  --    ]
  --
  -- runCounter :: ('Control.Effect.Carrier' m, 'Control.Effect.Threaders' '['Control.Effect.State.StateThreads'] m p)
  --            => CounterC m a
  --            -> m a
  -- runCounter =
  --    'Control.Effect.State.runState' 0
  --  . 'Control.Effect.reinterpretSimple' (\case
  --      Probe -> 'Control.Effect.State.state'' (\s -> (s+1,s))
  --    )
  --  . 'runComposition'
  -- @
  --
  -- Then you have @'lift' :: Monad m => m a -> CounterC m a@
  newtype CompositionC ts m a = CompositionC {
      unCompositionC :: CompositionBaseT ts m a
    }
  
  #define DERIVE_COMP_M(ctx)                            \
  deriving newtype instance ctx (CompositionBaseT ts m) \
                         => ctx (CompositionC ts m)
  
  #define DERIVE_COMP_T(ctx)                          \
  deriving newtype instance ctx (CompositionBaseT ts) \
                         => ctx (CompositionC ts)
  
  DERIVE_COMP_M(Functor)
  DERIVE_COMP_M(Applicative)
  DERIVE_COMP_M(Monad)
  DERIVE_COMP_M(Alternative)
  DERIVE_COMP_M(MonadPlus)
  DERIVE_COMP_M(MonadFix)
  DERIVE_COMP_M(Fail.MonadFail)
  DERIVE_COMP_M(MonadIO)
  DERIVE_COMP_M(MonadThrow)
  DERIVE_COMP_M(MonadCatch)
  DERIVE_COMP_M(MonadMask)
  
  -- Yes, this is necessary. Don't ask, I haven't got a clue.
  deriving newtype instance (Monad b, MonadBase b (CompositionBaseT ts m))
                         => MonadBase b (CompositionC ts m)
  DERIVE_COMP_M(MonadBaseControl b)
  DERIVE_COMP_M(Carrier)
  
  DERIVE_COMP_T(MonadTrans)
  DERIVE_COMP_T(MonadTransControl)
  
  -- KingoftheHomeless: Why a left fold? Consider:
  --
  --   CompositionBaseT [t, u, v] m a
  -- = ComposeT (ComposeT (ComposeT IdentityT t) u) v m a
  -- ~ ComposeT (ComposeT IdentityT t) u (v m) a
  -- ~ ComposeT IdentityT t (u (v m)) a
  -- ~ IdentityT (t (u (v m))) a
  -- ~ t (u (v m)) a
  --
  -- Where "~" is representational equality.
  --
  -- In contrast, imagine if CompositionBaseT were a right fold, instead. Then we'd get:
  --
  --   CompositionBaseT [t, u, v] m a
  -- = ComposeT t (ComposeT u (ComposeT v IdentityT)) m a
  -- ~ t (ComposeT u (ComposeT v IdentityT) m) a
  --
  -- ... and we can't reduce this further. Why? Because t,u,v may not be representational in the monads they're transforming!
  -- This matters! In fact, this library even makes use of monad transformers that aren't representational in the monad,
  -- such as InterpretSimpleC.
  --
  -- So only with a left fold can we guarantee that the unsafeCoerce in runComposition is safe.
  type family CompositionBaseT' acc ts :: (Type -> Type) -> Type -> Type where
    CompositionBaseT' acc '[] = acc
    CompositionBaseT' acc (t ': ts) = CompositionBaseT' (ComposeT acc t) ts
  
  type CompositionBaseT ts = CompositionBaseT' IdentityT ts
  
  type family CompositionBaseM (ts :: [(Type -> Type) -> Type -> Type]) (m :: Type -> Type) where
    CompositionBaseM '[] m = m
    CompositionBaseM (t ': ts) m = t (CompositionBaseM ts m)
  
  
  
  -- | Transform @'CompositionC' [t1, t2, ..., tn] m a@ to @t1 (t2 (... (tn m) ...)) a@
  runComposition :: CompositionC ts m a
                 -> CompositionBaseM ts m a
  -- This is a safe use of 'unsafeCoerce'; the two types are always representationally equal,
  -- without even needing the transformers in ts to be representational.
  -- GHC can only prove that, however, if ts is concrete. We could stick a 'Coercible' constraint,
  -- but in order to prove that constraint, both ComposeT and IdentityT needs to be in scope for the
  -- user.
  -- This seems like too much of a hassle, so unsafeCoerce is used instead.
  --
  -- TODO(KingoftheHomeless): Investigate if the use of unsafeCoerce messes up optimizations.
  runComposition = unsafeCoerce
  {-# INLINE runComposition #-}
  