The scrutinee that match binds. It starts with __, so it never collides with a user's name.

Whether a type is one this program can talk about: every name is declared, applied to as many arguments as it takes, and every type variable is bound by the declaration the type is written in.

A parameter is the one place a function type may sit. Its own parameters and result go through wfTy, which rejects a function type, so the types stay first order and the entry check never has to look inside one.

What each operation takes, rather than two Strings for all of them: an operation whose operands are not both Strings is then an arm here, not a new form of Core.Expr.

Scalars can be compared with ===, but constructor values and arrays would end up compared by reference.

The value type of a dictionary receiver, at whichever of the two spellings it was declared. A dictionary operation reads this rather than matching on .dict, because the two spellings differ only in the shape the boundary writes: inside the module both run on the same Map, so both take the same generated call.

What a value's shape can be tested against at one position: a constructor's tag, or a literal it may equal.

Every head a value of this type can take, each with the fields it carries. none where the values cannot be enumerated, so nothing short of a wildcard covers them.

Takes the type declarations rather than the program: a declaration is compiled against the prefix before it, and reading only the types is what lets the proof see that the prefix decides a match the same way the whole program does.

A constructor's fields as a fold's alternative sees them: a field that came round is bound to the answer for it and not to the field, so it is typed at the fold's result.

Retyping a constructor's fields for a fold's alternative leaves their names alone, so the paths the alternative reads are the declared field names — the same ones patParts reads.

What __fold is told about the declared type: its constructors by name, each with which of its fields come round. Read off the same foldKindOf the evaluator walks by.

The rows left once the first column is known to have head h, with that head's own fields spliced in front of the rest. A constructor pattern of the wrong width is dropped rather than spliced: the compiler type checks the patterns before asking about usefulness, so this drops nothing a program can write, and dropping a row only ever makes the answer "useful" — the answer that reports a match as not exhaustive.

The rows left once the first column is known to have none of the heads already listed.

Maranget's usefulness test: is there a value vector that q matches and no row of rows does? Exhaustiveness is this asked of an all-wildcard q, and an unreachable arm is this asked of that arm against the arms before it, so one function answers both.

Patterns are type-checked before this runs, so a head that does not belong to its column's type cannot reach here.

budget is what makes this a total function, and a total function is what lets a proof unfold it. Each step either drops a column or expands a type into one constructor's fields; running out answers true, which fails an exhaustiveness check rather than passing one.

How far useful may descend on the columns it starts with. Each expansion either descends one edge of the declaration graph, which validateType keeps acyclic, or lands in a type argument the column carries; tyDescBudget counts the same thing for the entry check.

The constructors of the type a fold walks, each carrying its fields at the types a fold's alternative reads them: a field that came round is bound to the answer for it. This is the signature the alternatives are type-checked against, and signature cannot give it — the rebuilt node is the declared type with every folded field replaced by the answer for it, which is not a type this language writes.

useful of one column whose signature is handed over rather than read off its type.

A fold's alternatives are matched against the rebuilt node, so the column they sit at has foldHeads and not signature. Reading it at the declared type instead is not conservative: two types may declare constructors of the same name, so a nested pattern typed at the fold's result can name every constructor the declared type has and still leave a rebuilt node uncovered. Below the one column the types are ordinary and useful takes over.

Each branch is useful's own step at one column with signature types ty replaced by some heads, so what it settles is the same thing: a head no row names sends the rows through defaultRows, where only a row that is wild at the column survives. Where that step leaves no column, it is written as the .isEmpty useful answers there rather than as a call at a budget that would have to be unfolded.

One lowered match arm: what the generated code tests before taking it, the names it binds and where it reads each from, and the body under those bindings.

A constructor value, under the key its name is carried under. Agree.encodeValue reads the key the same way, from the constructor's name alone, so the object the compiler writes and the object the reference semantics is encoded to are the same one.

A literal pattern is held to the same rules as a literal expression: an Int53 outside the safe range is no more matchable than it is writable.

Type-checks one pattern against the type at its position and lowers it to the tests the generated code runs and the names it binds, each paired with the path it is read from.

The tests are conjoined left to right by the caller, so an inner test is only reached once the tag it sits under has been confirmed and the path it reads is known to exist.

The top of a fold's alternative. Only the fields are typed differently from a match's, and only at this one level — what a folded field binds is an ordinary type, so anything nested inside reads through patPartsList unchanged.

Naming the node itself is refused rather than typed: the rebuilt node is the declared type with every field that came round replaced by the answer for it, and that is not a type this language can write.

Whether a type's fields can reach target through the declarations they name. Type arguments are searched too, so Tree (Tree Int53) is caught the same way a field of type Tree is.

Whether a declared type can reach itself through the types its fields name. Only such a type binds where it is expanded; one that cannot is written out where it is used, exactly as every declared type was before a type could name itself.

The declared types whose expansion the walk is inside, nearest first, at the arguments they were applied to. A name met again at the same arguments is the knot: it becomes a ref back to the binder rather than an expansion that would not end.

Expands a declared type into the shape the generated code checks an argument against. Recursion is what would make this diverge, and validateType has already rejected it, so no occurs check is needed here — one by name would reject Paginated (Paginated Int53), which is not recursive.

budget counts the name expansions still allowed. A name expansion substitutes the type arguments into the field types, so the result can be larger than what was expanded and the structure alone does not measure the recursion; tyDescBudget is what bounds it from above. Exhausting it is a compile error, so a budget that turns out to be too small loses the artifact rather than weakening the check it emits.

The constructor and field lists recurse through helpers rather than mapM so that a proof about the entry check can unfold them.

The descriptor a type crosses the boundary as: expanded from nothing, so the only binders in it are the ones the types themselves put there.

Every name expansion either descends one edge of the declaration graph, which validateType keeps acyclic and so is at most p.types.length long, or lands in a type argument, of which the type carries at most sizeOf ty.

Unfolds a tail let into a const statement. A let appearing mid-expression has to be wrapped in an immediately invoked arrow to preserve evaluation order, but wrapping the lets lined up at the head of a function as well would make the output unreadable.

The name an exported function takes its argument under, before the entry check hands it to the body under the declared name. The reserved prefix is what keeps it out of reach of a declared name.

The const per parameter that an exported function opens with: the declared name bound to the raw argument, checked against the declared type unless the type is a function, which has no shape to check.

Recursing rather than zipIdx.mapM for the reason tyDesc does: a proof about the entry has to unfold this to see what the body runs under.

The parameter list as it appears in the doc comment. String.intercalate walks an accumulator, which a proof about the characters the doc contains cannot unfold.

The arguments the entry hands the body: every parameter under its declared name, which is what the checks above it have just bound.

The result, read back out through the type the declaration was declared to return. A dictionary declared to cross as a plain object is the only node the walk moves, so where the expanded descriptor reaches none nothing is emitted and the entry is byte-for-byte what it is without a walk.

A declaration becomes two functions: the body, which is where the compiled expression goes and which every call from inside the package lands on, and the entry, which checks its arguments and hands them to the body under their declared names. The entry is what a consumer imports and what decl_correct, decl_traps and decl_refuses are statements about; the split is what keeps a call from inside the package from walking an argument that is already good.

A constructor is carried under the key its own type declares. Written as its own step rather than as an if in the walk below so that the reading can be taken back out of a validated program.

The key a type's constructors are told apart by has to stay free as a field name, and it has to be the key the constructor's name is carried under: a value carries that name and not the type it came from, so two types declaring a constructor of the same name cannot key it differently.

A type naming itself is not refused here. tyDescIn ties the knot where the name comes round again at the same arguments; a type whose expansion has no such fixed point — one applied to a bigger argument each time round — runs out of budget instead, and is refused by name.

A declaration is compiled against the whole program and callsPrecede is what keeps a function from calling itself or a later one. That is what keeps nontermination out of the subset: eval's fuel bounds the proof, not the language. Traversal is map / filter / reduce, which are syntax and cannot recur.

The module a program compiles to under the reading its own types declare. compileProgram takes a reading as given, because what is proved about it holds for any; this is where a program's own one is installed, and where a program whose keys are no reading at all is refused.