Revert "Represent read-only with a classifier"

This reverts commit 9abbb03.
This reverts commit 0a0e666.
This reverts commit 67ba9b5.

Read-only cannot be a classifier anymore, since it would overlap with Unscoped,
but neither subsumes the other.

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: CoreCapability | RootCapability | Reach | Restricted)
+  extends DerivedCapability
+
   /** The restricted capability `x.only[C]`. We have {x.only[C]} <: {x}.
    *
-   *  Restricted capabilities cannot wrap maybe capabilities
+   *  Restricted capabilities cannot wrap maybe capabilities or read-only 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: 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 restricted capabilities or maybe capabilities.
+   *  Reach capabilities cannot wrap read-only 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 def readOnly(using Context) = ReadOnly(this)
+    override val readOnly = 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
@@ -347,21 +347,23 @@ object Capabilities:
       case self: Maybe => self
       case _ => cached(Maybe(this))
 
-    def readOnly(using Context): Restricted | Maybe = this match
+    def readOnly: ReadOnly | Maybe = this match
       case Maybe(ref1) => Maybe(ref1.readOnly)
-      case self @ ReadOnly(_) => self
+      case self: ReadOnly => self
       case self: (CoreCapability | RootCapability | Reach | Restricted) => cached(ReadOnly(self))
 
-    def restrict(cls: ClassSymbol)(using Context): Restricted | Maybe = this match
+    def restrict(cls: ClassSymbol)(using Context): Restricted | ReadOnly | 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: (CoreCapability | RootCapability | Reach) => cached(Restricted(self, cls))
 
-    def reach: Reach | Restricted | Maybe = this match
+    def reach: Reach | Restricted | ReadOnly | 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))
@@ -382,6 +384,7 @@ object Capabilities:
      */
     final def classifier(using Context): Symbol = this match
       case Restricted(_, cls) => cls
+      case ReadOnly(ref1) => ref1.classifier
       case Maybe(ref1) => ref1.classifier
       case self: FreshCap => self.hiddenSet.classifier
       case _ => NoSymbol
@@ -400,9 +403,10 @@ object Capabilities:
       case Maybe(ref1) => ref1.stripReadOnly.maybe
       case _ => this
 
-    /** Drop restrictions with class `cls` or a superclass of `cls` */
+    /** Drop restrictions with clss `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
 
@@ -411,6 +415,7 @@ 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
@@ -596,6 +601,7 @@ 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. */
@@ -613,6 +619,8 @@ 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(_) =>
@@ -636,6 +644,8 @@ 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,6 +666,7 @@ 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
 
@@ -716,6 +727,7 @@ 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^{...}`.
@@ -799,6 +811,7 @@ 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
 
@@ -886,6 +899,7 @@ 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

@@ -1625,6 +1625,8 @@ 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 match
+          else newElem.stripRestricted.stripReadOnly 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.coversFresh(coreRef)) then
+            if refs2.exists(_.stripRestricted.stripReadOnly.coversFresh(coreRef)) then
               acc += coreRef
         acc
       assert(refs.forall(_.isTerminalCapability))

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

@@ -955,7 +955,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
       case Nil =>
     recur(cls.baseClasses.filter(_.isClassifiedCapabilityClass).distinct)
     if cls.derivesFrom(defn.Caps_SharedCapability) && cls.derivesFrom(defn.Caps_Mutable) then
-      report.error(em"$cls cannot inheit from both SharaedCapability and Mutable", cls.srcPos)
+      report.error(em"$cls cannot inheit from both SharedCapability and Mutable", cls.srcPos)
 
   // ------ Checks to run after main capture checking --------------------------
 

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

@@ -6402,6 +6402,11 @@ 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/check-inferred.check

@@ -45,12 +45,12 @@
 -- Error: tests/neg-custom-args/captures/check-inferred.scala:49:15 ----------------------------------------------------
 49 |  private val y = ??? : (() => A^{cap.only[caps.Read]})  // error
    |               ^
-   |         value y needs an explicit type because it captures a root capability in its type () => test.A^{cap.rd}.
-   |         Fields capturing a root capability need to be given an explicit type unless the capability is already
-   |         subsumed by the computed capability of the enclosing class.
+   | value y needs an explicit type because it captures a root capability in its type () => test.A^{cap.only[Read]}.
+   | Fields capturing a root capability need to be given an explicit type unless the capability is already
+   | subsumed by the computed capability of the enclosing class.
    |
-   |         where:    =>  refers to a fresh root capability in the type of value y
-   |                   cap is a fresh root capability created in value y
+   | where:    =>  refers to a fresh root capability in the type of value y
+   |           cap is a fresh root capability created in value y
 -- Error: tests/neg-custom-args/captures/check-inferred.scala:29:21 ----------------------------------------------------
 29 |    private val count = Ref() // error
    |                     ^

tests/neg-custom-args/captures/classified-inheritance2.check

@@ -1,4 +1,15 @@
 -- Error: tests/neg-custom-args/captures/classified-inheritance2.scala:4:6 ---------------------------------------------
 4 |class Logger extends SharedCapability, Mutable:  // error (1) does this make sense?
   |      ^
-  |      class Logger cannot inheit from both SharaedCapability and Mutable
+  |      class Logger cannot inheit from both SharedCapability and Mutable
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/classified-inheritance2.scala:12:27 ----------------------
+12 |  val t: Logger^{} = Logger()  // error
+   |                     ^^^^^^^^
+   |Found:    Logger^{cap.rd}
+   |Required: Logger^{}
+   |
+   |Note that capability cap.rd is not included in capture set {}.
+   |
+   |where:    cap is a fresh root capability classified as SharedCapability created in value t when constructing instance Logger
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/classified-inheritance2.scala

@@ -9,4 +9,4 @@ def onlyShared(x: Object^{cap.only[SharedCapability]}): Unit = ()
 
 def main(): Unit =
   onlyShared(Logger())  // even if we allow (1), why would this type check?
-  val t: Logger^{} = Logger()  // and this type checks too, thus the above line I guess
+  val t: Logger^{} = Logger()  // error