Panic verifying a generic function whose closure argument has a generic parameter type

[coord-e]

Summary

Verifying the body of a generic function that calls a closure whose argument type is a generic type parameter panics with called Option::unwrap() on a None value in rty::Instantiator::instantiate (src/rty.rs:1573).

This is independent of any specification — it reproduces on a plain higher-order function with no requires/ensures.

Reproduction

//@compile-flags: -C debug-assertions=off
fn apply<T, F: FnOnce(T) -> T>(x: T, f: F) -> T {
 f(x)
}
fn call_apply<T>(x: T) -> T {
 apply(x, |y| y)
}
fn main() {
 let r = call_apply(3);
 assert!(r == 3);
}

thread 'rustc' panicked at src/rty.rs:1573:56:
called `Option::unwrap()` on a `None` value

Abridged stack:

rty::Instantiator::instantiate (src/rty.rs:1573 Value => value_var.unwrap())
rty::clause_builder::RefinementClauseBuilder::add_body
analyze::basic_block::Analyzer::relate_fn_param_sub_types_with_builder
analyze::basic_block::Analyzer::relate_fn_sub_type
analyze::basic_block::Analyzer::type_call (analyzing the `f(x)` call inside apply)
...
analyze::Analyzer::def_ty_with_args (apply analyzed per-instantiation)

The Value variable in the closure parameter's refinement reaches Instantiator::instantiate without a value_var being set, during the RustCall parameter expansion for the f(x) call. It only triggers when the closure's argument type is a generic parameter (T); the monomorphic analogue (F: FnOnce(i32) -> i32) verifies fine.

Notes

• Reproduces on main both before and after Verify generic functions' bodies against requires/ensures contracts #105.
• Before Verify generic functions' bodies against requires/ensures contracts #105, a specified generic HOF was a trusted summary (its body was not verified), so an annotated version of this case did not hit the panic. Now that Verify generic functions' bodies against requires/ensures contracts #105 verifies generic bodies, annotated generic HOFs that take generic-typed closures hit it too. (Surfaced while rebasing the closure pre-/post-condition feature, Refer to closure pre-/post-conditions in specifications #104, whose closure_postcondition_generic.rs test exercises exactly this shape.)
• The monomorphic closure cases verify correctly, so this is specific to generic-typed closure parameters in the RustCall parameter-relation path.