catch Over an Expression That Cannot Fail Is RefusedStatus: Superseded by ADR-308 — its D1-D3 are D6-D8 there, its D4 is D9 as displaced by ADR-296 D24 and D38, its D5 is D10
Date: September 15, 2026
Target Version: Nikaia 0.0.8
Related: ADR-292 (the catch this refuses one shape of),
ADR-023 D8 and D9 (where a failure leaves, and the one that comes
out of a grammar), ADR-025 D1 (NK2605, the same question asked
from the other end), ADR-090 (the round that found this)
fn energy(text: &str) -> i64 {
return text.len() as i64 catch { 1000 }
}error[E0308]: mismatched types
|
| Ok(value) => value,
| ^^^^^^^^^ expected `i64`, found `Result<_, _>`text.len() is in the ledger and carries no throws. The catch lowers to a
match over a Result all the same, so the program does not compile and the
message names a match and an Ok arm the author never wrote —
Part III C.1’s class.
Found while building a fixture for ADR-090, which is why the
reproduction is that record’s own opening line: the catch there was written to
ignore its error and turned out to have none to ignore.
The question is already asked every day, in the other direction.
ADR-025 D1’s NK2605 refuses a call that can fail where nothing
handles it, and its rule is that the ledger is the fact: “reported only where
the callee’s contract says it can fail … a callee no ledger describes says
nothing here”. This is that standard read from the other end.
catch whose guarded expression is known not to fail is NK1134.Known, not merely unproven — D3 is the whole of what that means.
This is the decision rather than the smaller change. The alternative is to emit the expression without the match
and say nothing, which takes the program the author wrote and quietly deletes a
block from it. That block is checked code: a return inside a handler is the
function’s return (ADR-292), so dropping it silently changes
what the program does. And a handler that can never run is a belief about the
program — the author thinks something here can fail — which is worth a
sentence whether or not it costs anything to keep.
While a guarded expression is walked, the checker records something here can fail and something here could not be looked up separately:
| the walk found | what it means | NK1134 |
|---|---|---|
a contract carrying a throws |
the catch has work |
quiet |
| a call no contract describes | no answer | quiet |
a dsl … from … |
a parse can fail (D4) | quiet |
a nested catch |
no answer (D5) | quiet |
| neither, and everything resolved | nothing can fail | refused |
Part III C.4 is what forces the split: a call nobody has written down says nothing about whether it throws, and letting that read as it cannot would refuse programs that are right. The refusal fires on known not to fail, never on not known to fail.
ADR-023 D9: a parse failure leaves the parser as the Nikaia error
it is and lands in the catch beside the dsl. A dsl … from … is not a call
and carries no contract, so nothing in the ledger says so. The corpus is what
said so — access-log, calc, config, json, k-nucleotide and report
were all refused the first time this ran over examples/, six at once, which is
the evidence D3’s polarity is not theoretical. A dsl template block
(ADR-017) and an asm block are the emitter’s business rather than
this walk’s, so both answer no answer instead.
catch makes the outer one quiet, not refused.(text.parse() catch { 1 }) catch { 2 } really does have nothing left for the
second handler — the first consumed it. Saying so needs to know what a handler’s
own failure does, which is ADR-292’s question and is not settled
here. So the outer guard is told no answer, and the shape stays a program.
This is a deliberate hole, in the direction that cannot refuse a program that is
right.
NK1134, at the statement carrying the catch. The help is the whole repair:
delete the catch and its handler: the expression is the value.
Nothing in examples/ or tests/samples/ is refused, and no recorded
specification verdict moves. The cost is two booleans on the checker, set on
paths that already existed — may_fail_here learns one line before the early
return it already had, and reached_method(None) one before the gate it already
had.
#230’s entry closes — a catch on an expression that cannot fail
does not compile — with the polarity its closure statement demanded checked
both ways and by the corpus.
catch has no span of
its own; ADR-081 D2 built the first expression-level span and
this would be the second. The sentence carries the answer meanwhile.catch whose handler can never be reached for some other reason. Only
the Result shape is decided here; an unreachable handler under a guarded
expression that can fail is not this record’s.dsl X from e with X.rule(e), and it is
decided and not built — which is the only reason D4 is phrased about the
old form. On the day it is built, the entry is an ordinary call and the
question stops being special-cased: it is answered from the callee’s contract,
like every other call. So a generated entry rule has to carry a throws, or
NK1134 will refuse the eight programs D4 just found. Named here because that
is the shape of a defect nobody meets until the migration, and because D4’s
line is what has to be deleted then rather than edited.NK2605 and NK1134 should be one diagnostic. They ask one
question and answer opposite halves of it, and the repairs have nothing in
common — one adds a throws, the other deletes a block.Checker::guarded, a Guarded of two booleans replaced on entry to a
TryCatch and restored after it; the two marks in may_fail_here and
reached_method, each placed before an early return that was already there;
guard_has_no_answer for the unresolved call, the nested catch, the template
and the asm; the DslFrom arm’s one line; and nothing_here_can_fail, which
is the diagnostic. Exercised by six programs in
crates/nikaia/tests/infallible_catch.rs — the reproduction, four shapes that
are refused, three that are not, the nested catch, the grammar, and a sweep of
every .nika in examples/ and tests/samples/ that fails if D4’s line is
removed.