Fix captureSet computations for false reach capabilities

Fix the capture set computation of a type T @reachCapability where T
is not a singleton captureRef. Such types can be the results of typemaps.
The capture set in this case should be the deep capture set of T.

Author: odersky

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

@@ -204,8 +204,9 @@ extension (tp: Type)
     case tp: TypeParamRef =>
       tp.derivesFrom(defn.Caps_CapSet)
     case AnnotatedType(parent, annot) =>
-      annot.symbol == defn.ReachCapabilityAnnot
+      (annot.symbol == defn.ReachCapabilityAnnot
       || annot.symbol == defn.MaybeCapabilityAnnot
+      ) && parent.isTrackableRef
     case _ =>
       false
 

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

@@ -1057,7 +1057,7 @@ object CaptureSet:
   /** Capture set of a type */
   def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =
     def recur(tp: Type): CaptureSet = trace(i"ofType $tp, ${tp.getClass} $followResult", show = true):
-      tp.dealias match
+      tp.dealiasKeepAnnots match
         case tp: TermRef =>
           tp.captureSet
         case tp: TermParamRef =>
@@ -1068,6 +1068,12 @@ object CaptureSet:
           empty
         case CapturingType(parent, refs) =>
           recur(parent) ++ refs
+        case tp @ AnnotatedType(parent, ann) if ann.hasSymbol(defn.ReachCapabilityAnnot) =>
+          parent match
+            case parent: SingletonCaptureRef if parent.isTrackableRef =>
+              tp.singletonCaptureSet
+            case _ =>
+              CaptureSet.deepCaptureSet(parent)
         case tpd @ defn.RefinedFunctionOf(rinfo: MethodType) if followResult =>
           ofType(tpd.parent, followResult = false)             // pick up capture set from parent type
           ++ (recur(rinfo.resType)                             // add capture set of result
@@ -1083,7 +1089,7 @@ object CaptureSet:
               case tparams @ (LambdaParam(tl, _) :: _) => cs.substParams(tl, args)
               case _ => cs
         case tp: TypeProxy =>
-          recur(tp.underlying)
+          recur(tp.superType)
         case AndType(tp1, tp2) =>
           recur(tp1) ** recur(tp2)
         case OrType(tp1, tp2) =>

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

@@ -27,7 +27,7 @@ import config.{Config, Feature}
 
 import dotty.tools.dotc.util.SourcePosition
 import dotty.tools.dotc.ast.untpd.{MemberDef, Modifiers, PackageDef, RefTree, Template, TypeDef, ValOrDefDef}
-import cc.{CaptureSet, CapturingType, toCaptureSet, IllegalCaptureRef, isRetains}
+import cc.{CaptureSet, CapturingType, toCaptureSet, IllegalCaptureRef, isRetains, ReachCapability, MaybeCapability}
 import dotty.tools.dotc.parsing.JavaParsers
 
 class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
@@ -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 tp: AnnotatedType if tp.isReach || tp.isMaybe =>
+      case ReachCapability(_) | MaybeCapability(_) =>
         toTextCaptureRef(tp)
       case _ =>
         super.toText(tp)

tests/neg-custom-args/captures/leak-problem-2.check

@@ -0,0 +1,7 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leak-problem-2.scala:8:8 ---------------------------------
+8 |  = race(Seq(src1, src2)) // error
+  |    ^^^^^^^^^^^^^^^^^^^^^
+  |    Found:    Source[box T^?]^{src1, src2}
+  |    Required: Source[T]
+  |
+  | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/leak-problem-2.scala

@@ -0,0 +1,9 @@
+import language.experimental.captureChecking
+
+trait Source[+T]
+
+def race[T](@caps.unboxed sources: Seq[Source[T]^]): Source[T]^{sources*} = ???
+
+def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{}
+  = race(Seq(src1, src2)) // error
+    // this compiled and returned a Source that does not capture src1 and src2.

tests/neg-custom-args/captures/reaches.check

@@ -25,6 +25,18 @@
    |                           ^^^^^^^^^^^^
    |                       The expression's type box () => Unit is not allowed to capture the root capability `cap`.
    |                       This usually means that a capability persists longer than its allowed lifetime.
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:53:2 ---------------------------------------
+53 |  val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
+   |  ^
+   |  Found:    box () => Unit
+   |  Required: () => Unit
+   |
+   |  Note that box () => Unit cannot be box-converted to () => Unit
+   |  since at least one of their capture sets contains the root capability `cap`
+54 |  usingFile: f =>
+55 |    id(() => f.write())
+   |
+   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:27 --------------------------------------
 62 |    val f1: File^{id*} = id(f) // error, since now id(f): File^
    |                         ^^^^^
@@ -40,9 +52,3 @@
 79 |  ps.map((x, y) => compose1(x, y)) // error // error
    |             ^
    |             Local reach capability ps* leaks into capture scope of method mapCompose
--- [E057] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:53:51 --------------------------------------
-53 |  val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
-   |                                                   ^
-   |                                             Type argument () -> Unit does not conform to lower bound () => Unit
-   |
-   | longer explanation available when compiling with `-explain`