Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Options.Warnings

Synopsis

- data WarningMode = WarningMode {
  - _warningSet :: Set WarningName
  - _warn2Error :: Bool
  }
- warningSet :: Lens' WarningMode (Set WarningName)
- warn2Error :: Lens' WarningMode Bool
- lensSingleWarning :: WarningName -> Lens' WarningMode Bool
- defaultWarningSet :: String
- allWarnings :: Set WarningName
- usualWarnings :: Set WarningName
- noWarnings :: Set WarningName
- unsolvedWarnings :: Set WarningName
- incompleteMatchWarnings :: Set WarningName
- errorWarnings :: Set WarningName
- exactSplitWarnings :: Set WarningName
- defaultWarningMode :: WarningMode
- data WarningModeError
  - = Unknown Text
  - | NoNoError Text
- prettyWarningModeError :: WarningModeError -> Text
- warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate
- warningSets :: [(String, (Set WarningName, String))]
- data WarningName
  - = OptionRenamed_
  - | WarningProblem_
  - | OverlappingTokensWarning_
  - | MisplacedAttributes_
  - | UnknownPolarity_
  - | UnknownAttribute_
  - | UnsupportedAttribute_
  - | MultipleAttributes_
  - | LibUnknownField_
  - | 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_
  - | AbsurdPatternRequiresAbsentRHS_
  - | AsPatternShadowsConstructorOrPatternSynonym_
  - | PatternShadowsConstructor_
  - | CantGeneralizeOverSorts_
  - | ClashesViaRenaming_
  - | CoverageIssue_
  - | CoverageNoExactSplit_
  - | InlineNoExactSplit_
  - | DeprecationWarning_
  - | DuplicateUsing_
  - | FixingCohesion_
  - | FixingPolarity_
  - | FixingRelevance_
  - | 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_
  - | CoInfectiveImport_
  - | InfectiveImport_
  - | DuplicateFields_
  - | TooManyFields_
  - | MissingTypeSignatureForOpaque_
  - | NotAffectedByOpaque_
  - | UnfoldingWrongName_
  - | UnfoldTransparentName_
  - | UselessOpaque_
  - | HiddenNotInArgumentPosition_
  - | InstanceNotInArgumentPosition_
  - | MacroInLetBindings_
  - | AbstractInLetBindings_
  - | FaceConstraintCannotBeHidden_
  - | FaceConstraintCannotBeNamed_
  - | CustomBackendWarning_
- warningName2String :: WarningName -> String
- string2WarningName :: String -> Maybe WarningName
- usageWarning :: String

# 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

- _warningSet :: Set WarningName
- _warn2Error :: Bool

#### Instances

Instances details

EmbPrj WarningMode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningMode -> S Word32 Source # icod_ :: WarningMode -> S Word32 Source # value :: Word32 -> R WarningMode Source #
NFData WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods rnf :: WarningMode -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep WarningMode x -> WarningMode Source #

Show WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS Source # show :: WarningMode -> String Source # showList :: [WarningMode] -> ShowS Source #
Eq WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods (==) :: WarningMode -> WarningMode -> Bool Source # (/=) :: WarningMode -> WarningMode -> Bool Source #
type Rep WarningMode Source # |

Instance details

Defined in Agda.Interaction.Options.Warnings

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

warn2Error :: Lens' WarningMode Bool Source #

lensSingleWarning :: WarningName -> Lens' WarningMode Bool Source #

defaultWarningSet :: String Source #

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

allWarnings :: Set WarningName Source #

usualWarnings :: Set WarningName Source #

noWarnings :: Set WarningName Source #

unsolvedWarnings :: Set WarningName Source #

incompleteMatchWarnings :: Set WarningName Source #

errorWarnings :: Set WarningName Source #

exactSplitWarnings :: Set WarningName Source #

Warnings enabled by `--exact-split`.

defaultWarningMode :: WarningMode Source #

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 Methods icode :: WarningModeError -> S Word32 Source # icod_ :: WarningModeError -> S Word32 Source # value :: Word32 -> R WarningModeError Source #
NFData WarningModeError Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods rnf :: WarningModeError -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

Methods

from :: WarningModeError -> Rep WarningModeError x Source #

to :: Rep WarningModeError x -> WarningModeError Source #

Show WarningModeError Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningModeError -> ShowS Source # show :: WarningModeError -> String Source # showList :: [WarningModeError] -> ShowS Source #
type Rep WarningModeError Source # |

Instance details

Defined in Agda.Interaction.Options.Warnings

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

prettyWarningModeError :: WarningModeError -> Text Source #

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_ |
MisplacedAttributes_ |
UnknownPolarity_ |
UnknownAttribute_ |
UnsupportedAttribute_ |
MultipleAttributes_ |
LibUnknownField_ |
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_ |
AbsurdPatternRequiresAbsentRHS_ |
AsPatternShadowsConstructorOrPatternSynonym_ |
PatternShadowsConstructor_ |
CantGeneralizeOverSorts_ |
ClashesViaRenaming_ |
CoverageIssue_ |
CoverageNoExactSplit_ |
InlineNoExactSplit_ |
DeprecationWarning_ |
DuplicateUsing_ |
FixingCohesion_ |
FixingPolarity_ |
FixingRelevance_ |
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_ |
CoInfectiveImport_ |
InfectiveImport_ |
DuplicateFields_ |
TooManyFields_ |
MissingTypeSignatureForOpaque_ |
NotAffectedByOpaque_ |
UnfoldingWrongName_ |
UnfoldTransparentName_ |
UselessOpaque_ |
HiddenNotInArgumentPosition_ |
InstanceNotInArgumentPosition_ |
MacroInLetBindings_ |
AbstractInLetBindings_ |
FaceConstraintCannotBeHidden_ |
FaceConstraintCannotBeNamed_ |
CustomBackendWarning_ |

#### Instances

Instances details

EmbPrj WarningName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningName -> S Word32 Source # icod_ :: WarningName -> S Word32 Source # value :: Word32 -> R WarningName Source #
NFData WarningName Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods rnf :: WarningName -> () Source #
Bounded WarningName Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods minBound :: WarningName Source # maxBound :: WarningName Source #
Enum WarningName Source # |

Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

succ :: WarningName -> WarningName Source #

pred :: WarningName -> WarningName Source #

toEnum :: Int -> WarningName Source #

fromEnum :: WarningName -> Int Source #

enumFrom :: WarningName -> [WarningName] Source #

enumFromThen :: WarningName -> WarningName -> [WarningName] Source #

enumFromTo :: WarningName -> WarningName -> [WarningName] Source #

enumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName] Source #

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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 "MisplacedAttributes_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnknownPolarity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnknownAttribute_" '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 "EmptyPolarityPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "HiddenGeneralize_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidCatchallPragma_" '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 "MissingDataDeclaration_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MissingDefinitions_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotAllowedInMutual_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OpenImportAbstract_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "OpenImportPrivate_" '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 "AbsurdPatternRequiresAbsentRHS_" '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 "FixingCohesion_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FixingPolarity_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "FixingRelevance_" '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 "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 "PragmaCompileUnparsable_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaCompileWrong_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PragmaCompileWrongName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaExpectsDefinedSymbol_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PragmaExpectsUnambiguousConstructorOrFunction_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PragmaExpectsUnambiguousProjectionOrFunction_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoMain_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "NotARewriteRule_" '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 "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 "TooManyArgumentsToSort_" '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 "UselessTactic_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UserWarning_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "InvalidDisplayForm_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnusedVariablesInDisplayForm_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewritesNothing_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithClauseProjectionFixityMismatch_" '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 "TooManyPolarities_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TopLevelPolarity_" '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 "UnfoldingWrongName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnfoldTransparentName_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UselessOpaque_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "HiddenNotInArgumentPosition_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceNotInArgumentPosition_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "MacroInLetBindings_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AbstractInLetBindings_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FaceConstraintCannotBeHidden_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FaceConstraintCannotBeNamed_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CustomBackendWarning_" 'PrefixI 'False) (U1 :: Type -> Type)))))))))

Methods

from :: WarningName -> Rep WarningName x Source #

to :: Rep WarningName x -> WarningName Source #

Read WarningName Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods readsPrec :: Int -> ReadS WarningName Source # readList :: ReadS [WarningName] Source # readPrec :: ReadPrec WarningName Source # readListPrec :: ReadPrec [WarningName] Source #
Show WarningName Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningName -> ShowS Source # show :: WarningName -> String Source # showList :: [WarningName] -> ShowS Source #
Eq WarningName Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods (==) :: WarningName -> WarningName -> Bool Source # (/=) :: WarningName -> WarningName -> Bool Source #
Ord WarningName Source # |

Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

compare :: WarningName -> WarningName -> Ordering Source #

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

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

(>) :: WarningName -> WarningName -> Bool Source #

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

max :: WarningName -> WarningName -> WarningName Source #

min :: WarningName -> WarningName -> WarningName Source #

type Rep WarningName Source # |

Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningName = D1 ('MetaData "WarningName" "Agda.Interaction.Options.Warnings" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 "MisplacedAttributes_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnknownPolarity_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnknownAttribute_" '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 "EmptyPolarityPragma_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "HiddenGeneralize_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InvalidCatchallPragma_" '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 "MissingDataDeclaration_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MissingDefinitions_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotAllowedInMutual_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OpenImportAbstract_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "OpenImportPrivate_" '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 "AbsurdPatternRequiresAbsentRHS_" '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 "FixingCohesion_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FixingPolarity_" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "FixingRelevance_" '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 "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 "PragmaCompileUnparsable_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaCompileWrong_" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PragmaCompileWrongName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PragmaExpectsDefinedSymbol_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PragmaExpectsUnambiguousConstructorOrFunction_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PragmaExpectsUnambiguousProjectionOrFunction_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoMain_" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "NotARewriteRule_" '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 "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 "TooManyArgumentsToSort_" '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 "UselessTactic_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UserWarning_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "InvalidDisplayForm_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnusedVariablesInDisplayForm_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RewritesNothing_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithClauseProjectionFixityMismatch_" '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 "TooManyPolarities_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TopLevelPolarity_" '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 "UnfoldingWrongName_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnfoldTransparentName_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UselessOpaque_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "HiddenNotInArgumentPosition_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceNotInArgumentPosition_" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "MacroInLetBindings_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AbstractInLetBindings_" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FaceConstraintCannotBeHidden_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FaceConstraintCannotBeNamed_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CustomBackendWarning_" 'PrefixI 'False) (U1 :: Type -> Type)))))))))

warningName2String :: WarningName -> String Source #

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`