Problem
The spec describes invariant(...) clauses on data declarations (§2.6, §6.2.3) as a way to express constraints on constructor field values that are verified at every construction site. The current reference implementation does not support these — every documented form fails with [E130] no <DataName> bindings in scope because the slot environment for the invariant predicate is not wired up.
The previous tracking issue #560 was about the broken spec/SKILL examples that produced E130 — that was closed as COMPLETED on 2026-05-11 (presumably by removing/rewriting the failing examples). But the underlying feature remains NYI, and the spec + SKILL.md still describe it as a planned feature with stale citations to #560.
Current state
All four are now dangling — #560 is closed without an implementation.
Acceptance criteria
data X { Mk(@Int) } invariant(@Int.0 > 0) parses, type-checks, and verifies — the predicate is discharged at every Mk(...) call site- The slot environment for the invariant predicate has access to the bound field name (i.e., the
@Int.0 in Mk(@Int)'s position)
- A counterexample is reported via E130 only when the predicate is genuinely violated, not because the slot environment is missing
- Documentation in
spec/02-types.md §2.6, spec/06-contracts.md §6.2.3, and SKILL.md is updated to drop the NYI status box and point at concrete working examples
- Limitations-table entry in
spec/06-contracts.md is removed
- New conformance test in
tests/conformance/ covering: positive verification, negative verification with counterexample, refinement-type interaction, multiple invariant clauses
Why this isn't auto-injection
invariant(...) on data is different from auto-injected primitive obligations (tracked in #680). Auto-injection is "the compiler synthesises obligations for a / b, arr[i] etc."; invariant() is "the programmer declares a constraint on a custom data type". The two are independent features.
Dependency
May benefit from #427 (Tier 2 verification with assert/lemma hints) once that lands, but doesn't depend on it — the invariant predicate is typically Tier 1 (decidable arithmetic on bound fields).
Provenance
Surfaced during the 2026-05-19 v0.0.156 release doc sweep when noticing that 4 references to #560 in SKILL.md + spec/* were dangling against a closed issue. Filing as the successor to #560 with explicit acceptance criteria so the implementation work has a clear target.
Problem
The spec describes
invariant(...)clauses ondatadeclarations (§2.6, §6.2.3) as a way to express constraints on constructor field values that are verified at every construction site. The current reference implementation does not support these — every documented form fails with[E130] no <DataName> bindings in scopebecause the slot environment for the invariant predicate is not wired up.The previous tracking issue #560 was about the broken spec/SKILL examples that produced E130 — that was closed as COMPLETED on 2026-05-11 (presumably by removing/rewriting the failing examples). But the underlying feature remains NYI, and the spec + SKILL.md still describe it as a planned feature with stale citations to #560.
Current state
spec/02-types.md§2.6 has a "Status: Not yet implemented" box citingdata invariant(...)syntax has no working form at v0.0.127; spec/SKILL examples all fail E130 #560spec/06-contracts.md§6.2.3 has the same box citingdata invariant(...)syntax has no working form at v0.0.127; spec/SKILL examples all fail E130 #560spec/06-contracts.mdlimitations table has adata invariant(...)entry citingdata invariant(...)syntax has no working form at v0.0.127; spec/SKILL examples all fail E130 #560SKILL.md("With an invariant (NYI — seedata invariant(...)syntax has no working form at v0.0.127; spec/SKILL examples all fail E130 #560...)") citesdata invariant(...)syntax has no working form at v0.0.127; spec/SKILL examples all fail E130 #560All four are now dangling — #560 is closed without an implementation.
Acceptance criteria
data X { Mk(@Int) } invariant(@Int.0 > 0)parses, type-checks, and verifies — the predicate is discharged at everyMk(...)call site@Int.0inMk(@Int)'s position)spec/02-types.md§2.6,spec/06-contracts.md§6.2.3, andSKILL.mdis updated to drop the NYI status box and point at concrete working examplesspec/06-contracts.mdis removedtests/conformance/covering: positive verification, negative verification with counterexample, refinement-type interaction, multiple invariant clausesWhy this isn't auto-injection
invariant(...)on data is different from auto-injected primitive obligations (tracked in #680). Auto-injection is "the compiler synthesises obligations fora / b,arr[i]etc."; invariant() is "the programmer declares a constraint on a custom data type". The two are independent features.Dependency
May benefit from #427 (Tier 2 verification with assert/lemma hints) once that lands, but doesn't depend on it — the invariant predicate is typically Tier 1 (decidable arithmetic on bound fields).
Provenance
Surfaced during the 2026-05-19 v0.0.156 release doc sweep when noticing that 4 references to #560 in SKILL.md + spec/* were dangling against a closed issue. Filing as the successor to #560 with explicit acceptance criteria so the implementation work has a clear target.