Refinement: iff (defined) vs where (primitive)

Area: Refinement & types Teaches: the two ways a refined concept gets its members — iff derives membership from a predicate, where asserts membership and treats the predicate as an enforced invariant. This is the most consequential distinction in Argon’s type layer. Prerequisites: concepts and <: specialization. Run: ox build examples/primitive_refinement && ox run-scenario examples/primitive_refinement

Two refined concepts sit over one Person population, and the keyword decides who is a member:

// Defined: anyone satisfying the predicate is automatically a member.
pub type Adult   <: Person iff   { self.age >= 18 };

// Primitive: membership is granted by an authority; the predicate is a
// necessary invariant on members, checked at the grant — never a classifier.
pub type Cleared <: Person where { self.clearance_score >= 50 };

• iff (Adult) — membership is derived. You never assert it; the reasoner classifies every Person whose age >= 18. Asserting it directly (insert iof(p, Adult)) is refused with OE0211.
• where (Cleared) — membership is asserted. A clearance is conferred by an act (grant_clearance → insert iof(p, Cleared)); the predicate only guards that act. A qualifying score is necessary, not sufficient.

The teaching contrast

Run it and compare the two extents. After the scenario seeds four people:

query clearance::adults:  4 row(s)   — Adult (iff):   everyone 18+, auto-classified
query clearance::cleared: 2 row(s)   — Cleared (where): only the two who were granted

The decisive case is dave: he has clearance_score = 70 (≥ 50) but was never granted, so he is not Cleared. Under iff he’d be classified automatically; under where membership is conferred, never inferred.

Honest caveats (what runs today)

• Granting clearance below the invariant is rejected with OE0668 (the where predicate is enforced at the grant). Inserting an iff membership directly is refused with OE0211.
• Refinement membership is evaluated by the reasoner at query time against each individual’s fields, so the extents above reflect the seeded age/score values.

This example is compiled and run in CI; its iff/where runtime behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so it can’t drift from the language.