Vera version: vera 0.0.138
Origin: Friction surfaced while writing terminal Tetris on Vera 0.0.138.

Problem

State (in the Tetris implementation) had two Int fields (x and y). Match arms looked like:

match @State.0 {
  MkState(@Array<Int>, @Kind, @Rot, @Int, @Int, @Nat) -> {
    -- which @Int is x and which is y?
  }
}

Convention says rightmost is @Int.0, so @Int.0 = y and @Int.1 = x. Correct, and the same rule as parameter ordering, so it's consistent. But the field order in the data declaration (board, kind, rot, x, y, lines) is left-to-right, while slot indexing is right-to-left for same-typed fields. The Tetris author wrote a comment under every MkState match arm to remind themselves which slot was which.

Proposed (with sharp guardrail — see "Design constraints" below)

Optional field names in data declarations:

data State {
  MkState(
    board: Array<Int>,
    kind: Kind,
    rot: Rot,
    x: Int,
    y: Int,
    lines: Nat
  )
}

Match arms continue to use positional / De Bruijn slot references — field names are never bindable in patterns:

match @State.0 {
  MkState(@Array<Int>, @Kind, @Rot, @Int, @Int, @Nat) -> ...
}

The compiler uses the field names exclusively for:

• vera check --explain-slots output: "In MkState, @Int.0 = y (rightmost), @Int.1 = x (next)".
• Type-error messages mentioning MkState: "expected MkState(board: Array<Int>, kind: Kind, ...) — got 3 fields".
• vera ast --json constructor metadata.

Existing data declarations without field names continue to work unchanged — strict superset.

Design anchor

The principle at stake is DESIGN.md principle 4. Structural references over names:

Bindings referenced by type and positional index (@T.n), not arbitrary names. See DE_BRUIJN.md.

This is what makes vera context (#523) able to produce denser-per-byte project exports than identifier-based languages, what eliminates naming-coherence errors, and what makes slot resolution locally determinable from types alone. Any feature that lets writers bind by name (rather than by position+type) erodes that property.

Field names in data declarations sit on the advisory side of the principle — they are documentation that the compiler echoes back in diagnostics, not a parallel binding mechanism. But that's only true if the guardrails below hold; otherwise this proposal slides into territory the principle prohibits.

Design constraints (load-bearing)

This proposal is acceptable if and only if these guardrails hold:

1. Names are never bindable in patterns. match @State.0 { MkState(board: b, ...) -> ... } must remain a parse error. Once names are bindable, Vera has named locals — and named locals are exactly what De Bruijn slot indexing exists to avoid (DESIGN.md principle 4). The slot model is a property of the language, not of the syntax convenience.
2. Names are non-load-bearing for semantics. Renaming a field (x → xpos) must be a no-op except in --explain-slots and error-message output. No verifier change, no codegen change, no type-check change.
3. Names are advisory, not enforced. If a writer puts misleading names (x: Int when the field is actually used as y everywhere), the compiler does not — and must not — warn. Names are documentation and the writer is responsible for keeping them honest. (Enforcement would re-introduce a name-coherence error class that DESIGN.md principle 4 explicitly eliminates.)
4. Compatible with anonymous form. MkState(Array<Int>, Kind, Rot, Int, Int, Nat) (today's syntax) and MkState(board: Array<Int>, kind: Kind, ...) must coexist within the same program; mixing within one declaration (MkState(Array<Int>, kind: Kind, ...)) is a parse error.

If any of these guardrails would have to be relaxed during implementation, the proposal should be re-rejected — at that point it has crossed into "named bindings", which is a distinct (and design-incompatible) feature.

Why this is acceptable while #617 (anonymous tuples) is not

Tuples (#617, closed) proposed let (x, y) = ... destructuring, which is a pattern-binding form — names that shadow slot positions in a fresh scope. This proposal is the opposite: names that are advisory only and never enter the scope of pattern-matching or value-extraction. The slot model stays load-bearing for semantics (DESIGN.md principle 4 preserved); field names sit alongside it as documentation.

Origin

Friction document from terminal Tetris experiment, with design-anchor and constraint sections added after review.