Regression: `f () = (y <: _)` infers the refinement from f's Pure postcondition, rejecting y

[gebner]

Since #4515 (_revise_primitive_effects), the type of an equality is inferred from the refined result type of a Pure call. The other operand then has to satisfy the postcondition.

module Bug2d
assume val f : unit -> Pure int (requires True) (ensures fun r -> r > 0)
let test (y: int) : bool = f () = (y <: _)

nightly-2026-09-20 (5603331) accepts this. nightly-2026-09-21 (775ec34) and nightly-2026-09-23 (df3e072) reject it:

* Error 19 at Bug2d.fst(3,35-3,36):
  - Subtyping check failed
  - Expected type _: Prims.int{_ > 0} got type Prims.int
  - The SMT solver could not prove the query.
  - Failed to prove: y > 0
  - In context: y: Prims.int
  - See also Bug2d.fst(2,66-2,71)

(y <: _) stands in for any operand whose type is still a unification variable when the equality is checked. Before this change, ?t was solved to int. Now it is solved to r:int{r > 0}, taken from f's postcondition.

Where this shows up in practice: in Pulse, an impure spec such as pure (SizeT.v x = reveal (get ())), where get is a ghost fn returning nat, now fails with Failed to prove: FStar.SizeT.fits _. This breaks every len == arr._length precondition that PAL (C-to-Pulse) emits. As a workaround we now emit reveal #nat (...).