Status: Superseded by ADR-309 — its D1-D4 are D11-D14 there; D5 is not carried (displaced by ADR-035 D3, D2 there)
Superseded in part by: ADR-035, which retires this record’s D5;
ADR-262, which takes §3’s option (a) and retires D2 for an f"…"
Related: ADR-288 D2 (inferred sync fails closed),
ADR-024 (the checker that now walks into holes),
ADR-017 (the template holes this does not change)
Nikaia has two places where code hides inside something the parser treats as one token:
println("total is {stock::total(items)}") // an interpolated string (Part I 4.3)
return dsl html { // a template (ADR-017)
<p>{page::heading(entry)}</p>
} eodBoth are literals in the AST — Expr::LitStr and Expr::Dsl — and both carry expressions
inside them. Those expressions are real: they are parsed, they are lowered, they run. But they
were parsed in the emitter, on the way to Rust, and nothing that runs before the emitter had
ever seen them.
So every analysis in the compiler was blind to them. The symptom is easy to show:
fn add(a: i32, b: i32) -> i32 { return a + b }
fn main() { let n = add(1) } // NK1101: add wants 2 arguments, got 1
fn main() { println("{add(1)}") } // Lowered examples/x.nikaThe same call, the same mistake, and one of the two spellings was checked.
A missed NK1101 is a bad day for one programmer. The second half is worse, and it is the reason
this is an ADR and not a bug fix.
sync is inferred from what a body calls (ADR-288). The inference walks the statements of a
function, collects the calls, and asks the ledger whether any of them can pause. A call inside a
hole was not in that walk, so:
use std::io
pub fn greet() -> String { return "hello {io::read_to_string()}" }was recorded
[fn."greet"]
sync = "inferred"That is a false claim in a file a library ships. A consumer reads sync = "inferred" and puts
greet() inside access or par_iter, where a pausing call is exactly what must not happen. The
ledger has said twice what to do about an analysis that cannot decide — ADR-288 D2 and ADR-010 D1,
an analysis that fails open is a vulnerability generator — and this one did not merely fail open,
it affirmatively claimed the safe answer for an unsafe body.
The root cause is not the hole. It is that the hole’s parse lived in the emitter, which is the last stage, so “parsed” and “analysed” had come apart for one construct. Anything the emitter learns to parse is invisible to everything upstream by default. That is the shape of the mistake, and it is repeatable: ADR-017 added templates two ADRs after interpolation and inherited the same blindness without anyone noticing, because there was no place where a “the code inside a literal” question could be asked.
(a) Parse holes in the parser, into the AST. The honest fix, and the one most languages take:
an interpolated string becomes a node with a list of parts, some literal and some expressions, and
then it is not a literal at all. Rust’s format! does this at macro expansion; C#’s
$"…" lowers to string.Concat in the compiler front end; Swift’s
ExpressibleByStringInterpolation makes the parts an actual argument list.
Rejected for now and not on merit: it changes Expr::LitStr’s shape, and with it the
emitter’s string fast paths (template::literal_length, the String::with_capacity sizing, the
run-copying that measurement already settled at benches/template.nika), the golden fixtures, and
the error corpus. It buys correctness we can get today by a much smaller change, and it can be
done later without any of the decisions below changing meaning.
(b) Re-parse the holes in each analysis. Two call sites today, and a third the next time somebody adds a literal that holds code. This is how the blindness happened the first time.
(c) One function that answers “what code is inside this expression?”, used by everyone. Chosen.
emit::literal_expressions(parsed, expr) is the single place that opens a literal.It takes any expression and returns the expressions hidden inside it: the holes of an interpolated
string, the holes of a dsl html template — including the holes inside a template’s for body and
the collection it iterates. For anything else it returns nothing. Every analysis calls this and
none re-implements it.
literal_expressions drops a hole whose text does not parse and reports nothing. The emitter is
where that is diagnosed, with the span and the message it already has; an analysis inventing a
second error for the same text would be two errors for one mistake. This mirrors Ty::Unknown
(ADR-024): the absence of a claim, not a claim of absence.
Checker::holes walks the result of D1 through the ordinary expr path, so NK1101 and
everything else fire inside "{…}" and inside a template. A hole must produce the identical
diagnostic to the same expression written outside one — that equality is what
a_hole_in_a_string_is_checked_like_anything_else pins, by asserting the two are ==, not merely
that both are errors.
sync walk descends into holes, both directions.contracts::sync takes parsed so the same holes are visible to it. The inference loses the
claim when a hole can pause (the case in §2), and the check holds an asserted sync to its
holes, so NK2202 names a pausing call inside a literal like any other.
String; a plain one is a view.Falling out of the checker now looking at the literal at all: "a {b}" builds and owns its text,
"a b" does not. Ty::view("str") and Ty::named("String") respectively, and a malformed
interpolation is Ty::Unknown per D2. dsl html is Ty::Unknown for now — its result type is
ADR-017’s business, not this ADR’s.
230 tests pass with no ledger drift. That is the load-bearing observation: not one recorded
contract in std.contracts or any example’s ledger changed. Nothing in the corpus had been
depending on the blindness, so this closes the gap without moving any existing claim.
A new class of error is now reachable. Code that has always been wrong inside a hole now says so. That is the point, and it is a source-compatible break in exactly the way a type checker finding a bug is.
The next literal that holds code has a place to go. D1 is the answer to “where does this get seen?”, which did not exist when ADR-017 landed. That is the durable part of this decision.