-Ztrait-solver=next: deduplicate region constraints in query responses

[lcnr]

pub struct Bar
where
    for<'a> &'a mut Self:;

fn main() {}

results in overflow in the new solver when checking WF(Bar) or `for<'a> WF(&'a mut Bar). The issue is as follows:

pub struct Bar
where
    for<'a> &'a mut Bar:;

• for<'a> WF(&'a mut Bar) (attempt 0)
  • WF(&'a.1 mut Bar)
    • outlives(Bar, 'a.1) OK [Bar: 'a.1]
    • WF(Bar)
      • for<'a> WF(&'a mut Bar) cycle OK []
  • RESULT: OK [Bar: 'a.1]
• for<'a> WF(&'a mut Bar) (attempt 1)
  • WF(&'a.1 mut Bar)
    • outlives(Bar, 'a.1) OK [Bar: 'a.1]
    • WF(Bar)
      • for<'a> WF(&'a mut Bar) cycle OK [Bar: 'a.2] (create new universe)
  • RESULT: OK [Bar: 'a.1, Bar: 'a.2]
• for<'a> WF(&'a mut Bar) (attempt 2)
  • WF(&'a.1 mut Bar)
    • outlives(Bar, 'a.1) OK [Bar: 'a.1]
    • WF(Bar)
      • for<'a> WF(&'a mut Bar) cycle OK [Bar: 'a.2, Bar: 'a.3] (create new universe)
  • RESULT: OK [Bar: 'a.1, Bar: 'a.2, Bar: 'a.3]

starting with WF(BAR)

• WF(Bar) iteration 0
  • for<'a> WF(&'a mut Bar)
    • WF(&'a.1 mut Bar)
      • outlives(Bar, 'a.1) OK [Bar: 'a.1]
      • WF(Bar) cycle OK []
• WF(Bar) iteration 1
  • for<'a> WF(&'a mut Bar)
    • WF(&'a.1 mut Bar)
      • outlives(Bar, 'a.1) OK [Bar: 'a.1]
      • WF(Bar) cycle OK [Bar: 'a.?]

a similar issue is:

struct Foo
where
    Foo:,
    for<'a> &'a ():;

• WF(Foo) iteration 0
  • WF(Foo) cycle OK []
  • for<'a> WF(&'a ()) OK [(): 'a.1] (new universe for unnameable placeholder)
  • result OK [(): 'a.1]
• WF(Foo) iteration 1 (in new infcx)
  • WF(Foo) cycle OK [(): 'a.1] (new universe for unnameable placeholder)
  • for<'a> WF(&'a ()) OK [(): 'a.2] (new universe for unnameable placeholder)
  • result OK [(): 'a.1, (): 'a.2] yikes (have to rerun again)

The long term plan to solve this is to eagerly deal with new placeholders in the solver, short term we probably want to somehow deduplicate new placeholder constraints when creating the query response we're going to ignore this because hopefully this pattern does not exist in user-code.

[compiler-errors]

tests/ui/traits/issue-22655.rs similarly errors out with ambiguous because we end up generating a never-ending list of outlives:

unsafe impl<T: Send + ?Sized> Send for Unique<T> { }

pub struct Unique<T:?Sized> {
    pointer: *const T,
}

pub struct Node<V> {
    vals: V,
    edges: Unique<Node<V>>,
}

fn is_send<T: Send>() {}

fn main() {
    is_send::<Node<&'static ()>>();
}

[ndrewxie]

Hey all,

If nobody else is currently tackling this issue, could I take a shot at it?

Also my apologies if the remainder of the post is really badly misinformed - if it's clear that this issue should be left to someone in the new trait solver working group, just let me know and I'll try something else instead.

My first attempt at this was deduping all the placeholder region obligations (in eval_ctxt/canonical.rs, deduping the RePlaceholder s inside region_obligations in the function compute_external_query_constraints), and it resolved the compiler errors in the first two examples lcnr gave. However, I'm not fully sure if my approach is sound - what I did was collect all the Placeholders for each universe into a FxIndexMap, and if two universes had the same Placeholders (up to re-naming the universes inside the placeholders), then I would remove one of the universes.

My idea for the snippet presented by compiler-errors is to do the deduping inside of evaluate_canonical_goal (eval_ctxt.rs) instead - search_graph.with_new_goal returns a QueryResult, so would it be correct to just dedup the variables if they're "functionally identical" from the POV of the region_constraints present? i.e. if we take all the outlives constraints that involve one variable, and replace that variable in those constraints with another one, this procedure just yields a bunch of constraints that already exist (and therefore we can just remove the duplicates). I've been hesitant to prototype this because I'm really not sure of its soundness, because all the region variables being created are CanonicalVarInfos, not marked as placeholders - so maybe this would be removing some regions that actually correspond to real regions in the code?

Once again, if someone's already working on this, or if it's an issue best left to a dedicated working group, just lmk and I'll just go do something else :)

[lcnr]

@ndrewxie sure, go ahead. this is a fairly difficult issue to start with but it's also something nobody is working on right now and should be fairly interesting 😁

given that it's fairly complex, please do the following if you intend to keep working on this:

• use @ rustbot claim to assign this issue to you
• open a zulip thread to discuss this, in the t-types/trait-system-refactor stream. I personally greatly prefer zulip for more involved conversations
• also, if you already have some approach implemented, please share the code, even if it is still a WIP. It makes it easier to talk about specific parts of your approach.

What I can say by taking a quick look at your description "two universes had the same Placeholders " is not enough. The actual name of placeholders is mostly moot. I would instead like to check that the region constraints involving different placeholders are equal. E.g. if you have 'placeholder: 'a and 'other_placeholder: 'a as the only constraint, you can dedup them

[ndrewxie]

@rustbot claim

[ndrewxie]

Aah ok, thanks!

I opened the zulip thread here

[aliemjay]

This issue is not specific to HRTB bounds and universes. This snippet, for example, generates a never-ending stream of (): 'static bounds.

struct Foo
where
    Foo:,
    (): 'static;

Perhaps the title should be changed to "deduplicate region constraints" instead.

[ndrewxie]

Aah, I see. For the example you gave, all the constraints are identical, so I just added a quick dedup for 100% identical cases. Probably doesn't cover everything, but I'll keep working on it.

The question I'm having right now is, how far can this deduplication go? Can all region constraints be deduplicated, or is it just restricted to placeholders?

[lcnr]

all region constraints can get deduplicated (as long as we don't drop any meaningful information)

[ndrewxie]

all region constraints can get deduplicated (as long as we don't drop any meaningful information)

👍 Thanks! Just to be clear - if I'm deduping the canonicalized Response, any variable that's not in the root universe is a variable created during solving, so they don't count as "meaningful information" (as in, they can't just be all deleted, but they can be deduplicated).

I'm still ironing out a few final kinks - the trickiest case is if we have constraints that involve multiple variables that we can potentially deduplicate, but I think I've finally settled on a solution that would work (sorry that I've taken so long - took me a while to figure out what each part of the solver was doing and the best place to insert my changes)

But just one question - what time complexity is permitted? My current implementation is very likely going to be O(n^2), as it relies on building a table of "which constraints are 'approximately equal' to each other", which is inherently O(n^2). I define 'approximately equal' as constraints that are identical except they differ in variables that we can re-write - e.g. one constraint involves placeholder var 1 and the other involves var 2, but they're otherwise identical. These 'approximately equal' constraints then get pruned - if merging 2 constraints by re-writing variables would impact other constraints in a way that doesn't map constraints onto already-existing constraints, then these 2 constraints are no longer considered 'approximately equal'. Continuing this way would yield constraints that we know can be merged, which should accomplish the dedup, right? But there's definitely no way this is faster than O(n^2).

[lcnr]

Any variable that's not in the root universe is a variable created during solving, so they don't count as "meaningful information" (as in, they can't just be all deleted, but they can be deduplicated).

👍

O(n^2) should definitely be fine. n should be quite small in nearly all cases so I think that optimizing this for small n is actually more important.

sorry that I've taken so long - took me a while to figure out what each part of the solver was doing and the best place to insert my changes

no worries 😁 this is currently not blocking any work and a complex issue. Happy that you're apparently able to make significant progress on this yourself