Represent read-only with a classifier (#24295)

`x.rd` is now a shorthand for `x.only[caps.Read]`.

Author: odersky

compiler/src/dotty/tools/dotc/cc/Capability.scala

@@ -90,33 +90,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)
+    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
@@ -132,7 +132,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
@@ -346,23 +346,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))
@@ -377,9 +375,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
 
@@ -397,10 +395,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
 
@@ -409,7 +406,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
@@ -591,7 +587,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. */
@@ -609,8 +604,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(_) =>
@@ -634,8 +627,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(_) =>
@@ -656,7 +647,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
 
@@ -717,7 +707,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^{...}`.
@@ -801,7 +790,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
 
@@ -889,7 +877,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)

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -1615,8 +1615,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 =>

compiler/src/dotty/tools/dotc/cc/SepCheck.scala

@@ -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)
@@ -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))

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -6402,11 +6402,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

tests/neg-custom-args/captures/mutability.check

@@ -115,5 +115,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.

tests/neg-custom-args/captures/mutvars.check

@@ -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.

tests/pos-custom-args/captures/i24334.scala

@@ -0,0 +1,4 @@
+import language.experimental.captureChecking
+class Ref extends caps.Mutable
+def f1[C1^](a: Ref^{C1}): Unit =
+  val t = a