region checking in coherence mode

[lcnr]

the way we destructure TypeOutlives is incomplete, and probably some other parts of regionck as well.

We must not use resolve_regions in places which are required to be complete.

I previously used the invariant "during coherence mode we have to be complete", but rust-lang/rust#112875 uses resolve_regions and intercrate mode, so it breaks the invariant. Either the invariant is wrong and only "the implicit negative checks" require completeness, or that code is broken and we need to change it somehow.

[compiler-errors]

It seems pretty obvious to me that we don't need completeness in negative coherence -- if we incompletely consider type outlives obligations to fail when they can succeed via some other rule in rust-lang/rfcs#1214, our program will consider two impls to overlap, and we emit an error

...at least as long as we're doing region solving only at the "root obligation" level -- processing type obligations eagerly when checking if nested obligations hold would conceivably cause completeness problems.

[lcnr]

my current vibe here is:

• the explicit negative coherence searches for occurances of negated where bounds which hold, so it has to be sound
• the implicit negative coherence searches for occurances of where bounds which don't hold, so it has to be complete

HOWEVER:
Explicit negative coherence starts by equating the impl headers and then replacing inference vars with placeholders. This must be complete, as we'd otherwise could get into a position where we only have to prove u32: !Trait instead of the more general T: !Trait by incorrectly constraining inference vars. I don't know whether it has to be sound, probably not 🤷 it feels sus to not require soundness there however.

[lcnr]

i don't think there's anything actionable here, we may want to document something somewhere, but 🤷