Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.Options.Warnings

Synopsis

Documentation

data WarningMode Source #

A WarningMode has two components: a set of warnings to be displayed and a flag stating whether warnings should be turned into fatal errors.

Constructors

WarningMode 

Fields

Instances

Instances details
EmbPrj WarningMode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningMode -> S Int32 Source #

icod_ :: WarningMode -> S Int32 Source #

value :: Int32 -> R WarningMode Source #

NFData WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

rnf :: WarningMode -> ()

Generic WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Associated Types

type Rep WarningMode 
Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "WarningMode" 'PrefixI 'True) (S1 ('MetaSel ('Just "_warningSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set WarningName)) :*: S1 ('MetaSel ('Just "_warn2Error") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

Methods

from :: WarningMode -> Rep WarningMode x

to :: Rep WarningMode x -> WarningMode

Show WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

showsPrec :: Int -> WarningMode -> ShowS

show :: WarningMode -> String

showList :: [WarningMode] -> ShowS

Eq WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

(==) :: WarningMode -> WarningMode -> Bool

(/=) :: WarningMode -> WarningMode -> Bool

type Rep WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "WarningMode" 'PrefixI 'True) (S1 ('MetaSel ('Just "_warningSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set WarningName)) :*: S1 ('MetaSel ('Just "_warn2Error") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

defaultWarningSet :: String Source #

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

exactSplitWarnings :: Set WarningName Source #

Warnings enabled by --exact-split.

data WarningModeError Source #

Some warnings are errors and cannot be turned off.

Constructors

Unknown Text

Unknown warning.

NoNoError Text

Warning that cannot be disabled.

Instances

Instances details
EmbPrj WarningModeError Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

NFData WarningModeError Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

rnf :: WarningModeError -> ()

Generic WarningModeError Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Associated Types

type Rep WarningModeError 
Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningModeError = D1 ('MetaData "WarningModeError" "Agda.Interaction.Options.Warnings" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Unknown" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "NoNoError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))
Show WarningModeError Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

showsPrec :: Int -> WarningModeError -> ShowS

show :: WarningModeError -> String

showList :: [WarningModeError] -> ShowS

type Rep WarningModeError Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningModeError = D1 ('MetaData "WarningModeError" "Agda.Interaction.Options.Warnings" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Unknown" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "NoNoError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate Source #

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

warningSets :: [(String, (Set WarningName, String))] Source #

Common sets of warnings

data WarningName Source #

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

Constructors

OptionRenamed_ 
WarningProblem_

Some warning could not be set or unset. Parser Warnings

OverlappingTokensWarning_ 
UnsupportedAttribute_ 
MultipleAttributes_ 
LibUnknownField_ 
EmptyAbstract_ 
EmptyConstructor_ 
EmptyField_ 
EmptyGeneralize_ 
EmptyInstance_ 
EmptyMacro_ 
EmptyMutual_ 
EmptyPostulate_ 
EmptyPrimitive_ 
EmptyPrivate_ 
EmptyRewritePragma_ 
EmptyWhere_ 
HiddenGeneralize_ 
InvalidCatchallPragma_ 
InvalidConstructor_ 
InvalidConstructorBlock_ 
InvalidCoverageCheckPragma_ 
InvalidNoPositivityCheckPragma_ 
InvalidNoUniverseCheckPragma_ 
DuplicateRecordDirective_ 
InvalidTerminationCheckPragma_ 
MissingDeclarations_ 
MissingDefinitions_ 
NotAllowedInMutual_ 
OpenPublicAbstract_ 
OpenPublicPrivate_ 
PolarityPragmasButNotPostulates_ 
PragmaCompiled_ 
PragmaNoTerminationCheck_ 
ShadowingInTelescope_ 
UnknownFixityInMixfixDecl_ 
UnknownNamesInFixityDecl_ 
UnknownNamesInPolarityPragmas_ 
UselessAbstract_ 
UselessInstance_ 
UselessMacro_ 
UselessPrivate_ 
AbsurdPatternRequiresNoRHS_ 
AsPatternShadowsConstructorOrPatternSynonym_ 
PatternShadowsConstructor_ 
CantGeneralizeOverSorts_ 
ClashesViaRenaming_ 
CoverageIssue_ 
CoverageNoExactSplit_ 
InlineNoExactSplit_ 
DeprecationWarning_ 
DuplicateUsing_ 
FixityInRenamingModule_ 
InvalidCharacterLiteral_ 
UselessPragma_ 
IllformedAsClause_ 
InstanceArgWithExplicitArg_ 
InstanceWithExplicitArg_ 
InstanceNoOutputTypeName_ 
InteractionMetaBoundaries_ 
InversionDepthReached_ 
ModuleDoesntExport_ 
NoGuardednessFlag_ 
NotInScope_ 
NotStrictlyPositive_ 
ConstructorDoesNotFitInData_ 
CoinductiveEtaRecord_ 
UnsupportedIndexedMatch_ 
OldBuiltin_ 
BuiltinDeclaresIdentifier_ 
PlentyInHardCompileTimeMode_ 
PragmaCompileErased_ 
PragmaCompileList_ 
PragmaCompileMaybe_ 
NoMain_ 
RewriteLHSNotDefinitionOrConstructor_ 
RewriteVariablesNotBoundByLHS_ 
RewriteVariablesBoundMoreThanOnce_ 
RewriteLHSReduces_ 
RewriteHeadSymbolIsProjection_ 
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_ 
UnreachableClauses_ 
UnsolvedConstraints_ 
UnsolvedInteractionMetas_ 
UnsolvedMetaVariables_ 
UselessHiding_ 
UselessInline_ 
UselessPatternDeclarationForRecord_ 
UselessPublic_ 
UserWarning_ 
WithoutKFlagPrimEraseEquality_ 
ConflictingPragmaOptions_ 
WrongInstanceDeclaration_ 
CoInfectiveImport_ 
InfectiveImport_ 
DuplicateFields_ 
TooManyFields_ 
MissingTypeSignatureForOpaque_ 
NotAffectedByOpaque_ 
UnfoldTransparentName_ 
UselessOpaque_ 
FaceConstraintCannotBeHidden_ 
FaceConstraintCannotBeNamed_ 
DuplicateInterfaceFiles_ 
CustomBackendWarning_ 

Instances

Instances details
EmbPrj WarningName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningName -> S Int32 Source #

icod_ :: WarningName -> S Int32 Source #

value :: Int32 -> R WarningName Source #

NFData WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

rnf :: WarningName -> ()

Bounded WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Enum WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Generic WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Associated Types

type Rep WarningName 
Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningName = D1 ('MetaData "WarningName" "Agda.Interaction.Options.Warnings" "Agda-2.6.20240714-inplace" 'False) (((((((C1 ('MetaCons "OptionRenamed_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WarningProblem_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OverlappingTokensWarning_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsupportedAttribute_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "MultipleAttributes_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LibUnknownField_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "EmptyAbstract_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyConstructor_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "EmptyField_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyGeneralize_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "EmptyInstance_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyMacro_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "EmptyMutual_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyPostulate_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "EmptyPrimitive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyPrivate_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: ((((C1 ('MetaCons "EmptyRewritePragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyWhere_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "HiddenGeneralize_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidCatchallPragma_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "InvalidConstructor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidConstructorBlock_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InvalidCoverageCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidNoPositivityCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "InvalidNoUniverseCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DuplicateRecordDirective_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InvalidTerminationCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingDeclarations_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "MissingDefinitions_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotAllowedInMutual_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OpenPublicAbstract_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OpenPublicPrivate_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PolarityPragmasButNotPostulates_" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "PragmaCompiled_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaNoTerminationCheck_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ShadowingInTelescope_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnknownFixityInMixfixDecl_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnknownNamesInFixityDecl_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnknownNamesInPolarityPragmas_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UselessAbstract_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessInstance_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "UselessMacro_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPrivate_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AbsurdPatternRequiresNoRHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsPatternShadowsConstructorOrPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatternShadowsConstructor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CantGeneralizeOverSorts_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ClashesViaRenaming_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CoverageIssue_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoverageNoExactSplit_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "InlineNoExactSplit_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DeprecationWarning_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DuplicateUsing_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FixityInRenamingModule_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "InvalidCharacterLiteral_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPragma_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "IllformedAsClause_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceArgWithExplicitArg_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "InstanceWithExplicitArg_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceNoOutputTypeName_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InteractionMetaBoundaries_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InversionDepthReached_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ModuleDoesntExport_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoGuardednessFlag_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NotInScope_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotStrictlyPositive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConstructorDoesNotFitInData_" 'PrefixI 'False) (U1 :: Type -> Type)))))))) :+: ((((((C1 ('MetaCons "CoinductiveEtaRecord_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsupportedIndexedMatch_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OldBuiltin_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinDeclaresIdentifier_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PlentyInHardCompileTimeMode_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaCompileErased_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PragmaCompileList_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaCompileMaybe_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "NoMain_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteLHSNotDefinitionOrConstructor_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewriteVariablesNotBoundByLHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteVariablesBoundMoreThanOnce_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RewriteLHSReduces_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteHeadSymbolIsProjection_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewriteHeadSymbolIsProjectionLikeFunction_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteHeadSymbolIsTypeConstructor_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: ((((C1 ('MetaCons "RewriteHeadSymbolContainsMetas_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteConstructorParametersNotGeneral_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewriteContainsUnsolvedMetaVariables_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteBlockedOnProblems_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RewriteRequiresDefinitions_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteDoesNotTargetRewriteRelation_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewriteBeforeFunctionDefinition_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteBeforeMutualFunctionDefinition_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "ConfluenceCheckingIncompleteBecauseOfMeta_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConfluenceForCubicalNotSupported_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewriteMaybeNonConfluent_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteNonConfluent_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RewriteAmbiguousRules_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteMissingRule_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DuplicateRewriteRule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SafeFlagEta_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagInjective_" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "SafeFlagNoCoverageCheck_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagNonTerminating_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SafeFlagNoPositivityCheck_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagNoUniverseCheck_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "SafeFlagPolarity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagPostulate_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SafeFlagPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagTerminating_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "SafeFlagWithoutKFlagPrimEraseEquality_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TerminationIssue_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UnreachableClauses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedConstraints_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnsolvedInteractionMetas_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedMetaVariables_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UselessHiding_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UselessInline_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPatternDeclarationForRecord_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "UselessPublic_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UserWarning_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithoutKFlagPrimEraseEquality_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConflictingPragmaOptions_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "WrongInstanceDeclaration_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoInfectiveImport_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InfectiveImport_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DuplicateFields_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "TooManyFields_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingTypeSignatureForOpaque_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NotAffectedByOpaque_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnfoldTransparentName_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UselessOpaque_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FaceConstraintCannotBeHidden_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FaceConstraintCannotBeNamed_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DuplicateInterfaceFiles_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CustomBackendWarning_" 'PrefixI 'False) (U1 :: Type -> Type)))))))))

Methods

from :: WarningName -> Rep WarningName x

to :: Rep WarningName x -> WarningName

Read WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

readsPrec :: Int -> ReadS WarningName

readList :: ReadS [WarningName]

readPrec :: ReadPrec WarningName

readListPrec :: ReadPrec [WarningName]

Show WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

showsPrec :: Int -> WarningName -> ShowS

show :: WarningName -> String

showList :: [WarningName] -> ShowS

Eq WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

(==) :: WarningName -> WarningName -> Bool

(/=) :: WarningName -> WarningName -> Bool

Ord WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningName = D1 ('MetaData "WarningName" "Agda.Interaction.Options.Warnings" "Agda-2.6.20240714-inplace" 'False) (((((((C1 ('MetaCons "OptionRenamed_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WarningProblem_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OverlappingTokensWarning_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsupportedAttribute_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "MultipleAttributes_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LibUnknownField_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "EmptyAbstract_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyConstructor_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "EmptyField_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyGeneralize_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "EmptyInstance_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyMacro_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "EmptyMutual_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyPostulate_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "EmptyPrimitive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyPrivate_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: ((((C1 ('MetaCons "EmptyRewritePragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmptyWhere_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "HiddenGeneralize_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidCatchallPragma_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "InvalidConstructor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidConstructorBlock_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InvalidCoverageCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidNoPositivityCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "InvalidNoUniverseCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DuplicateRecordDirective_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InvalidTerminationCheckPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingDeclarations_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "MissingDefinitions_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotAllowedInMutual_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OpenPublicAbstract_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OpenPublicPrivate_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PolarityPragmasButNotPostulates_" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "PragmaCompiled_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaNoTerminationCheck_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ShadowingInTelescope_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnknownFixityInMixfixDecl_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnknownNamesInFixityDecl_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnknownNamesInPolarityPragmas_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UselessAbstract_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessInstance_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "UselessMacro_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPrivate_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AbsurdPatternRequiresNoRHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsPatternShadowsConstructorOrPatternSynonym_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatternShadowsConstructor_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CantGeneralizeOverSorts_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ClashesViaRenaming_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CoverageIssue_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoverageNoExactSplit_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "InlineNoExactSplit_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DeprecationWarning_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DuplicateUsing_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FixityInRenamingModule_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "InvalidCharacterLiteral_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPragma_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "IllformedAsClause_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceArgWithExplicitArg_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "InstanceWithExplicitArg_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceNoOutputTypeName_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InteractionMetaBoundaries_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InversionDepthReached_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "ModuleDoesntExport_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoGuardednessFlag_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NotInScope_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotStrictlyPositive_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConstructorDoesNotFitInData_" 'PrefixI 'False) (U1 :: Type -> Type)))))))) :+: ((((((C1 ('MetaCons "CoinductiveEtaRecord_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsupportedIndexedMatch_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OldBuiltin_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinDeclaresIdentifier_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PlentyInHardCompileTimeMode_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaCompileErased_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PragmaCompileList_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaCompileMaybe_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "NoMain_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteLHSNotDefinitionOrConstructor_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewriteVariablesNotBoundByLHS_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteVariablesBoundMoreThanOnce_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RewriteLHSReduces_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteHeadSymbolIsProjection_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewriteHeadSymbolIsProjectionLikeFunction_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteHeadSymbolIsTypeConstructor_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: ((((C1 ('MetaCons "RewriteHeadSymbolContainsMetas_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteConstructorParametersNotGeneral_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewriteContainsUnsolvedMetaVariables_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteBlockedOnProblems_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RewriteRequiresDefinitions_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteDoesNotTargetRewriteRelation_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewriteBeforeFunctionDefinition_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteBeforeMutualFunctionDefinition_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "ConfluenceCheckingIncompleteBecauseOfMeta_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConfluenceForCubicalNotSupported_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewriteMaybeNonConfluent_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteNonConfluent_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RewriteAmbiguousRules_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RewriteMissingRule_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DuplicateRewriteRule_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SafeFlagEta_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagInjective_" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "SafeFlagNoCoverageCheck_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagNonTerminating_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SafeFlagNoPositivityCheck_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagNoUniverseCheck_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "SafeFlagPolarity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagPostulate_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SafeFlagPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SafeFlagTerminating_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "SafeFlagWithoutKFlagPrimEraseEquality_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TerminationIssue_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UnreachableClauses_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedConstraints_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnsolvedInteractionMetas_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedMetaVariables_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UselessHiding_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UselessInline_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPatternDeclarationForRecord_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "UselessPublic_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UserWarning_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithoutKFlagPrimEraseEquality_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConflictingPragmaOptions_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "WrongInstanceDeclaration_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoInfectiveImport_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InfectiveImport_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DuplicateFields_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "TooManyFields_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingTypeSignatureForOpaque_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NotAffectedByOpaque_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnfoldTransparentName_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UselessOpaque_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FaceConstraintCannotBeHidden_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FaceConstraintCannotBeNamed_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DuplicateInterfaceFiles_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CustomBackendWarning_" 'PrefixI 'False) (U1 :: Type -> Type)))))))))

string2WarningName :: String -> Maybe WarningName Source #

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

usageWarning :: String Source #

warningUsage generated using warningNameDescription