{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}
-- | See overview in the README.md
module Control.Monad.Trans.Unlift
    ( -- * Trans
      MonadTransUnlift
    , Unlift (..)
    , askUnlift
    , askRun
      -- * Base
    , MonadBaseUnlift
    , UnliftBase (..)
    , askUnliftBase
    , askRunBase
      -- * Reexports
    , MonadTrans (..)
    , MonadBase (..)
    , MonadTransControl (..)
    , MonadBaseControl (..)
    ) where

import           Control.Monad               (liftM)
import           Control.Monad.Base          (MonadBase (..))
import           Control.Monad.Trans.Class   (MonadTrans (..))
import           Control.Monad.Trans.Control (MonadBaseControl (..),
                                              MonadTransControl (..))
import           Data.Constraint             ((:-), (\\))
import           Data.Constraint.Forall      (Forall, inst)

-- | A function which can move an action down the monad transformer stack, by
-- providing any necessary environment to the action.
--
-- Note that, if ImpredicativeTypes worked reliably, this type wouldn't be
-- necessary, and 'askUnlift' would simply include a more generalized type.
--
-- Since 0.1.0
newtype Unlift t = Unlift { unlift :: forall a n. Monad n => t n a -> n a }

class    (StT t a ~ a) => Identical t a
instance (StT t a ~ a) => Identical t a

-- | A monad transformer which can be unlifted, obeying the monad morphism laws.
--
-- Since 0.1.0
class    (MonadTransControl t, Forall (Identical t)) => MonadTransUnlift t
instance (MonadTransControl t, Forall (Identical t)) => MonadTransUnlift t

mkUnlift :: forall t m a . (Forall (Identical t), Monad m)
         => (forall n b. Monad n => t n b -> n (StT t b)) -> t m a -> m a
mkUnlift r act = r act \\ (inst :: Forall (Identical t) :- Identical t a)

-- | Get the 'Unlift' action for the current transformer layer.
--
-- Since 0.1.0
askUnlift :: forall t m. (MonadTransUnlift t, Monad m) => t m (Unlift t)
askUnlift = liftWith unlifter
  where
    unlifter :: (forall n b. Monad n => t n b -> n (StT t b)) -> m (Unlift t)
    unlifter r = return $ Unlift (mkUnlift r)

-- | A simplified version of 'askUnlift' which addresses the common case where
-- polymorphism isn't necessary.
--
-- Since 0.1.0
askRun :: (MonadTransUnlift t, Monad (t m), Monad m) => t m (t m a -> m a)
askRun = liftM unlift askUnlift
{-# INLINE askRun #-}

-- | Similar to 'Unlift', but instead of moving one layer down the stack, moves
-- the action to the base monad.
--
-- Since 0.1.0
newtype UnliftBase b m = UnliftBase { unliftBase :: forall a. m a -> b a }

class    (StM m a ~ a) => IdenticalBase m a
instance (StM m a ~ a) => IdenticalBase m a

-- | A monad transformer stack which can be unlifted, obeying the monad morphism laws.
--
-- Since 0.1.0
class (MonadBaseControl b m, Forall (IdenticalBase m)) => MonadBaseUnlift b m | m -> b
instance (MonadBaseControl b m, Forall (IdenticalBase m)) => MonadBaseUnlift b m

mkUnliftBase :: forall m a b. (Forall (IdenticalBase m), Monad b)
             => (forall c. m c -> b (StM m c)) -> m a -> b a
mkUnliftBase r act = r act \\ (inst :: Forall (IdenticalBase m) :- IdenticalBase m a)

-- | Get the 'UnliftBase' action for the current transformer stack.
--
-- Since 0.1.0
askUnliftBase :: forall b m. (MonadBaseUnlift b m) => m (UnliftBase b m)
askUnliftBase = liftBaseWith unlifter
  where
    unlifter :: (forall c. m c -> b (StM m c)) -> b (UnliftBase b m)
    unlifter r = return $ UnliftBase (mkUnliftBase r)

-- | A simplified version of 'askUnliftBase' which addresses the common case
-- where polymorphism isn't necessary.
--
-- Since 0.1.0
askRunBase :: (MonadBaseUnlift b m)
           => m (m a -> b a)
askRunBase = liftM unliftBase askUnliftBase
{-# INLINE askRunBase #-}