introduce region-clauses into the ParamEnv
, use to replace the body_id
#42341
Labels
A-trait-system
Area: Trait system
C-cleanup
Category: PRs that clean code up or issues documenting cleanup.
T-compiler
Relevant to the compiler team, which will review and decide on the PR/issue.
When we are in a closure body, we often gain additional implied "outlives" relation based on the types of the closure arguments. Consider this:
Here, the type of
x
will be&'0 T
for some anonymous region'0
. Within the function body, then, we can conclude thatT: '0
. We currently handle this through a variety of messy schemes. As part of chalkificaton, I would like to consolidate this into a cleaner, more uniform handling of environments and universes. This issue lays out an "evolving" plan for doing that.Current handling
Currently, for every trait obligation that we have to prove (e.g.,
T: Debug
), we have anObligationCause
-- this is primarily used for debugging, in that it specifies why we have to prove this thing. However, this type also carries abody_id
identifying the closure it came from. When we wind up having to prove an outlives relationship likeFoo: 'a
, we record this in the fulfillment context (a kind of record of things we have yet to prove), and we track thebody_id
where the obligation was incurred. Then, after type-checking, in the region-checking phase, we walk down the AST and figure out -- for each closure body -- what outlives facts we know at that point in time. We then pull out the list of outlives obligations from the fulfillment cx for a given body-id and try to prove them, using those facts. This whole process is complex and fragile.Roughly how I want it to work
We now have the ability to have every obligation have its own, distinct environment (we used to have just one ambient environment). This means that instead of having this ad-hoc
body_id
field, we can just extend the environment when we enter into a closure body. So, for example, when type-checking the body of the closure in the beginning, our environment would be extended with aT: 'a
outlives clause. We can do this right away, just as soon as we start type-checking the closure. This environment is automatically propagated to sub-goals, so when we wind up with some outlives obligations that we have to prove, they will haveT: 'a
in their list of clauses (i.e., the facts that they can draw upon). This means that regionck doesn't have to do anything "special" -- rather, the input to regionck will change from being a flat list of obligations, to obligations that can carry more environmental information.There is one complication here:
Actual steps
OK, I ran out of time for this part. =)
The text was updated successfully, but these errors were encountered: