Diagnostic codes

Every compiler diagnostic carries a stable code:

error<E400>: Type mismatch: expected 'Int', found 'List<Int>'
  --> src/main.vr:5:18
   │
 5 │     let y: Int = xs;
   │                  ^^

This page covers the codes you are most likely to meet, not all of them — the compiler's own registry holds considerably more, and verum explain <code> prints the description for any code, listed here or not.

Codes are grouped by category, and the number range tells you which phase rejected the program. That is often enough to know where to look: an E1xx means the compiler could not find a name, so the problem is a mount or a spelling; an E4xx means it found everything and the types disagree.

Range	Category	Phase
E0xx	Parse	Lexing and parsing
E1xx	Name resolution	Binding names to declarations
E2xx	Module	mount resolution and visibility
E3xx	Memory	CBGR: moves, borrows, lifetimes
E4xx	Type	Inference, unification, protocols
E5xx	Verification	Contracts, refinements, SMT
E6xx	Context	The using [...] dependency system
E7xx	Async	Futures, tasks, cancellation
E8xx	FFI	Foreign boundary and ABI
E9xx	Internal	Compiler bugs — please report

Four-digit codes are a different scheme

A code with FOUR digits after the E does not follow the table above, and reading it as if it did sends you to the wrong phase: E0101 is a memory error, not a parse error.

error<E0101>: use-after-free detected          ← memory, not E0xx parse
error<E0900>: denied lint: unstable intrinsic  ← lint, a category the
                                                 three-digit table has no
                                                 range for at all

Range	Category	Codes	Example
E00xx	Parse / Internal	11	E0001 expected function body or semicolon
E01xx	Memory	3	E0101 use-after-free detected
E02xx	Type	5	E0203 ? operand error type does not convert
E03xx	Type / Context / Verification	19	E0307 advanced protocol constraint unsatisfied
E04xx	Module / Name / Parse / Type	9	E0401 stdlib bootstrap could not resolve a module surface
E05xx	Lint / Verification	2	E0500 denied lint (general)
E06xx	Type	2	E0601 non-exhaustive patterns
E07xx	Context / Internal	3	E0700 VBC codegen received the wrong input form
E08xx	Context / Internal	4	E0800 VBC monomorphization received the wrong input form
E09xx	Lint	7	E0900 denied lint: unstable intrinsic
E10xx	Lint	6	E1000 denied lint: unused stage

The parse family is hexadecimal

Forty-eight codes carry a LETTER where you expect a digit — E0A0 through E0E2. They are not typos. The parse family is numbered in HEXADECIMAL, and has been all along: E010 is parse error 16, not 10, and E0E2 is parse error 226. Below E0A0 every code is spelled with digits alone, so nothing on the page gives the base away — which is why the family reads as decimal right up until it does not.

Every one of the 48 is a parse error, so the E0xx row of the first table is still the right place to look.

error<E0E2>: Parse error: 'assert!' is Rust macro syntax, not valid in Verum
  help: did you mean `assert(...) (without !)`?

Range	Count	First	Last
E0Axx	13	E0A0 throw without expression	E0AC invalid yield
E0Bxx	16	E0B0 generic type args unclosed angle	E0BF invalid unary op
E0Cxx	10	E0C0 tagged literal missing string	E0C9 invalid let pattern
E0Dxx	6	E0D0 trailing separator	E0D5 empty shape params
E0Exx	3	E0E0 rust keyword used	E0E2 rust macro syntax

The E0Exx range is the Rust-migration range, and it is exactly three codes wide — a Rust keyword (E0E0), a Rust type name (E0E1), a name!(...) macro call (E0E2). They are the only three codes in the whole registry whose description mentions Rust at all.

The registry contains 361 codes in all — 202 three-digit, 111 four-digit, 48 hexadecimal. The sections below cover the three-digit families, which are the ones ordinary programs hit; for any code in any of the three schemes, verum explain <code> prints its entry, and for E0E2 it prints the whole Rust-to-Verum mapping table.

Parse — E0xx

Code	Meaning	Emitted?
E001	unterminated character literal	yes
E002	invalid escape sequence	yes
E003	invalid number literal	yes
E004	empty character literal	yes
E005	invalid interpolation syntax	yes
E006	unknown token/character	yes
E007	invalid float literal	no

E007 is a registry entry with no emit site: a malformed float is reported by the integer-literal code or by E001 on the token that follows it. Cited here because the code exists and a reader searching for it should learn that, not wonder why it never appears.

A parse error worth calling out separately, because it reads oddly the first time: putting a record literal directly in a match scrutinee makes the parser take the literal's { as the match body.

match Shape.Rect { w: 3, h: 4 } { ... }   // E087 / E018
let s = Shape.Rect { w: 3, h: 4 };        // bind first
match s { ... }

Name resolution — E1xx

Code	Meaning	Emitted?
E100	undefined variable	yes
E101	type not found — no declaration of that name is in scope	yes
E102	wrong number of arguments to a function or method	yes
E103	field not found on type	yes
E104	duplicate definition	no
E105	ambiguous name — it could refer to several protocols, or be imported from more than one module	yes
E106	unresolved type placeholder	yes

E104 has no emit site — a redeclaration is reported by the type codes. E106 was missing from this table and does fire: it is the one you get when a type is referenced but never defined, as distinct from E101 (undefined type at a use site).

E102 also covers calling a function with too few arguments — the message names the arity:

error<E102>: Function requires at least 5 arguments, got 4 (calling `verify_pss_prehashed`)

E103 is the one to read carefully when a field name looks right. It means the type has no such field — usually a rename the call site never followed (pre_release vs prerelease, peer_addr vs peer).

Module — E2xx

Code	Meaning	Emitted?
E200	import not found	no — see below
E201	circular import	yes
E202	visibility error — the named item is not visible from this module	yes
E203	module not found	no — see below
E204	circular constant dependency	yes

Three of these four never fire

only E201 has an emit site. E200, E202 and E203 are registry entries that nothing produces, and the conditions they name are reported by the type codes instead:

mount core.zzz.nothing;                      // error<E402>: module `core.zzz` not found
mount core.collections.list.{NoSuchSymbol};  // error<E401>: cannot find `NoSuchSymbol` in module …

So a reader who meets "module not found" and looks up E203 finds a code the compiler will never show them, while the one they did see — E402 — is filed under Type below, described as "module not found; also Send not implemented, and …". One code, several jobs.

E202 fires for nothing because import privacy is not enforced at all: the five-level visibility table in language/modules is documentation of an intent, not of a check.

Memory — E3xx

Code	Meaning
E310	borrow conflict; also use after move, an invalid index, and a &checked reference that may escape
E311	field already borrowed — cannot borrow while a field of it is
E312	lifetime error
E313	cannot move a value while it is borrowed
E314	borrow conflict
E302	affine value used in a loop
E303	linear value not consumed exactly once
E304	affine value used more than once
E305	use of an uninitialized or partially initialized value
E306	capability violation
E320	stack allocation exceeds the safe limit
E321	unbounded recursion detected
E370	positivity violation in a recursive type

See CBGR for the three-tier reference model these diagnostics enforce.

Type — E4xx

Four of these carry more than one meaning. The table gives the registry's own wording, because the second meaning is usually the one you will meet:

Code	Meaning
E400	type mismatch
E401	a name is not found in the module named; also an invalid assignment or cast
E402	module not found; also Send not implemented, and mixed Int/Float arithmetic
E403	infinite (self-referential) type; also Sync not implemented, and undefined function
E404	inferred type is not fully determined — annotate it; also a missing protocol implementation, and an unknown field or method
E405	protocol method not implemented
E406	type inference failure
E407	recursive type without indirection
E408	dependent value-argument arity mismatch
E412	value is not a function
E413	const generic parameter mismatch
E414	ambiguous type: not inferable without more context
E415	name is not a type
E416	? used outside a function
E417	cycle among type definitions
E418	existential type escapes its scope
E419	existential bound not satisfied
E420	kind mismatch
E421	type constructor arity mismatch
E422	associated type cannot be resolved
E423	ambiguous associated type
E424	negative bound violated
E425	specialization overlap
E426	higher-kinded bound not satisfied
E429	a refutable pattern in a position that must always match

E429 — the pattern has to match

Three positions bind exactly once against exactly one value, so a pattern used there must match every time: a function parameter (matched against whatever the caller passes), a plain let, and a comprehension's let clause (bound once per row).

let n = 5;
let 7 = n;                       // E429: a literal matches one value of many
let 1..=9 = n;                   // E429: a range, same objection
let 1 | 2 = n;                   // E429: an or-pattern, an alternative can fail

set{ y for x in xs let 7 = x }   // E429: the clause binds once per row

The refutable case has its own form — let … else { … } — and a comprehension filters with an if clause BEFORE it binds:

let Maybe.Some(x) = v else { return; };            // fine

set{ pair.1
     for email in addresses
     if email.split_once(&"@") is Maybe.Some(_)    // filter first
     let pair = email.split_once(&"@").unwrap() }  // then bind

A variant pattern is not yet caught

let Maybe.Some(x) = v; without an else is still accepted, and binds an unchecked payload — reading a field of x then dereferences null. Deciding refutability for a variant needs the resolved type, and the check that raises E429 works on the pattern's syntax: a single-variant newtype destructured by name (let UserId(n) = id;) always matches and must stay legal. Until that half lands, write let … else whenever the type has more than one variant.

A code with three meanings cannot be looked up the way this page is meant to be used — you read the message, not the number. The overload is why E200/E203 above are dead: their conditions were folded into E401/E402 and the module namespace was left standing.

E400 is the most common diagnostic in the language, and its message always names both sides. Three shapes are worth recognising:

A container is not its element.

let mut xs: List<Int> = List.new();
let y: Int = xs;
// error<E400>: Type mismatch: expected 'Int', found 'List<Int>'

Indexing yields the element — let y: Int = xs[0]; — and xs.len() yields a count. A collection never stands in for an integer. See Coercion markers for which types may stand in for which, and why containers are excluded.

A sum type is not its payload.

let m: Maybe<Int> = xs.first();
let z: Int = m;
// error<E400>: Type mismatch: expected 'Int', found 'None(Unit) | Some(Int)'

Unwrap it deliberately — match, unwrap_or, ? — so the absent case has an answer.

A Maybe wrapped twice.

fn head(xs: &List<Int>) -> Maybe<Int> {
    Maybe.Some(xs.first())   // xs.first() is ALREADY Maybe<Int>
}
// error<E400>: Type mismatch: expected 'Int', found 'Maybe<Int>'

The fix is to return xs.first() directly.

E407 means a type contains itself with no indirection — a value of it would need infinite size. Insert Heap<T>, which puts the recursive occurrence behind an allocation:

type Tree is Leaf(Int) | Node { left: Heap<Tree>, right: Heap<Tree> };

let t = Tree.Node { left: Heap(Tree.Leaf(1)), right: Heap(Tree.Leaf(2)) };
match t {
    Leaf(v)             => print(v),
    Node { left, right } => print(0),
}

Note that a recursive walk over such a tree needs the Heap opened before the child is passed on — passing left where a &Tree is expected is an E400, not an E407.

Verification — E5xx

Code	Meaning
E500	contract violated
E501	invalid refinement predicate; also: a meta function declared pure has side effects
E502	a meta function uses runtime contexts, which are not available at compile time
E503	a pure function has side effects
E504	.await used outside an async context
E505	corecursive function is non-productive
E506	meta argument violates its refinement

E501 is a rejection of your program, and this paragraph used to say the opposite — that the solver had run out of budget. That was the registry's wording, not the compiler's. The code has exactly two emit sites and neither mentions a timeout:

grep -rn 'invalid refinement predicate' crates/verum_types/src/lib.rs
grep -rn 'must be pure but has side effects' crates/verum_types/src/lib.rs

Grepping for the code itself is the obvious command and the wrong one: .code("E501") and the message it carries sit on different lines, so a line-oriented search shows you the code without the text or the text without the code. The two messages above are what the emit sites build.

So read it as "the predicate itself is not a valid refinement", or as a purity violation in a meta function. See Refinement types.

E504 was corrected in the same pass and for the same reason. The registry calls it "postcondition not established"; its single producer in the type checker reports

`.await` can only be used inside an async context (async fn, async block, or async closure)

which is what a reader will actually see. That one is invisible to the site's error-code gate, because the message is assembled as format!("E504: {}", message) with the text supplied from elsewhere — worth knowing if you are relying on that gate to catch this class.

Context — E6xx

Code	Meaning	Emitted?
E600	context not provided	yes
E601	context conflict	no
E602	context cycle	no
E603	context mismatch	yes
E604	context not allowed here	yes
E605	undefined context	yes
E606	context has no such method	yes
E607	invalid sub-context	yes
E608	excluded context used	yes
E609	transitive negative-context violation	yes
E610	non-context protocol in a using clause	yes
E611	direct negative-context violation	yes
E612	context alias conflict	yes
E613	context used but not declared in the function signature	yes

E600 means a function declared using [Database] was called from a scope with no provide for it. See Context system.

E601 and E602 are reserved rather than live. Both used to be emitted — but for conditions belonging to other categories: E601 reported a visibility violation and E602 an ambiguous name, neither of which is a context error. They now report under the codes that already meant them, E202 and E105, so the range contract this page opens with — E1xx a name, E6xx the context system — holds for them too. Nothing emits E601 or E602 today.

Async — E7xx, FFI — E8xx, Internal — E9xx

None of these nine has an emit site

every code below is a registry entry that no part of the compiler produces. Three whole categories are reserved rather than live.

Code	Meaning	Emitted?
E700	future cancelled unexpectedly	no
E701	async boundary violation	no
E702	task join error	no
E800	unsafe FFI violation	no
E801	ABI mismatch	no
E802	null pointer dereference in FFI	no
E803	invalid type for an inline-assembly const operand	yes
E804	inline-assembly output operand is not an lvalue	yes
E808	duplicate provide for one context	yes
E900	internal compiler error	no
E901	compiler assertion failed	no
E902	unexpected compiler state	no

They are listed because the registry has them and verum --explain will answer for them — not because a program can provoke one. An async misuse or an FFI mistake surfaces today as an ordinary E4xx type error, and an internal failure as a panic with a backtrace rather than a coded diagnostic.

make check-doc-error-codes holds this at fourteen cited-but-unemitted codes, so the list cannot quietly grow.

An E9xx, if one ever appears, is a compiler bug and never a problem with your program. Report it with the smallest input that reproduces it.

Reading a diagnostic

Three habits pay off:

1. Read both type names in an E400, not just the first. The message prints expected (what the context demands) then found (what the expression produced). Which of the two is wrong is your judgement, and the answer is not always "the expression".
2. Trust the caret over the line. Context lines are shown for orientation; the ^^^^ marks the sub-expression that failed.
3. An E1xx before an E4xx usually explains it. A name the compiler could not resolve degrades everything downstream of it. Fix the first diagnostic and re-run before reading the rest.