Check constraints: diagnostics on two moments

Area: Constraints & checks Teaches: check rules — constraint/integrity rules that emit a Diagnostic instead of populating an IDB. Where a check discharges is decided by its vocabulary: a catalog-level (TypeRef-sorted) check fires at build, an instance-level check is a runtime delta guard, and one whose EDB is partly declared in source fires at both moments. Prerequisites: concepts and <: specialization; refinement (iff/where) helps. Run: ox build examples/check_constraints && ox run-scenario examples/check_constraints

A check is not a derive. It has no head extent; it computes a condition and, when the condition holds, raises a coded Diagnostic. Argon is a constraint language, and a check is the unit of constraint. The decisive idea here is that the sort of a check’s variables tells the compiler when it can be discharged.

What to read in fleet.ar

A catalog-level check discharges at build. Every variable is TypeRef-sorted, so the condition is decidable over the declared types alone — no instances needed. #[static] makes that a contract: if the body ever drifts to instance vocabulary, the build fails with OE1322 rather than silently reclassifying to a runtime guard.

#[static]
pub check NoDeprecatedVehicles(t: TypeRef) :-
    specializes(t, Deprecated),
    t != Deprecated
    => Diagnostic {
        severity: Severity::Warning,
        code:     "Fleet::W001",
        message:  "type still specializes Deprecated — migrate it before v2",
    };

An instance-level Error check is a runtime delta guard. At runtime a mutation that creates a new violation is rejected atomically; mutations that don’t make things worse pass, and pre-existing violations never block:

pub check OverweightTruck(v: Truck) :-
    v.weight > 100
    => Diagnostic { severity: Severity::Error, code: "Fleet::E001", /* … */ };

A check whose EDB is partly declared in source fires at both moments. Truck(ghost) is a declared fact, so UnweighedTruck fires once at build over the declared facts, and again at runtime on the observe channel for any truck registered without a weighing:

pub check UnweighedTruck(v: Truck) :- v: Truck, not Weighed(v) => Diagnostic { /* W002 */ };
pub fact Truck(ghost);

Running it

ox build discharges the build-moment checks and prints two warnings, then writes the artifact (warnings pass — a firing Error check would refuse the build):

Fleet::W001  type still specializes Deprecated — migrate it before v2   [OldTruck]
Fleet::W002  truck has never been weighed   [#i3356…]
wrote examples/check_constraints/target/root.oxbin

(W002’s subject is the declared ghost truck, rendered as its opaque individual id.)

ox run-scenario registers hauler at weight 50. The OverweightTruck Error guard passes (no new violation), and the observe channel still reports the pre-existing Fleet::W002 on the never-weighed ghost:

Fleet::W002  truck has never been weighed   [#i3356…]
scenario: applied 1 mutation(s) from examples/check_constraints/demo.toml

Registering a truck with weight > 100 would instead be refused atomically with Fleet::E001.

Honest caveats (what runs today)

• ox check --codes prints only error-severity codes (it is the machine-readable feed for the coverage gates). Both checks here that fire at build are Warnings, so --codes reports ok and exits 0 — the warnings surface on plain ox build (rendered) and on the run-scenario observe channel, not in the --codes stream.
• Catalog-level discharge happens at ox check / ox build; surfacing it live in the editor via the LSP is tracked follow-on work.

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the runtime delta-guard behaviour — the under-limit registration commits and an over-limit one is refused — so the both-moments discharge can’t drift from the language.