Make Capability a sealed trait

 - two subtraits: SharedCapability and ExclusiveCapability

Author: odersky

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

@@ -492,7 +492,7 @@ object Capabilities:
 
     def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability)
     def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable)
-    def derivesFromSharable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Sharable)
+    def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)
 
     /** The capture set consisting of exactly this reference */
     def singletonCaptureSet(using Context): CaptureSet.Const =
@@ -707,7 +707,7 @@ object Capabilities:
         case x: ResultCap =>
           val result = y match
             case y: ResultCap => vs.unify(x, y)
-            case _ => y.derivesFromSharable
+            case _ => y.derivesFromShared
           if !result then
             TypeComparer.addErrorNote(CaptureSet.ExistentialSubsumesFailure(x, y))
           result
@@ -717,7 +717,7 @@ object Capabilities:
             case _: ResultCap => false
             case _: FreshCap if CCState.collapseFresh => true
             case _ =>
-              y.derivesFromSharable
+              y.derivesFromShared
               || canAddHidden && vs != VarState.HardSeparate && CCState.capIsRoot
         case Restricted(x1, cls) =>
           y.isKnownClassifiedAs(cls) && x1.maxSubsumes(y, canAddHidden)

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

@@ -378,7 +378,7 @@ extension (tp: Type)
 
   def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability)
   def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable)
-  def derivesFromSharedCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Sharable)
+  def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)
 
   /** Drop @retains annotations everywhere */
   def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling

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

@@ -612,7 +612,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     val badParams = mutable.ListBuffer[Symbol]()
     def currentOwner = role.dclSym.orElse(ctx.owner)
     for hiddenRef <- refsToCheck.deductSymRefs(role.dclSym).deduct(explicitRefs(tpe)) do
-      if !hiddenRef.derivesFromSharable then
+      if !hiddenRef.derivesFromShared then
         hiddenRef.pathRoot match
           case ref: TermRef =>
             val refSym = ref.symbol
@@ -649,7 +649,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     role match
       case _: TypeRole.Argument | _: TypeRole.Qualifier =>
         for ref <- refsToCheck do
-          if !ref.derivesFromSharable then
+          if !ref.derivesFromShared then
             consumed.put(ref, pos)
       case _ =>
   end checkConsumedRefs

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

@@ -375,14 +375,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
         else fntpe
 
       /** 1. Check that parents of capturing types are not pure.
-       *  2. Check that types extending caps.Sharable don't have a `cap` in their capture set.
-       *     TODO: Is this enough?
-       *     We need to also track that we cannot get exclusive capabilities in paths
-       *     where some prefix derives from Sharable. Also, can we just
-       *     exclude `cap`, or do we have to extend this to all exclusive capabilties?
-       *     The problem is that we know what is exclusive in general only after capture
-       *     checking, not before.
-       *     But maybe the rules for classification already cover these cases.
        */
       def checkRetainsOK(tp: Type): tp.type =
         tp match
@@ -393,8 +385,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
               // an explicit result type in the override, the inherited capture set
               // will be ignored anyway.
               fail(em"$parent is a pure type, it makes no sense to add a capture set to it")
-            else if refs.isUniversal && parent.derivesFromSharedCapability then
-              fail(em"$tp extends Sharable, so it cannot capture `cap`")
           case _ =>
         tp
 

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

@@ -1003,6 +1003,12 @@ class Definitions {
   @tu lazy val CapsModule: Symbol = requiredPackage("scala.caps")
     @tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("cap")
     @tu lazy val Caps_Capability: ClassSymbol = requiredClass("scala.caps.Capability")
+    @tu lazy val Caps_Classifier: ClassSymbol = requiredClass("scala.caps.Classifier")
+    @tu lazy val Caps_SharedCapability: ClassSymbol = requiredClass("scala.caps.SharedCapability")
+    @tu lazy val Caps_ExclusiveCapability: ClassSymbol = requiredClass("scala.caps.ExclusiveCapability")
+    @tu lazy val Caps_Control: ClassSymbol = requiredClass("scala.caps.Control")
+    @tu lazy val Caps_Mutable: ClassSymbol = requiredClass("scala.caps.Mutable")
+    @tu lazy val Caps_Read: ClassSymbol = requiredClass("scala.caps.Read")
     @tu lazy val Caps_CapSet: ClassSymbol = requiredClass("scala.caps.CapSet")
     @tu lazy val CapsInternalModule: Symbol = requiredModule("scala.caps.internal")
     @tu lazy val Caps_erasedValue: Symbol = CapsInternalModule.requiredMethod("erasedValue")
@@ -1013,10 +1019,6 @@ class Definitions {
     @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains")
     @tu lazy val Caps_ContainsModule: Symbol = requiredModule("scala.caps.Contains")
     @tu lazy val Caps_containsImpl: TermSymbol = Caps_ContainsModule.requiredMethod("containsImpl")
-    @tu lazy val Caps_Mutable: ClassSymbol = requiredClass("scala.caps.Mutable")
-    @tu lazy val Caps_Sharable: ClassSymbol = requiredClass("scala.caps.Sharable")
-    @tu lazy val Caps_Control: ClassSymbol = requiredClass("scala.caps.Control")
-    @tu lazy val Caps_Classifier: ClassSymbol = requiredClass("scala.caps.Classifier")
 
   @tu lazy val PureClass: ClassSymbol = requiredClass("scala.Pure")
 
@@ -2110,10 +2112,10 @@ class Definitions {
   @tu lazy val ccExperimental: Set[Symbol] = Set(
     CapsModule, CapsModule.moduleClass, PureClass,
     Caps_Capability, // TODO: Remove when Capability is stabilized
+    Caps_Classifier, Caps_SharedCapability, Caps_Control, Caps_ExclusiveCapability, Caps_Mutable, Caps_Read,
     RequiresCapabilityAnnot,
     captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass, UseAnnot,
-    Caps_Mutable, Caps_Sharable, Caps_Control, Caps_Classifier, ConsumeAnnot,
-    CapsUnsafeModule, CapsUnsafeModule.moduleClass,
+    ConsumeAnnot, CapsUnsafeModule, CapsUnsafeModule.moduleClass,
     CapsInternalModule, CapsInternalModule.moduleClass,
     RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot)
 

library/src/scala/caps/package.scala

@@ -21,9 +21,11 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
  * is turned on.
  * But even without capture checking, extending this trait can be useful for documenting the intended purpose
  * of a class.
+ *
+ * Capability has exactly two subtraits: Shared and Exclusive.
  */
 @experimental
-trait Capability extends Any
+sealed trait Capability extends Any
 
 /** A marker trait for classifier capabilities that can appear in `.only`
  *  qualifiers. Capability classes directly extending `Classifier` are treated
@@ -36,21 +38,36 @@ trait Classifier
 @experimental
 object cap extends Capability
 
-/** Marker trait for classes with methods that requires an exclusive reference. */
+/** Marker trait for capabilities that can be safely shared in a concurrent context.
+ * During separation checking, shared capabilities are not taken into account.
+ */
 @experimental
-trait Mutable extends Capability, Classifier
+trait SharedCapability extends Capability, Classifier
 
-/** Marker trait for capabilities that can be safely shared in a concurrent context.
-  * During separation checking, shared capabilities are not taken into account.
-  */
 @experimental
-trait Sharable extends Capability, Classifier
+type Shared = SharedCapability
+
+/** Marker trait for exclusive capabilities that are separation-checked
+ */
+@experimental
+trait ExclusiveCapability extends Capability, Classifier
+
+@experimental
+type Exclusive = SharedCapability
 
 /** Base trait for capabilities that capture some continuation or return point in
  *  the stack. Examples are exceptions, labels, Async, CanThrow.
  */
 @experimental
-trait Control extends Sharable, Classifier
+trait Control extends SharedCapability, Classifier
+
+/** Marker trait for classes with methods that require an exclusive reference. */
+@experimental
+trait Mutable extends ExclusiveCapability, Classifier
+
+/** Marker trait for classes with reader methods, typically extended by Mutable classes */
+@experimental
+trait Read extends Mutable, Classifier
 
 /** Carrier trait for capture set type parameters */
 @experimental

tests/disabled/pos/lazylist.scala

@@ -34,7 +34,7 @@ object LazyNil extends LazyList[Nothing]:
 def map[A, B](xs: {*} LazyList[A], f: {*} A => B): {f, xs} LazyList[B] =
   xs.map(f)
 
-class Cap extends caps.Capability
+class Cap extends caps.SharedCapability
 
 def test(cap1: Cap, cap2: Cap, cap3: Cap) =
   def f[T](x: LazyList[T]): LazyList[T] = if cap1 == cap1 then x else LazyNil

tests/neg-custom-args/captures/branding.scala

@@ -3,18 +3,18 @@ import caps.*
 
 
 def main() =
-  trait Channel[T] extends caps.Capability:
+  trait Channel[T] extends caps.SharedCapability:
     def send(msg: T): Unit
     def recv(): T
 
-  trait Logger extends caps.Capability:
+  trait Logger extends caps.SharedCapability:
     def log(msg: String): Unit
 
   // we can close over anything subsumed by the 'trusted' brand capability, but nothing else
   def runSecure[C^ >: {trusted} <: {trusted}](block: () ->{C} Unit): Unit = block()
 
   // This is a 'brand" capability to mark what can be mentioned in trusted code
-  object trusted extends caps.Capability
+  object trusted extends caps.SharedCapability
 
   val trustedLogger: Logger^{trusted} = ???
   val trustedChannel: Channel[String]^{trusted} = ???

tests/neg-custom-args/captures/branding2.scala

@@ -3,18 +3,18 @@ import caps.*
 
 
 def main() =
-  trait Channel[T] extends caps.Capability:
+  trait Channel[T] extends caps.SharedCapability:
     def send(msg: T): Unit
     def recv(): T
 
-  trait Logger extends caps.Capability:
+  trait Logger extends caps.SharedCapability:
     def log(msg: String): Unit
 
   // we can close over anything subsumed by the 'trusted' brand capability, but nothing else
   def runSecure(block: () ->{trusted} Unit): Unit = block()
 
   // This is a 'brand" capability to mark what can be mentioned in trusted code
-  object trusted extends caps.Capability
+  object trusted extends caps.SharedCapability
 
   val trustedLogger: Logger^{trusted} = ???
   val trustedChannel: Channel[String]^{trusted} = ???

tests/neg-custom-args/captures/byname.scala

@@ -1,4 +1,4 @@
-class Cap extends caps.Capability
+class Cap extends caps.SharedCapability
 
 def test(cap1: Cap, cap2: Cap) =
   def f() = if cap1 == cap1 then g else g