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.

POLARITY pragma without any polarities.

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

A data definition without a data signature.

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

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.

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.

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.

Public mixfix identifiers without a fixity declaration.

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.

open.

import or open import.