NLL: investigate ascription when a `_` wildcard tyvar is repeated

[pnkfelix]

Spawned off of #55637 (comment)

Update: I had updated this description with a demo. But reading over it now, I don't know why I thought the "demo" had anything to do with this bug as described. That is, I believe demo is showing a bug, but not necessarily this bug...

Nonetheless, I'm not going to spawn off yet another bug quite yet. Instead, I am just going to mark the demo as wrong-headed and try to spend some time exploring _ itself later.

Potentially wrong-headed demo

Here's a demo of the problem (play):

#![allow(dead_code, unused_mut)]
type Pair<T> = (T, T);

fn static_to_a_to_static_through_tyvar<'a>(x: &'a u32, s: &'static u32) -> &'static u32 {
    let (mut y, mut _z): Pair<&u32> = (s, x);

    // I should be able to add the call to `swap` below at whim based
    // on the above type annotation, which should coerce both `s` and
    // `x` to `&'1 u32` (and then `'1` should be inferred to be `'a`).

    // ::std::mem::swap(&mut y, &mut _z);

    // Likewise, the same rules that caused `y` and `_z` to have the
    // same `&'1 u32` type should likewise cause a borrow-check error
    // at this attempt to return a `&'static u32`.
    y
}

fn main() {
    static_to_a_to_static_through_tyvar(&3, &4);
}

Under AST-borrowck, it errors.

Under NLL migration mode, it errors.

• Update: no, it was accepted there (just like NLL below).

Under #![feature(nll)], is is accepted (play), and should not be.

More details below:

PR #55637 fixes #55552 by ignoring occurrences of _ that it finds as it descends through the type.

A potential problem is that type variables can be repeated, e.g. in a type Foo<T> = (T, T) and an annotation like Foo<_>

The problem then becomes: Is there some way that could lead to a scenario where one of the occurrences of the type variables gets unified with something that has a lifetime constraint like 'a, and the other occurrence of the type variable is unchecked (due to #55637) but ends up missing a case where it should have imposed that constraint on an expression whose type has a different incompatible lifetime...

[pnkfelix]

putting on Release milestone, to ensure we actually find out whether this is even a problem (i.e. make some examples of soundness bugs that are actually getting through due to this) before we do the Release.

[pnkfelix]

Oddly, so far the instances of this problem that I have been able to identify are not leveraging the code injected in PR #55637 ...

[nikomatsakis]

Removing from the milestone. This feels sufficiently obscure that it should not be categorized as a Release Blocker

[pnkfelix]

Hmm. I claimed above that the example from above (play) causes an error to be signalled under migration mode.

But it appears that this was simply false; migration mode has (incorrectly) accepted the (potentially wrong-headed) "example" since the latter half of October. I must have been failing to test it properly.

So that's something that should be fixed. It should probably get its own separate bug, even.

[pnkfelix]

An interesting twist: If I enable #![feature(type_ascription)] then the following variant of the (potentially wrong-headed) "example" is rejected by the compiler (play):

#![feature(nll, type_ascription)]

#![allow(dead_code, unused_mut)]
type Pair<T> = (T, T);

fn static_to_a_to_static_through_tyvar<'a>(_x: &'a u32, s: &'static u32) -> &'static u32 {
    let local = 3;
    let ((mut y, mut _z),) = ((s, &local),): (Pair<&u32>,);

    // I should be able to add the call to `swap` below at whim based
    // on the above type annotation, which should coerce both `s` and
    // `x` to `&'1 u32` (and then `'1` should be inferred to be `'a`).

    // ::std::mem::swap(&mut y, &mut _z);

    // Likewise, the same rules that caused `y` and `_z` to have the
    // same `&'1 u32` type should likewise cause a borrow-check error
    // at this attempt to return a `&'static u32`.
    y
}

fn main() {
    static_to_a_to_static_through_tyvar(&3, &4);
}

From what I can tell from the MIR .nll dump, the set of constraints on the regions has changed in this variations, but the other big change is this: in the case where the compiler is "misbehaving" and accepting the code, we see this ascription statement:

        AscribeUserType(_6, +, UserTypeProjection { base: Ty(Canonical { max_universe: U0, variables: [CanonicalVarInfo { kind: Region(U0) }], value: (&ReLateBound(DebruijnIndex(0), BrAnon(0)) u32, &ReLateBound(DebruijnIndex(0), BrAnon(0)) u32) }), projs: [] }); // bb0[13]: scope 1 at wildcard-tyvars.rs:10:26: 10:36

In the case where the compiler is correctly rejecting the code, we see this ascription statement:

        AscribeUserType(_6, o, UserTypeProjection { base: Ty(Canonical { max_universe: U0, variables: [CanonicalVarInfo { kind: Region(U0) }], value: (&ReLateBound(DebruijnIndex(0), BrAnon(0)) u32, &ReLateBound(DebruijnIndex(0), BrAnon(0)) u32) }), projs: [] }); // bb0[13]: scope 1 at wildcard-tyvars.rs:10:27: 10:50

The only difference between those two lines, apart from column-span information, is the + variance (covariant) for the first case and the o variance (invariant) for the second case. Interesting!

[pnkfelix]

Sweet, I think the fix to the bug illustrated by the "potentially wrong-headed demo" is actually trivial: there was a single type-ascription call that used Covariant that (maybe) should instead have used Invariant.

(And furthermore, I think the demo itself probably illustrates that the problem I was originally worried about, namely soundness bugs injected by repeated wildcards, most likely do not arise)

[pnkfelix]

Further discussion in issue #56715 led me to conclude that the fix proposed above (of changing an Variance::Covariant to Variance::Invariant) is not the right way to resolve this.

So I'll take a step back and won't continue to assume that the solution lies down that path.

Incidentally, there have been other proposals (to resolve other issues) that might just as well address the problem pointed out in the "potentially wrong-headed demo."

[pnkfelix]

I now have a new approach issue-54943-with-fix-for-55748, built upon the foundation of PR #55937, that rejects the demo from this issue. Yay!

The heart of this approach, which I should document, is based on an insight that came from a recent conversation with @nikomatsakis :

You are asserting that _: T should be understood as constraining the RHS -- it's hard to see what else it could do. But where exactly do we draw the line?

Or.. do we? I feel like perhaps the T has two effects?

One is to be a supertype of the RHS?

The other is to specify the types of the bindings (if any) as an "equality" constraint?

Enforcing these two distinct constraints from a type annotation (or rather, adding the second constraint since we already had the first one) is what issue-54943-with-fix-for-55748 is doing.