The compiler basically has these rules:
Γ, WF(fn(τ) -> σ), x : τ ⊢ EXPR: σ
----------------------------------
Γ ⊢ fn(x) { EXPR } : fn(τ) -> σ
Γ ⊢ WF(fn(τ) -> σ), x : τ, f : fn(τ) -> σ
-----------------------------------------
Γ ⊢ f(x) : σ
Aka when checking a function calls, it adds wf obligations on the function’s arguments and
Which (I’m quite sure are) sound by themselves, but are not sound in the presence of subtyping, because the supertype of the WF callee type might be non-WF by itself.
Note that ATM (unless we make the change of replacing the WF(fn(τ) -> σ) assumption with a WF(τ) assumption), no contravariance is required:
static S: &'static &'static u8 = &&0;
fn helper<'a, 'b>(x: &'a u8, _y: &'b u8) -> (&'b &'a u8, &'b u8) {
(S, x)
}
pub fn coerce_lifetime<'x, 'y>(x: &'x u8) -> &'static u8 {
let helper: for<'a, 'b> fn(&'a u8, &'b u8) -> (&'b &'a u8, &'b u8)
= helper;
let helper: for<'a> fn(&'a u8, &'static u8) -> (&'static &'a u8, &'static u8)
= helper;
let helper: for<'a> fn(&'a u8, &'static u8) -> (&'a &'a u8, &'static u8)
= helper;
helper(x, *S).1
}
This is the case at least since RFC #1214 landed (the pre-#1214 rules are totally crazy).
Note that typeck also checks WF in tons of random places, both to improve error messages and because trans does not like to see things such as structs with arrays in their middle etc, but the main place WF is required for soundness is because it is used as an assumption at call-sites.
