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

    import Control.Monad ( forM, unless )
    import Control.Monad.Except
    import Control.Monad.Reader ( ReaderT )
    import Control.Monad.State ( StateT )
    import Control.Monad.Trans ( lift )

    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)
    import {-# SOURCE #-} Agda.TypeChecking.Pretty.Call
    import {-# SOURCE #-} Agda.TypeChecking.Pretty.Warning ( prettyWarning )
    import {-# SOURCE #-} Agda.TypeChecking.Monad.Pure

    import Agda.Syntax.Abstract.Name ( QName )
    import Agda.Syntax.Common
    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.Lens
    import qualified Agda.Utils.Pretty as P

    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 :: TCWarning -> m ()

      default addWarning
        :: (MonadWarning n, MonadTrans t, t n ~ m)
        => TCWarning -> m ()
      addWarning = n () -> t n ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n () -> t n ()) -> (TCWarning -> n ()) -> TCWarning -> t n ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCWarning -> n ()
    forall (m :: * -> *). MonadWarning m => TCWarning -> m ()
    addWarning

    instance MonadWarning m => MonadWarning (ReaderT r m)
    instance MonadWarning m => MonadWarning (StateT s m)

    instance MonadWarning TCM where
      addWarning :: TCWarning -> TCM ()
    addWarning TCWarning
    tcwarn = do
        Lens' [TCWarning] TCState
    stTCWarnings Lens' [TCWarning] TCState -> ([TCWarning] -> [TCWarning]) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` Warning -> TCWarning -> [TCWarning] -> [TCWarning]
    forall {a}. Eq a => Warning -> a -> [a] -> [a]
    add Warning
    w' TCWarning
    tcwarn
        TCWarning -> TCM ()
    highlightWarning TCWarning
    tcwarn
        where
          w' :: Warning
    w' = TCWarning -> Warning
    tcWarning TCWarning
    tcwarn

          add :: Warning -> a -> [a] -> [a]
    add Warning
    w a
    tcwarn [a]
    tcwarns
            | Warning -> Bool
    onlyOnce Warning
    w Bool -> Bool -> Bool
    && a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    elem a
    tcwarn [a]
    tcwarns = [a]
    tcwarns -- Eq on TCWarning only checks head constructor
            | Bool
    otherwise                         = a
    tcwarn a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    tcwarns

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

    {-# SPECIALIZE genericWarning :: P.Doc -> TCM () #-}
    genericWarning :: MonadWarning m => P.Doc -> m ()
    genericWarning :: forall (m :: * -> *). MonadWarning m => Doc -> m ()
    genericWarning = Warning -> m ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> m ()) -> (Doc -> Warning) -> Doc -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> Warning
    GenericWarning

    {-# SPECIALIZE genericNonFatalError :: P.Doc -> TCM () #-}
    genericNonFatalError :: MonadWarning m => P.Doc -> m ()
    genericNonFatalError :: forall (m :: * -> *). MonadWarning m => Doc -> m ()
    genericNonFatalError = Warning -> m ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> m ()) -> (Doc -> Warning) -> Doc -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> Warning
    GenericNonFatalError

    {-# 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
      Range' SrcFile
    r <- Lens' (Range' SrcFile) TCEnv -> m (Range' SrcFile)
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' (Range' SrcFile) TCEnv
    eRange
      Maybe (Closure Call)
    c <- Lens' (Maybe (Closure Call)) TCEnv -> m (Maybe (Closure Call))
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' (Maybe (Closure Call)) TCEnv
    eCall
      Bool
    b <- m Bool
    forall (m :: * -> *). ReadTCState m => m Bool
    areWeCaching
      -- NicifierIssues print their own error locations in their list of
      -- issues (but we might need to keep the overall range `r` for
      -- comparing ranges)
      let r' :: Range' SrcFile
    r' = case Warning
    w of { NicifierIssue{} -> Range' SrcFile
    forall a. Range' a
    NoRange ; Warning
    _ -> Range' SrcFile
    r }
      Doc
    p <- Range' SrcFile -> Maybe (Closure Call) -> m Doc -> m Doc
    forall (m :: * -> *).
    MonadPretty m =>
    Range' SrcFile -> Maybe (Closure Call) -> m Doc -> m Doc
    sayWhen Range' SrcFile
    r' Maybe (Closure Call)
    c (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Warning -> m Doc
    forall (m :: * -> *). MonadPretty m => Warning -> m Doc
    prettyWarning Warning
    w
      TCWarning -> m TCWarning
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TCWarning -> m TCWarning) -> TCWarning -> m TCWarning
    forall a b. (a -> b) -> a -> b
    $ CallStack -> Range' SrcFile -> Warning -> Doc -> Bool -> TCWarning
    TCWarning CallStack
    loc Range' SrcFile
    r Warning
    w Doc
    p Bool
    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 -> [Warning] -> TCM () #-}
    warnings' :: MonadWarning m => CallStack -> [Warning] -> m ()
    warnings' :: forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> [Warning] -> m ()
    warnings' CallStack
    loc [Warning]
    ws = do

      WarningMode
    wmode <- 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 in the @warningSet@
      -- or not. If we find one which should be turned into an error, we keep processing
      -- the rest of the warnings and *then* report all of the errors at once.
      [Maybe TCWarning]
    merrs <- [Warning]
    -> (Warning -> m (Maybe TCWarning)) -> m [Maybe TCWarning]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Warning]
    ws ((Warning -> m (Maybe TCWarning)) -> m [Maybe TCWarning])
    -> (Warning -> m (Maybe TCWarning)) -> m [Maybe TCWarning]
    forall a b. (a -> b) -> a -> b
    $ \ Warning
    w' -> do
        TCWarning
    tcwarn <- CallStack -> Warning -> m TCWarning
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m TCWarning
    warning'_ CallStack
    loc Warning
    w'
        if WarningMode
    wmode WarningMode -> Lens' Bool WarningMode -> Bool
    forall o i. o -> Lens' i o -> i
    ^. Lens' Bool WarningMode
    warn2Error Bool -> Bool -> Bool
    && Warning -> WarningName
    warningName Warning
    w' WarningName -> Set WarningName -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` WarningMode
    wmode WarningMode
    -> Lens' (Set WarningName) WarningMode -> Set WarningName
    forall o i. o -> Lens' i o -> i
    ^. Lens' (Set WarningName) WarningMode
    warningSet
        then Maybe TCWarning -> m (Maybe TCWarning)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TCWarning -> Maybe TCWarning
    forall a. a -> Maybe a
    Just TCWarning
    tcwarn)
        else Maybe TCWarning
    forall a. Maybe a
    Nothing Maybe TCWarning -> m () -> m (Maybe TCWarning)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCWarning -> m ()
    forall (m :: * -> *). MonadWarning m => TCWarning -> m ()
    addWarning TCWarning
    tcwarn

      let errs :: [TCWarning]
    errs = [Maybe TCWarning] -> [TCWarning]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe TCWarning]
    merrs
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([TCWarning] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TCWarning]
    errs) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ 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
    $ [TCWarning] -> TypeError
    NonFatalErrors [TCWarning]
    errs

    {-# SPECIALIZE warnings :: HasCallStack => [Warning] -> TCM () #-}
    warnings :: (HasCallStack, MonadWarning m) => [Warning] -> m ()
    warnings :: forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    [Warning] -> m ()
    warnings = (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 ()
    warnings'

    {-# SPECIALIZE warning' :: CallStack -> Warning -> TCM () #-}
    warning' :: MonadWarning m => CallStack -> Warning -> m ()
    warning' :: forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m ()
    warning' CallStack
    loc = CallStack -> [Warning] -> m ()
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> [Warning] -> m ()
    warnings' CallStack
    loc ([Warning] -> m ()) -> (Warning -> [Warning]) -> Warning -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Warning -> [Warning]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    {-# 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

    -- | Should we only emit a single warning with this constructor.
    onlyOnce :: Warning -> Bool
    onlyOnce :: Warning -> Bool
    onlyOnce InversionDepthReached{} = Bool
    True
    onlyOnce Warning
    _ = Bool
    False

    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
    /= :: WhichWarnings -> WhichWarnings -> Bool
    $c/= :: WhichWarnings -> WhichWarnings -> Bool
    == :: WhichWarnings -> WhichWarnings -> Bool
    $c== :: 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
    min :: WhichWarnings -> WhichWarnings -> WhichWarnings
    $cmin :: WhichWarnings -> WhichWarnings -> WhichWarnings
    max :: WhichWarnings -> WhichWarnings -> WhichWarnings
    $cmax :: WhichWarnings -> WhichWarnings -> WhichWarnings
    >= :: WhichWarnings -> WhichWarnings -> Bool
    $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
    compare :: WhichWarnings -> WhichWarnings -> Ordering
    $ccompare :: WhichWarnings -> WhichWarnings -> Ordering
    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

    -- | Assorted warnings and errors to be displayed to the user
    data WarningsAndNonFatalErrors = WarningsAndNonFatalErrors
      { WarningsAndNonFatalErrors -> [TCWarning]
    tcWarnings     :: [TCWarning]
      , WarningsAndNonFatalErrors -> [TCWarning]
    nonFatalErrors :: [TCWarning]
      }

    -- | The only way to construct a empty WarningsAndNonFatalErrors

    emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors
    emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors
    emptyWarningsAndNonFatalErrors = [TCWarning] -> [TCWarning] -> WarningsAndNonFatalErrors
    WarningsAndNonFatalErrors [] []

    classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
    classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
    classifyWarnings [TCWarning]
    ws = [TCWarning] -> [TCWarning] -> WarningsAndNonFatalErrors
    WarningsAndNonFatalErrors [TCWarning]
    warnings [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

    -- * Warnings in the parser
    ---------------------------------------------------------------------------

    -- | running the Parse monad

    runPM :: PM a -> TCM a
    runPM :: forall a. PM a -> TCM a
    runPM PM a
    m = do
      (Either ParseError a
    res, [ParseWarning]
    ws) <- PM a -> TCMT IO (Either ParseError a, [ParseWarning])
    forall (m :: * -> *) a.
    MonadIO m =>
    PM a -> m (Either ParseError a, [ParseWarning])
    runPMIO PM a
    m
      (ParseWarning -> TCM ()) -> [ParseWarning] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ())
    -> (ParseWarning -> Warning) -> ParseWarning -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseWarning -> Warning
    ParseWarning) [ParseWarning]
    ws
      case Either ParseError a
    res of
        Left  ParseError
    e -> TCErr -> TCM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (Range' SrcFile -> Doc -> TCErr
    Exception (ParseError -> Range' SrcFile
    forall a. HasRange a => a -> Range' SrcFile
    getRange ParseError
    e) (ParseError -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty ParseError
    e))
        Right a
    a -> a -> TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a