    module Agda.TypeChecking.Monad.Debug
      ( module Agda.TypeChecking.Monad.Debug
      , Verbosity, VerboseKey, VerboseLevel
      ) where

    import qualified Control.Exception as E
    import qualified Control.DeepSeq as DeepSeq (force)

    import Control.Monad.IO.Class       ( MonadIO(..) )
    import Control.Monad.Except
    import Control.Monad.Reader
    import Control.Monad.State
    import Control.Monad.Trans.Control  ( MonadTransControl(..), liftThrough )
    import Control.Monad.Trans.Maybe
    import Control.Monad.Trans.Identity
    import Control.Monad.Writer

    import Data.Maybe

    import {-# SOURCE #-} Agda.TypeChecking.Errors
    import Agda.TypeChecking.Monad.Base

    import Agda.Interaction.Options
    import {-# SOURCE #-} Agda.Interaction.Response (Response(..))

    import Agda.Utils.CallStack ( HasCallStack, withCallerCallStack )
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.ListT
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Pretty
    import Agda.Utils.Update
    import qualified Agda.Utils.Trie as Trie

    import Agda.Utils.Impossible

    class (Functor m, Applicative m, Monad m) => MonadDebug m where

      formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> m String
      traceDebugMessage  :: VerboseKey -> VerboseLevel -> String -> m a -> m a

      -- | Print brackets around debug messages issued by a computation.
      verboseBracket     :: VerboseKey -> VerboseLevel -> String -> m a -> m a

      getVerbosity       :: m Verbosity

      -- | Check whether we are currently debug printing.
      isDebugPrinting    :: m Bool

      -- | Flag in a computation that we are currently debug printing.
      nowDebugPrinting   :: m a -> m a

      -- default implementation of transformed debug monad

      default formatDebugMessage
        :: (MonadTrans t, MonadDebug n, m ~ t n)
        => VerboseKey -> VerboseLevel -> TCM Doc -> m String
      formatDebugMessage VerboseKey
    k VerboseLevel
    n TCM Doc
    d = n VerboseKey -> t n VerboseKey
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n VerboseKey -> t n VerboseKey) -> n VerboseKey -> t n VerboseKey
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> VerboseLevel -> TCM Doc -> n VerboseKey
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
    formatDebugMessage VerboseKey
    k VerboseLevel
    n TCM Doc
    d

      default traceDebugMessage
        :: (MonadTransControl t, MonadDebug n, m ~ t n)
        => VerboseKey -> VerboseLevel -> String -> m a -> m a
      traceDebugMessage VerboseKey
    k VerboseLevel
    n VerboseKey
    s = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
    (MonadTransControl t, Monad (t m), Monad m) =>
    (m (StT t a) -> m (StT t b)) -> t m a -> t m b
    liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
    -> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    -> VerboseLevel -> VerboseKey -> n (StT t a) -> n (StT t a)
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    traceDebugMessage VerboseKey
    k VerboseLevel
    n VerboseKey
    s

      default verboseBracket
        :: (MonadTransControl t, MonadDebug n, m ~ t n)
        => VerboseKey -> VerboseLevel -> String -> m a -> m a
      verboseBracket VerboseKey
    k VerboseLevel
    n VerboseKey
    s = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
    (MonadTransControl t, Monad (t m), Monad m) =>
    (m (StT t a) -> m (StT t b)) -> t m a -> t m b
    liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
    -> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    -> VerboseLevel -> VerboseKey -> n (StT t a) -> n (StT t a)
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    verboseBracket VerboseKey
    k VerboseLevel
    n VerboseKey
    s

      default getVerbosity
        :: (MonadTrans t, MonadDebug n, m ~ t n)
        => m Verbosity
      getVerbosity = n Verbosity -> t n Verbosity
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift n Verbosity
    forall (m :: * -> *). MonadDebug m => m Verbosity
    getVerbosity

      default isDebugPrinting
        :: (MonadTrans t, MonadDebug n, m ~ t n)
        => m Bool
      isDebugPrinting = n Bool -> t n Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift n Bool
    forall (m :: * -> *). MonadDebug m => m Bool
    isDebugPrinting

      default nowDebugPrinting
        :: (MonadTransControl t, MonadDebug n, m ~ t n)
        => m a -> m a
      nowDebugPrinting = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
    (MonadTransControl t, Monad (t m), Monad m) =>
    (m (StT t a) -> m (StT t b)) -> t m a -> t m b
    liftThrough n (StT t a) -> n (StT t a)
    forall (m :: * -> *) a. MonadDebug m => m a -> m a
    nowDebugPrinting

    -- Default implementations (working around the restriction to only
    -- have one default signature).

    defaultGetVerbosity :: HasOptions m => m Verbosity
    defaultGetVerbosity :: forall (m :: * -> *). HasOptions m => m Verbosity
    defaultGetVerbosity = PragmaOptions -> Verbosity
    optVerbose (PragmaOptions -> Verbosity) -> m PragmaOptions -> m Verbosity
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

    defaultIsDebugPrinting :: MonadTCEnv m => m Bool
    defaultIsDebugPrinting :: forall (m :: * -> *). MonadTCEnv m => m Bool
    defaultIsDebugPrinting = (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envIsDebugPrinting

    defaultNowDebugPrinting :: MonadTCEnv m => m a -> m a
    defaultNowDebugPrinting :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    defaultNowDebugPrinting = Lens' Bool TCEnv -> (Bool -> Bool) -> m a -> m a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' Bool TCEnv
    eIsDebugPrinting ((Bool -> Bool) -> m a -> m a) -> (Bool -> Bool) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True

    -- | Print a debug message if switched on.
    displayDebugMessage :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
    displayDebugMessage :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    displayDebugMessage VerboseKey
    k VerboseLevel
    n VerboseKey
    s = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    traceDebugMessage VerboseKey
    k VerboseLevel
    n VerboseKey
    s (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | During printing, catch internal errors of kind 'Impossible' and print them.
    catchAndPrintImpossible
      :: (CatchImpossible m, Monad m)
      => VerboseKey -> VerboseLevel -> m String -> m String
    catchAndPrintImpossible :: forall (m :: * -> *).
    (CatchImpossible m, Monad m) =>
    VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
    catchAndPrintImpossible VerboseKey
    k VerboseLevel
    n m VerboseKey
    m = (Impossible -> Maybe Impossible)
    -> m VerboseKey -> (Impossible -> m VerboseKey) -> m VerboseKey
    forall (m :: * -> *) b a.
    CatchImpossible m =>
    (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
    catchImpossibleJust Impossible -> Maybe Impossible
    catchMe m VerboseKey
    m ((Impossible -> m VerboseKey) -> m VerboseKey)
    -> (Impossible -> m VerboseKey) -> m VerboseKey
    forall a b. (a -> b) -> a -> b
    $ \ Impossible
    imposs -> do
      VerboseKey -> m VerboseKey
    forall (m :: * -> *) a. Monad m => a -> m a
    return (VerboseKey -> m VerboseKey) -> VerboseKey -> m VerboseKey
    forall a b. (a -> b) -> a -> b
    $ Doc -> VerboseKey
    render (Doc -> VerboseKey) -> Doc -> VerboseKey
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
        [ VerboseKey -> Doc
    text (VerboseKey -> Doc) -> VerboseKey -> Doc
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "Debug printing " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    k VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    ":" VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseLevel -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show VerboseLevel
    n VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    " failed due to exception:"
        , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (VerboseKey -> Doc) -> [VerboseKey] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (VerboseLevel -> Doc -> Doc
    nest VerboseLevel
    2 (Doc -> Doc) -> (VerboseKey -> Doc) -> VerboseKey -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VerboseKey -> Doc
    text) ([VerboseKey] -> [Doc]) -> [VerboseKey] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> [VerboseKey]
    lines (VerboseKey -> [VerboseKey]) -> VerboseKey -> [VerboseKey]
    forall a b. (a -> b) -> a -> b
    $ Impossible -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Impossible
    imposs
        ]
      where
      -- Exception filter: Catch only the 'Impossible' exception during debug printing.
      catchMe :: Impossible -> Maybe Impossible
      catchMe :: Impossible -> Maybe Impossible
    catchMe = (Impossible -> Bool) -> Impossible -> Maybe Impossible
    forall a. (a -> Bool) -> a -> Maybe a
    filterMaybe ((Impossible -> Bool) -> Impossible -> Maybe Impossible)
    -> (Impossible -> Bool) -> Impossible -> Maybe Impossible
    forall a b. (a -> b) -> a -> b
    $ \case
        Impossible{}            -> Bool
    True
        Unreachable{}           -> Bool
    False
        ImpMissingDefinitions{} -> Bool
    False

    instance MonadDebug TCM where

      traceDebugMessage :: forall a.
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
    traceDebugMessage VerboseKey
    k VerboseLevel
    n VerboseKey
    s TCM a
    cont = do
        -- Andreas, 2019-08-20, issue #4016:
        -- Force any lazy 'Impossible' exceptions to the surface and handle them.
        VerboseKey
    s  <- IO VerboseKey -> TCM VerboseKey
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO VerboseKey -> TCM VerboseKey)
    -> (VerboseKey -> IO VerboseKey) -> VerboseKey -> TCM VerboseKey
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VerboseKey -> VerboseLevel -> IO VerboseKey -> IO VerboseKey
    forall (m :: * -> *).
    (CatchImpossible m, Monad m) =>
    VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
    catchAndPrintImpossible VerboseKey
    k VerboseLevel
    n (IO VerboseKey -> IO VerboseKey)
    -> (VerboseKey -> IO VerboseKey) -> VerboseKey -> IO VerboseKey
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VerboseKey -> IO VerboseKey
    forall a. a -> IO a
    E.evaluate (VerboseKey -> IO VerboseKey)
    -> (VerboseKey -> VerboseKey) -> VerboseKey -> IO VerboseKey
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VerboseKey -> VerboseKey
    forall a. NFData a => a -> a
    DeepSeq.force (VerboseKey -> TCM VerboseKey) -> VerboseKey -> TCM VerboseKey
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    s
        InteractionOutputCallback
    cb <- (TCState -> InteractionOutputCallback)
    -> TCMT IO InteractionOutputCallback
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC ((TCState -> InteractionOutputCallback)
     -> TCMT IO InteractionOutputCallback)
    -> (TCState -> InteractionOutputCallback)
    -> TCMT IO InteractionOutputCallback
    forall a b. (a -> b) -> a -> b
    $ PersistentTCState -> InteractionOutputCallback
    stInteractionOutputCallback (PersistentTCState -> InteractionOutputCallback)
    -> (TCState -> PersistentTCState)
    -> TCState
    -> InteractionOutputCallback
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PersistentTCState
    stPersistentState
        InteractionOutputCallback
    cb (VerboseLevel -> VerboseKey -> Response
    Resp_RunningInfo VerboseLevel
    n VerboseKey
    s)
        TCM a
    cont

      formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM VerboseKey
    formatDebugMessage VerboseKey
    k VerboseLevel
    n TCM Doc
    d = VerboseKey -> VerboseLevel -> TCM VerboseKey -> TCM VerboseKey
    forall (m :: * -> *).
    (CatchImpossible m, Monad m) =>
    VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
    catchAndPrintImpossible VerboseKey
    k VerboseLevel
    n (TCM VerboseKey -> TCM VerboseKey)
    -> TCM VerboseKey -> TCM VerboseKey
    forall a b. (a -> b) -> a -> b
    $ do
        Doc -> VerboseKey
    render (Doc -> VerboseKey) -> TCM Doc -> TCM VerboseKey
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM Doc
    d TCM Doc -> (TCErr -> TCM Doc) -> TCM Doc
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    err -> do
          TCErr -> TCM VerboseKey
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm VerboseKey
    prettyError TCErr
    err TCM VerboseKey -> (VerboseKey -> Doc) -> TCM Doc
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ VerboseKey
    s -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
            [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (VerboseKey -> Doc) -> [VerboseKey] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map VerboseKey -> Doc
    text
              [ VerboseKey
    "Printing debug message"
              , VerboseKey
    k  VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    ":" VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseLevel -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show VerboseLevel
    n
              , VerboseKey
    "failed due to error:"
              ]
            , VerboseLevel -> Doc -> Doc
    nest VerboseLevel
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Doc
    text VerboseKey
    s
            ]

      verboseBracket :: forall a.
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
    verboseBracket VerboseKey
    k VerboseLevel
    n VerboseKey
    s = VerboseKey
    -> VerboseLevel
    -> (TCMT IO a -> TCMT IO a)
    -> TCMT IO a
    -> TCMT IO a
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
    applyWhenVerboseS VerboseKey
    k VerboseLevel
    n ((TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a)
    -> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \ TCMT IO a
    m -> do
        VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    openVerboseBracket VerboseKey
    k VerboseLevel
    n VerboseKey
    s
        (TCMT IO a
    m TCMT IO a -> TCMT IO () -> TCMT IO a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* VerboseKey -> VerboseLevel -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m ()
    closeVerboseBracket VerboseKey
    k VerboseLevel
    n) TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    e -> do
          VerboseKey -> VerboseLevel -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m ()
    closeVerboseBracketException VerboseKey
    k VerboseLevel
    n
          TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    e

      getVerbosity :: TCM Verbosity
    getVerbosity     = TCM Verbosity
    forall (m :: * -> *). HasOptions m => m Verbosity
    defaultGetVerbosity
      isDebugPrinting :: TCM Bool
    isDebugPrinting  = TCM Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    defaultIsDebugPrinting
      nowDebugPrinting :: forall a. TCM a -> TCM a
    nowDebugPrinting = TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    defaultNowDebugPrinting

    -- MonadTrans default instances

    deriving instance MonadDebug m => MonadDebug (BlockT m)  -- ghc <= 8.0, GeneralizedNewtypeDeriving
    instance MonadDebug m => MonadDebug (ChangeT m)
    instance MonadDebug m => MonadDebug (ExceptT e m)
    instance MonadDebug m => MonadDebug (MaybeT m)
    instance MonadDebug m => MonadDebug (ReaderT r m)
    instance MonadDebug m => MonadDebug (StateT s m)
    instance (MonadDebug m, Monoid w) => MonadDebug (WriterT w m)
    instance MonadDebug m => MonadDebug (IdentityT m)

    -- We are lacking MonadTransControl ListT

    instance MonadDebug m => MonadDebug (ListT m) where
      traceDebugMessage :: forall a.
    VerboseKey -> VerboseLevel -> VerboseKey -> ListT m a -> ListT m a
    traceDebugMessage VerboseKey
    k VerboseLevel
    n VerboseKey
    s = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall (m :: * -> *) (m' :: * -> *) a.
    (Monad m, Monad m') =>
    (forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
    liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
    -> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> VerboseLevel -> VerboseKey -> m a1 -> m a1
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    traceDebugMessage VerboseKey
    k VerboseLevel
    n VerboseKey
    s
      verboseBracket :: forall a.
    VerboseKey -> VerboseLevel -> VerboseKey -> ListT m a -> ListT m a
    verboseBracket    VerboseKey
    k VerboseLevel
    n VerboseKey
    s = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall (m :: * -> *) (m' :: * -> *) a.
    (Monad m, Monad m') =>
    (forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
    liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
    -> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> VerboseLevel -> VerboseKey -> m a1 -> m a1
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    verboseBracket VerboseKey
    k VerboseLevel
    n VerboseKey
    s
      nowDebugPrinting :: forall a. ListT m a -> ListT m a
    nowDebugPrinting        = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
    forall (m :: * -> *) (m' :: * -> *) a.
    (Monad m, Monad m') =>
    (forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
    liftListT forall a1. m a1 -> m a1
    forall (m :: * -> *) a. MonadDebug m => m a -> m a
    nowDebugPrinting

    -- | Debug print some lines if the verbosity level for the given
    --   'VerboseKey' is at least 'VerboseLevel'.
    --
    -- Note: In the presence of @OverloadedStrings@, just
    -- @@
    --   reportS key level "Literate string"
    -- @@
    -- gives an @Ambiguous type variable@ error in @GHC@.
    -- Use the legacy functions 'reportSLn' and 'reportSDoc' instead then.
    --
    class ReportS a where
      reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m ()

    instance ReportS (TCM Doc) where reportS :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    reportS = VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc
    instance ReportS String    where reportS :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportS = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn

    instance ReportS [TCM Doc] where reportS :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> [TCM Doc] -> m ()
    reportS VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc VerboseKey
    k VerboseLevel
    n (TCM Doc -> m ()) -> ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Doc] -> Doc) -> TCMT IO [Doc] -> TCM Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat (TCMT IO [Doc] -> TCM Doc)
    -> ([TCM Doc] -> TCMT IO [Doc]) -> [TCM Doc] -> TCM Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [TCM Doc] -> TCMT IO [Doc]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence
    instance ReportS [String]  where reportS :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> [VerboseKey] -> m ()
    reportS VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn  VerboseKey
    k VerboseLevel
    n (VerboseKey -> m ())
    -> ([VerboseKey] -> VerboseKey) -> [VerboseKey] -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [VerboseKey] -> VerboseKey
    unlines
    instance ReportS [Doc]     where reportS :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> [Doc] -> m ()
    reportS VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn  VerboseKey
    k VerboseLevel
    n (VerboseKey -> m ()) -> ([Doc] -> VerboseKey) -> [Doc] -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> VerboseKey
    render (Doc -> VerboseKey) -> ([Doc] -> Doc) -> [Doc] -> VerboseKey
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
    instance ReportS Doc       where reportS :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> Doc -> m ()
    reportS VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn  VerboseKey
    k VerboseLevel
    n (VerboseKey -> m ()) -> (Doc -> VerboseKey) -> Doc -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> VerboseKey
    render

    -- | Conditionally println debug string.
    {-# SPECIALIZE reportSLn :: VerboseKey -> VerboseLevel -> String -> TCM () #-}
    reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
    reportSLn :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn VerboseKey
    k VerboseLevel
    n VerboseKey
    s = VerboseKey -> VerboseLevel -> m () -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m () -> m ()
    verboseS VerboseKey
    k VerboseLevel
    n (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    displayDebugMessage VerboseKey
    k VerboseLevel
    n (VerboseKey -> m ()) -> VerboseKey -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    s VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    "\n"

    __IMPOSSIBLE_VERBOSE__ :: (HasCallStack, MonadDebug m) => String -> m a
    __IMPOSSIBLE_VERBOSE__ :: forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    VerboseKey -> m a
    __IMPOSSIBLE_VERBOSE__ VerboseKey
    s = do { VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn VerboseKey
    "impossible" VerboseLevel
    10 VerboseKey
    s ; Impossible -> m a
    forall a. Impossible -> a
    throwImpossible Impossible
    err }
      where
        -- Create the "Impossible" error using *our* caller as the call site.
        err :: Impossible
    err = (CallStack -> Impossible) -> Impossible
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> Impossible
    Impossible

    -- | Conditionally render debug 'Doc' and print it.
    {-# SPECIALIZE reportSDoc :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM () #-}
    reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc VerboseKey
    k VerboseLevel
    n TCM Doc
    d = VerboseKey -> VerboseLevel -> m () -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m () -> m ()
    verboseS VerboseKey
    k VerboseLevel
    n (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
      VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    displayDebugMessage VerboseKey
    k VerboseLevel
    n (VerboseKey -> m ())
    -> (VerboseKey -> VerboseKey) -> VerboseKey -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    "\n") (VerboseKey -> m ()) -> m VerboseKey -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
    formatDebugMessage VerboseKey
    k VerboseLevel
    n (Lens' Bool TCEnv -> (Bool -> Bool) -> TCM Doc -> TCM Doc
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' Bool TCEnv
    eIsDebugPrinting (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) TCM Doc
    d)

    -- | Debug print the result of a computation.
    reportResult :: MonadDebug m => VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
    reportResult :: forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
    reportResult VerboseKey
    k VerboseLevel
    n a -> TCM Doc
    debug m a
    action = do
      a
    x <- m a
    action
      a
    x a -> m () -> m a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc VerboseKey
    k VerboseLevel
    n (a -> TCM Doc
    debug a
    x)

    unlessDebugPrinting :: MonadDebug m => m () -> m ()
    unlessDebugPrinting :: forall (m :: * -> *). MonadDebug m => m () -> m ()
    unlessDebugPrinting = m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM m Bool
    forall (m :: * -> *). MonadDebug m => m Bool
    isDebugPrinting

    -- | Debug print some lines if the verbosity level for the given
    --   'VerboseKey' is at least 'VerboseLevel'.
    --
    -- Note: In the presence of @OverloadedStrings@, just
    -- @@
    --   traceS key level "Literate string"
    -- @@
    -- gives an @Ambiguous type variable@ error in @GHC@.
    -- Use the legacy functions 'traceSLn' and 'traceSDoc' instead then.
    --
    class TraceS a where
      traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m c -> m c

    instance TraceS (TCM Doc) where traceS :: forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
    traceS = VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
    forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
    traceSDoc
    instance TraceS String    where traceS :: forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
    traceS = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
    forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
    traceSLn

    instance TraceS [TCM Doc] where traceS :: forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c
    traceS VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
    forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
    traceSDoc VerboseKey
    k VerboseLevel
    n (TCM Doc -> m c -> m c)
    -> ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> m c -> m c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Doc] -> Doc) -> TCMT IO [Doc] -> TCM Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat (TCMT IO [Doc] -> TCM Doc)
    -> ([TCM Doc] -> TCMT IO [Doc]) -> [TCM Doc] -> TCM Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [TCM Doc] -> TCMT IO [Doc]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence
    instance TraceS [String]  where traceS :: forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> [VerboseKey] -> m c -> m c
    traceS VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
    forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
    traceSLn  VerboseKey
    k VerboseLevel
    n (VerboseKey -> m c -> m c)
    -> ([VerboseKey] -> VerboseKey) -> [VerboseKey] -> m c -> m c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [VerboseKey] -> VerboseKey
    unlines
    instance TraceS [Doc]     where traceS :: forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c
    traceS VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
    forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
    traceSLn  VerboseKey
    k VerboseLevel
    n (VerboseKey -> m c -> m c)
    -> ([Doc] -> VerboseKey) -> [Doc] -> m c -> m c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> VerboseKey
    render (Doc -> VerboseKey) -> ([Doc] -> Doc) -> [Doc] -> VerboseKey
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
    instance TraceS Doc       where traceS :: forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> Doc -> m c -> m c
    traceS VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
    forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
    traceSLn  VerboseKey
    k VerboseLevel
    n (VerboseKey -> m c -> m c)
    -> (Doc -> VerboseKey) -> Doc -> m c -> m c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> VerboseKey
    render

    traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
    traceSLn :: forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
    traceSLn VerboseKey
    k VerboseLevel
    n VerboseKey
    s = VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
    applyWhenVerboseS VerboseKey
    k VerboseLevel
    n ((m a -> m a) -> m a -> m a) -> (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    traceDebugMessage VerboseKey
    k VerboseLevel
    n (VerboseKey -> m a -> m a) -> VerboseKey -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    s VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    "\n"

    -- | Conditionally render debug 'Doc', print it, and then continue.
    traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
    traceSDoc :: forall (m :: * -> *) c.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
    traceSDoc VerboseKey
    k VerboseLevel
    n TCM Doc
    d = VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
    applyWhenVerboseS VerboseKey
    k VerboseLevel
    n ((m a -> m a) -> m a -> m a) -> (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \m a
    cont -> do
      VerboseKey
    s <- VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
    formatDebugMessage VerboseKey
    k VerboseLevel
    n (TCM Doc -> m VerboseKey) -> TCM Doc -> m VerboseKey
    forall a b. (a -> b) -> a -> b
    $ Lens' Bool TCEnv -> (Bool -> Bool) -> TCM Doc -> TCM Doc
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' Bool TCEnv
    eIsDebugPrinting (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) TCM Doc
    d
      VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    traceDebugMessage VerboseKey
    k VerboseLevel
    n (VerboseKey
    s VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    "\n") m a
    cont

    openVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
    openVerboseBracket :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    openVerboseBracket VerboseKey
    k VerboseLevel
    n VerboseKey
    s = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    displayDebugMessage VerboseKey
    k VerboseLevel
    n (VerboseKey -> m ()) -> VerboseKey -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "{ " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    s VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    "\n"

    closeVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
    closeVerboseBracket :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m ()
    closeVerboseBracket VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    displayDebugMessage VerboseKey
    k VerboseLevel
    n VerboseKey
    "}\n"

    closeVerboseBracketException :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
    closeVerboseBracketException :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m ()
    closeVerboseBracketException VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    displayDebugMessage VerboseKey
    k VerboseLevel
    n VerboseKey
    "} (exception)\n"

    ------------------------------------------------------------------------
    -- Verbosity

    -- Invariant (which we may or may not currently break): Debug
    -- printouts use one of the following functions:
    --
    --   reportS
    --   reportSLn
    --   reportSDoc

    parseVerboseKey :: VerboseKey -> [String]
    parseVerboseKey :: VerboseKey -> [VerboseKey]
    parseVerboseKey = (Char -> Bool) -> VerboseKey -> [VerboseKey]
    forall a. (a -> Bool) -> [a] -> [[a]]
    wordsBy (Char -> VerboseKey -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` (VerboseKey
    ".:" :: String))

    -- | Check whether a certain verbosity level is activated.
    --
    --   Precondition: The level must be non-negative.
    {-# SPECIALIZE hasVerbosity :: VerboseKey -> VerboseLevel -> TCM Bool #-}
    hasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
    hasVerbosity :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m Bool
    hasVerbosity VerboseKey
    k VerboseLevel
    n | VerboseLevel
    n VerboseLevel -> VerboseLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    < VerboseLevel
    0     = m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                     | Bool
    otherwise = do
        Verbosity
    t <- m Verbosity
    forall (m :: * -> *). MonadDebug m => m Verbosity
    getVerbosity
        let ks :: [VerboseKey]
    ks = VerboseKey -> [VerboseKey]
    parseVerboseKey VerboseKey
    k
            m :: VerboseLevel
    m  = VerboseLevel -> [VerboseLevel] -> VerboseLevel
    forall a. a -> [a] -> a
    lastWithDefault VerboseLevel
    0 ([VerboseLevel] -> VerboseLevel) -> [VerboseLevel] -> VerboseLevel
    forall a b. (a -> b) -> a -> b
    $ [VerboseKey] -> Verbosity -> [VerboseLevel]
    forall k v. Ord k => [k] -> Trie k v -> [v]
    Trie.lookupPath [VerboseKey]
    ks Verbosity
    t
        Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (VerboseLevel
    n VerboseLevel -> VerboseLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    <= VerboseLevel
    m)

    -- | Check whether a certain verbosity level is activated (exact match).

    {-# SPECIALIZE hasExactVerbosity :: VerboseKey -> VerboseLevel -> TCM Bool #-}
    hasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
    hasExactVerbosity :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m Bool
    hasExactVerbosity VerboseKey
    k VerboseLevel
    n =
      (VerboseLevel -> Maybe VerboseLevel
    forall a. a -> Maybe a
    Just VerboseLevel
    n Maybe VerboseLevel -> Maybe VerboseLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe VerboseLevel -> Bool)
    -> (Verbosity -> Maybe VerboseLevel) -> Verbosity -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [VerboseKey] -> Verbosity -> Maybe VerboseLevel
    forall k v. Ord k => [k] -> Trie k v -> Maybe v
    Trie.lookup (VerboseKey -> [VerboseKey]
    parseVerboseKey VerboseKey
    k) (Verbosity -> Bool) -> m Verbosity -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Verbosity
    forall (m :: * -> *). MonadDebug m => m Verbosity
    getVerbosity

    -- | Run a computation if a certain verbosity level is activated (exact match).

    {-# SPECIALIZE whenExactVerbosity :: VerboseKey -> VerboseLevel -> TCM () -> TCM () #-}
    whenExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
    whenExactVerbosity :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m () -> m ()
    whenExactVerbosity VerboseKey
    k VerboseLevel
    n = m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (m Bool -> m () -> m ()) -> m Bool -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> VerboseLevel -> m Bool
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m Bool
    hasExactVerbosity VerboseKey
    k VerboseLevel
    n

    __CRASH_WHEN__ :: (HasCallStack, MonadTCM m, MonadDebug m) => VerboseKey -> VerboseLevel -> m ()
    __CRASH_WHEN__ :: forall (m :: * -> *).
    (HasCallStack, MonadTCM m, MonadDebug m) =>
    VerboseKey -> VerboseLevel -> m ()
    __CRASH_WHEN__ VerboseKey
    k VerboseLevel
    n = VerboseKey -> VerboseLevel -> m () -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m () -> m ()
    whenExactVerbosity VerboseKey
    k VerboseLevel
    n (Impossible -> m ()
    forall a. Impossible -> a
    throwImpossible Impossible
    err)
      where
        -- Create the "Unreachable" error using *our* caller as the call site.
        err :: Impossible
    err = (CallStack -> Impossible) -> Impossible
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> Impossible
    Unreachable

    -- | Run a computation if a certain verbosity level is activated.
    --
    --   Precondition: The level must be non-negative.
    {-# SPECIALIZE verboseS :: VerboseKey -> VerboseLevel -> TCM () -> TCM () #-}
    -- {-# SPECIALIZE verboseS :: MonadIO m => VerboseKey -> VerboseLevel -> TCMT m () -> TCMT m () #-} -- RULE left-hand side too complicated to desugar
    -- {-# SPECIALIZE verboseS :: MonadTCM tcm => VerboseKey -> VerboseLevel -> tcm () -> tcm () #-}
    verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
    verboseS :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m () -> m ()
    verboseS VerboseKey
    k VerboseLevel
    n m ()
    action = m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (VerboseKey -> VerboseLevel -> m Bool
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m Bool
    hasVerbosity VerboseKey
    k VerboseLevel
    n) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ m () -> m ()
    forall (m :: * -> *) a. MonadDebug m => m a -> m a
    nowDebugPrinting m ()
    action

    -- | Apply a function if a certain verbosity level is activated.
    --
    --   Precondition: The level must be non-negative.
    applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
    applyWhenVerboseS :: forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
    applyWhenVerboseS VerboseKey
    k VerboseLevel
    n m a -> m a
    f m a
    a = m Bool -> m a -> m a -> m a
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (VerboseKey -> VerboseLevel -> m Bool
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> m Bool
    hasVerbosity VerboseKey
    k VerboseLevel
    n) (m a -> m a
    f m a
    a) m a
    a

    -- | Verbosity lens.
    verbosity :: VerboseKey -> Lens' VerboseLevel TCState
    verbosity :: VerboseKey -> Lens' VerboseLevel TCState
    verbosity VerboseKey
    k = (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    Lens' PragmaOptions TCState
    stPragmaOptions ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState)
    -> ((VerboseLevel -> f VerboseLevel)
        -> PragmaOptions -> f PragmaOptions)
    -> (VerboseLevel -> f VerboseLevel)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Verbosity -> f Verbosity) -> PragmaOptions -> f PragmaOptions
    Lens' Verbosity PragmaOptions
    verbOpt ((Verbosity -> f Verbosity) -> PragmaOptions -> f PragmaOptions)
    -> ((VerboseLevel -> f VerboseLevel) -> Verbosity -> f Verbosity)
    -> (VerboseLevel -> f VerboseLevel)
    -> PragmaOptions
    -> f PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [VerboseKey] -> Lens' (Maybe VerboseLevel) Verbosity
    forall k v. Ord k => [k] -> Lens' (Maybe v) (Trie k v)
    Trie.valueAt (VerboseKey -> [VerboseKey]
    parseVerboseKey VerboseKey
    k) ((Maybe VerboseLevel -> f (Maybe VerboseLevel))
     -> Verbosity -> f Verbosity)
    -> ((VerboseLevel -> f VerboseLevel)
        -> Maybe VerboseLevel -> f (Maybe VerboseLevel))
    -> (VerboseLevel -> f VerboseLevel)
    -> Verbosity
    -> f Verbosity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VerboseLevel -> Lens' VerboseLevel (Maybe VerboseLevel)
    forall a. Eq a => a -> Lens' a (Maybe a)
    defaultTo VerboseLevel
    0
      where
        verbOpt :: Lens' Verbosity PragmaOptions
        verbOpt :: Lens' Verbosity PragmaOptions
    verbOpt Verbosity -> f Verbosity
    f PragmaOptions
    opts = Verbosity -> f Verbosity
    f (PragmaOptions -> Verbosity
    optVerbose PragmaOptions
    opts) f Verbosity -> (Verbosity -> PragmaOptions) -> f PragmaOptions
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Verbosity
    v -> PragmaOptions
    opts { optVerbose :: Verbosity
    optVerbose = Verbosity
    v }
        -- Andreas, 2019-08-20: this lens should go into Interaction.Option.Lenses!

        defaultTo :: Eq a => a -> Lens' a (Maybe a)
        defaultTo :: forall a. Eq a => a -> Lens' a (Maybe a)
    defaultTo a
    x a -> f a
    f Maybe a
    m = (a -> Bool) -> a -> Maybe a
    forall a. (a -> Bool) -> a -> Maybe a
    filterMaybe (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    x) (a -> Maybe a) -> f a -> f (Maybe a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> f a
    f (a -> Maybe a -> a
    forall a. a -> Maybe a -> a
    fromMaybe a
    x Maybe a
    m)