Summary

The invariant(...) clause on data declarations — documented in spec/02-types.md §2.4.1, spec/06-contracts.md §6.2.3, and SKILL.md line ~442 — has no working syntax at v0.0.127. Every variant I tried, including a direct copy of the spec example, fails with E130 "no bindings in scope" before verification can even attempt to check the invariant. There are zero working uses of invariant(...) in examples/ or tests/conformance/.

Direct repro of spec/06-contracts.md §6.2.3 example

private data SortedArray
  invariant(is_sorted_impl(@SortedArray.0))
{
  Mk(Array<Int>)
}

private fn is_sorted_impl(@SortedArray -> @Bool)
  requires(true) ensures(true) effects(pure)
{
  match @SortedArray.0 {
    Mk(@Array<Int>) -> array_length(@Array<Int>.0) <= 1
  }
}

$ vera verify repro.vera
[E130] Error at repro.vera, line 2, column 13:

      invariant(is_sorted_impl(@SortedArray.0))
                               ^

  Cannot resolve @SortedArray.0: no SortedArray bindings in scope.

  Slot reference @SortedArray.0 requires at least 1 binding(s) of type SortedArray.

Variants tried, all fail

The invariant body cannot reference any binding under any of the documented forms:

There appears to be no slot binding made available inside the invariant(...) body, regardless of which type name (the constructor's field type, the data type itself, the type parameter) is referenced.

Cross-doc state

• spec/02-types.md §2.4.1 ("ADT Invariants") — gives a SortedList<T> example with invariant(is_sorted(@SortedList<T>.0)).
• spec/06-contracts.md §6.2.3 ("Invariants (invariant)") — gives the SortedArray example above.
• SKILL.md (around line 442) — gives data Positive invariant(@Int.0 > 0) { MkPositive(Int) } as a worked example.
• KNOWN_ISSUES.md — does not flag invariant as broken.
• examples/ and tests/conformance/ — grep -rn "invariant(" . returns no hits across either directory.

So the language documents an ADT-invariant feature in three places, with three example shapes, none of which actually work, and the issue is not tracked anywhere I could find.

What I'd want either way

Either:

1. Fix the parser/checker so a slot reference to "the value being constructed" is in scope inside the invariant(...) body. Whichever name resolves (@T.0 for data T, or @Field.0 for the constructor's field type) should match what the docs already show.
2. Or, mark the feature as not-yet-implemented in KNOWN_ISSUES.md, remove the worked examples from spec/SKILL until it lands, and add an explicit error like E613 "invariant declarations not yet supported" rather than E130 (which makes it look like a slot bug the user can fix).

The current state — three documents claiming the feature works, three examples that don't compile, no tracked issue — is the worst combination for an agent reading the docs as authoritative.

Why it matters

ADT invariants are how Vera lets users express structural properties at the type level (SortedArray, NonEmpty<T>, Positive). Without them, every consumer of an ADT has to re-establish the structural property at every call site via requires(...), defeating the design goal. Refinement types ({ @Int | @Int.0 > 0 }) cover only built-in primitives per spec 6.2.3 — for user ADTs the invariant clause is the documented mechanism.

Environment

• Vera v0.0.127 (editable install from aallan/vera@main)
• Python 3.14.3, macOS 25.4 (arm64)