Agda.TypeChecking.Monad.Base

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

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.

The target of a constructor isn't an application of its datatype. The Type records what it does target.

The target of a constructor isn't its datatype applied to something that isn't the parameters. First term is the correct target and the second term is the actual target.

Expected a type to be an application of a particular datatype.

constructor, datatype

Datatype, constructors.

constructor, type

The left hand side of a function definition has a hidden argument where a non-hidden was expected.

Expected a non-hidden function and found a hidden lambda.

A function is applied to a hidden argument where a non-hidden was expected.

A function is applied to a hidden named argument it does not have. The list contains names of possible hidden arguments at this point.

Wrong user-given relevance annotation in lambda.

Wrong user-given quantity annotation in lambda.

Wrong user-given cohesion annotation in lambda.

The given quantity does not correspond to the expected quantity.

The given hiding does not correspond to the expected hiding.

The given relevance does not correspond to the expected relevane.

The given type should have been a sort.

The given type should have been a pi.

This sort is not a type expression.

This term is not a type expression.

The two function types have different relevance.

The two function types have different relevance.

The two function types have different cohesion.

One of the function types has a finite domain (i.e. is a Partial@) and the other isonot.

The two function types have different hiding.

The arguments are the meta variable and the parameter that it wants to depend on.

the meta is what we might be blocked on.

The declaration list comes from a single C.NiceDeclaration.

Record type, fields not supplied by user, non-fields but supplied.

The first term references the given list of variables, which are in "the future" with respect to the given lock (and its leftmost variable)

Arguments: later term, its type, lock term. The lock term does not mention any @lock variables.

A record type inferred as recursive needs a manual declaration whether it should be inductively or coinductively. Sized type errors

The list of constraints is given redundantly as pairs of ProblemConstraint (original constraint) and HypSizeConstraint (form with size assumptions in context spelled out). The Doc is some extra reason for why solving failed.

This type, representing a type of sizes, might be empty.

This term, a function type constructor, lives in SizeUniv, which is not allowed. Import errors

Collected errors when processing the .agda-lib file.

Some interaction points (holes) have not been filled by user. There are not UnsolvedMetas since unification solved them. This is an error, since interaction points are never filled without user interaction.

Found module name, expected module name.

Module name, file from which it was loaded, file which the include path says contains the module.

The file name does not correspond to a module name. Scope errors

The given data/record definition rests in a different module than its signature.

The expr was used in the right hand side of an implicit module definition, but it wasn't of the form m Delta.

This variable is bound in the lhs of the pattern synonym in instance position, but not on the rhs. This is forbidden because expansion of pattern synonyms would not be faithful to availability of instances in instance search.

A variable to be bound in the pattern synonym resolved on the rhs as name of a constructor or a pattern synonym. The resolvents are given in the list.

This variable is only bound on the lhs of the pattern synonym, not on the rhs.

These variables are only bound on the rhs of the pattern synonym, not on the lhs. Operator errors

The list contains patterns that failed to be interpreted. If it is non-empty, the first entry could be printed as error hint.

Pattern and its possible interpretations.

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