Skip to content

Add restricted capabilities x.only[C] #23485

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.

Sign up for GitHub

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

Jump to bottom
Draft
wants to merge 7 commits into
base: main
Choose a base branch
from
Draft

Add restricted capabilities x.only[C] #23485

wants to merge 7 commits into from

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Jul 7, 2025 •
edited
Loading

Implementation along the lines of #23463

  • Syntax and parsing rules for only-capabilities.
  • A Classifier base trait.
  • Enforce restriction that a class cannot inherit two unrelated classified capability classes.
  • A new capability class for only-capabilities.
  • Implement captureSetOfInfo for only capabilities.
  • The empty capability is x.only[Nothing]. It should have empty captureSetOfInfo.
  • Well-formedness rules: only must refer to a classified capability class.
  • Normalization rules:
    - it's *, then .only, then .rd,
    - multiple .only normalize to the smallest one if the classes are related,
    - multiple .only normalize to the empty capability if the classes are not related.
  • define transitive capture set and cache it in a capability. The tcs does not exist if a capture set in the hierarchy is still an unsolved capture set variable.
  • Add a classifier field to FreshCap and ResultCap.
  • Modify capToFresh and toResultInResults so that the classifier field is correctly set.
  • Using tcs, define when a capability is classified by a classifier class.
  • A FreshCap with a classifier C can subsume only capabilities that are classified as C.
  • Implement subsumption rules:
    - c.as[C] <: d if c <: d or c.as[D] <: empty
    - c.as[C] <: d.as[D] if c <: d and C derives from D
    - c <: d.as[D] if c <: d and c is classified as D
    - c.as[D] <: empty if tcs(c) consists of capabilities that all derive from classifier classes unrelated to D.

prolativ
prolativ reviewed Jul 7, 2025
View reviewed changes
compiler/src/dotty/tools/dotc/cc/SepCheck.scala Outdated
@@ -597,7 +597,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
* - If the reference is to a this type of the enclosing class, the
* access must be in a @consume method.
*
* References that extend SharedCapability are excluded from checking.
* References that extend cpas.Sharable are excluded from checking.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
* References that extend cpas.Sharable are excluded from checking.
* References that extend caps.Sharable are excluded from checking.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

odersky added 5 commits July 7, 2025 16:50
@odersky
Introduce only-capabilities
7eae7e3 
Basic representations and definitions, so that we can parse only-capabilities,
convert them to internal representation `Restrict(c, cls)`, not crash on them during
capture checking and print them out correctly.
@odersky
Add showRef utility method
f845855
@odersky
Introduce capability classifiers
e1965f6
@odersky
Implement subsumption rules for restricted capabilities
4b69577
@odersky
Update MimaFilters
9719712
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@prolativ prolativ prolativ left review comments

At least 1 approving review is required to merge this pull request.

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@odersky @prolativ