consider the following code:

struct Inv<'a>(*mut &'a u8);
type Sup = for<'x>     fn(Inv<'x>, Inv<'x>);
type Sub = for<'a, 'b> fn(Inv<'a>, Inv<'b>);
fn relate(sub: Sub) -> Sup { sub }

The subtyping relation of polymorphic types: `Sub <: Sup`, is equivalent to the logical statement:
> for each instance of `Sup`, there exists an instance of `Sub` such that `Sub <: Sup`

in chalk terms ...
`forall<'x> { exists<'a, 'b> { fn(Inv<'a>, Inv<'b>) <: fn(Inv<'x>, Inv<'x>) } }`

after applying usual subtyping rules:
`forall<'x> { exists<'a, 'b> { 'x == 'a, 'x == 'b } }`

when encoding this using universes/placeholders, we get a simple set of region constraints:
`{ '!x_U1 == '?a_U1, '!x_U1 == '?b_U1 }`
where `'!x_U1` is placeholder/universal var in universe U1, and `'?a_U1`
is an existential var in U1.

# Where higher-ranked subtyping fails
Note that higher-ranked subtyping/equality is infallible at the `TypeRelation` level.
We only register higher-ranked region constraints using placeholders/universes to be checked later.

Higher ranked region constraints are checked in the following places:
- full region resolution in mir_borrowck and regionck: not discussed here.
- the "leak check"
The leak check is responsible of judging if a higher ranked subtyping/equality holds before the full region resolution.
It is used only in coherence and candidate evaluation.

trait Trait { const POLYMORPHIC: bool; }
impl<'a> Trait for         fn(&'a str) { const POLYMORPHIC: bool = false; }
impl     Trait for for<'a> fn(&'a str) { const POLYMORPHIC: bool = true; }
//~^ WARN conflicting implementations of trait `Trait` for type `fn(&str)`

// Equating Self type to both impl headers is infallible.
// It's the job of the leack-check to select the right impl ..
const _: bool = <fn(&'static str) as Trait>::POLYMORPHIC; // false
const _: bool = <fn(&'_ str)      as Trait>::POLYMORPHIC; // true

We emmit a `coherence_leak_check` future-compat warning in all cases where leak-check is required for coherence,
because the leak-check was introduced as a "hack" to keep backward compatibility during the transition to universes in #56105

Note is that by ignoring the the leak check, we are strictly accepting less code - more impls would be conidered overlapping by coherence and we would have more inference ambiguities due to a less powerful winnowing.

# how to check higher-ranked region-constraints
two rules to obey:
1. rule#1: A placeholder shouldn't outlive *any region* from a parent universe.
1. rule#2: A placeholder shouldn't outlive *another placeholder* of the same or of a child universe.

exist<'a> { forall<'x> { 'x: 'a } } => '!x_U1 : '?a_U0 // rejected by rule #1
forall<'x> { exist<'a> { 'x: 'a } } => '!x_U1 : '?a_U1 // ok.

forall<'x, 'a>          { 'x: 'a }   => 'x_U1 : '!a_U1 // rejected by rule #2
forall<'x> { forall<'a> { 'x: 'a } } => 'x_U1 : '!a_U2 // rejected by rule #2
forall<'x> { exist<'a>  { 'x: 'a } } => 'x_U1 : '?a_U1 // ok.

The reason behind rule#1 is that a placeholder region can be shorter than the shortest region from a parent universe
as it may represent a region local to the callee stack, for example, which is always shorter than any region from the caller function.

fn absurd<'a>()
where
    for<'x> &'x str: 'a,
{
}

fn main() {
    absurd::<'_>(); // '!x_U1 : '?a_U0
    //~^ ERROR higher-ranked lifetime error
}

If we were to ignore rule#1, we could return references local to the function body:

fn absurd<'a>() -> &'a str
where
    for<'x> &'x str: 'a,
{
    &String::from("temporary") // any reference oultives 'a, so why not!
}

# The need to relax leak-check
The leak-check is the reason why coherence recoognize these two impls as non-overlapping:

trait Trait {}
impl<'a> Trait for         fn(&'a str) {}
impl     Trait for for<'a> fn(&'a str) {}
//~^ WARN conflicting implementations of trait `Trait` for type `fn(&str)`

While the the previous code seems benign, because it is :),
here is a case that we should really break if we consider the future direction of using implicit bounds on binders:

trait Trait {}

// `'a and 'b are equal inside the binder
// both impls should overlap.
impl<T> Trait for for<'a, 'b> fn(&'a &'b (), &'b &'a ()) -> &'a () {}
impl<T> Trait for for<'a, 'b> fn(&'a &'b (), &'b &'a ()) -> &'b () {}
//~^ WARN conflicting implementations of trait `Trait`

One way to keep supporting the former while breaking the latter is to ignore rule#2 in the leak check. This is implemented in #112999.

The way we distinguish the two is by introducing the concept of "sane" implied bounds on binders. A higher-ranked subtyping/equality is rejected by the leak-check if and only if there is no possible set of sane implied bounds that can make the subtyping hold.

trait Trait {}

// These impls are accepted previously and now overlap under the new leak-check
// because we can add a set of sane implied bounds to both binders to make them equal:
// for<'a: 'b, 'b> fn(&'a u8, &'b u8) -> &'b u8;
// for<'a, 'b: 'a> fn(&'a u8, &'b u8) -> &'a u8;
impl Trait for for<'a, 'b> fn(&'a u8, &'b u8) -> &'b u8 {}
impl Trait for for<'a, 'b> fn(&'a u8, &'b u8) -> &'a u8 {}

// A variant of wasm-bindgen...
// This is still supported by the new leak check
// There is no set of *sane* implied bounds we can add to the binders that makes the impls overlap
// The only bound that can be added to the binder in order to make the types equal is this:
// for<'a: 'static> fn(&'a u8);
// but this is not a sane implied bound by definition (see below).
impl Trait for fn(&'static u8) {}
impl Trait for for<'a> fn(&'a u8) {}

> Implication bounds on a binder are considered "sane" iff the lower bound of the outlive relation is one of the bound regions of the binder

# Questions and comments

## "rule#2: A placeholder shouldn’t outlive another placeholder of the same or of a child universe."

jack: so, this is something to think about - if someone writes `for<'a, 'b> Trait<'a, 'b>` with `trait Trait<'a, 'b> where 'a: 'b`, this would always fail

jack: actually, even rule #1 could be interesting to think about in the sense of implied bounds:

fn absurd<'a>()
where
    for<'x> &'x str: 'a,
{
}

this could certainly be desugared to:

fn absurd<'a>()
where
    for<'x where 'x: 'a> &'x str: 'a,
{
}

aliemjay: `for<'x where 'x: 'a> &'x str: 'a,` wouldn't be a "sane" implied bound and I suggest to never support such type of implied bounds.

## missing rule for HR regions

nikomatsakis: It's true that placeholders should not outlive regions from parent universes, but it's also true that they should not be outlived by those regions (except for 'static). This is a bit subtle because of inference -- i.e., if you have `?x : !y`, you can always satisfy it by infering `?x` to be static (but that may cause other constraints to be unsolveable). Still, I found the text a bit surprising.

## how Niko expected to solve this problem

This isn't yet modeled in a-mir-formality, but I was expecting to introduce the implied bounds into the environment and then essentially, well, look for solutions. So in the case that we wish to disallow, we would have `'a: 'b` and `'b: 'a` in the environment, and would be able therefore to prove both of these via an env rule. I admit I've not though about efficient implementation. I'm not sure I understand the idea of just "not enforcing" rule 2. Have to think about that I guess.