module Agda.Interaction.Options.Warnings
(
WarningMode (..)
, warningSet
, warn2Error
, defaultWarningSet
, allWarnings
, usualWarnings
, noWarnings
, unsolvedWarnings
, incompleteMatchWarnings
, errorWarnings
, defaultWarningMode
, WarningModeError(..)
, prettyWarningModeError
, warningModeUpdate
, warningSets
, WarningName (..)
, warningName2String
, string2WarningName
, usageWarning
)
where
import Control.Arrow ( (&&&) )
import Control.DeepSeq
import Control.Monad ( guard, when )
import Text.Read ( readMaybe )
import Data.Set (Set)
import qualified Data.Set as Set
import Data.List ( stripPrefix, intercalate )
import GHC.Generics (Generic)
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Impossible
data WarningMode = WarningMode
{ WarningMode -> Set WarningName
_warningSet :: Set WarningName
, WarningMode -> Bool
_warn2Error :: Bool
} deriving (WarningMode -> WarningMode -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WarningMode -> WarningMode -> Bool
$c/= :: WarningMode -> WarningMode -> Bool
== :: WarningMode -> WarningMode -> Bool
$c== :: WarningMode -> WarningMode -> Bool
Eq, Int -> WarningMode -> ShowS
[WarningMode] -> ShowS
WarningMode -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [WarningMode] -> ShowS
$cshowList :: [WarningMode] -> ShowS
show :: WarningMode -> [Char]
$cshow :: WarningMode -> [Char]
showsPrec :: Int -> WarningMode -> ShowS
$cshowsPrec :: Int -> WarningMode -> ShowS
Show, forall x. Rep WarningMode x -> WarningMode
forall x. WarningMode -> Rep WarningMode x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep WarningMode x -> WarningMode
$cfrom :: forall x. WarningMode -> Rep WarningMode x
Generic)
instance NFData WarningMode
warningSet :: Lens' (Set WarningName) WarningMode
warningSet :: Lens' (Set WarningName) WarningMode
warningSet Set WarningName -> f (Set WarningName)
f WarningMode
o = (\ Set WarningName
ws -> WarningMode
o { _warningSet :: Set WarningName
_warningSet = Set WarningName
ws }) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set WarningName -> f (Set WarningName)
f (WarningMode -> Set WarningName
_warningSet WarningMode
o)
warn2Error :: Lens' Bool WarningMode
warn2Error :: Lens' Bool WarningMode
warn2Error Bool -> f Bool
f WarningMode
o = (\ Bool
ws -> WarningMode
o { _warn2Error :: Bool
_warn2Error = Bool
ws }) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> f Bool
f (WarningMode -> Bool
_warn2Error WarningMode
o)
defaultWarningSet :: String
defaultWarningSet :: [Char]
defaultWarningSet = [Char]
"warn"
defaultWarningMode :: WarningMode
defaultWarningMode :: WarningMode
defaultWarningMode = Set WarningName -> Bool -> WarningMode
WarningMode Set WarningName
ws Bool
False where
ws :: Set WarningName
ws = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
defaultWarningSet [([Char], (Set WarningName, [Char]))]
warningSets
data WarningModeError = Unknown String | NoNoError String
prettyWarningModeError :: WarningModeError -> String
prettyWarningModeError :: WarningModeError -> [Char]
prettyWarningModeError = \case
Unknown [Char]
str -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"Unknown warning flag: ", [Char]
str, [Char]
"." ]
NoNoError [Char]
str -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"You may only turn off benign warnings. The warning "
, [Char]
str
,[Char]
" is a non-fatal error and thus cannot be ignored." ]
type WarningModeUpdate = WarningMode -> WarningMode
warningModeUpdate :: String -> Either WarningModeError WarningModeUpdate
warningModeUpdate :: [Char] -> Either WarningModeError WarningModeUpdate
warningModeUpdate [Char]
str = case [Char]
str of
[Char]
"error" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensSet i o
set Lens' Bool WarningMode
warn2Error Bool
True
[Char]
"noerror" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensSet i o
set Lens' Bool WarningMode
warn2Error Bool
False
[Char]
_ | Just Set WarningName
ws <- forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
str [([Char], (Set WarningName, [Char]))]
warningSets
-> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensSet i o
set Lens' (Set WarningName) WarningMode
warningSet Set WarningName
ws
[Char]
_ -> case forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix [Char]
"no" [Char]
str of
Maybe [Char]
Nothing -> do
WarningName
wname <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. a -> Either a b
Left ([Char] -> WarningModeError
Unknown [Char]
str)) forall a b. b -> Either a b
Right ([Char] -> Maybe WarningName
string2WarningName [Char]
str)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
Set.insert WarningName
wname)
Just [Char]
str' -> do
WarningName
wname <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. a -> Either a b
Left ([Char] -> WarningModeError
Unknown [Char]
str')) forall a b. b -> Either a b
Right ([Char] -> Maybe WarningName
string2WarningName [Char]
str')
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (WarningName
wname forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set WarningName
errorWarnings) (forall a b. a -> Either a b
Left ([Char] -> WarningModeError
NoNoError [Char]
str'))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
Set.delete WarningName
wname)
warningSets :: [(String, (Set WarningName, String))]
warningSets :: [([Char], (Set WarningName, [Char]))]
warningSets = [ ([Char]
"all" , (Set WarningName
allWarnings, [Char]
"All of the existing warnings"))
, ([Char]
"warn" , (Set WarningName
usualWarnings, [Char]
"Default warning level"))
, ([Char]
"ignore", (Set WarningName
errorWarnings, [Char]
"Ignore all the benign warnings"))
]
noWarnings :: Set WarningName
noWarnings :: Set WarningName
noWarnings = forall a. Set a
Set.empty
unsolvedWarnings :: Set WarningName
unsolvedWarnings :: Set WarningName
unsolvedWarnings = forall a. Ord a => [a] -> Set a
Set.fromList
[ WarningName
UnsolvedMetaVariables_
, WarningName
UnsolvedInteractionMetas_
, WarningName
UnsolvedConstraints_
]
incompleteMatchWarnings :: Set WarningName
incompleteMatchWarnings :: Set WarningName
incompleteMatchWarnings = forall a. Ord a => [a] -> Set a
Set.fromList [ WarningName
CoverageIssue_ ]
errorWarnings :: Set WarningName
errorWarnings :: Set WarningName
errorWarnings = forall a. Ord a => [a] -> Set a
Set.fromList
[ WarningName
CoverageIssue_
, WarningName
GenericNonFatalError_
, WarningName
MissingDefinitions_
, WarningName
MissingDeclarations_
, WarningName
NotAllowedInMutual_
, WarningName
NotStrictlyPositive_
, WarningName
OverlappingTokensWarning_
, WarningName
PragmaCompiled_
, WarningName
SafeFlagPostulate_
, WarningName
SafeFlagPragma_
, WarningName
SafeFlagNonTerminating_
, WarningName
SafeFlagTerminating_
, WarningName
SafeFlagWithoutKFlagPrimEraseEquality_
, WarningName
SafeFlagNoPositivityCheck_
, WarningName
SafeFlagPolarity_
, WarningName
SafeFlagNoUniverseCheck_
, WarningName
SafeFlagEta_
, WarningName
SafeFlagInjective_
, WarningName
SafeFlagNoCoverageCheck_
, WarningName
TerminationIssue_
, WarningName
UnsolvedMetaVariables_
, WarningName
UnsolvedInteractionMetas_
, WarningName
UnsolvedConstraints_
, WarningName
InfectiveImport_
, WarningName
CoInfectiveImport_
, WarningName
RewriteNonConfluent_
, WarningName
RewriteMaybeNonConfluent_
, WarningName
RewriteAmbiguousRules_
, WarningName
RewriteMissingRule_
]
allWarnings :: Set WarningName
allWarnings :: Set WarningName
allWarnings = forall a. Ord a => [a] -> Set a
Set.fromList [forall a. Bounded a => a
minBound..forall a. Bounded a => a
maxBound]
usualWarnings :: Set WarningName
usualWarnings :: Set WarningName
usualWarnings = Set WarningName
allWarnings forall a. Ord a => Set a -> Set a -> Set a
Set.\\ forall a. Ord a => [a] -> Set a
Set.fromList
[ WarningName
UnknownFixityInMixfixDecl_
, WarningName
CoverageNoExactSplit_
, WarningName
ShadowingInTelescope_
]
data WarningName
=
OverlappingTokensWarning_
| UnsupportedAttribute_
| MultipleAttributes_
| LibUnknownField_
| EmptyAbstract_
| EmptyConstructor_
| EmptyField_
| EmptyGeneralize_
| EmptyInstance_
| EmptyMacro_
| EmptyMutual_
| EmptyPostulate_
| EmptyPrimitive_
| EmptyPrivate_
| EmptyRewritePragma_
| EmptyWhere_
| 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_
| CantGeneralizeOverSorts_
| ClashesViaRenaming_
| CoverageIssue_
| CoverageNoExactSplit_
| DeprecationWarning_
| DuplicateUsing_
| FixityInRenamingModule_
| GenericNonFatalError_
| GenericUseless_
| GenericWarning_
| IllformedAsClause_
| InstanceArgWithExplicitArg_
| InstanceWithExplicitArg_
| InstanceNoOutputTypeName_
| InversionDepthReached_
| ModuleDoesntExport_
| NoGuardednessFlag_
| NotInScope_
| NotStrictlyPositive_
| OldBuiltin_
| 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_
| DuplicateFieldsWarning_
| TooManyFieldsWarning_
deriving (WarningName -> WarningName -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WarningName -> WarningName -> Bool
$c/= :: WarningName -> WarningName -> Bool
== :: WarningName -> WarningName -> Bool
$c== :: WarningName -> WarningName -> Bool
Eq, Eq WarningName
WarningName -> WarningName -> Bool
WarningName -> WarningName -> Ordering
WarningName -> WarningName -> WarningName
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: WarningName -> WarningName -> WarningName
$cmin :: WarningName -> WarningName -> WarningName
max :: WarningName -> WarningName -> WarningName
$cmax :: WarningName -> WarningName -> WarningName
>= :: WarningName -> WarningName -> Bool
$c>= :: WarningName -> WarningName -> Bool
> :: WarningName -> WarningName -> Bool
$c> :: WarningName -> WarningName -> Bool
<= :: WarningName -> WarningName -> Bool
$c<= :: WarningName -> WarningName -> Bool
< :: WarningName -> WarningName -> Bool
$c< :: WarningName -> WarningName -> Bool
compare :: WarningName -> WarningName -> Ordering
$ccompare :: WarningName -> WarningName -> Ordering
Ord, Int -> WarningName -> ShowS
[WarningName] -> ShowS
WarningName -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [WarningName] -> ShowS
$cshowList :: [WarningName] -> ShowS
show :: WarningName -> [Char]
$cshow :: WarningName -> [Char]
showsPrec :: Int -> WarningName -> ShowS
$cshowsPrec :: Int -> WarningName -> ShowS
Show, ReadPrec [WarningName]
ReadPrec WarningName
Int -> ReadS WarningName
ReadS [WarningName]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [WarningName]
$creadListPrec :: ReadPrec [WarningName]
readPrec :: ReadPrec WarningName
$creadPrec :: ReadPrec WarningName
readList :: ReadS [WarningName]
$creadList :: ReadS [WarningName]
readsPrec :: Int -> ReadS WarningName
$creadsPrec :: Int -> ReadS WarningName
Read, Int -> WarningName
WarningName -> Int
WarningName -> [WarningName]
WarningName -> WarningName
WarningName -> WarningName -> [WarningName]
WarningName -> WarningName -> WarningName -> [WarningName]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName]
$cenumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName]
enumFromTo :: WarningName -> WarningName -> [WarningName]
$cenumFromTo :: WarningName -> WarningName -> [WarningName]
enumFromThen :: WarningName -> WarningName -> [WarningName]
$cenumFromThen :: WarningName -> WarningName -> [WarningName]
enumFrom :: WarningName -> [WarningName]
$cenumFrom :: WarningName -> [WarningName]
fromEnum :: WarningName -> Int
$cfromEnum :: WarningName -> Int
toEnum :: Int -> WarningName
$ctoEnum :: Int -> WarningName
pred :: WarningName -> WarningName
$cpred :: WarningName -> WarningName
succ :: WarningName -> WarningName
$csucc :: WarningName -> WarningName
Enum, WarningName
forall a. a -> a -> Bounded a
maxBound :: WarningName
$cmaxBound :: WarningName
minBound :: WarningName
$cminBound :: WarningName
Bounded, forall x. Rep WarningName x -> WarningName
forall x. WarningName -> Rep WarningName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep WarningName x -> WarningName
$cfrom :: forall x. WarningName -> Rep WarningName x
Generic)
instance NFData WarningName
string2WarningName :: String -> Maybe WarningName
string2WarningName :: [Char] -> Maybe WarningName
string2WarningName = forall a. Read a => [Char] -> Maybe a
readMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. [a] -> [a] -> [a]
++ [Char]
"_")
warningName2String :: WarningName -> String
warningName2String :: WarningName -> [Char]
warningName2String = forall a. [a] -> [a] -> [a]
initWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show
usageWarning :: String
usageWarning :: [Char]
usageWarning = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n"
[ [Char]
"The -W or --warning option can be used to disable or enable\
\ different warnings. The flag -W error (or --warning=error)\
\ can be used to turn all warnings into errors, while -W noerror\
\ turns this off again."
, [Char]
""
, [Char]
"A group of warnings can be enabled by -W group, where group is\
\ one of the following:"
, [Char]
""
, [([Char], [Char])] -> [Char]
untable (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a, b) -> a
fst forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [([Char], (Set WarningName, [Char]))]
warningSets)
, [Char]
"Individual benign warnings can be turned on and off by -W Name and\
\ -W noName, respectively, where Name comes from the following\
\ list (warnings marked with 'd' are turned on by default, and 'b'\
\ stands for \"benign warning\"):"
, [Char]
""
, [([Char], [Char])] -> [Char]
untable forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> (a -> Maybe b) -> [b]
forMaybe [forall a. Bounded a => a
minBound..forall a. Bounded a => a
maxBound] forall a b. (a -> b) -> a -> b
$ \ WarningName
w ->
let wnd :: [Char]
wnd = WarningName -> [Char]
warningNameDescription WarningName
w in
( WarningName -> [Char]
warningName2String WarningName
w
, (if WarningName
w forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
usualWarnings then [Char]
"d" else [Char]
" ") forall a. [a] -> [a] -> [a]
++
(if Bool -> Bool
not (WarningName
w forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
errorWarnings) then [Char]
"b" else [Char]
" ") forall a. [a] -> [a] -> [a]
++
[Char]
" " forall a. [a] -> [a] -> [a]
++
[Char]
wnd
) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
wnd)
]
where
untable :: [(String, String)] -> String
untable :: [([Char], [Char])] -> [Char]
untable [([Char], [Char])]
rows =
let len :: Int
len = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [([Char], [Char])]
rows) in
[[Char]] -> [Char]
unlines forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> [a] -> [b]
map [([Char], [Char])]
rows forall a b. (a -> b) -> a -> b
$ \ ([Char]
hdr, [Char]
cnt) ->
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
hdr, forall a. Int -> a -> [a]
replicate (Int
1 forall a. Num a => a -> a -> a
+ Int
len forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
hdr) Char
' ', [Char]
cnt ]
warningNameDescription :: WarningName -> String
warningNameDescription :: WarningName -> [Char]
warningNameDescription = \case
WarningName
OverlappingTokensWarning_ -> [Char]
"Multi-line comments spanning one or more literate text blocks."
WarningName
UnsupportedAttribute_ -> [Char]
"Unsupported attributes."
WarningName
MultipleAttributes_ -> [Char]
"Multiple attributes."
WarningName
LibUnknownField_ -> [Char]
"Unknown field in library file."
WarningName
EmptyAbstract_ -> [Char]
"Empty `abstract' blocks."
WarningName
EmptyConstructor_ -> [Char]
"Empty `constructor' blocks."
WarningName
EmptyField_ -> [Char]
"Empty `field` blocks."
WarningName
EmptyGeneralize_ -> [Char]
"Empty `variable' blocks."
WarningName
EmptyInstance_ -> [Char]
"Empty `instance' blocks."
WarningName
EmptyMacro_ -> [Char]
"Empty `macro' blocks."
WarningName
EmptyMutual_ -> [Char]
"Empty `mutual' blocks."
WarningName
EmptyPostulate_ -> [Char]
"Empty `postulate' blocks."
WarningName
EmptyPrimitive_ -> [Char]
"Empty `primitive' blocks."
WarningName
EmptyPrivate_ -> [Char]
"Empty `private' blocks."
WarningName
EmptyRewritePragma_ -> [Char]
"Empty `REWRITE' pragmas."
WarningName
EmptyWhere_ -> [Char]
"Empty `where' blocks."
WarningName
InvalidCatchallPragma_ -> [Char]
"`CATCHALL' pragmas before a non-function clause."
WarningName
InvalidConstructor_ -> [Char]
"`constructor' blocks may only contain type signatures for constructors."
WarningName
InvalidConstructorBlock_ -> [Char]
"No `constructor' blocks outside of `interleaved mutual' blocks."
WarningName
InvalidCoverageCheckPragma_ -> [Char]
"Coverage checking pragmas before non-function or `mutual' blocks."
WarningName
InvalidNoPositivityCheckPragma_ -> [Char]
"No positivity checking pragmas before non-`data', `record' or `mutual' blocks."
WarningName
InvalidNoUniverseCheckPragma_ -> [Char]
"No universe checking pragmas before non-`data' or `record' declaration."
WarningName
InvalidRecordDirective_ -> [Char]
"No record directive outside of record definition / below field declarations."
WarningName
InvalidTerminationCheckPragma_ -> [Char]
"Termination checking pragmas before non-function or `mutual' blocks."
WarningName
MissingDeclarations_ -> [Char]
"Definitions not associated to a declaration."
WarningName
MissingDefinitions_ -> [Char]
"Declarations not associated to a definition."
WarningName
NotAllowedInMutual_ -> [Char]
"Declarations not allowed in a mutual block."
WarningName
OpenPublicAbstract_ -> [Char]
"'open public' directive in an 'abstract' block."
WarningName
OpenPublicPrivate_ -> [Char]
"'open public' directive in a 'private' block."
WarningName
PolarityPragmasButNotPostulates_ -> [Char]
"Polarity pragmas for non-postulates."
WarningName
PragmaCompiled_ -> [Char]
"'COMPILE' pragmas not allowed in safe mode."
WarningName
PragmaNoTerminationCheck_ -> [Char]
"`NO_TERMINATION_CHECK' pragmas are deprecated"
WarningName
ShadowingInTelescope_ -> [Char]
"Repeated variable name in telescope."
WarningName
UnknownFixityInMixfixDecl_ -> [Char]
"Mixfix names without an associated fixity declaration."
WarningName
UnknownNamesInFixityDecl_ -> [Char]
"Names not declared in the same scope as their syntax or fixity declaration."
WarningName
UnknownNamesInPolarityPragmas_ -> [Char]
"Names not declared in the same scope as their polarity pragmas."
WarningName
UselessAbstract_ -> [Char]
"`abstract' blocks where they have no effect."
WarningName
UselessHiding_ -> [Char]
"Names in `hiding' directive that are anyway not imported."
WarningName
UselessInline_ -> [Char]
"`INLINE' pragmas where they have no effect."
WarningName
UselessInstance_ -> [Char]
"`instance' blocks where they have no effect."
WarningName
UselessPrivate_ -> [Char]
"`private' blocks where they have no effect."
WarningName
UselessPublic_ -> [Char]
"`public' blocks where they have no effect."
WarningName
UselessPatternDeclarationForRecord_ -> [Char]
"`pattern' attributes where they have no effect."
WarningName
AbsurdPatternRequiresNoRHS_ -> [Char]
"A clause with an absurd pattern does not need a Right Hand Side."
WarningName
AsPatternShadowsConstructorOrPatternSynonym_ -> [Char]
"@-patterns that shadow constructors or pattern synonyms."
WarningName
CantGeneralizeOverSorts_ -> [Char]
"Attempt to generalize over sort metas in 'variable' declaration."
WarningName
ClashesViaRenaming_ -> [Char]
"Clashes introduced by `renaming'."
WarningName
CoverageIssue_ -> [Char]
"Failed coverage checks."
WarningName
CoverageNoExactSplit_ -> [Char]
"Failed exact split checks."
WarningName
DeprecationWarning_ -> [Char]
"Feature deprecation."
WarningName
GenericNonFatalError_ -> [Char]
""
WarningName
GenericUseless_ -> [Char]
"Useless code."
WarningName
GenericWarning_ -> [Char]
""
WarningName
IllformedAsClause_ -> [Char]
"Illformed `as'-clauses in `import' statements."
WarningName
InstanceNoOutputTypeName_ -> [Char]
"instance arguments whose type does not end in a named or variable type are never considered by instance search."
WarningName
InstanceArgWithExplicitArg_ -> [Char]
"instance arguments with explicit arguments are never considered by instance search."
WarningName
InstanceWithExplicitArg_ -> [Char]
"`instance` declarations with explicit arguments are never considered by instance search."
WarningName
InversionDepthReached_ -> [Char]
"Inversions of pattern-matching failed due to exhausted inversion depth."
WarningName
NoGuardednessFlag_ -> [Char]
"Coinductive record but no --guardedness flag."
WarningName
ModuleDoesntExport_ -> [Char]
"Imported name is not actually exported."
WarningName
DuplicateUsing_ -> [Char]
"Repeated names in using directive."
WarningName
FixityInRenamingModule_ -> [Char]
"Found fixity annotation in renaming directive for module."
WarningName
NotInScope_ -> [Char]
"Out of scope name."
WarningName
NotStrictlyPositive_ -> [Char]
"Failed strict positivity checks."
WarningName
OldBuiltin_ -> [Char]
"Deprecated `BUILTIN' pragmas."
WarningName
PragmaCompileErased_ -> [Char]
"`COMPILE' pragma targeting an erased symbol."
WarningName
RewriteMaybeNonConfluent_ -> [Char]
"Failed local confluence check while computing overlap."
WarningName
RewriteNonConfluent_ -> [Char]
"Failed local confluence check while joining critical pairs."
WarningName
RewriteAmbiguousRules_ -> [Char]
"Failed global confluence check because of overlapping rules."
WarningName
RewriteMissingRule_ -> [Char]
"Failed global confluence check because of missing rule."
WarningName
SafeFlagEta_ -> [Char]
"`ETA' pragmas with the safe flag."
WarningName
SafeFlagInjective_ -> [Char]
"`INJECTIVE' pragmas with the safe flag."
WarningName
SafeFlagNoCoverageCheck_ -> [Char]
"`NON_COVERING` pragmas with the safe flag."
WarningName
SafeFlagNonTerminating_ -> [Char]
"`NON_TERMINATING' pragmas with the safe flag."
WarningName
SafeFlagNoPositivityCheck_ -> [Char]
"`NO_POSITIVITY_CHECK' pragmas with the safe flag."
WarningName
SafeFlagNoUniverseCheck_ -> [Char]
"`NO_UNIVERSE_CHECK' pragmas with the safe flag."
WarningName
SafeFlagPolarity_ -> [Char]
"`POLARITY' pragmas with the safe flag."
WarningName
SafeFlagPostulate_ -> [Char]
"`postulate' blocks with the safe flag."
WarningName
SafeFlagPragma_ -> [Char]
"Unsafe `OPTIONS' pragmas with the safe flag."
WarningName
SafeFlagTerminating_ -> [Char]
"`TERMINATING' pragmas with the safe flag."
WarningName
SafeFlagWithoutKFlagPrimEraseEquality_ -> [Char]
"`primEraseEquality' used with the safe and without-K flags."
WarningName
TerminationIssue_ -> [Char]
"Failed termination checks."
WarningName
UnreachableClauses_ -> [Char]
"Unreachable function clauses."
WarningName
UnsolvedConstraints_ -> [Char]
"Unsolved constraints."
WarningName
UnsolvedInteractionMetas_ -> [Char]
"Unsolved interaction meta variables."
WarningName
UnsolvedMetaVariables_ -> [Char]
"Unsolved meta variables."
WarningName
UserWarning_ -> [Char]
"User-defined warning added using one of the 'WARNING_ON_*' pragmas."
WarningName
WithoutKFlagPrimEraseEquality_ -> [Char]
"`primEraseEquality' usages with the without-K flags."
WarningName
WrongInstanceDeclaration_ -> [Char]
"Terms marked as eligible for instance search should end with a name."
WarningName
CoInfectiveImport_ -> [Char]
"Importing a file not using e.g. `--safe' from one which does."
WarningName
InfectiveImport_ -> [Char]
"Importing a file using e.g. `--cubical' into one which doesn't."
WarningName
DuplicateFieldsWarning_ -> [Char]
"Record expression with duplicate field names."
WarningName
TooManyFieldsWarning_ -> [Char]
"Record expression with invalid field names."