Skip to main content

Error Code Reference

Complete reference for all Sector9 error codes with explanations and solutions.

Sector9 uses error codes prefixed with M, inherited from the original Motoko diagnostic numbering, followed by a four-digit number. Use sector9 --explain MXXXX to get detailed explanations for codes that have them.

Error Categories Overview​

RangeCategoryDescription
M0000-M0002InfrastructureInternal errors, parsing, lexing
M0003-M0019Imports & NamingModule resolution, naming conflicts
M0020-M0036Variables & TypesBinding, scoping, type parameters
M0037-M0050Async & LiteralsAsync/await placement, literal validation
M0051-M0099Type CheckingOperators, patterns, assignments
M0100-M0158Advanced TypesClasses, actors, stability, patterns
M0159-M0200Candid & InteropSerialization, type compatibility
M0201-M0239Modern FeaturesMigrations, mixins, implicit arguments
M0240-M0246Verification: Purity/CollectionsPure/spec-collection restrictions; historical linearity checks are disabled
M0311-M0318Verification: GhostGhost state and pure function context
M0335-M0360Verification: ModeViper-mode specific restrictions

Infrastructure Errors (M0000-M0002)​

M0000 - Internal Compiler Error​

An unexpected internal error occurred. This indicates a bug in the compiler.

What to do: Report the issue with a minimal reproducing example.

M0001 - Syntax Error​

The parser encountered unexpected input.

Example:

persistent actor {
  public func broken( : async Nat {  // Missing parameter
    42
  };
}

Fix: Check for missing tokens, unbalanced braces, or invalid syntax.

M0002 - Lexer Error​

Invalid character or token encountered during lexical analysis.

Common causes:

  • Invalid UTF-8 in string literals
  • Malformed operators
  • Invalid escape sequences
  • Unclosed string literals

Import and Naming Errors (M0003-M0019)​

M0003 - Self Import​

A module attempted to import itself.

Example:

// File: Self.sr9
import S "./Self";  // Error: Self.sr9 cannot import itself

module { }

Fix: Remove the circular import.

M0009 - File Not Found​

The imported file does not exist.

Example:

import Utils "./nonexistent";  // Error: file not found

Fix: Check the file path and ensure the file exists.

M0014 - Non-Static Expression​

A non-static expression appears in a module or library context where only static expressions are allowed.

Example:

module {
  var counter : Nat = 0;  // Error: mutable state not allowed in module
}

Fix: Use persistent actor for stateful code, or make the expression static.

M0016 - Usage Before Definition​

A variable is used before it is defined.

Example:

let y = x + 1;  // Error: x not defined yet
let x = 5;

Fix: Reorder definitions so dependencies come first.

M0017 - Duplicate Binding​

The same name is bound multiple times in a pattern.

Example:

let (x, x) = (1, 2);  // Error: x bound twice

Fix: Use distinct names.

M0018 - Duplicate Name in Type​

A type definition contains duplicate field names.

Example:

type Bad = { name : Text; name : Int };  // Error: duplicate field

Fix: Use unique field names.

Variable and Type Errors (M0020-M0036)​

M0026 - Unbound Variable​

A variable is used that has not been declared.

Example:

public func add(x : Nat) : async Nat {
  x + y  // Error: unbound variable y
}

Fix: Declare the variable or fix the spelling.

M0028 - Field Does Not Exist​

Access to a field that does not exist in the type.

Example:

let person = { name = "Alice" };
person.age  // Error: field 'age' does not exist

Fix: Check the field name or add the missing field.

M0029 - Unbound Type​

Reference to a type that has not been defined.

Example:

func process(x : Unknown) : Nat { 0 }  // Error: unbound type Unknown

Fix: Define the type or import it.

M0031 - Non-Shared Parameter Type​

A shared function has a parameter type that cannot be shared across canisters.

Example:

public shared func process(f : Nat -> Nat) : async () { }  // Error

Fix: Use only shareable types (primitives, records, variants, arrays) for shared function parameters.

M0035 - Invalid Shared Return Type​

A shared function has an invalid return type.

Example:

public shared func get() : Nat { 42 }  // Error: missing async

Fix: Use async return type or remove shared.

Async and Literal Errors (M0037-M0050)​

M0037 - Misplaced Async​

An async operation appears in a context without send capability.

Example:

persistent actor {
  let x = try { await someCall() } catch (_) { 0 };  // Error: await at top level of actor
}

What it means: await and inter-canister calls require send capability, which is only available inside async functions. You also cannot message from a finally clause.

Fix: Move the await into an async function, or restructure the initialization.

M0038 - Misplaced Await​

An await expression appears outside an async context.

Example:

func sync() : Nat {
  await asyncCall()  // Error: await outside async function
}

Fix: Make the function async or restructure the code.

M0048 - Literal Out of Range​

A numeric literal exceeds the range of its type.

Example:

let x : Nat8 = 300;  // Error: 300 > 255

Fix: Use a larger type or reduce the value.

M0049 - Invalid UTF-8 String​

A string literal contains invalid UTF-8 encoding.

Fix: Ensure string literals contain valid UTF-8 characters.

Type Checking Errors (M0051-M0099)​

M0051 - Duplicate Definition​

A name is defined multiple times in the same block.

Example:

{
  let x = 1;
  let x = 2;  // Error: duplicate definition
}

Fix: Use different names or remove the duplicate.

M0059 - Operator Not Defined​

An operator is used with an incompatible operand type.

Example:

let x = "hello" + 5;  // Error: + not defined for Text and Nat

Fix: Use compatible types or convert values.

M0073 - Expected Mutable Target​

Assignment to an immutable variable.

Example:

let x = 5;
x := 10;  // Error: x is immutable

Fix: Declare the variable with var instead of let.

M0095 - Return Type Mismatch​

The function body type does not match the declared return type.

Example:

func add(x : Nat, y : Nat) : Text {
  x + y  // Error: Nat does not match Text
}

Fix: Correct the return type or the function body.

M0096 - Type Mismatch​

An expression cannot produce the expected type.

Example:

let x : Bool = 42;  // Error: Nat cannot produce Bool

Fix: Use a compatible value or change the type annotation.

M0098 - Cannot Instantiate Function​

Function arguments do not match the parameter types.

Example:

func greet(name : Text) : Text { "Hello, " # name };
greet(42)  // Error: cannot apply to Nat

Fix: Pass arguments of the correct type.

Advanced Type Errors (M0100-M0158)​

M0137 - Forward Type Reference​

A type definition references a type parameter from an outer scope.

Example:

class Outer<T>() {
  type Inner = T;  // Error: cannot capture outer type parameter
}

Fix: Pass the type parameter explicitly.

M0141 - Non-Unique Actor​

Multiple actors or non-import declarations in a program file.

An actor or actor class must be the only non-imported declaration in its file.

Fix: Move other definitions to separate module files.

M0145 - Pattern Not Exhaustive​

A pattern match does not cover all possible values.

Example:

switch (opt) {
  case (?x) { x }
  // Missing: case null
}

Fix: Add cases for all possible values.

M0146 - Pattern Never Matched​

A pattern case can never be reached.

Example:

switch (x) {
  case _ { 0 };
  case 5 { 5 };  // Warning: never matched (wildcard above catches all)
}

Fix: Reorder cases or remove unreachable patterns.

M0149 - Expected Mutable Field​

An immutable field was provided where a mutable field was expected.

Example:

{ count = 0 } : { var count : Nat }  // Error: missing var

Fix: Add the var keyword: { var count = 0 }.

M0150 - Expected Immutable Field​

A mutable field was provided where an immutable field was expected.

Example:

{ var count = 0 } : { count : Nat }  // Error: unexpected var

Fix: Remove the var keyword.

M0151 - Missing Field​

A required field is missing from an object literal.

Example:

{ name = "Alice" } : { name : Text; age : Nat }  // Error: missing age

Fix: Add the missing field.

M0155 - Nat Subtraction Warning​

Subtraction was inferred as Nat type, which traps on negative results.

Example:

let diff = n - 1;  // Warning: Nat subtraction may trap

Fix: Add explicit type annotation (let diff : Int = n - 1) or use the unary plus operator (let diff = +n - 1).

Candid and Interop Errors (M0159-M0200)​

M0175 - Non-Shared to_candid​

The to_candid function requires a shared type argument.

Example:

to_candid(myFunc)  // Error: functions are not shared

Fix: Only use to_candid with shareable types.

M0200 - Cannot Decide Subtyping​

The type checker cannot determine if subtyping or equality holds.

Example:

type Recursive = ?Recursive;
// Complex recursive types may trigger this

Fix: Simplify the types or add explicit annotations.

Modern Feature Errors (M0201-M0239)​

M0225 - Mixin Entry Point​

A mixin cannot be used directly as a program entry point.

Fix: Use the mixin inside an actor with include.

M0230 - Cannot Infer Implicit​

An implicit argument cannot be determined from context.

Fix: Provide the argument explicitly.

Verification: Spec Collection Errors (M0240-M0246)​

These errors relate to spec collection checks. Linearity enforcement is currently disabled, so M0243-M0246 are not emitted.

M0240 - Pure Function Restriction​

A pure or lemma function violates purity restrictions.

Violations include:

  • Writing state
  • Awaiting
  • Containing assert, trap, or runtime:assert

Example:

pure func bad() : Nat {
  assert true;  // Error: pure functions may not contain assertions
  0
}

Fix: Remove the impure operation or change the function to non-pure.

M0242 - Non-Immutable Spec Type​

A spec collection element type contains mutable state.

Example:

ghost var accounts : Map<Nat, { var balance : Nat }> = Map.empty();
// Error: var fields not allowed in spec collections

Fix: Use immutable types in spec collections.

M0243 - Linear Value Already Consumed (disabled)​

This error was raised when a linear collection was used after being consumed. Linearity checks are currently disabled.

Example:

ghost {
  let m = Map.empty<Nat, Nat>();
  let m2 = Map.update(m, 1, 100);  // m remains usable today
  let m3 = Map.update(m, 2, 200);  // Historical M0243; no longer emitted
}

Current guidance: No fix is required for reuse. Thread values through updates only when you want later code to use the updated collection:

ghost {
  var m = Map.empty<Nat, Nat>();
  m := Map.update(m, 1, 100);
  m := Map.update(m, 2, 200);
}

M0244 - Linear Value Not Bound (disabled)​

This error was raised when a linear collection result was not bound. Linearity checks are currently disabled.

Example:

ghost {
  Map.update(m, 1, 100);  // Historical M0244; no longer emitted
}

Current guidance: Bind the result only when you need the updated collection: m := Map.update(m, 1, 100).

M0245 / M0246 - Linear Type in Pattern (disabled)​

This error was raised when a pattern binding contained a linear type. Linearity checks are currently disabled.

Example:

for (entry in map.entries()) { }  // Historical M0245/M0246; no longer emitted

Current guidance: Pattern bindings over spec collections are allowed by the current non-linear collection model unless another verifier restriction applies.

Verification: Ghost and Pure Errors (M0311-M0318)​

These errors enforce the separation between ghost (verification-only) and runtime code.

M0311 - Implication in Runtime​

The implication operator (==>) appears in runtime code.

Example:

let x = (a > 0) ==> (b > 0);  // Error: ==> only in ghost context

Fix: Use not a or b in runtime code, or move to a ghost context.

M0312 - Biconditional in Runtime​

The biconditional operator (<==>) appears in runtime code.

Fix: Use explicit boolean logic in runtime code.

M0313 - Misplaced old()​

The old() expression appears outside a verifier-only context where method-entry snapshots are legal.

Example:

public func check() : async Bool {
  old(balance) > 0  // Error: old() is not a runtime expression
}

Fix: Use old() only in postconditions, phase postconditions, ghost/proof code, or lemma bodies. It is not allowed in requires, entry_requires, actor invariants, or runtime expressions.

M0314 - Ghost Variable in Runtime​

A ghost variable is accessed from runtime code.

Example:

persistent actor {
  ghost var count : Nat = 0;

  public func get() : async Nat {
    count  // Error: ghost variable in runtime
  };
}

Fix: Ghost variables can only be accessed in ghost contexts (ensures, ghost blocks, lemmas).

M0315 - Local Variable in Contract​

A local variable is used in a contract where it is not accessible.

Fix: Use parameters or fields accessible in contracts.

M0316 - Ghost Variable in Contract​

A ghost variable is used incorrectly in a contract context.

Fix: Check the specific contract context restrictions.

M0317 - Pure Function Field Access​

A pure function accesses actor or module state.

Example:

persistent actor {
  var balance : Nat = 0;

  pure func getBalance() : Nat {
    balance  // Error: pure cannot access balance
  };
}

Fix: Pass the value as a parameter:

pure func compute(bal : Nat) : Nat { bal + 1 }

M0318 - Ghost Field Access Violation​

A ghost field is accessed in an invalid context.

Fix: Ensure ghost fields are only accessed in ghost contexts within the defining module.

Verification Mode Errors (M0335-M0360)​

These errors only appear when using verification features.

M0335 - Decreases Not Supported​

Termination proofs (decreases clause) are not supported.

Example:

func countdown(n : Nat) : Nat
  decreases n  // Error: not supported in verification mode

Fix: Remove the decreases clause. Sector9 verifies partial correctness only.

M0336 - Declaration-Only Function​

A function without a body cannot be compiled.

Example:

func stub(x : Nat) : Nat;  // Error when compiling

Fix: Add a body before compiling, or use only in verification mode.

M0360 - Non-Pure Higher-Order Function​

Higher-order function values must be pure or carry type contracts in verification mode. Uncontracted callback types are treated as pure.

Example:

let f : Nat -> Nat = func(x) { counter += 1; x };  // Error

Fix: Add the pure modifier, or use a contract-typed parameter and a contract-bearing value.

Warning Codes​

Some codes may appear as warnings rather than errors. Key warnings include:

CodeMessage
M0074Array elements have inconsistent types
M0081If branches have inconsistent types
M0089Redundant ignore
M0145Pattern does not cover value
M0146Pattern is never matched
M0154Deprecation annotation in use
M0155Inferred Nat for subtraction
M0194Unused identifier
M0198Unused field pattern

Use -W none to suppress all warnings or -W error to treat warnings as errors.

Getting Help​

Built-in Explanations​

For codes with detailed documentation:

sector9 --explain M0037

JSON Output​

For programmatic analysis of errors:

sector9 --verify --json file.sr9

JSON output includes structured error information with failure_id, obligation_kind, fix_hints, and footprint_missing fields.

Counterexamples​

For verification failures, add --counterexample to see concrete failing values:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --counterexample file.sr9

Summary​

  • Error codes use the format MXXXX where X is a digit
  • Ranges indicate category: imports (0003-0019), types (0020-0099), verification (0240-0360)
  • Use sector9 --explain MXXXX for detailed explanations
  • Type errors prevent verification; verification failures indicate unprovable specifications
  • Ghost/pure errors (M031x) enforce separation between verification and runtime code
  • M024x errors now mainly cover purity/spec-collection restrictions; historical linearity checks M0243-M0246 are disabled
  • Use --json for programmatic error handling