Open compiler-errors opened 11 months ago
I see a few solutions for this problem:
Typeck's infcx stores a list of generator witness def-ids it must stall. This should be trivial to compute from the HIR. This is canonicalized as part of the goal (like opaque type storage) and we force any nested goals to be ambiguous if we encounter one of these witnesses.
We don't normalize during writeback. This seems problematic when it comes to modifying the rest of the compiler.
We use the defining anchor + reveal to stall any generator witnesses that we can determine are local to the body we're typecking. This seems problematic because check_coroutine_obligations
also runs in a user-facing reveal mode, so I don't know how to distinguish typeck from post-typeck here...
my initial vibe is to normalize in writeback before instantiating the witness infer var and accept ambiguous obligations in deeply_normalize
as long as the normalized-to type is not ambiguous, returning these nested obligations. This is a bit annoying to implement as we need to restructure the code a bit, but I expect that to be the easiest and "cleanest" solution.
my initial vibe is to normalize in writeback before instantiating the witness infer var and accept ambiguous obligations in deeply_normalize as long as the normalized-to type is not ambiguous, returning these nested obligations.
This concerns me a bit, since we're now breaking two invariants in both deeply normalize and writeback:
The fact that we stall obligations on an infer var and draining them feels ad-hoc, and it suggests to me that the solver should be taught about this generator witness stalling first-class, the same way it knows about opaques in a first-class way.
writeback shouldn't encounter infer vars, which are ambiguity errors.
It still shouldn't, it would be: deeply-normalize -> instantiate-witness-infer -> writeback
deeply normalize should either normalize something, or it shouldn't, and if it does, then it shouldn't be ambiguous.
It is not ideal :thinking: for me the core invariant is that we don't leave some projection which can be later normalized. So erroring of the term infer var is unconstrained but accepting the projection goal itself to be ambig seems fine to me.
I guess this could cause issues if a wf project goal actually manages to result in constraints but later still does not hold. I think it's kind of an invariant that that doesn't happen once we cover impls using param env candidates. I think we currently have the defacto invariant: if a Projection
goal constrains the term, it either holds or the trait is not implemented, resulting in an error elsewhere.
The fact that we stall obligations on an infer var and draining them feels ad-hoc[..]
I agree that it is adhoc, however, given that hir typeck and mir build are separate queries, I personally think it's fairly clean. in a sense writeback is really just a deep structurally_resolve
needed by mir_build. That we require all obligations to be proven at that time is more or less incidental.
[..], and it suggests to me that the solver should be taught about this generator witness stalling first-class, the same way it knows about opaques in a first-class way.
I disagree quite strongly here. The witness being an infer var is the first-class way to tell the solver that it should stall.
it would be: deeply-normalize -> instantiate-witness-infer -> writeback
That seems really annoying to handle:
deeply_normalize
isn't equipped to return stalled ambiguous predicates (and every other call site doesn't care about them)TypeFoldable
, so we need to ad-hoc pass over every field like writeback doesdrain_unstalled_obligations
is just wrongThoughts:
analysis_in_body
) we don't need to.drain_unstalled_obligations
, we could implement a proof tree visitor to just drain the obligations that end up touching one of these generator def ids. We don't need to do that now, tho, but it allows us to emit "true ambiguities" properly rather than just draining all obligations lolMaking the typing mode larger is a bit concerning. Maybe we should put the opaques and the coroutines into the same list together?
We normalize types during writeback resolve: https://github.com/rust-lang/rust/blob/b6a8c762eed0ae0383658c38d65cb91bbd9800a1/compiler/rustc_hir_typeck/src/writeback.rs#L790-L794
When normalizing types, this may cause us to try to prove an auto trait bound on a generator witness that is local to the body: