Drop @capability annotations #20396

A maximal capability is one that derives from `caps.Cap`. Also: drop the given caps.Cap. It's not clear why there needs to be a given for it.

The current handling of class type refinements is unsound. We cannot simply use a variable for the capture set of a class argument. What we need to do instead is treat class arguments as tracked. In this commit we at least allow explicitly declared tracked arguments. This needed two modifications: - Don't additionally add a capture set for tracked arguments - Handle the case where a capture reference is of a singleton type which is another capture reference. As a next step we should treat all class arguments as implicitly tracked.

Replace with references that inherit trait `Capability`.

Drop convention that classes inheriting from universal capturing types are capability classes. Capture sets of parents are instead ignored. The convention led to algebraic anomalies. For instance if class C extends A => B, Serializable then C <: (A => B) & Serializable, which has an empty capture set. Yet we treat every occurrence of C as implicitly carrying `cap`.

Only enrich classes with capture refinements for a parameter if the deep capture set of the parameter's type is nonempty.

… adaptation This change lets more ref trees with underlying function types keep their singleton types.

- Avoid creating capture sets of untrackable references - Refine disallowRootCapability to consider only explicit captures

When an expression has a type that derives from caps.Capability, add an explicit capture set. Also: Address other review comments

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Drop @capability annotations #20396

Drop @capability annotations #20396

Commits on May 27, 2024