RFD 0031 — The relation-constraint plane + meta-property completion

• State: committed
• Opened: 2026-06-12
• Decides: how a vocabulary author expresses and the elaborator enforces the relation-level compile-time constraints an ontology needs — completing the meta-property and reflection surface the book promised but left unbuilt. Concretely: (1) metarel endpoint-metatype verification (§4.3 “the elaborator verifies the relation’s endpoint metatypes match the metarel’s positions” — #311); (2) relation-signature reflection — $rel/$arm catalog atoms so a package-shipped check can quantify over declared relations, their classifying metarel, and endpoint types (#312); (3) per-target axis overrides keyed on a vocabulary’s own axis name (RFD 0027 D2 — R-M9); (4) reflection-intrinsic category errors on struct/enum carriers (§4.4.2 — R-M10); (5) the metaxis typed-axis where refinement parse (§4.1 — R-M11); and (6) relation bracket-cardinality enforcement (§4.3/§5 — #310). Built as the Wave-C arc4-metaproperty work of the v0.2.1 program. The macro atom is explicitly out of scope (its own later design discussion). Builds on RFD 0027 (the meta-property plane, whose D2 per-target plane and D4 reflection surface this completes) and RFD 0023 (reflective TypeRef). Relates to Meta-calculus and Constructs.

This RFD records, as built, the relation-constraint surface the readiness register (.local/research/readiness-2026-06-12) named as the vocabulary-authoring blocker half of the production bar: a vocabulary team (Gustavo/Tiago, building ArgUFO) cannot write the relation-level compile-time constraints their ontology needs — “an ability must inhere via an aspect, not a kind” is unenforceable, and there is no reflection over relations to write such a constraint as a package-shipped check. The substrate the meta-property plane (RFD 0027) built for types is here extended to relations, plus the residual meta-property gaps (R-M9/M10/M11) closed.

Question

RFD 0027 built the meta-property plane for the type tier: metaxes, metatypes, abstract/fixed modifiers, the $meta/$iof/$axis catalog relations, sort-directed meta(t).axis projection. It left the relation tier half-built and three meta-property gaps open:

1. Metarel endpoints are unverified. pub metarel mediation(mediator: relator, mediated: kind) declares position metatypes, but pub mediation Bad(a: Vehicle, b: Person) — where Vehicle is kind-sorted, not relator-sorted — was accepted clean. The §4.3 promise (“the elaborator verifies the relation’s endpoint metatypes match the metarel’s positions”) was prose only; the position metatype names were parsed and discarded (never persisted on MetarelDeclBody). This is the core ask: an ability must inhere via an aspect, not a kind, and nothing enforced it.

2. No reflection over relations. $iof/$meta/$axis/$implements reflect over types and traits; nothing reflects over relation arms. A vocabulary package could not write a check that quantifies over declared relations (their classifying metarel, their endpoint types) — so the metarel-endpoint discipline, even once enforced by the compiler, could not be extended or audited by package-shipped rules.

3. Per-target axis overrides have no surface. RFD 0027 D2 specified per-target MetaProperty assertions (“metatype-level bindings unioned with per-target assertions, per-target taking precedence”), but the only emitter was the hardcoded MLT #[order(N)] magic string. A vocabulary declaring metaxis rigidity for type { … } gave consumers no way to override rigidity on one specific concept. In-body { rigidity::semi_rigid } → OE0001; the attribute form → OE0705.

4. Reflection on struct/enum is silently clean. §4.4.2 promises a category error (“calling meta() on a struct/enum-declared value is a category error … emits a diagnostic at elaboration”). meta(p) == Point over a struct checked clean — no diagnostic existed.

5. The metaxis where-refinement does not parse as printed. §4.1’s pub metaxis weight for type = Real where _ > 0.0; → OE0001 (the typed-domain type_expr greedily consumed the trailing where as a refined-type refinement expecting { … }). Only the braced = Real where { _ > 0.0 }; parsed.

6. Relation bracket cardinalities are silently ignored. pub rel R(...) [1..1] [0..*]; parsed into a CARDINALITY token-soup node that no lowering read (#310). A documented modifier, honored nowhere.

Decisions

D1 — Metarel endpoint-metatype verification (#311)

The metarel’s position metatypes become real on the wire. MetarelDeclBody gains position_metatypes: Vec<Option<NameRef>> — one entry per declared endpoint, the resolved metatype NameRef named in that position (relator, kind, …), or None for a bare-typed position (metarel material(kind, kind) names a metatype per position; a position naming a primordial or a generic param binds None and is unconstrained). The generic stdlib pub metarel rel<E1: metatype, E2: metatype>(E1, E2) binds None at every position — it “accepts any endpoint metatypes” (§4.3), so it imposes no endpoint constraint, exactly as documented.

At relation lowering, the elaborator verifies. For a relation pub <metarel> R(a: A, b: B) classified by a metarel with position metatypes [Some(m₀), Some(m₁), …]:

• each endpoint concept A’s declared metatype is resolved (the concept’s introducing classifier, already captured by the workspace symbol sweep), and
• if the endpoint’s metatype is not the position metatype, the relation is refused with OE0631 (MetarelEndpointMetatypeMismatch), naming the position, the expected metatype, the endpoint concept, and its actual metatype.

A None position imposes no constraint. An endpoint whose type is a primordial (Int/String/…) or whose metatype cannot be resolved is not refused here (it is unconstrained or already refused by the §3.4 introducer gate) — OE0631 fires only when both the position metatype and the endpoint metatype are known and incompatible.

Elaboration path (v0). Metatypes are flat in v0 — there is no declared metatype <: graph — so the comparison is metatype short-name identity (MetarelDeclBody.position_metatypes carries the resolved NameRefs for the runtime; the elaboration-time gate compares the short names the workspace catalog resolves both endpoints to). It is still an identity comparison, not a magic string: the compiler never branches on a particular metatype/axis word (the §3.4 / RFD 0027 D6 doctrine — the compiler never branches on user vocabulary). The sub-metatype tolerance (an endpoint metatype that is a descendant of the position metatype satisfies the constraint) is reserved — it activates when metatype subtyping lands; until then the flat case is exact identity. This holds across the dependency boundary: a relation declared in a consumer package against a metarel imported from a dependency is verified against the dependency’s published position metatypes (the cross-package OE0631 path, #311).

D2 — Relation-signature reflection: $rel and $arm (#312)

Two new catalog-closed reflection relations, in the established $iof/$meta/$axis style (abstract reflection primitives, never ontology vocabulary):

• $rel(r: TypeRef, m: TypeRef) — for every declared relation r (a TypeRef value naming the relation), m is its classifying metarel. Catalog-closed: one row per declared relation.
• $arm(r: TypeRef, pos: Int, t: TypeRef) — for every declared relation r, pos is a 0-based arm position and t is the endpoint type declared at that position. One row per (relation, position).

Surface spelling mirrors the type-tier reflection sugar: rel(r, m) and arm(r, pos, t) are admitted in any rule body without a use (the rel/arm heads lower to the reserved-head predicates $rel/$arm, exactly as iof → $iof). Both are first-class and all positions may be free — enumeration is the intended use, the same justification as $implements. A package-shipped check can now quantify:

// "every endpoint of a `characterization` relation must be aspect-sorted or the bearer kind"
pub check BadCharacterization(r: TypeRef) :-
    rel(r, characterization), arm(r, 1, t), meta(t) == kind, not meta(t) == aspect
    => Diagnostic { ... };

rel here is the vocabulary’s metarel name in value position (a TypeRef), not the stdlib std::core::rel introducer — they are distinct (one is a metarel name used as a value, the other the generic introducer keyword). The reflection head spelled rel(...)/arm(...) is the abstract primitive; resolution distinguishes the value-position metarel reference from the head.

D3 — Per-target axis overrides (R-M9, RFD 0027 D2 realized)

A concept declaration may carry per-target axis assignments in its body, in the same axis::value / axis = literal spelling a metatype body uses:

pub kind Person { rigidity::semi_rigid }          // override the metatype's rigidity binding
pub kind Worker { age: Int, rigidity::semi_rigid } // mixed with field declarations

An axis::value (or axis = literal) clause in a concept body lowers to a per-target MetaProperty event (axis, target=concept, value) — the same channel MLT’s #[order(N)] already emits, now reachable from a generic, vocabulary-named surface. The clause is validated exactly like a metatype binding (axis resolves to a visible pub metaxis whose for targets include type; value in domain — OE0622/OE0623/OE0624; duplicate — OE0625). The effective $axis relation unions metatype-level bindings with these per-target assertions, per-target taking precedence (RFD 0027 D3 — functional per (target, axis), OE0629 the load-time backstop).

The compiler never reads the axis name. The override mechanism resolves the axis to its NameRef and validates against the declared domain of whatever metaxis the vocabulary declared; a string-match on rigidity (or any axis/value name) appears nowhere. A vocabulary that declares metaxis foo for type { a, b } gets per-target foo::a overrides for free, with zero compiler changes — the mechanism is axis-name-agnostic by construction.

D4 — Reflection-intrinsic category error on struct/enum (R-M10)

meta/iof/specializes/extent applied to a carrier that is a struct- or enum-declared type (language-level data, not an ontologically-classified concept) is a category error, refused at elaboration with OE0632 (ReflectionOnUnclassified) — the feature-named diagnostic §4.4.2 promised, parallel to OE1016 (Truth4OfOnStruct). The check fires when the type-position argument of a reflection intrinsic statically resolves to a struct/enum declaration; reflection over concepts (the metatype-classified tower) is unaffected.

D5 — The metaxis where-refinement parse (R-M11)

The typed-domain metaxis body parses = TypeExpr ('where' refinement)? where the refinement is a bare predicate (_ > 0.0, self > 0.0) terminated by ;, or the braced { … } form. The parser stops type_expr from greedily consuming the trailing where: the metaxis-decl rule parses the base type expression without the refined-type where-suffix, then handles where itself (either a { … } block or a bare predicate to ;). Both printed spellings now parse and the refinement lowers into the typed-domain AxisDomainBody::Typed { refinement } already on the wire.

D6 — Relation bracket-cardinality enforcement (#310)

The [lo..hi] cardinality brackets parse into a structured Cardinality { lo, hi } (lo: u32, hi: Option<u32> — * = None) per arm, persisted on RelationDeclBody.

• Max-caps are CWA-checkable and enforced at the write path: an insert/update that would make an entity participate in more than hi tuples of relation R in the constrained position is refused with OE1014 family (the closed-world cardinality gate), feature-named OE1341 (RelationCardinalityExceeded). Max-caps are checkable at ox check/build only when statically decidable; the live enforcement is at write/serve.
• Min-cardinalities need the evaluation channel. A [1..1] lower bound is an existence requirement that, under the closed-world default, would refuse an entity that does not (yet) participate — but staged construction (classify now, relate later) makes a build-time refusal wrong, and the field-access-time / evaluation-channel emitter that would surface staged incompleteness is RFD 0007’s design and not built in v0 (the same disposition as OE0207’s staged-construction note). Decision: enforce max-caps loudly; min-cards are recognized, validated for well-formedness (lo <= hi), persisted, and refused-or-deferred explicitly — a non-zero lo that cannot be statically discharged emits the reserved OW1342 (RelationMinCardinalityDeferred, a build-time note-severity diagnostic naming the unenforced bound) rather than silently accepting it as enforced. No silent-ignore: the bracket is honored (max) or explicitly flagged-as-deferred (min). Full min-card-under-OWA enforcement is the recorded follow-on, gated on RFD 0007’s evaluation channel.

This composes with D1: the metarel constraint plane (endpoint metatypes) and the cardinality plane together are the relation-level compile-time constraint surface.

D7 — mode un-reserved; dead-reservation sweep (#309)

mode is removed from the lexer keyword list — it lexes as IDENT, so pub metatype mode { … } (the most important UFO vocabulary word) is admitted. The documented graph-traversal mode-spec ::= 'mode' ('walk' | …) surface (§7.4) is unbuilt (allowlisted OE0001, arc6-debt); when it lands it recognizes mode contextually in the role-step position (lex-as-IDENT, match-by-text), the same discipline type/rel already use — no reserved keyword needed. The sweep also un-reserves ordered, a vestigial reservation with zero grammar consumers and no documented surface (order — distinct keyword — backs order by). The other zero-consumer reserved words (walk/trail/acyclic/simple/shortest/union/with/upsert/detach/…) stay reserved: each backs a documented future surface that refuses feature-named-or-OE0001 by design (the coverage allowlist’s burn-down class), so un-reserving them would let a modeler shadow a planned keyword.

D8 — Teaching hints (#313)

Three diagnostic-message improvements, no new codes:

• A comma-separated refinement constraint list (where { a > 0, b < 10 }) gets a directed hint: “constraints combine with && — write a > 0 && b < 10” (one spelling; comma is not sugar).
• OE0660 (bare field name in a refinement) gains “did you mean self.<field>?”.
• The non-existent pub kind X : T = { field: value } declaration shape gets a directed hint naming the two real alternatives (pub kind X : T { field: … } for a typed instance, or a separate pub fact/construction).

Diagnostics inventory

Out of scope

• The macro atom — its own later design discussion.
• Multi-valued axes — RFD 0027’s recorded non-decision stands.
• Full min-cardinality-under-OWA enforcement — gated on RFD 0007’s evaluation channel; D6 enforces max-caps and explicitly flags deferred min-cards.
• Cross-module relation-subsumption parent resolution — unchanged from RFD 0005.

Wire / drift-gate note

D1 (position_metatypes) and D6 (Cardinality) add fields to MetarelDeclBody / RelationDeclBody. These are storage-mirror shapes; the @[language_interface] drift gate covers the syntax inductives, not the storage bodies (the storage mirror is a documented known-limitation of the gate, RFD 0027 D9 §note). The Lean storage mirrors gain the fields in the catch-up; the Rust wire is canonical for these runtime-facing bodies.