A field keeps what its type said

[onatozmenn]

A parameter of type Positive was already known to be positive. A field
declared Positive was not, and the two say the same thing.

record Held { by: Positive }

fn needs(n: Positive) -> Int where n > 0, { n }

fn through(h: Held) -> Int { needs(h.by) }   // was Guarded, is Proven

The value has no name at that call for anything to have narrowed, and no
contract answered for it, so the only thing that knew anything was the type the
record was declared with — and nothing asked it. facts.rs said so itself:

Int.max is the number […] Every other field read is a value nothing here
knows.

Measured first

Where a refinement stops travelling, found by walking it rather than guessed:

written as	tier
needs(b) where b: Positive	proven
needs(h.by) where by: Positive	guarded ← this
needs(b) where b: NonZero	guarded ← something else

Two separate gaps, and only the first is closed here.

The second is value != 0, which admits everything but one number: two
intervals, not one, and Facts keeps ranges. That is a limit of what a fact
is, not of fields, and it is one of the two things still stopping std/ratio
from proving simplified's bottom != 0 at its call sites — the other being
the product of two numbers, which no interval bounds. Both are stated in the
changelog rather than left to be rediscovered.

The change

facts::Env gains one question: what does this expression's declared type
admit. The checker answers from its type table, because the fact machinery has
none, and answers Range::ANY when the type says nothing. Reading a
refinement's own predicate stays blind about fields, or a predicate mentioning
one would come straight back for the type being read.

Honest about what it buys

No obligation in the corpus moves. The records there are declared with
plain Int, so nothing there was losing anything. What moved is that the
compiler stopped throwing away something it already had, and the corpus numbers
(167 / 11 / 23) are unchanged on purpose rather than by accident.

Break-verified

CAUGHT     a field read stops asking what its type admits
SURVIVED   the type table answers for a type that is not refined

The survivor was not a missing test. A type that is not refined already answers
Range::ANY, so the guard asking whether it was refined bought nothing — dead
code, and it and the Option around it are gone.

The first run of that script reported both cases survived, and was wrong
both times: the edit never applied, and a check that cannot see its own
mutation is worse than no check. It verifies the text changed and that the run
produced a result before reading either.

Checks

cargo fmt, clippy -D warnings, nextest --profile ci (2469 passed, 4
skipped), cargo test --doc --workspace.