[nicolas-abril]

Fixes #1186.

Cause

In root_cols in bend2/safe.ts, a ~ parameter whose type has finitely many values (a Quant, or a datatype whose constructors have no fields) makes its def go out once per value. A datatype with no constructors passed that test vacuously, so the def went out zero times. It was never emitted and never listed as out of scope, and --verdict printed ALL PROOFS CHECK for a def the kernel never saw.

Fix

An empty type no longer counts as finite (adt.c.length > 0). It takes the opaque constant k~p that any other type's specialized parameter takes. This follows the issue's alternative rather than marking the def out of scope, as suggested in the discussion:

• A body that never names the parameter (the issue's repro) now reaches the kernel: skipped.qv : ∀x0 : Nat -> Nat = λx0 => x0, and the verdict passes.
• A body that names it (e.g. absurd(v)) is out of scope, because the constant has no model. --verdict fails with uses: no model for uses~v. On main this case also passed silently.

Checks

• tests/check/spec_empty_param.bend (new) is the issue's repro. On main skip is missing from the .bendtt; here it goes out and checks.
• --verdict on every test with a ~ parameter (73 files) gives identical output on main and on this branch.
• bun gates/repo.ts passes. The cluster gates (gates/test.ts, gates/safe.ts) weren't run.

🤖 Generated with Claude Code

[nicolas-abril]

Closing: this isn't the right fix. A ~ def means the set of its instances, one per closed argument; with an empty type there are none, so main's zero roots were correct, and emitting the body at an opaque constant with no model makes a vacuous def that names v (e.g. absurd(v)) fail --verdict.

The real gap is that --verdict trusts root_cols' enumeration to cover the law. The follow-up will emit, for a root with a finite ~ parameter, the law's own universal statement as a λ-match dispatching to its instances, so the kernel checks the coverage (and for an empty type checks λ{} directly).