    module Agda.Interaction.Options.HasOptions
      ( HasOptions (pragmaOptions, commandLineOptions)
      ) where

    import Control.Monad.Except (ExceptT)
    import Control.Monad.Reader (ReaderT)
    import Control.Monad.State (StateT)
    import Control.Monad.Trans ( MonadTrans, lift )
    import Control.Monad.Trans.Identity (IdentityT)
    import Control.Monad.Trans.Maybe (MaybeT)
    import Control.Monad.Writer (WriterT)

    import Agda.Interaction.Options.Base (PragmaOptions, CommandLineOptions)
    import Agda.Utils.Update (ChangeT)
    import Agda.Utils.ListT (ListT)

    class (Functor m, Applicative m, Monad m) => HasOptions m where
      -- | Returns the pragma options which are currently in effect.
      pragmaOptions      :: m PragmaOptions
      -- | Returns the command line options which are currently in effect.
      commandLineOptions :: m CommandLineOptions

      default pragmaOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m PragmaOptions
      pragmaOptions      = n PragmaOptions -> t n PragmaOptions
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift n PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

      default commandLineOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m CommandLineOptions
      commandLineOptions = n CommandLineOptions -> t n CommandLineOptions
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift n CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions

    -- HasOptions lifts through monad transformers
    -- (see default signatures in the HasOptions class).

    instance HasOptions m => HasOptions (ChangeT m)
    instance HasOptions m => HasOptions (ExceptT e m)
    instance HasOptions m => HasOptions (IdentityT m)
    instance HasOptions m => HasOptions (ListT m)
    instance HasOptions m => HasOptions (MaybeT m)
    instance HasOptions m => HasOptions (ReaderT r m)
    instance HasOptions m => HasOptions (StateT s m)
    instance (HasOptions m, Monoid w) => HasOptions (WriterT w m)