2026-09-10, evening. A lay of the land, written while a long rung runs. Less a report than a set of positions worth arguing about.
Two days ago we decided the Rust compiler is the reference for well-typed IR rather than a copy of upstream's. This is what that has turned up since, sorted by who is ahead, and then the more interesting question: where might both be wrong, and how would we know?
digraph {
rankdir=LR; bgcolor="transparent"; pad=0.2; nodesep=0.4;
node [shape=box style="rounded,filled" fillcolor="#f4f0e4" color="#c9bfa7" fontname="Helvetica" fontsize=12];
edge [color="#b0a890" arrowsize=0.7 fontname="Helvetica" fontsize=10];
src [label="a program" fillcolor="#e8e2d0"];
interp [label="the interpreter\n(type-erasing)"];
rust [label="Rust IR" fillcolor="#e3efe0"];
up [label="codexir IR"];
zig [label="zig plug\n(the TYPE oracle: refuses a hole)"];
wasm [label="wasm plug"];
metal [label="bare metal\n(erases types; the MEMORY oracle)"];
out [label="OUTPUT\nvs .expected, the VALUE oracle" shape=note fillcolor="#fbf7ea"];
src -> interp; src -> rust; src -> up;
rust -> zig [label="ir-zig"]; up -> zig [label="run-zig"]; up -> wasm [label="run-wasm"]; up -> metal [style=dashed label="rarely"];
rust -> up [dir=none style=dotted label="ir-diff"];
interp -> out [label="run-interp"]; zig -> out; wasm -> out; metal -> out [style=dashed];
}
Every arrow is a comparison we can run in seconds, and no single one is an oracle for everything. Four roads end at the same output node, and that is the closing of the loop: a value the interpreter, the zig plug and the wasm plug all print, from one text, has been computed three different ways. The interpreter grades values and cannot see a type. The zig plug grades types and, we learned this evening, has holes of its own below the IR. Bare metal is authoritative about memory and identity and erases the very thing we are asking about. Agreement between Rust and codexir is a regression net and nothing more: two front ends can agree on a wrong answer, and this week they did, on a real literal for two hours and on nested patterns for as long as those ports existed.
Each of these is a place our IR carries a type upstream's leaves as a hole or gets wrong, backed by a test on our side and, where it fits, a PR on theirs.
list-length (make-empty 0). Two Roc ports sit on it.Honest inventory, because the essays so far have mostly told the other story.
my-id (x) = x used at Integer and Text: upstream
rejects at check, we pin it to int-default and then say nothing when the Text
use cannot compile. Two honest answers exist and we give neither. This is
phase 3 of the curriculum and the largest open piece of the engine.codexrun runs the program anyway. Upstream halts. An unmade call.rsa-verify and edge-mesh-mint.
Two units, deferred deliberately, still owed.Lazy, vector patterns. Three of
1,269 corpus programs.let, two rows
that cannot reconcile), eighteen are type mismatches we do not raise, nine
are parser resyncs, and a long tail of one to six each.This is the section the reference decision was really about. Once the byte-diff is a net rather than a judge, the question "who is right" needs an oracle that is neither front end, and we have exactly two: the interpreter for values and the zig plug for types. Both have limits that this week made concrete.
The plug is the type oracle and it had holes below the IR. Nested constructor patterns were compiled as wildcards by both hosted plugs. The IR was right on both front ends; the interpreter was right; the plugs agreed with each other and were wrong together. Nothing above the plugs could have seen it, and the only reason it surfaced is that a Roc port's expected value disagreed. A type oracle with a hole is worse than none, because it passes programs it should refuse.
Agreement can be accidental. A first-batch port matched a three-deep nested
pattern and printed the right answer on every arm, because a compiler that
reads the nested part as _ still takes that arm for that input. It was green
for an hour. The fix was two more inputs that must fall through. The general
form: every unit that exercises a discriminating construct needs an input
the construct must reject. We do not have that discipline and we should.
The self-host is blind to whole classes. It has almost no real literals, no nested patterns, no Text literal patterns, no polymorphic record literals with closure fields. It is byte-exact through the zig plug and it was byte-exact while all of those were broken. Its strength, 2,869 definitions of the compiler's own idiom, is also exactly its blind spot: it tests the language the compiler's author writes in.
The counters are exact and prove less than they seem. Substitution counts
and mint counts did not move when real literals stopped typing as error,
because unification with error costs what unification with real costs.
Exact counters were never sufficient; this week they were not even sensitive.
And things we have not looked at. Effect rows on the wire have had one
finding and no corpus aimed at them. Linear types have a gate and no Roc
whetstone, because Roc has none. Records with revised and __record-set
spines. The noexpect marker, which COMPILER-32 says still reaches the wire
from lower-lazy. Each of these is a place where both front ends could be
carrying the same wrong type and no arm would say so.
Forty-six, up from twenty-nine this morning. Grouped by what happened:
| batch | ports | what they found |
|---|---|---|
| the original 29 | closures, iterators, aliases, folds | alias-empty (COMPILER-74); the three iterator ports (PR 140); two zig plug discards (PR 138) |
| today's first ten | closure-returning shapes, recursive sums through lists and records, mutual recursion, a match | nothing: green on every arm, both front ends agreeing |
| today's seven | nested tags, multi-payload, when inside arithmetic, captures, or-patterns, a polymorphic builtin in a let, a no-payload variant |
the nested-pattern miscompile in both plugs; one more COMPILER-74 specimen |
Two things stand out. The curriculum's ordering did what it was for: the phase 2 and 3 files (recursive data, polymorphism, match lowering) are where the finds came from, and the first ten going green was not a waste, it is the floor we now know the closure and recursive-sum territory stands on. And the rate is not uniform: Roc's targeted cases, the ones named for a Roc issue or a regression number, hit harder than the descriptive ones. Roc's own bug history is a map of where a compiler for this kind of language goes wrong, and we have ported eleven of its 167 such cases.
What Roc cannot give us: list patterns and guards (Codex has neither), string
interpolation, Roc's inspect format, anything about effects or linearity.
What it gives cheaply: every corner of structural typing, closures and
recursion, with a mature compiler's answer attached.
None of these is decided. They are the ones I would argue for.
eval_regression_repros and
eval_issue_tests, before any more descriptive ones. Sixty-odd of the 167
are portable. Each is a place Roc's compiler was wrong once.when,
a guard-like if, or a literal pattern carries an input the arm must
reject. Cheap to add now to the 46; cheaper still to require at port time.Adding CDX3002 (an undefined name) this evening is the shape to expect: the
diagnostic itself was one line, and what it exposed was six places the
environment had been silently wrong for weeks, one of them every instance
method's own parameter. A diagnostic is an instrument before it is a
verdict. The same instrument says the concrete-type-mismatch rule cannot
widen past the primitives yet, because the remaining "conflicts" on clean
programs are ours: the desk units and the chapter-scoped names.
6. Aim a corpus at effects. Roc has no whetstone for rows. Cobblestone's own
handler tests are the nearest thing; a curated set of those, run through
the arms, would put the third axis of the type engine under the same light.
7. Process. Two things bit twice today and both have a rule now: a
verification longer than a coffee break gets a heads-up first, and a verdict
comes from an arm or a saved file, never from a shell one-liner. A third
worth writing down: a bundle built with a fix under test lives in ~/runs/
beside its provenance, and the arms take it by environment variable. That
pattern carried three PRs today without anyone confusing which plug was
which.
The reference decision is holding, and the clearest evidence is still the uncomfortable kind: the loop it enabled keeps catching the compiler being wrong in directions we were not looking, including the arm we call the oracle.
The pile got read. One unattended night, thirteen commits, and the corpus
check gate went from 1,146 agree / 123 differ to 1,248 / 21, with the
counter gate at 1,036 / 16 from 1,022 / 30 and the self-host still exact on
the wire. The order was the order of the sort above: the effects axis
(handler discharge, argument-row widening), then the proof normalizer and
induction by cases, proof acyclicity and grammar, the resolver's rules, the
literal ranges and lanes, the narrowing lints with a range prover, the small
rules one unit each, the lexer's and parser's refusals surfaced through
checkdump with upstream's codes, capability scope, pagination, the
chapter scoper, record completeness, punctuality, the cost model, class
instances.
Three things are worth keeping from it.
The census was the only honest instrument. Twice a rule that was correct by upstream's text invented errors on clean programs, and both times the cause was ours: a recursive record ran the proof-relevance walk out of fuel, and a record where an integer belonged was the chapter-scoping gap. The rule got narrowed both times, the gap got fixed once, and the second time it was the scoper that fixed the desk family -- twenty counter units at once. Widening a rule without the census is how a checker learns to lie.
The parser is now a reporter, not a resync machine. Its own accounts of what it cannot read stay uncoded; the messages that are upstream's refusals carry upstream's number and halt the driver, as the lexer's do. A skipped line is a verdict only in the two shapes upstream calls one.
What is left is small and named. Three Integer vs Fun mismatches wait
on the post-scoper census; two units want a second CDX1071 upstream's
expression parser emits twice; one punctual and one realtime unit are a
count each. The counter side's sixteen are mostly the typeclass family:
upstream synthesises __show_T and __compare_T from deriving, and the
class-instance rule here reads the clause instead of the synthesis. That
synthesis is the next counter-parity chunk, and it is a desugarer port, not
a checker one.