The type checker's diagnostics: one named error/warning variant per violation.

inductive TCError : Type

The type checker's errors. todo is a placeholder, to be replaced by named variants as checking rules are implemented.

• todo (pos : SourceSpan) (msg : String) : TCError

  Escape hatch: an arbitrary message at a position, standing in for a real named variant.

• unboundVariable (pos : SourceSpan) (name : String) : TCError

  A Γ-lookup miss.

• failedToConvertTypes (pos : SourceSpan) (expected got : TypedTLAPlus.Typ) : TCError

  No coercion exists from the synthesized type to the expected one.

• expectedTypeAnnotation (pos : SourceSpan) (what : String) : TCError

  A construct that can only synthesize when annotated was used with no annotation present.

• cannotInferType (pos : SourceSpan) (reason : String) : TCError

  A checking-only construct (empty set, unbounded CHOOSE) was hit in a position that needs a synthesized type.

• notASetType (pos : SourceSpan) (got : TypedTLAPlus.Typ) : TCError

  A Set(τ) type was expected here, but something else was found.

• notARecordType (pos : SourceSpan) (got : TypedTLAPlus.Typ) : TCError

  A record type was expected here, but something else was found.

• notIndexable (pos : SourceSpan) (got : TypedTLAPlus.Typ) : TCError

  Indexing (e[e']) requires a function, tuple, or sequence type.

• unknownField (pos : SourceSpan) (field : String) (available : List String) : TCError

  A record access/update named a field the record's type doesn't have.

• invalidTupleIndex (pos : SourceSpan) (index : String) (arity : ℕ) : TCError

  A tuple access/update's index wasn't a literal natural number in range.

• notAnOperatorType (pos : SourceSpan) (got : TypedTLAPlus.Typ) : TCError

  An operator call's callee didn't synthesize an operator type at all.

• arityMismatch (pos : SourceSpan) (expected got : ℕ) : TCError

  An operator call's argument count didn't match its type's parameter count.

• ambiguousType (pos : SourceSpan) : TCError

  A lub-based synthesis rule found no common type across its branches/elements.

• notAFunctionType (pos : SourceSpan) (got : TypedTLAPlus.Typ) : TCError

  A function type (τ -> τ') was expected here, but something else was found.

• notATupleType (pos : SourceSpan) (got : TypedTLAPlus.Typ) : TCError

  A tuple type was expected here, but something else was found.

• paramArityMismatch (pos : SourceSpan) (param : String) (declared inferred : ℕ) : TCError

  A higher-order operator-definition parameter's declared arity (from F(_,...,_)'s _ count) didn't match its annotated type's own operator-arity.

• notAChannelType (pos : SourceSpan) (got : TypedTLAPlus.Typ) : TCError

  A receive/send/multicast statement's channel reference didn't synthesize a Channel(τ)-shaped type.

• notShowable (pos : SourceSpan) (got : TypedTLAPlus.Typ) : TCError

  A print statement's argument didn't synthesize a showable type.

• notSendable (pos : SourceSpan) (got : TypedTLAPlus.Typ) : TCError

  A channel's declared element type isn't sendable — Operator/Channel/Const/rigid type variables, or anything containing one, can't be sent over a channel.

• unconstrainedMetavariable (pos : SourceSpan) : TCError

  A metavariable left over at the end of a declaration's checking had no pending upper bound recorded on it at all — it was never actually constrained by anything during checking.

def instReprTCError.repr : TCError → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprTCError : Repr TCError

Equations

• instReprTCError = { reprPrec := instReprTCError.repr }

@[implicit_reducible]

instance instInhabitedTCError : Inhabited TCError

Equations

• instInhabitedTCError = { default := instInhabitedTCError.default }

def instBEqTCError.beq : TCError → TCError → Bool

Equations

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

@[implicit_reducible]

instance instBEqTCError : BEq TCError

Equations

• instBEqTCError = { beq := instBEqTCError.beq }

@[implicit_reducible]

instance instCompilerDiagnosticTCErrorString : CompilerDiagnostic TCError String

Equations

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

inductive TCWarning : Type

The type checker's non-fatal diagnostics, collected out-of-band. todo is a placeholder.

• todo (pos : SourceSpan) (msg : String) : TCWarning

  Escape hatch: an arbitrary message at a position, standing in for a real named variant.

• unsafeCast (pos : SourceSpan) (op : String) : TCWarning

  A call to an unsafe representation downcast — Fugue!FunAsSeq or Fugue!SetAsFun — whose compiled form aborts at runtime when its precondition (a 1..n domain, a functional pair set) does not hold. op is the operator's name.

def instReprTCWarning.repr : TCWarning → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprTCWarning : Repr TCWarning

Equations

• instReprTCWarning = { reprPrec := instReprTCWarning.repr }

@[implicit_reducible]

instance instInhabitedTCWarning : Inhabited TCWarning

Equations

• instInhabitedTCWarning = { default := instInhabitedTCWarning.default }

@[implicit_reducible]

instance instBEqTCWarning : BEq TCWarning

Equations

• instBEqTCWarning = { beq := instBEqTCWarning.beq }

def instBEqTCWarning.beq : TCWarning → TCWarning → Bool

Equations

• instBEqTCWarning.beq (TCWarning.todo a a_1) (TCWarning.todo b b_1) = (a == b && a_1 == b_1)
• instBEqTCWarning.beq (TCWarning.unsafeCast a a_1) (TCWarning.unsafeCast b b_1) = (a == b && a_1 == b_1)
• instBEqTCWarning.beq x✝¹ x✝ = false

def TCWarning.name : TCWarning → String

The -W<name>/-Wno-<name> name a given warning is filtered under.

Equations

• (TCWarning.todo a a_1).name = "todo"
• (TCWarning.unsafeCast a a_1).name = "unsafe"

@[implicit_reducible]

instance instCompilerDiagnosticTCWarningString : CompilerDiagnostic TCWarning String

Equations

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