trait solver: Handle reflexive region constraints

[Dnreikronos]

Fixes rust-lang/project-assumptions-on-binders#19

A reflexive placeholder constraint like 'a: 'a can show up after we compute transitive region constraints. We then try to pull it out of the current universe by looking for lower-universe candidates. With none to choose from it becomes false, even though 'a: 'a was true the whole time.

I first had this buried in the binder region work, which made a green test pretty meaningless because too much else was changing around it. Split out on its own, the fix is just to accept equal regions before doing the universe rewrite. I think that is the sensible place to stop: it handles the direct case and the reflexive edges made by the transitive pass. I added a regression for the direct case.

cc/ @BoxyUwU o/

[rustbot]

r? @JohnTitor

rustbot has assigned @JohnTitor.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

Why was this reviewer chosen?

The reviewer was selected based on:

• Owners of files modified in this PR: compiler
• compiler expanded to 75 candidates
• Random selection from 21 candidates

[Dnreikronos]

Sup @BoxyUwU and @adwinwhite o/
I noticed #161963 has the same reflexive check as the first commit in this PR, so that part overlaps. I pushed a few more changes here because I don't think that check covers the whole problem in rust-lang/project-assumptions-on-binders#19.

The first check handles 'a: 'a while we're leaving the placeholder's universe. That check is still right, it just fires too early for the other case I was looking at. In the small syn repro, the type outlives constraint only gets taken apart once we're back at the root, so the earlier check never sees the reflexive region constraint.

When I followed that path, some information was missing from the assumptions used at the root. The implied I: '_ from &'_ self was in region_bound_pairs, but it wasn't included when we destructured the solver constraints. An assumption such as &'b u8: 'a also didn't always give this code the 'b: 'a relation.

There's a similar problem while leaving a binder. If the binder's own assumptions already prove 'b: 'a, we still try to rewrite it into a lower universe. When there are no lower-universe candidates, that turns a true constraint into Or([]). The new code checks whether the assumptions already prove it before doing that rewrite.

At the root, a RegionOutlives('a, 'a) produced by destructuring is now treated as true too. That's the part that gets the syn minimization through.

I added tests for direct and transitive assumptions, type outlives assumptions, and the root case. The full assumptions_on_binders UI directory passes locally, 17 tests, and tidy passes too. I haven't tested every affected case listed in #19 yet, so I don't want to claim more than I've checked.

My take is that #161963 is a good small fix for #161733, while this PR now deals with the wider path behind #19. I would keep the extra work here, but I'm not sure where you want the PR boundary. Would you rather keep it this way or move the extra changes to a follow-up on #161963?