New CC scheme: let class subsume function fields deeply

Author: Linyxus

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

@@ -482,27 +482,30 @@ object Capabilities:
         case info: OrType => viaInfo(info.tp1)(test) && viaInfo(info.tp2)(test)
         case _ => false
 
+      def trySubpath(y: TermRef, trySamePrefix: Boolean = true): Boolean =
+        y.prefix.match
+          case ypre: Capability =>
+            this.subsumes(ypre)
+            || trySamePrefix
+            && this.match
+                case x @ TermRef(xpre: Capability, _) if x.symbol == y.symbol =>
+                  // To show `{x.f} <:< {y.f}`, it is important to prove `x` and `y`
+                  // are equvalent, which means `x =:= y` in terms of subtyping,
+                  // not just `{x} =:= {y}` in terms of subcapturing.
+                  // It is possible to construct two singleton types `x` and `y`,
+                  // which subsume each other, but are not equal references.
+                  // See `tests/neg-custom-args/captures/path-prefix.scala` for example.
+                  withMode(Mode.IgnoreCaptures):
+                    TypeComparer.isSameRef(xpre, ypre)
+                case _ =>
+                  false
+          case _ => false
+
       try (this eq y)
       || maxSubsumes(y, canAddHidden = !vs.isOpen)
       || y.match
         case y: TermRef =>
-            y.prefix.match
-              case ypre: Capability =>
-                this.subsumes(ypre)
-                || this.match
-                    case x @ TermRef(xpre: Capability, _) if x.symbol == y.symbol =>
-                      // To show `{x.f} <:< {y.f}`, it is important to prove `x` and `y`
-                      // are equvalent, which means `x =:= y` in terms of subtyping,
-                      // not just `{x} =:= {y}` in terms of subcapturing.
-                      // It is possible to construct two singleton types `x` and `y`,
-                      // which subsume each other, but are not equal references.
-                      // See `tests/neg-custom-args/captures/path-prefix.scala` for example.
-                      withMode(Mode.IgnoreCaptures):
-                        TypeComparer.isSameRef(xpre, ypre)
-                    case _ =>
-                      false
-              case _ => false
-          || viaInfo(y.info)(subsumingRefs(this, _))
+          trySubpath(y) || viaInfo(y.info)(subsumingRefs(this, _))
         case Maybe(y1) => this.stripMaybe.subsumes(y1)
         case ReadOnly(y1) => this.stripReadOnly.subsumes(y1)
         case y: TypeRef if y.derivesFrom(defn.Caps_CapSet) =>
@@ -516,6 +519,12 @@ object Capabilities:
               this.subsumes(hi)
             case _ =>
               y.captureSetOfInfo.elems.forall(this.subsumes)
+        case Reach(y1: TermRef) =>
+          def isClassFunctionParam: Boolean =
+            def isClassParam = y1.symbol.is(ParamAccessor)
+            def isFunctionType = defn.isFunctionType(y1.widenDealias)
+            isClassParam && isFunctionType
+          isClassFunctionParam && trySubpath(y1, trySamePrefix = false)
         case _ => false
       || this.match
           case Reach(x1) => x1.subsumes(y.stripReach)

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

@@ -766,21 +766,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       val appType = resultToFresh(
         super.recheckApplication(tree, qualType, funType, argTypes),
         Origin.ResultInstance(funType, tree.symbol))
-      val qualCaptures = qualType.captureSet
-      val argCaptures =
-        for (argType, formal) <- argTypes.lazyZip(funType.paramInfos) yield
-          if formal.hasAnnotation(defn.UseAnnot) then argType.deepCaptureSet else argType.captureSet
-      appType match
-        case appType @ CapturingType(appType1, refs)
-        if qualType.exists
-            && !tree.fun.symbol.isConstructor
-            && qualCaptures.mightSubcapture(refs)
-            && argCaptures.forall(_.mightSubcapture(refs)) =>
-          val callCaptures = argCaptures.foldLeft(qualCaptures)(_ ++ _)
-          appType.derivedCapturingType(appType1, callCaptures)
-            .showing(i"narrow $tree: $appType, refs = $refs, qual-cs = ${qualType.captureSet} = $result", capt)
-        case appType =>
-          appType
+      appType
 
     private def isDistinct(xs: List[Type]): Boolean = xs match
       case x :: xs1 => xs1.isEmpty || !xs1.contains(x) && isDistinct(xs1)
@@ -832,8 +818,12 @@ class CheckCaptures extends Recheck, SymTransformer:
         for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
           val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol
           if !getter.is(Private) && getter.hasTrackedParts then
-            refined = refined.refinedOverride(getterName, argType.unboxed) // Yichen you might want to check this
-            allCaptures ++= argType.captureSet
+            refined = refined.refinedOverride(getterName, argType.unboxed) // TODO: This looks unsound.
+                                                                           // Try to find an counter-example.
+            if defn.isFunctionType(argType.widenDealias) then
+              allCaptures ++= argType.deepCaptureSet
+            else
+              allCaptures ++= argType.captureSet
         (refined, allCaptures)
 
       /** Augment result type of constructor with refinements and captures.