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

Existential Capabilities #20566

Merged
merged 61 commits into from
Jul 19, 2024
Merged

Existential Capabilities #20566

merged 61 commits into from
Jul 19, 2024

Commits on Jul 17, 2024

  1. More robust level handling

    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    0e71645 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    5b9d305 View commit details
    Browse the repository at this point in the history
  3. Generalize isAlwaysEmpty and streamline isBoxedCaptured

     - isBoxedCaptured no longer requires the construction of intermediate capture sets.
     - isAlwaysEmpty is also true for solved variables that have no elements
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    b375d97 View commit details
    Browse the repository at this point in the history
  4. Refine class refinements

     - Use a uniform criterion when to add them
     - Don't add them for @constructorOnly or @cc.untrackedCaptures arguments
    
    @untrackedCaptures is a new annotation
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    f9ddc71 View commit details
    Browse the repository at this point in the history
  5. Improve handling of no-cap-under-box/unbox errors

     - Improve error messages
     - Better propagation of @uncheckedCaptures
     - -un-deprecacte caps.unsafeUnbox and friends.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    0458012 View commit details
    Browse the repository at this point in the history
  6. Go back to original no cap in box/unbox restrictions

    We go back to the original lifetime restriction that box/unbox cannot
    apply to universal capture sets, and drop the later restriction that
    type variable instantiations may not deeply capture cap.
    
    The original restriction is proven to be sound and is probably expressive
    enough when we add reach capabilities.
    
    This required some changes in tests and also in the standard library.
    
    The original restriction is in place for source <= 3.2 and >= 3.5. Source
    3.3 and 3.4 use the alternative restriction on type variable instances.
    
    Some neg tests have not been brought forward to 3.4. They are all in
    tests/neg-customargs/captures and start with
    
    //> using options -source 3.4
    
    We need to look at these tests one-by-one and analyze whether the new 3.5 behavior
    is correct.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    24506ae View commit details
    Browse the repository at this point in the history
  7. More robust scheme to re-check definitions once.

    The previous scheme relied on subtle and unstated assumptions between
    symbol updates and re-checking. If they were violated some definitions
    could not be rechecked at all. The new scheme is more robust. We always
    re-check except when the checker implementation returns true for `skipRecheck`.
    And that test is based on an explicitly maintained set of completed symbols.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    1008a0d View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    a30cf47 View commit details
    Browse the repository at this point in the history
  9. Enable existential capabilities

    Enabled from 3.5.
    
    There are still a number of open questions
    
     - Clarify type inference with existentials propagating into capture sets.
       Right now, no pos or run test exercises this.
     - Also map arguments of function to existentials (at least double flip ones).
     - Adapt reach capabilities and drop previous restrictions.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    20b8630 View commit details
    Browse the repository at this point in the history
  10. Tighten rules against escaping local references

    Fixes the problem in effect-swaps.scala
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    ca715e8 View commit details
    Browse the repository at this point in the history
  11. Go back to expansion of capability class references at Setup

    This gives us the necessary levers to switch to existential capabilities.
    
    # Conflicts:
    #	compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    b9c2109 View commit details
    Browse the repository at this point in the history
  12. Drop expandedUniversalSet

    An expandedUniversalSet was the same as `{cap}` but not reference-equal
    to CaptureSet.universal. This construct was previously needed to avoid
    multiple expansions, but this does not seem to be the case any longer so
    the construct can be dropped.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    420f2cd View commit details
    Browse the repository at this point in the history
  13. Configuration menu
    Copy the full SHA
    e9474ff View commit details
    Browse the repository at this point in the history
  14. Map capability classes to existentials

    # Conflicts:
    #	compiler/src/dotty/tools/dotc/cc/Setup.scala
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    0161bb0 View commit details
    Browse the repository at this point in the history
  15. Change encoding of impure dependent function types

    The encoding of (x: T) => U in capture checked code has changed.
    
    Previously: T => U' { def apply(x: T): U }
    Now: (T -> U' { def apply(x: T): U })^{cap}
    
    We often handle dependent functions by transforming the apply method and then mapping
    back to a function type using `.toFunctionType`. But that would always generate a
    pure function, so the impurity info could get lost.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    7296b40 View commit details
    Browse the repository at this point in the history
  16. Fix mapping of cap to existentials

    Still missing: Mapping parameters
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    4add745 View commit details
    Browse the repository at this point in the history
  17. Let only value types derive from Capabilities

    Fixes crash with opaque types reported by @natsukagami
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    d5c15dd View commit details
    Browse the repository at this point in the history
  18. Type inference for existentials

     - Add existentials to inferred types
     - Map existentials in one compared type to existentials in the other
     - Also: Don't re-analyze existentials in mapCap.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    d242e01 View commit details
    Browse the repository at this point in the history
  19. Configuration menu
    Copy the full SHA
    687516e View commit details
    Browse the repository at this point in the history
  20. Configuration menu
    Copy the full SHA
    9b27b69 View commit details
    Browse the repository at this point in the history
  21. Configuration menu
    Copy the full SHA
    1d3ae88 View commit details
    Browse the repository at this point in the history
  22. Fix existential mapping of non-dependent impure function aliases =>

    There was a forgotten case.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    4ad9e3c View commit details
    Browse the repository at this point in the history
  23. Drop restrictions in widenReachCaptures

    These should be no longer necessary with existentials.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    b950c7d View commit details
    Browse the repository at this point in the history
  24. Cleanup ccConfig settings

    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    adfb700 View commit details
    Browse the repository at this point in the history
  25. Configuration menu
    Copy the full SHA
    7bf8be7 View commit details
    Browse the repository at this point in the history
  26. Refine parameter accessors that have nonempty deep capture sets

    A parameter accessor with a nonempty deep capture set needs to be tracked in refinements
    even if it is pure, as long as it might contain captures that can be referenced using
    a reach capability.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    cd78a9e View commit details
    Browse the repository at this point in the history
  27. More precise capture set unions

    When we take `{elem} <: B ++ C` where `elem` is not yet included in `B ++ C`,
    B is a constant and C is a variable, propagate with `{elem} <: C`.
    Likewise if C is a constant and B is a variable.
    
    This tries to minimize the slack between a union and its operands.
    
    Note: Propagation does not happen very often in our test suite so far: Once in pos tests and
    15 times in scala2-library-cc.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    28f4bb5 View commit details
    Browse the repository at this point in the history
  28. Configuration menu
    Copy the full SHA
    04aa63d View commit details
    Browse the repository at this point in the history
  29. Reclassify maximal capabilities

    Don't treat user-defined capabilities deriving from caps.Capability as
    maximal. That was a vestige from when we treated capability classes natively.
    It caused code that should compile to fail because if `x extends Capability` then
    `x` could not be widened to `x*`.
    
    As a consequence we have one missed error in effect-swaps again, which re-establishes
    the original (faulty) situation.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    9436f11 View commit details
    Browse the repository at this point in the history
  30. Bring back RefiningVar

    We might want to treat it specially since a RefiningVar should ideally be closed for
    further additions when the constructor has been analyzed.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    7ac94c9 View commit details
    Browse the repository at this point in the history
  31. Configuration menu
    Copy the full SHA
    aad3395 View commit details
    Browse the repository at this point in the history
  32. Improve printing of capture sets before cc

    Use the syntactic sugar instead of expanding with capsOf
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    1c11071 View commit details
    Browse the repository at this point in the history
  33. Add some neg tests

    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    72462a7 View commit details
    Browse the repository at this point in the history
  34. Update doc page

    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    0a1854d View commit details
    Browse the repository at this point in the history
  35. Configuration menu
    Copy the full SHA
    c965322 View commit details
    Browse the repository at this point in the history
  36. Add option to avoid intersections for class refinements

    Add an option to avoid the type intersection when we do a select of a parameter
    accessor that is mentioned in a class refinement type. It seems to give us a little
    bit if performance, but nothing significant. So the option is off by default.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    2cd685a View commit details
    Browse the repository at this point in the history
  37. Configuration menu
    Copy the full SHA
    8b03405 View commit details
    Browse the repository at this point in the history
  38. Introduced @unboxed parameters

    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    520100b View commit details
    Browse the repository at this point in the history
  39. Configuration menu
    Copy the full SHA
    7708276 View commit details
    Browse the repository at this point in the history
  40. Configuration menu
    Copy the full SHA
    2b04423 View commit details
    Browse the repository at this point in the history
  41. Configuration menu
    Copy the full SHA
    074be82 View commit details
    Browse the repository at this point in the history
  42. Configuration menu
    Copy the full SHA
    1640340 View commit details
    Browse the repository at this point in the history
  43. Fix isAlwaysPure

    The condition on capturing types did not make sense. In a type T^{} with an empty capture set
    `T` can still be a type variable that's instantiated to a type with a capture set. Instead,
    T^cs is always pure if T is always pure. For instance `List[T]^{p}` is always pure. That's
    important in the context of the standard library, where such a type usually results from
    an instantiation of a type variable such as `C[T]^{p}`.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    4333d3e View commit details
    Browse the repository at this point in the history
  44. Fix special capture set handling in recheckApply, Step 1

    Step1: refactor
    
    The logic was querying the original types of trees, but we want the rechecked types instead.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    90749ea View commit details
    Browse the repository at this point in the history
  45. Fix special capture set handling in recheckApply, Step 2

    Step 2: Change the logic. The previous one was unsound. The new logic is a bot too
    conservative. I left comments in tests where it could be improved.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    bc818a9 View commit details
    Browse the repository at this point in the history
  46. Refactor CaptureRef operations

    Make all operations final methods on Type or CaptureRef
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    bb94805 View commit details
    Browse the repository at this point in the history
  47. Break out CaptureRef into a separate file

    Move extension methods on CaptureRef into CaptureRef itself or into CaptureOps
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    cc95088 View commit details
    Browse the repository at this point in the history
  48. Don't box arguments of any form of type cast or test

    Previously, only asInstanceOf was excluded.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    3667ab8 View commit details
    Browse the repository at this point in the history
  49. Revert "Fix special capture set handling in recheckApply, Step 2"

    This reverts commit f1f5a05.
    
    # Conflicts:
    #	compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    d8ace30 View commit details
    Browse the repository at this point in the history
  50. Fix special capture set handling in recheckApply, Step 2 revised

    Step 2: Change the logic. The previous one was unsound. The new logic is makes use of the
    distinction between regular and unboxed parameters.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    7db1d43 View commit details
    Browse the repository at this point in the history
  51. Fix captureSet computations for false reach capabilities

    Fix the capture set computation of a type T @reachCapability where T
    is not a singleton captureRef. Such types can be the results of typemaps.
    The capture set in this case should be the deep capture set of T.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    c1036bf View commit details
    Browse the repository at this point in the history
  52. Configuration menu
    Copy the full SHA
    5a35160 View commit details
    Browse the repository at this point in the history
  53. Make the unboxed parameter scheme standard

    Drop the config option that enables it.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    082214e View commit details
    Browse the repository at this point in the history
  54. Rename @unboxed --> @unbox

    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    afcbdcb View commit details
    Browse the repository at this point in the history
  55. Another test

    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    0b22948 View commit details
    Browse the repository at this point in the history
  56. Configuration menu
    Copy the full SHA
    91cbca8 View commit details
    Browse the repository at this point in the history
  57. Fix lubs over capturing types

    Also, fix Seq rechecking so that elements are always box adapted
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    54828c7 View commit details
    Browse the repository at this point in the history
  58. Don't do post checks in inlined code

    Capability references in inlined code might end up not being tracked or being redundant.
    Don't flag this as an error.
    odersky committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    c8d418a View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2024

  1. Configuration menu
    Copy the full SHA
    04dba38 View commit details
    Browse the repository at this point in the history
  2. Give some explanation if a capture set was under-approximated

    Give some explanation if an empty capture set was the result of an under-approximation.
    odersky committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    9391b9a View commit details
    Browse the repository at this point in the history
  3. Split postcheck phase in two

    Perform bounds checking before checking self types. Checking self types interpolates them,
    which may give an upper approximation solution that failes subsequent bounds checks. On the
    other hand, well-formedness checkimng should come after self types checking since otherwise
    we get spurious "has empty capture set, cannot be tracked" messages.
    odersky committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    fac643a View commit details
    Browse the repository at this point in the history