Bug fixes

 1. Fix canBeTracked for TermRefs

    only TermRefs where prefix is NoPrefix or `this` can be tracked. The
    others have to be widened.

 2. Fix rule for comparing capture refs on the left

 3. Be more careful where comparisons are frozen

Author: odersky

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

@@ -82,3 +82,11 @@ extension (tp: Type)
       tp.tp1.canHaveInferredCapture || tp.tp2.canHaveInferredCapture
     case _ =>
       false
+
+  def stripCapturing(using Context): Type = tp.dealiasKeepAnnots match
+    case CapturingType(parent, _) =>
+      parent.stripCapturing
+    case atd @ AnnotatedType(parent, annot) =>
+      atd.derivedAnnotatedType(parent.stripCapturing, annot)
+    case _ =>
+      tp

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

@@ -79,26 +79,23 @@ sealed abstract class CaptureSet extends Showable:
   def accountsFor(x: CaptureRef)(using Context): Boolean =
     reporting.trace(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true) {
       elems.contains(x)
-      || !x.isRootCapability && (x.captureSetOfInfo frozen_<:< this) == CompareResult.OK
+      || !x.isRootCapability
+          && x.captureSetOfInfo.subCaptures(this, frozen = true) == CompareResult.OK
     }
 
   /** The subcapturing test */
-  def <:< (that: CaptureSet)(using Context): CompareResult =
-    subcaptures(that)(using ctx, VarState())
+  def subCaptures(that: CaptureSet, frozen: Boolean)(using Context): CompareResult =
+    subCaptures(that)(using ctx, if frozen then FrozenState else VarState())
 
-  /** The subcapturing test, where all variables are treated as frozen */
-  def frozen_<:<(that: CaptureSet)(using Context): CompareResult =
-    subcaptures(that)(using ctx, FrozenState)
-
-  def =:= (that: CaptureSet)(using Context): Boolean =
-       (this frozen_<:< that) == CompareResult.OK
-    && (that frozen_<:< this) == CompareResult.OK
-
-  private def subcaptures(that: CaptureSet)(using Context, VarState): CompareResult =
+  private def subCaptures(that: CaptureSet)(using Context, VarState): CompareResult =
     val result = that.tryInclude(elems)
     if result == CompareResult.OK then addSuper(that) else varState.abort()
     result
 
+  def =:= (that: CaptureSet)(using Context): Boolean =
+       this.subCaptures(that, frozen = true) == CompareResult.OK
+    && that.subCaptures(this, frozen = true) == CompareResult.OK
+
   /** The smallest capture set (via <:<) that is a superset of both
    *  `this` and `that`
    */
@@ -230,6 +227,7 @@ object CaptureSet:
     def addNewElems(newElems: Refs)(using Context, VarState): CompareResult =
       if recordElemsState() then
         elems ++= newElems
+        // assert(id != 2 || elems.size != 2, this)
         val depsIt = deps.iterator
         while depsIt.hasNext do
           val result = depsIt.next.tryInclude(newElems)

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

@@ -24,7 +24,7 @@ import typer.Applications.productSelectorTypes
 import reporting.trace
 import NullOpsDecorator._
 import annotation.constructorOnly
-import cc.{CapturingType, derivedCapturingType, CaptureSet}
+import cc.{CapturingType, derivedCapturingType, CaptureSet, stripCapturing}
 
 /** Provides methods to compare types.
  */
@@ -491,8 +491,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             // under -Ycheck. Test case is i7965.scala.
 
       case CapturingType(parent1, refs1) =>
-        if refs1 <:< tp2.captureSet == CaptureSet.CompareResult.OK then recur(parent1, tp2)
-        else thirdTry
+        if refs1.subCaptures(tp2.captureSet, frozenConstraint) == CaptureSet.CompareResult.OK then
+          recur(parent1, tp2)
+        else
+          thirdTry
       case tp1: AnnotatedType if !tp1.isRefining =>
         recur(tp1.parent, tp2)
       case tp1: MatchType =>
@@ -810,15 +812,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             }
           case _ => false
         comparePaths || {
-          val tp2n = tp1 match
-            case tp1: CaptureRef
-            if tp1.isTracked && tp2.captureSet.accountsFor(tp1) =>
-              // If `{x}` subcaptures the capture set of the RHS, we can dispense
-              // with capture checking. This is achieved by widening the RHS with
-              // the universal capture set `{*}`.
-              CapturingType(tp2, CaptureSet.universal)
-            case _ => tp2
-          isSubType(tp1.underlying.widenExpr, tp2n, approx.addLow)
+          var tp1w = tp1.underlying.widenExpr
+          tp1 match
+            case tp1: CaptureRef if tp1.isTracked =>
+              val stripped = tp1w.stripCapturing
+              tp1w = CapturingType(stripped, tp1.singletonCaptureSet)
+            case _ =>
+          isSubType(tp1w, tp2, approx.addLow)
         }
       case tp1: RefinedType =>
         isNewSubType(tp1.parent)
@@ -2382,8 +2382,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     case tp1: TypeVar if tp1.isInstantiated =>
       tp1.underlying & tp2
     case CapturingType(parent1, refs1) =>
-      if tp2.captureSet <:< refs1 == CaptureSet.CompareResult.OK then parent1 & tp2
-      else tp1.derivedCapturingType(parent1 & tp2, refs1)
+      if tp2.captureSet.subCaptures(refs1, frozenConstraint) == CaptureSet.CompareResult.OK then
+        parent1 & tp2
+      else
+        tp1.derivedCapturingType(parent1 & tp2, refs1)
     case tp1: AnnotatedType if !tp1.isRefining =>
       tp1.underlying & tp2
     case _ =>

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

@@ -165,7 +165,8 @@ object TypeOps:
         // corrective steps, so no widening is wanted.
         simplify(l, theMap) | simplify(r, theMap)
       case CapturingType(parent, refs) =>
-        if !ctx.mode.is(Mode.Type) && refs <:< parent.captureSet == CompareResult.OK then
+        if !ctx.mode.is(Mode.Type)
+            && refs.subCaptures(parent.captureSet, frozen = true) == CompareResult.OK then
           simplify(parent, theMap)
         else
           mapOver

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

@@ -1848,7 +1848,7 @@ object Types {
       if captureSet.accountsFor(ref) then this else CapturingType(this, ref.singletonCaptureSet)
 
     def capturing(cs: CaptureSet)(using Context): Type =
-      if cs.isConst && (cs frozen_<:< captureSet) == CompareResult.OK then this
+      if cs.isConst && cs.subCaptures(captureSet, frozen = true) == CompareResult.OK then this
       else this match
         case CapturingType(parent, cs1) => parent.capturing(cs1 ++ cs)
         case _ => CapturingType(this, cs)
@@ -2703,7 +2703,7 @@ object Types {
      */
     def canBeTracked(using Context) =
       ((prefix eq NoPrefix)
-      || symbol.is(ParamAccessor)
+      || symbol.is(ParamAccessor) && (prefix eq symbol.owner.thisType)
       || symbol.hasAnnotation(defn.AbilityAnnot)
       || isRootCapability
       ) && !symbol.is(Method)

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

@@ -63,7 +63,7 @@ object CheckCaptures:
   def checkWellformedPost(tp: Type, pos: SrcPos)(using Context): Unit = tp match
     case CapturingType(parent, refs) =>
       for ref <- refs.elems do
-        if (ref.captureSet frozen_<:< CaptureSet.empty) == CompareResult.OK then
+        if ref.captureSet.subCaptures(CaptureSet.empty, frozen = true) == CompareResult.OK then
           report.error(em"$ref cannot be tracked since its capture set is empty", pos)
         else if parent.captureSet.accountsFor(ref) then
           report.warning(em"redundant capture: $parent already accounts for $ref", pos)
@@ -164,15 +164,15 @@ class CheckCaptures extends Recheck:
         checkSubset(targetSet, curEnv.captured, pos)
 
     def assertSub(cs1: CaptureSet, cs2: CaptureSet)(using Context) =
-      assert((cs1 <:< cs2) == CompareResult.OK, i"$cs1 is not a subset of $cs2")
+      assert(cs1.subCaptures(cs2, frozen = false) == CompareResult.OK, i"$cs1 is not a subset of $cs2")
 
     def checkElem(elem: CaptureRef, cs: CaptureSet, pos: SrcPos)(using Context) =
-      val res = elem.singletonCaptureSet <:< cs
+      val res = elem.singletonCaptureSet.subCaptures(cs, frozen = false)
       if res != CompareResult.OK then
         report.error(i"$elem cannot be referenced here; it is not included in allowed capture set ${res.blocking}", pos)
 
     def checkSubset(cs1: CaptureSet, cs2: CaptureSet, pos: SrcPos)(using Context) =
-      val res = cs1 <:< cs2
+      val res = cs1.subCaptures(cs2, frozen = false)
       if res != CompareResult.OK then
         report.error(i"references $cs1 are not all included in allowed capture set ${res.blocking}", pos)