Make reach capabilities annotated types

Author: odersky

compiler/src/dotty/tools/dotc/ast/Desugar.scala

@@ -1858,6 +1858,8 @@ object desugar {
             Annotated(
               AppliedTypeTree(ref(defn.SeqType), t),
               New(ref(defn.RepeatedAnnot.typeRef), Nil :: Nil))
+        else if op.name == nme.CC_REACH then
+          Apply(ref(defn.Caps_reachCapability), t :: Nil)
         else
           assert(ctx.mode.isExpr || ctx.reporter.errorsReported || ctx.mode.is(Mode.Interactive), ctx.mode)
           Select(t, op.name)

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

@@ -77,9 +77,14 @@ class NoCommonRoot(rs: Symbol*)(using Context) extends Exception(
 extension (tree: Tree)
 
   /** Map tree with CaptureRef type to its type, throw IllegalCaptureRef otherwise */
-  def toCaptureRef(using Context): CaptureRef = tree.tpe match
-    case ref: CaptureRef if ref.isTrackableRef => ref
-    case tpe => throw IllegalCaptureRef(tpe) // if this was compiled from cc syntax, problem should have been reported at Typer
+  def toCaptureRef(using Context): CaptureRef = tree match
+    case ReachCapabilityApply(arg) =>
+      arg.toCaptureRef.reach
+    case _ => tree.tpe match
+      case ref: CaptureRef if ref.isTrackableRef =>
+        ref
+      case tpe =>
+        throw IllegalCaptureRef(tpe) // if this was compiled from cc syntax, problem should have been reported at Typer
 
   /** Convert a @retains or @retainsByName annotation tree to the capture set it represents.
    *  For efficience, the result is cached as an Attachment on the tree.
@@ -209,15 +214,15 @@ extension (tp: Type)
     tm(tp)
 
   /** If `x` is a capture ref, its reach capability `x*`, represented internally
-   *  as `x.$reach`. `x*` stands for all capabilities reachable through `x`".
+   *  as `x @reachCapability`. `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.
    */
-  def reach(using Context): TermRef =
+  def reach(using Context): CaptureRef =
     assert(tp.isTrackableRef)
-    TermRef(tp, nme.CC_REACH, defn.Any_ccReach)
+    AnnotatedType(tp, Annotation(defn.ReachCapabilityAnnot, util.Spans.NoSpan))
 
   /** If `ref` is a trackable capture ref, and `tp` has only covariant occurrences of a
    *  universal capture set, replace all these occurrences by `{ref*}`. This implements
@@ -365,3 +370,21 @@ extension (tp: AnnotatedType)
   def isBoxed(using Context): Boolean = tp.annot match
     case ann: CaptureAnnotation => ann.boxed
     case _ => false
+
+/** An extractor for `caps.reachCapability(ref)`, which is used to express a reach
+ *  capability as a tree in a @retains annotation.
+ */
+object ReachCapabilityApply:
+  def unapply(tree: Apply)(using Context): Option[Tree] = tree match
+    case Apply(reach, arg :: Nil) if reach.symbol == defn.Caps_reachCapability => Some(arg)
+    case _ => None
+
+/** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
+ *  the reach capability `ref*` as a type.
+ */
+object ReachCapability:
+  def unapply(tree: AnnotatedType)(using Context): Option[SingletonCaptureRef] = tree match
+    case AnnotatedType(parent: SingletonCaptureRef, ann)
+    if ann.symbol == defn.ReachCapabilityAnnot => Some(parent)
+    case _ => None
+

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

@@ -156,7 +156,7 @@ sealed abstract class CaptureSet extends Showable:
           case y: TermRef => !y.isReach && (y.prefix eq x)
           case _ => false
       || x.match
-          case x: TermRef if x.isReach => x.stripReach.subsumes(y.stripReach)
+          case ReachCapability(x1) => x1.subsumes(y.stripReach)
           case _ => false
 
   /** {x} <:< this   where <:< is subcapturing, but treating all variables
@@ -500,18 +500,15 @@ object CaptureSet:
     private def levelOK(elem: CaptureRef)(using Context): Boolean =
       if elem.isRootCapability then !noUniversal
       else elem match
-        case elem: TermRef =>
-          if elem.isReach then levelOK(elem.stripReach)
-          else if levelLimit.exists then
-            var sym = elem.symbol
-            if sym.isLevelOwner then sym = sym.owner
-            levelLimit.isContainedIn(sym.levelOwner)
-          else true
-        case elem: ThisType =>
-          if levelLimit.exists then
-            levelLimit.isContainedIn(elem.cls.levelOwner)
-          else true
-        case elem: TermParamRef =>
+        case elem: TermRef if levelLimit.exists =>
+          var sym = elem.symbol
+          if sym.isLevelOwner then sym = sym.owner
+          levelLimit.isContainedIn(sym.levelOwner)
+        case elem: ThisType if levelLimit.exists =>
+          levelLimit.isContainedIn(elem.cls.levelOwner)
+        case ReachCapability(elem1) =>
+          levelOK(elem1)
+        case _ =>
           true
 
     def addDependent(cs: CaptureSet)(using Context, VarState): CompareResult =
@@ -1015,8 +1012,8 @@ object CaptureSet:
   /** The capture set of the type underlying CaptureRef */
   def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
     case ref: TermRef if ref.isRootCapability => ref.singletonCaptureSet
-    case ref: TermRef if ref.isReach => deepCaptureSet(ref.prefix.widen)
-      .showing(i"Deep capture set of $ref: ${ref.prefix.widen} = $result", capt)
+    case ReachCapability(ref1) => deepCaptureSet(ref1.widen)
+      .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
     case _ => ofType(ref.underlying, followResult = true)
 
   /** Capture set of a type */

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

@@ -130,7 +130,10 @@ object CheckCaptures:
         report.error(em"Singleton type $parent cannot have capture set", parent.srcPos)
       case _ =>
     for elem <- ann.retainedElems do
-      elem.tpe match
+      val elem1 = elem match
+        case ReachCapabilityApply(arg) => arg
+        case _ => elem
+      elem1.tpe match
         case ref: CaptureRef =>
           if !ref.isTrackableRef then
             report.error(em"$elem cannot be tracked since it is not a parameter or local value", elem.srcPos)
@@ -1249,7 +1252,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       val checker = new TypeTraverser:
         private var allowed: SimpleIdentitySet[TermParamRef] = SimpleIdentitySet.empty
 
-        private def isAllowed(ref: CaptureRef): Boolean = ref.stripReach match
+        private def isAllowed(ref: CaptureRef): Boolean = ref match
           case ref: TermParamRef => allowed.contains(ref)
           case _ => true
 

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

@@ -312,11 +312,8 @@ class Definitions {
           Final,
           bounds = TypeBounds.lower(AnyClass.thisType))
 
-    @tu lazy val Any_ccReach = enterMethod(AnyClass, nme.CC_REACH, AnyType, SyntheticArtifact | Final)
-
     def AnyMethods: List[TermSymbol] = List(Any_==, Any_!=, Any_equals, Any_hashCode,
-      Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest,
-      Any_typeCast, Any_ccReach)
+      Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest, Any_typeCast)
 
   @tu lazy val ObjectClass: ClassSymbol = {
     val cls = requiredClass("java.lang.Object")
@@ -981,6 +978,7 @@ class Definitions {
   @tu lazy val CapsModule: Symbol = requiredModule("scala.caps")
     @tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("cap")
     @tu lazy val Caps_Cap: TypeSymbol = CapsModule.requiredType("Cap")
+    @tu lazy val Caps_reachCapability: TermSymbol = CapsModule.requiredMethod("reachCapability")
     @tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe")
     @tu lazy val Caps_unsafeAssumePure: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumePure")
     @tu lazy val Caps_unsafeBox: Symbol = CapsUnsafeModule.requiredMethod("unsafeBox")
@@ -1055,6 +1053,7 @@ class Definitions {
   @tu lazy val TargetNameAnnot: ClassSymbol = requiredClass("scala.annotation.targetName")
   @tu lazy val VarargsAnnot: ClassSymbol = requiredClass("scala.annotation.varargs")
   @tu lazy val SinceAnnot: ClassSymbol = requiredClass("scala.annotation.since")
+  @tu lazy val ReachCapabilityAnnot = requiredClass("scala.annotation.internal.reachCapability")
   @tu lazy val RequiresCapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.internal.requiresCapability")
   @tu lazy val RetainsAnnot: ClassSymbol = requiredClass("scala.annotation.retains")
   @tu lazy val RetainsByNameAnnot: ClassSymbol = requiredClass("scala.annotation.retainsByName")

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

@@ -2163,7 +2163,7 @@ object Types {
   }
 
   /** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs */
-  trait CaptureRef extends SingletonType:
+  trait CaptureRef extends TypeProxy, ValueType:
     private var myCaptureSet: CaptureSet | Null = uninitialized
     private var myCaptureSetRunId: Int = NoRunId
     private var mySingletonCaptureSet: CaptureSet.Const | Null = null
@@ -2175,9 +2175,9 @@ object Types {
       isTrackableRef && (isRootCapability || !captureSetOfInfo.isAlwaysEmpty)
 
     /** Is this a reach reference of the form `x*`? */
-    def isReach(using Context): Boolean = false // overridden in TermRef
+    def isReach(using Context): Boolean = false // overridden in AnnotatedType
 
-    def stripReach(using Context): CaptureRef = this // overridden in TermRef
+    def stripReach(using Context): CaptureRef = this // overridden in AnnotatedType
 
     /** Is this reference the generic root capability `cap` ? */
     def isRootCapability(using Context): Boolean = false
@@ -2214,6 +2214,8 @@ object Types {
 
   end CaptureRef
 
+  trait SingletonCaptureRef extends SingletonType, CaptureRef
+
   /** A trait for types that bind other types that refer to them.
    *  Instances are: LambdaType, RecType.
    */
@@ -2877,7 +2879,7 @@ object Types {
    */
   abstract case class TermRef(override val prefix: Type,
                               private var myDesignator: Designator)
-    extends NamedType, ImplicitRef, CaptureRef {
+    extends NamedType, ImplicitRef, SingletonCaptureRef {
 
     type ThisType = TermRef
     type ThisName = TermName
@@ -2913,21 +2915,12 @@ object Types {
       || symbol.is(ParamAccessor) && (prefix eq symbol.owner.thisType)
       || isRootCapability
       ) && !symbol.isOneOf(UnstableValueFlags)
-      || isReach
-
-    override def isReach(using Context): Boolean =
-      name == nme.CC_REACH && symbol == defn.Any_ccReach
-
-    override def stripReach(using Context): CaptureRef =
-      if isReach then prefix.asInstanceOf[CaptureRef] else this
 
     override def isRootCapability(using Context): Boolean =
       name == nme.CAPTURE_ROOT && symbol == defn.captureRoot
 
     override def normalizedRef(using Context): CaptureRef =
-      if isReach then TermRef(stripReach.normalizedRef, name, denot)
-      else if isTrackableRef then symbol.termRef
-      else this
+      if isTrackableRef then symbol.termRef else this
   }
 
   abstract case class TypeRef(override val prefix: Type,
@@ -3066,7 +3059,8 @@ object Types {
    *  Note: we do not pass a class symbol directly, because symbols
    *  do not survive runs whereas typerefs do.
    */
-  abstract case class ThisType(tref: TypeRef) extends CachedProxyType, CaptureRef {
+  abstract case class ThisType(tref: TypeRef)
+  extends CachedProxyType, SingletonCaptureRef {
     def cls(using Context): ClassSymbol = tref.stableInRunSymbol match {
       case cls: ClassSymbol => cls
       case _ if ctx.mode.is(Mode.Interactive) => defn.AnyClass // was observed to happen in IDE mode
@@ -4679,7 +4673,8 @@ object Types {
   /** Only created in `binder.paramRefs`. Use `binder.paramRefs(paramNum)` to
    *  refer to `TermParamRef(binder, paramNum)`.
    */
-  abstract case class TermParamRef(binder: TermLambda, paramNum: Int) extends ParamRef, CaptureRef {
+  abstract case class TermParamRef(binder: TermLambda, paramNum: Int)
+  extends ParamRef, SingletonCaptureRef {
     type BT = TermLambda
     def kindString: String = "Term"
     def copyBoundType(bt: BT): Type = bt.paramRefs(paramNum)
@@ -5386,7 +5381,7 @@ object Types {
   // ----- Annotated and Import types -----------------------------------------------
 
   /** An annotated type tpe @ annot */
-  abstract case class AnnotatedType(parent: Type, annot: Annotation) extends CachedProxyType, ValueType {
+  abstract case class AnnotatedType(parent: Type, annot: Annotation) extends CachedProxyType, CaptureRef {
 
     override def underlying(using Context): Type = parent
 
@@ -5415,6 +5410,23 @@ object Types {
       isRefiningCache
     }
 
+    override def isTrackableRef(using Context) =
+      isReach && parent.isTrackableRef
+
+    /** Is this a reach reference of the form `x*`? */
+    override def isReach(using Context): Boolean =
+      annot.symbol == defn.ReachCapabilityAnnot
+
+    override def stripReach(using Context): SingletonCaptureRef =
+      (if isReach then parent else this).asInstanceOf[SingletonCaptureRef]
+
+    override def normalizedRef(using Context): CaptureRef =
+      if isReach then AnnotatedType(stripReach.normalizedRef, annot) else this
+
+    override def captureSet(using Context): CaptureSet =
+      if isReach then super.captureSet
+      else CaptureSet.ofType(this, followResult = false)
+
     // equals comes from case class; no matching override is needed
 
     override def computeHash(bs: Binders): Int =

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

@@ -1479,7 +1479,7 @@ object Parsers {
         if isIdent(nme.raw.STAR) then
           in.nextToken()
           atSpan(startOffset(id)):
-            Select(id, nme.CC_REACH)
+            PostfixOp(id, Ident(nme.CC_REACH))
         else id
 
     /**  CaptureSet ::=  `{` CaptureRef {`,` CaptureRef} `}`    -- under captureChecking

compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

@@ -15,7 +15,7 @@ import util.SourcePosition
 import scala.util.control.NonFatal
 import scala.annotation.switch
 import config.{Config, Feature}
-import cc.{CapturingType, RetainingType, CaptureSet, isBoxed, levelOwner, retainedElems}
+import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, isBoxed, levelOwner, retainedElems}
 
 class PlainPrinter(_ctx: Context) extends Printer {
 
@@ -377,8 +377,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
   def toTextRef(tp: SingletonType): Text = controlled {
     tp match {
       case tp: TermRef =>
-        if tp.isReach then toTextRef(tp.stripReach) ~ "*"
-        else toTextPrefixOf(tp) ~ selectionString(tp)
+        toTextPrefixOf(tp) ~ selectionString(tp)
       case tp: ThisType =>
         nameString(tp.cls) + ".this"
       case SuperType(thistpe: SingletonType, _) =>
@@ -404,6 +403,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
     homogenize(tp) match
       case tp: TermRef if tp.symbol == defn.captureRoot => Str("cap")
       case tp: SingletonType => toTextRef(tp)
+      case ReachCapability(tp1) => toTextRef(tp1) ~ "*"
       case _ => toText(tp)
 
   protected def isOmittablePrefix(sym: Symbol): Boolean =

compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala

@@ -703,7 +703,10 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         val opPrec = parsing.precedence(op.name)
         changePrec(opPrec) { toText(l) ~ " " ~ toText(op) ~ " " ~ toText(r) }
       case PostfixOp(l, op) =>
-        changePrec(InfixPrec) { toText(l) ~ " " ~ toText(op) }
+        if op.name == nme.CC_REACH then
+          changePrec(DotPrec) { toText(l) ~ "*" }
+        else
+          changePrec(InfixPrec) { toText(l) ~ " " ~ toText(op) }
       case PrefixOp(op, r) =>
         changePrec(DotPrec) { toText(op) ~ " " ~ toText(r) }
       case Parens(t) =>

library/src/scala/annotation/internal/reach.scala

@@ -0,0 +1,8 @@
+package scala.annotation
+package internal
+
+/** An annotation that marks a capture ref as a reach capability.
+ *  `x*` is encoded as `x.type @reachCapability`
+ */
+class reachCapability extends StaticAnnotation
+

library/src/scala/caps.scala

@@ -15,6 +15,12 @@ import annotation.experimental
 
   given Cap = cap
 
+  /** Reach capabilities x* which appear as terms in @retains annotations are encoded
+   *  as `caps.reachCapability(x)`. When converted to CaptureRef types in capture sets
+   *  they are  represented as `x.type @annotation.internal.reachCapability`.
+   */
+  extension (x: Any) def reachCapability: Any = x
+
   object unsafe:
 
     extension [T](x: T)

tests/run-macros/i6518.check

@@ -2,7 +2,6 @@
 ##
 $asInstanceOf$
 $isInstanceOf$
-$reach
 ==
 andThen
 apply