| 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
- prettyWarningModeError :: WarningModeError -> Text
- warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate
- warningSets :: [(String, (Set WarningName, String))]
- data WarningName
- = OptionRenamed_
- | WarningProblem_
- | 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_
- 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
| |
Instances
| EmbPrj WarningMode Source # | |||||
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 # | |||||
Defined in Agda.Interaction.Options.Warnings Methods rnf :: WarningMode -> () | |||||
| Generic WarningMode Source # | |||||
Defined in Agda.Interaction.Options.Warnings Associated Types
| |||||
| Show WarningMode Source # | |||||
Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS show :: WarningMode -> String showList :: [WarningMode] -> ShowS | |||||
| Eq WarningMode Source # | |||||
Defined in Agda.Interaction.Options.Warnings | |||||
| type Rep WarningMode Source # | |||||
Defined in Agda.Interaction.Options.Warnings type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.6.20240731-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) 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 #
errorWarnings :: Set WarningName Source #
exactSplitWarnings :: Set WarningName Source #
Warnings enabled by --exact-split.
data WarningModeError Source #
Some warnings are errors and cannot be turned off.
Instances
| EmbPrj WarningModeError Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningModeError -> S Int32 Source # icod_ :: WarningModeError -> S Int32 Source # value :: Int32 -> R WarningModeError Source # | |||||
| NFData WarningModeError Source # | |||||
Defined in Agda.Interaction.Options.Warnings Methods rnf :: WarningModeError -> () | |||||
| Generic WarningModeError Source # | |||||
Defined in Agda.Interaction.Options.Warnings Associated Types
Methods from :: WarningModeError -> Rep WarningModeError x to :: Rep WarningModeError x -> WarningModeError | |||||
| Show WarningModeError Source # | |||||
Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningModeError -> ShowS show :: WarningModeError -> String showList :: [WarningModeError] -> ShowS | |||||
| type Rep WarningModeError Source # | |||||
Defined in Agda.Interaction.Options.Warnings type Rep WarningModeError = D1 ('MetaData "WarningModeError" "Agda.Interaction.Options.Warnings" "Agda-2.6.20240731-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))) | |||||
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
Instances
| EmbPrj WarningName Source # | |||||
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 # | |||||
Defined in Agda.Interaction.Options.Warnings Methods rnf :: WarningName -> () | |||||
| Bounded WarningName Source # | |||||
Defined in Agda.Interaction.Options.Warnings | |||||
| Enum WarningName Source # | |||||
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 Source # | |||||
Defined in Agda.Interaction.Options.Warnings Associated Types
| |||||
| Read WarningName Source # | |||||
Defined in Agda.Interaction.Options.Warnings Methods readsPrec :: Int -> ReadS WarningName readList :: ReadS [WarningName] readPrec :: ReadPrec WarningName readListPrec :: ReadPrec [WarningName] | |||||
| Show WarningName Source # | |||||
Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningName -> ShowS show :: WarningName -> String showList :: [WarningName] -> ShowS | |||||
| Eq WarningName Source # | |||||
Defined in Agda.Interaction.Options.Warnings | |||||
| Ord WarningName Source # | |||||
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 Source # | |||||
Defined in Agda.Interaction.Options.Warnings type Rep WarningName = D1 ('MetaData "WarningName" "Agda.Interaction.Options.Warnings" "Agda-2.6.20240731-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))))))))) | |||||
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