ADR-080: An impl Owes Its trait, and a Write Through the Brackets Is Not an Index

Status: Accepted Date: September 15, 2026 Related: ADR-295 (which left both halves of D1 open and named D4’s cost), ADR-285 D1 (a length is an i64, and the trait that made one index rule work everywhere — D2 is that trick a second time), ADR-296 D17 (the emitter knows no types, which is why both of these are decided in std rather than in the emitter)

1. Context

Two refusals or rules the language below already had the shape for.

A trait exists to be checked against. Unchecked, a method the trait does not declare, or one it declares and the impl omits, goes to rustc as E0407 and E0046. And a third: an implementation that pauses where the declaration says sync lowers to async fn against a plain fn, and the language below answers

error[E0053]: method `load` has an incompatible type for trait

A write through the brackets on a map leaves the key unknown. With an indexed assignment, Part I 4.5’s own three-line map example does not compile:

let mut scores = HashMap::new()
scores["Player1"] = 100
error[E0282]: type annotations needed for
              `HashMap<_, i32, BuildHasherDefault<FxHasher>>`
help: consider giving `scores` an explicit type, where the type for type
      parameter `K` is specified

TrustedMap, BuildHasherDefault<FxHasher> and a type parameter K: three spellings the program never wrote. Part III C.1’s class at its worst, because the message names this compiler’s own internal word for a map (ADR-292).

Why the key stays unknown, and it is not what it looks like. Rust’s Index for a map is over whatever the key borrows as — HashMap<K, V>: Index<&Q> where K: Borrow<Q> — so indexing with a &str is satisfied by String, &str and Box<str> alike and pins nothing. The index conversion (ADR-285 D1’s index::at, the identity for anything that is not a number) is innocent: it hands the key through unchanged, and an unchanged key still only borrows.

2. Decisions

D1 — What an impl owes its trait is checked here: three checks under two codes.

A trait this unit does not declare is not checked against, and that is the rule rather than a gap: impl Error for ConfigError names the one trait the compiler reads rather than one a .nika file wrote (ADR-023 D3), and a trait a package publishes is not reached (ADR-295). Silence is the only correct answer about a declaration that is not here.

A walk of its own, and the reason is the ledger’s sync column. The type checker runs before sync::infer — that order is what keeps ADR-288 sound, since the checker resolves the method calls the inference reads — so a rule needing the finished column cannot live inside it. It runs from check_program beside dsl::check and views::check, each of which is separate for the same kind of reason.

D2 — A write through the brackets is an insert, and a read on a map is a T?.

m[k] = v lowers to nikaia_std::index::set(&mut m, index::at(k), v). Set is implemented for a map as insert, which takes the key by value and therefore pins it, and for a sequence as the indexed assignment it already was.

A trait and not two emitter cases, which is ADR-285 D1’s own sentence applied a second time: this emitter does not know types (ADR-296 D17), and xs[0] = 5 and scores[k] = v are the same three tokens. The language below chooses on the container, so a rule applied everywhere cannot be applied to the wrong container.

Only the plain =. A compound m[k] += 1 reads the slot as well as writing it, and reading an absent key is a null (ADR-293 D1), so the form is m[k] = (m[k] ?? 0) + 1, with the fallback saying what an absent key counts as (D2 of that record).

3. Consequences

Part I 4.5’s map example compiles and runs.

Part I 4.7’s trait section is checked end to end. Declare, implement, bound, call — and every way the impl can fail its declaration is answered here rather than below.

4. What this does not decide

This site is open source. Improve this page.