Check constraints arising from higher-rank trait bounds (HRTBs)

[ecstatic-morse]

This issue tracks error compatibility with the current version of rustc for functions involving HRTBs. This is one of the major features missing from Polonius.

Currently, rustc uses the concept of Universes (described in detail here to reason about HRTBs. Previously, it used something called the leak check, which I believe still exists in some form.

rustc implementation history (possibly incomplete):

• Universes rust#55517
• Re-implement leak check in terms of universes rust#58592
• replace the leak check with universes, take 2 rust#65232
• extend NLL checker to understand 'empty combined with universes rust#70950
• MCP notes

Relevant test cases (definitely incomplete):

• ICE related to lifetimes and traits rust#58451
• Regression in trait bounds that are redundant with associated type's HRTB rust#57639

Currently, Polonius cannot handle quantified constraints arising from HRTBs. One possible framework, hereditary-harrop predicates, were explored in Niko's blog post. I discussed the implications of allowing a reduced set of these (just the quantifiers) in a later post.

For now, the goal is simply to reach feature parity with current versions of rustc, but the rustc borrow-checker has some shortcomings around HRTBs, where it needs to represent constraints like for <'a, 'b: 'a>, and there are some upcoming features that may complicate things further:

• Implied bounds on nested references + variance = soundness hole rust#25860
• HRTB on subtrait unsoundly provides HTRB on supertrait with weaker implied bounds rust#84591
  • same as above, but more current
• Tracking issue for member constraints in region inference rust#61997
• GATs?

[ecstatic-morse]

Sprint 2021-07-30 Notes

After a day to reflect, I've written up a summary of the conversation I had with Niko about HRTBs and Polonius. Personal notes are italicized.

HRTBs and Polonius

After some background discussion about universes, Niko gave the following example to illustrate how HRTBs can become entangled in borrow-checking function bodies:

fn foo<'a>(x: &'a u32) where for<'b> 'a: 'b { } // Pseudo-Rust ('b <: 'a -> 'a = 'static)

// The equivalent (I think) in actual Rust.
/*
trait Outlives<'a, 'b> {}
impl<'a: 'b, 'b> Outlives<'a, 'b> for () {}
fn foo<'a>(x: &'a u32) where for<'b> (): Outlives<'a, 'b> {}
*/

fn bar() {
    let x = 22;
    let y/*: &'y i32*/ = &22
    foo(y);
}

In the example, foo is called with the result of a borrow (we'll call its origin 'y), but the bounds on foo require the input lifetime to be 'static, so this should result in an error. Niko went on to describe how NLL would handle this using universes.

I'm still a bit confused as to where the boundary between trait selection, type checking, and borrow checking (Polonius) lies exactly. Most of the HRTBs tests for rustc have to do with trait selection and type checking AFAICT, function bodies are not usually involved. Niko went on to give the a related example where the bounds are reversed:

fn foo<'a>(a: &'a u32) where for<'b> 'b: 'a { }

fn bar<'x>(x: &'x u32) {
    foo(x);
}

But forall<'b> 'b <: 'ais not satisfiable (there's no "top" element in Polonius), so it seems like we could reject this during type checking as soon as we see it get invoked. Similarly, I wonder why we can't simplify the bound on the other example so it becomes 'a: 'static? Maybe it stops working once we start having bounds spread across multiple traits? I dunno.

A digression on subset errors vs. loan invalidation

Niko briefly discussed an alternate approach to generating errors for borrows of stack variables that escape the function body. For example,

fn foo() -> &'static u32 {
    let x = 22;
    &/*'x*/ x
}

Currently, Polonius would emit an error when it sees that the loan created in &y was invalidated after y goes out of scope, because 'static is "always live". However, that's not the only possible formulation. The assignment to the return place would create a subset relationship 'x <: 'static, which means a loan would flow into 'static, despite 'static being (nominally) the empty set.

Niko also gave the example following example involving a deref projection.

fn foo<'a>(x: &'a u32) -> &'a u32 {
    let y = &*x; // loan L0
    y // here, 'a contains loan L0, but that's ok
}

Back to HRTBs

Niko returned to discussing the forall<'a> { exists<'b> { 'b: 'a } } constraints that might arise when you have a HRTB that also involves an existential lifetime variable. Regarding this constraint,

nikomatsakis: if you just try to prove this in isolation -- something goes wrong
nikomatsakis: if you just ignore universes, I mean
nikomatsakis: we will get 'a being in universe U0 (say) and then a !1 placeholder
nikomatsakis: and the rule that !1 <= 'a
nikomatsakis: but we ought not to be able to add !1 to 'a, because it is universe U0
nikomatsakis: so I do think you need a rule looking for this case
nikomatsakis: it's not the rule I wrote before though
nikomatsakis: it's saying:
    is there a subset relation 'a <= 'b somewhere
    in which 'a is a placeholder region in universe Um
    and 'b is universe Un
    and Un < Um

I was a bit confused by this, since in my framework (see the second example), this type of constraint is immediately unsatisfiable, so maybe we could handle this type of thing a different way? Unfortunately I didn't realize this in the moment (I blame the literal catfight).

He then gave the following example of a place where this kind of constraint might arise:

trait TheTrait { }
impl<'a> TheTrait for fn(&'a u32) { }

fn take<X: TheTrait>() { }

fn main() {
    take::<fn(&u32)>();
}

Ultimately, Niko concluded,

> - polonius does need universe info
> - it's missing one rule, to capture exists<'a> { forall<'b> { 'b: 'a } } and make that an error
> - but the existing subset errors capture the other stuff

I'm not as convinced, but everything was moving pretty fast at this point. My blog post was all about how all universally quantified trait bounds are either unsatisfiable (as in the second point) or can be reduced to a bound on 'static. Is this still true? How do universes factor in here? Is it just a different way of saying the same thing? Or am I missing something essential? I think a more complex example of where universes are necessary would help.

Next Steps

The conversation ended here. The good news is that we might be close to replicating the existing borrow checker as far as HRTBs go. However, there's some open soundness holes (Niko mentions issue 25860), that might need a more advanced approach. Unfortunately I don't have any insight into these, and my understanding of universes and region inferences is lacking, so I'll need to do quite a bit of studying to get up to speed.