{-# LANGUAGE UndecidableInstances #-}
module Control.Monad.Classes.Core where
import GHC.Prim (Proxy#, proxy#)
import Control.Monad.Trans.Class
import Data.Peano (Peano (..))
type family CanDo (m :: (* -> *)) (eff :: k) :: Bool
type family MapCanDo (eff :: k) (stack :: * -> *) :: [Bool] where
MapCanDo eff (t m) = (CanDo (t m) eff) ': MapCanDo eff m
MapCanDo eff m = '[ CanDo m eff ]
type family FindTrue
(bs :: [Bool])
:: Peano
where
FindTrue (True ': t) = Zero
FindTrue (False ': t) = Succ (FindTrue t)
type Find eff (m :: * -> *) =
FindTrue (MapCanDo eff m)
class MonadLiftN (n :: Peano) m
where
type Down n m :: * -> *
liftN :: Proxy# n -> Down n m a -> m a
instance MonadLiftN Zero m
where
type Down Zero m = m
liftN _ = id
instance
( MonadLiftN n m
, MonadTrans t
, Monad m
) => MonadLiftN (Succ n) (t m)
where
type Down (Succ n) (t m) = Down n m
liftN _ = lift . liftN (proxy# :: Proxy# n)