Status: Accepted
Related: Part III C.1 (the Iron Rule this restores, and the internal-error path
it already names), ADR-010 D5 (the TrustedMap substitution),
ADR-312 D1 (Shared[T]),
ADR-005 D7 (the diagnostics contract)
The emitter writes type names the program does not: TrustedMap for a map whose
input the operator chose, Rc or Arc for a Shared[T], and — as the language
grows — a deferred-parameter DSL’s shadow struct, a grammar’s generated types,
nikaia_std’s own names. A relayed rustc message can name any of them.
A rule per name would have to be invented again for every new one. The
tempting criterion — put a name back where the substitution is “a name and not
a translation”, as TrustedMap is (same table, same API, same equality), and
leave it in Rust’s words where it is not, as Rc and Arc are not — offers two
options where there are three. Leaving Rc<Conn> and Arc<Conn> standing does
not serve the reader: they wrote Shared[Conn], the page has no word Rc, and
Part III C.1 says outright that “an untranslated backend (rustc) error reaching
the user is a Nikaia compiler bug”. It names the third way in the next
sentence — “if an unmapped error surfaces, the compiler reports it as an
internal error (‘this is a Nikaia bug, please report’) — never as normal
output”.
The case here is the neighbour of that one: the mapping succeeds and produces a message that cannot be about the program. The answer is the same.
Rc<T> and Arc<T> become Shared[T] like TrustedMap becomes HashMap. The
per-name question — is this a name or a translation? — is not asked, because the
answer it was protecting against is covered by D2.
Nested hulls come through whole: Arc<Vec<Rc<Conn>>> is Shared[Vec<Shared[Conn]>],
because the brackets are matched rather than searched for.
“expected Shared[Conn], found Shared[Conn]” is not a fact about the program.
It means this compiler emitted two different Rust types for one Nikaia type, which
is a defect of its own — so it is reported as one, in Part III C.1’s words: this
is a Nikaia bug, please report it, together with the sentence rustc actually
wrote, shown to the reader and appended to a log beside the generated Rust.
Detected by comparing the two, which is what makes it general. A message
rustc itself wrote that way is its own business — two types of one name, from
two crates, is a real thing to say about a real program — so the rule is not “a
message that names one thing twice” but “a message that only became that way
here”. A substitution added later needs no entry anywhere: it is the collapse
that is noticed, not the name.
And the reader is told whose mistake it is. The message says their program may well be fine. A diagnostic that looks like a refusal and is really a compiler bug costs somebody an afternoon of reading their own correct code.
The rule needs no list. Whatever name is added to the substitution, a collapse it causes is caught by the same comparison: a new substitution arrives and says so.
A build that hits this fails. Which programs compile does not depend on this — only what the reader is told about one that does not.
Rc and Arc can diverge for one value at all. The reference-count
inference is what decides (ADR-312); this record says what happens
if it is ever wrong, and says nothing about whether it can be.