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 Range
- | OpaqueInMutual Range
- | DisallowedInterleavedMutual Range String (List1 Name)
data DeclarationWarning = DeclarationWarning {
- dwLocation :: CallStack
- dwWarning :: DeclarationWarning'
}
data DeclarationWarning'
- = EmptyAbstract Range
- | EmptyConstructor Range
- | EmptyField Range
- | EmptyGeneralize Range
- | EmptyInstance Range
- | EmptyMacro Range
- | EmptyMutual Range
- | EmptyPostulate Range
- | EmptyPrivate Range
- | EmptyPrimitive Range
- | HiddenGeneralize Range
- | InvalidCatchallPragma Range
- | InvalidConstructor Range
- | InvalidConstructorBlock Range
- | InvalidCoverageCheckPragma Range
- | InvalidNoPositivityCheckPragma Range
- | InvalidNoUniverseCheckPragma Range
- | InvalidRecordDirective Range
- | InvalidTerminationCheckPragma Range
- | MissingDeclarations [(Name, Range)]
- | MissingDefinitions [(Name, Range)]
- | NotAllowedInMutual Range String
- | OpenPublicPrivate Range
- | OpenPublicAbstract Range
- | 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 Range
- | UselessInstance Range
- | UselessPrivate Range
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 Source #
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 of mutual block.
UnquoteDefRequiresSignature (List1 Name)
BadMacroDef NiceDeclaration
UnfoldingOutsideOpaque Range	An unfolding declaration was not the first declaration contained in an opaque block.
OpaqueInMutual Range	`opaque` block nested in a `mutual` block. This can never happen, even with reordering.
DisallowedInterleavedMutual Range 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 #

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.4.2-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 #

NFData DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning -> () #

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.4.2-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 Range	Empty `abstract` block.
EmptyConstructor Range	Empty `constructor` block.
EmptyField Range	Empty `field` block.
EmptyGeneralize Range	Empty `variable` block.
EmptyInstance Range	Empty `instance` block
EmptyMacro Range	Empty `macro` block.
EmptyMutual Range	Empty `mutual` block.
EmptyPostulate Range	Empty `postulate` block.
EmptyPrivate Range	Empty `private` block.
EmptyPrimitive Range	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.
InvalidRecordDirective Range	A record directive outside of a record / below existing fields.
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 Range	`private` has no effect on `open public`. (But the user might think so.)
OpenPublicAbstract Range	`abstract` has no effect on `open public`. (But the user might think so.)
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 Range	`abstract` block with nothing that can (newly) be made abstract.
UselessInstance Range	`instance` block with nothing that can (newly) become an instance.
UselessPrivate Range	`private` block with nothing that can (newly) be made private.