Agda.Syntax.Concrete.Definitions.Errors

Documentation

data DeclarationException

Exception with internal source code callstack

Constructors

DeclarationException

Fields

• deLocation :: CallStack
• deException :: DeclarationException'

Instances

HasRange DeclarationException

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationException -> Range

MonadError DeclarationException Nice

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

throwError :: DeclarationException -> Nice a

catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a

data DeclarationException'

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

Pretty DeclarationException'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationException' -> Doc

prettyPrec :: Int -> DeclarationException' -> Doc

prettyList :: [DeclarationException'] -> Doc

HasRange DeclarationException'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationException' -> Range

Show DeclarationException'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

showsPrec :: Int -> DeclarationException' -> ShowS

show :: DeclarationException' -> String

showList :: [DeclarationException'] -> ShowS

data DeclarationWarning

Constructors

DeclarationWarning

Fields

• dwLocation :: CallStack
• dwWarning :: DeclarationWarning'

Instances

Pretty DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationWarning -> Doc

prettyPrec :: Int -> DeclarationWarning -> Doc

prettyList :: [DeclarationWarning] -> Doc

HasRange DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationWarning -> Range

EmbPrj DeclarationWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning -> S Int32

icod_ :: DeclarationWarning -> S Int32

value :: Int32 -> R DeclarationWarning

Generic DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationWarning :: Type -> Type

Methods

from :: DeclarationWarning -> Rep DeclarationWarning x

to :: Rep DeclarationWarning x -> DeclarationWarning

Show DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

showsPrec :: Int -> DeclarationWarning -> ShowS

show :: DeclarationWarning -> String

showList :: [DeclarationWarning] -> ShowS

NFData DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning -> ()

type Rep DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning = D1 ('MetaData "DeclarationWarning" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.3.20230930-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'

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.

Instances

Pretty DeclarationWarning'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationWarning' -> Doc

prettyPrec :: Int -> DeclarationWarning' -> Doc

prettyList :: [DeclarationWarning'] -> Doc

HasRange DeclarationWarning'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationWarning' -> Range

EmbPrj DeclarationWarning'

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning' -> S Int32

icod_ :: DeclarationWarning' -> S Int32

value :: Int32 -> R DeclarationWarning'

Generic DeclarationWarning'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationWarning' :: Type -> Type

Methods

from :: DeclarationWarning' -> Rep DeclarationWarning' x

to :: Rep DeclarationWarning' x -> DeclarationWarning'

Show DeclarationWarning'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

showsPrec :: Int -> DeclarationWarning' -> ShowS

show :: DeclarationWarning' -> String

showList :: [DeclarationWarning'] -> ShowS

NFData DeclarationWarning'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning' -> ()

type Rep DeclarationWarning'

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning' = D1 ('MetaData "DeclarationWarning'" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.3.20230930-inplace" 'False) (((((C1 ('MetaCons "EmptyAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "EmptyField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "EmptyGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "EmptyMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "EmptyPostulate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "EmptyPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyPrimitive" '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 "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 "InvalidRecordDirective" '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 Range))) :+: (C1 ('MetaCons "OpenPublicAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (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 Range)) :+: (C1 ('MetaCons "UselessInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "UselessPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))))))

declarationWarningName :: DeclarationWarning -> WarningName

declarationWarningName' :: DeclarationWarning' -> WarningName

unsafeDeclarationWarning :: DeclarationWarning -> Bool

Nicifier warnings turned into errors in --safe mode.

unsafeDeclarationWarning' :: DeclarationWarning' -> Bool

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

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