Skip to content

Represent read-only with a classifier #24295

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

Merged
merged 4 commits into from
Nov 5, 2025
+31 −47
Merged

Represent read-only with a classifier #24295

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9abbb03
Represent read-only with a classifier
odersky Oct 25, 2025
0a0e666
Drop redundant matches against ReadOnly(...)
odersky Oct 28, 2025
67ba9b5
Drop redundant calls to stripReadOnly
odersky Oct 28, 2025
a5b4a51
Add testfile for #24334
Linyxus Nov 4, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 21 additions & 34 deletions compiler/src/dotty/tools/dotc/cc/Capability.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,33 +91,33 @@ object Capabilities:
*/
case class Maybe(underlying: Capability) extends DerivedCapability

/** The readonly capability `x.rd`. We have {x.rd} <: {x}.
*
* Read-only capabilities cannot wrap maybe capabilities
* but they can wrap reach capabilities. We have
* (x?).readOnly = (x.rd)?
*/
case class ReadOnly(underlying: ObjectCapability | RootCapability | Reach | Restricted)
extends DerivedCapability

/** The restricted capability `x.only[C]`. We have {x.only[C]} <: {x}.
*
* Restricted capabilities cannot wrap maybe capabilities or read-only capabilities
* Restricted capabilities cannot wrap maybe capabilities
* but they can wrap reach capabilities. We have
* (x?).restrict[T] = (x.restrict[T])?
* (x.rd).restrict[T] = (x.restrict[T]).rd
*/
case class Restricted(underlying: ObjectCapability | RootCapability | Reach, cls: ClassSymbol)
case class Restricted(underlying: CoreCapability | RootCapability | Reach, cls: ClassSymbol)
extends DerivedCapability

/** An extractor for the read-only capability `x.rd`. `x.rd` is represented as
* `c.only[caps.Read]`.
*/
object ReadOnly:
def apply(underlying: CoreCapability | RootCapability | Reach | Restricted)(using Context): Restricted =
Restricted(underlying.stripRestricted.asInstanceOf, defn.Caps_Read)
Copy link
Contributor

@natsukagami natsukagami Nov 5, 2025

Choose a reason for hiding this comment

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

Is it valid here to strip the existing restricted? e.g. if the classifiers was extended with a sub-classifier of Read

Copy link
Contributor Author

@odersky odersky Nov 5, 2025

Choose a reason for hiding this comment

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

We don't support restrictions with more than one classifierr, so the only issue here is that we might want to keep the existing sub-classifier of Read (if such things exist). But I think that should be handled by the caller.

Copy link
Contributor

@Linyxus Linyxus Nov 5, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

But we said Mutable should be a special "classifier" that allows its instance to capture anything. So we might well have a matrix m: Matrix^{fresh1, async} that captures a control capability Async (here the fresh1 is the Mutable fresh for this matrix). Then, getting readonly on m.only[Control].rd should, by principle, be empty. But with the current logic it will be m.rd or equivalently fresh1.rd.

Copy link
Contributor

@Linyxus Linyxus Nov 5, 2025

Choose a reason for hiding this comment

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

After a second thought I think it should be fine. This expressiveness issue could be solved by first widening m.only[Control] to just async and then take readonly on it.

Copy link
Contributor

@Linyxus Linyxus Nov 5, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

After a second thought I think it should be fine. This expressiveness issue could be solved by first widening m.only[Control] to just async and then take readonly on it, which will be empty.

def unapply(ref: Restricted)(using Context): Option[CoreCapability | RootCapability | Reach] =
if ref.cls == defn.Caps_Read then Some(ref.underlying) else None

/** If `x` is a capability, its reach capability `x*`. `x*` stands for all
* capabilities reachable through `x`.
* We have `{x} <: {x*} <: dcs(x)}` where the deep capture set `dcs(x)` of `x`
* is the union of all capture sets that appear in covariant position in the
* type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
* are unrelated.
*
* Reach capabilities cannot wrap read-only capabilities or maybe capabilities.
* Reach capabilities cannot wrap restricted capabilities or maybe capabilities.
* We have
* (x?).reach = (x.reach)?
* (x.rd).reach = (x.reach).rd
Expand All @@ -133,7 +133,7 @@ object Capabilities:
object GlobalCap extends RootCapability:
def descr(using Context) = "the universal root capability"
override val maybe = Maybe(this)
override val readOnly = ReadOnly(this)
override def readOnly(using Context) = ReadOnly(this)
override def restrict(cls: ClassSymbol)(using Context) = Restricted(this, cls)
override def reach = unsupported("cap.reach")
override def singletonCaptureSet(using Context) = CaptureSet.universal
Expand Down Expand Up @@ -347,23 +347,21 @@ object Capabilities:
case self: Maybe => self
case _ => cached(Maybe(this))

def readOnly: ReadOnly | Maybe = this match
def readOnly(using Context): Restricted | Maybe = this match
case Maybe(ref1) => Maybe(ref1.readOnly)
case self: ReadOnly => self
case self: (ObjectCapability | RootCapability | Reach | Restricted) => cached(ReadOnly(self))
case self @ ReadOnly(_) => self
case self: (CoreCapability | RootCapability | Reach | Restricted) => cached(ReadOnly(self))

def restrict(cls: ClassSymbol)(using Context): Restricted | ReadOnly | Maybe = this match
def restrict(cls: ClassSymbol)(using Context): Restricted | Maybe = this match
case Maybe(ref1) => Maybe(ref1.restrict(cls))
case ReadOnly(ref1) => ReadOnly(ref1.restrict(cls).asInstanceOf[Restricted])
case self @ Restricted(ref1, prevCls) =>
val combinedCls = leastClassifier(prevCls, cls)
if combinedCls == prevCls then self
else cached(Restricted(ref1, combinedCls))
case self: (ObjectCapability | RootCapability | Reach) => cached(Restricted(self, cls))
case self: (CoreCapability | RootCapability | Reach) => cached(Restricted(self, cls))

def reach: Reach | Restricted | ReadOnly | Maybe = this match
def reach: Reach | Restricted | Maybe = this match
case Maybe(ref1) => Maybe(ref1.reach)
case ReadOnly(ref1) => ReadOnly(ref1.reach.asInstanceOf[Reach | Restricted])
case Restricted(ref1, cls) => Restricted(ref1.reach.asInstanceOf[Reach], cls)
case self: Reach => self
case self: ObjectCapability => cached(Reach(self))
Expand All @@ -378,9 +376,9 @@ object Capabilities:
case tp: SetCapability => tp.captureSetOfInfo.isReadOnly
case _ => this ne stripReadOnly

/** The restriction of this capability or NoSymbol if there is none */
final def restriction(using Context): Symbol = this match
case Restricted(_, cls) => cls
case ReadOnly(ref1) => ref1.restriction
case Maybe(ref1) => ref1.restriction
case _ => NoSymbol

Expand All @@ -398,10 +396,9 @@ object Capabilities:
case Maybe(ref1) => ref1.stripReadOnly.maybe
case _ => this

/** Drop restrictions with clss `cls` or a superclass of `cls` */
/** Drop restrictions with class `cls` or a superclass of `cls` */
final def stripRestricted(cls: ClassSymbol)(using Context): Capability = this match
case Restricted(ref1, cls1) if cls.isSubClass(cls1) => ref1
case ReadOnly(ref1) => ref1.stripRestricted(cls).readOnly
case Maybe(ref1) => ref1.stripRestricted(cls).maybe
case _ => this

Expand All @@ -410,7 +407,6 @@ object Capabilities:

final def stripReach(using Context): Capability = this match
case Reach(ref1) => ref1
case ReadOnly(ref1) => ref1.stripReach.readOnly
case Restricted(ref1, cls) => ref1.stripReach.restrict(cls)
case Maybe(ref1) => ref1.stripReach.maybe
case _ => this
Expand Down Expand Up @@ -592,7 +588,6 @@ object Capabilities:
def computeHiddenSet(f: Refs => Refs)(using Context): Refs = this match
case self: FreshCap => f(self.hiddenSet.elems)
case Restricted(elem1, cls) => elem1.computeHiddenSet(f).map(_.restrict(cls))
case ReadOnly(elem1) => elem1.computeHiddenSet(f).map(_.readOnly)
case _ => emptyRefs

/** The transitive classifiers of this capability. */
Expand All @@ -610,8 +605,6 @@ object Capabilities:
assert(cls != defn.AnyClass)
if cls == defn.NothingClass then ClassifiedAs(Nil)
else ClassifiedAs(cls :: Nil)
case ReadOnly(ref1) =>
ref1.transClassifiers
case Maybe(ref1) =>
ref1.transClassifiers
case Reach(_) =>
Expand All @@ -635,8 +628,6 @@ object Capabilities:
case Restricted(_, cls1) =>
assert(cls != defn.AnyClass)
cls1.isSubClass(cls)
case ReadOnly(ref1) =>
ref1.tryClassifyAs(cls)
case Maybe(ref1) =>
ref1.tryClassifyAs(cls)
case Reach(_) =>
Expand All @@ -657,7 +648,6 @@ object Capabilities:
cs.forall(c => leastClassifier(c, cls) == defn.NothingClass)
case _ => false
isEmpty || ref1.isKnownEmpty
case ReadOnly(ref1) => ref1.isKnownEmpty
case Maybe(ref1) => ref1.isKnownEmpty
case _ => false

Expand Down Expand Up @@ -718,7 +708,6 @@ object Capabilities:
case _ => false
|| viaInfo(y.info)(subsumingRefs(this, _))
case Maybe(y1) => this.stripMaybe.subsumes(y1)
case ReadOnly(y1) => this.stripReadOnly.subsumes(y1)
case Restricted(y1, cls) => this.stripRestricted(cls).subsumes(y1)
case y: TypeRef if y.derivesFrom(defn.Caps_CapSet) =>
// The upper and lower bounds don't have to be in the form of `CapSet^{...}`.
Expand Down Expand Up @@ -805,7 +794,6 @@ object Capabilities:
y.isKnownClassifiedAs(cls) && x1.maxSubsumes(y, canAddHidden)
case _ =>
y match
case ReadOnly(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)
case Restricted(y1, cls) => this.stripRestricted(cls).maxSubsumes(y1, canAddHidden)
case _ => false

Expand Down Expand Up @@ -893,7 +881,6 @@ object Capabilities:
case c: DerivedCapability =>
val c1 = c.underlying.toType
c match
case _: ReadOnly => ReadOnlyCapability(c1)
case Restricted(_, cls) => OnlyCapability(c1, cls)
case _: Reach => ReachCapability(c1)
case _: Maybe => MaybeCapability(c1)
Expand Down
2 changes: 0 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1578,8 +1578,6 @@ object CaptureSet:
case Restricted(c1, cls) =>
if cls == defn.NothingClass then CaptureSet.empty
else c1.captureSetOfInfo.restrict(cls) // todo: should we simplify using subsumption here?
case ReadOnly(c1) =>
c1.captureSetOfInfo.readOnly
case Maybe(c1) =>
c1.captureSetOfInfo.maybe
case c: RootCapability =>
Expand Down
4 changes: 2 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/SepCheck.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -180,7 +180,7 @@ object SepCheck:
case newElem :: newElems1 =>
if seen.contains(newElem) then
recur(seen, acc, newElems1)
else newElem.stripRestricted.stripReadOnly match
else newElem.stripRestricted match
case _: FreshCap if !newElem.isKnownClassifiedAs(defn.Caps_SharedCapability) =>
val hiddens = if followHidden then newElem.hiddenSet.toList else Nil
recur(seen + newElem, acc + newElem, hiddens ++ newElems1)
Expand Down Expand Up @@ -220,7 +220,7 @@ object SepCheck:
refs1.foreach: ref =>
if !ref.isReadOnly then
val coreRef = ref.stripRestricted
if refs2.exists(_.stripRestricted.stripReadOnly.coversFresh(coreRef)) then
if refs2.exists(_.stripRestricted.coversFresh(coreRef)) then
acc += coreRef
acc
assert(refs.forall(_.isTerminalCapability))
Expand Down
5 changes: 0 additions & 5 deletions compiler/src/dotty/tools/dotc/core/Types.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6384,11 +6384,6 @@ object Types extends TypeUtils {
mapCapability(c1) match
case c2: Capability => c2.restrict(cls)
case (cs: CaptureSet, exact) => (cs.restrict(cls), exact)
case ReadOnly(c1) =>
assert(!deep)
mapCapability(c1) match
case c2: Capability => c2.readOnly
case (cs: CaptureSet, exact) => (cs.readOnly, exact)
case Maybe(c1) =>
assert(!deep)
mapCapability(c1) match
Expand Down
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/mutability.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,5 +94,5 @@
-- Error: tests/neg-custom-args/captures/mutability.scala:45:9 ---------------------------------------------------------
45 | r6().x.set(33) // error
| ^^^^^^^^^^
| Cannot call update method set of Ref[Int]^{cap.rd}
| since its capture set {cap.rd} is read-only.
| Cannot call update method set of Ref[Int]^{r6*.rd}
| since its capture set {r6*.rd} is read-only.
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/mutvars.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,5 +94,5 @@
-- Error: tests/neg-custom-args/captures/mutvars.scala:44:13 -----------------------------------------------------------
44 | r6().x.fld = 33 // error
| ^^^^^^^^^^^^^^^
| Cannot assign to field fld of Ref[Int]^{cap.rd}
| since its capture set {cap.rd} is read-only.
| Cannot assign to field fld of Ref[Int]^{r6*.rd}
| since its capture set {r6*.rd} is read-only.
4 changes: 4 additions & 0 deletions tests/pos-custom-args/captures/i24334.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
import language.experimental.captureChecking
class Ref extends caps.Mutable
def f1[C1^](a: Ref^{C1}): Unit =
val t = a
Loading