Every diagnostic code the compiler can emit, with the stage that emits it and a one-line summary. This is the only place a number is bound to a meaning: each CompilerDiagnostic instance names an entry here (Diagnostics.unexpectedToken.code) rather than writing a literal, so a code that a diagnostic uses but the registry does not list cannot exist.

Numbers are allocated sequentially and are permanent: never renumbered, never reused. A diagnostic that disappears keeps its entry, marked retired, so an old build log or an old fugue explain E0042 stays meaningful. Add new diagnostics at the end.

fugue explain <code> prints docs/diagnostics/<code>.md; the summary here is what fugue explain --list shows, and what the regression runner's coverage report labels a code with.

structure Diagnostics.Entry : Type

One diagnostic's registry entry.

• code : DiagnosticCode

  Its code.

• stage : Stage

  The stage that emits it.

• warningName : String

  The -W<name> this is filtered under. Warnings only; empty for an error, which -W never suppresses.

• summary : String

  One line, imperative-free: what the diagnostic means, not how to fix it (that is what docs/diagnostics/<code>.md is for).

@[implicit_reducible]

instance Diagnostics.instReprEntry : Repr Entry

Equations

• Diagnostics.instReprEntry = { reprPrec := Diagnostics.instReprEntry.repr }

def Diagnostics.instReprEntry.repr : Entry → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Diagnostics.instInhabitedEntry : Inhabited Entry

Equations

• Diagnostics.instInhabitedEntry = { default := Diagnostics.instInhabitedEntry.default }

Lexing

def Diagnostics.unexpectedCharacter : Entry

Parser_'s lexer rejected a character.

Equations

• Diagnostics.unexpectedCharacter = { code := Diagnostics.e✝ 1, stage := Stage.lex, summary := "A character the lexer cannot start any token with." }

Parsing

def Diagnostics.unexpectedToken : Entry

Parser_'s parser rejected a token.

Equations

• Diagnostics.unexpectedToken = { code := Diagnostics.e✝ 2, stage := Stage.parse, summary := "A token that cannot continue the construct being parsed." }

Annotation resolution

def Diagnostics.annotationArity : Entry

@type/@mailbox/@parameter given the wrong number of arguments.

Equations

• Diagnostics.annotationArity = { code := Diagnostics.e✝ 3, stage := Stage.annotation, summary := "An annotation was given the wrong number of arguments." }

def Diagnostics.annotationArgumentKind : Entry

An annotation's argument is not the kind of thing that annotation takes.

Equations

• Diagnostics.annotationArgumentKind = { code := Diagnostics.e✝ 4, stage := Stage.annotation, summary := "An annotation's argument is not of the kind it expects." }

def Diagnostics.annotationTypeParse : Entry

A @type annotation's payload does not parse as a type.

Equations

• Diagnostics.annotationTypeParse = { code := Diagnostics.e✝ 5, stage := Stage.annotation, summary := "The type inside an annotation does not parse." }

def Diagnostics.annotationExpressionParse : Entry

An annotation's payload does not parse as an expression.

Equations

• Diagnostics.annotationExpressionParse = { code := Diagnostics.e✝ 6, stage := Stage.annotation, summary := "The expression inside an annotation does not parse." }

def Diagnostics.annotationMailboxShape : Entry

@mailbox was not given a var[e₁, …, eₙ]-shaped expression.

Equations

• Diagnostics.annotationMailboxShape = { code := Diagnostics.e✝ 7, stage := Stage.annotation, summary := "A @mailbox annotation is not of the form 'var[e₁, …, eₙ]'." }

Desugaring

def Diagnostics.misplacedAt : Entry

@ used outside an EXCEPT update.

Equations

• Diagnostics.misplacedAt = { code := Diagnostics.e✝ 8, stage := Stage.desugar, summary := "'@' appears outside the EXCEPT update it would refer to." }

def Diagnostics.gotoNotInTailPosition : Entry

goto somewhere other than the end of its statement list.

Equations

• Diagnostics.gotoNotInTailPosition = { code := Diagnostics.e✝ 9, stage := Stage.desugar, summary := "A goto is not the last statement of its list." }

def Diagnostics.unlabelledStatement : Entry

A statement with no label reachable above it.

Equations

• Diagnostics.unlabelledStatement = { code := Diagnostics.e✝ 10, stage := Stage.desugar, summary := "A statement belongs to no labelled atomic block." }

def Diagnostics.nestedLabel : Entry

A label inside a with body.

Equations

• Diagnostics.nestedLabel = { code := Diagnostics.e✝ 11, stage := Stage.desugar, summary := "A label appears inside a 'with' body, which cannot contain one." }

def Diagnostics.whileInWith : Entry

A while inside a with body.

Equations

• Diagnostics.whileInWith = { code := Diagnostics.e✝ 12, stage := Stage.desugar, summary := "A 'while' appears inside a 'with' body." }

def Diagnostics.whileNotLabelled : Entry

A while not immediately preceded by a label.

Equations

• Diagnostics.whileNotLabelled = { code := Diagnostics.e✝ 13, stage := Stage.desugar, summary := "A 'while' is not immediately preceded by a label." }

def Diagnostics.notFollowedByLabel : Entry

An if/either that needs a label after it and does not have one.

Equations

• Diagnostics.notFollowedByLabel = { code := Diagnostics.e✝ 14, stage := Stage.desugar, summary := "A statement that ends an atomic block is not followed by a label." }

def Diagnostics.withBoundVarWritten : Entry

A write to a with-bound name.

Equations

• Diagnostics.withBoundVarWritten = { code := Diagnostics.e✝ 15, stage := Stage.desugar, summary := "A 'with'-bound name is assigned to or received into." }

def Diagnostics.wrongAnnotationKind : Entry

An annotation of the wrong kind for the site it sits at.

Equations

• Diagnostics.wrongAnnotationKind = { code := Diagnostics.e✝ 16, stage := Stage.desugar, summary := "An annotation of a kind this site does not accept." }

def Diagnostics.duplicateAnnotation : Entry

The same annotation twice on one site.

Equations

• Diagnostics.duplicateAnnotation = { code := Diagnostics.e✝ 17, stage := Stage.desugar, summary := "The same annotation kind appears twice on one declaration." }

def Diagnostics.conflictingAssignment : Entry

Two assignments to the same variable in one atomic block.

Equations

• Diagnostics.conflictingAssignment = { code := Diagnostics.e✝ 18, stage := Stage.desugar, summary := "A variable is assigned more than once within one atomic block." }

def Diagnostics.invalidRecordFieldAccess : Entry

A record field access whose field is not an identifier.

Equations

• Diagnostics.invalidRecordFieldAccess = { code := Diagnostics.e✝ 19, stage := Stage.desugar, summary := "A record field access whose field is not an identifier." }

EXTENDS resolution

def Diagnostics.moduleNotFound : Entry

EXTENDS names a module no search path provides.

Equations

• Diagnostics.moduleNotFound = { code := Diagnostics.e✝ 21, stage := Stage.resolve, summary := "An EXTENDS-ed module was not found on any search path." }

def Diagnostics.ambiguousModule : Entry

EXTENDS names a module found in more than one place.

Equations

• Diagnostics.ambiguousModule = { code := Diagnostics.e✝ 22, stage := Stage.resolve, summary := "An EXTENDS-ed module name resolves to more than one candidate." }

def Diagnostics.cyclicExtends : Entry

EXTENDS forms a cycle.

Equations

• Diagnostics.cyclicExtends = { code := Diagnostics.e✝ 23, stage := Stage.resolve, summary := "EXTENDS forms a cycle." }

Type checking

def Diagnostics.typeCheckTodo : Entry

Placeholder for a checking rule with no named diagnostic yet.

Equations

• Diagnostics.typeCheckTodo = { code := Diagnostics.e✝ 24, stage := Stage.typeCheck, summary := "An unnamed type-checking failure (placeholder)." }

def Diagnostics.unboundVariable : Entry

A name with no binding in scope.

Equations

• Diagnostics.unboundVariable = { code := Diagnostics.e✝ 25, stage := Stage.typeCheck, summary := "A name with no binding in scope." }

def Diagnostics.typeMismatch : Entry

Two types that do not convert.

Equations

• Diagnostics.typeMismatch = { code := Diagnostics.e✝ 26, stage := Stage.typeCheck, summary := "A value's type is not compatible with the type expected here." }

def Diagnostics.missingTypeAnnotation : Entry

A type annotation is required and absent.

Equations

• Diagnostics.missingTypeAnnotation = { code := Diagnostics.e✝ 27, stage := Stage.typeCheck, summary := "A type annotation is required at this position." }

def Diagnostics.cannotInferType : Entry

A type could not be inferred.

Equations

• Diagnostics.cannotInferType = { code := Diagnostics.e✝ 28, stage := Stage.typeCheck, summary := "No type could be inferred for this expression." }

def Diagnostics.notASetType : Entry

A set was expected.

Equations

• Diagnostics.notASetType = { code := Diagnostics.e✝ 29, stage := Stage.typeCheck, summary := "A set was expected here." }

def Diagnostics.notARecordType : Entry

A record was expected.

Equations

• Diagnostics.notARecordType = { code := Diagnostics.e✝ 30, stage := Stage.typeCheck, summary := "A record was expected here." }

def Diagnostics.notIndexable : Entry

Indexing into something that cannot be indexed.

Equations

• Diagnostics.notIndexable = { code := Diagnostics.e✝ 31, stage := Stage.typeCheck, summary := "This type cannot be indexed." }

def Diagnostics.unknownField : Entry

A record field that the record type does not have.

Equations

• Diagnostics.unknownField = { code := Diagnostics.e✝ 32, stage := Stage.typeCheck, summary := "A record field this record type does not have." }

def Diagnostics.invalidTupleIndex : Entry

A tuple index outside the tuple's range, or not a literal.

Equations

• Diagnostics.invalidTupleIndex = { code := Diagnostics.e✝ 33, stage := Stage.typeCheck, summary := "A tuple index that is not a literal within the tuple's range." }

def Diagnostics.notAnOperatorType : Entry

An operator was expected.

Equations

• Diagnostics.notAnOperatorType = { code := Diagnostics.e✝ 34, stage := Stage.typeCheck, summary := "An operator was expected here." }

def Diagnostics.arityMismatch : Entry

An operator applied to the wrong number of arguments.

Equations

• Diagnostics.arityMismatch = { code := Diagnostics.e✝ 35, stage := Stage.typeCheck, summary := "An operator applied to the wrong number of arguments." }

def Diagnostics.ambiguousType : Entry

A type that stayed ambiguous.

Equations

• Diagnostics.ambiguousType = { code := Diagnostics.e✝ 36, stage := Stage.typeCheck, summary := "More than one type fits, with nothing to choose between them." }

def Diagnostics.notAFunctionType : Entry

A function was expected.

Equations

• Diagnostics.notAFunctionType = { code := Diagnostics.e✝ 37, stage := Stage.typeCheck, summary := "A function was expected here." }

def Diagnostics.notATupleType : Entry

A tuple was expected.

Equations

• Diagnostics.notATupleType = { code := Diagnostics.e✝ 38, stage := Stage.typeCheck, summary := "A tuple was expected here." }

def Diagnostics.paramArityMismatch : Entry

A higher-order parameter used at an arity its declared type does not have.

Equations

• Diagnostics.paramArityMismatch = { code := Diagnostics.e✝ 39, stage := Stage.typeCheck, summary := "A higher-order parameter used at an arity its type does not allow." }

def Diagnostics.notAChannelType : Entry

A channel was expected.

Equations

• Diagnostics.notAChannelType = { code := Diagnostics.e✝ 40, stage := Stage.typeCheck, summary := "A channel was expected here." }

def Diagnostics.notShowable : Entry

print given something with no printable form.

Equations

• Diagnostics.notShowable = { code := Diagnostics.e✝ 41, stage := Stage.typeCheck, summary := "This type has no printable form." }

def Diagnostics.notSendable : Entry

A value that cannot be sent over a channel.

Equations

• Diagnostics.notSendable = { code := Diagnostics.e✝ 42, stage := Stage.typeCheck, summary := "This type cannot be sent over a channel." }

def Diagnostics.unconstrainedMetavariable : Entry

A metavariable left unconstrained at the end of checking.

Equations

• Diagnostics.unconstrainedMetavariable = { code := Diagnostics.e✝ 43, stage := Stage.typeCheck, summary := "A type was left undetermined at the end of checking." }

Well-formedness

def Diagnostics.unknownLabel : Entry

A goto to a label no process defines.

Equations

• Diagnostics.unknownLabel = { code := Diagnostics.e✝ 44, stage := Stage.wellFormedness, summary := "A goto targets a label that is never defined." }

def Diagnostics.redefinedDone : Entry

Done redefined as an ordinary label.

Equations

• Diagnostics.redefinedDone = { code := Diagnostics.e✝ 45, stage := Stage.wellFormedness, summary := "The reserved label 'Done' is redefined." }

def Diagnostics.duplicateName : Entry

Two declarations of one name in one scope.

Equations

• Diagnostics.duplicateName = { code := Diagnostics.e✝ 46, stage := Stage.wellFormedness, summary := "A name is declared twice in the same scope." }

def Diagnostics.shadowedName : Entry

An inner declaration shadowing an outer one.

Equations

• Diagnostics.shadowedName = { code := Diagnostics.e✝ 47, stage := Stage.wellFormedness, summary := "A declaration shadows an outer one of the same name." }

def Diagnostics.channelInExpression : Entry

A channel value inside an ordinary expression.

Equations

• Diagnostics.channelInExpression = { code := Diagnostics.e✝ 48, stage := Stage.wellFormedness, summary := "A channel appears where an ordinary value is expected." }

def Diagnostics.channelTypedVariable : Entry

A variables entry with a channel type.

Equations

• Diagnostics.channelTypedVariable = { code := Diagnostics.e✝ 49, stage := Stage.wellFormedness, summary := "A 'variables' entry has a channel type." }

def Diagnostics.nonEmptyLocalChannels : Entry

A process declaring its own channels/fifos.

Equations

• Diagnostics.nonEmptyLocalChannels = { code := Diagnostics.e✝ 50, stage := Stage.wellFormedness, summary := "A process declares process-local channels." }

def Diagnostics.globalPlusCalVariable : Entry

An algorithm-level PlusCal variables block.

Equations

• Diagnostics.globalPlusCalVariable = { code := Diagnostics.e✝ 51, stage := Stage.wellFormedness, summary := "An algorithm-level 'variables' block: no shared memory." }

def Diagnostics.globalTLAPlusVariable : Entry

A reference to a module-level TLA⁺ VARIABLE.

Equations

• Diagnostics.globalTLAPlusVariable = { code := Diagnostics.e✝ 52, stage := Stage.wellFormedness, summary := "A reference to a module-level VARIABLE: no shared memory." }

def Diagnostics.bareTemporalOrAction : Entry

A temporal or action operator reachable from a statement.

Equations

• Diagnostics.bareTemporalOrAction = { code := Diagnostics.e✝ 53, stage := Stage.wellFormedness, summary := "A temporal or action operator is reachable from a statement." }

def Diagnostics.unboundedQuantifier : Entry

An unbounded quantifier where a finite one is required.

Equations

• Diagnostics.unboundedQuantifier = { code := Diagnostics.e✝ 54, stage := Stage.wellFormedness, summary := "An unbounded quantifier, which has no finite runtime meaning." }

def Diagnostics.receiveChannelMismatch : Entry

A process receiving from more than one channel.

Equations

• Diagnostics.receiveChannelMismatch = { code := Diagnostics.e✝ 62, stage := Stage.wellFormedness, summary := "A process receives from a channel other than the single one it listens on." }

def Diagnostics.mailboxNotIndexedBySelf : Entry

A process set receiving from a channel shared by all of its instances.

Equations

• Diagnostics.mailboxNotIndexedBySelf = { code := Diagnostics.e✝ 63, stage := Stage.wellFormedness, summary := "A process set receives from a channel not indexed by 'self'." }

def Diagnostics.receiveWithoutMailbox : Entry

A process receiving without a @mailbox declaration.

Equations

• Diagnostics.receiveWithoutMailbox = { code := Diagnostics.e✝ 64, stage := Stage.wellFormedness, summary := "A process receives from a channel it never declared as its @mailbox." }

def Diagnostics.duplicateProcessName : Entry

Two processes of one algorithm carrying the same name.

Equations

• Diagnostics.duplicateProcessName = { code := Diagnostics.e✝ 65, stage := Stage.wellFormedness, summary := "Two processes of one algorithm share a name." }

def Diagnostics.duplicateLabel : Entry

Two blocks of one algorithm carrying the same label.

Equations

• Diagnostics.duplicateLabel = { code := Diagnostics.e✝ 66, stage := Stage.wellFormedness, summary := "Two blocks of one algorithm share a label." }

Typed2Computable

def Diagnostics.notComputable : Entry

A construct with no finite runtime representation.

Equations

• Diagnostics.notComputable = { code := Diagnostics.e✝ 55, stage := Stage.computable, summary := "A construct with no finite runtime representation." }

def Diagnostics.computableInternalInvariant : Entry

An invariant Typed2Computable relies on did not hold — a compiler bug, not a program error.

Equations

• Diagnostics.computableInternalInvariant = { code := Diagnostics.e✝ 56, stage := Stage.computable, summary := "Internal invariant violated in Typed2Computable (compiler bug)." }

Computable2Guarded

def Diagnostics.guardedInternalInvariant : Entry

An invariant Computable2Guarded relies on did not hold — a compiler bug.

Equations

• Diagnostics.guardedInternalInvariant = { code := Diagnostics.e✝ 57, stage := Stage.guarded, summary := "Internal invariant violated in Computable2Guarded (compiler bug)." }

Guarded2Network

def Diagnostics.networkInternalInvariant : Entry

An invariant Guarded2Network relies on did not hold — a compiler bug.

Equations

• Diagnostics.networkInternalInvariant = { code := Diagnostics.e✝ 58, stage := Stage.network, summary := "Internal invariant violated in Guarded2Network (compiler bug)." }

Network2Go

def Diagnostics.goInternalInvariant : Entry

An invariant Network2Go relies on did not hold — a compiler bug.

Equations

• Diagnostics.goInternalInvariant = { code := Diagnostics.e✝ 60, stage := Stage.go, summary := "Internal invariant violated in Network2Go (compiler bug)." }

def Diagnostics.goUnsupported : Entry

A well-typed construct the Go backend has no way to compile.

Equations

• Diagnostics.goUnsupported = { code := Diagnostics.e✝ 61, stage := Stage.go, summary := "A construct with no Go counterpart (infinite set, Bags, function equality)." }

Module identity

def Diagnostics.moduleNameMismatch : Entry

A file whose MODULE name is not the file's own name.

Equations

• Diagnostics.moduleNameMismatch = { code := Diagnostics.e✝ 59, stage := Stage.parse, summary := "A module's declared name does not match the name of the file it is in." }

Warnings

def Diagnostics.fairIgnored : Entry

fair/fair+ parsed and ignored.

Equations

• Diagnostics.fairIgnored = { code := Diagnostics.w✝ 1, stage := Stage.parse, warningName := "fair", summary := "'fair'/'fair+' is parsed but never acted on." }

def Diagnostics.unusedAnnotation : Entry

An annotation nothing consumes.

Equations

• Diagnostics.unusedAnnotation = { code := Diagnostics.w✝ 2, stage := Stage.parse, warningName := "unused-annotation", summary := "A well-formed annotation sits where nothing reads it." }

def Diagnostics.duplicateParameterAnnotation : Entry

@parameter repeated harmlessly.

Equations

• One or more equations did not get rendered due to their size.

def Diagnostics.typeCheckTodoWarning : Entry

Placeholder for an unnamed checker warning.

Equations

• Diagnostics.typeCheckTodoWarning = { code := Diagnostics.w✝ 4, stage := Stage.typeCheck, warningName := "todo", summary := "An unnamed type-checking warning (placeholder)." }

def Diagnostics.partialMulticastAnnotation : Entry

A multicast filter annotating only some of its components.

Equations

• One or more equations did not get rendered due to their size.

def Diagnostics.extendsAlgorithm : Entry

An EXTENDS-ed module with a PlusCal algorithm of its own, which EXTENDS does not carry over.

Equations

• One or more equations did not get rendered due to their size.

def Diagnostics.unusedMailbox : Entry

A @mailbox declared by a process that contains no receive.

Equations

• One or more equations did not get rendered due to their size.

def Diagnostics.unsafeCast : Entry

A call to an unsafe representation downcast (Fugue!FunAsSeq, Fugue!SetAsFun).

Equations

• One or more equations did not get rendered due to their size.

def Diagnostics.entries : List Entry

Every registered diagnostic, in code order. fugue explain --list prints this; the regression runner's coverage report walks it to find codes no fixture exercises.

Equations

• One or more equations did not get rendered due to their size.

def Diagnostics.warningNames : List String

Every -W<name> a warning can be suppressed under, in code order. What the CLI validates -W against, so the set of accepted names is the set of warnings that exist: Entry.code has no default, so a warning cannot be emitted without an entry here to derive its name from, and a name here with no warning behind it would have nothing to suppress.

Equations

• Diagnostics.warningNames = List.filterMap (fun (e : Diagnostics.Entry) => if e.warningName.isEmpty = true then none else some e.warningName) Diagnostics.entries

def Diagnostics.find? (code : DiagnosticCode) : Option Entry

The entry for code, if it is registered.

Equations

• Diagnostics.find? code = List.find? (fun (x : Diagnostics.Entry) => x.code == code) Diagnostics.entries