Agda.Interaction.Options.Warnings

Documentation

data WarningMode

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

• _warningSet :: Set WarningName
• _warn2Error :: Bool

Instances

EmbPrj WarningMode

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningMode -> S Int32

icod_ :: WarningMode -> S Int32

value :: Int32 -> R WarningMode

Generic WarningMode

Defined in Agda.Interaction.Options.Warnings

Associated Types

type Rep WarningMode :: Type -> Type

Methods

from :: WarningMode -> Rep WarningMode x

to :: Rep WarningMode x -> WarningMode

Show WarningMode

Defined in Agda.Interaction.Options.Warnings

Methods

showsPrec :: Int -> WarningMode -> ShowS

show :: WarningMode -> String

showList :: [WarningMode] -> ShowS

NFData WarningMode

Defined in Agda.Interaction.Options.Warnings

Methods

rnf :: WarningMode -> ()

Eq WarningMode

Defined in Agda.Interaction.Options.Warnings

Methods

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

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

type Rep WarningMode

Defined in Agda.Interaction.Options.Warnings

type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.6.3.20230914-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)))

warningSet :: Lens' WarningMode (Set WarningName)

warn2Error :: Lens' WarningMode Bool

lensSingleWarning :: WarningName -> Lens' WarningMode Bool

defaultWarningSet :: String

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

allWarnings :: Set WarningName

usualWarnings :: Set WarningName

noWarnings :: Set WarningName

unsolvedWarnings :: Set WarningName

incompleteMatchWarnings :: Set WarningName

errorWarnings :: Set WarningName

exactSplitWarnings :: Set WarningName

Warnings enabled by --exact-split.

defaultWarningMode :: WarningMode

data WarningModeError

Some warnings are errors and cannot be turned off.

Constructors

Unknown String

NoNoError String

prettyWarningModeError :: WarningModeError -> String

warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate

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))]

Common sets of warnings

data WarningName

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

Constructors

OptionRenamed_

OverlappingTokensWarning_

UnsupportedAttribute_

MultipleAttributes_

LibUnknownField_

EmptyAbstract_

EmptyConstructor_

EmptyField_

EmptyGeneralize_

EmptyInstance_

EmptyMacro_

EmptyMutual_

EmptyPostulate_

EmptyPrimitive_

EmptyPrivate_

EmptyRewritePragma_

EmptyWhere_

HiddenGeneralize_

InvalidCatchallPragma_

InvalidConstructor_

InvalidConstructorBlock_

InvalidCoverageCheckPragma_

InvalidNoPositivityCheckPragma_

InvalidNoUniverseCheckPragma_

InvalidRecordDirective_

InvalidTerminationCheckPragma_

MissingDeclarations_

MissingDefinitions_

NotAllowedInMutual_

OpenPublicAbstract_

OpenPublicPrivate_

PolarityPragmasButNotPostulates_

PragmaCompiled_

PragmaNoTerminationCheck_

ShadowingInTelescope_

UnknownFixityInMixfixDecl_

UnknownNamesInFixityDecl_

UnknownNamesInPolarityPragmas_

UselessAbstract_

UselessInstance_

UselessPrivate_

AbsurdPatternRequiresNoRHS_

AsPatternShadowsConstructorOrPatternSynonym_

PatternShadowsConstructor_

CantGeneralizeOverSorts_

ClashesViaRenaming_

CoverageIssue_

CoverageNoExactSplit_

InlineNoExactSplit_

DeprecationWarning_

DuplicateUsing_

FixityInRenamingModule_

InvalidCharacterLiteral_

UselessPragma_

GenericWarning_

IllformedAsClause_

InstanceArgWithExplicitArg_

InstanceWithExplicitArg_

InstanceNoOutputTypeName_

InteractionMetaBoundaries_

InversionDepthReached_

ModuleDoesntExport_

NoGuardednessFlag_

NotInScope_

NotStrictlyPositive_

UnsupportedIndexedMatch_

OldBuiltin_

PlentyInHardCompileTimeMode_

PragmaCompileErased_

RewriteMaybeNonConfluent_

RewriteNonConfluent_

RewriteAmbiguousRules_

RewriteMissingRule_

SafeFlagEta_

SafeFlagInjective_

SafeFlagNoCoverageCheck_

SafeFlagNonTerminating_

SafeFlagNoPositivityCheck_

SafeFlagNoUniverseCheck_

SafeFlagPolarity_

SafeFlagPostulate_

SafeFlagPragma_

SafeFlagTerminating_

SafeFlagWithoutKFlagPrimEraseEquality_

TerminationIssue_

UnreachableClauses_

UnsolvedConstraints_

UnsolvedInteractionMetas_

UnsolvedMetaVariables_

UselessHiding_

UselessInline_

UselessPatternDeclarationForRecord_

UselessPublic_

UserWarning_

WithoutKFlagPrimEraseEquality_

WrongInstanceDeclaration_

CoInfectiveImport_

InfectiveImport_

DuplicateFields_

TooManyFields_

NotAffectedByOpaque_

UnfoldTransparentName_

UselessOpaque_

FaceConstraintCannotBeHidden_

FaceConstraintCannotBeNamed_

Instances

EmbPrj WarningName

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningName -> S Int32

icod_ :: WarningName -> S Int32

value :: Int32 -> R WarningName

Bounded WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

minBound :: WarningName

maxBound :: WarningName

Enum WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

succ :: WarningName -> WarningName

pred :: WarningName -> WarningName

toEnum :: Int -> WarningName

fromEnum :: WarningName -> Int

enumFrom :: WarningName -> [WarningName]

enumFromThen :: WarningName -> WarningName -> [WarningName]

enumFromTo :: WarningName -> WarningName -> [WarningName]

enumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName]

Generic WarningName

Defined in Agda.Interaction.Options.Warnings

Associated Types

type Rep WarningName :: Type -> Type

Methods

from :: WarningName -> Rep WarningName x

to :: Rep WarningName x -> WarningName

Read WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

readsPrec :: Int -> ReadS WarningName

readList :: ReadS [WarningName]

readPrec :: ReadPrec WarningName

readListPrec :: ReadPrec [WarningName]

Show WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

showsPrec :: Int -> WarningName -> ShowS

show :: WarningName -> String

showList :: [WarningName] -> ShowS

NFData WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

rnf :: WarningName -> ()

Eq WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

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

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

Ord WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

compare :: WarningName -> WarningName -> Ordering

(<) :: WarningName -> WarningName -> Bool

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

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

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

max :: WarningName -> WarningName -> WarningName

min :: WarningName -> WarningName -> WarningName

type Rep WarningName

Defined in Agda.Interaction.Options.Warnings

type Rep WarningName = D1 ('MetaData "WarningName" "Agda.Interaction.Options.Warnings" "Agda-2.6.3.20230914-inplace" 'False) ((((((C1 ('MetaCons "OptionRenamed_" '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 "InvalidRecordDirective_" '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 "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 "GenericWarning_" '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 "UnsupportedIndexedMatch_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OldBuiltin_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PlentyInHardCompileTimeMode_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "PragmaCompileErased_" '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 "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 "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 "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))))))))

warningName2String :: WarningName -> String

string2WarningName :: String -> Maybe WarningName

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

usageWarning :: String

warningUsage generated using warningNameDescription