The current region inference scheme has some known limitations. Many of these were uncovered and discussed as part of the work on RFC 1214. There have also been a number of recent regressions that are tangentially, at least, related to the way region inference currently works. At its worst, the shortcomings in region inference can lead to nondeterministic errors, where doing small things like adding redundant parentheses can cause or solve type inference failures. Yuck. This post covers a smattering of thoughts on the topic.
Nondeterminism and lifetime parameters
Problem
The current region system allows a region to be inferred to one of:
- a scope or expression
- a named lifetime parameter (
'a) 'static- a special empty region that has no corresponding syntax
To a first approximation, it works by starting region variables small and growing them in response to constraints. It assumes that there is a “least upper bound” operation that can be applied to any two regions to yield something sensible. When it was written, this was basically true, but in the meantime lifetime parameters have gotten a lot more complex. Now we have things like:
where 'b: 'a,
'b: 'c,
'd: 'a,
'd: 'c,
now what is the LUB('a, 'c)? Basically, there is no single answer:
both 'b and 'd are greater than both 'a and 'c, but neither
'b: 'd nor 'd: 'b holds. Right now, we pick something conservative
('static, in fact), but this is not great, because the order in
which we process constraints can affect the final solution.
For example, imagine three constraints:
'a <= $0'c <= $0'b <= $0
If we process these in order, we’ll first grow $0 to 'a and then
to 'static, where it remains. But if we process in the order 1, 3,
2, we get a different result. We first grow to 'a and then to 'b,
where $0 remains. Double yuck!
Proposed solution
Allow region variables to be inferred to the intersection of a list of
named lifetime parameters. So the result of LUB('a, 'c), in the
previous example, would be {'b & 'd}, instead of 'static. If you
work this through, you’ll see that the order of processing constraints
no longer matters.
The LUB operation on two sets of named lifetime parameters X and Y can be defined roughly by:
concat([forall i, j. UBS(X[i], Y[j]))
where UBS yields the set of disjoint upper-bounds (so, e.g.,
UBS('a, 'c) = ['b, 'd]). (This UBS operation is already implemented,
see the method minimal_upper_bounds on transitive_relation.)
Adopt a pure dataflow solution; impoverished constraint language
Problem
The regionck constraint model consists of a set of
constraints of the form R1 <= R2, all of which must hold:
C = R <= R
| AND(C, C)
But, as discussed in RFC 1214, if you want to handle projections, you really need the ability to have “OR” constraints. Similar problems arise from where-clauses and a few other sources.
When solving this constraint set, the region inference algorithm also classifies nodes as “expanding” or “contracting” based upon what kinds of incoming edges they have. This is sort of a holdover from the days before there was an empty region. It is also problematic because it means we can’t incrementally solve region constraints at all: we have to wait until all constraints are known so that we can do these classifications.
This contraction mode means that if you have a variable with only
upper bounds, like a single constraint $0 <= X, we will infer $0
to X. Since this represents a maximal solution, it can be useful for
uncovering missing lower bounds, since often a solution of X is too
large (for example, the missing constraint #29006 was uncovered by
such an error). nut the contraction mode also causes some difficulties
(e.g., changing this behavior happens to fix #29048).
Solution
Extend constraint language to include OR:
C = R <= R
| AND(C, C)
| OR(C, C)
Of course, this has a big impact on how the code works. Basically, the idea would be that we have to exhaustively explore the options. Luckily, we mostly generate a pretty flat tree, so we ought to be able to do a strategy like:
- At any given level, gather up all the
R <= Rconstraints that are reachable without going through anORnode. - Solve those using data-flow, to find minimal regions. Call this interim solution X.
- Explore the required
ORconstraints, starting from X. For each constraint, at least one of the sides must hold. Note that there are a lot of possible combinations here. We certainly want to at minimum continue distingushing “verifies”, where inference is not affected.
Note that at any given level I have implicitly adopted a pure dataflow model, where all variables start as empty and strictly grow. (We can also grow the root level incrementally, which may allow us to make some progress on problems like #21974, but there are also more complications in that general area.)
We will lose the “bug-finding” behavior of the current algorithm. This is, however, not a reliable way to uncovering bugs, so I’m not sure that’s a great loss. Instead, I think we should just focus on doing type-checking on the MIR as a kind of “double check” for inference. In fact, I’d like to move all region checking to the MIR, as I discuss in the next section.
More principled treatment of regions in closures, non-lexical lifetimes, etc
This is not a real solution yet, more of a general direction. The current typeck code feels overly complex, and it has a lot of trouble squaring the type inference we need around closures with the region hierarchy that closures ought to have. In particular, closures are distinct functions, and so should have a distinct region hierarchy, but we have to type check them altogether to get better inference for local variables and the like.
In my ideal world, we’d address this by having typeck not handle
regions at all, instead substituting some kind of dummy region (let’s
call it 'dummy) everywhere (though we will have to track where
region bindings occur as well). We’d then build up the MIR, which will
have all regions just using 'dummy initially.
We’d then re-run a full type-check on the MIR. This will be relatively easy because the MIR is very simple. In this later pass, we will also replace regions with inference variables, and construct a proper graph. This should let us treat closures as completely distinct fns, like we want to. It also makes it easy to move to non-lexical lifetimes. (This doesn’t really solve #21974 yet, since we’ll still have to be doing trait selection.)
All done.
Thanks for listening.