Agda.Syntax.Concrete.Definitions.Errors

In a mutual block, a clause could belong to any of the ≥2 type signatures (Name).

In an interleaved mutual block, a constructor could belong to any of the data signatures (Name)

In a mutual block, all or none need a MEASURE pragma. Range is the one of the offending pragma or the mutual block.

An unfolding declaration was not the first declaration contained in an opaque block.

opaque block nested in a mutual block. This can never happen, even with reordering. The KwRange is the one of the opaque keyword.

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.

Empty abstract block.

Empty data _ where block.

Empty field block.

Empty variable block.

Empty instance block

Empty macro block.

Empty mutual block.

Empty postulate block.

Empty private block.

Empty primitive block.

A Hidden identifier in a variable declaration. Hiding has no effect there as generalized variables are always hidden (or instance variables).

A {-# CATCHALL #-} pragma that does not precede a function clause.

Invalid definition in a constructor block

Invalid constructor block (not inside an interleaved mutual block)

A {-# NON_COVERING #-} pragma that does not apply to any function.

A {-# NO_POSITIVITY_CHECK #-} pragma that does not apply to any data or record type.

A {-# NO_UNIVERSE_CHECK #-} pragma that does not apply to a data or record type.

A {-# TERMINATING #-} and {-# NON_TERMINATING #-} pragma that does not apply to any function.

Definitions (e.g. constructors or functions) without a declaration.

Declarations (e.g. type signatures) without a definition.

private has no effect on open public. (But the user might think so.) KwRange is the range of the public keyword.

abstract has no effect on open public. (But the user might think so.) KwRange is the range of the public keyword.

Pragma {-# NO_TERMINATION_CHECK #-} has been replaced by {-# TERMINATING #-} and {-# NON_TERMINATING #-}.

COMPILE pragmas are not allowed in safe mode.

ETA pragma is unsafe.

INJECTIVE pragma is unsafe.

NON_COVERING pragma is unsafe.

NO_POSITIVITY_CHECK pragma is unsafe.

NO_UNIVERSE_CHECK pragma is unsafe.

NON_TERMINATING pragma is unsafe.

POLARITY pragma is unsafe.

TERMINATING pragma is unsafe.

abstract block with nothing that can (newly) be made abstract.

instance block with nothing that can (newly) become an instance.

macro block with nothing that can (newly) be made macro.

private block with nothing that can (newly) be made private.