Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Concrete.Definitions.Errors

Synopsis

- data DeclarationException = DeclarationException {
  - deLocation :: CallStack
  - deException :: DeclarationException'
  }
- data DeclarationException'
  - = MultipleEllipses Pattern
  - | DuplicateDefinition Name
  - | DuplicateAnonDeclaration Range
  - | MissingWithClauses Name LHS
  - | WrongDefinition Name DataRecOrFun DataRecOrFun
  - | 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)
- declarationExceptionString :: DeclarationException' -> String
- 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
  - | EmptyPolarityPragma Range
  - | HiddenGeneralize Range
  - | InvalidCatchallPragma Range
  - | InvalidConstructorBlock Range
  - | InvalidCoverageCheckPragma Range
  - | InvalidNoPositivityCheckPragma Range
  - | InvalidNoUniverseCheckPragma Range
  - | InvalidTerminationCheckPragma Range
  - | MissingDataDeclaration Name
  - | MissingDefinitions (List1 (Name, Range))
  - | NotAllowedInMutual Range String
  - | OpenImportPrivate Range KwRange KwRange OpenOrImport
  - | OpenImportAbstract Range KwRange OpenOrImport
  - | PolarityPragmasButNotPostulates (Set1 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 (Set1 Name)
  - | UnknownNamesInFixityDecl (Set1 Name)
  - | UnknownNamesInPolarityPragmas (Set1 Name)
  - | UselessAbstract KwRange
  - | UselessInstance KwRange
  - | UselessMacro KwRange
  - | UselessPrivate KwRange
- data OpenOrImport
  - = OpenNotImport
  - | ImportMayOpen
- 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 Source # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a Source #

data DeclarationException' Source #

The exception type.

Constructors

MultipleEllipses Pattern |
DuplicateDefinition Name |
DuplicateAnonDeclaration Range |
MissingWithClauses Name LHS |
WrongDefinition Name DataRecOrFun DataRecOrFun |
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 #
NFData DeclarationException' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods rnf :: DeclarationException' -> () Source #
Generic DeclarationException' Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationException' |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationException' = D1 ('MetaData "DeclarationException'" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "MultipleEllipses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern)) :+: (C1 ('MetaCons "DuplicateDefinition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "DuplicateAnonDeclaration" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "MissingWithClauses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHS)) :+: C1 ('MetaCons "WrongDefinition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataRecOrFun) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataRecOrFun)))) :+: (C1 ('MetaCons "WrongContentBlock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfBlock) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "AmbiguousFunClauses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHS) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Name)))))) :+: ((C1 ('MetaCons "AmbiguousConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))) :+: (C1 ('MetaCons "InvalidMeasureMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "UnquoteDefRequiresSignature" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Name))))) :+: ((C1 ('MetaCons "BadMacroDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NiceDeclaration)) :+: C1 ('MetaCons "UnfoldingOutsideOpaque" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "OpaqueInMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "DisallowedInterleavedMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Name))))))))

Methods

from :: DeclarationException' -> Rep DeclarationException' x Source #

to :: Rep DeclarationException' x -> DeclarationException' Source #

Show DeclarationException' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods showsPrec :: Int -> DeclarationException' -> ShowS Source # show :: DeclarationException' -> String Source # showList :: [DeclarationException'] -> ShowS Source #
type Rep DeclarationException' Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationException' = D1 ('MetaData "DeclarationException'" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "MultipleEllipses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern)) :+: (C1 ('MetaCons "DuplicateDefinition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "DuplicateAnonDeclaration" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "MissingWithClauses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHS)) :+: C1 ('MetaCons "WrongDefinition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataRecOrFun) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataRecOrFun)))) :+: (C1 ('MetaCons "WrongContentBlock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfBlock) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "AmbiguousFunClauses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHS) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Name)))))) :+: ((C1 ('MetaCons "AmbiguousConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))) :+: (C1 ('MetaCons "InvalidMeasureMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "UnquoteDefRequiresSignature" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Name))))) :+: ((C1 ('MetaCons "BadMacroDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NiceDeclaration)) :+: C1 ('MetaCons "UnfoldingOutsideOpaque" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange))) :+: (C1 ('MetaCons "OpaqueInMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "DisallowedInterleavedMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Name))))))))

declarationExceptionString :: DeclarationException' -> String Source #

The name of the error.

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 Word32 Source # icod_ :: DeclarationWarning -> S Word32 Source # value :: Word32 -> R DeclarationWarning Source #
NFData DeclarationWarning Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods rnf :: 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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep DeclarationWarning x -> DeclarationWarning Source #

Show DeclarationWarning Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods showsPrec :: Int -> DeclarationWarning -> ShowS Source # show :: DeclarationWarning -> String Source # showList :: [DeclarationWarning] -> ShowS Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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.
EmptyPolarityPragma Range | POLARITY pragma without any polarities.
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.
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.
MissingDataDeclaration Name | A `data` definition without a `data` signature.
MissingDefinitions (List1 (Name, Range)) | Declarations (e.g. type signatures) without a definition.
NotAllowedInMutual Range String |
OpenImportPrivate Range KwRange KwRange OpenOrImport | `private` has no effect on `open (import) public`. (But the user might think so.) `Range` is the range of the `open public` or `open import public` declaration. The first `KwRange` is the range of the `public` keyword. The second `KwRange` is the range of the `private` keyword.
OpenImportAbstract Range KwRange OpenOrImport | `abstract` has no effect on `open` or `import`. (But the user might think so.) `Range` is the range of the `open` or `import` declaration. `KwRange` is the range of the `abstract` keyword.
PolarityPragmasButNotPostulates (Set1 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 (Set1 Name) | Public mixfix identifiers without a fixity declaration.
UnknownNamesInFixityDecl (Set1 Name) |
UnknownNamesInPolarityPragmas (Set1 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 Word32 Source # icod_ :: DeclarationWarning' -> S Word32 Source # value :: Word32 -> R DeclarationWarning' Source #
NFData DeclarationWarning' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods rnf :: 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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 "EmptyPolarityPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: 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 "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 "MissingDataDeclaration" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "MissingDefinitions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (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 "OpenImportPrivate" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpenOrImport))) :+: C1 ('MetaCons "OpenImportAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpenOrImport)))) :+: (C1 ('MetaCons "PolarityPragmasButNotPostulates" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set1 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 (Set1 Name)))))) :+: ((C1 ('MetaCons "UnknownNamesInFixityDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set1 Name))) :+: (C1 ('MetaCons "UnknownNamesInPolarityPragmas" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set1 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 Source #

to :: Rep DeclarationWarning' x -> DeclarationWarning' Source #

Show DeclarationWarning' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods showsPrec :: Int -> DeclarationWarning' -> ShowS Source # show :: DeclarationWarning' -> String Source # showList :: [DeclarationWarning'] -> ShowS Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 "EmptyPolarityPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: 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 "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 "MissingDataDeclaration" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "MissingDefinitions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (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 "OpenImportPrivate" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpenOrImport))) :+: C1 ('MetaCons "OpenImportAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpenOrImport)))) :+: (C1 ('MetaCons "PolarityPragmasButNotPostulates" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set1 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 (Set1 Name)))))) :+: ((C1 ('MetaCons "UnknownNamesInFixityDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set1 Name))) :+: (C1 ('MetaCons "UnknownNamesInPolarityPragmas" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set1 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))))))))

data OpenOrImport Source #

`open` or `import`

Constructors

OpenNotImport | `open`.
ImportMayOpen | `import` or `open import`.

#### Instances

Instances details

Pretty OpenOrImport Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods pretty :: OpenOrImport -> Doc Source # prettyPrec :: Int -> OpenOrImport -> Doc Source # prettyList :: [OpenOrImport] -> Doc Source #
EmbPrj OpenOrImport Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: OpenOrImport -> S Word32 Source # icod_ :: OpenOrImport -> S Word32 Source # value :: Word32 -> R OpenOrImport Source #
NFData OpenOrImport Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods rnf :: OpenOrImport -> () Source #
Bounded OpenOrImport Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods minBound :: OpenOrImport Source # maxBound :: OpenOrImport Source #
Enum OpenOrImport Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

succ :: OpenOrImport -> OpenOrImport Source #

pred :: OpenOrImport -> OpenOrImport Source #

toEnum :: Int -> OpenOrImport Source #

fromEnum :: OpenOrImport -> Int Source #

enumFrom :: OpenOrImport -> [OpenOrImport] Source #

enumFromThen :: OpenOrImport -> OpenOrImport -> [OpenOrImport] Source #

enumFromTo :: OpenOrImport -> OpenOrImport -> [OpenOrImport] Source #

enumFromThenTo :: OpenOrImport -> OpenOrImport -> OpenOrImport -> [OpenOrImport] Source #

Generic OpenOrImport Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep OpenOrImport |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors type Rep OpenOrImport = D1 ('MetaData "OpenOrImport" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "OpenNotImport" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ImportMayOpen" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: OpenOrImport -> Rep OpenOrImport x Source #

to :: Rep OpenOrImport x -> OpenOrImport Source #

Show OpenOrImport Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods showsPrec :: Int -> OpenOrImport -> ShowS Source # show :: OpenOrImport -> String Source # showList :: [OpenOrImport] -> ShowS Source #
type Rep OpenOrImport Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors type Rep OpenOrImport = D1 ('MetaData "OpenOrImport" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "OpenNotImport" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ImportMayOpen" 'PrefixI 'False) (U1 :: Type -> Type))

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`.