Prevent opaque types being instantiated twice with different regions within the same function by oli-obk · Pull Request #116935 · rust-lang/rust (original) (raw)
Let me break down this list:
- Is sound
There's lots of sound code that doesn't work in the old trait solver or the new trait solver.
Especially when it comes to things that are equal modulo regions, we already have a lot of limitations when it comes to the trait solver distinguishing choices (e.g. where
clauses), because the trait solver fundamentally is not built to distinguish lifetimes.
- Is reasonable, plausibly could have real-world application
I haven't seen any examples of code that rely on this property. I agree that it's plausible, but it's clear that our guestimates of the probability of this being an issue that is hit in practice differ.
My understanding from discussing this briefly with @oli-obk is that he only wrote the tests that exercise this behavior because they could work, not because they were motivated by any real-life examples (though I may be misremembering, so any paraphrasing is my own).
- Intuitively "should work"
Again, lots of things that intuitively should work don't due to real, concrete limitations to the compiler, especially ones that enable other code to work, and for the trait solver to be sound. I go into more detail below, but this limitation exists to make space for lazy normalization and region uniquification.
- Has no obvious work-around
You can use type or const parameters to work around this, but again, a fix would likely be motivated by first understanding what is trying to be achieved at a high level.
- Works with the old trait solver
The purpose of this limitation being put in place is precisely to level out the differences between the new trait solver and the old trait solver. See below.
- And there's apparently no hope of ever making it work again, ever?
We are not technically committing to this behavior until the new trait solver lands, but yes, I don't think there's a way to make this work soundly in a language that doesn't do borrow-checking in tandem with type-checking.
Hopefully at the point of stabilization of the new solver, we will be able to more precisely motivate the reasons why the trait solver requires this to work the way it does. but TL;DR is "lazy normalization" and "region uniquification". The former is a property that we need to have to make the trait solver sound, and the latter is one that gives us better caching and is a requirement to make the trait solver work properly between typeck and borrowck.
The side-effect of this limitation is that we can treat defining instantiations of TAITs as being defined anywhere in the body. For example (https://godbolt.org/z/v9GjnP769) (though don't go trying it with region args yet, that still fails due to bugs with aliases in the new trait solver).