-Z trait-solver=next: Deduplicate region constraints in query responses

[ndrewxie]

An attempt at fixing #109764 .

This is a MVP version, so I'm opening a PR primarily so others can review and critique it (is this correct protocol? or should a work-in-progress like this be handled differently?). I'm sure there's many points where my implementation is incorrect, but right now it does compile all the snippets provided in the issue (which I put into 1 test file called dedup-vars), and doesn't break any other code (at least, nothing that's detected by any tests :P)

Right now, I'm deduplicating the output of canonicalizing the Response - is this correct?

The idea is as follows:

• Identify which variables can be deduplicated (i.e. merged if the constraints that involve them are isomorphic). For this version, I assumed that any variable that isn't in the root universe is dedupable, as canonicalization should compress all universes nameable from the caller to the root universe - correct?
• For each constraint (region constraints and member constraints), extract all the variables that are present, in order. This logic is handled by constraint-walker.rs. The question is, am I extracting the variables from the constraints correctly (or am I missing some)?
• For each constraint, we then create a "prototypical" version of the constraint, which is formed by replacing all variables with a dummy var. Constraints are considered structurally equal if their prototypical version is the same, i.e. they differ only in variables
• The constraint variables, as well as sets of structurally equal constraints is then fed into a dedup solver, which looks for isomorphisms between sets of constraints. The solver returns a set of constraints that can be removed, as well as a set of variables that can be removed
• The constraints and variables returned by the solver are then deleted. My question here is, does the order of constraints (as they're stored in .outlives and .member_constraints) matter? Right now, I'm not making any effort to preserve this order, but if it's needed I suppose I could do so, it'll just be less clean
• Variable universes are "compressed" - this is given in the function compress_variables in dedup_solver/mod.rs. As variables are removed, they leave "holes" of unused universes, so I pack the universes in the remaining variables to fill this hole (minimizing the maximum universe in the vars). Is the idea of this sound, or is there something more subtle to universes that I'm missing?

Also just a quick question, what exactly is opaque_types? I couldn't find much documentation about it, and reading the code didn't give any significant clues... Should this deduplication handle that in some way?

[rustbot]

r? @b-naber

(rustbot has picked a reviewer for you, use r? to override)

[rustbot]

⚠️ Warning ⚠️

• These commits modify submodules.

[rustbot]

Some changes occurred to the core trait solver

cc @rust-lang/initiative-trait-system-refactor

Some changes occurred in src/tools/cargo

cc @ehuss

[ndrewxie]

Aaaah my bad, it appears I screwed something up and staged some temp file changes to src/tools/cargo - if the rust bot pinged you about that, you can safely disregard this PR - I'll fix it once I figure out how to.

Edit: It appears that the current standings are git: 1, me: 0. I've tried doing git rm -r --cached src/tools/cargo, but it just broke my x.py (as in, none of the ./x.py commands worked afterwards). Anybody knows how I can untrack a folder?

[ndrewxie]

also r? @lcnr

[lcnr]

haven't looked at the algorithm yet, but some initial thoughts about to slightly simplify this impl.

you commited changes to cargo in 4bc7dd1b8275b129c89657852c446abe2338f471, see https://rustc-dev-guide.rust-lang.org/git.html#i-changed-a-submodule-by-accident for elp on how to solve this.

Is your algorithm something which can be viewed as:

• map rust constraints to a graph
• solve a known problem on graphs (or multiple problems in sequence)
• map the result back to rust constraints

iiuc DedupSolver::dedup calls a bunch of subroutines and at least some of them may be equivalent to something on ordinary graphs. If so, it would be good to 1. use or mention the terminology used for graphs. generally, DedupSolver::dedup seems like the core of your approach, so this might be a good place to explain what's going on there. Right now the meaning of "category" and "rule" isn't immediately clear to me.

[ndrewxie]

Yeah, the deduplication is essentially just one big graph algorithm :) The constraints are vertices, and if two constraints can potentially be merged, they have an edge between them, and the variable mapping that would merge them is the edge label.

I suppose a "category" can best be described as an isolated clique in the graph, i.e. a clique that has no edges joining it to any other clique.

"Rule" is just my internal representation of a rust constraint, I just used it during development cuz "rule" is shorter, but I'll go ahead and replace it with constraint now

I'd like to make a few minor changes to the dedup solver, so right now I didn't add any additional comments documenting that (so it probably can't be reviewed yet) - once I settle those, I'll put additional comments and explanations for review.

[compiler-errors]

@ndrewxie please use a rebase instead of a merge if you want to update your branch -- we have no "no merge commit" policy in the repo

[ndrewxie]

@ndrewxie please use a rebase instead of a merge if you want to update your branch -- we have no "no merge commit" policy in the repo

Alright, gocha. Do you have any pointers for how I can undo my mistake? (sorry, I'm not too good with git...)
Thanks!

[compiler-errors]

I think you can just do git pull --rebase $UPSTREAM master where $UPSTREAM is whatever origin name you've set for the rust-lang/rust repo, not your fork..

[ndrewxie]

Alright, I undid my erroneous merge. When I try doing git pull --rebase I'm getting a lot of merge conflicts, however. What's the best way to deal with this?

Also sorry I haven't had too much time to work on this recently, been wrapping up another PR and have a bunch of mandatory testing. In a couple more days, I should have more time to clean up my implementation and document it a bit more for review.

Also just one question regarding lcnr's comment about deduplicating in compute_external_query_constraints instead of deduplicating the canonicalized Response - I understand why that's desirable, but without the variable universe information which is provided in canonicalization, how can I decide whether a variable (referenced in a region constraint) is nameable from the caller or not? Cuz correct me if I'm wrong, but 2 variables can only be merged if 1. the rules they appear in are isomorphic (i.e. equal up to a re-arranging of variables) and 2. at least one of them is not nameable from the caller (otherwise we might remove an inference variable that the caller "knows about")

[lcnr]

the information about universes is also available before we have the canonical response, because how could we otherwise create the response? 😁

you can look at how canonicalization gets the universe for existential variables, iirc we use infcx.probe_var or sth

[ndrewxie]

the information about universes is also available before we have the canonical response, because how could we otherwise create the response? 😁

you can look at how canonicalization gets the universe for existential variables, iirc we use infcx.probe_var or sth

Haha I guess you're right, thanks for the help! I guess the new motto going forward is, "if you can't find something, just ctrl + f under InfCtxt" 😄

EDIT: Just now I realized that my whole constraint_walker stuff could be done with a TypeFolder, which would be far cleaner and be less error-prone. I'm currently re-writing that component.

[lcnr]

the way you currently lower region constraints to a set of variables feels wrong to me 🤔 didn't yet go over the extern solver in detail, but if you have &'var (): 'static and &'static (): 'var they should result in the same input for the solver afaict.

This is currently somewhat difficult for me to review and understand as there are a few things which feel a bit weird '^^ would you be up to take some time to chat about this in sync? either via text on zulip or via zoom?

Something else which would be really valuable would be some example lowerings from rust syntax to the solver constraints. You already did some manual lowering for the tests and having some small examples of "input X lowers to these constraints" would be very helpful.

[ndrewxie]

if you have &'var (): 'static and &'static (): 'var they should result in the same input for the solver afaict.

Just to confirm, this is because if var outlives static, then var must be static, so therefore static outlives var too, right? I guess this makes sense, but how could we apply it to more complicated types like &'var1 (&'var2, &'var3, &'var4)? Would we say that only &'static (): 'var1, or would this be true for var2, var3 and var4?

would you be up to take some time to chat about this in sync? either via text on zulip or via zoom?

Sure! Zulip would be more convenient for me, but both work. Github tells me you're in Germany, so on weekends any time after 15:00 CEST (9:00 AM EDT for me) should be fine. On weekdays, I'm basically limited to after 4:00 PM EDT, so after 22:00 CEST should work.

But yeah the solver in its present state isn't very clear - I'll rework it a bit today and add the comments you asked for. The solver is certainly related to graph theory, but my understanding of that is admittedly limited, and I can't really find a neat way to map the majority of it onto pre-existing graph theory problems...

[lcnr]

Just to confirm, this is because if var outlives static, then var must be static, so therefore static outlives var too, right?

woops, I meant that we should not consider them to be equal but iirc your solver currently generates the same constraints for them. What are the generated constraints for &'var (): 'static and &'static (): 'var rn?

[ndrewxie]

woops, I meant that we should not consider them to be equal but iirc your solver currently generates the same constraints for them.

Well, yes and no - the solver does extract the same variables for both (if we say 'var is index 0, then both will be represented as [0]), however, the solver will not attempt to merge the constraints. The reason for this lies in the constraint cliques - the idea is that we partition constraints into groups ("cliques") based on a variety of properties, and we only try merging constraints if they belong to the same clique. In this case, those two constraints will not belong to the same clique because of the placement of the &'static.

These cliques get refined later in the solving process, but when we first scan the constraints and extract variables, we create "rough" cliques by the following procedure:

1. Take an input constraint and walk over it (TypeFolder) and extract variables as a Vec
2. A copy of each constraint is then made, with all the variables replaced with a dummy placeholder (done through TypeFolder). For example, &'var (): 'static would become &<SOME DUMMY PLACEHOLDER>: 'static, and &'static (): var would become &'static (): <SOME DUMMY PLACEHOLDER>. I think I called them "erased constraints" or something in my code. Essentially, this process erases the information of the actual var values, however, everything that isn't a var value (e.g. 'static) is still kept. Moreover, the order and location of all these terms is still retained. This allows us to answer the question of, "are these constraints equal if we ignore variables"?
3. We then build a map, mapping an erased constraint to a set of constraints that produce that erased constraint. These sets of constraints now form the constraint cliques.

In the case you provided, two cliques would be made:

1. &'static (): <SOME DUMMY PLACEHOLDER>, which corresponds to &'static (): var
2. &<SOME DUMMY PLACEHOLDER>: 'static, which corresponds to &'var (): 'static
   This clique information is passed into the solver, so the solver will not attempt to merge these two constraints.

My apologies if this was poorly explained in the comments (or is poorly explained now 😅). I'll put in better documentation for this part later today.

[bors]

☔ The latest upstream changes (presumably #111473) made this pull request unmergeable. Please resolve the merge conflicts.

[wesleywiser]

Hi @lcnr, just letting you know that this PR has been updated. I think it's ready for review whenever you have a chance. Thanks! 🙂

[lcnr]

closing this for now as I hope the pattern fixed here does not occur in actual code so it adds complexity to the solver. I am still thankful to @ndrewxie for working on this and chatting about it on zulip, as this provided me with a far better understanding of what's going on here and also uncovered a bigger issue of our overflow handling.