Change encoding of reach capabilities under @use

The new encoding wraps such capabilities with @use instead of relying on a
@ReachUnderUse annotation. Advantage: This can generalize to capture set variables
under @use.

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

@@ -178,7 +178,7 @@ extension (tree: Tree)
    */
   def toCaptureRefs(using Context): List[CaptureRef] = tree match
     case ReachCapabilityApply(arg) =>
-      arg.toCaptureRefs.map(_.reach())
+      arg.toCaptureRefs.map(_.reach)
     case CapsOfApply(arg) =>
       arg.toCaptureRefs
     case _ => tree.tpe.dealiasKeepAnnots match
@@ -236,8 +236,8 @@ extension (tp: Type)
       tp.derivesFrom(defn.Caps_CapSet)
     case AnnotatedType(parent, annot) =>
       (annot.symbol == defn.ReachCapabilityAnnot
-      || annot.symbol == defn.ReachUnderUseCapabilityAnnot
       || annot.symbol == defn.MaybeCapabilityAnnot
+      || annot.symbol == defn.UseAnnot
       ) && parent.isTrackableRef
     case _ =>
       false
@@ -264,10 +264,9 @@ extension (tp: Type)
   def deepCaptureSet(using Context): CaptureSet =
     val dcs = CaptureSet.ofTypeDeeply(tp)
     if dcs.isAlwaysEmpty then dcs
-    else tp match
+    else tp.stripUse match
       case tp @ ReachCapability(_) => tp.singletonCaptureSet
-      case tp @ ReachUnderUseCapability(_) => tp.singletonCaptureSet
-      case tp: SingletonCaptureRef => tp.reach().singletonCaptureSet
+      case tp: SingletonCaptureRef => tp.reach.singletonCaptureSet
       case _ => dcs
 
   /** A type capturing `ref` */
@@ -430,11 +429,9 @@ extension (tp: Type)
    *  type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
    *  are unrelated.
    */
-  def reach(underUse: Boolean = false)(using Context): CaptureRef = tp match
+  def reach(using Context): CaptureRef = tp match
     case tp: CaptureRef if tp.isTrackableRef =>
-      if tp.isReach then tp
-      else if underUse then ReachUnderUseCapability(tp)
-      else ReachCapability(tp)
+      if tp.isReach then tp else ReachCapability(tp)
 
   /** If `x` is a capture ref, its maybe capability `x?`, represented internally
    *  as `x @maybeCapability`. `x?` stands for a capability `x` that might or might
@@ -458,6 +455,14 @@ extension (tp: Type)
     case tp: CaptureRef if tp.isTrackableRef =>
       if tp.isMaybe then tp else MaybeCapability(tp)
 
+  def isUnderUse(using Context): Boolean = tp match
+    case AnnotatedType(_: CaptureRef, annot) => annot.symbol == defn.UseAnnot
+    case _ => false
+
+  def stripUse(using Context): Type = tp match
+    case AnnotatedType(tp1: CaptureRef, annot) if annot.symbol == defn.UseAnnot => tp1
+    case _ => tp
+
   /** 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
    *  the new aspect of the (Var) rule, which can now be stated as follows:
@@ -515,7 +520,9 @@ extension (tp: Type)
           if variance <= 0 then isFlipped = true
           t.dealiasKeepAnnots match
             case t @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>
-              t.derivedCapturingType(apply(p), ref.reach(underUse).singletonCaptureSet)
+              var reach = ref.reach
+              if underUse then reach = reach.underUse
+              t.derivedCapturingType(apply(p), reach.singletonCaptureSet)
             case t @ AnnotatedType(parent, ann) =>
               if ann.symbol == defn.UseAnnot then
                 val saved = underUse
@@ -682,15 +689,14 @@ object CapsOfApply:
 class AnnotatedCapability(annot: Context ?=> ClassSymbol):
   def apply(tp: Type)(using Context) =
     AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
-  def unapply(tp: AnnotatedType)(using Context): Option[CaptureRef] = tp match
+  def unapply(tp: AnnotatedType)(using Context): Option[CaptureRef] = tp.stripUse match
     case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent)
     case _ => None
 
 /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
  *  the reach capability `ref*` as a type.
  */
 object ReachCapability extends AnnotatedCapability(defn.ReachCapabilityAnnot)
-object ReachUnderUseCapability extends AnnotatedCapability(defn.ReachUnderUseCapabilityAnnot)
 
 /** An extractor for `ref @maybeCapability`, which is used to express
  *  the maybe capability `ref?` as a type.

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

@@ -13,6 +13,7 @@ import CCState.*
 import Periods.NoRunId
 import compiletime.uninitialized
 import StdNames.nme
+import Annotations.Annotation
 
 /** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
  *  as well as two kinds of AnnotatedTypes representing reach and maybe capabilities.
@@ -29,36 +30,31 @@ trait CaptureRef extends TypeProxy, ValueType:
     this.isTrackableRef && (isMaxCapability || !captureSetOfInfo.isAlwaysEmpty)
 
   /** Is this a reach reference of the form `x*`? */
-  final def isReach(using Context): Boolean = this match
-    case AnnotatedType(_, annot) =>
-      annot.symbol == defn.ReachCapabilityAnnot || annot.symbol == defn.ReachUnderUseCapabilityAnnot
+  final def isReach(using Context): Boolean = this.stripUse match
+    case AnnotatedType(_, annot) => annot.symbol == defn.ReachCapabilityAnnot
     case _ => false
 
   final def isUnderUse(using Context): Boolean = this match
-    case AnnotatedType(_, annot) => annot.symbol == defn.ReachUnderUseCapabilityAnnot
+    case AnnotatedType(_, annot) => annot.symbol == defn.UseAnnot
     case _ => false
 
-  def toUnderUse(using Context): CaptureRef =
-    if isUnderUse then
-      this match
-        case _: AnnotatedType => stripReach.reach(underUse = true)
-        // TODO: Handle capture set variables here
-    else this
+  def underUse(using Context): CaptureRef =
+    AnnotatedType(this, Annotation(defn.UseAnnot, util.Spans.NoSpan))
 
   /** Is this a maybe reference of the form `x?`? */
-  final def isMaybe(using Context): Boolean = this match
+  final def isMaybe(using Context): Boolean = this.stripUse match
     case AnnotatedType(_, annot) => annot.symbol == defn.MaybeCapabilityAnnot
     case _ => false
 
   final def stripReach(using Context): CaptureRef =
     if isReach then
-      val AnnotatedType(parent: CaptureRef, _) = this: @unchecked
+      val AnnotatedType(parent: CaptureRef, _) = this.stripUse: @unchecked
       parent
     else this
 
   final def stripMaybe(using Context): CaptureRef =
     if isMaybe then
-      val AnnotatedType(parent: CaptureRef, _) = this: @unchecked
+      val AnnotatedType(parent: CaptureRef, _) = this.stripUse: @unchecked
       parent
     else this
 
@@ -144,7 +140,6 @@ trait CaptureRef extends TypeProxy, ValueType:
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
-        case ReachUnderUseCapability(x1) => x1.subsumes(y.stripReach)
         case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
         case x: TermParamRef => subsumesExistentially(x, y)
         case x: TypeRef => assumedContainsOf(x).contains(y)

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

@@ -517,8 +517,6 @@ object CaptureSet:
           elem.cls.ccLevel.nextInner <= level
         case ReachCapability(elem1) =>
           levelOK(elem1)
-        case ReachUnderUseCapability(elem1) =>
-          levelOK(elem1)
         case MaybeCapability(elem1) =>
           levelOK(elem1)
         case _ =>
@@ -1068,8 +1066,6 @@ object CaptureSet:
       else CaptureSet.universal
     case ReachCapability(ref1) => deepCaptureSet(ref1.widen)
       .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
-    case ReachUnderUseCapability(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 */
@@ -1087,8 +1083,7 @@ object CaptureSet:
         case CapturingType(parent, refs) =>
           recur(parent) ++ refs
         case tp @ AnnotatedType(parent, ann)
-        if ann.hasSymbol(defn.ReachCapabilityAnnot)
-            || ann.hasSymbol(defn.ReachUnderUseCapabilityAnnot) =>
+        if ann.hasSymbol(defn.ReachCapabilityAnnot) =>
           parent match
             case parent: SingletonCaptureRef if parent.isTrackableRef =>
               tp.singletonCaptureSet

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

@@ -1359,7 +1359,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     */
     def checkOverrides = new TreeTraverser:
       class OverridingPairsCheckerCC(clazz: ClassSymbol, self: Type, srcPos: SrcPos)(using Context) extends OverridingPairsChecker(clazz, self):
-        /** Check subtype with box adaptation and @use checking. 
+        /** Check subtype with box adaptation and @use checking.
          *  This function is passed to RefChecks to check the compatibility of overriding pairs.
          *  @param sym  symbol of the field definition that is being checked
          *  @use checking: Overrides must have fewer @uses than overridden members.
@@ -1385,7 +1385,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                   adapted.stripCapturing
                 case _ => adapted
             finally curEnv = saved
-            
+
           def lowerUseSeen: UseHandler = (tpUnderUse, other, fromBelow) => cmp =>
             cmp()
           def noLowerUseSeen: UseHandler = (tpUnderUse, other, fromBelow) => cmp =>
@@ -1395,8 +1395,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           CCState.withUseHandler(noLowerUseSeen):
             TypeComparer.usingContravarianceForMethods:
               actual1 frozen_<:< expected1
-        end checkSubtype
-        
+        end checkSubType
+
         override def needsCheck(overriding: Symbol, overridden: Symbol)(using Context): Boolean =
           !setup.isPreCC(overriding) && !setup.isPreCC(overridden)
 

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

@@ -1078,7 +1078,6 @@ class Definitions {
   @tu lazy val TargetNameAnnot: ClassSymbol = requiredClass("scala.annotation.targetName")
   @tu lazy val VarargsAnnot: ClassSymbol = requiredClass("scala.annotation.varargs")
   @tu lazy val ReachCapabilityAnnot = requiredClass("scala.annotation.internal.reachCapability")
-  @tu lazy val ReachUnderUseCapabilityAnnot = requiredClass("scala.annotation.internal.reachUnderUseCapability")
   @tu lazy val RequiresCapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.internal.requiresCapability")
   @tu lazy val RetainsAnnot: ClassSymbol = requiredClass("scala.annotation.retains")
   @tu lazy val RetainsCapAnnot: ClassSymbol = requiredClass("scala.annotation.retainsCap")

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, ReachCapability, ReachUnderUseCapability, MaybeCapability, isBoxed, retainedElems, isRetainsLike}
+import cc.*
 
 class PlainPrinter(_ctx: Context) extends Printer {
 
@@ -417,8 +417,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
       case tp: TermRef if tp.symbol == defn.captureRoot => Str("cap")
       case tp: SingletonType => toTextRef(tp)
       case tp: (TypeRef | TypeParamRef) => toText(tp) ~ "^"
-      case ReachCapability(tp1) => toTextCaptureRef(tp1) ~ "*"
-      case ReachUnderUseCapability(tp1) => toTextCaptureRef(tp1) ~ "*@use"
+      case ReachCapability(tp1) =>
+        toTextCaptureRef(tp1) ~ "*" ~ Str("@use").provided(tp.isUnderUse)
       case MaybeCapability(tp1) => toTextCaptureRef(tp1) ~ "?"
       case tp => toText(tp)
 

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

@@ -330,7 +330,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         "?" ~ (("(ignored: " ~ toText(ignored) ~ ")") provided printDebug)
       case tp @ PolyProto(targs, resType) =>
         "[applied to [" ~ toTextGlobal(targs, ", ") ~ "] returning " ~ toText(resType)
-      case ReachCapability(_) | ReachUnderUseCapability(_) | MaybeCapability(_) =>
+      case ReachCapability(_) | MaybeCapability(_) =>
         toTextCaptureRef(tp)
       case _ =>
         super.toText(tp)