Agda.Compiler.Backend

The first argument is the state in which the error was raised.

The exception which is usually caught. Raised for pattern violations during unification (assignV) but also in other situations where we want to backtrack. Contains an unblocker to control when the computation should be retried.

BUILTIN REWRITE. We can have several rewrite relations.

Never a Section or ScopeDecl

Meta variables of record type.

Meta variables of "hereditarily singleton" record type.

Meta variables of level type, if type-in-type is activated.

This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked.

Via stdout.

Both via files and via stdout.

monotone

antitone

no information (mixed variance)

constant

Check that the sort Sort of data type QName admits data/record types. E.g., sorts IUniv, SizeUniv etc. do not admit such constructions. See checkDataSort.

Meta created for a term blocked by a postponed type checking problem or unsolved constraints. The MetaInstantiation for the meta (when unsolved) is either BlockedConst or PostponedTypeCheckingProblem.

The range is the one of the absurd pattern.

Check that the Term is either not a SIZELT or a non-empty SIZELT.

the first argument is the instance argument and the second one is the list of candidates (or Nothing if we haven’t determined the list of candidates yet)

Resolve the head symbol of the type that the given instance targets

Last argument is the error causing us to postpone.

First argument is computation and the others are hole and goal type

CheckLockedVars t ty lk lk_ty with t : ty, lk : lk_ty and t lk well-typed.

Is the term usable at the given modality? This check should run if the Sort is Nothing or isFibrant.

`UnreachableClauses f rs` means that the clauses in f whose ranges are rs are unreachable

`CoverageIssue f pss` means that pss are not covered in f

Clause was turned into copattern matching clause(s) by an {-# INLINE constructor #-} and thus is not a definitional equality any more.

Checking whether constructor QName Sort fits into data Sort produced TCErr

A record type declared as both coinductive and having eta-equality.

Do not use directly with warning

Do not use directly with warning

Do not use directly with warning

Do not use directly with warning

In `OldBuiltin old new`, the BUILTIN old has been replaced by new.

The builtin declares a new identifier, so it should not be in scope.

The given record directive is conflicting with a prior one in the same record declaration.

If the user wrote just {-# REWRITE #-}.

An empty where block is dead code.

If the user wrote something other than an unqualified name in the as clause of an import statement. The String gives optionally extra explanation.

A character literal Agda does not support, e.g. surrogate code points.

If a renaming import directive introduces a name or module name clash in the exported names of a module. (See issue #4154.)

The pattern declaration is useless in the presence of either coinductive or eta-equality. Content of String is "coinductive" or "eta", resp.

Warning when pragma is useless and thus ignored. Range is for dead code highlighting.

If the user opens a module public before the module header. (See issue #2377.)

Names in hiding directive that don't hide anything imported by a using directive.

An instance was declared with an implicit argument, which means it will never actually be considered by instance search.

The type of an instance argument doesn't end in a named or variable type, so it will never be considered by instance search.

As InstanceWithExplicitArg, but for local bindings rather than top-level instances.

The --inversion-max-depth was reached.

A coinductive record was declared but neither --guardedness nor --sized-types is enabled.

Unsafe OPTIONS.

`ConflictingPragmaOptions a b`: Inconsistent options `--a` and `--no-b`, since `--a` implies `--b`. Ignoring `--no-b`.

`DeprecationWarning old new version`: old is deprecated, use new instead. This will be an error in Agda version.

User-defined warning (e.g. to mention that a name is deprecated)

Duplicate mentions of the same name in using directive(s).

Fixity of modules cannot be changed via renaming (since modules have no fixity).

Some imported names are not actually exported by the source module. The second argument is the names that could be exported. The third argument is the module names that could be exported.

Importing a file using an infective option into one which doesn't

Importing a file not using a coinfective option from one which does

Confluence checking incomplete because the definition of the QName contains unsolved metavariables.

Confluence checking with --cubical might be incomplete.

Confluence checker found critical pair and equality checking resulted in a type error

Confluence checker got stuck on computing overlap between two rewrite rules

The global confluence checker found a term u that reduces to both v1 and v2 and there is no rule to resolve the ambiguity.

The global confluence checker found a term u that reduces to v, but v does not reduce to rho(u).

COMPILE directive for an erased symbol.

COMPILE GHC pragma for lists; ignored.

COMPILE GHC pragma for MAYBE; ignored.

Compiler run on module that does not have a main function.

Out of scope error we can recover from.

Was not able to compute a full equivalence when splitting.

The as-name in an as-pattern may not shadow a constructor (IsLHS) or pattern synonym name (IsPatSyn), because this can be confusing to read.

A pattern variable has the name of a constructor (data constructor or matchable record constructor).

Explicit use of @ω or @plenty in hard compile-time mode.

An abstract or opaque definition lacks a type signature.

Face constraint patterns (i = 0) must be visible arguments.

Face constraint patterns (i = 0) must be unnamed arguments.

`DuplicateInterfaceFiles selectedInterfaceFile ignoredInterfaceFile`

Used for backend-specific warnings. The string is the backend name.