Conformance
Enforced at ox check and ox build over the closed catalog (elaboration-time diagnostics, not
check rules):
| Obligation | Diagnostic |
|---|---|
| Impl provides every declared member | OE0670 ImplMemberMissing |
| Impl member not declared by the trait / signature mismatch (incl. parameter-name mismatch on invocation-plane members — wire arguments bind by name across every impl of a callable) | OE0671 ImplMemberExtraneous |
| Orphan rule | OE0672 OrphanImplViolation |
Two impls of one trait with <:-comparable targets, or targets sharing a declared common descendant | OE0673 ImplTargetsOverlap |
| Supertrait impls present | OE0674 SupertraitUnsatisfied |
Self discipline (incl. the invocation-plane receiver rule: fn/mutate members lead with self) | OE0675 SelfMisuse |
| Genuinely unsupported member shapes: trait default bodies, inherent (bare-impl) members, unrecognized forms | OE1326 TraitMemberNotYet |
| Bare member atom over an uncovered type | OE1327 TraitMemberUncovered |
No-overlap (OE0673) instantiates the mechanized coherence contract by construction — a nominal
target is a TraitBound with satisfied T := T ⊑ target — so at most one impl covers any
declared instantiable type and there is never a specificity question. Both arms matter:
impl Adulthood for Person + impl Adulthood for USPerson is OE0673 (the “default + override”
pattern is rejected by design — write disjoint targets, or one impl whose body branches), and
impl T for Person + impl T for Customer is OE0673 when some pub type Employee <: Person, Customer is declared (the common descendant would sit under two clauses). One residual cannot be
closed statically — the set of an individual’s runtime classifications is not known at compile
time: an individual dynamically classified under two <:-incomparable
covered targets with no declared common descendant. Its semantics is defined, not accidental — in
the rule plane the clauses are independent sufficient conditions (both may fire; the union is
their disjunction); in the invocation plane an ambiguous receiver is a loud runtime refusal.