Summary

spec/03-slot-references.md Example 9 is the only place that describes what happens to the scrutinee's slot when a match arm pattern binds a value of the same type:

@List<T>.0 = the tail (innermost List<T>, from the pattern) — note this shadows the function parameter

"Shadow" is left undefined. Two readings are equally consistent with that sentence:

• (A) The pattern binding replaces the scrutinee at @T.0; the original is gone.
• (B) The pattern binding pushes onto the slot stack; the original is still accessible at @T.1 (@T.2, etc., when more bindings are pushed) — the same shift-on-shadow rule that let uses.

The compiler implements (B). This is not derivable from the documentation. Function-signature --explain-slots output does not extend into match arms, so there is no diagnostic that lets an agent confirm the rule short of running an experimental program and reading the output.

Worked example

The bug below type-checked cleanly, verified with 27 Tier-1 contracts, ran without traps, and produced wrong output. The fix is a one-character index change. It is the difference between reading the spec as (A) vs (B).

Capture-avoiding substitution under De Bruijn indices:

-- subst(depth, replacement, target):
--   @Int.0  = depth
--   @Term.0 = target (rightmost)
--   @Term.1 = replacement (leftmost)
private fn subst(@Int, @Term, @Term -> @Term)
  requires(true) ensures(true)
  decreases(@Term.0)
  effects(pure)
{
  match @Term.0 {
    Var(@Int) ->
      if @Int.0 == @Int.1 then { @Term.1 }      -- (A) and (B) agree here
      else if @Int.0 > @Int.1 then { Var(@Int.0 - 1) }
      else { Var(@Int.0) },

    -- pattern pushes inner body. Under reading (A): @Term.0 = body, @Term.1 = replacement.
    --                            Under reading (B): @Term.0 = body, @Term.1 = target,
    --                                               @Term.2 = replacement.
    Abs(@Term) ->
      Abs(subst(@Int.0 + 1, shift(1, 0, @Term.???), @Term.0)),

    -- pattern pushes (a, b). Under (A): @Term.0=arg, @Term.1=fn, @Term.2=replacement.
    --                       Under (B): @Term.0=arg, @Term.1=fn, @Term.2=target,
    --                                  @Term.3=replacement.
    App(@Term, @Term) ->
      App(subst(@Int.0, @Term.???, @Term.1), subst(@Int.0, @Term.???, @Term.0))
  }
}

The compiler accepts either index in the ??? positions because both are valid @Term references in scope. Only behaviour at runtime distinguishes them. The correct indices are @Term.2 (Abs) and @Term.3 (App), confirming reading (B). Writing @Term.1 and @Term.2 produces a structurally well-typed but semantically wrong substitution that creates open terms (free Var(2) inside a 2-binder context for what should be a closed result).

Why it matters

This is not a corner case — it's the core mechanic of Vera's slot system. Every non-trivial match arm that mentions a previously-bound value of the matched type is affected. The spec's worked Example 9 only shows accessing the new binding, not the shadowed one, so the question "how do I reach the original now?" has no answer in the docs.

Issue #519 item 7 acknowledges the broader gap ("the slot-shift-on-shadowing rule as a principle, not an inference from examples"). This issue scopes that to the specific match-arm case, with a worked example agents are likely to hit (any structural recursion over an ADT with a parameter that needs to thread through binders — substitution, evaluation, type checking, tree rewrites).

Suggested fix

In spec/03-slot-references.md Section "Pattern Matching", add the rule explicitly with a short table:

match @T.0 { K(@T) -> body }
                ↑
                pushes a new @T at index 0; the original (now shadowed)
                @T from the scrutinee's binding remains accessible at @T.1.
                Patterns with k same-type fields push k bindings; the original
                lives at @T.k inside the arm.

A second, smaller fix: have vera check --explain-slots print one slot table per match arm (or per let block) rather than only at function signatures. The signature-level snapshot is the right first tool but is least useful at the position where mistakes actually happen. (Tracked separately as a tooling enhancement issue.)

Environment

• Vera v0.0.127, observed while writing a 250-line λ-calculus interpreter; the wrong-index version produced runtime output that was almost correct (term shape preserved, indices off by one) — the kind of bug that survives smoke tests and surfaces in the next layer of the program.