defer reasoning about region relationships until after regionck #3238
Comments
ghost
assigned 
|
Interestingly, I realized today that fixing this bug also allows us to resolve some other thorny issues in defining the region system. In particular, we could solve #3696 in the ideal way---that is, we can wait to define the region hierarchy at all until just before regionck, when types are known. Another problem that would be solved is a bug related to the nested lifetime extension in closures---sometimes the full types of closure arguments are not known until the end, so we can't establish the relationships between their free regions. |
|
A condition for this bug is that the region relationships are written down in the manual. If it's written-down but not actually implemented-as-written, this can be moved to a backward-compatibility milestone. |
|
@nikomatsakis is this still valid? |
|
Absolutely. I'm about to submit a PR on it, actually, just blocked trying to write docs to clearly explain what's going on. |
This patch makes error handling for region inference failures more uniform by not reporting *any* region errors until the reigon inference step. This requires threading through more information about what caused a region constraint, so that we can still give informative error messages. I have only taken partial advantage of this information: when region inference fails, we still report the same error we always did, despite the fact that we now know precisely what caused the various constriants and what the region variable represents, which we did not know before. This change is required not only to improve error messages but because the region hierarchy is not in fact fully known until regionck, because it is not clear where closure bodies fit in (our current treatment is unsound). Moreover, the relationships between free variables cannot be fully determined until type inference is otherwise complete. cc rust-lang#3238.
We want to run the proofs in the target crate and don't need to build (or run) the proofs in any of the host crates. This avoids a need to make available the `kani` crate to any such host crates. Resolves rust-lang#3101, rust-lang#3238
Right now, if you try to relate two regions, you either get back an immediate error or---more likely---you generate a constraint that will later be processed by region inference. In the former case, the error message is generally clearler: this is because the error is reported by the code that is relating the regions, and it can say something more specific about why the relation came about. In the latter case, the inferencer is reporting the error, and all it really knows is something like "due to the code at this span, r1 should be a subregion of r2". So the message is correspondingly vague.
Instead of merely passing in a span to the inferencer, we should pass in something like ty::type_err(). Then the region inferencer could use this to report a more intelligent message about why the constraint which could not be satisfied came about. This would also mean that you get more consistent errors.
The text was updated successfully, but these errors were encountered: