revamp region constraints

[nikomatsakis]

The current region constraints aren't quite expressive enough and have some flaws. After chatting some with @aturon, the current plan is to shoot for the following structure. First off, chalk is implementing a function Solve that has roughly this structure:

Solve(Env, Goal) = LifetimeGoal

a successful result is meant to imply that (in purely logical terms):

Env, LifetimeGoal |- Goal

This should always be achievable, since in the limit we can make LifetimeGoal be false. Note that we have to be careful around "negation-as-failure" style negative reasoning here, but factoring out the imprecison into LifetimeGoal actually helps.

What is the grammar then of our LifetimeGoal? I want to first lay out the complete grammar. I think then we can imagine an approximation function approx(LG) = LG' that e.g. eliminates disjunctions:

LG = for<'a...'z> LG
   | exists<'a...'z> LG
   | if(LC) LG
   | LG, LG
   | LG; LG
   | LA
LC = LC, LC
   | for<'a...'z> LC
   | if(LG) LC
   | LA
LA = 'a: 'b
   | 'a = 'b // clearly not a fundamental goal but convenient

In some cases, when doing unification, we'll need to generate new region variables at outer scopes. Some examples:

exists<A> for<'l> A = &'l T

The idea was to transform this by first introducing a variable 'x in same universe as A:

exists<'x> exists<A> for<'l> A = &'l T

then saying that A = &'x T with the resulting goal of:

for<'l> 'x = 'l

More generally, we could capture whatever environment is "in scope" and insert it into the goal. This seems to imply that we need (for the lifetime clauses) as rich a grammar as our environment supports.

Next example:

for<'a> exists<T> for<'b> if('a = 'b) T = &'b i32

To resolve this, we would introduce an existential in the same universe as T:

for<'a> exists<'x> exists<T> for<'b> if('a = 'b) T = &'b i32

which then allows us to say that T = &'x i32 with the (ultimately) lifetime goal:

for<'a> exists<'x> for<'b> if('a = 'b) 'b = 'x