Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Concrete.Definitions.Errors

Synopsis

data DeclarationException = DeclarationException {
- deLocation :: CallStack
- deException :: DeclarationException'
}
data DeclarationException'
- = MultipleEllipses Pattern
- | InvalidName Name
- | DuplicateDefinition Name
- | DuplicateAnonDeclaration Range
- | MissingWithClauses Name LHS
- | WrongDefinition Name DataRecOrFun DataRecOrFun
- | DeclarationPanic String
- | WrongContentBlock KindOfBlock Range
- | AmbiguousFunClauses LHS (List1 Name)
- | AmbiguousConstructor Range Name [Name]
- | InvalidMeasureMutual Range
- | UnquoteDefRequiresSignature (List1 Name)
- | BadMacroDef NiceDeclaration
- | UnfoldingOutsideOpaque KwRange
- | OpaqueInMutual KwRange
- | DisallowedInterleavedMutual KwRange String (List1 Name)
data DeclarationWarning = DeclarationWarning {
- dwLocation :: CallStack
- dwWarning :: DeclarationWarning'
}
data DeclarationWarning'
- = EmptyAbstract KwRange
- | EmptyConstructor KwRange
- | EmptyField KwRange
- | EmptyGeneralize KwRange
- | EmptyInstance KwRange
- | EmptyMacro KwRange
- | EmptyMutual KwRange
- | EmptyPostulate KwRange
- | EmptyPrivate KwRange
- | EmptyPrimitive KwRange
- | HiddenGeneralize Range
- | InvalidCatchallPragma Range
- | InvalidConstructor Range
- | InvalidConstructorBlock Range
- | InvalidCoverageCheckPragma Range
- | InvalidNoPositivityCheckPragma Range
- | InvalidNoUniverseCheckPragma Range
- | InvalidTerminationCheckPragma Range
- | MissingDeclarations [(Name, Range)]
- | MissingDefinitions [(Name, Range)]
- | NotAllowedInMutual Range String
- | OpenPublicPrivate KwRange
- | OpenPublicAbstract KwRange
- | PolarityPragmasButNotPostulates [Name]
- | PragmaNoTerminationCheck Range
- | PragmaCompiled Range
- | SafeFlagEta Range
- | SafeFlagInjective Range
- | SafeFlagNoCoverageCheck Range
- | SafeFlagNoPositivityCheck Range
- | SafeFlagNoUniverseCheck Range
- | SafeFlagNonTerminating Range
- | SafeFlagPolarity Range
- | SafeFlagTerminating Range
- | ShadowingInTelescope (List1 (Name, List2 Range))
- | UnknownFixityInMixfixDecl [Name]
- | UnknownNamesInFixityDecl [Name]
- | UnknownNamesInPolarityPragmas [Name]
- | UselessAbstract KwRange
- | UselessInstance KwRange
- | UselessMacro KwRange
- | UselessPrivate KwRange
declarationWarningName :: DeclarationWarning -> WarningName
declarationWarningName' :: DeclarationWarning' -> WarningName
unsafeDeclarationWarning :: DeclarationWarning -> Bool
unsafeDeclarationWarning' :: DeclarationWarning' -> Bool
unsafePragma :: CMaybe DeclarationWarning' m => Pragma -> m

Documentation

data DeclarationException Source #

Exception with internal source code callstack

Constructors

DeclarationException
Fields deLocation :: CallStack deException :: DeclarationException'

Instances

Instances details

HasRange DeclarationException Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationException -> Range Source #
MonadError DeclarationException Nice
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods throwError :: DeclarationException -> Nice a catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a

data DeclarationException' Source #

The exception type.

Constructors

MultipleEllipses Pattern
InvalidName Name
DuplicateDefinition Name
DuplicateAnonDeclaration Range
MissingWithClauses Name LHS
WrongDefinition Name DataRecOrFun DataRecOrFun
DeclarationPanic String
WrongContentBlock KindOfBlock Range
AmbiguousFunClauses LHS (List1 Name)	In a mutual block, a clause could belong to any of the ≥2 type signatures (`Name`).
AmbiguousConstructor Range Name [Name]	In an interleaved mutual block, a constructor could belong to any of the data signatures (`Name`)
InvalidMeasureMutual Range	In a mutual block, all or none need a MEASURE pragma. `Range` is the one of the offending pragma or the mutual block.
UnquoteDefRequiresSignature (List1 Name)
BadMacroDef NiceDeclaration
UnfoldingOutsideOpaque KwRange	An unfolding declaration was not the first declaration contained in an opaque block.
OpaqueInMutual KwRange	`opaque` block nested in a `mutual` block. This can never happen, even with reordering. The `KwRange` is the one of the `opaque` keyword.
DisallowedInterleavedMutual KwRange String (List1 Name)	A declaration that breaks an implicit mutual block (named by the String argument) was present while the given lone type signatures were still without their definitions.

Instances

Instances details

Pretty DeclarationException' Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods pretty :: DeclarationException' -> Doc Source # prettyPrec :: Int -> DeclarationException' -> Doc Source # prettyList :: [DeclarationException'] -> Doc Source #
HasRange DeclarationException' Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationException' -> Range Source #
Show DeclarationException' Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods showsPrec :: Int -> DeclarationException' -> ShowS show :: DeclarationException' -> String showList :: [DeclarationException'] -> ShowS

data DeclarationWarning Source #

Constructors

DeclarationWarning
Fields dwLocation :: CallStack dwWarning :: DeclarationWarning'

Instances

Instances details

Pretty DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationWarning -> Doc Source #

prettyPrec :: Int -> DeclarationWarning -> Doc Source #

prettyList :: [DeclarationWarning] -> Doc Source #

HasRange DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationWarning -> Range Source #

EmbPrj DeclarationWarning Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning -> S Int32 Source #

icod_ :: DeclarationWarning -> S Int32 Source #

value :: Int32 -> R DeclarationWarning Source #

NFData DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning -> ()

Generic DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationWarning

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning = D1 ('MetaData "DeclarationWarning" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.20240731-inplace" 'False) (C1 ('MetaCons "DeclarationWarning" 'PrefixI 'True) (S1 ('MetaSel ('Just "dwLocation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CallStack) :*: S1 ('MetaSel ('Just "dwWarning") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclarationWarning')))

Methods

from :: DeclarationWarning -> Rep DeclarationWarning x

to :: Rep DeclarationWarning x -> DeclarationWarning

Show DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

showsPrec :: Int -> DeclarationWarning -> ShowS

show :: DeclarationWarning -> String

showList :: [DeclarationWarning] -> ShowS

type Rep DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning = D1 ('MetaData "DeclarationWarning" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.20240731-inplace" 'False) (C1 ('MetaCons "DeclarationWarning" 'PrefixI 'True) (S1 ('MetaSel ('Just "dwLocation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CallStack) :*: S1 ('MetaSel ('Just "dwWarning") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclarationWarning')))

data DeclarationWarning' Source #

Non-fatal errors encountered in the Nicifier.

Constructors

EmptyAbstract KwRange	Empty `abstract` block.
EmptyConstructor KwRange	Empty `data _ where` block.
EmptyField KwRange	Empty `field` block.
EmptyGeneralize KwRange	Empty `variable` block.
EmptyInstance KwRange	Empty `instance` block
EmptyMacro KwRange	Empty `macro` block.
EmptyMutual KwRange	Empty `mutual` block.
EmptyPostulate KwRange	Empty `postulate` block.
EmptyPrivate KwRange	Empty `private` block.
EmptyPrimitive KwRange	Empty `primitive` block.
HiddenGeneralize Range	A `Hidden` identifier in a `variable` declaration. Hiding has no effect there as generalized variables are always hidden (or instance variables).
InvalidCatchallPragma Range	A {-# CATCHALL #-} pragma that does not precede a function clause.
InvalidConstructor Range	Invalid definition in a constructor block
InvalidConstructorBlock Range	Invalid constructor block (not inside an interleaved mutual block)
InvalidCoverageCheckPragma Range	A {-# NON_COVERING #-} pragma that does not apply to any function.
InvalidNoPositivityCheckPragma Range	A {-# NO_POSITIVITY_CHECK #-} pragma that does not apply to any data or record type.
InvalidNoUniverseCheckPragma Range	A {-# NO_UNIVERSE_CHECK #-} pragma that does not apply to a data or record type.
InvalidTerminationCheckPragma Range	A {-# TERMINATING #-} and {-# NON_TERMINATING #-} pragma that does not apply to any function.
MissingDeclarations [(Name, Range)]	Definitions (e.g. constructors or functions) without a declaration.
MissingDefinitions [(Name, Range)]	Declarations (e.g. type signatures) without a definition.
NotAllowedInMutual Range String
OpenPublicPrivate KwRange	`private` has no effect on `open public`. (But the user might think so.) `KwRange` is the range of the `public` keyword.
OpenPublicAbstract KwRange	`abstract` has no effect on `open public`. (But the user might think so.) `KwRange` is the range of the `public` keyword.
PolarityPragmasButNotPostulates [Name]
PragmaNoTerminationCheck Range	Pragma `{-# NO_TERMINATION_CHECK #-}` has been replaced by `{-# TERMINATING #-}` and `{-# NON_TERMINATING #-}`.
PragmaCompiled Range	`COMPILE` pragmas are not allowed in safe mode.
SafeFlagEta Range	`ETA` pragma is unsafe.
SafeFlagInjective Range	`INJECTIVE` pragma is unsafe.
SafeFlagNoCoverageCheck Range	`NON_COVERING` pragma is unsafe.
SafeFlagNoPositivityCheck Range	`NO_POSITIVITY_CHECK` pragma is unsafe.
SafeFlagNoUniverseCheck Range	`NO_UNIVERSE_CHECK` pragma is unsafe.
SafeFlagNonTerminating Range	`NON_TERMINATING` pragma is unsafe.
SafeFlagPolarity Range	`POLARITY` pragma is unsafe.
SafeFlagTerminating Range	`TERMINATING` pragma is unsafe.
ShadowingInTelescope (List1 (Name, List2 Range))
UnknownFixityInMixfixDecl [Name]
UnknownNamesInFixityDecl [Name]
UnknownNamesInPolarityPragmas [Name]
UselessAbstract KwRange	`abstract` block with nothing that can (newly) be made abstract.
UselessInstance KwRange	`instance` block with nothing that can (newly) become an instance.
UselessMacro KwRange	`macro` block with nothing that can (newly) be made macro.
UselessPrivate KwRange	`private` block with nothing that can (newly) be made private.

Instances

Instances details

Pretty DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationWarning' -> Doc Source #

prettyPrec :: Int -> DeclarationWarning' -> Doc Source #

prettyList :: [DeclarationWarning'] -> Doc Source #

HasRange DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationWarning' -> Range Source #

EmbPrj DeclarationWarning' Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning' -> S Int32 Source #

icod_ :: DeclarationWarning' -> S Int32 Source #

value :: Int32 -> R DeclarationWarning' Source #

NFData DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning' -> ()

Generic DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationWarning'

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning' = D1 ('MetaData "DeclarationWarning'" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.20240731-inplace" 'False) (((((C1 ('MetaCons "EmptyAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "EmptyField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "EmptyGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))))) :+: ((C1 ('MetaCons "EmptyMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "EmptyPostulate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "EmptyPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyPrimitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)))))) :+: (((C1 ('MetaCons "HiddenGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidCatchallPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "InvalidConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "InvalidConstructorBlock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidCoverageCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "InvalidNoPositivityCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "InvalidNoUniverseCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidTerminationCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "MissingDeclarations" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Range)])) :+: (C1 ('MetaCons "MissingDefinitions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Range)])) :+: C1 ('MetaCons "NotAllowedInMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))))) :+: ((((C1 ('MetaCons "OpenPublicPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "OpenPublicAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "PolarityPragmasButNotPostulates" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "PragmaNoTerminationCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "PragmaCompiled" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "SafeFlagEta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagInjective" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "SafeFlagNoCoverageCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "SafeFlagNoPositivityCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagNoUniverseCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))) :+: (((C1 ('MetaCons "SafeFlagNonTerminating" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagPolarity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "SafeFlagTerminating" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, List2 Range)))) :+: C1 ('MetaCons "UnknownFixityInMixfixDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))))) :+: ((C1 ('MetaCons "UnknownNamesInFixityDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "UnknownNamesInPolarityPragmas" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "UselessAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)))) :+: (C1 ('MetaCons "UselessInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "UselessMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "UselessPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))))))))

Methods

from :: DeclarationWarning' -> Rep DeclarationWarning' x

to :: Rep DeclarationWarning' x -> DeclarationWarning'

Show DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

showsPrec :: Int -> DeclarationWarning' -> ShowS

show :: DeclarationWarning' -> String

showList :: [DeclarationWarning'] -> ShowS

type Rep DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning' = D1 ('MetaData "DeclarationWarning'" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.20240731-inplace" 'False) (((((C1 ('MetaCons "EmptyAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "EmptyField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "EmptyGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))))) :+: ((C1 ('MetaCons "EmptyMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "EmptyPostulate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "EmptyPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "EmptyPrimitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)))))) :+: (((C1 ('MetaCons "HiddenGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidCatchallPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "InvalidConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "InvalidConstructorBlock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidCoverageCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "InvalidNoPositivityCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "InvalidNoUniverseCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidTerminationCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "MissingDeclarations" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Range)])) :+: (C1 ('MetaCons "MissingDefinitions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Range)])) :+: C1 ('MetaCons "NotAllowedInMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))))) :+: ((((C1 ('MetaCons "OpenPublicPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "OpenPublicAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "PolarityPragmasButNotPostulates" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "PragmaNoTerminationCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "PragmaCompiled" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "SafeFlagEta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagInjective" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "SafeFlagNoCoverageCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "SafeFlagNoPositivityCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagNoUniverseCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))) :+: (((C1 ('MetaCons "SafeFlagNonTerminating" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "SafeFlagPolarity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "SafeFlagTerminating" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, List2 Range)))) :+: C1 ('MetaCons "UnknownFixityInMixfixDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))))) :+: ((C1 ('MetaCons "UnknownNamesInFixityDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "UnknownNamesInPolarityPragmas" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "UselessAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)))) :+: (C1 ('MetaCons "UselessInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: (C1 ('MetaCons "UselessMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "UselessPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))))))))

declarationWarningName :: DeclarationWarning -> WarningName Source #

declarationWarningName' :: DeclarationWarning' -> WarningName Source #

unsafeDeclarationWarning :: DeclarationWarning -> Bool Source #

Nicifier warnings turned into errors in --safe mode.

unsafeDeclarationWarning' :: DeclarationWarning' -> Bool Source #

unsafePragma :: CMaybe DeclarationWarning' m => Pragma -> m Source #

Pragmas not allowed in --safe mode produce an unsafeDeclarationWarning.