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

replace the leak check with universes, take 2 #65232

Merged
merged 10 commits into from
Feb 8, 2020

Commits on Feb 6, 2020

  1. Configuration menu
    Copy the full SHA
    82c1435 View commit details
    Browse the repository at this point in the history
  2. add a IsEmpty for use in verified bounds

    We currently have a kind of arbitrary check for `Verify` conditions
    which says that if the "test region" is `'empty`, then the check
    passes. This was added to fix rust-lang#42467 -- it happens to be correct for
    the purposes that we use verify bounds for, but it doesn't feel
    generally correct. Replace with a more principled test.
    nikomatsakis committed Feb 6, 2020
    Configuration menu
    Copy the full SHA
    65fc086 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    03b2fff View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    b52414f View commit details
    Browse the repository at this point in the history
  5. index ReEmpty by universe

    We now make `'empty` indexed by a universe index, resulting
    in a region lattice like this:
    
    ```
    static ----------+-----...------+       (greatest)
    |                |              |
    early-bound and  |              |
    free regions     |              |
    |                |              |
    scope regions    |              |
    |                |              |
    empty(root)   placeholder(U1)   |
    |            /                  |
    |           /         placeholder(Un)
    empty(U1) --         /
    |                   /
    ...                /
    |                 /
    empty(Un) --------                      (smallest)
    ```
    
    Therefore, `exists<A> { forall<B> { B: A } }` is now unprovable,
    because A must be at least Empty(U1) and B is placeholder(U2), and hence
    the two regions are unrelated.
    nikomatsakis committed Feb 6, 2020
    Configuration menu
    Copy the full SHA
    534f044 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    6bc79c9 View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    5e0197f View commit details
    Browse the repository at this point in the history
  8. add the ability to skip leak check within a snapshot

    The intention is that coherence code will skip the leak check and
    determine whether two impls *would have* overlapped, and then issue a
    warning.
    nikomatsakis committed Feb 6, 2020
    Configuration menu
    Copy the full SHA
    e9c7894 View commit details
    Browse the repository at this point in the history
  9. Configuration menu
    Copy the full SHA
    363faba View commit details
    Browse the repository at this point in the history
  10. Configuration menu
    Copy the full SHA
    4b3c66d View commit details
    Browse the repository at this point in the history