Bind higher-ranked lifetimes of fn-pointer contract-target types #4933

Requested feature:

A proof_for_contract target whose fn-pointer argument is higher-ranked (fn(&u8) -> u8 is for<'a> fn(&'a u8) -> u8) should stay distinct from the same target spelled with 'static (fn(&'static u8) -> u8). The BareFn arm added in #4916 erases the fn pointer's regions (Binder::dummy), so the two collapse to one type and a higher-ranked target resolves to a coexisting 'static impl instead of its own. The fix is to bind the higher-ranked lifetimes as late-bound regions, and it has to be syntax-driven, since erasing is correct when the 'static lifetime is written explicitly.

Use case:

proof_for_contract on a target whose fn-pointer argument is higher-ranked, when a fn(&'static u8) -> u8 sibling impl also exists (the two coexist, with coherence_leak_check only warning). Without the binding, the higher-ranked target resolves to the 'static impl and its harness reports the target as not reachable. tautschnig identified this in the review of #4916 (#4916 (comment)) and sketches the fix there. Follow-up to #4916 and #4909.

Test case:

Save as hr.rs (self-contained, no standard library):

#![allow(coherence_leak_check)]

struct Wrap<T>(T);
trait Probe {
    fn probe(&self) -> u32;
}

impl Probe for Wrap<fn(&u8) -> u8> {
    #[kani::ensures(|r| *r == 7)]
    fn probe(&self) -> u32 {
        7
    }
}

impl Probe for Wrap<fn(&'static u8) -> u8> {
    #[kani::ensures(|r| *r == 9)]
    fn probe(&self) -> u32 {
        9
    }
}

#[kani::proof_for_contract(<Wrap<fn(&'static u8) -> u8> as Probe>::probe)]
fn h_static() {
    fn d(x: &'static u8) -> u8 {
        *x
    }
    let _ = Wrap(d as fn(&'static u8) -> u8).probe();
}

#[kani::proof_for_contract(<Wrap<fn(&u8) -> u8> as Probe>::probe)]
fn h_hr() {
    fn d(x: &u8) -> u8 {
        *x
    }
    let _ = Wrap(d as fn(&u8) -> u8).probe();
}

using the following command line invocation:

kani hr.rs -Z function-contracts

On the BareFn arm (#4916), h_static verifies but h_hr fails: its target resolves to the 'static impl, so kani reports it as not reachable from the h_hr harness. With the binding, both should verify.