Augment exclusivity tests with required flag

Author: odersky

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

@@ -441,11 +441,13 @@ object Capabilities:
     /** An exclusive capability is a capability that derives
      *  indirectly from a maximal capability without going through
      *  a read-only capability or a capability classified as SharedCapability first.
+     *  @param required  if true, exclusivity can be obtained by setting the mutability
+     *                   status of some capture set variable from Ignored to Writer.
      */
-    final def isExclusive(using Context): Boolean =
+    final def isExclusive(required: Boolean = false)(using Context): Boolean =
       !isReadOnly
       && !classifier.derivesFrom(defn.Caps_SharedCapability)
-      && (isTerminalCapability || captureSetOfInfo.isExclusive)
+      && (isTerminalCapability || captureSetOfInfo.isExclusive(required))
 
     /** Similar to isExlusive, but also includes capabilties with capture
      *  set variables in their info whose status is still open.

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

@@ -148,8 +148,20 @@ sealed abstract class CaptureSet extends Showable:
 
   final def isAlwaysReadOnly(using Context): Boolean = isConst && isReadOnly
 
-  final def isExclusive(using Context): Boolean =
-    elems.exists(_.isExclusive)
+  /** Is capture set exclusive? If `required` is true, a variable capture set
+   *  is forced to Writer mutability which makes it exclusive. Otherwise a set
+   *  is exclusive if one of its elements is exclusive.
+   *  Possible issue: If required is true, and the set is a constant, with
+   *  multiple elements that each have a variable capture set, then we make
+   *  the set exclusive by updating the first such variable capture set with
+   *  Ignore mutability to have Write mutability. That makes the effect
+   *  order dependent.
+   */
+  def isExclusive(required: Boolean = false)(using Context): Boolean =
+    if required && !isConst && mutability == Ignored then
+      mutability = Writer
+    mutability == Writer
+    || elems.exists(_.isExclusive(required))
 
   /** Similar to isExclusive, but also includes capture set variables
    *  with unknown status.

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

@@ -572,7 +572,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
       def checkReadOnlyMethod(included: CaptureSet, meth: Symbol): Unit =
         included.checkAddedElems: elem =>
-          if elem.isExclusive then
+          if elem.isExclusive() then
             report.error(
                 em"""Read-only $meth accesses exclusive capability $elem;
                     |$meth should be declared an update method to allow this.""",
@@ -2256,10 +2256,9 @@ class CheckCaptures extends Recheck, SymTransformer:
             val pcls = parent.nuType.classSymbol
             val parentIsExclusive =
               if parent.isType then
-                capturedVars(pcls).isExclusive
-                || captureSetImpliedByFields(pcls.asClass, parent.nuType).isExclusive
-
-              else parent.nuType.captureSet.isExclusive
+                capturedVars(pcls).isExclusive()
+                || captureSetImpliedByFields(pcls.asClass, parent.nuType).isExclusive()
+              else parent.nuType.captureSet.isExclusive()
             if parentIsExclusive then
               report.error(
                 em"""illegal inheritance: $cls which extends `Stateful` is not allowed to also extend $pcls

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

@@ -83,24 +83,32 @@ object Mutability:
         if mbr.symbol.is(Method) then mbr.symbol.isUpdateMethod
         else !mbr.symbol.hasAnnotation(defn.UntrackedCapturesAnnot)
 
-    /** OK, except if `tp` extends `Stateful` but `tp`'s capture set is non-exclusive */
-    private def exclusivity(using Context): Exclusivity =
+    /** OK, except if `tp` extends `Stateful` but `tp`'s capture set is non-exclusive
+     *  @param required  if true, exclusivity can be obtained by setting the mutability
+     *                   status of some capture set variable from Ignored to Writer.
+     */
+    private def exclusivity(required: Boolean)(using Context): Exclusivity =
       if tp.derivesFrom(defn.Caps_Stateful) then
         tp match
-          case tp: Capability if tp.isExclusive => Exclusivity.OK
-          case _ => tp.captureSet.exclusivity(tp)
+          case tp: Capability if tp.isExclusive(required) => Exclusivity.OK
+          case _ =>
+            if tp.captureSet.isExclusive(required) then Exclusivity.OK
+            else Exclusivity.ReadOnly(tp)
       else Exclusivity.OK
 
-    /** Test conditions (1) and (2) listed in `adaptReadOnly` below */
-    private def exclusivityInContext(using Context): Exclusivity = tp match
+    /** Test conditions (1) and (2) listed in `adaptReadOnly` below
+     *  @param required  if true, exclusivity can be obtained by setting the mutability
+     *                   status of some capture set variable from Ignored to Writer.
+     */
+    private def exclusivityInContext(required: Boolean = false)(using Context): Exclusivity = tp match
       case tp: ThisType =>
         if tp.derivesFrom(defn.Caps_Stateful)
         then ctx.owner.inExclusivePartOf(tp.cls)
         else Exclusivity.OK
       case tp @ TermRef(prefix: Capability, _) =>
-        prefix.exclusivityInContext.andAlso(tp.exclusivity)
+        prefix.exclusivityInContext(required).andAlso(tp.exclusivity(required))
       case _ =>
-        tp.exclusivity
+        tp.exclusivity(required)
 
     def expectsReadOnly(using Context): Boolean = tp match
       case tp: PathSelectionProto =>
@@ -109,10 +117,6 @@ object Mutability:
         tp.isValueType
         && (!tp.isStatefulType || tp.captureSet.mutability == CaptureSet.Mutability.Reader)
 
-  extension (cs: CaptureSet)
-    private def exclusivity(tp: Type)(using Context): Exclusivity =
-      if cs.isExclusive then Exclusivity.OK else Exclusivity.ReadOnly(tp)
-
   extension (ref: TermRef | ThisType)
     /** Map `ref` to `ref.readOnly` if its type extends Mutble, and one of the
      *  following is true:
@@ -122,7 +126,7 @@ object Mutability:
      */
     def adjustReadOnly(pt: Type)(using Context): Capability = {
       if ref.derivesFromStateful
-          && (pt.expectsReadOnly || ref.exclusivityInContext != Exclusivity.OK)
+          && (pt.expectsReadOnly || ref.exclusivityInContext() != Exclusivity.OK)
       then ref.readOnly
       else ref
     }.showing(i"Adjust RO $ref vs $pt = $result", capt)
@@ -131,7 +135,7 @@ object Mutability:
    *  of a field of `qualType`.
    */
   def checkUpdate(qualType: Type, pos: SrcPos)(msg: => String)(using Context): Unit =
-    qualType.exclusivityInContext match
+    qualType.exclusivityInContext(required = true) match
       case Exclusivity.OK =>
       case err =>
         report.error(em"$msg\nsince ${err.description(qualType)}.", pos)
@@ -238,8 +242,8 @@ object Mutability:
       case improved @ CapturingType(parent, refs)
       if parent.derivesFrom(defn.Caps_Stateful)
           && expected.isValueType
-          && refs.isExclusive
-          && !original.exclusivityInContext.isOK =>
+          && refs.isExclusive()
+          && !original.exclusivityInContext().isOK =>
         improved.derivedCapturingType(parent, refs.readOnly)
           .showing(i"Adapted readonly $improved for $tree with original = $original in ${ctx.owner} --> $result", capt)
       case improved =>

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

@@ -260,7 +260,7 @@ object SepCheck:
        */
       def common(refs1: Refs, refs2: Refs) =
         refs1.filter: ref =>
-          ref.isExclusive && refs2.exists(_.stripReadOnly.covers(ref))
+          ref.isExclusive() && refs2.exists(_.stripReadOnly.covers(ref))
         ++
         refs1
           .filter:

tests/neg-custom-args/captures/ref-with-file.check

@@ -1,5 +1,5 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ref-with-file.scala:15:12 --------------------------------
-15 |  withFile: f => // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ref-with-file.scala:18:12 --------------------------------
+18 |  withFile: f => // error
    |            ^
    |Found:    (f: File^'s1) ->'s2 Ref[File^'s3]^
    |Required: (f: File^²) => Ref[File^'s4]^'s5
@@ -10,12 +10,12 @@
    |          ^   refers to a fresh root capability classified as Unscoped in the type of value r
    |          ^²  refers to the universal root capability
    |          cap is a fresh root capability created in anonymous function of type (f: File^'s1): Ref[File^'s3]^ of parameter parameter f² of method $anonfun
-16 |    val r = Ref(f)
-17 |    r
+19 |    val r = Ref(f)
+20 |    r
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ref-with-file.scala:18:12 --------------------------------
-18 |  withFile: f => // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ref-with-file.scala:21:12 --------------------------------
+21 |  withFile: f => // error
    |            ^
    |Found:    (f: File^'s6) ->'s7 (??? : -> Nothing)
    |Required: (f: File^) => Nothing
@@ -25,7 +25,22 @@
    |where:    =>  refers to a fresh root capability created in method Test when checking argument to parameter op of method withFile
    |          ^   refers to the universal root capability
    |          cap is a fresh root capability created in anonymous function of type (f: File^'s6): (??? : -> Nothing) of parameter parameter f² of method $anonfun
-19 |    val r = Ref(f)
-20 |    ???
+22 |    val r = Ref(f)
+23 |    ???
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ref-with-file.scala:25:18 --------------------------------
+25 |  withFileAndRef: (f, r: Ref[String]^) => // error
+   |                  ^
+   |Capability cap outlives its scope: it leaks into outer capture set 's8 which is owned by method Test.
+   |The leakage occurred when trying to match the following types:
+   |
+   |Found:    (f: File^'s9, r: Ref[String]^) ->'s10 Ref[String]^
+   |Required: (f: File^, r: Ref[String]^) => Ref[String]^'s8
+   |
+   |where:    =>        refers to a fresh root capability created in method Test when checking argument to parameter op of method withFileAndRef
+   |          ^ and cap refer to the universal root capability
+26 |    r.put(f.read())
+27 |    r
    |
    | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/ref-with-file.scala

@@ -11,6 +11,9 @@ class File:
 def withFile[T](op: (f: File^) => T): T =
   op(new File)
 
+def withFileAndRef[T](op: (f: File^, r: Ref[String]^) => T): T =
+  op(File(), Ref(""))
+
 def Test =
   withFile: f => // error
     val r = Ref(f)
@@ -19,5 +22,7 @@ def Test =
     val r = Ref(f)
     ???
 
-
+  withFileAndRef: (f, r: Ref[String]^) => // error
+    r.put(f.read())
+    r
 

tests/new/test.scala

@@ -1,13 +1,27 @@
-class Ref[T](init: T) extends caps.Mutable:
-  var x: T = init
-  update def set(x: T) = this.x = x
-
-class Ref2[T](init: T) extends caps.Mutable:
-  val x = Ref[T](init)
-
-def test =
-  val r4 = () =>
-    val r = Ref2(22)
-    r
-  //val _: Ref2[Int]^{r4*} = r4()
-  r4().x.set(33) // ok
+import caps.*
+
+class Ref[T](init: T) extends caps.Stateful, Unscoped:
+  var x = init
+  def get: T = x
+  update def put(y: T): Unit = x = y
+
+class File:
+  def read(): String = ???
+
+def withFile[T](op: (f: File^) => T): T =
+  op(new File)
+
+def withFileAndRef[T](op: (f: File^, r: Ref[String]^) => T): T =
+  op(File(), Ref(""))
+
+def Test =
+/*
+  withFileAndRef: (f, r: Ref[String]^) =>
+    r.put(f.read())
+*/
+
+  withFileAndRef: (f, r) =>
+    r.put(f.read())
+
+
+

tests/pos-custom-args/captures/ref-with-file.scala

@@ -11,9 +11,15 @@ class File:
 def withFile[T](op: (f: File^) => T): T =
   op(new File)
 
+def withFileAndRef[T](op: (f: File^, r: Ref[String]^) => T): T =
+  op(File(), Ref(""))
+
 def Test =
   withFile: f =>
     val r = Ref(f.read())
     r
+  withFileAndRef: (f, r: Ref[String]^) =>
+    r.put(f.read())
+