🥮 mooncakes.io
README

marianoguerra/wax/check does not have a README file

#
Checker

source
pub struct Checker {
  ctx : 
ModuleContext
  ops : Operands
  unpeeled : Map[String, Int]
}

One run of the checker over one function body.

#
Checker::check

source

Check one instruction against a type the context already knows.

A construction whose name the expectation can supply is typed as though the name had been written, and the spelling is restored afterwards. Everything else is synthesized and then checked, which is what the call sites did by hand before this existed.

#
Checker::expression

source

Check one instruction in EXPRESSION position, returning the typed node.

Expression position is where a value is wanted. The constructs that differ from statement position are exactly the block-like ones, which are inferred here and not there, plus the two statements that produce nothing at all and so cannot stand where a value is expected.

#
Checker::gaps

source
fn Checker::gaps(self : Checker) -> Array[(String, Int)]

The constructs whose lowering could not be peeled back, most frequent first. Empty on well-formed input.

#
Checker::new

source

#
Checker::statement

source

Check one instruction in STATEMENT position, returning the typed node.

Statement position is the general case: the instruction may leave any number of values, including none. Expression position is the special one, and goes through expression_type to insist on exactly one.

#
MethodCall

source
pub(all) enum MethodCall {
  Atomic(
Family)
  MemAccess
  SimdMemAccess
  MemManage
  TableManage
  SegmentDrop
  Ordinary
} derive(Eq)

What recv.meth(..) turned out to be.

#
MissingBatch

source
type MissingBatch

One pending-value underflow: the counts to report, and whether they have been.

The placeholder cell recorded alongside lets the hole that ends up consuming it report at its own location, rather than the popping code needing to know how the missing values are distributed.

#
Operands

source

The stack, and the underflow placeholders accumulated while checking one function.

#
Operands::new

source
fn Operands::new() -> Operands

#
Operands::pop

source

Take the top operand, checking it against an expected type.

#
Operands::pop_any

source

Take the top operand's type, whatever it is.

No diagnostic is emitted here. The placeholder is recorded with its counts so the hole that consumes it reports at its own location, and an underflow POISONS the stack -- so one missing value is tracked once rather than once per subsequent pop.

#
Operands::pop_args

source

Take an instruction's arguments, rightmost first -- which is the order they were pushed in.

#
Operands::pop_many

source

Take count pending values, newest last, with the underflow batch if one occurred.

#
Operands::push

source

Push a value.

Pushing an Error POISONS the stack rather than stacking the error. The failed producer's true arity is unknown -- a call that did not resolve may have produced any number of values -- so later consumers have to absorb any count silently. Reporting an underflow there would anchor a derived error away from the original fault.

#
Operands::push_results

source

Push an instruction's results.

A location is attached only when there is exactly one result: with several, no single value is "the" thing at that span, and a mismatch on one of them is better reported against the instruction.

#
Operands::set_unreachable

source
fn Operands::set_unreachable(self : Operands) -> Unit

Mark everything after this point as dead code.

#
Operands::with_empty

source
fn[A] Operands::with_empty(self : Operands, f : () -> A) -> (A, Stack)

Run f on a fresh empty stack, restoring what was there before.

The stack is immutable, so saving it really is a snapshot -- which is what lets a block be checked without its operands leaking in or out.

#
ResolvedVar

source

What a bare name turned out to be.

#
Stack

source

The operand stack.

Three of the four cases are not "the stack is empty" in different words, and keeping them apart is what stops one mistake becoming a cascade:

  • Empty is a genuine underflow, and reports.
  • Unreachable is the polymorphic stack of dead code -- after a br, a return, an unreachable. Pops yield a fresh Unknown and consume nothing, and the dead-code lint keys on it.
  • Poisoned is what an already-reported failure leaves behind: a producer that did not resolve, or an underflow. Pops yield Error SILENTLY, because whatever went wrong has been said once already.

#
StackKind

source
pub(all) enum StackKind {
  Input
  Output
  Holes
} derive(Eq, 
Debug)

Which side of an instruction a stack complaint is about, which decides both the wording and where the caret goes.

#
add_type

source

Register a rec group: its names, its interned types, and the link between them.

Returns the index of the group's first member, or None if it did not resolve.

The two-step name registration is what makes a mutually recursive group possible. Every member is bound to a Rec placeholder before anything is resolved, so a member written first can name one written last; only once the group is interned are those placeholders replaced by real indices. A group that fails to resolve has its names withdrawn, so nothing is left pointing at a type that was never interned.

#
apply_declared_features

source

Turn on every feature the module DECLARES, before anything asks whether one is enabled.

A #![feature = "..."] states a fact about the whole module, so only a top-level annotation counts and one inside a conditional is a misplacement rather than a guarded declaration -- it is resolved before any branch is specialized, so a guarded one would leave every construct it gates erroring whichever way the branch went.

A feature the command line explicitly turned off is a conflict, reported once here -- and then enabled anyway, because the alternative is to report it again at every construct that needed it.

#
assign_target

source
fn assign_target(ctx : 
ModuleContext, idx : 
Ident, resolved : ResolvedVar, compound? : Bool) -> Unit

Record and report what an assignment target turned out to be.

Called AFTER the value has been checked, which matters: the local is marked initialized only then, so x = x + 1 still sees x's pre-assignment state while its right-hand side is being checked.

compound says the source wrote x op= e. That form desugars to x = x ope, and the desugared READ already reported an unbound name at this very span -- so reporting the write as well would say the same thing twice.

#
bind_local

source

Introduce a local with a known type.

Used for a binding that has an initializer: the value has just been checked against the type, so the local holds one.

#
block_signature

source

A block's declared parameters and results, as cells.

None when either fails to resolve: the block's shape is then unknown, and checking its body against a shape we do not have would invent complaints. The failure was already reported by the resolver.

#
branch_target

source

The types a branch to this label delivers.

Searches the enclosing frames innermost first, so a shadowing inner label of the same name wins -- which is what makes a label a lexical binding rather than a module-wide name.

An unresolved label reports and yields no types. It also SETS a flag on the context, and that flag is what stops the failure becoming two: a block whose only value delivery was the unresolved branch legitimately computes no value, and complaining about that as well would anchor a derived error away from the unbound label the reader actually has to fix.

#
check_float_bin_op

source

Check and unify the operands of a FLOAT-only operator.

A large literal is taken as a float here without complaint -- the operator has already ruled out every integer reading, so there is nothing to object to.

#
check_int_bin_op

source

Check and unify the operands of an INTEGER-only operator.

Two fully flexible operands become Int rather than staying Number: the operator has committed them to being integers even though it has not said which width.

A large literal is pinned to i64 outright. It cannot be i32, and the result of an integer operator cannot be a float, so i64 is the only type left -- which is exactly where this differs from the either-group rule below.

#
check_lane_immediate

source

Validate a lane immediate against its bound.

A lane index has to be a constant integer: there is no opcode for a computed lane, so a non-literal is not a slower lane selection, it is not one at all.

Compared UNSIGNED, and a literal too large even for u64 is rejected here rather than left to overflow: it would otherwise slip through to the code generator, which parses it and crashes. The reference has the same guard in both of its lane checks, for exactly that reason.

#
check_memarg

source

Validate the align and offset immediates of a memory access.

The two are checked independently and both are reported, because they are two separate things the author wrote and either can be wrong on its own.

natural is the access's own width in bytes. An alignment above it is rejected: it claims a guarantee the access cannot use and the engine cannot check. Below it is fine -- that only forgoes an optimisation.

The offset is bounded by the address type rather than by the access: on a 32-bit memory an offset at or past 2^32 can never name a reachable address, whatever the base.

#
check_module

source

Check one configuration of one module: declare every name, then check every field.

The two passes are the whole shape of the checker. Nothing can be checked until every name exists, because a function may call one defined below it; and the names cannot be given types until the types are registered, which is why the declaration pass has its own internal order.

#
check_num_concrete

source

Check and unify the operands of an operator that accepts EITHER group -- +, -, *, ==, !=.

Two fully flexible operands stay Number, because the operator has not ruled anything out: it could still resolve either way. Any more committed operand pins the pair to its group.

The instructive case is a large literal with a committed integer. The integer cannot be a float and the large literal cannot be i32, so their sole common type is i64 -- but with another large literal or a bare number it stays LargeInt, because a float is still reachable. The integer-only rule above pins in that case; this one does not, and the difference is exactly what each operator has ruled out.

#
check_operands

source

Check a construct's operands against the parameter types it wants.

Each value is reported at ITS OWN argument's span rather than at the construct's, so a wrong third argument points at the third argument.

#
check_subtypes

source

Check a run of values against a run of expected types.

A count mismatch is reported once and the values are not then checked individually: with the wrong number of them, pairing them up would produce a second, misleading complaint about whichever ones happened to line up.

#
checked_block

source

Check a block body against a declared shape.

The counterpart of collect_into: that one is for a block whose result is being INFERRED, this one for a block that already knows what it produces. Both run the body on a fresh empty stack under a control frame; the difference is what happens at the exit. Here the results are simply popped and checked, because there is a declared type to check them against.

branch_target is the one parameter that is not always results, and the distinction is the whole difference between a block and a loop. A br to a block's label jumps to its END and so delivers the block's RESULTS. A br to a loop's label jumps to its TOP and so delivers the loop's PARAMETERS -- it is re-entering, not leaving. Passing results for a loop would accept branches carrying the wrong values entirely.

#
classify_method_call

source

Which intrinsic family a recv.meth(..) call belongs to, if any.

Ordered as the reference orders its guards, and the order matters where two families share a name: the atomics claim theirs first, then the plain accesses, then SIMD, then the management operations. A name that no family claims -- or one whose receiver is not the right kind of thing -- is an ordinary call.

#
collect_into

source

Type one block body against a shared Collecting result cell, recording every value that reaches its exit.

The label is bound to r, so a br to it records its value; r is also the body's result type, so a trailing nested block is synthesized and its value collected rather than typed as a void statement and lost.

check_body is the instruction checker, passed in rather than called directly: an if runs this once per branch with the SAME cell, which is how both branches' exits come to be joined together.

branch_target defaults to the result cell, which is what a br to a block's label delivers. A LOOP passes the empty array instead: a branch there re-enters at the top with the loop's parameters, of which an inferred loop has none, so its value is only ever its fall-through.

#
comptype

source

What a defined type defines.

#
cont_functype

source

The function type a continuation type wraps.

(cont $ft) is a continuation of the function type $ft, so answering this is two hops through the store: the reference names a continuation, the continuation names a function. Anything else along the way is not a continuation at all.

#
declare_fields

source

Register every name a module binds, before any body is checked.

Types go first and separately: a function's declared type has to resolve while the function is being registered, so every type in the module must already be in the store -- including one declared after the function that names it.

#
declare_local

source

Introduce a local declared without an initializer -- let x: t;.

Whether it starts holding a value is decided by the type, and this is the only place that decision is made: a defaultable type has a zero value to start at, and a non-nullable reference does not, so it stays uninitialized until something assigns it. That is what makes a later read of it an error rather than a read of nothing.

An unannotated name has no type to take and declares nothing at all.

#
deliver_to_branch_target

source

Deliver the values below a br_if / br_on_null operand to the branch target, and answer what they are typed as on the fall-through.

A pass-through branch is the odd one out among branches: the value is delivered to the target when the branch is taken AND stays on the stack when it is not. So it is typed as the target's result either way -- which makes the requirement stricter than for an ordinary br. An ordinary delivery need only be a SUBTYPE of the result. A pass-through value has to be EXACTLY it, because the fall-through path will go on using it at that type.

That is what exacts records, and the snapshot has to be taken HERE, before the delivery below pins the value: after pinning, its natural type is gone and every value would look like it matched.

#
enter_function_scope

source

Establish a function's scope: its origin, parameters, and result types.

Returns the result cells, which are both the function's return targets and the types its fall-through is checked against -- the caller opens the outermost control frame with them.

label_decls and assigned_locals are collected by the syntactic lints, which are a later stage; they are parameters rather than gathered here so that when those land the caller fills them without this changing.

#
expression_type

source

The single value an instruction produced.

An instruction that left no value, or several, is not an expression, and this says so and recovers with Error poison -- so a caller that asked in vain still has something to carry on with.

Reported ONCE per rendered position and count. One node is legitimately asked by several consumers -- a call's callee twice, a labelled block as both value and statement -- and nested value-less expressions share a start column (a.m().m(), both halves value-less), so a full-span key would let two identical reports print at the same place. Keying on what the reader actually sees -- the start column and the count -- keeps a genuine second error with a different count.

#
field_has_default

source

Whether a field has a default value, so a ..default construction can leave it out.

Everything numeric does -- zero. A reference does only if it is nullable: there is no null to default a non-null reference to, so it must be given.

#
field_read_type

source

The type a field READ produces.

A packed field is not read at its stored width: i8 and i16 come off as i32, and which sign extension applies is the reader's choice. Int8 and Int16 carry that -- they are i32 values that remember how narrow they were, so the lowering can pick struct.get_s against struct.get_u.

#
field_subtype

source

Is one field type a subtype of another?

A MUTABLE field is invariant: it is read and written, so it has to be a subtype in both directions. An immutable one is covariant, being only read. Getting this backwards is how a type system lets a caller store the wrong thing through a widened reference.

#
finalize_inferred

source

Settle an inferred block's result: the cells its exits are checked against, and the annotation to write back.

Two cases, which are the two reasons to be here at all.

The source OMITTED the annotation. Then inference supplies it, and the result must commit to a width -- the written output cannot say "number". Since the commitment pins every flexible exit to the same type, only a CONCRETE pass-through value of a different type can still disagree, and with no annotation there is nothing to make it match, so it is reported.

The source HAS an annotation and simplify is converting from wasm. Then the question is whether it is redundant, and the bar is higher than agreement: dropping it must leave text that RE-INFERS to the same type. Hence the conditions, each guarding a way that could fail.

#
float_literal_lattice

source
fn float_literal_lattice(s : String) -> 
InferredType

The lattice type of a float literal.

A literal that fits an f32 stays FLEXIBLE -- it could be either width, and its use decides. One that does not fit is pinned to f64 immediately, because there is no choice left to make: f32 would overflow it to infinity.

#
fresh_collecting

source

A fresh Collecting result cell and the record behind it.

declared is the annotation under test -- what a wasm-to-Wax conversion wrote, which inference is deciding whether to keep -- or None when the source omitted it. needed is preset when the annotation is already known to be load-bearing.

#
functype_matches

source

Whether ft can be used where ft' is expected.

Contravariant in the parameters and covariant in the results, which is the usual rule and the one place it is easy to write backwards: what is expected must accept everything the caller may pass, and must produce something the caller can use. Arities have to agree exactly -- there is no subtyping between function types of different shapes.

#
get_suggestions

source
fn get_suggestions(ctx : 
ModuleContext, name : String) -> Array[String]

Names close enough to be worth suggesting for an unbound READ.

Everything a bare name could have meant: locals, globals, functions.

#
get_type_definition

source

The definition a name refers to, if it resolves.

One of the two things the code generator needs from the checker; the other is the annotation itself.

#
heap_lub

source

The least upper bound of two heap types, or None when they have none.

Concrete types are walked up their supertype chains until they meet, taking whichever is currently DEEPER -- compared by store index, since a supertype is always interned before its subtypes. That termination argument is the whole reason add_type drops a supertype the spec forbids: a cyclic chain here would not terminate.

#
heaptype

source

#
hex_u64

source
fn hex_u64(v : UInt64) -> String

A UInt64 as lower-case hex.

Not reinterpret_as_int64().to_string(radix=16): that renders the top half of the range as a negative number, so a 64-bit memory's ceiling would print as 0x-1.

#
index_structs_by_fields

source
fn index_structs_by_fields(ctx : 
ModuleContext) -> Unit

Index the struct types by their field set, so a literal that omits the type name can be resolved from its fields alone.

Every type is registered before this runs, so the index is complete. A key shared by two DIFFERENT names is marked ambiguous (None) and such a literal must name its type; the same name appearing twice under different conditional branches is one type, not two, and does not.

#
infer_result

source

Fold what was collected into the block's inferred result.

None when nothing reached the exit -- a void body, or one that always diverges. Either way the block produces no value, which is a different thing from producing one nobody can name.

#
infer_struct_by_fields

source

The unique struct type with exactly these field names, if there is one.

This is what lets { x: 1, y: 2 } be written without naming its type. The index is built once, after every type is registered, so the answer is complete; None means either no struct has that field set or several do, and in both cases the literal has to name what it means.

#
int_literal_lattice

source
fn int_literal_lattice(s : String) -> 
InferredType

The lattice type of an integer literal.

The magnitude alone rules widths out, and each exclusion is a real one:

  • Over the 32-bit range it cannot be i32, so it is LargeInt, which defaults to i64 -- not Number, which defaults to i32.
  • Too big for u64 it cannot be any integer at all, so it is treated as a float. Using it as an integer is then a clean type error rather than an overflow in the encoder, which is where the reference used to crash.

The sign is a separate negation in the AST, so what arrives here is unsigned.

#
internalize

source

As internalize_valtype, but as a cell ready to go on the stack.

inline carries the composite type of a synthesized reference -- a string's byte array, an inline function type -- so a diagnostic renders the structure rather than a generated name that means nothing to the reader.

#
internalize_valtype

source

A source value type together with its resolved form.

The pair is what the checker works in: typ keeps the name, so a diagnostic can print what the author wrote, and internal carries the store index, so subtyping can be decided. Resolution can fail, and then there is no pair.

#
is_cont_heaptype

source

Whether a heap type is a continuation.

Continuations form their own hierarchy with no surface cast syntax, so a cast naming one is always a mistake.

#
is_defaultable

source

Does this type have a zero value?

Everything but a non-nullable reference does. A local of such a type has nothing to start as, so it must be assigned before it is read -- which is the whole reason the checker tracks initialization at all.

#
is_effectless

source

Whether evaluating this expression can do nothing but produce a value.

Conservative in the one direction that matters: anything not listed is assumed to have an effect, so the lint never claims a computation is pointless when it might trap, write, or call.

#
join_collected

source

Reduce everything that reached a block's exit to one type.

This is what the whole Collecting machinery exists for. subtype records each delivery -- the fall-through, each br, each caught value -- and this folds them together.

Folded in SOURCE order, which matters twice over: a mismatch names the values in the order the reader wrote them, and recovery keeps the FIRST, which is the one they most likely meant. Continuing with the first also stops a single odd delivery from disagreeing with every subsequent one and producing a complaint per exit.

#
join_value_types

source

The common type of two values reaching one exit, or None if they have none.

Like subtype, this MUTATES: joining a flexible literal with a concrete type pins it, and joining two flexible ones merges their cells so that pinning either later pins both. Without that, a literal reaching a block's exit keeps its default width and the lowering emits, say, an f64 constant as the fall-through of an f32-typed block.

#
label_in_scope

source

Does this label resolve to a frame in scope?

Reports nothing and records no use. It exists to tell an UNBOUND label -- already diagnosed -- from a legitimately void target, which otherwise look the same, both delivering no types.

#
lane_bound

source
fn lane_bound(imm : 
Imm) -> Int?

How many lanes an immediate may name.

The bound comes from the OPCODE, not from the operand. A v128 is sixteen bytes however it is being read, so i8x16.extract_lane admits 0..15 and f64x2.extract_lane only 0..1 -- and the value on the stack is the same v128 in both cases. A shuffle names two vectors' lanes at once, hence 32.

#
leave_function_scope

source
fn leave_function_scope(ctx : 
ModuleContext) -> Unit

Leave a function's scope.

References made after this are module-level again -- a global initializer, a segment -- and so are roots.

#
leftovers

source

The values still on a stack, and whether any of them is poison.

A value of type Error means an error has already been reported, so if any leftover carries one the stack is unreliable and a leftover complaint would be a cascade. The locations are of the leftovers that have one; a value with only a recovery placeholder location is still a real value, just not locatable.

#
lint_ref_cast

source

Report what a reference cast or test does before it is even run.

Only the INNERMOST always-trapping cast of a chain is reported. A cast over a value that can never be produced is unreachable, and whatever it says merely follows from the inner verdict -- the fix belongs at the inner cast. The span is recorded whether or not the report came out, so a longer chain stays quiet past its second cast.

Only the trapping verdict chains that way. A REDUNDANT outer cast is an independent claim about the cast itself -- its target is the type the operand already has, whatever that operand does at run time -- with its own fix, and the wasm validator reports it on the lowered form, where a source chain becomes one ref.cast per cast.

#
literal_type

source

The type of a literal, from its spelling alone.

These are the arms of the instruction match that need nothing but the token: no operands, no name to resolve, no recursion. They commit only as far as the spelling requires, which is what lets 1 become an i64 where one is wanted and an f32 where one is.

#
lookup_array_type

source

The element type an array type declares.

#
lookup_func_type

source

The function type a name refers to.

#
lookup_struct_type

source

The fields a struct type declares.

#
mark_initialized

source
fn mark_initialized(ctx : 
ModuleContext, name : String) -> Unit

#
max_memory_size

source
fn max_memory_size(address_type : 
AddressType, page_size_log2 : Int?) -> UInt64

The largest size a memory of this address type and page size can have.

#
max_table_size

source
fn max_table_size(address_type : 
AddressType) -> UInt64

The largest size a table of this address type can have.

A table has no page size, so only the address type bounds it.

#
mem_lane_bound

source
fn mem_lane_bound(natural_align : Int) -> Int

The lane bound of a memory access that takes one.

Derived from the access width rather than from a shape: a load8_lane reads one byte into one of sixteen byte lanes, a load64_lane eight bytes into one of two.

#
mem_natural_align

source
fn mem_natural_align(meth : String) -> Int

The natural alignment of a memory access, in bytes: the width it reads or writes.

#
memory_receiver

source

Is this name a memory usable as a receiver -- mem.load(..)?

A local of the same name shadows it, exactly as it shadows a Get.

#
missing_else_ok

source

Whether an if without an else is well formed.

A missing else means the false path falls straight through, delivering the parameters it was given. That is only sound when the parameters already ARE the results -- same count, each a subtype -- because otherwise the block promises a value the false path never produces.

#
n_functype

source

A function type, with the duplicate-parameter check.

The check runs even when a parameter's type fails to resolve, because a duplicate name is worth reporting whether or not the types are sound.

#
n_heaptype

source

As heaptype, but a reference may also be to a member of the rec group currently being registered -- which is what lets a group of mutually recursive types be built at all, and what lets it dedup wherever it lands.

#
render_stack

source
fn render_stack(st : Stack) -> String

The stack rendered for a diagnostic, topmost last.

#
report_empty_exits

source

Report the exits that delivered nothing, now that every exit has been met.

Nothing to report when NO exit delivered a value: a block every exit of which delivers nothing is simply void.

#
report_exact_mismatches

source

Report every pass-through value whose type is not exactly the block's inferred result.

Only when the result resolves to a single value type: with no standalone type there is nothing to compare against, and the block has other complaints already.

#
report_leftovers

source
fn report_leftovers(st : Stack, diagnostics : 
Context, location : 
Location, render : (Stack) -> String) -> Unit

Report whatever is still on the stack when a scope ends.

The suppression rule is the one the poison states exist for: a leftover of type Error means an error has already been reported, so the stack is unreliable and complaining about it would be a cascade. Empty, Unreachable and Poisoned all mean there is nothing genuine left.

#
report_missing_hole

source

Report the underflow behind the value a hole just consumed.

The report points at the HOLE, which is the most precise anchor a missing value has -- the pop that noticed the underflow does not know how the missing values are distributed across the holes that will consume them, so it records a placeholder and says nothing.

One report per underflow: the batch is marked, and the fallback covers a placeholder that never reached a hole because recovery dropped it.

#
report_uninitialized

source

Report a read of a local that does not hold a value yet -- or, while a trailing operand is being checked out of emission order, defer it.

Both the ordinary read and a deferred read's re-check come through here, so a re-check that still fails under an OUTER deferral re-defers rather than reporting.

#
resolve_type_name

source

The canonical index of an already-defined referenced type.

A Rec here would mean a group still under construction, which the callers of this -- as opposed to resolve_type_ref -- never look up.

#
resolve_variable

source

Resolve a bare name.

The order is the language's: a local shadows everything. Globals, functions, memories and tables share one namespace, so a local is the only thing that can collide with them -- which is why every receiver test below has to defer to a local in the same way.

#
segment_receiver

source

Likewise for a data or element segment named by seg.drop().

#
set_suggestions

source
fn set_suggestions(ctx : 
ModuleContext, name : String) -> Array[String]

Names worth suggesting for an unbound ASSIGNMENT.

A narrower set than for a read: only a MUTABLE global can be assigned, so suggesting an immutable one would send the reader somewhere that cannot work.

#
storage_subtype

source

Is one resolved storage type a subtype of another?

A packed type is a subtype of itself alone: i8 and i16 are different widths, and neither is a value type.

#
subtype

source

Is the inferred type ty a subtype of the expected type ty_, unifying them if so?

The asymmetry is the point. ty is what was inferred and may still be flexible; ty_ is expected, and comes from a declaration, an annotation or an instruction signature -- so it is always concrete, or a block result being inferred. That is why several shapes are impossible on the right and abort rather than returning false: reaching them means a caller passed an expected type that no declaration could have produced, which is a bug here rather than an error in the program being checked.

pin is what a br_table turns off. Its one value is checked against several targets of legitimately different types, so pinning it to the first would wrongly reject the rest.

#
table_receiver

source

Likewise for a table used as tab[..] or tab.size().

#
tee_target

source

The type a tee delivers, and the reporting that goes with it.

Only a local is tee-able. Everything else recovers with the OPERAND's own type rather than an unknown, because an unknown cannot be checked against anything and would turn one error into a second one downstream.

#
type_get

source

Type a read of a bare name.

Every failure recovers as an error value rather than stopping, and each does so for a slightly different reason: an unbound name has just been reported, a poisoned function was reported at its definition, and a poison local's initializer was reported where it failed. In all three the point is the same -- one mistake should produce one diagnostic.

#
type_trailing_operand

source
fn[A] type_trailing_operand(ctx : 
ModuleContext, run : () -> A) -> (A, () -> Unit)

Check an operand that is written before the values it follows but EMITTED after them, and return a thunk to run at its real slot.

The initialized-locals analysis threads in emission order, so checking such an operand early sees a state that is a SUBSET of the true one. Three things follow, and each is what makes the analysis sound rather than merely plausible:

  • A read that succeeds now would also succeed later, so it is fine.
  • A read that FAILS now might succeed later, once an earlier operand has assigned the local -- so it is deferred, not reported.
  • The operand's own writes are withheld, because an earlier operand runs first and must not see them.

The returned thunk re-checks the deferred reads against the state that actually holds at the emission slot, then applies the withheld writes.

#
unpack_type

source

The value type a field is WRITTEN at.

The other half of the packed story: a write takes a plain i32 and the narrowing is implicit, so unlike a read there is nothing to remember.

#
val_lub

source

The least upper bound of two value types.

Only references have one to compute: any other pair either is the same type or has nothing in common, because the numeric types form no hierarchy.

Nullability is the OR of the two, since a value that may be null on either side may be null in the result.

#
valtype

source

#
walk_fields

source

Apply f to every module field, descending into conditionals under the assumption of the branch each field appears in.

f therefore never sees a Conditional: by the time a field reaches it, the assumption it was written under is already in ctx.cond, which is what every table this pass writes to reads.

Source Files

Powered by MoonBit

Site sourceReport issuePackagesBuild queueSkillsStatistics

© 2026 mooncakes.io