| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Concrete.Definitions.Errors
Synopsis
- data DeclarationException = 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 {}
- 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 | |
Instances
| HasRange DeclarationException Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationException -> Range Source # | |
| MonadError DeclarationException Nice Source # | |
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 ( |
| AmbiguousConstructor Range Name [Name] | In an interleaved mutual block, a constructor could belong to any of the data signatures ( |
| 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 |
|
| 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
| Pretty DeclarationException' Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Errors Methods pretty :: DeclarationException' -> Doc Source # prettyPrec :: Int -> DeclarationException' -> Doc Source # prettyList :: [DeclarationException'] -> Doc Source # | |
| HasRange DeclarationException' Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Errors Methods | |
| Show DeclarationException' Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Errors Methods showsPrec :: Int -> DeclarationException' -> ShowS # show :: DeclarationException' -> String # showList :: [DeclarationException'] -> ShowS # | |
data DeclarationWarning Source #
Constructors
| DeclarationWarning | |
Fields | |
Instances
data DeclarationWarning' Source #
Non-fatal errors encountered in the Nicifier.
Constructors
| EmptyAbstract Range | Empty |
| EmptyConstructor Range | Empty |
| EmptyField Range | Empty |
| EmptyGeneralize Range | Empty |
| EmptyInstance Range | Empty |
| EmptyMacro Range | Empty |
| EmptyMutual Range | Empty |
| EmptyPostulate Range | Empty |
| EmptyPrivate Range | Empty |
| EmptyPrimitive Range | Empty |
| HiddenGeneralize Range | A |
| 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 |
|
| OpenPublicAbstract Range |
|
| PolarityPragmasButNotPostulates [Name] | |
| PragmaNoTerminationCheck Range | Pragma |
| 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 |
|
Instances
unsafeDeclarationWarning :: DeclarationWarning -> Bool Source #
Nicifier warnings turned into errors in --safe mode.
unsafePragma :: CMaybe DeclarationWarning' m => Pragma -> m Source #
Pragmas not allowed in --safe mode produce an unsafeDeclarationWarning.