opaque type definition: strict lifetime equality vs equal-by-inference #113971

The following code compiles but I don't think it should:

#![feature(type_alias_impl_trait)]
trait Captures<'a> {}
impl<T> Captures<'_> for T {}

fn ensure_outlives<'a, X: 'a>(_: X) {}
fn relate<X>(_: X, _: X) {}

type Opaque<'a> = impl Copy + Captures<'a>;
fn test<'x>(_: Opaque<'x>) {
    let opaque = None::<Opaque<'_>>; // let's call this lifetime '?1
    let hidden = None::<u8>;
    ensure_outlives::<'x>(opaque); // outlives constraint: '?1: 'x
    relate(opaque, hidden); // defining use: Opaque<'?1> := u8
}

Here we have a defining use of an opaque type Opaque<'_> == u8 with a questionable legality. Let's call the inferred lifetime '?1.

At each defining use of an opaque type, we require its lifetime arguments (['?1]) to be equal to one of the lifetime parameters in scope (in this case there is only 'x). This defining use passes this check because ensure_outlives registers a region constraint '?1: 'x, and, because we infer the least possible value for lifetime variables, we end up inferring '?1 == 'x.

The current situation is fine in regard to borrowck soundness (which is the reason we have such check in the first place) but it requires a subtle reasoning of lifetimes and makes the code more fragile (more on that later). For these reason, I believe we should enforce a stricter form of equality that requires both constraints ['x: '?1, '?1: 'x] in order to consider the lifetimes equal. It would be backward-compatible to change that later.

To demonstrate how fragile the current behavior can be, here is a couple of trivial changes that break the original example.

• '?1: 'x constraint is no longer generated at ensure_equal:

-type Opaque<'a> = impl Copy + Captures<'a>;
+type Opaque<'a> = impl Copy + Captures<'a> + 'static;

• a fundamental limitation of member constraints is exposed. I believe it is hard to fix.

     let opaque = None::<Opaque<'_>>;
-    let hidden = None::<u8>;
+    let hidden = None::<&'x u8>;

cc @rust-lang/nitiative-impl-trait