A plain verify block is warned it will flap even when no case reaches the effectful arm

[n1bor]

When a function reads a value that may come from a capability, every plain verify block on it is warned twice, on the grounds that its cases will flap. For a sum type whose effectful arm no test reaches, that is not true, and there is no way to say so short of a project-wide [[check.suppress]].

Repro

type Bag
    Memory(Map<String, String>)
    Database(Infra.Kv.Handle)

fn size(bag: Bag) -> Result<Int, String>
    ? "How many the bag holds, whichever arm it is."
    ! [Infra.Kv.count]
    match bag
        Bag.Memory(held) -> Result.Ok(Map.len(held))
        Bag.Database(handle) -> Infra.Kv.count(handle)

verify size
    size(Bag.Memory(Map.fromList([]))) => Result.Ok(0)
    size(Bag.Memory(Map.fromList([("a", "b")]))) => Result.Ok(1)

warning[verify-effectful]: Function 'size' has effects and a plain verify block; use `verify size trace` …
warning[check]: plain 'verify size' has no stub for generative effect(s) used by size: Infra.Kv.count.
  Each case compares against a freshly-produced value so the test will flap. …

Neither case compares against a freshly-produced value. Both select Bag.Memory, which reaches no operation. The cases are as deterministic as they were before the arm existed, and they have been passing unchanged.

Scale

This is not one function. Adding a database backend to a key-value store here put Infra.Kv.get on the read path of 25 functions, each of which has a plain verify block written against an in-memory fixture. That is 50 warnings, on a project whose only other warnings are 26 verify-coverage. The tests did not change and nothing about them became less deterministic.

What the repairs cost

• given stubs. The stub is never called, because no case selects the arm that would call it. Adding 25 of them puts a fixture in the source for a read that does not happen, which reads as though the tests check a stub when in fact they check the real in-memory backend.
• trace. There are no emissions to assert on.
• law. These are ordinary example tests.
• [[check.suppress]]. Project- or glob-wide, so it would also hide the instances that are real — in the same files.

Two ways out, either would do

1. Fold the argument. Where a case's argument is a literal constructor and the function's body is a match on it, the reachable arms are known, and an effect only on an unreachable arm cannot flap anything. This would also fix the wording, which currently asserts something false about the cases in front of it.

2. Let a block say the plain form is deliberate. The message already ends "Keep the unbound plain form only for a deliberate one-shot smoke check" — but there is no way to write down that it is deliberate. Something per-block, verify size plain or similar, would settle it at the one place that has the argument, instead of at a glob in aver.toml.

Aver 0.28.1 (a3075ff8).