module Mikan.TypeChecking.Warnings
  ( -- * Monads which can log warnings
    MonadWarning(..)
    -- * Warning construction
  , warning'_, warning_, warning', warning, warnings, warnings'

  , raiseWarningsOnUsage
  , isUnsolvedWarning
  , isMetaTCWarning
  , onlyShowIfUnsolved
  , warningsAddedBy
  , 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 Control.DeepSeq

import Data.Foldable
import Data.List qualified as List
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Maybe ( catMaybes )
import Data.Text qualified as Text

import GHC.Generics

import Mikan.TypeChecking.Monad.Base
import Mikan.TypeChecking.Monad.Debug
import Mikan.TypeChecking.Monad.Caching ( areWeCaching )
import {-# SOURCE #-} Mikan.TypeChecking.Monad.State () -- instance MonadFileId TCM
import {-# SOURCE #-} Mikan.TypeChecking.Pretty ( MonadPretty, prettyTCM, vcat, ($$), nest )
import {-# SOURCE #-} Mikan.TypeChecking.Pretty.Call
import {-# SOURCE #-} Mikan.TypeChecking.Pretty.Warning ( prettyWarning )
import Mikan.TypeChecking.Monad.Diagnostic

import Mikan.Syntax.Concrete.Name ( nameSuffix )
import Mikan.Syntax.Abstract.Name ( QName(..), Name(..) )
import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.Syntax.Position
import Mikan.Syntax.Parser
import Mikan.Syntax.Internal.Blockers (neverUnblock)

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

import Mikan.Version ( docsUrl )

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

import Mikan.Utils.Impossible
import Mikan.Syntax.Common
import Mikan.Syntax.Concrete.Definitions.Errors

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

class (MonadPretty m, MonadError TCErr m) => MonadWarning m where
  -- | Store a warning in the TC state. Warnings are stored regardless
  -- of whether they will be shown to the user, but, in general,
  -- highlighting information is only generated from enabled warnings.
  --
  -- This method should generally not be used directly: see 'warning' instead.
  addWarning
    :: Bool      -- ^ Should highlighting information be generated for this warning?
    -> TCWarning -- ^ The finished 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 = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv
    (do (Set TCWarning -> Identity (Set TCWarning))
-> TCState -> Identity TCState
Lens' TCState (Set TCWarning)
stTCWarnings ((Set TCWarning -> Identity (Set TCWarning))
 -> TCState -> Identity TCState)
-> (Set TCWarning -> Set TCWarning) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` 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)
    (case TCWarning -> WhichWarnings
classifyWarning TCWarning
tcwarn of
      WhichWarnings
ErrorWarnings -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
      WhichWarnings
AllWarnings   -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

-- * Raising warnings
---------------------------------------------------------------------------
warnUrl :: String -> String
warnUrl :: String -> String
warnUrl = String -> String
docsUrl (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"tools/command-line-options.html#cmdoption-arg-" String -> String -> String
forall a. [a] -> [a] -> [a]
++)

{-# SPECIALIZE warning'_ :: CallStack -> Ranged Warning -> TCM TCWarning #-}

-- | Construct a 'TCWarning' from the given 'Diagnostic' value,
-- associating it with the 'Range' provided by the 'Ranged'. This
-- handles pretty-printing the diagnostic into a warning message,
-- including its range and the elaboration context.
warning'_
  :: (MonadWarning m, Diagnostic e)
  => CallStack
  -- ^ Original source location where the warning was added.
  --
  -- See @warning_@ for a version with 'HasCallStack'.
  -> Ranged e
  -- ^ The diagnostic to wrap. The included 'Range' should be correct:
  -- if it is 'noRange', the diagnostic /will not/ be associated with a
  -- position, rather than being associated with the current position.
  --
  -- See 'warning'' for one that uses the 'eRange'.
  -> m TCWarning
warning'_ :: forall (m :: * -> *) e.
(MonadWarning m, Diagnostic e) =>
CallStack -> Ranged e -> m TCWarning
warning'_ CallStack
loc (Ranged Range
r' e
w) = do
  c <- Lens' TCEnv (Maybe (Closure Call)) -> m (Maybe (Closure Call))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Maybe (Closure Call) -> f (Maybe (Closure Call)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Maybe (Closure Call))
eCall
  b <- areWeCaching

  let
    reason = e -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason e
w

    -- Render the diagnostic identifier string as a link to the
    -- documentation.
    ws = e -> String
forall a. Diagnostic a => a -> String
diagnosticString e
w
    wref = Text -> Doc -> Doc
P.href (String -> Text
Text.pack (String -> String
warnUrl String
ws)) (String -> Doc
forall a. String -> Doc a
P.text String
ws)

    -- Only 'DiagWarning's which are not in the 'errorWarnings' list can
    -- be turned off by a @-W@ flag.
    sev = case DiagnosticReason
reason of
      DiagWarning{ _warningName :: DiagnosticReason -> WarningName
_warningName = WarningName
wn }
        | WarningName
wn WarningName -> Set WarningName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set WarningName
errorWarnings -> Doc
"warning: -W[no]" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
wref
      DiagnosticReason
_ -> Doc
"error:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Doc -> Doc
P.brackets Doc
wref

  p <- vcat
    [ pure $ P.hsep
      [ if null r' then mempty else P.pretty r' <> P.colon
      , sev
      ]
    , prettyTCM w
    , prettyTCM c
    ]

  return $ TCWarning loc r' (toSomeDiagnostic w) p (P.render p) b

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

{-# SPECIALIZE warnings' :: CallStack -> List1 (Ranged Warning) -> TCM () #-}

-- | Add a nonempty list of 'Ranged' 'Diagnostic's to the TC state as
-- warnings, constructed as per 'warning'_'.
--
-- This takes the warning mode into account: if @-Werror@ was given and
-- any of the warnings in the list were enabled, they are /thrown/ as
-- 'NonFatalErrors' rather than being added to the state.
warnings' :: (MonadWarning m, Diagnostic e)
  => CallStack
  -- ^ The original source location to associate with the warnings.
  --
  -- See 'warnings' for a version with 'HasCallStack'.
  -> List1 (Ranged e)
  -- ^ The diagnostics to record. The positioning note in 'warning'_'
  -- applies here too.
  -> m ()
warnings' :: forall (m :: * -> *) e.
(MonadWarning m, Diagnostic e) =>
CallStack -> List1 (Ranged e) -> m ()
warnings' CallStack
loc List1 (Ranged e)
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 \w' :: Ranged e
w'@(Ranged Range
_ e
diag) -> do

    -- TODO: warning flags?
    let
      (Bool
enabled, Bool
hl) = case e -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason e
diag of
        DiagWarning{ _warningName :: DiagnosticReason -> WarningName
_warningName = WarningName
wn } -> (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, 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
exactSplitWarnings)
        DiagError{}                      -> (Bool
False, Bool
True)

    tcwarn <- CallStack -> Ranged e -> m TCWarning
forall (m :: * -> *) e.
(MonadWarning m, Diagnostic e) =>
CallStack -> Ranged e -> m TCWarning
warning'_ CallStack
loc Ranged e
w'
    if wError && enabled
      then pure (Just tcwarn)
      else Nothing <$ addWarning (enabled || hl) 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 :: * -> *) e a.
(MonadTCError m, Diagnostic e) =>
CallStack -> e -> 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 (Ranged Warning) -> TCM () #-}
warnings :: (HasCallStack, MonadWarning m, Diagnostic e) => List1 (Ranged e) -> m ()
warnings :: forall (m :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
List1 (Ranged e) -> m ()
warnings = (CallStack -> m ()) -> m ()
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> m ()) -> m ())
-> (List1 (Ranged e) -> CallStack -> m ())
-> List1 (Ranged e)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallStack -> List1 (Ranged e) -> m ())
-> List1 (Ranged e) -> CallStack -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip CallStack -> List1 (Ranged e) -> m ()
forall (m :: * -> *) e.
(MonadWarning m, Diagnostic e) =>
CallStack -> List1 (Ranged e) -> m ()
warnings'

{-# SPECIALIZE warning' :: Diagnostic e => CallStack -> e -> TCM () #-}
-- | Add a single 'Diagnostic' value as a warning to the TC state,
-- associated with the range of the current elaborator computation.
--
-- This function takes the warning mode into account, as with 'warnings''.
warning' :: (MonadWarning m, Diagnostic e) => CallStack -> e -> m ()
warning' :: forall (m :: * -> *) e.
(MonadWarning m, Diagnostic e) =>
CallStack -> e -> m ()
warning' CallStack
loc e
diag = 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
  warnings' loc . singleton . Ranged r $ toSomeDiagnostic diag

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

-- | Raise every 'WARNING_ON_USAGE' connected to a name.
{-# SPECIALIZE raiseWarningsOnUsage :: QName -> TCM () #-}
raiseWarningsOnUsage :: (MonadWarning m) => QName -> m ()
raiseWarningsOnUsage :: forall (m :: * -> *). MonadWarning 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
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"scope.warning.usage" VerboseLevel
50 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Checking usage of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
d
  (QName -> Map QName UserWarningInfo -> Maybe UserWarningInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
d (Map QName UserWarningInfo -> Maybe UserWarningInfo)
-> m (Map QName UserWarningInfo) -> m (Maybe UserWarningInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Map QName UserWarningInfo)
forall (m :: * -> *).
ReadTCState m =>
m (Map QName UserWarningInfo)
getUserWarnings) m (Maybe UserWarningInfo)
-> (Maybe UserWarningInfo -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (UserWarningInfo -> m ()) -> Maybe UserWarningInfo -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ \ (UserWarningInfo ShortText
w Name
c) -> do
    -- We also check that the concrete name of the WARNING_ON_USAGE pragma
    -- matches the concrete name that was used, so that we can deprecate e.g.
    -- referring to Type as Set.
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ASetter Name Name (Maybe Suffix) (Maybe Suffix)
-> Maybe Suffix -> Name -> Name
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Name Name (Maybe Suffix) (Maybe Suffix)
Lens' Name (Maybe Suffix)
nameSuffix Maybe Suffix
forall a. Maybe a
Nothing (Name -> Name
nameConcrete (QName -> Name
qnameName QName
d)) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
c) do
      Warning -> m ()
forall (m :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> m ()
warning (ShortText -> Warning
UserWarning ShortText
w)

warningsAddedBy :: (ReadTCState m, MonadTCState m) => m a -> m (a, Set.Set TCWarning)
warningsAddedBy :: forall (m :: * -> *) a.
(ReadTCState m, MonadTCState m) =>
m a -> m (a, Set TCWarning)
warningsAddedBy m a
cont = do
  !old <- Lens' TCState (Set TCWarning)
-> (Set TCWarning -> (Set TCWarning, Set TCWarning))
-> m (Set TCWarning)
forall (m :: * -> *) a r.
(MonadTCState m, ReadTCState m) =>
Lens' TCState a -> (a -> (r, a)) -> m r
stateTCLens (Set TCWarning -> f (Set TCWarning)) -> TCState -> f TCState
Lens' TCState (Set TCWarning)
stTCWarnings \Set TCWarning
old -> (Set TCWarning
old, Set TCWarning
forall a. Monoid a => a
mempty)
  !res <- cont
  stateTCLens stTCWarnings \Set TCWarning
new ->
    let !merged :: Set TCWarning
merged = Set TCWarning
new Set TCWarning -> Set TCWarning -> Set TCWarning
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set TCWarning
old
     in ((a
res, Set TCWarning
new), Set TCWarning
merged)

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

isUnsolvedWarning :: TCWarning -> Bool
isUnsolvedWarning :: TCWarning -> Bool
isUnsolvedWarning TCWarning
w = case SomeDiagnostic -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
w) of
  DiagWarning{_warningName :: DiagnosticReason -> WarningName
_warningName = WarningName
nm} -> WarningName
nm WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
unsolvedWarnings
  DiagnosticReason
DiagError                      -> Bool
False

isMetaTCWarning :: TCWarning -> Bool
isMetaTCWarning :: TCWarning -> Bool
isMetaTCWarning TCWarning
w = case SomeDiagnostic -> Maybe UnsolvedWarning
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
w) of
  Just UnsolvedInteractionMetas{} -> Bool
True
  Just UnsolvedMetaVariables{}    -> Bool
True
  Maybe UnsolvedWarning
_                               -> Bool
False

onlyShowIfUnsolved :: TCWarning -> Bool
onlyShowIfUnsolved :: TCWarning -> Bool
onlyShowIfUnsolved TCWarning
w = case SomeDiagnostic -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
w) of
  DiagWarning { _warningName :: DiagnosticReason -> WarningName
_warningName = WarningName
InversionDepthReached_ } -> Bool
True
  DiagnosticReason
_                                                     -> 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
  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)

instance Ord WhichWarnings where
  compare :: WhichWarnings -> WhichWarnings -> Ordering
compare = \case
    WhichWarnings
ErrorWarnings -> \case
      WhichWarnings
ErrorWarnings -> Ordering
EQ
      WhichWarnings
AllWarnings   -> Ordering
LT
    WhichWarnings
AllWarnings -> \case
      WhichWarnings
ErrorWarnings -> Ordering
GT
      WhichWarnings
AllWarnings   -> Ordering
EQ

classifyWarning :: TCWarning -> WhichWarnings
classifyWarning :: TCWarning -> WhichWarnings
classifyWarning TCWarning
w = case SomeDiagnostic -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
w) of
  DiagWarning{ _warningName :: DiagnosticReason -> WarningName
_warningName = WarningName
w }
    | WarningName
w WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
errorWarnings -> WhichWarnings
ErrorWarnings
    | Bool
otherwise                    -> WhichWarnings
AllWarnings
  DiagError{} -> WhichWarnings
ErrorWarnings

classifyWarnings :: Set.Set TCWarning -> WarningsAndNonFatalErrors
classifyWarnings :: Set TCWarning -> WarningsAndNonFatalErrors
classifyWarnings Set TCWarning
ws = Set TCWarning -> Set TCWarning -> WarningsAndNonFatalErrors
WarningsAndNonFatalErrors Set TCWarning
warnings Set 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
. TCWarning -> WhichWarnings
classifyWarning
  (Set TCWarning
errors, Set TCWarning
warnings) = (TCWarning -> Bool)
-> Set TCWarning -> (Set TCWarning, Set TCWarning)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition TCWarning -> Bool
partite Set TCWarning
ws

instance Diagnostic UnsolvedWarning where
  diagnosticReason :: UnsolvedWarning -> DiagnosticReason
diagnosticReason = \case
    UnsolvedInteractionMetas{}  -> WarningName -> DiagnosticReason
DiagWarning WarningName
UnsolvedInteractionMetas_
    UnsolvedConstraints{}       -> WarningName -> DiagnosticReason
DiagWarning WarningName
UnsolvedConstraints_
    UnsolvedMetaVariables{}     -> WarningName -> DiagnosticReason
DiagWarning WarningName
UnsolvedMetaVariables_
    InteractionMetaBoundaries{} -> WarningName -> DiagnosticReason
DiagWarning WarningName
InteractionMetaBoundaries_

  diagnosticString :: UnsolvedWarning -> String
diagnosticString = WarningName -> String
warningNameToString (WarningName -> String)
-> (UnsolvedWarning -> WarningName) -> UnsolvedWarning -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiagnosticReason -> WarningName
_warningName (DiagnosticReason -> WarningName)
-> (UnsolvedWarning -> DiagnosticReason)
-> UnsolvedWarning
-> WarningName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnsolvedWarning -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason

instance Diagnostic DeclarationWarning where
  diagnosticReason :: DeclarationWarning -> DiagnosticReason
diagnosticReason DeclarationWarning
warn = case DeclarationWarning -> DeclarationWarning'
dwWarning DeclarationWarning
warn of
    SafeFlagEta{}               -> DiagnosticReason
DiagError
    SafeFlagInjective{}         -> DiagnosticReason
DiagError
    SafeFlagNoCoverageCheck{}   -> DiagnosticReason
DiagError
    SafeFlagNoPositivityCheck{} -> DiagnosticReason
DiagError
    SafeFlagNoUniverseCheck{}   -> DiagnosticReason
DiagError
    SafeFlagNonTerminating{}    -> DiagnosticReason
DiagError
    SafeFlagPolarity{}          -> DiagnosticReason
DiagError
    SafeFlagTerminating{}       -> DiagnosticReason
DiagError
    MissingDefinitions{}        -> DiagnosticReason
DiagError
    MissingDataDeclaration{}    -> DiagnosticReason
DiagError
    NotAllowedInMutual{}        -> DiagnosticReason
DiagError
    DeclarationWarning'
_                           -> WarningName -> DiagnosticReason
DiagWarning (WarningName -> DiagnosticReason)
-> WarningName -> DiagnosticReason
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> WarningName
declarationWarningName DeclarationWarning
warn

  diagnosticString :: DeclarationWarning -> String
diagnosticString = WarningName -> String
warningNameToString (WarningName -> String)
-> (DeclarationWarning -> WarningName)
-> DeclarationWarning
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeclarationWarning -> WarningName
declarationWarningName

instance Diagnostic Warning where
  diagnosticReason :: Warning -> DiagnosticReason
diagnosticReason = WarningName -> DiagnosticReason
DiagWarning (WarningName -> DiagnosticReason)
-> (Warning -> WarningName) -> Warning -> DiagnosticReason
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> WarningName
warningName
  diagnosticString :: Warning -> String
diagnosticString = WarningName -> String
warningNameToString (WarningName -> String)
-> (Warning -> WarningName) -> Warning -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> WarningName
warningName