ADR-093: A Loop That Cannot End Needs No Unreachable `return`

Status: Superseded by ADR-276 — its D1-D3 are D6-D8 there Date: September 15, 2026 Target Version: Nikaia 0.0.8 Related: ADR-070 D3 (which decided this and named it the one real cost of D1), ADR-085 (which emits loop and is the prerequisite), ADR-084 (which added the second half of the test by putting break in the language)

1. Context

fn forever() -> i32 {
    while true {
        let x = 1
    }
}

error[NK1104]: this function hands back `()`, and it declares `i32`

So a function that genuinely never returns — an accept loop, an event loop, a supervisor — had to end with a return 0 that cannot be reached, and a reader of that line cannot tell dead code from a mistake.

ADR-070 D3 decided it, and it is the one real cost of that record’s D1 — no second keyword — which is why the two were settled together.

It could not have been built before ADR-085, whatever the checker did. while true { } is () in the language below and loop { } diverges and is !, so a function whose body is an unconditional loop and whose declared type is i32 was an E0308 there. The checker would have stopped refusing and rustc would have refused instead, about a file nobody wrote. ADR-085 emits loop, so the two halves now agree by construction.

2. Decisions

D1 — A body whose last statement is a loop nothing leaves does not answer for its type.

The tail check is skipped rather than satisfied: there is no value, and inventing one would be claiming something about a program that has none.

D2 — The test is the literal `true`, and no `break` bound to this loop.

Two halves, and the second is ADR-084’s. Before that record break was not in the language, and this entry’s own earlier version argued the work was small because it wasn’t — “the analysis other languages need for this question is, here, one test on the condition”. That was true and is not.

The literal only, never a name that happens to be true: the equivalence is ADR-070 D1’s and it is about the written form. It is also exactly the shape ADR-085 turns into loop, so the checker claims divergence in precisely the cases the emitter delivers it.

D3 — The walk over-approximates a jump leaves this loop, on purpose.

It descends into a lambda, where a break is not bound to this loop at all — so a lambda holding one reads as a way out that it is not. That is the safe direction, and the two failure modes are not symmetric:

the walk says	what it costs
a jump leaves it, wrongly	the unreachable `return` this record removes — where every program already is
nothing leaves it, wrongly	a body that falls off its end, and `rustc` about a file nobody wrote

A precise answer would have to be right; this one only has to lean the same way ADR-090 D3’s does.

3. Consequences

NK1104 stops firing on the shape and keeps firing on the two that look like it: a while whose condition is a name, and a while true a break leaves. Nothing else moves — the check is one call at the tail, and the walk is the one ADR-084 already needed.

#183’s entry closes — a loop that cannot end still has to be followed by a return.

4. What this does not decide

A loop that is not the last statement. while true { … } followed by anything is not this shape, and the statement after it is unreachable — which is a different claim and wants its own diagnostic rather than silence.
A function that never returns for some other reason — an infinite recursion, a call to something that aborts. Nothing here reads a call graph, and a !-valued call is not in the ledger’s type language (open-decisions.md).
Whether the unreachable return should be refused where it is now unnecessary. It stays legal. Taking it back would break every program written against the old rule, which is the polarity ADR-051 D1 states.

5. What is built

check::never_ends and check::a_jump_leaves, and the one filter on the function tail’s span that consults them. Exercised by four programs in crates/nikaia/tests/never_ends.rs: the reproduction, the two shapes that still answer for their type, a break bound to a loop written inside, and the emitted loop handed to rustc and run — which is what makes the claim safe rather than merely quiet.

This site is open source. Improve this page.

ADR-093: A Loop That Cannot End Needs No Unreachable return