Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

region checking in intercrate mode #64

Open
lcnr opened this issue Sep 22, 2023 · 2 comments
Open

region checking in intercrate mode #64

lcnr opened this issue Sep 22, 2023 · 2 comments
Labels
A-coherence Having to do with regressions in `-Ztrait-solver=next-coherence`

Comments

@lcnr
Copy link
Contributor

lcnr commented Sep 22, 2023

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.

@lcnr lcnr added the A-coherence Having to do with regressions in `-Ztrait-solver=next-coherence` label Sep 22, 2023
@compiler-errors
Copy link
Member

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
Copy link
Contributor Author

lcnr commented Sep 22, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-coherence Having to do with regressions in `-Ztrait-solver=next-coherence`
Projects
None yet
Development

No branches or pull requests

2 participants