Agda.TypeChecking.Monad.Exception

Basically a copy of the ErrorT monad transformer. It's handy to slap onto TCM and still be a MonadTCM (which isn't possible with ErrorT).

Documentation

newtype ExceptionT err m a

Constructors

ExceptionT

Fields

• runExceptionT :: m (Either err a)

Instances

(Error err, MonadError err' m) => MonadError err' (ExceptionT err m)

Methods

throwError :: err' -> ExceptionT err m a

catchError :: ExceptionT err m a -> (err' -> ExceptionT err m a) -> ExceptionT err m a

(Error err, MonadReader r m) => MonadReader r (ExceptionT err m)

Methods

ask :: ExceptionT err m r

local :: (r -> r) -> ExceptionT err m a -> ExceptionT err m a

reader :: (r -> a) -> ExceptionT err m a

(Error err, MonadState s m) => MonadState s (ExceptionT err m)

Methods

get :: ExceptionT err m s

put :: s -> ExceptionT err m ()

state :: (s -> (a, s)) -> ExceptionT err m a

(Monad m, Error err) => MonadException err (ExceptionT err m)

Methods

throwException :: err -> ExceptionT err m a

catchException :: ExceptionT err m a -> (err -> ExceptionT err m a) -> ExceptionT err m a

MonadTrans (ExceptionT err)

Methods

lift :: Monad m => m a -> ExceptionT err m a

(Monad m, Error err) => Monad (ExceptionT err m)

Methods

(>>=) :: ExceptionT err m a -> (a -> ExceptionT err m b) -> ExceptionT err m b

(>>) :: ExceptionT err m a -> ExceptionT err m b -> ExceptionT err m b

return :: a -> ExceptionT err m a

fail :: String -> ExceptionT err m a

Functor f => Functor (ExceptionT err f)

Methods

fmap :: (a -> b) -> ExceptionT err f a -> ExceptionT err f b

(<$) :: a -> ExceptionT err f b -> ExceptionT err f a

(Error err, Applicative m, Monad m) => Applicative (ExceptionT err m)

Methods

pure :: a -> ExceptionT err m a

(<*>) :: ExceptionT err m (a -> b) -> ExceptionT err m a -> ExceptionT err m b

(*>) :: ExceptionT err m a -> ExceptionT err m b -> ExceptionT err m b

(<*) :: ExceptionT err m a -> ExceptionT err m b -> ExceptionT err m a

(Error err, MonadIO m) => MonadIO (ExceptionT err m)

Methods

liftIO :: IO a -> ExceptionT err m a

(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm)

Methods

liftTCM :: TCM a -> ExceptionT err tcm a

(HasConstInfo m, Error err) => HasConstInfo (ExceptionT err m)

Methods

getConstInfo :: QName -> ExceptionT err m Definition

getRewriteRulesFor :: QName -> ExceptionT err m RewriteRules

class Error err => MonadException err m | m -> err where

Minimal complete definition

throwException, catchException

Methods

throwException :: err -> m a

catchException :: m a -> (err -> m a) -> m a

Instances

(Monad m, MonadException err m) => MonadException err (StateT s m)

Methods

throwException :: err -> StateT s m a

catchException :: StateT s m a -> (err -> StateT s m a) -> StateT s m a

(Monad m, MonadException err m, Monoid w) => MonadException err (WriterT w m)

Methods

throwException :: err -> WriterT w m a

catchException :: WriterT w m a -> (err -> WriterT w m a) -> WriterT w m a

(Monad m, Error err) => MonadException err (ExceptionT err m)

Methods

throwException :: err -> ExceptionT err m a

catchException :: ExceptionT err m a -> (err -> ExceptionT err m a) -> ExceptionT err m a

(Monad m, MonadException err m) => MonadException err (ReaderT * r m)

Methods

throwException :: err -> ReaderT * r m a

catchException :: ReaderT * r m a -> (err -> ReaderT * r m a) -> ReaderT * r m a