    module Agda.TypeChecking.Warnings
      ( MonadWarning(..)
      , warning'_, warning_, warning', warning, warnings
      , raiseWarningsOnUsage
      , isUnsolvedWarning
      , isMetaWarning
      , isMetaTCWarning
      , onlyShowIfUnsolved
      , WhichWarnings(..), classifyWarning
      -- not exporting constructor of WarningsAndNonFatalErrors
      , WarningsAndNonFatalErrors, tcWarnings, nonFatalErrors
      , classifyWarnings
      ) where

    import Control.Monad ( forM, unless, when )
    import Control.Monad.Except ( MonadError(..) )
    import Control.Monad.Reader ( ReaderT )
    import Control.Monad.State  ( StateT )
    import Control.Monad.Trans  ( MonadTrans, lift )
    import Control.Monad.Trans.Maybe
    import Control.Monad.Writer ( WriterT )

    import Data.Foldable
    import qualified Data.List as List
    import qualified Data.Map  as Map
    import qualified Data.Set  as Set
    import Data.Maybe     ( catMaybes )
    import Data.Semigroup ( Semigroup, (<>) )

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Monad.Caching
    import {-# SOURCE #-} Agda.TypeChecking.Pretty ( MonadPretty, prettyTCM, vcat, ($$) )
    import {-# SOURCE #-} Agda.TypeChecking.Pretty.Call
    import {-# SOURCE #-} Agda.TypeChecking.Pretty.Warning ( prettyWarning )

    import Agda.Syntax.Abstract.Name ( QName )
    import qualified Agda.Syntax.Common.Pretty as P
    import Agda.Syntax.Position
    import Agda.Syntax.Parser

    import Agda.Interaction.Options
    import Agda.Interaction.Options.Warnings
    import {-# SOURCE #-} Agda.Interaction.Highlighting.Generate (highlightWarning)

    import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
    import Agda.Utils.Function  ( applyUnless )
    import Agda.Utils.Lens
    import Agda.Utils.List1 (List1)
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import qualified Agda.Utils.Set1 as Set1
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    -- * The warning monad
    ---------------------------------------------------------------------------

    class (MonadPretty m, MonadError TCErr m) => MonadWarning m where
      -- | Store a warning and generate highlighting from it.
      addWarning ::
           Bool       -- ^ Is the warning enabled?
        -> TCWarning  -- ^ The warning.
        -> m ()

      default addWarning
        :: (MonadWarning n, MonadTrans t, t n ~ m)
        => Bool -> TCWarning -> m ()
      addWarning Bool
    enabled = n () -> m ()
    n () -> t n ()
    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 () -> m ()) -> (TCWarning -> n ()) -> TCWarning -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> TCWarning -> n ()
    forall (m :: * -> *). MonadWarning m => Bool -> TCWarning -> m ()
    addWarning Bool
    enabled

    -- instance MonadWarning m => MonadWarning (ExceptT e m)  -- Conflict with MonadError TCErr constraint
    instance MonadWarning m => MonadWarning (MaybeT m)
    instance MonadWarning m => MonadWarning (ReaderT r m)
    instance MonadWarning m => MonadWarning (StateT s m)
    instance (MonadWarning m, Monoid w) => MonadWarning (WriterT w m)

    instance MonadWarning TCM where
      addWarning :: Bool -> TCWarning -> TCM ()
    addWarning Bool
    enabled TCWarning
    tcwarn = do
        (Set TCWarning -> f (Set TCWarning)) -> TCState -> f TCState
    Lens' TCState (Set TCWarning)
    stTCWarnings Lens' TCState (Set TCWarning)
    -> (Set TCWarning -> Set TCWarning) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` TCWarning -> Set TCWarning -> Set TCWarning
    forall a. Ord a => a -> Set a -> Set a
    Set.insert TCWarning
    tcwarn
        -- Andreas, 2025-04-01, issue #6994, no highlighting for disabled warnings
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    enabled (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCWarning -> TCM ()
    highlightWarning TCWarning
    tcwarn

    -- * Raising warnings
    ---------------------------------------------------------------------------

    {-# SPECIALIZE warning'_ :: CallStack -> Warning -> TCM TCWarning #-}
    warning'_ :: (MonadWarning m) => CallStack -> Warning -> m TCWarning
    warning'_ :: forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m TCWarning
    warning'_ CallStack
    loc Warning
    w = do
      r <- Lens' TCEnv Range -> m Range
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Range -> f Range) -> TCEnv -> f TCEnv
    Lens' TCEnv Range
    eRange
      c <- viewTC eCall
      b <- areWeCaching
      let r' = case Warning
    w of
            -- Some warnings come with their own error locations.
            NicifierIssue             DeclarationWarning
    w0 -> DeclarationWarning -> Range
    forall a. HasRange a => a -> Range
    getRange DeclarationWarning
    w0
            UnsolvedInteractionMetas  Set1 Range
    rs -> Set1 Range -> Range
    forall a. HasRange a => a -> Range
    getRange Set1 Range
    rs
            UnsolvedMetaVariables     Set1 Range
    rs -> Set1 Range -> Range
    forall a. HasRange a => a -> Range
    getRange Set1 Range
    rs
            UnsolvedConstraints       List1 ProblemConstraint
    cs -> List1 ProblemConstraint -> Range
    forall a. HasRange a => a -> Range
    getRange List1 ProblemConstraint
    cs
            InteractionMetaBoundaries Set1 Range
    rs -> Set1 Range -> Range
    forall a. HasRange a => a -> Range
    getRange Set1 Range
    rs
            Warning
    _ -> Range
    r
      let wn = Warning -> WarningName
    warningName Warning
    w
      let ws = WarningName -> [Char]
    warningName2String WarningName
    wn
      p <- vcat
        [ pure $ P.hsep
          [ if null r' then mempty else P.pretty r' P.<> P.colon
          , if wn `elem` errorWarnings then "error:" P.<+> P.brackets (P.text ws)
            else P.text $ "warning: -W[no]" ++ ws
            -- Only benign warnings can be deactivated with -WnoXXX.
          ]
        , prettyWarning w
        , prettyTCM c
        ]
      return $ TCWarning loc r' w p (P.render p) b

    {-# SPECIALIZE warning_ :: Warning -> TCM TCWarning #-}
    warning_ :: (HasCallStack, MonadWarning m) => Warning -> m TCWarning
    warning_ :: forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m TCWarning
    warning_ = (CallStack -> m TCWarning) -> m TCWarning
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack ((CallStack -> m TCWarning) -> m TCWarning)
    -> (Warning -> CallStack -> m TCWarning) -> Warning -> m TCWarning
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (CallStack -> Warning -> m TCWarning)
    -> Warning -> CallStack -> m TCWarning
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip CallStack -> Warning -> m TCWarning
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m TCWarning
    warning'_

    -- UNUSED Liang-Ting Chen 2019-07-16
    ---- | @applyWarningMode@ filters out the warnings the user has not requested
    ---- Users are not allowed to ignore non-fatal errors.
    --
    --applyWarningMode :: WarningMode -> Warning -> Maybe Warning
    --applyWarningMode wm w = case classifyWarning w of
    --  ErrorWarnings -> Just w
    --  AllWarnings   -> w <$ guard (Set.member (warningName w) $ wm ^. warningSet)

    {-# SPECIALIZE warnings' :: CallStack -> List1 Warning -> TCM () #-}
    warnings' :: MonadWarning m => CallStack -> List1 Warning -> m ()
    warnings' :: forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> List1 Warning -> m ()
    warnings' CallStack
    loc List1 Warning
    ws = do

      WarningMode enabledWarnings wError <- PragmaOptions -> WarningMode
    optWarningMode (PragmaOptions -> WarningMode) -> m PragmaOptions -> m WarningMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

      -- We collect *all* of the warnings no matter whether they are enabled or not.
      -- If we find an enabled warning which should be turned into an error, we keep processing
      -- the rest of the warnings and *then* report all of the errors at once.
      merrs <- forM ws $ \ Warning
    w' -> do
        let wn :: WarningName
    wn = Warning -> WarningName
    warningName Warning
    w'
        let enabled :: Bool
    enabled = WarningName
    wn WarningName -> Set WarningName -> Bool
    forall a. Eq a => a -> Set a -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` Set WarningName
    enabledWarnings
        tcwarn <- CallStack -> Warning -> m TCWarning
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m TCWarning
    warning'_ CallStack
    loc Warning
    w'
        if wError && enabled
        then pure (Just tcwarn)
        else Nothing <$ addWarning (enabled  || wn `elem` exactSplitWarnings) tcwarn
          -- Andreas, 2025-04-01, issue #6994: always highlight non-exact splits

      List1.unlessNull (List1.catMaybes merrs) \ List1 TCWarning
    errs ->
        CallStack -> TypeError -> m ()
    forall (m :: * -> *) a.
    MonadTCError m =>
    CallStack -> TypeError -> m a
    typeError' CallStack
    loc (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ Set1 TCWarning -> TypeError
    NonFatalErrors (Set1 TCWarning -> TypeError) -> Set1 TCWarning -> TypeError
    forall a b. (a -> b) -> a -> b
    $ List1 TCWarning -> Set1 TCWarning
    forall a. Ord a => NonEmpty a -> NESet a
    Set1.fromList List1 TCWarning
    errs

    {-# SPECIALIZE warnings :: HasCallStack => List1 Warning -> TCM () #-}
    warnings :: (HasCallStack, MonadWarning m) => List1 Warning -> m ()
    warnings :: forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    List1 Warning -> m ()
    warnings = (CallStack -> m ()) -> m ()
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack ((CallStack -> m ()) -> m ())
    -> (List1 Warning -> CallStack -> m ()) -> List1 Warning -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (CallStack -> List1 Warning -> m ())
    -> List1 Warning -> CallStack -> m ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip CallStack -> List1 Warning -> m ()
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> List1 Warning -> m ()
    warnings'

    {-# SPECIALIZE warning' :: CallStack -> Warning -> TCM () #-}
    warning' :: MonadWarning m => CallStack -> Warning -> m ()
    warning' :: forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m ()
    warning' CallStack
    loc = CallStack -> List1 Warning -> m ()
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> List1 Warning -> m ()
    warnings' CallStack
    loc (List1 Warning -> m ())
    -> (Warning -> List1 Warning) -> Warning -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Warning -> List1 Warning
    forall el coll. Singleton el coll => el -> coll
    singleton

    {-# SPECIALIZE warning :: HasCallStack => Warning -> TCM () #-}
    warning :: (HasCallStack, MonadWarning m) => Warning -> m ()
    warning :: forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning = (CallStack -> m ()) -> m ()
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack ((CallStack -> m ()) -> m ())
    -> (Warning -> CallStack -> m ()) -> Warning -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (CallStack -> Warning -> m ()) -> Warning -> CallStack -> m ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip CallStack -> Warning -> m ()
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m ()
    warning'

    -- | Raise every 'WARNING_ON_USAGE' connected to a name.
    {-# SPECIALIZE raiseWarningsOnUsage :: QName -> TCM () #-}
    raiseWarningsOnUsage :: (MonadWarning m, ReadTCState m) => QName -> m ()
    raiseWarningsOnUsage :: forall (m :: * -> *).
    (MonadWarning m, ReadTCState m) =>
    QName -> m ()
    raiseWarningsOnUsage QName
    d = do
      -- In case we find a defined name, we start by checking whether there's
      -- a warning attached to it
      [Char] -> VerboseLevel -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> [Char] -> m ()
    reportSLn [Char]
    "scope.warning.usage" VerboseLevel
    50 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Checking usage of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    P.prettyShow QName
    d
      (Text -> m ()) -> Maybe Text -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Warning -> m ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> m ()) -> (Text -> Warning) -> Text -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Warning
    UserWarning) (Maybe Text -> m ()) -> m (Maybe Text) -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> Map QName Text -> Maybe Text
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    d (Map QName Text -> Maybe Text)
    -> m (Map QName Text) -> m (Maybe Text)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Map QName Text)
    forall (m :: * -> *). ReadTCState m => m (Map QName Text)
    getUserWarnings

    -- * Classifying warnings
    ---------------------------------------------------------------------------

    isUnsolvedWarning :: Warning -> Bool
    isUnsolvedWarning :: Warning -> Bool
    isUnsolvedWarning Warning
    w = Warning -> WarningName
    warningName Warning
    w WarningName -> Set WarningName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set WarningName
    unsolvedWarnings

    isMetaWarning :: Warning -> Bool
    isMetaWarning :: Warning -> Bool
    isMetaWarning = \case
       UnsolvedInteractionMetas{} -> Bool
    True
       UnsolvedMetaVariables{}    -> Bool
    True
       Warning
    _                          -> Bool
    False

    isMetaTCWarning :: TCWarning -> Bool
    isMetaTCWarning :: TCWarning -> Bool
    isMetaTCWarning = Warning -> Bool
    isMetaWarning (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCWarning -> Warning
    tcWarning

    onlyShowIfUnsolved :: Warning -> Bool
    onlyShowIfUnsolved :: Warning -> Bool
    onlyShowIfUnsolved InversionDepthReached{} = Bool
    True
    onlyShowIfUnsolved Warning
    _ = Bool
    False

    -- | Classifying warnings: some are benign, others are (non-fatal) errors

    data WhichWarnings =
        ErrorWarnings -- ^ warnings that will be turned into errors
      | AllWarnings   -- ^ all warnings, including errors and benign ones
      -- Note: order of constructors is important for the derived Ord instance
      deriving (WhichWarnings -> WhichWarnings -> Bool
    (WhichWarnings -> WhichWarnings -> Bool)
    -> (WhichWarnings -> WhichWarnings -> Bool) -> Eq WhichWarnings
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: WhichWarnings -> WhichWarnings -> Bool
    == :: WhichWarnings -> WhichWarnings -> Bool
    $c/= :: WhichWarnings -> WhichWarnings -> Bool
    /= :: WhichWarnings -> WhichWarnings -> Bool
    Eq, Eq WhichWarnings
    Eq WhichWarnings =>
    (WhichWarnings -> WhichWarnings -> Ordering)
    -> (WhichWarnings -> WhichWarnings -> Bool)
    -> (WhichWarnings -> WhichWarnings -> Bool)
    -> (WhichWarnings -> WhichWarnings -> Bool)
    -> (WhichWarnings -> WhichWarnings -> Bool)
    -> (WhichWarnings -> WhichWarnings -> WhichWarnings)
    -> (WhichWarnings -> WhichWarnings -> WhichWarnings)
    -> Ord WhichWarnings
    WhichWarnings -> WhichWarnings -> Bool
    WhichWarnings -> WhichWarnings -> Ordering
    WhichWarnings -> WhichWarnings -> WhichWarnings
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: WhichWarnings -> WhichWarnings -> Ordering
    compare :: WhichWarnings -> WhichWarnings -> Ordering
    $c< :: WhichWarnings -> WhichWarnings -> Bool
    < :: WhichWarnings -> WhichWarnings -> Bool
    $c<= :: WhichWarnings -> WhichWarnings -> Bool
    <= :: WhichWarnings -> WhichWarnings -> Bool
    $c> :: WhichWarnings -> WhichWarnings -> Bool
    > :: WhichWarnings -> WhichWarnings -> Bool
    $c>= :: WhichWarnings -> WhichWarnings -> Bool
    >= :: WhichWarnings -> WhichWarnings -> Bool
    $cmax :: WhichWarnings -> WhichWarnings -> WhichWarnings
    max :: WhichWarnings -> WhichWarnings -> WhichWarnings
    $cmin :: WhichWarnings -> WhichWarnings -> WhichWarnings
    min :: WhichWarnings -> WhichWarnings -> WhichWarnings
    Ord)

    classifyWarning :: Warning -> WhichWarnings
    classifyWarning :: Warning -> WhichWarnings
    classifyWarning Warning
    w =
      if Warning -> WarningName
    warningName Warning
    w WarningName -> Set WarningName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set WarningName
    errorWarnings
      then WhichWarnings
    ErrorWarnings
      else WhichWarnings
    AllWarnings

    classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
    classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
    classifyWarnings [TCWarning]
    ws =
        Set TCWarning -> Set TCWarning -> WarningsAndNonFatalErrors
    WarningsAndNonFatalErrors ([TCWarning] -> Set TCWarning
    forall a. Ord a => [a] -> Set a
    Set.fromList [TCWarning]
    warnings) ([TCWarning] -> Set TCWarning
    forall a. Ord a => [a] -> Set a
    Set.fromList [TCWarning]
    errors)
      where
        partite :: TCWarning -> Bool
    partite = (WhichWarnings -> WhichWarnings -> Bool
    forall a. Ord a => a -> a -> Bool
    < WhichWarnings
    AllWarnings) (WhichWarnings -> Bool)
    -> (TCWarning -> WhichWarnings) -> TCWarning -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Warning -> WhichWarnings
    classifyWarning (Warning -> WhichWarnings)
    -> (TCWarning -> Warning) -> TCWarning -> WhichWarnings
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCWarning -> Warning
    tcWarning
        ([TCWarning]
    errors, [TCWarning]
    warnings) = (TCWarning -> Bool) -> [TCWarning] -> ([TCWarning], [TCWarning])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition TCWarning -> Bool
    partite [TCWarning]
    ws