Status: Superseded by ADR-286 — its D1-D5 are D31-D35 there
Date: September 21, 2026
Target Version: Nikaia 0.0.132
Closes: #141 (a path whose head names
nothing is not refused), which is the second half of NK1171
Related: ADR-051 (NK1117, nothing declares this name),
ADR-010 D1 (absence is read fail-closed, and a wrong value is
worse than a missing one), ADR-104 (a description is reviewed
like code), ADR-140 D5 (a module nothing describes yet is left
alone)
Op::Mul beside enum Op { Add, Sub } is NK1171 since the compiler learned
to compare the name against the declaration it had already read. nowhere::wobble
was not refused at all, and what the reader got was the language below:
failed to resolve: use of unresolved module or unlinked crate `nowhere`Crate is not a word this language has, and the file it is about is one nobody wrote — Part III C.1. The entry that recorded it also recorded why it stayed open, and the reason was good: a module of a package, an item of a foreign crate and a name no ledger has been told about all look the same from inside the checker — an absent key — so refusing on absence would refuse correct programs, which C.4 forbids.
And the measurement is what made it answerable. Instrumenting the path arm
over the whole corpus turned up seven distinct paths used as values —
Summary::merge, Report::merge, Refused::NoStatement, Refused::NoDatabase,
Op::Times, Op::Divide, Json::Null — and not one has a head this
compiler has not read.
struct, an enum,
a grammar, an opaque handle, a type parameter, an extern name;.nika file beside this one
(Part I 9.1);std module.Every one of the five is something this compiler has already read — three of
them were written down somewhere before this record and the walk that asks them
in order is what was missing. So the refusal is not this key is absent; it is
this word answers to none of the five things a word in front of a :: may be.
head:: answers for the head.A described crate is a list of its items, and no table carries the crate’s
own word on a line of its own. So the last question the walk asks is a
prefix: if either ledger has any key beginning head::, the head is one
this build was told about, whatever the member turns out to be.
Without this, nikaia describe’s own output would have been refused by the
compiler that asked for it.
Part III C.2: a way out that cannot be taken is not
one. Each of the three the message offers is a file the reader writes — a
.nika file beside this one for a module, a [dependencies] line for a
package, nikaia describe <head> for a foreign crate — which is the whole
difference between this and unresolved module or unlinked crate, where the
reader is told what failed and not what to do.
The list is a list of permissions and not of prohibitions: a head that
answers any one of them is left alone, and the refusal fires only where all five
are silent. That is ADR-010 D1’s polarity applied to a refusal
rather than to a claim — a missing refusal costs a rustc message, and a wrong
one costs a correct program.
The files of a package share one namespace
(Part I 9.1), so Shade::Even in main.nika names an
enum that may stand in shades.nika — and the tables D1 asks first are this
unit’s. Written against those alone the refusal is a correct program
refused, which is the one thing this checker may never do, and the same shape
ADR-182’s package had one construct over.
Read off the item tree of the other files and not off a ledger, because a
ledger records what a type promises and what is asked here is only that the
word was written down: a private enum a neighbouring file declares is a head,
whatever its contract says.
NK1171’s other half closes, and the two refusals divide the ground
cleanly: NK1171 is a member a type this compiler read does not have, and
NK1181 is a head nothing declares.tests/specification/COMPILES.txt recorded each of them as refused — by
rustc, after lowering — so neither was ever a program. What changed is who
says so and in what words: a head the block does not declare is now this
compiler’s sentence with a way out, before the language below is handed
anything. That is C.1 closing rather than a
regression, and the two baselines together are what show it.BTreeMap and a walk of the
package’s other item trees, at the paths that reach the fail-open — which is
only the ones no type and no ledger answered.io::wobble is not refused here: the
head is a module std’s ledger declares, and what that module holds is the
ledger’s question. ADR-140 D5’s a module nothing describes yet
is the same line seen from the other side.text beside std::text is the
consumer’s to name apart, and the rule that the local one wins is
[Checker::a_module_used_before_it_is_introduced]’s and not this record’s.All of D1 to D5, at 0.0.132.
Checker::a_head_nothing_declares, called where the path arm used to fall
open, with NK1181 and the three-way way out.crates/nikaia/tests/qualified_names.rs holds the line from both sides: a
head nothing declares is refused, the corpus’s own heads are not, and a std
module stays a head whatever stands after it.crates/nikaia/tests/project.rs builds and runs the two-file program D5
is about, because a single-file test cannot see it: every unit test of the
refusal passed while that program did not build.