ADR-174: A Bound Is Enforced Where It Is Used

Status: Superseded by ADR-295 — its D1-D3 are D15-D17 there Date: September 20, 2026 Target Version: Nikaia 0.0.106 Related: ADR-078 (the trait declaration and the bound), ADR-074 D1 (a parameter is a type inside the body, a variable at a call), ADR-023 D3 (a trait the compiler reads rather than one a .nika file wrote), #193 (the record this takes step 3 of), Part III C.1 and C.4

1. Context

ADR-078 made trait Speaks { … } and [T: Speaks] real, and the bound did one of the two things a bound is for: it put say in reach of the body, so x.say() resolves and a member no bound declares is NK1126.

The other thing a bound is for is to say which types may stand there, and nothing asked it. Measured:

struct Rock { weight: i64 }

fn tell[T: Speaks](x: T) -> String sync {
    return x.say()
}

tell(rock)      // accepted

The program passed every stage of this compiler and the language below answered the trait bound Rock: Speaks is not satisfied, about a file nobody wrote — Part III C.1’s class exactly, and the same class the generics tests were written against in the first place.

Why it was not asked is that one half of the question had no table. The ledger says Speaks is a trait (Ledger::traits, ADR-078 D3), which is what NK1126 needs. It did not say Dog answers for Speaks, which is what a call needs, and that claim is made in exactly one place: the impl head.

2. Decisions

D1 — The ledger records who implements what.

Ledger::implementations: a trait’s name to the set of types whose impl names it. Written where the impl stands, merged when a program’s ledger absorbs its units’, and not written to the ledger file — for traits’ reason and in the same breath: nothing outside the unit can name one of these traits (ADR-078 §4), so nothing outside it can ask this question either.

In the ledger and not in the checker’s own walk, which is the whole of why this is a decision rather than a patch. impl Speaks for Dog may stand in a different file from the fn tell[T: Speaks] that asks, and one file’s walk sees one file. Measured: a two-file project that builds and runs was refused by the first shape of this check, which is C.4’s correct program refused — the failure a refusal is most expensive in.

D2 — A call whose type does not answer for the bound is refused here (NK1164).

At the call, the binding that already answers what did the argument make T (ADR-074 D2) is asked the second question too. A method’s own parameters carry bounds the same way, and one written call is one rule (ADR-066), so both call paths ask it.

Two sentences, because there are two readers. A concrete type is told to write the impl: write impl Speaks for Rock { … }, or pass a type that already has one. A parameter of the caller’s own cannot be — V is a name a further caller fills in, and impl Speaks for V is not a line anybody can write — so it is told to widen its own bound: add it to the bound: [V: … + Speaks]. Part III C.2 owes every diagnostic a way out, and a way out that cannot be taken is not one.

D3 — It fails open in three places.

C.4 is the other half of C.1’s page, and a correct program refused is worse than a wrong one passed on to rustc. So the refusal is withheld where this compiler could not have the answer:

• A trait this unit does not declare. impl Error for ConfigError names a trait the compiler reads (ADR-023 D3) and a trait a package publishes cannot be reached at all yet; traits::check draws the same line one rule over.
• An argument this compiler could not type, which binds nothing.
• A parameter that carries the bound, which answers for it — there the caller did not pick the type either, and that is D1 of ADR-074 read at one remove.

3. Consequences

A bound is worth something at both ends now. It was already the thing that says what a body may do with its parameter; it is now also the thing that says what a caller may hand in, which is what makes the first half safe: a body that calls say on its T is a body whose callers have all been asked.

The impl table travels with both spellings. Inside a package a type is Dog and to a consumer it is pets::Dog, so absorbing a module records both. A bound cannot name a path today (#193 step 1), so the qualified half is what the next step will need rather than what this one uses — and an extra spelling can only make the check fail open, which is the side D3 puts the doubt on.

4. What this does not decide

• A bound that names a path, [H: http::Handler]. That is #193 step 1 and it waits on a trait being reachable across a package, which ADR-078 §4 calls a question about modules rather than about traits.
• Resolution through the implementing type’s own entry. x.say() on a [T: Speaks] resolves through the trait’s entry, which is the right answer for its signature; whether a call should reach the impl’s own is #193 step 4 and nothing needs it yet.
• A bound on an impl’s own parameter, which has nowhere to stand (ADR-074 §4) and is untouched.
• Two bounds that declare the same method, which is ADR-078 §4’s and stays there.

5. What is built

All of D1, D2 and D3.

• Ledger::implementations, written in Ledger::infer’s Item::Impl arm and merged in absorb_renaming with both spellings.
• Checker::declared_bounds — each function’s bounds under the key a call resolves to, read from the AST because the ledger’s signature has no column for a bound and a bound cannot name a path, so a trait a bound names is a trait this unit declares.
• NK1164, with its two sentences, asked at the free-call and the method-call site from the binding both already build.
• crates/nikaia/tests/traits.rs: the refusal, the + list, the parameter that carries the bound and the one that does not, the trait nothing here declares — and the accepted program compiled and run, because a bound that type-checks here and not below would be worth nothing.
• Measured on a two-file project that builds and runs, which is what moved the table from the checker into the ledger.

This site is open source. Improve this page.