`--explain-slots` is signature-only; suggest extending into match arms / W001 holes

[yansircc]

Summary

vera check --explain-slots <file> prints a slot-resolution table per function signature but not per arm body. This makes it useful for the case it documents in SKILL.md ("a function with multiple parameters of the same type") and unhelpful for the case where De Bruijn ordering bugs actually concentrate: deep inside a match arm, after a few let bindings, where the slot stack has grown by 3–5 levels and the agent is recursing into an ADT.

Concrete workflow gap

In a structural-recursion function like the substitution operator (separate companion docs issue), the position-of-error is:

App(@Term, @Term) -> {
  let @Term = ...;
  let @Term = ...;
  match @Term.1 {
    Abs(@Term) -> {
      let @Term = subst(0, @Term.???, @Term.???);   -- <-- here
      ...
    }
  }
}

By this point in the function the agent needs to know the resolved index of every named binding. --explain-slots cannot help — its output stops at the signature. The agent's options are:

1. Manually trace pattern-push-and-let across 5 levels of nesting.
2. Write the program, run it, dump intermediate state via IO.print(show(...)), binary-search the buggy index.

Option 2 is what I ended up doing. It works, but it's the workflow Vera positions itself against — agents bouncing off compiler/runtime feedback to reconstruct what they could have asked the tooling.

Suggested enhancement

Three concrete options, in increasing implementation cost:

(a) Slot tables in error context. When vera check reports E130 (unresolved slot), include the slot table at the position of the error, not just the function signature. This piggybacks on existing diagnostics infrastructure.

(b) --explain-slots-at <line>:<col>. A flag that prints the resolved slot environment at a specific source position, no error required. Lets an agent ask "what's in scope here?" before writing the expression.

(c) Slot table inside the ? typed-hole warning. W001 already lists "Available bindings". Extending it to print each binding's resolved @T.n would turn typed holes into the canonical "what slots can I use right now" probe — and SKILL.md already markets typed holes as the cheap way to figure out shape.

(c) is probably the highest leverage per LOC: holes already exist, the W001 diagnostic already enumerates context, and typed holes are the recommended workflow for incremental construction.

Why it matters

The companion documentation issue (match-arm shadow semantics) is essentially a cascade of this missing tool — when slot semantics in match arms are under-documented, the diagnostic that would substitute for documentation (showing the actual resolved indices at each position) is also missing. Together they make the slot system a "must run experiments to understand" feature rather than a "compiler tells me what to write" feature. Closing either issue alone helps; closing both makes the slot system live up to the agent-friendly framing.

Environment

• Vera v0.0.127.

[yansircc]

Self-correction: suggestion (c) is already implemented

Re-reading SKILL.md after filing this, I confirmed that suggestion (c) — "slot table inside the ? typed-hole warning" — is already what W001 emits. I missed this when filing.

Probe (in a match arm, the position the issue claims has poor diagnostics):

private fn probe(@Int, @Term, @Term -> @Term)
  requires(true) ensures(true) effects(pure)
{
  match @Term.0 {
    Abs(@Term) -> ?,
    Var(@Int) -> ?,
    App(@Term, @Term) -> ?
  }
}

vera check output for the Abs(@Term) arm:

W001: Available bindings: @Term.0: Term; @Term.1: Term; @Term.2: Term; @Int.0: Int.

Resolved indices, full slot environment, inside a match arm. That is exactly what suggestion (c) was asking for. The W001 hint already does the job; the gap I claimed in the original issue body is wrong.

What remains valid from the issue:

• (a) — slot tables in error context (E130). Still useful: when @T.n resolves to nothing, the error currently doesn't include the slot environment. Adding it would let an agent fix the index without writing a hole and re-running. (Lower priority than I implied — typed holes cover the write-time case; this is for the read-time case where the agent receives an unresolved-slot error.)
• (b) — --explain-slots-at <line>:<col>. Still has a narrow value: probing existing code without modifying it. Holes require source edits, which an automated agent loop or a human reviewer might want to avoid. But the value is much smaller than I framed.
• (c) — slot table in W001. Already implemented. Withdraw this part of the suggestion.

Net: the tooling gap is narrower than the original issue body claims. I should have run a hole probe before filing. The "slot system has no diagnostic in match arms" framing is wrong; it has typed holes. Apologies for the noise.

The companion documentation issue (#557) is also affected — its "agent must run experimental program" framing was incorrect for the same reason. I've added a self-correction there too.

[aallan]

Cross-reference: option (c) here — enumerating each binding's resolved @T.n inside the W001 typed-hole warning — overlaps with planned work in #222 (LSP server). The #222 implementation plan's Phase D delivers typed-hole completion (built on _check_hole, the #226 typed-holes machinery, which already computes the in-scope bindings) plus slot resolution via resolve_slot / slot_table — the same in-scope-@T.n context this issue asks to surface.

Options (a) (slot table in the E130 error context) and (b) (--explain-slots-at <line>:<col>) are CLI-side and independent of the LSP, so they can land separately without waiting on #222.

[aallan]

Scope record from #1262's review: that PR implements option (a) — E130's fix text gains the in-scope binding table — and its review verified the implementation against a 2,080-site corpus differential (zero violations) and twelve scope shapes against the W001 surface (zero disagreements). This issue stays open for option (b) (--explain-slots-at <line>:<col>), which the ROADMAP row now names; the PR footer reads Refs #558 accordingly. Option (c) remains withdrawn per the earlier discussion here, though this issue's title still names it — retitle when (b) lands or sooner.