instantiating impl generic args with `'empty` is unsound

[lcnr]

originally found by @carlini as "bug 5" in https://rust-lang.zulipchat.com/#narrow/channel/364551-t-types.2Ftrait-system-refactor/topic/Reporting.20a.20collection.20of.20soundness.20bugs.20in.20next-solver/near/617737394

use std::fmt::Display;
trait ToObj<'a> {
    fn to_obj(self) -> Box<dyn Display + 'a>;
}
impl<'a, T: Display + 'a> ToObj<'a> for T {
    fn to_obj(self) -> Box<dyn Display + 'a> {
        Box::new(self)
    }
}

trait Super {
    fn yeet(&self);
}
impl<'a> Super for ()
where
    for<'b> &'b str: ToObj<'a>,
{
    fn yeet(&self) {
        let dangling = String::from("hello").as_str().to_obj();
        println!("{dangling}");
    }
}

trait Trait: Super {}
impl Trait for () {}

fn main() {
    let _ = (&() as &dyn Trait).yeet();
}

This incorrectly compiles with both the old and the new solver.

The problem is that lexical region resolution supports 'empty and considers for<'b> 'b: 'a to hold if 'a is 'empty. leak_check and MIR borrowck do not have the notion of 'empty anymore.

[lcnr]

To exploit this unsoundness, we need to only use the impl which relies on 'empty outside of a body as doing so during MIR borrowck errors.

The original repro by @carlini did this as part of the Drop impl: https://rust.godbolt.org/z/zn1vnrM6f I don't understand where this encounters the leak_check when compiled with the old solver.

[lcnr]

This would get fixed by #152438

rust/compiler/rustc_infer/src/infer/lexical_region_resolve/mod.rs

Lines 583 to 585 in e457a7b

	let VarValue::Value(sub_region) = *sub_data else {
	continue;
	};

This is responsible for allowing 'placeholder/param: 'empty

[lcnr]

trait Ext<'a> {
    fn ext(self) -> &'a String;
}
impl<'a, 'b: 'a> Ext<'a> for &'b String {
    fn ext(self) -> &'a String {
        self
    }
}

struct S;
impl<'a> Drop for S
where
    for<'b> &'b String: Ext<'a>,
{
    fn drop(&mut self) {
        let dangling: &'a String = (&String::from("hello")).ext();
        println!("{dangling}");
    }
}

fn main() {
    let _ = S;
}

This does not compile with the old solver. The reason for this is kind of subtle.

Instead of '!b: '?a we get '!b_drop = '?b_ext, '?a_ext: '?a_drop, and '?b_ext: '?a_ext

This means we set '?b_ext to '!b_drop. We then expand VarSubVar for '?b_ext: '?a_ext. That also just sets '?a_ext to 'b_drop. Finally we get '?a_ext: '?a_drop

I hate the sub and sup here. For this constraint '?a_drop is sub and '?a_ext is sup. '?a_drop is Empty while '?a_ext is RePlaceholder which can't be named by 'sub_universe. This forces '?a_ext to 'static. This is how we error.

So we have 'empty only wrt to direct param outlives var, but not param eq var outlives var ✨