Carry what a type states across a basic block boundary

[coord-e]

Fixes #201.

Root cause

A block that inherits its precondition gets two things and no more: the target's parameters, typed from their MIR types alone, and a formula capturing what the predecessor's env says about each parameter's value.

PrecondCapture is where the second part is assembled, and it only ever reads a value:

fn push(&mut self, target: ..., var_ty: PlaceType) {
    self.body.push_conj(var_ty.formula...);            // the formula
    self.target_equations.push((target, var_ty.term...)); // the term
    // var_ty.ty is not read
}

and push_env_state folds in rty.refinement — the outer refinement of { T | phi } — leaving T alone. So everything a type states by itself is dropped at the boundary and rebuilt unrefined from MIR: the refinements nested inside it, and the specification a function type spells out.

A fn-pointer value is where this becomes visible, because a function type has nowhere else to keep its specification. type_call reads the pointer through operand_type(func).ty, gets an unrefined (..) -> .., and relate_fn_sub_type relates the call against true, leaving the result unconstrained.

Before, for let f: fn(i64) -> i64 = add1; let a = f(0); let b = f(a);:

register_basic_block_def bb=bb1 rty=(_0: (), _1: (int) → int, _2: int) → () has_precondition=false

fn_sub_type got=({ int | p0 ν }) → { int | p1 ν $0 }   expected=({ int | ν = 0 }) → { int | p6 ν }     ; bb0
fn_sub_type got=(int) → int                            expected=({ int | ν = _2 }) → { int | p7 ν _2 }  ; bb1

Trigger

The trigger is the block, not the number of calls: a call is a terminator, so the first call in a body sits in the reify cast's own block and is typed precisely, while every later one does not. A single call behind a branch reproduces it just as well.

It is not limited to ReifyFnPointer locals, nor to the root of a type. A fn-pointer parameter hits the same path once it is called from a later block, and so does a fn pointer nested in a tuple.

Change

install_inherited_bb_ty already materializes a goto target's type from the predecessor's env, so it now hands the env's types over there too, alongside the precondition it was already capturing.

A type in the env is closed: a refinement nested in one constrains the value at its own position and names nothing from the env. So the type transfers as it stands, with no substitution — assert_closed states that invariant where it is relied on. The sort assertion beside it holds the env's view and the MIR-built parameter to the same shape.

Blocks that need their own precondition are untouched. Those get template types and relate the two sides at the goto, and that relation — being structural — already carried all of this, nested positions included.

Why not relate the types at the goto here too

Because on this path there is nothing to relate against:

if !needs_own_precondition(&self.body, bb) {
    self.install_inherited_bb_ty(bb, outer_fn_param_vars);
    return;                       // <- no relation happens on this path
}

The target's type comes from TypeBuilder::build_basic_block, which registers no templates (its FakeRegistry panics if asked to). With no predicate variables in the expected type, a subtyping relation yields true ⟹ true, and the block body goes on reading its parameters from that same type.

Sending these blocks down the predicate-variable path instead was tried and is not a one-line change: it makes pass/option_unwrap_or_else and fail/option_unwrap_or_else abort in type_goto, where assert_closed meets a parameter type that is not closed, and it pushes pass/closure_receiver_mut_model past a 150s solver timeout. Unifying the two paths looks worthwhile but wants that invariant sorted out first.

Testing

• tests/ui/{pass,fail}/fn_ptr_call_twice.rs, fn_ptr_call_in_branch.rs, fn_ptr_param_call_twice.rs, and fn_ptr_in_tuple_call_twice.rs added. Each fail one is the pass one with the property broken as narrowly as possible. The last pins the nested case, which a version of this change that looked only at the root of a type did not fix.
• All three reproducers from the issue verify as safe, and every row of the issue's behavior matrix matches its Expected column.
• Soundness spot-checks still report Unsat: b == 3 and b == 1 on the two-call program, x == 3 on the &mut one, the branch variant, the two-target variant, and a fn pointer chosen by a branch (if c { add1 } else { add2 }).
• cargo test with the PCSat tests filtered out: 284 passed, 0 failed, plus 3 unit tests and 2 doc-tests.
• The 32 PCSat tests were run directly, sequentially, on this branch and on main at cd33fbf, with identical verdicts: 31 as expected on both, and fail/option_map.rs undecided on both at a 150s solver timeout.
• The closedness assert_closed relies on was measured before relying on it: instrumented to report any variable occurring in an env type at a goto, then run over all 316 test files. No occurrences.
• cargo fmt --all -- --check and cargo clippy -- -D warnings are clean.

Two things found while testing, neither addressed here:

• A pre-existing ICE, filed as Panic: a null-sorted value (fn(..) pointer, &str) stored in an aggregate that also has a non-singleton field is filtered out of Env::dependencies, aborting with unbound var or no entry found for key #217: a null-sorted value (fn(..) pointer or &str) stored in an aggregate that also has a non-singleton field aborts in constraint construction. It reproduces identically on main. That is why fn_ptr_in_tuple_call_twice uses a one-element tuple.
• The emitted SMT-LIB2 is not reproducible across runs — the same binary on the same input emits the same clauses with bound variables permuted, so THRUST_OUTPUT_DIR dumps cannot be diffed to compare two builds. Worth a separate issue if determinism there is wanted.

Since the fix is not specific to function pointers, #201's framing is narrower than the defect. Happy to retitle it, or to leave it as the fn-pointer symptom and open a separate issue for the general loss — whichever you prefer.