Add lifetime outlives goal

[jackh726]

c.c. #435

I'm not sure if this is exactly the approach we want to take here, but I figured I would open this for comments at least

[nikomatsakis]

So... what I did in my other branch was similar to this, but with one difference. There was a 'meta goal' like

AddRegionConstraint('a, 'b)

that part of the Goal enum. In the simplify logic, this goal is simply converted to a region constraint and (for now) always provable. Then we can have

Outlives('a, 'b) :- AddRegionConstraint('a, 'b)

This feels like a more elegant setup to me than what's in the PR, in that it adds a kind of "special meta goal" but otherwise leaves things untouched. I also converted unification so that it never produces region constraints but instead only adds new subgoals.

The next step, which I didn't yet take, would be to (a) only apply AddRegionConstraint for things in the root universe (perhaps it fails for lifetimes in other universes, for example) and (b) have some other rules for handling outlives for higher-ranked things (this is what I was in the midst of exploring when I realized that, to encode the rules the way I wanted, we needed the semantic-vs-synctactic equality split).

[jackh726]

@nikomatsakis Okay so I rebased this to master. But I'm a little unsure how to continue here.

1. The AddRegionConstraint goal isn't really possible to do now that chalk-engine uses Goal directly. I removed the special handling in resolvent, so now we only add constriants in simplify, which more closely matches your branch.
2. I looked at your branch in regards to having unification add goals instead of constraints. This doesn't quite fit into the current scheme since there's no translation there of Outlives -> AddRegionConstraint.
3. Can you elaborate on your last point? (applying AddRegionConstraint for things in the root universe, and higher-ranked things) Maybe a test case?

[nikomatsakis]

ah I guess that's why you have slg here

[nikomatsakis]

@jackh726

So, I think that your current branch is effectively "hard-coding" the AddRegionConstraint logic in some sense, by baking it into the "simplification" logic for handling domain goals (rather than adding a special sort of goal that is baked in, and then "converting" to that via a standard program clause).

I don't quite understand your point about having refactored the resolvent special handling, and I don't quite understand what you mean about not being able to modify unification, but I can maybe try to do the thing I was talking about and see what happens.

I think I still prefer to have a special goal like AddRegionConstraint (or maybe a built-in notion of Outlives) so that the solver never tries to "bake in" what a domain-goal means, but it's not a really big difference.

As for the interaction with higher-ranked, let's shelve it for now, I don't think it's relevant to this PR yet.