HRTB can't prove some trivially true statements

[djzin]

fn lifetime<'a>()
    where &'a (): 'a
{
    /* do nothing */
}

fn doesnt_work()
    where for<'a> &'a (): 'a
{
    /* do nothing */
}

fn main() {
    lifetime();
    doesnt_work();
}

Was trying to demonstrate lifetimes of references fulfilling the 'a lifetime bound - but then came across this. The bound can be proven easily for a specific 'a - but for some reason not for the higher-ranked version. The error for doesnt_work looks like this:

rustc 1.19.0-nightly (5dfcd85fd 2017-05-19)
error[E0280]: the requirement `for<'a> &'a () : 'a` is not satisfied
  --> <anon>:15:5
   |
15 |     doesnt_work();
   |     ^^^^^^^^^^^
   |
   = note: required by `doesnt_work`

error: aborting due to previous error

[djzin]

Note this also works:

trait Prove<'a> : 'a {}

impl<'a> Prove<'a> for &'a () {}

fn does_work()
    where for<'a> &'a (): Prove<'a>
{}

but attaching a where bound to the trait impl makes it fail!

trait Prove<'a> : 'a {}

impl<'a> Prove<'a> for &'a () where Self: 'a {}

fn doesnt_work()
    where for<'a> &'a (): Prove<'a>
{}

[steveklabnik]

Triage: original example still does not compile

[oskgo]

Triage: Both examples compile on rust stable 1.66.0

Seems related to #27113, which should also be closed.

[oskgo]

@rustbot label +E-needs-test