NLL accepts higher-ranked subtype that non-NLL rejects

[matthewjasper]

The following code example (playground)

// #![feature(nll)]

trait X {
    type G;
    fn make_g() -> Self::G;
}

impl<'a> X for fn(&'a ()) {
    type G = &'a ();

    fn make_g() -> Self::G {
        &()
    }
}

trait Y {
    type F;
    fn make_f() -> Self::F;
}

impl<T> Y for fn(T) {
    type F = fn(T);
    
    fn make_f() -> Self::F {
        |_| {}
    }
}

// Always an error, but the message is bad
fn higher_ranked_region_has_lost_its_binder() {
    let x = <fn (&())>::make_g();
}

// Works, but only with feature(nll)
fn magical() {
    let x = <fn (&())>::make_f();
}

produces the output

error[E0308]: mismatched types
  --> src/lib.rs:31:13
   |
31 |     let x = <fn (&())>::make_g();
   |             ^^^^^^^^^^^^^^^^^^ one type is more general than the other
   |
   = note: expected type `X`
              found type `X`

error[E0308]: mismatched types
  --> src/lib.rs:36:13
   |
36 |     let x = <fn (&())>::make_f();
   |             ^^^^^^^^^^^^^^^^^^ one type is more general than the other
   |
   = note: expected type `Y`
              found type `Y`

The second example also unexpectedly compiles in full NLL mode.

[nikomatsakis]

I renamed the title to focus on the part I would most like to investigate, which is why this function works but only with feature-nll:

// Works, but only with feature(nll)
fn magical() {
    let x = <fn (&())>::make_f();
}

That seems like a blocker to disabling migration mode.

[pnkfelix]

cc #58781

[pnkfelix]

marking P-medium to reflect that this is solely about #![feature(nll)], not migration mode (#58781). When the latter becomes higher priority, this will likewise be raised up.

[matthewjasper]

Update: this is only an issue now with -Zno-leak-check

[pnkfelix]

cc blocks #59490

[oli-obk]

Diagnostics triage: this is not a diagnostics issue

[Aaron1011]

This is now a compiler error with -Z no-leak-check:

error: higher-ranked subtype error
  --> test.rs:31:13
   |
31 |     let x = <fn (&())>::make_g();
   |             ^^^^^^^^^^^^^^^^^^^^

[matthewjasper]

Yes, but it should be two compiler errors, one in make_f and one on make_g.

[Aaron1011]

Looking at this further - why don't we want magical to compile? It looks perfectly correct to me.

[nikomatsakis]

Running this example with my branch from #65232 yields, among some other errors:

error: implementation of `X` is not general enough
  --> /home/nmatsakis/tmp/issue-57642.rs:31:13
   |
3  | / trait X {
4  | |     type G;
5  | |     fn make_g() -> Self::G;
6  | | }
   | |_- trait `X` defined here
...
31 |       let x = <fn (&())>::make_g();
   |               ^^^^^^^^^^^^^^^^^^ implementation of `X` is not general enough
   |
   = note: `X` would have to be implemented for the type `for<'r> fn(&'r ())`
   = note: ...but `X` is actually implemented for the type `fn(&'0 ())`, for some specific lifetime `'0`

error: implementation of `Y` is not general enough
  --> /home/nmatsakis/tmp/issue-57642.rs:36:13
   |
16 | / trait Y {
17 | |     type F;
18 | |     fn make_f() -> Self::F;
19 | | }
   | |_- trait `Y` defined here
...
36 |       let x = <fn (&())>::make_f();
   |               ^^^^^^^^^^^^^^^^^^ implementation of `Y` is not general enough
   |
   = note: `Y` would have to be implemented for the type `for<'r> fn(&'r ())`
   = note: ...but `Y` is actually implemented for the type `fn(&'0 ())`, for some specific lifetime `'0`

This error seems correct. If I had to guess the problem with NLL, though, I would guess that this is working because of the 'empty rule -- in other words, we are inferring Y to be implemented for fn(&'empty ()) and we are (not incorrectly) deducing that fn(&'empty()) = fn(&()). My branch rejects this because I specifically tried to disallow that. I am not entirely convinced that we should disallow this -- it's just that 'empty doesn't have a very natural analog in polonius (though you can make it make sense). In fact, the idea of 'empty is kind of useful, or could be, so it may be that we want to accept it.

If we want to disallow this example, I think we'll have to extend NLL to have a similarly "graded" notion of 'empty. I imagine the way to do this would be to extend the set of elements to include "empty" elements in each universe we create, and then permit these empty elements get added to all the "free regions" in the root universe.

[Aaron1011]

On the latest nightly, passing -Z borrowck=mir -Z no-leak-check causes higher_ranked_region_has_lost_its_binder and magical to produce higher-ranked subtype error.

I think this is now purely a diagnostic issue, rather than a soundness issue.