{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{- |
Module: Control.Monad.Trans.Uplift
Description: Uplift substacks of monad transformer stacks
Copyright: (c) Samuel Schlesinger 2020
Maintainer: sgschlesinger@gmail.com
Stability: experimental
Portability: POSIX, Windows
-}
module Control.Monad.Trans.Uplift
  ( uplift
  , Substack(..)
  , Uplift
  , IndexOf
  , N(..)
  ) where

import Control.Monad.Trans (MonadTrans(lift))

-- | Type level natural numbers
data N = S N | Z

-- | A type family for computing the substack of a monad transformer stack,
-- dropping the top n transformers.
type family Substack n f where
  Substack 'Z f = f
  Substack ('S n) (t f) = Substack n f

-- | A class for lifting arbitrary substacks of our transformer stack.
class Uplift n f where
  liftSubstack :: Substack n f a -> f a

instance Uplift 'Z f where
  liftSubstack :: Substack 'Z f a -> f a
liftSubstack = Substack 'Z f a -> f a
forall a. a -> a
id

instance (Monad f, MonadTrans t, Uplift n f) => Uplift ('S n) (t f) where
  liftSubstack :: Substack ('S n) (t f) a -> t f a
liftSubstack = f a -> t f a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (f a -> t f a)
-> (Substack n f a -> f a) -> Substack n f a -> t f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (n :: N) (f :: k -> *) (a :: k).
Uplift n f =>
Substack n f a -> f a
forall (f :: * -> *) a. Uplift n f => Substack n f a -> f a
liftSubstack @n

-- | A type family for computing the index of a particular transformer in
-- a stack.
type family IndexOf t f where
  IndexOf t (t f) = 'Z
  IndexOf t (t' f) = 'S (IndexOf t f)

-- | Uplift the substack starting with the given transformer into the full
-- stack. This function is expected to be used with type applications when
-- working with polymorphic code.
uplift :: forall t f a. Uplift (IndexOf t f) f => Substack (IndexOf t f) f a -> f a
uplift :: Substack (IndexOf t f) f a -> f a
uplift = forall k (n :: N) (f :: k -> *) (a :: k).
Uplift n f =>
Substack n f a -> f a
forall (f :: k -> *) (a :: k).
Uplift (IndexOf t f) f =>
Substack (IndexOf t f) f a -> f a
liftSubstack @(IndexOf t f)