RFD 0026 — Trait rule members: clause-union dispatch, conformance, and the implements intrinsic

• State: accepted — implementation planned
• Opened: 2026-06-10
• Decides: the complete semantics of the trait atom’s contents — what may be declared inside pub trait and provided by impl Trait for Type, how rule members evaluate (clause-union with a static coverage gate), how fn/mutate members dispatch (receiver-resolved), the conformance obligations (completeness, orphan, no-overlap, supertraits), the reflective conformance surface (TraitRef, implements), and member naming. Settles issues #202/#203/#204 (Gustavo’s trait report) and the ArgUFO // TODO: implement trait feature demand. Design discussion: .local/research/traits/DESIGN-2026-06-10.md. Companion: RFD 0025 (check discharge; merges first — see Sequencing) — trait check members monomorphize into ordinary RuleMode::Check rules whose discharge follows 0025 unchanged, and this RFD amends 0025 D1 (see D6).

Prior state (verified at 8deb583): trait/impl declarations parse and reach the wire as shapes; bodies are swallowed by eat_balanced and lowered as Vec::new() (§12.2), so a rule member written inside an impl silently never exists — check and build stay green (#202). No calling convention, no conformance checking, no way to test conformance in a rule body (#204). The book promises only fn signatures in traits; rule members are new surface. The parser accepts <: for supertraits (grammar.rs::trait_decl) while STATUS documents : — a pre-existing three-way drift this RFD resolves (D5.5).

Question

A trait that carries nothing is a name. The recorded design lineage (redesign charters; the five-atom settlement) made the trait atom Argon’s behavioral contract: concepts say what something is; traits say what something can do. For a language whose behavior is mostly rules, “what something can do” must include rules — Gustavo’s pattern:

pub trait Adulthood {
    derive Adult(Self)
}

impl Adulthood for USPerson {
    derive Adult(p: Self) :- p.age >= 18
}

pub derive IsAdult(p: USPerson) :- Adult(p)

What does Adult mean as a predicate, who provides its clauses, what may call it, what guarantees conformance, and how does a program ask whether a type implements a trait?

D1 — Rule members evaluate by type-guarded clause union; dispatch is derivation

A trait declares the member signature; each impl contributes a clause. The impl above elaborates to the ordinary rule

derive Adulthood::Adult(p: USPerson) :- p: USPerson, p.age >= 18

(the head-parameter annotation injects the membership guard through the existing type-test lowering, which closes correctly over <: since #199). A second impl for another type adds a second clause with the same head — Datalog unions same-head rules natively. No new evaluation machinery exists or is added: monomorphized member rules flow through the classifier, stratifier, the #171 evaluability gate, and the reasoner as ordinary RuleDecl events.

This is not a departure from Rust dispatch — it is what dispatch becomes in a bottom-up engine. The fixpoint evaluator has no call sites; an atom is a join. “Select the body by the value’s runtime type” (Rust dyn) transposes to “select the clause whose type guard the individual satisfies.” The no-overlap rule (D5.3) keeps clause selection single-valued per declared type: at most one impl covers any declared sortal type, statically checked. Per individual, Argon’s multiple classification admits one residual the static check cannot close (an individual instantiating two <:-incomparable covered types); its semantics is defined, not accidental — see D5.3.

Wherever a Rust-static reading would compile at all (the argument’s static type covered by exactly one impl), clause union gives identical answers. The programs where it gives more are exactly the polymorphic rules the feature exists for:

impl Adulthood for USPerson     { derive Adult(p: Self) :- p.age >= 18 }
impl Adulthood for GermanPerson { derive Adult(p: Self) :- p.age >= 18, p.has_residence }

pub derive CanVote(p: Person) :- Adult(p), p.registered   -- heterogeneous, per-subtype

Rust expresses that with bounded generics (<T: Adulthood>) or dyn — machinery v0.1 defers (OE0667). Clause union delivers it with what the engine already does.

Specialization and inheritance are rejected (Ivan, 2026-06-10): traits are Rust-exact. No “more-specific impl wins” — overlapping impl targets are an error (D5.3), and any future priority-between-clauses story belongs to defeasibility, not dispatch. Traits form no subsumption lattice and never enter the concept lattice.

D2 — Two planes: all five member forms, split by how they are consumed

Query members, precisely. The trait-side signature is the full §7.4 query signature: query Ident '(' member-params ')' '->' TypeExpr ';'. The impl provides a full §7.4 body (select … from …); the trait signature fixes the parameter sorts, the return type, and thereby the projection shape every impl must produce. Self is admitted in parameter positions only; Self in the return type is refused (OE0675) — a return-position Self makes the union endpoint’s type a union over impl targets, which needs union types (#184) or bounded generics (V1); tracked as an explicit non-decision. With a Self-free return, both consumptions are well-typed: in rule bodies the member’s head participates in the §7.3.1 vocabulary like any query head; as a dispatch endpoint, Trait::member(args) returns the union of the per-impl results (each clause guarded by its target).

Member signatures in the trait must mention Self in at least one parameter position (else the member is not about the implementing type and belongs at module level — the diagnostic says exactly that). Multiple Self positions are legal; every Self position is guarded/substituted.

Out of scope, refused loudly (not silently): trait-side default bodies (a default rule body needs structural bounds on Self to typecheck against fields — V1 bounded-generics territory, OE0667), generic members, bounded generics, return-position Self, per-standpoint impls (recorded open question; impls are standpoint-global), associated type/const (already reserved).

Grammar scope (corrects a §5.4 conflict found in review): the member grammar above is the item grammar for trait impls (impl Trait for Type). Bare impls (impl Type { … }) keep §5.4’s item set unchanged (any declaration kind, including rel and associated items); conformance obligations D5.1/D5.2 apply to trait impls only.

D3 — The coverage gate: bare atoms require full coverage; partiality requires an explicit guard

Clause union’s one honest weakness against Rust: in Rust, calling a method on a type with no impl is a compile error; under naive union, a member atom over an uncovered type is just false — the silently-vacuous class this project exterminates on sight.

Coverage, defined. Coverage is computed over the workspace-closed catalog using the metacalculus sortality metaxis (§4.1): a declared type S is instantiable iff S is sortal (non-sortals — categories, mixins — carry no identity principle and admit no direct instances: every individual is classified through some sortal, so non-sortals need no covering themselves; their sortal descendants do). A static type T is fully covered by a trait’s impl set iff every instantiable declared S ⊑ T (including T itself when sortal) satisfies S ⊑ targetᵢ for some impl target. This is a finite catalog scan — decidable at ox check/ox build.

The gate:

1. A bare member atom Adult(p) requires p’s static type to be fully covered. Not fully covered ⇒ OE1327, whose help names the uncovered instantiable types and offers both fixes — add the impl, or write the guard.
2. Partial coverage is legal only under an explicit conformance guard: implements(meta(p), Adulthood), Adult(p). Dispatch that can fail is always visible in the source; uncovered individuals are excluded by the guard, not by silence.
3. A member atom over a type with no covering impl anywhere is always OE1327 (the atom can never fire; the guard would be vacuous too — the help says so).

Guard semantics under multiple classification. meta(p) is multi-valued (one row per <:-minimal classifier, §4.4). The guard is existential by construction — meta is a relation and the conjunction is a join: implements(meta(p), Tr) holds iff some minimal classifier of p is covered. That is the intended reading: the member can fire for p exactly when some covered classification applies, and the clause that fires is the one whose guard that classifier satisfies.

D4 — Naming: Trait::member qualified heads; catalog keyed by qualified path

• The member predicate is one name: pkg::mod::Adulthood::Adult (the trait’s module owns it). Per-clause rule identities qualify further by impl target, so clauses are distinct events with one shared head.
• The rule catalog’s runtime keying moves from bare short name to qualified path, with short-name lookup retained as the unambiguous-suffix resolver (the #180 pattern applied to rules). This fixes the pre-existing cross-module derive Foo collision class as a forced move.
• Call forms in rule bodies: Adulthood::Adult(p) (qualified — always legal; qualified predicate atoms get wired by this work); Adult(p) (bare — legal when exactly one provider of that name/arity is in lexical scope; ambiguity is an error naming the candidates, mirroring §12.4’s collision rule). No postfix p.Adult() sugar (Ivan, 2026-06-10): it buys spelling only and collides with field-access space (p.Adult is OE0204 territory). Method-call syntax arrives with the invocation plane, where §12.4 already promises it for fns.
• OE0223/OE0204 become trait-aware: when an unresolved name matches a trait member in scope, the help states the member, its trait, and the legal call forms.

D5 — Conformance obligations (elaboration-time, not check rules)

All catalog-closed, all enforced at ox check and ox build; none depend on the RFD 0025 runtime path:

1. Completeness — a trait impl provides every member its trait declares. OE0670.
2. Extraneous / mismatched member — a trait impl provides a member the trait doesn’t declare, or with a different signature (arity, parameter types, return type, plane). OE0671. (Bare impls are exempt — they have no contract; §5.4 governs them.)
3. No-overlap (coherence) — two impls of one trait are rejected (OE0673) when their targets are <:-comparable or share a declared common descendant (both catalog-decidable). The second arm is what multiple classification demands: impl T for Person + impl T for Customer with a declared pub kind Employee <: Person, Customer would put every Employee under two clauses. The worked counter-example for the first arm: impl Adulthood for Person + impl Adulthood for USPerson is OE0673 — the natural “default + override” pattern is rejected by design (no specialization; write disjoint targets, or one impl whose body branches). Residual, defined: an individual dynamically classified under two <:-incomparable covered targets with no declared common descendant (pure multiple classification) cannot be excluded statically under OWA. Semantics: in the rule plane, clauses are independent sufficient conditions — both may fire and the union is their disjunction (well-defined, documented; not an error). In the invocation plane, an ambiguous receiver is a loud runtime refusal naming both impls — never an arbitrary pick.
4. Orphan rule — impl Trait for Type must live in the package declaring Trait or the one declaring Type (§12.4, previously reserved). OE0672.
5. Supertraits as requires-constraints — impl Sub for T demands impl Super for T exist (Rust-exact; not inheritance). OE0674. Surface token: supertraits are spelled : (pub trait Repaintable: Drawable). Honestly stated: (a) the parser today implements <: (and the shared supertype_clause also admits the specializes keyword — both removed for traits in slice 0) for trait supertraits (grammar.rs::trait_decl), while STATUS.md documents : — STATUS was wrong about what’s built; (b) : in concept headers means MLT instantiation — a distinct, non-conflicting context (a trait header is never a concept header; Rust likewise overloads : by position). Slice 0 switches the trait production to :, makes <: after trait Ident a parse error with a fix-it (no in-repo source uses it), and corrects STATUS. <: stays the concept-lattice operator exclusively.
6. Self discipline — Self resolves only inside trait/impl bodies (trait: the obligation’s type parameter; impl: the target type); misuse, a trait member signature with no Self parameter position, or return-position Self (D2) is OE0675.

Member forms whose implementation slice has not landed are refused at parse with OE1326 (TraitMemberNotYet) — the gate that makes #202’s silent swallow structurally impossible from slice 0 onward.

D6 — Reflective conformance: TraitRef and implements

• TraitRef — a new reflective sort parallel to TypeRef (RFD 0023): values are handles into the closed declared trait catalog, carrier Value::Name. Deliberately not folded into TypeRef — traits stay off the concept lattice. TraitRef does not join the Metatype <: TypeRef <: Entity chain; it is a sibling sort under Entity.

• implements(t: TypeRef, tr: TraitRef) -> Bool — the fifth reflection intrinsic, materialized as the RT-closed reserved-head relation $implements from ImplDecl events (the $iof/$specializes pattern, #132) with two closures folded in: supertrait closure (implements(T, Sub) → implements(T, Super) — the D5.5 constraint’s logical consequence, not inheritance) and target upward-coverage along <: (an impl for Person covers USPerson), coherent with #199.

• implements is exempt from OE0212 (MetaArgUnbound): unlike the type-position arguments of meta/iof/specializes/extent, both positions of implements may be free — $implements is a finite catalog-closed relation and enumeration is the intended use (free t: all implementing types; free tr: all traits of a type; instance-level composes with meta(x), #135). §4.4’s intrinsic invariants are amended accordingly (the “type-position argument is a TypeRef value” sentence and the OE0212 rule both carve out implements; its second argument is TraitRef-sorted). Being catalog-closed also makes not implements(…) stratification-safe. An implementors(Trait) -> Set<TypeRef> expression-plane intrinsic rides the same materialization.

• implements is available in both planes: rule atoms (including NAF) and boolean expressions (if/match scrutinees in fn/mutate bodies, executing since #192/#194).

• Amendment to RFD 0025 D1 (applied to 0025’s text when both RFDs are on main; 0025 merges first): the catalog-level classification sentence

  a check is catalog-level iff every variable in head and body is TypeRef-sorted

  becomes

  a check is catalog-level iff every variable in head and body is reflective-sorted (TypeRef, TraitRef, or Metatype)

  so that trait-conformance checks — Gustavo’s PersonImplementsAdulthood — classify catalog-level and discharge at ox check through 0025’s harness, #[static] by convention. This RFD builds the vocabulary; 0025 owns discharge. Without the amendment, a free tr: TraitRef variable would misclassify the check as instance-level.

D7 — Wire, drift, and what does NOT change

• Member rules are emitted as ordinary RuleDecl/ComputeDecl events — the runtime and reasoner load them with zero changes. No new AxiomKind.
• ImplDeclBody.items (already Vec<CborValue>, “rule_decl-shaped”) carries the member rules’ identities/provenance for tooling and conformance — not evaluation. TraitDeclBody.methods carries member signatures (name, arity, parameter types, return type, plane). Both fields exist today as empty vecs; the wire was built for this (§12.2’s stated intent).
• Lean Syntax/Decl.lean already models TraitDecl.items/ImplBlock.items : List Decl — the Lean was ahead; Rust catches up. Stale Lean doc annotations the token change invalidates (TraitDecl.supers “via <:”; Substrate/Trait.lean/Conditional.lean citing “spec §13”) are corrected in the Lean PR. Drift gate: TraitAtom/TraitDecl/ImplBlock shapes unchanged; the member-signature carrier aligns by the usual @[language_interface] discipline.

Lean obligations (before the Rust slices, per workflow)

1. Monomorphization conservativity — elaborating a trait/impl catalog adds a finite concrete rule set; the extended program’s well-founded model restricted to the old vocabulary is unchanged, and stratification is preserved given D5.3. Restates the legacy parametric-rules result on the modern Reasoning/Datalog/ spine. The load-bearing theorem.
2. Coherence instantiation, by construction — a nominal impl target is a TraitBound in Conditional.lean’s sense: bound.satisfied T := T ⊑ target. The obligation is to build that instantiation and prove: the D5.3 catalog check (no <:-comparable targets, no declared common descendant) implies unique applicability over declared sortal types, whence coherent_of_unique_applicable applies. The per-individual multiple-classification residual (D5.3) is outside the theorem’s scope and documented as such — the theorem speaks about types, not individuals.
3. Conformance decidability — completeness/orphan/overlap/coverage/implements are finite catalog scans; structural tier (§10 ladder).
4. Substrate/Trait.lean member-signature model mirroring TraitDeclBody.methods (+ the doc fixes from D7).

Sequencing and implementation plan (each slice lands whole and loud)

Merge order: RFD 0025 (checks) → this RFD (which then applies the D6 amendment text to 0025) → Lean PR → slices. The 0025 cross-links in this RFD and §12 resolve when 0025 lands.

• Slice 0 — real trait-item/impl-item parsing for trait impls (kills eat_balanced; bare impls keep §5.4 parsing), scoped Self, supertrait token <: → : (parse error + fix-it for <:; STATUS corrected), OE1326 gating of every not-yet-landed member form, OE0675.
• Slice 1 — rule plane end-to-end: elaboration (Self substitution, guard injection, RuleDecl emission, items/methods population), qualified-path naming + qualified atoms + bare-call resolution, conformance gates OE0670–OE0674, coverage gate OE1327 (full-coverage form; the partial-coverage guard escape activates in slice 2 with implements), trait-aware OE0223/OE0204. Keystones: Gustavo’s program verbatim; multi-impl union; NAF over a member; recursion through a member; cross-module impl; the OE0673 counter-examples (comparable targets; declared-common-descendant).
• Slice 2 — TraitRef, $implements, implements in both planes, partial-coverage guard rule, the 0025-D1 amendment in force (reflective-sorted classifier), examples/trait_contracts/ (corpus-pinned, including a #[static] conformance check).
• Slice 3 — invocation plane: fn members + static dispatch (§12.4), mutate members + receiver dispatch (ambiguous-receiver refusal) through CLI/serve/SDK, oxc-gen emission for member endpoints.

Diagnostics allocated

Renumbering note (slice 1): this RFD originally allocated OE1323 for TraitMemberUncovered, but RFD 0025 (which merged first) took OE1323–OE1325 for its check-diagnostic payload codes (MalformedCheckDiagnostic / CheckCodeNamespace / CheckMessageArgUnbound); the coverage gate ships as OE1327.

Amendment (2026-06-11) — check members may pin their severity (issue #230)

The final-validation audit (aa7a7d0e) probed two impls of one check member declaring divergent severities: Limited::OverLimit as Error on Truck (mutations rejected) and Warning on Crane (mutations pass). D5.2 compares plane/arity/param-types/return only, so the trait could not pin the blocking semantics of its own obligation. Decided (issue #230, option a): a trait-side check member signature MAY pin its severity with the payload-arrow suffix, mirroring the check payload form —

pub trait Limited {
    check OverLimit(Self) => Severity::Error;
}

Only the severity is pinnable — code: and message: stay per-impl (a full Diagnostic { … } payload at the trait side is refused, OE1323). Pinning is optional; an unpinned member keeps the per-impl freedom above (documented status quo, not an error). Semantics when pinned:

• An impl’s member-check payload may omit severity: — it inherits the pin (the ergonomic point). OE1323’s “all three fields required” relaxes to: code: + message: required, severity: required unless trait-pinned.
• Restating the same severity: legal (harmless).
• Stating a different severity: OE0676 ImplMemberSeverityDiverges at ox check/ox build (conformance pass, collect-all), naming the trait, the member, the pin, and the divergent severity. Rationale: a contract whose blocking behavior varies by implementor is a weak contract.
• #[observe] on an impl member whose pinned severity is Error remains legal (observe is a discharge-mode opt-out, not a severity change — RFD 0025 D3).

Wire: TraitMemberSig gains severity: Option<DiagnosticSeverity> (additive, serde-default; always None for non-check members). Lean: Argon.Substrate.Trait.TraitMemberSig.severity, with the conformance gate Argon.TypeSystem.Conformance.SeverityPinned joining the Conformant conjunction (the OE0671 model comparison becomes severity-blind SigShapeEq; severityPinned_invariant states the implementor-invariance headline).

Non-decisions (tracked, out of scope)

• Bounded generics / conditional impls / default member bodies / return-position Self — V1 (OE0667 stands; the Conditional.lean theory is ready for it; return-position Self also waits on union types, #184).
• Per-standpoint impls (vault open question; impls are standpoint-global).
• Postfix predicate sugar p.Adult() (revisit with the invocation plane if wanted).
• Modeling guidance is reference material, not normative: a classification (Adult) is a phase/iff concept; a trait is a capability/obligation contract — §12.8.