Refactor LifetimeOutlives goals to produce AddRegionConstraint subgoals

[nathanwhit]

This PR implements the suggestion described in this comment, modulo the "next steps" described.

I'm not sure if this is ultimately the approach we want to take, but this at least allows for simplification of the unifier and reduces the amount of hard-coded DomainGoal logic in the solver.

Closes #508.

[jackh726]

This looks good to me. A lot cleaner overall. I'm wondering if it's still worth experimenting with having program_clauses return constraints too. (One other solution we talked about).

Can you check if there are any relevant docs in the book that need to be updated?

[nikomatsakis]

Sorry, I meant to comment on this PR -- I was also wondering about the idea of having the ProgramClause structure have an associated set of region constraints, such that we can have the chalk-solve logic handle this basically. I kind of like that approach, it avoids adding a "special goal" and concentrates the logic in chalk-solve. It's a bit of a larger refactoring though.

@nathanwhit did you see that proposal and does it make sense to you? (i.e., do you understand what we're proposing)

[nathanwhit]

@jackh726 Updated the chalk book to reflect this PR (there was really only one section that needed changing).

[jackh726]

So, I'm mostly okay with merging this as-is. But I do agree with @nikomatsakis that I would like to see to chalk-solve handle the constraints. But this is better than master atm. So I wouldn't say this closes #508.

@nikomatsakis okay with you to merge this without closing #508?

[nathanwhit]

Sorry, I meant to comment on this PR -- I was also wondering about the idea of having the ProgramClause structure have an associated set of region constraints, such that we can have the chalk-solve logic handle this basically. I kind of like that approach, it avoids adding a "special goal" and concentrates the logic in chalk-solve. It's a bit of a larger refactoring though.

@nathanwhit did you see that proposal and does it make sense to you? (i.e., do you understand what we're proposing)

So I've read through the discussion on zulip a few times, and I understand the proposal in broad strokes but I'm a bit unsure of the details. The main point I'm unclear on is whether the proposal is to:

• associate each ProgramClause with a set of constraints (i.e. change the ProgramClauseImplication struct to add constraints)
• associate a set of program clauses with a set of constraints (i.e. generally return a set of program clauses and a set of constraints in places we currently just return program clauses)
• do something else entirely

[jackh726]

I think in my mind, I was originally imagining that chalk-solve would give a set of program clauses, and a set of region constraints but it's a little bit of an experiment, so if it makes more sense have each ProgramClause have a (set of) region contraints, that might be okay too.

[nikomatsakis]

I think the best thing would be to make ProgramClauseImplication include region constraints. If we were going to formalize the chalk solver (and I would like to do so, actually, once we kind of settle whether it would be the recursive solver or what), then I think this is also the approach I would take there.

Basically our formulation is that we have a program clause of the form

P :- Q1..Qn; R1..Rn

where Q1..Qn are subgoals that must be proven and R1..Rn are region constraints that must be recorded and given back to the solver to be solved later.

[jackh726]

The only downside I think with having the region constraints be a part of ProgramClauseImplication is then we have an extra Vec (or interned) of values for every one created. Even though most are going to be empty.

[nikomatsakis]

@jackh726 right, most are empty, so I figured that this code is minimal (a few bytes). Still, maybe an issue for performance at some point.

[jackh726]

So, I'm mostly okay with merging this as-is. But I do agree with @nikomatsakis that I would like to see to chalk-solve handle the constraints. But this is better than master atm. So I wouldn't say this closes #508.

@nikomatsakis okay with you to merge this without closing #508?

@nikomatsakis not sure if you saw this