Refine rules for capture parameters and members (#22000)

noti0na1 · web-flow · commit 6bf4483932b3 · 2024-12-01T21:57:09.000+01:00
This PR refines rules for capture set variables (parameters and members). Fix #21999, #22005, #22030 ## Add requirements for capture set variables When a capture set is encoded as a type, the type must refer to `CapSet` and bounded by `>: CapSet <: CapSet^`. An unbounded capture parameter would be `C >: CapSet <: CapSet^`, which can be desugared from `C^`. ```scala def f[C^](io: IO^{C^}) = ??? // becomes def f[C >: CapSet <: CapSet^](io: IO^{C^}) = ??? ``` We may consider the similar desugaring for type member in the future: ```scala class A: type C^ // becomes class A: type C >: CapSet <: CapSet^ ``` Then, constaints between capture variables become possible: ```scala def test[X^, Y^, Z >: X <: Y](x: C^{X^}, y: C^{Y^}, z: C^{Z^}) = ??? // Z is still bounded by >: CapSet <: CapSet^ ``` Update definitions in the library `caps.scala`, such that a type following the rule can be used inside a capture set. ```scala // Rule out C^{(Nothing)^} during typer def capsOf[CS >: CapSet <: CapSet @retainsCap]: Any = ??? sealed trait Contains[+C >: CapSet <: CapSet @retainsCap, R <: Singleton] ``` ## Add cases to handle `CapSet` in `subsumes` ``` * X = CapSet^cx, exists rx in cx, rx subsumes y ==> X subsumes y * Y = CapSet^cy, forall ry in cy, x subsumes ry ==> x subsumes Y * X: CapSet^c1...CapSet^c2, (CapSet^c1) subsumes y ==> X subsumes y * Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2) ==> x subsumes Y * Contains[X, y] ==> X subsumes y ``` ## Fix some issues related to overriding When deciding whether a class has a non-trivial self type, we look at the underlying type without capture set. [test_scala2_library_tasty]
diff --git a/compiler/src/dotty/tools/dotc/ast/untpd.scala b/compiler/src/dotty/tools/dotc/ast/untpd.scala
@@ -527,10 +527,13 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
   def makeCapsOf(tp: RefTree)(using Context): Tree =
     TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)
 
-  def makeCapsBound()(using Context): Tree =
-    makeRetaining(
+  // Capture set variable `[C^]` becomes: `[C >: CapSet <: CapSet^{cap}]`
+  def makeCapsBound()(using Context): TypeBoundsTree =
+    TypeBoundsTree(
       Select(scalaDot(nme.caps), tpnme.CapSet),
-      Nil, tpnme.retainsCap)
+      makeRetaining(
+        Select(scalaDot(nme.caps), tpnme.CapSet),
+        Nil, tpnme.retainsCap))
 
   def makeConstructor(tparams: List[TypeDef], vparamss: List[List[ValDef]], rhs: Tree = EmptyTree)(using Context): DefDef =
     DefDef(nme.CONSTRUCTOR, joinParams(tparams, vparamss), TypeTree(), rhs)
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureAnnotation.scala b/compiler/src/dotty/tools/dotc/cc/CaptureAnnotation.scala
@@ -42,6 +42,7 @@ case class CaptureAnnotation(refs: CaptureSet, boxed: Boolean)(cls: Symbol) exte
       case cr: TermRef => ref(cr)
       case cr: TermParamRef => untpd.Ident(cr.paramName).withType(cr)
       case cr: ThisType => This(cr.cls)
+      // TODO: Will crash if the type is an annotated type, for example `cap?`
     }
     val arg = repeated(elems, TypeTree(defn.AnyType))
     New(symbol.typeRef, arg :: Nil)
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -93,12 +93,19 @@ trait CaptureRef extends TypeProxy, ValueType:
   final def invalidateCaches() =
     myCaptureSetRunId = NoRunId
 
-  /** x subsumes x
-   *   this subsumes this.f
+  /**  x subsumes x
+   *   x =:= y       ==>  x subsumes y
+   *   x subsumes y  ==>  x subsumes y.f
    *   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
+   *   X = CapSet^cx, exists rx in cx, rx subsumes y     ==>  X subsumes y
+   *   Y = CapSet^cy, forall ry in cy, x subsumes ry     ==>  x subsumes Y
+   *   X: CapSet^c1...CapSet^c2, (CapSet^c1) subsumes y  ==>  X subsumes y
+   *   Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2)  ==>  x subsumes Y
+   *   Contains[X, y]  ==>  X subsumes y
+   *
+   *   TODO: Document cases with more comments.
    */
   final def subsumes(y: CaptureRef)(using Context): Boolean =
 
@@ -135,14 +142,29 @@ trait CaptureRef extends TypeProxy, ValueType:
               case _ => false
           || viaInfo(y.info)(subsumingRefs(this, _))
         case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
+        case y: TypeRef if y.derivesFrom(defn.Caps_CapSet) =>
+          // The upper and lower bounds don't have to be in the form of `CapSet^{...}`.
+          // They can be other capture set variables, which are bounded by `CapSet`,
+          // like `def test[X^, Y^, Z >: X <: Y]`.
+          y.info match
+            case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
+            case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
+        case CapturingType(parent, refs) if parent.derivesFrom(defn.Caps_CapSet) =>
+          refs.elems.forall(this.subsumes)
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
         case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
         case x: TermParamRef => subsumesExistentially(x, y)
-        case x: TypeRef if x.symbol.info.derivesFrom(defn.Caps_CapSet) =>
-          x.captureSetOfInfo.elems.exists(_.subsumes(y))
-        case x: TypeRef => assumedContainsOf(x).contains(y)
+        case x: TypeRef if assumedContainsOf(x).contains(y) => true
+        case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
+          x.info match
+            case TypeBounds(lo: CaptureRef, _) =>
+              lo.subsumes(y)
+            case _ =>
+              x.captureSetOfInfo.elems.exists(_.subsumes(y))
+        case CapturingType(parent, refs) if parent.derivesFrom(defn.Caps_CapSet) =>
+          refs.elems.exists(_.subsumes(y))
         case _ => false
   end subsumes
 
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -161,7 +161,9 @@ sealed abstract class CaptureSet extends Showable:
     def debugInfo(using Context) = i"$this accountsFor $x, which has capture set ${x.captureSetOfInfo}"
     def test(using Context) = reporting.trace(debugInfo):
       elems.exists(_.subsumes(x))
-      || !x.isMaxCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
+      || !x.isMaxCapability
+        && !x.derivesFrom(defn.Caps_CapSet)
+        && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
     comparer match
       case comparer: ExplainingTypeComparer => comparer.traceIndented(debugInfo)(test)
       case _ => test
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -866,7 +866,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           if others.accountsFor(ref) then
             report.warning(em"redundant capture: $dom already accounts for $ref", pos)
 
-        if ref.captureSetOfInfo.elems.isEmpty && !ref.derivesFrom(defn.Caps_Capability) then
+        if ref.captureSetOfInfo.elems.isEmpty
+            && !ref.derivesFrom(defn.Caps_Capability)
+            && !ref.derivesFrom(defn.Caps_CapSet) then
           val deepStr = if ref.isReach then " deep" else ""
           report.error(em"$ref cannot be tracked since its$deepStr capture set is empty", pos)
         check(parent.captureSet, parent)
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -2240,7 +2240,7 @@ object Parsers {
       atSpan(in.offset):
         if in.isIdent(nme.UPARROW) && Feature.ccEnabled then
           in.nextToken()
-          TypeBoundsTree(EmptyTree, makeCapsBound())
+          makeCapsBound()
         else
           TypeBoundsTree(bound(SUPERTYPE), bound(SUBTYPE))
 
diff --git a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
@@ -21,6 +21,7 @@ import config.MigrationVersion
 import config.Printers.refcheck
 import reporting.*
 import Constants.Constant
+import cc.stripCapturing
 
 object RefChecks {
   import tpd.*
@@ -84,7 +85,7 @@ object RefChecks {
    *  (Forwarding tends to hide problems by binding parameter names).
    */
   private def upwardsThisType(cls: Symbol)(using Context) = cls.info match {
-    case ClassInfo(_, _, _, _, tp: Type) if (tp ne cls.typeRef) && !cls.isOneOf(FinalOrModuleClass) =>
+    case ClassInfo(_, _, _, _, tp: Type) if (tp.stripCapturing ne cls.typeRef) && !cls.isOneOf(FinalOrModuleClass) =>
       SkolemType(cls.appliedRef).withName(nme.this_)
     case _ =>
       cls.thisType
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
@@ -22,18 +22,18 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
   /** A type constraint expressing that the capture set `C` needs to contain
    *  the capability `R`
    */
-  sealed trait Contains[C <: CapSet @retainsCap, R <: Singleton]
+  sealed trait Contains[+C >: CapSet <: CapSet @retainsCap, R <: Singleton]
 
   /** The only implementation of `Contains`. The constraint that `{R} <: C` is
    *  added separately by the capture checker.
    */
-  given containsImpl[C <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
+  given containsImpl[C >: CapSet <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
 
   /** A wrapper indicating a type variable in a capture argument list of a
    *  @retains annotation. E.g. `^{x, Y^}` is represented as `@retains(x, capsOf[Y])`.
    */
   @compileTimeOnly("Should be be used only internally by the Scala compiler")
-  def capsOf[CS]: Any = ???
+  def capsOf[CS >: CapSet <: CapSet @retainsCap]: Any = ???
 
   /** Reach capabilities x* which appear as terms in @retains annotations are encoded
    *  as `caps.reachCapability(x)`. When converted to CaptureRef types in capture sets
diff --git a/scala2-library-cc/src/scala/collection/Stepper.scala b/scala2-library-cc/src/scala/collection/Stepper.scala
@@ -53,7 +53,7 @@ trait Stepper[@specialized(Double, Int, Long) +A] {
     *
     * See method `trySplit` in [[java.util.Spliterator]].
     */
-  def trySplit(): Stepper[A]
+  def trySplit(): Stepper[A]^{this}
 
   /** Returns an estimate of the number of elements of this Stepper, or [[Long.MaxValue]]. See
     * method `estimateSize` in [[java.util.Spliterator]].
@@ -71,15 +71,15 @@ trait Stepper[@specialized(Double, Int, Long) +A] {
     * a [[java.util.Spliterator.OfInt]] (which is a `Spliterator[Integer]`) in the subclass [[IntStepper]]
     * (which is a `Stepper[Int]`).
     */
-  def spliterator[B >: A]: Spliterator[_]
+  def spliterator[B >: A]: Spliterator[_]^{this}
 
   /** Returns a Java [[java.util.Iterator]] corresponding to this Stepper.
     *
     * Note that the return type is `Iterator[_]` instead of `Iterator[A]` to allow returning
     * a [[java.util.PrimitiveIterator.OfInt]] (which is a `Iterator[Integer]`) in the subclass
     * [[IntStepper]] (which is a `Stepper[Int]`).
     */
-  def javaIterator[B >: A]: JIterator[_]
+  def javaIterator[B >: A]: JIterator[_]^{this}
 
   /** Returns an [[Iterator]] corresponding to this Stepper. Note that Iterators corresponding to
     * primitive Steppers box the elements.
diff --git a/tests/neg-custom-args/captures/capset-bound2.scala b/tests/neg-custom-args/captures/capset-bound2.scala
@@ -0,0 +1,13 @@
+import caps.*
+
+class IO
+
+def f[C^](io: IO^{C^}) = ???
+
+def test =
+  f[CapSet](???)
+  f[CapSet^{}](???)
+  f[CapSet^](???)
+  f[Nothing](???) // error
+  f[String](???) // error
+  
diff --git a/tests/neg-custom-args/captures/capset-members.scala b/tests/neg-custom-args/captures/capset-members.scala
@@ -0,0 +1,30 @@
+import caps.*
+
+trait Abstract[X^]:
+  type C >: X <: CapSet^
+  // Don't test the return type using Unit, because it is a pure type.
+  def boom(): AnyRef^{C^}
+
+class Concrete extends Abstract[CapSet^{}]:
+  type C = CapSet^{}
+  // TODO: Why do we get error without the return type here?
+  def boom(): AnyRef = new Object
+
+class Concrete2 extends Abstract[CapSet^{}]:
+  type C = CapSet^{}
+  def boom(): AnyRef^ = new Object // error
+
+class Concrete3 extends Abstract[CapSet^{}]:
+  def boom(): AnyRef = new Object
+
+class Concrete4(a: AnyRef^) extends Abstract[CapSet^{a}]:
+  type C = CapSet // error
+  def boom(): AnyRef^{a} = a // error
+
+class Concrete5(a: AnyRef^, b: AnyRef^) extends Abstract[CapSet^{a}]:
+  type C = CapSet^{a}
+  def boom(): AnyRef^{b} = b // error
+
+class Concrete6(a: AnyRef^, b: AnyRef^) extends Abstract[CapSet^{a}]:
+  def boom(): AnyRef^{b} = b // error
+  
diff --git a/tests/neg-custom-args/captures/capture-parameters.scala b/tests/neg-custom-args/captures/capture-parameters.scala
@@ -0,0 +1,9 @@
+import caps.*
+
+class C
+
+def test[X^, Y^, Z >: X <: Y](x: C^{X^}, y: C^{Y^}, z: C^{Z^}) =
+  val x2z: C^{Z^} = x
+  val z2y: C^{Y^} = z
+  val x2y: C^{Y^} = x // error
+  
diff --git a/tests/neg-custom-args/captures/capture-poly.scala b/tests/neg-custom-args/captures/capture-poly.scala
@@ -3,7 +3,7 @@ import caps.*
 trait Foo extends Capability
 
 trait CaptureSet:
-  type C <: CapSet^
+  type C >: CapSet <: CapSet^
 
 def capturePoly[C^](a: Foo^{C^}): Foo^{C^} = a
 def capturePoly2(c: CaptureSet)(a: Foo^{c.C^}): Foo^{c.C^} = a
diff --git a/tests/neg-custom-args/captures/i21868.scala b/tests/neg-custom-args/captures/i21868.scala
@@ -1,14 +1,13 @@
 import caps.*
 
 trait AbstractWrong:
-    type C <: CapSet
-    def boom(): Unit^{C^} // error
+  type C <: CapSet
+  def f(): Unit^{C^} // error
 
-trait Abstract:
-    type C <: CapSet^
-    def boom(): Unit^{C^}
-
-class Concrete extends Abstract:
-    type C = Nothing
-    def boom() = () // error
+trait Abstract1:
+  type C >: CapSet <: CapSet^
+  def f(): Unit^{C^}
 
+// class Abstract2:
+//   type C^
+//   def f(): Unit^{C^}
diff --git a/tests/neg-custom-args/captures/i21868b.scala b/tests/neg-custom-args/captures/i21868b.scala
@@ -0,0 +1,49 @@
+import language.experimental.modularity
+import caps.*
+
+class IO
+
+class File
+
+trait Abstract:
+  type C >: CapSet <: CapSet^
+  def f(file: File^{C^}): Unit
+
+class Concrete1 extends Abstract:
+  type C = CapSet
+  def f(file: File) = ()
+
+class Concrete2(io: IO^) extends Abstract:
+  type C = CapSet^{io}
+  def f(file: File^{io}) = ()
+
+class Concrete3(io: IO^) extends Abstract:
+  type C = CapSet^{io}
+  def f(file: File) = () // error
+
+trait Abstract2(tracked val io: IO^):
+  type C >: CapSet <: CapSet^{io}
+  def f(file: File^{C^}): Unit
+
+class Concrete4(io: IO^) extends Abstract2(io):
+  type C = CapSet
+  def f(file: File) = ()
+
+class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
+  type C = CapSet^{io2} // error
+  def f(file: File^{io2}) = ()
+
+trait Abstract3[X^]:
+  type C >: CapSet <: X
+  def f(file: File^{C^}): Unit
+
+class Concrete6(io: IO^) extends Abstract3[CapSet^{io}]:
+  type C = CapSet
+  def f(file: File) = ()
+
+class Concrete7(io1: IO^, io2: IO^) extends Abstract3[CapSet^{io1}]:
+  type C = CapSet^{io2} // error
+  def f(file: File^{io2}) = ()
+
+class Concrete8(io1: IO^, io2: IO^) extends Abstract3[CapSet^{io1}]:
+  def f(file: File^{io2}) = () // error
diff --git a/tests/neg-custom-args/captures/i22005.scala b/tests/neg-custom-args/captures/i22005.scala
@@ -0,0 +1,8 @@
+import caps.*
+
+class IO
+class File(io: IO^)
+
+class Handler[C^]:
+  def f(file: File^): File^{C^} = file // error
+  def g(file: File^{C^}): File^ = file // ok
diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check
@@ -1,19 +1,19 @@
--- Error: tests/neg-custom-args/captures/use-capset.scala:7:50 ---------------------------------------------------------
-7 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
+-- Error: tests/neg-custom-args/captures/use-capset.scala:5:50 ---------------------------------------------------------
+5 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
   |                                               ^^^^^^^
   |                                               Capture set parameter C leaks into capture scope of method g.
   |                                               To allow this, the type C should be declared with a @use annotation
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:22 -----------------------------------
-13 |  val _: () -> Unit = h // error: should be ->{io}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:22 -----------------------------------
+11 |  val _: () -> Unit = h // error: should be ->{io}
    |                      ^
    |                      Found:    (h : () ->{io} Unit)
    |                      Required: () -> Unit
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:15:50 -----------------------------------
-15 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 -----------------------------------
+13 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
    |                                                  ^^
-   |                                          Found:    (h2 : () ->? (x$0: List[box Object^]^{}) ->{io} Object^{io})
-   |                                          Required: () -> List[box Object^{io}] -> Object^{io}
+   |                                      Found:    (h2 : () ->? (x$0: List[box Object^{io}]^{}) ->{io} Object^{io})
+   |                                      Required: () -> List[box Object^{io}] -> Object^{io}
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/use-capset.scala b/tests/neg-custom-args/captures/use-capset.scala
@@ -1,7 +1,5 @@
 import caps.{use, CapSet}
 
-
-
 def f[C^](@use xs: List[Object^{C^}]): Unit = ???
 
 private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
diff --git a/tests/neg/cc-poly-2.check b/tests/neg/cc-poly-2.check
@@ -1,10 +1,3 @@
--- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:13:15 ---------------------------------------------------------
-13 |    f[Nothing](d) // error
-   |               ^
-   |               Found:    (d : Test.D^)
-   |               Required: Test.D
-   |
-   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:14:19 ---------------------------------------------------------
 14 |    f[CapSet^{c1}](d) // error
    |                   ^
diff --git a/tests/neg/cc-poly-2.scala b/tests/neg/cc-poly-2.scala
@@ -10,7 +10,7 @@ object Test:
 
   def test(c1: C, c2: C) =
     val d: D^ = D()
-    f[Nothing](d) // error
+    // f[Nothing](d) // already ruled out at typer
     f[CapSet^{c1}](d) // error
     val x = f(d)
     val _: D^{c1} = x // error
diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs.scala
diff --git a/tests/pos/cc-poly-source-capability.scala b/tests/pos/cc-poly-source-capability.scala

Original file line number	Diff line number	Diff line change
`@@ -42,6 +42,7 @@ case class CaptureAnnotation(refs: CaptureSet, boxed: Boolean)(cls: Symbol) exte`
`42`	`42`	`case cr: TermRef => ref(cr)`
`43`	`43`	`case cr: TermParamRef => untpd.Ident(cr.paramName).withType(cr)`
`44`	`44`	`case cr: ThisType => This(cr.cls)`
	`45`	+ // TODO: Will crash if the type is an annotated type, for example `cap?`
`45`	`46`	`}`
`46`	`47`	`val arg = repeated(elems, TypeTree(defn.AnyType))`
`47`	`48`	`New(symbol.typeRef, arg :: Nil)`