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.

[matthewjasper]

@davidtwco It appears that #55937 fixed this. Can this issue be closed?

[davidtwco]

@matthewjasper my understanding was that @pnkfelix was going to build atop #55937 in order to fix this issue.

In their previous comment, @pnkfelix linked a branch that built on a earlier iteration of #55937 and added e45dca5 - the changes in this commit aren't on master so I assume there's still some work to land to fix whatever underlying issue exists.

[pnkfelix]

Sorry for the confusion here. For some reason the examples I kept posting didn't have a use of a repeated ty instantiated with a type wildcard.

I think this example should serve to show how things still go wrong, even in the current nightly, when you are using just a wildcard instead of an explicit type:

#![feature(nll)]

#![allow(dead_code, unused_mut)]
type PairUncoupled<'a, 'b, T> = (&'a T, &'b T);
type PairCoupledRegions<'a, T> = (&'a T, &'a T);
type PairCoupledTypes<T> = (T, T);

fn uncoupled_lhs<'a>(_x: &'a u32, s: &'static u32) -> &'static u32 {
    let ((mut y, mut _z),): (PairUncoupled<u32>,) = ((s, &_x),); // ok
    // Above compiling does *not* imply below would compile.
    // ::std::mem::swap(&mut y, &mut _z);
    y
}

fn coupled_regions_lhs<'a>(_x: &'a u32, s: &'static u32) -> &'static u32 {
    let ((mut y, mut _z),): (PairCoupledRegions<u32>,) = ((s, &_x),); //~ ERROR
    // Above compiling would imply below should compile.
    // ::std::mem::swap(&mut y, &mut _z);
    y
}

fn coupled_types_lhs<'a>(_x: &'a u32, s: &'static u32) -> &'static u32 {
    let ((mut y, mut _z),): (PairCoupledTypes<&u32>,) = ((s, &_x),); //~ ERROR
    // Above compiling would imply below should compile.
    // ::std::mem::swap(&mut y, &mut _z);
    y
}

fn coupled_wilds_lhs<'a>(_x: &'a u32, s: &'static u32) -> &'static u32 {
    let ((mut y, mut _z),): (PairCoupledTypes<_>,) = ((s, &_x),); //~ ERROR
    // Above compiling would imply below should compile.
    // ::std::mem::swap(&mut y, &mut _z);
    y
}

fn main() {
    uncoupled_lhs(&3, &4);
    coupled_regions_lhs(&3, &4);
    coupled_types_lhs(&3, &4);
    coupled_wilds_lhs(&3, &4);
}

(Details block here holds an earlier example that was not the correct way to illustrate the issue here, because the whole point of #55748 (comment) is that we want to focus on ascription on patterns, not expressions.)

I think this example ([play](https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=4b316654cd5660bb6955830f6b57463d)) should serve to show how things still go wrong, even in the current nightly, when you are using just a wildcard instead of an explicit type:

#![feature(nll, type_ascription)]

#![allow(dead_code, unused_mut)]
type PairUncoupled<'a, 'b, T> = (&'a T, &'b T);
type PairCoupledRegions<'a, T> = (&'a T, &'a T);
type PairCoupledTypes<T> = (T, T);

fn uncoupled<'a>(_x: &'a u32, s: &'static u32) -> &'static u32 {
    let ((mut y, mut _z),) = ((s, &_x),): (PairUncoupled<u32>,); // ok
    y
}

fn coupled_regions<'a>(_x: &'a u32, s: &'static u32) -> &'static u32 {
    let ((mut y, mut _z),) = ((s, &_x),): (PairCoupledRegions<u32>,); //~ ERROR
    y
}

fn coupled_types<'a>(_x: &'a u32, s: &'static u32) -> &'static u32 {
    let ((mut y, mut _z),) = ((s, &_x),): (PairCoupledTypes<&u32>,); //~ ERROR
    y
}

fn coupled_wilds<'a>(_x: &'a u32, s: &'static u32) -> &'static u32 {
    let ((mut y, mut _z),) = ((s, &_x),): (PairCoupledTypes<_>,); //~ ERROR
    // ::std::mem::swap(&mut y, &mut _z);
    y
}

fn main() {
    uncoupled(&3, &4);
    coupled_regions(&3, &4);
    coupled_types(&3, &4);
    coupled_wilds(&3, &4);
}

in particular, under NLL, this example produces only two errors (for coupled_regions and coupled_types, while it misses the case of coupled_wilds.

I think my aforementioned branch fixes that. I will double-check this claim now.

[pnkfelix]

I think my aforementioned branch fixes that. I will double-check this claim now.

Sigh. My ("rebased") branch does not appear to fix the coupled_wilds case. Reviewing now.

[pnkfelix]

(ah, my demo was once again flawed: I had the type ascriptions on the RHS's, while the bug I'm trying to fix with my branch is when they are on the LHS.)

[pnkfelix]

And now that I have fixed my test, it appears the current rustc captures the effect I desired: A single type ascription on a pattern provides both a (covariant) constraint on the input (or projection thereof) and an invariant constraint on the bindings (if any) within the pattern.

[pnkfelix]

(yes it seems like commit 4933793 captured and commented the desired behavior here.)

Let me just check if our test suite already has this case covered.

[pnkfelix]

Okay I'm considering myself done with the investigation now. PR #57729 adds the test I want, and issue #57731 tracks the bug with handling of EXPR: TYPE when the type contains _.