`-Zassumptions-on-binders=min_coroutines`

[BoxyUwU]

the general idea here is a minimal form of assumptions on binders which:

• Only has assumptions for the binder around coroutine witness types
• Doesn't rewrite constraints involving placeholders to be constraints involving smaller universe variables

this avoids a lot of the complexity with the full assumptions on binders design and avoids soundness issues from assuming more things without them ever being proven.

getting a first version of this flag will require:

• checking which version of abby is enabled when entering binders and changing behaviour for the binder when entering witness types only
• fix up a bunch of the asserts in the eagerly_handle_placeholders logic to no longer assert things about what universe things are (when min_coroutines is in use) as we now won't be fully eagerly handling placeholders in all -Zassumptions-on-binders variants
• drop pretty much all of the rewrite rules when using min_coroutines. we want to drop constraints if they hold, and otherwise keep them unchanged and propagated to the root.
• dont destructure type outlives constraints into their constituent parts eagerly (cc eagerly destructing type outlives constraints? #23). I'm not sure if this is actually necessary for this to be a useful feature or not. If it isn't then I want to avoid doing this to keep min_coroutines as small as possible. If it does wind up being necessary it can be done we can re-enable it in the future and after we've added support for VisibleForLeakCheck (cc support VisibleForLeakCheck #30)

this issue doesn't cover all of the stuff needed for stabilization of this flag, just what the initial implementation will need to be

[Dnreikronos]

@BoxyUwU o/
I will work on this!

[Dnreikronos]

Sup Boxy o/

Quick status thing since this has been sitting a while.

Bullets 1 and 4 are done and in rust-lang/rust#162159. Witness binders are the only ones getting assumptions, and type outlives constraints stay whole instead of getting destructured.

2 and 3 aren't. Didn't properly clock that until after your review round, which, yeah, should've spotted it earlier.

3 is the one that actually bites. Dropping the rewrite rules only kicks in for binders that have assumptions, and in this mode that's witness binders, nothing else. Everything else gets None, falls through to the normal path and pops out as ambiguity instead of being kept and handed to the root. Net result is ordinary higher ranked bounds get rejected here while stable and full abby both take them fine. There's an example on the PR.

Fix is probably just handing non-witness binders Some(empty) instead of None. Then every universe has assumptions, the early return always fires, and the whole eager rewrite path is dead in this mode. Which would sort bullet 2 for free too, since the universe asserts all live in that path. Big if though. I've only read the code, haven't tried it.

Where I keep going back and forth is the order. Right now an ordinary leak fails as NoSolution in the solver. Defer it to the root instead, and if the root doesn't always get to see it, we've traded an error for silence. There's a case on the PR where constraints registered inside a type op query just never reach borrowck, which is basically the thing you suspected on #18. So I'd want that fixed first, or bullet 3 makes it worse instead of better.

Anyway...happy to pick up 2 and 3 as a follow up once the PR settles, shout if you'd rather they go in it.