result is checked wherever a clause writes it

[onatozmenn]

I went looking for the machinery that would settle transfer's two remaining ensures clauses, needed the definition result binds to, found two copies of that lookup, and found that one of them was wrong.

The hole

The type checker's copy matched expressions with a wildcard. Everything that fell through it left result with no type, an unknown type agrees with everything, and the clause went through in silence:

fn twice(n: Int) -> Int
  ensures
    ok  => result == "text",                    // DEED4001
{ n + n }

fn twice(n: Int) -> Int
  ensures
    ok  => use_it(|x: Int| result == "text"),   // accepted, silently
{ n + n }

Both return Int. The second is caught by the property runner instead, as DEED6003, "twice did not keep this promise" — which sends a reader to look at the postcondition when the mistake is a type error two characters to the right. It is the class DEED6006's own note describes: either this file was not checked or the check has a hole.

The fix

The lookup moves to deed-resolve — where a question about what a name refers to belongs — and is written on deed_ast::children, which matches without a wildcard, so a new kind of expression is a build error rather than a clause that quietly stops being checked.

The interpreter had already been fixed for exactly this once, in the change that gave children its no-wildcard match. The checker's copy predates it and nobody had a reason to look at both. That is what having two of them cost; there is one now.

Held by

result_is_checked_wherever_in_a_clause_it_is_written and a_clause_that_reads_result_correctly_is_accepted_in_every_shape: six shapes the wildcard swallowed — a closure, a list, a branch, a match arm, a block, a walk — in both directions, so the first cannot pass on a checker that rejects all six for a reason of its own.

Break-verified by declining to descend into a closure again: that fails both new tests and the two interpreter tests from the earlier fix, which is the evidence the lookup is now genuinely shared.

Nothing in examples/ or std/ relied on the hole; no obligation moves.

While here

The header of checking.rs opened by counting its own tests, said ninety-one, and there are a hundred and thirty-seven. It no longer quotes a total. The claim worth making about that file is the one underneath it — that no test there settles for asserting that something failed — and that one does not depend on how many tests there are.