Implement @use scheme

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

@@ -525,8 +525,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
   def makeRetaining(parent: Tree, refs: List[Tree], annotName: TypeName)(using Context): Annotated =
     Annotated(parent, New(scalaAnnotationDot(annotName), List(refs)))
 
-  def makeCapsOf(id: Ident)(using Context): Tree =
-    TypeApply(Select(scalaDot(nme.caps), nme.capsOf), id :: Nil)
+  def makeCapsOf(tp: Tree)(using Context): Tree =
+    TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)
 
   def makeCapsBound()(using Context): Tree =
     makeRetaining(

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

@@ -92,6 +92,16 @@ class CCState:
    */
   val approxWarnings: mutable.ListBuffer[Message] = mutable.ListBuffer()
 
+  /** The operation to perform `recordUse` is called. This is typically the case
+   *  when a subtype check is performed between a part of a function argument
+   *  and a corresponding part of a formal parameter that was labelled @use.
+   *  Such annotations are mapped to `<use>[T]` applications, which are handled
+   *  as compiletime ops.
+   *  The parameter to the handler is typically the deep capture set of the argument.
+   *  The result of the handler is the result to be returned from the subtype check.
+   */
+  private var useHandler: CaptureSet => Boolean = Function.const(true)
+
   private var curLevel: Level = outermostLevel
   private val symLevel: mutable.Map[Symbol, Int] = mutable.Map()
 
@@ -108,6 +118,17 @@ object CCState:
    */
   def currentLevel(using Context): Level = ccState.curLevel
 
+  /** Perform operation `op` with a given useHandler */
+  inline def withUseHandler[T](handler: CaptureSet => Boolean)(inline op: T)(using Context): T =
+    val ccs = ccState
+    val saved = ccs.useHandler
+    ccs.useHandler = handler
+    try op finally ccs.useHandler = saved
+
+  /** Record a deep capture set in the current `useSet` */
+  def recordUse(cs: CaptureSet)(using Context): Boolean =
+    ccState.useHandler(cs)
+
   inline def inNestedLevel[T](inline op: T)(using Context): T =
     val ccs = ccState
     val saved = ccs.curLevel
@@ -146,7 +167,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
@@ -194,7 +215,8 @@ extension (tp: Type)
       true
     case tp: TermRef =>
       ((tp.prefix eq NoPrefix)
-      || tp.symbol.is(ParamAccessor) && tp.prefix.isThisTypeOf(tp.symbol.owner)
+      || tp.symbol.isField && !tp.symbol.isStatic && (
+        tp.prefix.isThisTypeOf(tp.symbol.owner) || tp.prefix.isTrackableRef)
       || tp.isRootCapability
       ) && !tp.symbol.isOneOf(UnstableValueFlags)
     case tp: TypeRef =>
@@ -203,6 +225,7 @@ extension (tp: Type)
       tp.derivesFrom(defn.Caps_CapSet)
     case AnnotatedType(parent, annot) =>
       (annot.symbol == defn.ReachCapabilityAnnot
+      || annot.symbol == defn.ReachUnderUseCapabilityAnnot
       || annot.symbol == defn.MaybeCapabilityAnnot
       ) && parent.isTrackableRef
     case _ =>
@@ -232,7 +255,8 @@ extension (tp: Type)
     if dcs.isAlwaysEmpty then dcs
     else tp match
       case tp @ ReachCapability(_) => tp.singletonCaptureSet
-      case tp: SingletonCaptureRef => tp.reach.singletonCaptureSet
+      case tp @ ReachUnderUseCapability(_) => tp.singletonCaptureSet
+      case tp: SingletonCaptureRef => tp.reach().singletonCaptureSet
       case _ => dcs
 
   /** A type capturing `ref` */
@@ -395,9 +419,11 @@ extension (tp: Type)
    *  type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
    *  are unrelated.
    */
-  def reach(using Context): CaptureRef = tp match
+  def reach(underUse: Boolean = false)(using Context): CaptureRef = tp match
     case tp: CaptureRef if tp.isTrackableRef =>
-      if tp.isReach then tp else ReachCapability(tp)
+      if tp.isReach then tp
+      else if underUse then ReachUnderUseCapability(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
@@ -470,26 +496,32 @@ extension (tp: Type)
     object narrowCaps extends TypeMap:
       /** Has the variance been flipped at this point? */
       private var isFlipped: Boolean = false
+      private var underUse = false
 
       def apply(t: Type) =
         val saved = isFlipped
         try
           if variance <= 0 then isFlipped = true
-          t.dealias match
-            case t1 @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>
-              t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
-            case t1 @ FunctionOrMethod(args, res @ Existential(_, _))
+          t.dealiasKeepAnnots match
+            case t @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>
+              t.derivedCapturingType(apply(p), ref.reach(underUse).singletonCaptureSet)
+            case t @ AnnotatedType(parent, ann) =>
+              if ann.symbol == defn.UseAnnot then
+                val saved = underUse
+                underUse = true
+                try mapOver(t)
+                finally underUse = saved
+              else
+                t.derivedAnnotatedType(this(parent), ann)
+            case t @ FunctionOrMethod(args, res @ Existential(_, _))
             if args.forall(_.isAlwaysPure) =>
               // Also map existentials in results to reach capabilities if all
               // preceding arguments are known to be always pure
-              apply(t1.derivedFunctionOrMethod(args, Existential.toCap(res)))
+              this(t.derivedFunctionOrMethod(args, Existential.toCap(res)))
             case Existential(_, _) =>
               t
-            case _ => t match
-              case t @ CapturingType(p, cs) =>
-                t.derivedCapturingType(apply(p), cs) // don't map capture set variables
-              case t =>
-                mapOver(t)
+            case _ =>
+              mapOver(t)
         finally isFlipped = saved
     end narrowCaps
 
@@ -639,14 +671,15 @@ object CapsOfApply:
 class AnnotatedCapability(annot: Context ?=> ClassSymbol):
   def apply(tp: Type)(using Context) =
     AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
-  def unapply(tree: AnnotatedType)(using Context): Option[SingletonCaptureRef] = tree match
-    case AnnotatedType(parent: SingletonCaptureRef, ann) if ann.symbol == annot => Some(parent)
+  def unapply(tp: AnnotatedType)(using Context): Option[CaptureRef] = tp 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

@@ -30,9 +30,21 @@ trait CaptureRef extends TypeProxy, ValueType:
 
   /** Is this a reach reference of the form `x*`? */
   final def isReach(using Context): Boolean = this match
-    case AnnotatedType(_, annot) => annot.symbol == defn.ReachCapabilityAnnot
+    case AnnotatedType(_, annot) =>
+      annot.symbol == defn.ReachCapabilityAnnot || annot.symbol == defn.ReachUnderUseCapabilityAnnot
     case _ => false
 
+  final def isUnderUse(using Context): Boolean = this match
+    case AnnotatedType(_, annot) => annot.symbol == defn.ReachUnderUseCapabilityAnnot
+    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
+
   /** Is this a maybe reference of the form `x?`? */
   final def isMaybe(using Context): Boolean = this match
     case AnnotatedType(_, annot) => annot.symbol == defn.MaybeCapabilityAnnot
@@ -61,18 +73,19 @@ trait CaptureRef extends TypeProxy, ValueType:
     case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists)
     case _ => false
 
-  /** Normalize reference so that it can be compared with `eq` for equality */
-  final def normalizedRef(using Context): CaptureRef = this match
-    case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef =>
-      tp.derivedAnnotatedType(parent.normalizedRef, annot)
-    case tp: TermRef if tp.isTrackableRef =>
-      tp.symbol.termRef
-    case _ => this
+  // With the support of pathes, we don't need to normalize the `TermRef`s anymore.
+  // /** Normalize reference so that it can be compared with `eq` for equality */
+  // final def normalizedRef(using Context): CaptureRef = this match
+  //   case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef =>
+  //     tp.derivedAnnotatedType(parent.normalizedRef, annot)
+  //   case tp: TermRef if tp.isTrackableRef =>
+  //     tp.symbol.termRef
+  //   case _ => this
 
   /** The capture set consisting of exactly this reference */
   final def singletonCaptureSet(using Context): CaptureSet.Const =
     if mySingletonCaptureSet == null then
-      mySingletonCaptureSet = CaptureSet(this.normalizedRef)
+      mySingletonCaptureSet = CaptureSet(this)
     mySingletonCaptureSet.uncheckedNN
 
   /** The capture set of the type underlying this reference */
@@ -97,27 +110,46 @@ trait CaptureRef extends TypeProxy, ValueType:
    *   x subsumes y  ==>  x* subsumes y, x subsumes y?
    *   x subsumes y  ==>  x* subsumes y*, x? subsumes y?
    *   x: x1.type /\ x1 subsumes y  ==>  x subsumes y
+   *   TODO: Document path cases
    */
   final def subsumes(y: CaptureRef)(using Context): Boolean =
+
+    def subsumingRefs(x: Type, y: Type): Boolean = x match
+      case x: CaptureRef => y match
+        case y: CaptureRef => x.subsumes(y)
+        case _ => false
+      case _ => false
+
+    def viaInfo(info: Type)(test: Type => Boolean): Boolean = info.match
+      case info: SingletonCaptureRef => test(info)
+      case info: AndType => test(info.tp1) || test(info.tp2)
+      case info: OrType => test(info.tp1) && test(info.tp2)
+      case _ => false
+
     (this eq y)
     || this.isRootCapability
     || y.match
         case y: TermRef =>
-          (y.prefix eq this)
-          || y.info.match
-              case y1: SingletonCaptureRef => this.subsumes(y1)
+            y.prefix.match
+              case ypre: CaptureRef =>
+                this.subsumes(ypre)
+                || this.match
+                    case x @ TermRef(xpre: CaptureRef, _) if x.symbol == y.symbol =>
+                      subsumingRefs(xpre, ypre) && subsumingRefs(ypre, xpre)
+                    case _ =>
+                      false
               case _ => false
+          || viaInfo(y.info)(subsumingRefs(this, _))
         case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
-        case x: TermRef =>
-          x.info match
-            case x1: SingletonCaptureRef => x1.subsumes(y)
-            case _ => false
+        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)
         case _ => false
+  end subsumes
 
   def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] =
     CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)

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

@@ -374,7 +374,7 @@ object CaptureSet:
 
   def apply(elems: CaptureRef*)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty
-    else Const(SimpleIdentitySet(elems.map(_.normalizedRef.ensuring(_.isTrackableRef))*))
+    else Const(SimpleIdentitySet(elems.map(_.ensuring(_.isTrackableRef))*))
 
   def apply(elems: Refs)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty else Const(elems)
@@ -508,11 +508,17 @@ object CaptureSet:
         !noUniversal
       else elem match
         case elem: TermRef if level.isDefined =>
-          elem.symbol.ccLevel <= level
+          elem.prefix match
+            case prefix: CaptureRef =>
+              levelOK(prefix)
+            case _ =>
+              elem.symbol.ccLevel <= level
         case elem: ThisType if level.isDefined =>
           elem.cls.ccLevel.nextInner <= level
         case ReachCapability(elem1) =>
           levelOK(elem1)
+        case ReachUnderUseCapability(elem1) =>
+          levelOK(elem1)
         case MaybeCapability(elem1) =>
           levelOK(elem1)
         case _ =>
@@ -1062,6 +1068,8 @@ 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 */
@@ -1078,7 +1086,9 @@ object CaptureSet:
           empty
         case CapturingType(parent, refs) =>
           recur(parent) ++ refs
-        case tp @ AnnotatedType(parent, ann) if ann.hasSymbol(defn.ReachCapabilityAnnot) =>
+        case tp @ AnnotatedType(parent, ann)
+        if ann.hasSymbol(defn.ReachCapabilityAnnot)
+            || ann.hasSymbol(defn.ReachUnderUseCapabilityAnnot) =>
           parent match
             case parent: SingletonCaptureRef if parent.isTrackableRef =>
               tp.singletonCaptureSet