    module Agda.Interaction.Options.Warnings
           (
             WarningMode (..)
           , warningSet
           , warn2Error
           , lensSingleWarning
           , defaultWarningSet
           , allWarnings
           , usualWarnings
           , noWarnings
           , unsolvedWarnings
           , incompleteMatchWarnings
           , errorWarnings
           , exactSplitWarnings
           , defaultWarningMode
           , WarningModeError(..)
           , prettyWarningModeError
           , warningModeUpdate
           , warningSets
           , WarningName (..)
           , warningName2String
           , string2WarningName
           , usageWarning
           )
    where

    import Control.Arrow ( (&&&) )
    import Control.DeepSeq
    import Control.Monad ( guard, when )
    import Control.Monad.Except ( throwError )

    import qualified Data.HashMap.Strict as HMap
    import Data.List ( stripPrefix, intercalate, partition, sort )
    import Data.Set  ( Set )
    import qualified Data.Set as Set
    import Data.Text ( Text )
    import qualified Data.Text as Text

    import GHC.Generics (Generic)

    import Agda.Utils.Either ( maybeToEither )
    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.Maybe

    import Agda.Utils.Impossible

    -- | A @WarningMode@ has two components: a set of warnings to be displayed
    -- and a flag stating whether warnings should be turned into fatal errors.
    data WarningMode = WarningMode
      { WarningMode -> Set WarningName
    _warningSet :: Set WarningName
      , WarningMode -> Bool
    _warn2Error :: Bool
      } deriving (WarningMode -> WarningMode -> Bool
    (WarningMode -> WarningMode -> Bool)
    -> (WarningMode -> WarningMode -> Bool) -> Eq WarningMode
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: WarningMode -> WarningMode -> Bool
    == :: WarningMode -> WarningMode -> Bool
    $c/= :: WarningMode -> WarningMode -> Bool
    /= :: WarningMode -> WarningMode -> Bool
    Eq, Int -> WarningMode -> ShowS
    [WarningMode] -> ShowS
    WarningMode -> String
    (Int -> WarningMode -> ShowS)
    -> (WarningMode -> String)
    -> ([WarningMode] -> ShowS)
    -> Show WarningMode
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> WarningMode -> ShowS
    showsPrec :: Int -> WarningMode -> ShowS
    $cshow :: WarningMode -> String
    show :: WarningMode -> String
    $cshowList :: [WarningMode] -> ShowS
    showList :: [WarningMode] -> ShowS
    Show, (forall x. WarningMode -> Rep WarningMode x)
    -> (forall x. Rep WarningMode x -> WarningMode)
    -> Generic WarningMode
    forall x. Rep WarningMode x -> WarningMode
    forall x. WarningMode -> Rep WarningMode x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. WarningMode -> Rep WarningMode x
    from :: forall x. WarningMode -> Rep WarningMode x
    $cto :: forall x. Rep WarningMode x -> WarningMode
    to :: forall x. Rep WarningMode x -> WarningMode
    Generic)

    instance NFData WarningMode

    -- Lenses

    warningSet :: Lens' WarningMode (Set WarningName)
    warningSet :: Lens' WarningMode (Set WarningName)
    warningSet Set WarningName -> f (Set WarningName)
    f WarningMode
    o = (\ Set WarningName
    ws -> WarningMode
    o { _warningSet = ws }) (Set WarningName -> WarningMode)
    -> f (Set WarningName) -> f WarningMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Set WarningName -> f (Set WarningName)
    f (WarningMode -> Set WarningName
    _warningSet WarningMode
    o)

    warn2Error :: Lens' WarningMode Bool
    warn2Error :: Lens' WarningMode Bool
    warn2Error Bool -> f Bool
    f WarningMode
    o = (\ Bool
    ws -> WarningMode
    o { _warn2Error = ws }) (Bool -> WarningMode) -> f Bool -> f WarningMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> f Bool
    f (WarningMode -> Bool
    _warn2Error WarningMode
    o)

    lensSingleWarning :: WarningName -> Lens' WarningMode Bool
    lensSingleWarning :: WarningName -> Lens' WarningMode Bool
    lensSingleWarning WarningName
    w = (Set WarningName -> f (Set WarningName))
    -> WarningMode -> f WarningMode
    Lens' WarningMode (Set WarningName)
    warningSet ((Set WarningName -> f (Set WarningName))
     -> WarningMode -> f WarningMode)
    -> ((Bool -> f Bool) -> Set WarningName -> f (Set WarningName))
    -> (Bool -> f Bool)
    -> WarningMode
    -> f WarningMode
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WarningName -> Lens' (Set WarningName) Bool
    forall k. Ord k => k -> Lens' (Set k) Bool
    contains WarningName
    w

    -- | The @defaultWarningMode@ is a curated set of warnings covering non-fatal
    -- errors and disabling style-related ones

    defaultWarningSet :: String
    defaultWarningSet :: String
    defaultWarningSet = String
    "warn"

    defaultWarningMode :: WarningMode
    defaultWarningMode :: WarningMode
    defaultWarningMode = Set WarningName -> Bool -> WarningMode
    WarningMode Set WarningName
    ws Bool
    False where
      ws :: Set WarningName
    ws = (Set WarningName, String) -> Set WarningName
    forall a b. (a, b) -> a
    fst ((Set WarningName, String) -> Set WarningName)
    -> (Set WarningName, String) -> Set WarningName
    forall a b. (a -> b) -> a -> b
    $ (Set WarningName, String)
    -> Maybe (Set WarningName, String) -> (Set WarningName, String)
    forall a. a -> Maybe a -> a
    fromMaybe (Set WarningName, String)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Set WarningName, String) -> (Set WarningName, String))
    -> Maybe (Set WarningName, String) -> (Set WarningName, String)
    forall a b. (a -> b) -> a -> b
    $ String
    -> [(String, (Set WarningName, String))]
    -> Maybe (Set WarningName, String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    defaultWarningSet [(String, (Set WarningName, String))]
    warningSets

    -- | Some warnings are errors and cannot be turned off.
    data WarningModeError
      = Unknown Text
          -- ^ Unknown warning.
      | NoNoError Text
          -- ^ Warning that cannot be disabled.
      deriving (Int -> WarningModeError -> ShowS
    [WarningModeError] -> ShowS
    WarningModeError -> String
    (Int -> WarningModeError -> ShowS)
    -> (WarningModeError -> String)
    -> ([WarningModeError] -> ShowS)
    -> Show WarningModeError
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> WarningModeError -> ShowS
    showsPrec :: Int -> WarningModeError -> ShowS
    $cshow :: WarningModeError -> String
    show :: WarningModeError -> String
    $cshowList :: [WarningModeError] -> ShowS
    showList :: [WarningModeError] -> ShowS
    Show, (forall x. WarningModeError -> Rep WarningModeError x)
    -> (forall x. Rep WarningModeError x -> WarningModeError)
    -> Generic WarningModeError
    forall x. Rep WarningModeError x -> WarningModeError
    forall x. WarningModeError -> Rep WarningModeError x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. WarningModeError -> Rep WarningModeError x
    from :: forall x. WarningModeError -> Rep WarningModeError x
    $cto :: forall x. Rep WarningModeError x -> WarningModeError
    to :: forall x. Rep WarningModeError x -> WarningModeError
    Generic)

    instance NFData WarningModeError

    prettyWarningModeError :: WarningModeError -> Text
    prettyWarningModeError :: WarningModeError -> Text
    prettyWarningModeError = \case
      Unknown   Text
    w -> [Text] -> Text
    Text.concat [ Text
    "Unknown warning flag: ", Text
    w, Text
    "." ]
      NoNoError Text
    w -> [Text] -> Text
    Text.concat
        [ Text
    "You may only turn off benign warnings. The warning "
        , Text
    w
        , Text
    " is a non-fatal error and thus cannot be ignored."
        ]

    -- | From user-given directives we compute WarningMode updates
    type WarningModeUpdate = WarningMode -> WarningMode

    -- | @warningModeUpdate str@ computes the action of @str@ over the current
    -- @WarningMode@: it may reset the set of warnings, add or remove a specific
    -- flag or demand that any warning be turned into an error

    warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate
    warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate
    warningModeUpdate String
    str = case String
    str of
      String
    "error"   -> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
    forall a. a -> Either WarningModeError a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (WarningModeUpdate -> Either WarningModeError WarningModeUpdate)
    -> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
    forall a b. (a -> b) -> a -> b
    $ Lens' WarningMode Bool -> LensSet WarningMode Bool
    forall o i. Lens' o i -> LensSet o i
    set (Bool -> f Bool) -> WarningMode -> f WarningMode
    Lens' WarningMode Bool
    warn2Error Bool
    True
      String
    "noerror" -> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
    forall a. a -> Either WarningModeError a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (WarningModeUpdate -> Either WarningModeError WarningModeUpdate)
    -> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
    forall a b. (a -> b) -> a -> b
    $ Lens' WarningMode Bool -> LensSet WarningMode Bool
    forall o i. Lens' o i -> LensSet o i
    set (Bool -> f Bool) -> WarningMode -> f WarningMode
    Lens' WarningMode Bool
    warn2Error Bool
    False
      String
    _ | Just Set WarningName
    ws <- (Set WarningName, String) -> Set WarningName
    forall a b. (a, b) -> a
    fst ((Set WarningName, String) -> Set WarningName)
    -> Maybe (Set WarningName, String) -> Maybe (Set WarningName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String
    -> [(String, (Set WarningName, String))]
    -> Maybe (Set WarningName, String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    str [(String, (Set WarningName, String))]
    warningSets
                -> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
    forall a. a -> Either WarningModeError a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (WarningModeUpdate -> Either WarningModeError WarningModeUpdate)
    -> WarningModeUpdate -> Either WarningModeError WarningModeUpdate
    forall a b. (a -> b) -> a -> b
    $ Lens' WarningMode (Set WarningName)
    -> LensSet WarningMode (Set WarningName)
    forall o i. Lens' o i -> LensSet o i
    set (Set WarningName -> f (Set WarningName))
    -> WarningMode -> f WarningMode
    Lens' WarningMode (Set WarningName)
    warningSet Set WarningName
    ws
      String
    _ -> case String -> String -> Maybe String
    forall a. Eq a => [a] -> [a] -> Maybe [a]
    stripPrefix String
    "no" String
    str of
        Maybe String
    Nothing   -> do
          wname <- String -> Either WarningModeError WarningName
    stringToWarningName String
    str
          pure (over warningSet $ Set.insert wname)
        Just String
    str' -> do
          wname <- String -> Either WarningModeError WarningName
    stringToWarningName String
    str'
          when (wname `elem` errorWarnings) $
            throwError $ NoNoError $ Text.pack str'
          pure (over warningSet $ Set.delete wname)
      where
        stringToWarningName :: String -> Either WarningModeError WarningName
        stringToWarningName :: String -> Either WarningModeError WarningName
    stringToWarningName String
    str = WarningModeError
    -> Maybe WarningName -> Either WarningModeError WarningName
    forall e a. e -> Maybe a -> Either e a
    maybeToEither (Text -> WarningModeError
    Unknown (Text -> WarningModeError) -> Text -> WarningModeError
    forall a b. (a -> b) -> a -> b
    $ String -> Text
    Text.pack String
    str) (Maybe WarningName -> Either WarningModeError WarningName)
    -> Maybe WarningName -> Either WarningModeError WarningName
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe WarningName
    string2WarningName String
    str

    -- | Common sets of warnings

    warningSets :: [(String, (Set WarningName, String))]
    warningSets :: [(String, (Set WarningName, String))]
    warningSets = [ (String
    "all"   , (Set WarningName
    allWarnings, String
    "All of the existing warnings"))
                  , (String
    "warn"  , (Set WarningName
    usualWarnings, String
    "Default warning level"))
                  , (String
    "ignore", (Set WarningName
    errorWarnings, String
    "Ignore all the benign warnings"))
                  ]

    noWarnings :: Set WarningName
    noWarnings :: Set WarningName
    noWarnings = Set WarningName
    forall a. Set a
    Set.empty

    unsolvedWarnings :: Set WarningName
    unsolvedWarnings :: Set WarningName
    unsolvedWarnings = [WarningName] -> Set WarningName
    forall a. Ord a => [a] -> Set a
    Set.fromList
                     [ WarningName
    UnsolvedMetaVariables_
                     , WarningName
    UnsolvedInteractionMetas_
                     , WarningName
    UnsolvedConstraints_
                     ]

    incompleteMatchWarnings :: Set WarningName
    incompleteMatchWarnings :: Set WarningName
    incompleteMatchWarnings = [WarningName] -> Set WarningName
    forall a. Ord a => [a] -> Set a
    Set.fromList [ WarningName
    CoverageIssue_ ]

    errorWarnings :: Set WarningName
    errorWarnings :: Set WarningName
    errorWarnings = [WarningName] -> Set WarningName
    forall a. Ord a => [a] -> Set a
    Set.fromList
      [ WarningName
    CoverageIssue_
      , WarningName
    InvalidCharacterLiteral_
      , WarningName
    MissingDefinitions_
      , WarningName
    MissingDataDeclaration_
      , WarningName
    NotAllowedInMutual_
      , WarningName
    NotStrictlyPositive_
      , WarningName
    ConstructorDoesNotFitInData_
      , WarningName
    OverlappingTokensWarning_
      , WarningName
    PragmaCompiled_
      , WarningName
    SafeFlagPostulate_
      , WarningName
    SafeFlagPragma_
      , WarningName
    SafeFlagNonTerminating_
      , WarningName
    SafeFlagTerminating_
      , WarningName
    SafeFlagWithoutKFlagPrimEraseEquality_
      , WarningName
    SafeFlagNoPositivityCheck_
      , WarningName
    SafeFlagPolarity_
      , WarningName
    SafeFlagNoUniverseCheck_
      , WarningName
    SafeFlagEta_
      , WarningName
    SafeFlagInjective_
      , WarningName
    SafeFlagNoCoverageCheck_
      , WarningName
    TerminationIssue_
      , WarningName
    TooManyArgumentsToSort_
      , WarningName
    UnsolvedMetaVariables_
      , WarningName
    UnsolvedInteractionMetas_
      , WarningName
    UnsolvedConstraints_
      , WarningName
    InfectiveImport_
      , WarningName
    CoInfectiveImport_
      -- Andreas, 2024-02-15: the following warning used to be a GenericWarning (not an error warning).
      -- Maybe revisit.
      -- , ConfluenceCheckingIncompleteBecauseOfMeta_
      , WarningName
    RewriteNonConfluent_
      , WarningName
    RewriteMaybeNonConfluent_
      , WarningName
    RewriteAmbiguousRules_
      , WarningName
    RewriteMissingRule_
      , WarningName
    TopLevelPolarity_

      -- Recoverable scope-checking errors
      , WarningName
    HiddenNotInArgumentPosition_
      , WarningName
    InstanceNotInArgumentPosition_
      , WarningName
    MacroInLetBindings_
      , WarningName
    AbstractInLetBindings_
      ]

    allWarnings :: Set WarningName
    allWarnings :: Set WarningName
    allWarnings = [WarningName] -> Set WarningName
    forall a. Ord a => [a] -> Set a
    Set.fromList [WarningName
    forall a. Bounded a => a
    minBound..WarningName
    forall a. Bounded a => a
    maxBound]

    usualWarnings :: Set WarningName
    usualWarnings :: Set WarningName
    usualWarnings =
      Set WarningName
    allWarnings Set WarningName -> Set WarningName -> Set WarningName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.\\ Set WarningName
    exactSplitWarnings Set WarningName -> Set WarningName -> Set WarningName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.\\ [WarningName] -> Set WarningName
    forall a. Ord a => [a] -> Set a
    Set.fromList
        [ WarningName
    UnknownFixityInMixfixDecl_
        , WarningName
    ShadowingInTelescope_
        ]

    -- | Warnings enabled by @--exact-split@.
    --
    exactSplitWarnings :: Set WarningName
    exactSplitWarnings :: Set WarningName
    exactSplitWarnings = [WarningName] -> Set WarningName
    forall a. Ord a => [a] -> Set a
    Set.fromList
      [ WarningName
    CoverageNoExactSplit_
      , WarningName
    InlineNoExactSplit_
      ]

    -- | The @WarningName@ data enumeration is meant to have a one-to-one correspondance
    -- to existing warnings in the codebase.

    data WarningName
      -- Option Warnings
      = OptionRenamed_
      | WarningProblem_
          -- ^ Some warning could not be set or unset.
      -- Parser Warnings
      | OverlappingTokensWarning_
      | MisplacedAttributes_
      | UnknownPolarity_
      | UnknownAttribute_
      | UnsupportedAttribute_
      | MultipleAttributes_
      -- Library Warnings
      | LibUnknownField_
      -- Nicifer Warnings
      | EmptyAbstract_
      | EmptyConstructor_
      | EmptyField_
      | EmptyGeneralize_
      | EmptyInstance_
      | EmptyMacro_
      | EmptyMutual_
      | EmptyPostulate_
      | EmptyPrimitive_
      | EmptyPrivate_
      | EmptyRewritePragma_
      | EmptyWhere_
      | EmptyPolarityPragma_
      | HiddenGeneralize_
      | InvalidCatchallPragma_
      | InvalidConstructorBlock_
      | InvalidCoverageCheckPragma_
      | InvalidNoPositivityCheckPragma_
      | InvalidNoUniverseCheckPragma_
      | DuplicateRecordDirective_
      | InvalidTerminationCheckPragma_
      | MissingDataDeclaration_
      | MissingDefinitions_
      | NotAllowedInMutual_
      | OpenImportAbstract_
      | OpenImportPrivate_
      | PolarityPragmasButNotPostulates_
      | PragmaCompiled_
      | PragmaNoTerminationCheck_
      | ShadowingInTelescope_
      | UnknownFixityInMixfixDecl_
      | UnknownNamesInFixityDecl_
      | UnknownNamesInPolarityPragmas_
      | UselessAbstract_
      | UselessInstance_
      | UselessMacro_
      | UselessPrivate_
      -- Scope and Type Checking Warnings
      | AbsurdPatternRequiresAbsentRHS_
      | AsPatternShadowsConstructorOrPatternSynonym_
      | PatternShadowsConstructor_
      | CantGeneralizeOverSorts_
      | ClashesViaRenaming_                -- issue #4154
      | CoverageIssue_
      | CoverageNoExactSplit_
      | InlineNoExactSplit_
      | DeprecationWarning_
      | DuplicateUsing_
      | FixingCohesion_
      | FixingPolarity_
      | FixingRelevance_
      -- TODO: linearity
      -- -- | FixingQuantity_
      | FixityInRenamingModule_
      | InvalidCharacterLiteral_
      | UselessPragma_
      | IllformedAsClause_
      | InstanceArgWithExplicitArg_
      | InstanceWithExplicitArg_
      | InstanceNoOutputTypeName_
      | InteractionMetaBoundaries_
      | InversionDepthReached_
      | ModuleDoesntExport_
      | NotInScope_
      | NotStrictlyPositive_
      | ConstructorDoesNotFitInData_
      | CoinductiveEtaRecord_
      | UnsupportedIndexedMatch_
      | OldBuiltin_
      | BuiltinDeclaresIdentifier_
      | PlentyInHardCompileTimeMode_
      | PragmaCompileErased_
      | PragmaCompileList_
      | PragmaCompileMaybe_
      | PragmaCompileUnparsable_
      | PragmaCompileWrong_
      | PragmaCompileWrongName_
      | PragmaExpectsDefinedSymbol_
      | PragmaExpectsUnambiguousConstructorOrFunction_
      | PragmaExpectsUnambiguousProjectionOrFunction_
      | NoMain_
      | NotARewriteRule_
      | RewriteLHSNotDefinitionOrConstructor_
      | RewriteVariablesNotBoundByLHS_
      | RewriteVariablesBoundMoreThanOnce_
      | RewriteLHSReduces_
      | RewriteHeadSymbolIsProjectionLikeFunction_
      | RewriteHeadSymbolIsTypeConstructor_
      | RewriteHeadSymbolContainsMetas_
      | RewriteConstructorParametersNotGeneral_
      | RewriteContainsUnsolvedMetaVariables_
      | RewriteBlockedOnProblems_
      | RewriteRequiresDefinitions_
      | RewriteDoesNotTargetRewriteRelation_
      | RewriteBeforeFunctionDefinition_
      | RewriteBeforeMutualFunctionDefinition_
      | ConfluenceCheckingIncompleteBecauseOfMeta_
      | ConfluenceForCubicalNotSupported_
      | RewriteMaybeNonConfluent_
      | RewriteNonConfluent_
      | RewriteAmbiguousRules_
      | RewriteMissingRule_
      | DuplicateRewriteRule_
      | SafeFlagEta_
      | SafeFlagInjective_
      | SafeFlagNoCoverageCheck_
      | SafeFlagNonTerminating_
      | SafeFlagNoPositivityCheck_
      | SafeFlagNoUniverseCheck_
      | SafeFlagPolarity_
      | SafeFlagPostulate_
      | SafeFlagPragma_
      | SafeFlagTerminating_
      | SafeFlagWithoutKFlagPrimEraseEquality_
      | TerminationIssue_
      | TooManyArgumentsToSort_
      | UnreachableClauses_
      | UnsolvedConstraints_
      | UnsolvedInteractionMetas_
      | UnsolvedMetaVariables_
      | UselessHiding_
      | UselessInline_
      | UselessPatternDeclarationForRecord_
      | UselessPublic_
      | UselessTactic_
      | UserWarning_
      | InvalidDisplayForm_
      | UnusedVariablesInDisplayForm_
      | RewritesNothing_
      | WithClauseProjectionFixityMismatch_
      | WithoutKFlagPrimEraseEquality_
      | ConflictingPragmaOptions_
      | WrongInstanceDeclaration_
      | TooManyPolarities_
      | TopLevelPolarity_
      -- Checking consistency of options
      | CoInfectiveImport_
      | InfectiveImport_
      -- Record field warnings
      | DuplicateFields_
      | TooManyFields_
      -- Opaque/unfolding
      | MissingTypeSignatureForOpaque_
      | NotAffectedByOpaque_
      | UnfoldingWrongName_
      | UnfoldTransparentName_
      | UselessOpaque_
      -- Recoverable scope checking errors
      | HiddenNotInArgumentPosition_
      | InstanceNotInArgumentPosition_
      | MacroInLetBindings_
      | AbstractInLetBindings_
      -- Cubical
      | FaceConstraintCannotBeHidden_
      | FaceConstraintCannotBeNamed_
      -- Backends
      | CustomBackendWarning_
      deriving (WarningName -> WarningName -> Bool
    (WarningName -> WarningName -> Bool)
    -> (WarningName -> WarningName -> Bool) -> Eq WarningName
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: WarningName -> WarningName -> Bool
    == :: WarningName -> WarningName -> Bool
    $c/= :: WarningName -> WarningName -> Bool
    /= :: WarningName -> WarningName -> Bool
    Eq, Eq WarningName
    Eq WarningName =>
    (WarningName -> WarningName -> Ordering)
    -> (WarningName -> WarningName -> Bool)
    -> (WarningName -> WarningName -> Bool)
    -> (WarningName -> WarningName -> Bool)
    -> (WarningName -> WarningName -> Bool)
    -> (WarningName -> WarningName -> WarningName)
    -> (WarningName -> WarningName -> WarningName)
    -> Ord WarningName
    WarningName -> WarningName -> Bool
    WarningName -> WarningName -> Ordering
    WarningName -> WarningName -> WarningName
    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 :: WarningName -> WarningName -> Ordering
    compare :: WarningName -> WarningName -> Ordering
    $c< :: WarningName -> WarningName -> Bool
    < :: WarningName -> WarningName -> Bool
    $c<= :: WarningName -> WarningName -> Bool
    <= :: WarningName -> WarningName -> Bool
    $c> :: WarningName -> WarningName -> Bool
    > :: WarningName -> WarningName -> Bool
    $c>= :: WarningName -> WarningName -> Bool
    >= :: WarningName -> WarningName -> Bool
    $cmax :: WarningName -> WarningName -> WarningName
    max :: WarningName -> WarningName -> WarningName
    $cmin :: WarningName -> WarningName -> WarningName
    min :: WarningName -> WarningName -> WarningName
    Ord, Int -> WarningName -> ShowS
    [WarningName] -> ShowS
    WarningName -> String
    (Int -> WarningName -> ShowS)
    -> (WarningName -> String)
    -> ([WarningName] -> ShowS)
    -> Show WarningName
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> WarningName -> ShowS
    showsPrec :: Int -> WarningName -> ShowS
    $cshow :: WarningName -> String
    show :: WarningName -> String
    $cshowList :: [WarningName] -> ShowS
    showList :: [WarningName] -> ShowS
    Show, ReadPrec [WarningName]
    ReadPrec WarningName
    Int -> ReadS WarningName
    ReadS [WarningName]
    (Int -> ReadS WarningName)
    -> ReadS [WarningName]
    -> ReadPrec WarningName
    -> ReadPrec [WarningName]
    -> Read WarningName
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: Int -> ReadS WarningName
    readsPrec :: Int -> ReadS WarningName
    $creadList :: ReadS [WarningName]
    readList :: ReadS [WarningName]
    $creadPrec :: ReadPrec WarningName
    readPrec :: ReadPrec WarningName
    $creadListPrec :: ReadPrec [WarningName]
    readListPrec :: ReadPrec [WarningName]
    Read, Int -> WarningName
    WarningName -> Int
    WarningName -> [WarningName]
    WarningName -> WarningName
    WarningName -> WarningName -> [WarningName]
    WarningName -> WarningName -> WarningName -> [WarningName]
    (WarningName -> WarningName)
    -> (WarningName -> WarningName)
    -> (Int -> WarningName)
    -> (WarningName -> Int)
    -> (WarningName -> [WarningName])
    -> (WarningName -> WarningName -> [WarningName])
    -> (WarningName -> WarningName -> [WarningName])
    -> (WarningName -> WarningName -> WarningName -> [WarningName])
    -> Enum WarningName
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: WarningName -> WarningName
    succ :: WarningName -> WarningName
    $cpred :: WarningName -> WarningName
    pred :: WarningName -> WarningName
    $ctoEnum :: Int -> WarningName
    toEnum :: Int -> WarningName
    $cfromEnum :: WarningName -> Int
    fromEnum :: WarningName -> Int
    $cenumFrom :: WarningName -> [WarningName]
    enumFrom :: WarningName -> [WarningName]
    $cenumFromThen :: WarningName -> WarningName -> [WarningName]
    enumFromThen :: WarningName -> WarningName -> [WarningName]
    $cenumFromTo :: WarningName -> WarningName -> [WarningName]
    enumFromTo :: WarningName -> WarningName -> [WarningName]
    $cenumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName]
    enumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName]
    Enum, WarningName
    WarningName -> WarningName -> Bounded WarningName
    forall a. a -> a -> Bounded a
    $cminBound :: WarningName
    minBound :: WarningName
    $cmaxBound :: WarningName
    maxBound :: WarningName
    Bounded, (forall x. WarningName -> Rep WarningName x)
    -> (forall x. Rep WarningName x -> WarningName)
    -> Generic WarningName
    forall x. Rep WarningName x -> WarningName
    forall x. WarningName -> Rep WarningName x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. WarningName -> Rep WarningName x
    from :: forall x. WarningName -> Rep WarningName x
    $cto :: forall x. Rep WarningName x -> WarningName
    to :: forall x. Rep WarningName x -> WarningName
    Generic)

    instance NFData WarningName

    -- | The flag corresponding to a warning is precisely the name of the constructor
    -- minus the trailing underscore.

    string2WarningName :: String -> Maybe WarningName
    string2WarningName :: String -> Maybe WarningName
    string2WarningName = (String -> HashMap String WarningName -> Maybe WarningName
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    `HMap.lookup` HashMap String WarningName
    warnings) where
      warnings :: HashMap String WarningName
    warnings = [(String, WarningName)] -> HashMap String WarningName
    forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
    HMap.fromList ([(String, WarningName)] -> HashMap String WarningName)
    -> [(String, WarningName)] -> HashMap String WarningName
    forall a b. (a -> b) -> a -> b
    $ (WarningName -> (String, WarningName))
    -> [WarningName] -> [(String, WarningName)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\WarningName
    x -> (WarningName -> String
    warningName2String WarningName
    x, WarningName
    x)) [WarningName
    forall a. Bounded a => a
    minBound..WarningName
    forall a. Bounded a => a
    maxBound]

    warningName2String :: WarningName -> String
    warningName2String :: WarningName -> String
    warningName2String = String -> ShowS
    forall a. [a] -> [a] -> [a]
    initWithDefault String
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ShowS -> (WarningName -> String) -> WarningName -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WarningName -> String
    forall a. Show a => a -> String
    show

    -- | @warningUsage@ generated using @warningNameDescription@

    usageWarning :: String
    usageWarning :: String
    usageWarning = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n"
      [ String
    "The -W or --warning option can be used to disable or enable\
        \ different warnings. The flag -W error (or --warning=error)\
        \ can be used to turn all warnings into errors, while -W noerror\
        \ turns this off again."
      , String
    ""
      , String
    "A group of warnings can be enabled by -W group, where group is\
        \ one of the following:"
      , String
    ""
      , [(String, String)] -> String
    untable (((String, (Set WarningName, String)) -> (String, String))
    -> [(String, (Set WarningName, String))] -> [(String, String)]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((String, (Set WarningName, String)) -> String
    forall a b. (a, b) -> a
    fst ((String, (Set WarningName, String)) -> String)
    -> ((String, (Set WarningName, String)) -> String)
    -> (String, (Set WarningName, String))
    -> (String, String)
    forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
    forall (a :: * -> * -> *) b c c'.
    Arrow a =>
    a b c -> a b c' -> a b (c, c')
    &&& (Set WarningName, String) -> String
    forall a b. (a, b) -> b
    snd ((Set WarningName, String) -> String)
    -> ((String, (Set WarningName, String))
        -> (Set WarningName, String))
    -> (String, (Set WarningName, String))
    -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String, (Set WarningName, String)) -> (Set WarningName, String)
    forall a b. (a, b) -> b
    snd) [(String, (Set WarningName, String))]
    warningSets)

      , String
    "Individual benign warnings can be turned on and off by -W Name and\
        \ -W noName, respectively, where Name comes from the following\
        \ list (warnings marked with 'd' are turned on by default):"
      , String
    ""
      , Bool -> [WarningName] -> String
    forall {b}. IsBool b => b -> [WarningName] -> String
    warningTable Bool
    True [WarningName]
    benign

      , String
    "Error warnings are always on and cannot be turned off:"
      , String
    ""
      , Bool -> [WarningName] -> String
    forall {b}. IsBool b => b -> [WarningName] -> String
    warningTable Bool
    False [WarningName]
    severe
      ]

      where

        ([WarningName]
    severe, [WarningName]
    benign) = (WarningName -> Bool)
    -> [WarningName] -> ([WarningName], [WarningName])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (WarningName -> Set WarningName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set WarningName
    errorWarnings) [WarningName
    forall a. Bounded a => a
    minBound..WarningName
    forall a. Bounded a => a
    maxBound]

        warningTable :: b -> [WarningName] -> String
    warningTable b
    printD [WarningName]
    ws =
          [(String, String)] -> String
    untable ([(String, String)] -> String) -> [(String, String)] -> String
    forall a b. (a -> b) -> a -> b
    $ [WarningName]
    -> (WarningName -> Maybe (String, String)) -> [(String, String)]
    forall a b. [a] -> (a -> Maybe b) -> [b]
    forMaybe [WarningName]
    ws ((WarningName -> Maybe (String, String)) -> [(String, String)])
    -> (WarningName -> Maybe (String, String)) -> [(String, String)]
    forall a b. (a -> b) -> a -> b
    $ \ WarningName
    w ->
            let wnd :: String
    wnd = WarningName -> String
    warningNameDescription WarningName
    w in
            ( WarningName -> String
    warningName2String WarningName
    w
            , b -> ShowS -> ShowS
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen b
    printD ((if WarningName
    w WarningName -> Set WarningName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set WarningName
    usualWarnings then String
    "d" else String
    " ") String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++)
              String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
              String
    wnd
            ) (String, String) -> Maybe () -> Maybe (String, String)
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    wnd)

        untable :: [(String, String)] -> String
        untable :: [(String, String)] -> String
    untable [(String, String)]
    rows =
          let len :: Int
    len = [Int] -> Int
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum (((String, String) -> Int) -> [(String, String)] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (String -> Int)
    -> ((String, String) -> String) -> (String, String) -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String, String) -> String
    forall a b. (a, b) -> a
    fst) [(String, String)]
    rows) in
          [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [(String, String)] -> ((String, String) -> String) -> [String]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for ([(String, String)] -> [(String, String)]
    forall a. Ord a => [a] -> [a]
    sort [(String, String)]
    rows) (((String, String) -> String) -> [String])
    -> ((String, String) -> String) -> [String]
    forall a b. (a -> b) -> a -> b
    $ \ (String
    hdr, String
    cnt) ->
            [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [ String
    hdr, Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    hdr) Char
    ' ', String
    cnt ]

    -- | @WarningName@ descriptions used for generating usage information
    -- Leave String empty to skip that name.
    --
    -- The description should be a completion of the sentence "This warning is about ...".
    -- So, typically the subject is in plural.
    --
    warningNameDescription :: WarningName -> String
    warningNameDescription :: WarningName -> String
    warningNameDescription = \case
      -- Option Warnings
      WarningName
    OptionRenamed_                   -> String
    "Renamed options."
      WarningName
    WarningProblem_                  -> String
    "Problems with switching warnings."
      -- Parser Warnings
      WarningName
    OverlappingTokensWarning_        -> String
    "Multi-line comments spanning one or more literate text blocks."
      WarningName
    MisplacedAttributes_             -> String
    "Attributes where they are not supported."
      WarningName
    UnknownPolarity_                 -> String
    "Unknown polarities."
      WarningName
    UnknownAttribute_                -> String
    "Unknown attributes."
      WarningName
    UnsupportedAttribute_            -> String
    "Unsupported attributes."
      WarningName
    MultipleAttributes_              -> String
    "Multiple attributes."
      -- Library Warnings
      WarningName
    LibUnknownField_                 -> String
    "Unknown fields in library files."
      -- Nicifer Warnings
      WarningName
    EmptyAbstract_                   -> String
    "Empty `abstract' blocks."
      WarningName
    EmptyConstructor_                -> String
    "Empty `constructor' blocks."
      WarningName
    EmptyField_                      -> String
    "Empty `field` blocks."
      WarningName
    EmptyGeneralize_                 -> String
    "Empty `variable' blocks."
      WarningName
    EmptyInstance_                   -> String
    "Empty `instance' blocks."
      WarningName
    EmptyMacro_                      -> String
    "Empty `macro' blocks."
      WarningName
    EmptyMutual_                     -> String
    "Empty `mutual' blocks."
      WarningName
    EmptyPostulate_                  -> String
    "Empty `postulate' blocks."
      WarningName
    EmptyPrimitive_                  -> String
    "Empty `primitive' blocks."
      WarningName
    EmptyPrivate_                    -> String
    "Empty `private' blocks."
      WarningName
    EmptyRewritePragma_              -> String
    "Empty `REWRITE' pragmas."
      WarningName
    EmptyWhere_                      -> String
    "Empty `where' blocks."
      WarningName
    EmptyPolarityPragma_             -> String
    "`POLARITY' pragmas giving no polarities."
      WarningName
    HiddenGeneralize_                -> String
    "Hidden identifiers in variable blocks."
      WarningName
    InvalidCatchallPragma_           -> String
    "`CATCHALL' pragmas before a non-function clause."
      WarningName
    InvalidConstructorBlock_         -> String
    "`constructor' blocks outside of `interleaved mutual' blocks."
      WarningName
    InvalidCoverageCheckPragma_      -> String
    "Coverage checking pragmas before non-function or `mutual' blocks."
      WarningName
    InvalidNoPositivityCheckPragma_  -> String
    "Positivity checking pragmas before non-`data', `record' or `mutual' blocks."
      WarningName
    InvalidNoUniverseCheckPragma_    -> String
    "Universe checking pragmas before non-`data' or `record' declaration."
      WarningName
    DuplicateRecordDirective_        -> String
    "Conflicting directives in a record declaration."
      WarningName
    InvalidTerminationCheckPragma_   -> String
    "Termination checking pragmas before non-function or `mutual' blocks."
      WarningName
    MissingDataDeclaration_          -> String
    "Constructor definitions not associated to a data declaration."
      WarningName
    MissingDefinitions_              -> String
    "Declarations not associated to a definition."
      WarningName
    NotAllowedInMutual_              -> String
    "Declarations not allowed in a mutual block."
      WarningName
    OpenImportAbstract_              -> String
    "`open' or `import' statements in 'abstract' blocks."
      WarningName
    OpenImportPrivate_               -> String
    "`open' or `import' statements in 'private' blocks."
      WarningName
    PolarityPragmasButNotPostulates_ -> String
    "Polarity pragmas for non-postulates."
      WarningName
    PragmaCompiled_                  -> String
    "'COMPILE' pragmas in safe mode."
      WarningName
    PragmaNoTerminationCheck_        -> String
    "`NO_TERMINATION_CHECK' pragmas; such are deprecated."
      WarningName
    ShadowingInTelescope_            -> String
    "Repeated variable names in telescopes."
      WarningName
    UnknownFixityInMixfixDecl_       -> String
    "Mixfix names without an associated fixity declaration."
      WarningName
    UnknownNamesInFixityDecl_        -> String
    "Names not declared in the same scope as their syntax or fixity declaration."
      WarningName
    UnknownNamesInPolarityPragmas_   -> String
    "Names not declared in the same scope as their polarity pragmas."
      WarningName
    UselessAbstract_                 -> String
    "`abstract' blocks where they have no effect."
      WarningName
    UselessHiding_                   -> String
    "Names in `hiding' directive that are anyway not imported."
      WarningName
    UselessInline_                   -> String
    "`INLINE' pragmas where they have no effect."
      WarningName
    UselessInstance_                 -> String
    "`instance' blocks where they have no effect."
      WarningName
    UselessMacro_                    -> String
    "`macro' blocks where they have no effect."
      WarningName
    UselessPrivate_                  -> String
    "`private' blocks where they have no effect."
      WarningName
    UselessPublic_                   -> String
    "`public' directives that have no effect."
      WarningName
    UselessPatternDeclarationForRecord_ -> String
    "`pattern' attributes where they have no effect."
      WarningName
    UselessTactic_                   -> String
    "`@tactic` attributes where they have no effect."
      -- Scope and Type Checking Warnings
      WarningName
    AbsurdPatternRequiresAbsentRHS_  -> String
    "Clauses with an absurd pattern that have a right hand side."
      WarningName
    AsPatternShadowsConstructorOrPatternSynonym_ -> String
    "@-patterns that shadow constructors or pattern synonyms."
      WarningName
    PatternShadowsConstructor_       -> String
    "Pattern variables that shadow constructors."
      WarningName
    CantGeneralizeOverSorts_         -> String
    "Attempts to generalize over sort metas in 'variable' declaration."
      WarningName
    ClashesViaRenaming_              -> String
    "Clashes introduced by `renaming'."  -- issue #4154
      WarningName
    CoverageIssue_                   -> String
    "Failed coverage checks."
      WarningName
    CoverageNoExactSplit_            -> String
    "Failed exact split checks."
      WarningName
    InlineNoExactSplit_              -> String
    "Failed exact split checks after inlining record constructors."
      WarningName
    DeprecationWarning_              -> String
    "Deprecated features."
      -- TODO: linearity
      -- FixingQuantity_                  -> "Correcting invalid user-written quantity."
      WarningName
    FixingRelevance_                 -> String
    "Correcting invalid user-written relevance attribute."
      WarningName
    FixingCohesion_                  -> String
    "Correcting invalid user-written cohesion attribute."
      WarningName
    FixingPolarity_                  -> String
    "Correcting invalid user-written polarity attribute."
      WarningName
    InvalidCharacterLiteral_         -> String
    "Illegal character literals."
      WarningName
    UselessPragma_                   -> String
    "Pragmas that get ignored."
      WarningName
    IllformedAsClause_               -> String
    "Illformed `as'-clauses in `import' statements."
      WarningName
    InstanceNoOutputTypeName_        -> String
    "Instance arguments whose type does not end in a named or variable type; those are never considered by instance search."
      WarningName
    InstanceArgWithExplicitArg_      -> String
    "Instance arguments with explicit arguments; those are never considered by instance search."
      WarningName
    InstanceWithExplicitArg_         -> String
    "`instance` declarations with explicit arguments; those are never considered by instance search."
      WarningName
    InversionDepthReached_           -> String
    "Inversions of pattern-matching failures due to exhausted inversion depth."
      WarningName
    ModuleDoesntExport_              -> String
    "Imported names that are not actually exported."
      WarningName
    DuplicateUsing_                  -> String
    "Repeated names in using directive."
      WarningName
    FixityInRenamingModule_          -> String
    "Fixity annotations in `renaming' directive for `module'."
      WarningName
    NotInScope_                      -> String
    "Out of scope names."
      WarningName
    NotStrictlyPositive_             -> String
    "Failed strict positivity checks."
      WarningName
    ConstructorDoesNotFitInData_     -> String
    "Failed constructor size checks."
      WarningName
    CoinductiveEtaRecord_            -> String
    "Record type declared as both coinductive and having eta-equality."
      WarningName
    UnsupportedIndexedMatch_         -> String
    "Failures to compute full equivalence when splitting on indexed family."
      WarningName
    OldBuiltin_                      -> String
    "Deprecated `BUILTIN' pragmas."
      WarningName
    BuiltinDeclaresIdentifier_       -> String
    "`BUILTIN' pragmas that declare a new identifier but have been given an existing one."
      WarningName
    PlentyInHardCompileTimeMode_     -> String
    "Uses of @ω or @plenty in hard compile-time mode."
      WarningName
    PragmaCompileErased_             -> String
    "`COMPILE' pragmas targeting an erased symbol."
      WarningName
    PragmaCompileList_               -> String
    "`COMPILE GHC' pragmas for lists."
      WarningName
    PragmaCompileMaybe_              -> String
    "`COMPILE GHC' pragmas for `MAYBE'."
      WarningName
    PragmaCompileUnparsable_         -> String
    "Unparsable `COMPILE GHC' pragmas."
      WarningName
    PragmaCompileWrong_              -> String
    "Ill-formed `COMPILE GHC' pragmas."
      WarningName
    PragmaCompileWrongName_          -> String
    "`COMPILE' pragmas referring to identifiers that are neither definitions nor constructors.'"
      WarningName
    PragmaExpectsDefinedSymbol_      -> String
    "Pragmas referrings to identifiers that are not defined symbols."
      WarningName
    PragmaExpectsUnambiguousConstructorOrFunction_    -> String
    "Pragmas referring to identifiers that are not unambiguous constructors or functions.'"
      WarningName
    PragmaExpectsUnambiguousProjectionOrFunction_     -> String
    "Pragmas referring to identifiers that are not unambiguous projections or functions.'"
      WarningName
    NoMain_                          -> String
    "Compilation of modules that do not define `main'."
      WarningName
    NotARewriteRule_                 -> String
    "`REWRITE pragmas referring to identifiers that are neither definitions nor constructors.'"
      WarningName
    RewriteLHSNotDefinitionOrConstructor_             -> String
    "Rewrite rule head symbol is not a defined symbol or constructor."
      WarningName
    RewriteVariablesNotBoundByLHS_                    -> String
    "Rewrite rule does not bind all of its variables."
      WarningName
    RewriteVariablesBoundMoreThanOnce_                -> String
    "Constructor-headed rewrite rule has non-linear parameters."
      WarningName
    RewriteLHSReduces_                                -> String
    "Rewrite rule LHS is not in weak-head normal form."
      WarningName
    RewriteHeadSymbolIsProjectionLikeFunction_        -> String
    "Rewrite rule head symbol is a projection-like function."
      WarningName
    RewriteHeadSymbolIsTypeConstructor_               -> String
    "Rewrite rule head symbol is a type constructor."
      WarningName
    RewriteHeadSymbolContainsMetas_                   -> String
    "Definition of rewrite rule head symbol contains unsolved metas."
      WarningName
    RewriteConstructorParametersNotGeneral_           -> String
    "Constructor-headed rewrite rule parameters are not fully general."
      WarningName
    RewriteContainsUnsolvedMetaVariables_             -> String
    "Rewrite rule contains unsolved metas."
      WarningName
    RewriteBlockedOnProblems_                         -> String
    "Checking rewrite rule blocked by unsolved constraint."
      WarningName
    RewriteRequiresDefinitions_                       -> String
    "Checking rewrite rule blocked by missing definition."
      WarningName
    RewriteDoesNotTargetRewriteRelation_              -> String
    "Rewrite rule does not target the rewrite relation."
      WarningName
    RewriteBeforeFunctionDefinition_                  -> String
    "Rewrite rule is not yet defined."
      WarningName
    RewriteBeforeMutualFunctionDefinition_            -> String
    "Mutually declaration with the rewrite rule is not yet defined."
      WarningName
    ConfluenceCheckingIncompleteBecauseOfMeta_ -> String
    "Incomplete confluence checks because of unsolved metas."
      WarningName
    ConfluenceForCubicalNotSupported_ -> String
    "Incomplete confluence checks because of `--cubical'."
      WarningName
    RewriteMaybeNonConfluent_        -> String
    "Failed local confluence checks while computing overlap."
      WarningName
    RewriteNonConfluent_             -> String
    "Failed local confluence checks while joining critical pairs."
      WarningName
    RewriteAmbiguousRules_           -> String
    "Failed global confluence checks because of overlapping rules."
      WarningName
    RewriteMissingRule_              -> String
    "Failed global confluence checks because of missing rule."
      WarningName
    DuplicateRewriteRule_            -> String
    "Duplicate rewrite rules."
      WarningName
    SafeFlagEta_                     -> String
    "`ETA' pragmas with the safe flag."
      WarningName
    SafeFlagInjective_               -> String
    "`INJECTIVE' pragmas with the safe flag."
      WarningName
    SafeFlagNoCoverageCheck_         -> String
    "`NON_COVERING` pragmas with the safe flag."
      WarningName
    SafeFlagNonTerminating_          -> String
    "`NON_TERMINATING' pragmas with the safe flag."
      WarningName
    SafeFlagNoPositivityCheck_       -> String
    "`NO_POSITIVITY_CHECK' pragmas with the safe flag."
      WarningName
    SafeFlagNoUniverseCheck_         -> String
    "`NO_UNIVERSE_CHECK' pragmas with the safe flag."
      WarningName
    SafeFlagPolarity_                -> String
    "`POLARITY' pragmas with the safe flag."
      WarningName
    SafeFlagPostulate_               -> String
    "`postulate' blocks with the safe flag."
      WarningName
    SafeFlagPragma_                  -> String
    "Unsafe `OPTIONS' pragmas with the safe flag."
      WarningName
    SafeFlagTerminating_             -> String
    "`TERMINATING' pragmas with the safe flag."
      WarningName
    SafeFlagWithoutKFlagPrimEraseEquality_ -> String
    "`primEraseEquality' used with the safe and without-K flags."
      WarningName
    ConflictingPragmaOptions_        -> String
    "Conflicting pragma options."
      WarningName
    TerminationIssue_                -> String
    "Failed termination checks."
      WarningName
    UnreachableClauses_              -> String
    "Unreachable function clauses."
      WarningName
    UnsolvedConstraints_             -> String
    "Unsolved constraints."
      WarningName
    UnsolvedInteractionMetas_        -> String
    "Unsolved interaction meta variables."
      WarningName
    InteractionMetaBoundaries_       -> String
    "Interaction meta variables that have unsolved boundary constraints."
      WarningName
    UnsolvedMetaVariables_           -> String
    "Unsolved meta variables."
      WarningName
    UserWarning_                     -> String
    "User-defined warnings via one of the 'WARNING_ON_*' pragmas."
      WarningName
    InvalidDisplayForm_              -> String
    "Invalid display forms."
      WarningName
    UnusedVariablesInDisplayForm_    -> String
    "Bound but unused variables in display forms."
      WarningName
    TooManyArgumentsToSort_          -> String
    "Extra arguments given to a sort."
      WarningName
    RewritesNothing_                 -> String
    "`rewrite' clauses that do not fire."
      WarningName
    WithClauseProjectionFixityMismatch_ -> String
    "With clauses using projections in different fixities than their parent clauses."
      WarningName
    WithoutKFlagPrimEraseEquality_   -> String
    "Uses of `primEraseEquality' with the without-K flags."
      WarningName
    WrongInstanceDeclaration_        -> String
    "Instances that do not adhere to the required format."
      WarningName
    TooManyPolarities_               -> String
    "Too many polarities given in POLARITY pragma."
      WarningName
    TopLevelPolarity_                -> String
    "Declaring definitions with an explicit polarity annotation."
      -- Checking consistency of options
      WarningName
    CoInfectiveImport_               -> String
    "Importing a file not using e.g. `--safe'  from one which does."
      WarningName
    InfectiveImport_                 -> String
    "Importing a file using e.g. `--cubical' into one which does not."
      -- Record field warnings
      WarningName
    DuplicateFields_                 -> String
    "Record expressions with duplicate field names."
      WarningName
    TooManyFields_                   -> String
    "Record expressions with invalid field names."
      -- Opaque/unfolding warnings
      WarningName
    MissingTypeSignatureForOpaque_   -> String
    "Definitions that are `abstract` or `opaque` yet lack type signatures."
      WarningName
    NotAffectedByOpaque_             -> String
    "Declarations unaffected by enclosing `opaque` blocks."
      WarningName
    UnfoldingWrongName_              -> String
    "Names in `unfolding` clause that are not unambiguous functions."
      WarningName
    UnfoldTransparentName_           -> String
    "Non-`opaque` names mentioned in an `unfolding` clause."
      WarningName
    UselessOpaque_                   -> String
    "`opaque` blocks that have no effect."

      -- Recoverable scope-checking errors
      WarningName
    HiddenNotInArgumentPosition_     -> String
    "Hidden argument with no matching function."
      WarningName
    InstanceNotInArgumentPosition_   -> String
    "Instance argument with no matching function."
      WarningName
    MacroInLetBindings_              -> String
    "Macros can not be let-bound."
      WarningName
    AbstractInLetBindings_           -> String
    "Let bindings can not contain abstract declarations."

      -- Cubical
      WarningName
    FaceConstraintCannotBeHidden_    -> String
    "Face constraint patterns that are given as implicit arguments."
      WarningName
    FaceConstraintCannotBeNamed_     -> String
    "Face constraint patterns that are given as named arguments."
      -- Backends
      WarningName
    CustomBackendWarning_            -> String
    "Custom warnings from backends."