    {-# LANGUAGE CPP #-}

    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.Applicative          ( liftA2 )
    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 Data.Time                    ( getCurrentTime, getCurrentTimeZone, utcToLocalTime )
    import Data.Time.Format.ISO8601     ( iso8601Show )

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

    import Agda.Interaction.Options
    import Agda.Interaction.Response.Base (Response_boot(..))

    import Agda.Utils.CallStack ( HasCallStack, withCallerCallStack )
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.ListT
    import Agda.Utils.Maybe
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Monad
    import Agda.Syntax.Common.Pretty
    import Agda.Utils.ProfileOptions
    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
      getProfileOptions  :: m ProfileOptions

      -- | 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 (m :: * -> *) a. Monad m => m a -> t m a
    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 a. VerboseKey -> VerboseLevel -> VerboseKey -> n a -> n a
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    traceDebugMessage VerboseKey
    k VerboseLevel
    n VerboseKey
    s

    #ifdef DEBUG
      default verboseBracket
        :: (MonadTransControl t, MonadDebug n, m ~ t n)
        => VerboseKey -> VerboseLevel -> String -> m a -> m a
      verboseBracket k n s = liftThrough $ verboseBracket k n s
    #else
      default verboseBracket
        :: (MonadTransControl t, MonadDebug n, m ~ t n)
        => VerboseKey -> VerboseLevel -> String -> m a -> m a
      verboseBracket VerboseKey
    k VerboseLevel
    n VerboseKey
    s m a
    ma = m a
    ma
      {-# INLINE verboseBracket #-}
    #endif

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

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

      default isDebugPrinting
        :: (MonadTrans t, MonadDebug n, m ~ t n)
        => m Bool
      isDebugPrinting = n Bool -> t n Bool
    forall (m :: * -> *) a. Monad m => m a -> t m a
    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 a. n a -> n 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

    defaultGetProfileOptions :: HasOptions m => m ProfileOptions
    defaultGetProfileOptions :: forall (m :: * -> *). HasOptions m => m ProfileOptions
    defaultGetProfileOptions = PragmaOptions -> ProfileOptions
    optProfiling (PragmaOptions -> ProfileOptions)
    -> m PragmaOptions -> m ProfileOptions
    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' TCEnv Bool -> (Bool -> Bool) -> m a -> m a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    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 a. 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 (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ () -> m ()
    forall a. a -> m a
    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 b a. (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (VerboseKey -> m VerboseKey) -> VerboseKey -> m VerboseKey
    forall a b. (a -> b) -> a -> b
    $ Doc -> VerboseKey
    forall a. Doc a -> 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
    forall a. VerboseKey -> Doc a
    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
    forall a. VerboseLevel -> Doc a -> Doc a
    nest VerboseLevel
    2 (Doc -> Doc) -> (VerboseKey -> Doc) -> VerboseKey -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VerboseKey -> Doc
    forall a. VerboseKey -> Doc a
    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.
        s  <- IO VerboseKey -> TCM VerboseKey
    forall a. IO a -> TCMT IO a
    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
        cb <- getsTC $ stInteractionOutputCallback . stPersistentState

        -- Andreas, 2022-06-15, prefix with time stamp if `-v debug.time:100`:
        msg <- ifNotM (hasVerbosity "debug.time" 100) {-then-} (return s) {-else-} $ do
          now <- liftIO $ trailingZeros . iso8601Show <$> liftA2 utcToLocalTime getCurrentTimeZone getCurrentTime
          return $ concat [ now, ": ", s ]

        cb $ Resp_RunningInfo n msg
        cont
        where
        -- Surprisingly, iso8601Show gives us _up to_ 6 fractional digits (microseconds),
        -- but not exactly 6.  https://github.com/haskell/time/issues/211
        -- So we need to do the padding ourselves.
        -- yyyy-mm-ddThh:mm:ss.ssssss
        -- 12345678901234567890123456
        trailingZeros :: VerboseKey -> VerboseKey
    trailingZeros = VerboseLevel -> VerboseKey -> VerboseKey
    forall a. VerboseLevel -> [a] -> [a]
    take VerboseLevel
    26 (VerboseKey -> VerboseKey)
    -> (VerboseKey -> VerboseKey) -> VerboseKey -> VerboseKey
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Char -> VerboseKey
    forall a. a -> [a]
    repeat Char
    '0')

      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
    forall a. Doc a -> 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 a. 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
    err -> do
          TCErr -> TCM VerboseKey
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm VerboseKey
    renderError TCErr
    err TCM VerboseKey -> (VerboseKey -> Doc) -> TCM Doc
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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
    forall a. VerboseKey -> Doc a
    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
    forall a. VerboseLevel -> Doc a -> Doc a
    nest VerboseLevel
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Doc
    forall a. VerboseKey -> Doc a
    text VerboseKey
    s
            ]

    #ifdef DEBUG
      verboseBracket k n s = applyWhenVerboseS k n $ \ m -> do
        openVerboseBracket k n s
        (m <* closeVerboseBracket k n) `catchError` \ e -> do
          closeVerboseBracketException k n
          throwError e
    #else
      verboseBracket :: forall a.
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
    verboseBracket VerboseKey
    k VerboseLevel
    n VerboseKey
    s TCM a
    ma = TCM a
    ma
      {-# INLINE verboseBracket #-}
    #endif

      getVerbosity :: TCM Verbosity
    getVerbosity      = TCM Verbosity
    forall (m :: * -> *). HasOptions m => m Verbosity
    defaultGetVerbosity
      getProfileOptions :: TCM ProfileOptions
    getProfileOptions = TCM ProfileOptions
    forall (m :: * -> *). HasOptions m => m ProfileOptions
    defaultGetProfileOptions
      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 a. 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
      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 a. VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    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 m a1 -> m a1
    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 a b. (a -> b) -> TCMT IO a -> TCMT IO b
    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)
    forall (m :: * -> *) a. Monad m => [m a] -> m [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
    forall a. Doc a -> 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
    forall a. Doc a -> VerboseKey
    render

    #ifdef DEBUG

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

    #else

    {-# INLINE reportSLn #-}
    reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
    reportSLn :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn VerboseKey
    _ VerboseLevel
    _ VerboseKey
    _ = () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

    #endif

    -- | Conditionally println debug string. Works regardless of the debug flag.
    {-# SPECIALIZE reportSLn :: VerboseKey -> VerboseLevel -> String -> TCM () #-}
    alwaysReportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
    alwaysReportSLn :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    alwaysReportSLn 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
      -- Andreas, 2023-07-19, issue #6728 is fixed by manually inlining reportSLn here.
      -- reportSLn "impossible" 10 s
      -- It seems like GHC 9.6 optimization does otherwise something that throws
      -- away the debug message.
      let k :: VerboseKey
    k = VerboseKey
    "impossible"
      let n :: VerboseLevel
    n = VerboseLevel
    10
      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 -> 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

    #ifdef DEBUG

    -- | Conditionally render debug 'Doc' and print it.
    {-# SPECIALIZE reportSDoc :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM () #-}
    reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc k n d = verboseS k n $ do
      displayDebugMessage k n . (++ "\n") =<< formatDebugMessage k n (locallyTC eIsDebugPrinting (const True) d)

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

    #else

    -- | Conditionally render debug 'Doc' and print it.
    {-# INLINE reportSDoc #-}
    reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc VerboseKey
    _ VerboseLevel
    _ TCM Doc
    _ = () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

    -- | Debug print the result of a computation.
    {-# INLINE reportResult #-}
    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
    _ VerboseLevel
    _ a -> TCM Doc
    _ m a
    action = m a
    action

    #endif

    -- | Conditionally render debug 'Doc' and print it. Works regardless of the debug flag.
    {-# SPECIALIZE reportSDoc :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM () #-}
    alwaysReportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    alwaysReportSDoc :: forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
    alwaysReportSDoc 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' TCEnv Bool -> (Bool -> Bool) -> TCM Doc -> TCM Doc
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eIsDebugPrinting (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) TCM Doc
    d)

    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 a b. (a -> b) -> TCMT IO a -> TCMT IO b
    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)
    forall (m :: * -> *) a. Monad m => [m a] -> m [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
    forall a. Doc a -> 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
    forall a. Doc a -> VerboseKey
    render

    #ifdef DEBUG

    traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
    traceSLn k n s = applyWhenVerboseS k n $ traceDebugMessage k n $ s ++ "\n"

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

    #else

    {-# INLINE traceSLn #-}
    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
    _ VerboseLevel
    _ VerboseKey
    _ m a
    action = m a
    action

    -- | Conditionally render debug 'Doc', print it, and then continue.
    {-# INLINE traceSDoc #-}
    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
    _ VerboseLevel
    _ TCM Doc
    _ m a
    action = m a
    action

    #endif

    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

    -- | 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 = do
      t <- m Verbosity
    forall (m :: * -> *). MonadDebug m => m Verbosity
    getVerbosity
      return $ case t of
        Verbosity
    Strict.Nothing -> VerboseLevel
    n VerboseLevel -> VerboseLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    <= VerboseLevel
    1
        Strict.Just Trie VerboseKeyItem VerboseLevel
    t
          -- This code is not executed if no debug flags have been given.
          | Trie VerboseKeyItem VerboseLevel
    t Trie VerboseKeyItem VerboseLevel
    -> Trie VerboseKeyItem VerboseLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == [VerboseKeyItem]
    -> VerboseLevel -> Trie VerboseKeyItem VerboseLevel
    forall k v. [k] -> v -> Trie k v
    Trie.singleton [] VerboseLevel
    0 ->
            -- A special case for "-v0".
            VerboseLevel
    n VerboseLevel -> VerboseLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    <= VerboseLevel
    0
          | Bool
    otherwise ->
            let ks :: [VerboseKeyItem]
    ks = VerboseKey -> [VerboseKeyItem]
    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
    $ [VerboseKeyItem]
    -> Trie VerboseKeyItem VerboseLevel -> [VerboseLevel]
    forall k v. Ord k => [k] -> Trie k v -> [v]
    Trie.lookupPath [VerboseKeyItem]
    ks Trie VerboseKeyItem VerboseLevel
    t
            in 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 = do
      t <- m Verbosity
    forall (m :: * -> *). MonadDebug m => m Verbosity
    getVerbosity
      return $ case t of
        Verbosity
    Strict.Nothing -> VerboseLevel
    n VerboseLevel -> VerboseLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == VerboseLevel
    1
        Strict.Just Trie VerboseKeyItem VerboseLevel
    t
          -- This code is not executed if no debug flags have been given.
          | Trie VerboseKeyItem VerboseLevel
    t Trie VerboseKeyItem VerboseLevel
    -> Trie VerboseKeyItem VerboseLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == [VerboseKeyItem]
    -> VerboseLevel -> Trie VerboseKeyItem VerboseLevel
    forall k v. [k] -> v -> Trie k v
    Trie.singleton [] VerboseLevel
    0 ->
            -- A special case for "-v0".
            VerboseLevel
    n VerboseLevel -> VerboseLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == VerboseLevel
    0
          | Bool
    otherwise ->
            VerboseLevel -> Maybe VerboseLevel
    forall a. a -> Maybe a
    Just VerboseLevel
    n Maybe VerboseLevel -> Maybe VerboseLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == [VerboseKeyItem]
    -> Trie VerboseKeyItem VerboseLevel -> Maybe VerboseLevel
    forall k v. Ord k => [k] -> Trie k v -> Maybe v
    Trie.lookup (VerboseKey -> [VerboseKeyItem]
    parseVerboseKey VerboseKey
    k) Trie VerboseKeyItem VerboseLevel
    t

    -- | 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 a. m a -> m a
    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

    -- | Check whether a certain profile option is activated.
    {-# SPECIALIZE hasProfileOption :: ProfileOption -> TCM Bool #-}
    hasProfileOption :: MonadDebug m => ProfileOption -> m Bool
    hasProfileOption :: forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
    hasProfileOption ProfileOption
    opt = ProfileOption -> ProfileOptions -> Bool
    containsProfileOption ProfileOption
    opt (ProfileOptions -> Bool) -> m ProfileOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m ProfileOptions
    forall (m :: * -> *). MonadDebug m => m ProfileOptions
    getProfileOptions

    -- | Run some code when the given profiling option is active.
    whenProfile :: MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile :: forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    opt = m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (ProfileOption -> m Bool
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
    hasProfileOption ProfileOption
    opt)