Treat empty capture set on a Mutable type specially

Needed to invalidate the relation

    C^{} <: C^

for Mutable types C

Author: odersky

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

@@ -67,7 +67,7 @@ sealed abstract class CaptureSet extends Showable:
    *   - take mutability from the set's sources (for DerivedVars)
    *   - compute mutability on demand based on mutability of elements (for Consts)
    */
-  def associateWithMutable()(using Context): Unit
+  def associateWithMutable()(using Context): CaptureSet
 
   /** Is this capture set constant (i.e. not an unsolved capture variable)?
    *  Solved capture variables count as constant.
@@ -566,9 +566,16 @@ object CaptureSet:
   val emptyRefs: Refs = SimpleIdentitySet.empty
 
   /** The empty capture set `{}` */
-  @sharable // sharable since the set is empty, so setMutable is a no-op
+  @sharable // sharable since the set is empty, so mutability won't be set
   val empty: CaptureSet.Const = Const(emptyRefs)
 
+  /** The empty capture set `{}` of a Mutable type, with Reader status */
+  @sharable // sharable since the set is empty, so mutability won't be set
+  val emptyOfMutable: CaptureSet.Const =
+    val cs = Const(emptyRefs)
+    cs.mutability = Mutability.Reader
+    cs
+
   /** The universal capture set `{cap}` */
   def universal(using Context): Const =
     Const(SimpleIdentitySet(GlobalCap))
@@ -623,9 +630,11 @@ object CaptureSet:
 
     private var isComplete = true
 
-    def associateWithMutable()(using Context): Unit =
-      if !elems.isEmpty then
+    def associateWithMutable()(using Context): CaptureSet =
+      if elems.isEmpty then emptyOfMutable
+      else
         isComplete = false // delay computation of Mutability status
+        this
 
     override def mutability(using Context): Mutability =
       if !isComplete then
@@ -718,8 +727,9 @@ object CaptureSet:
      */
     var deps: Deps = SimpleIdentitySet.empty
 
-    def associateWithMutable()(using Context): Unit =
+    def associateWithMutable()(using Context): CaptureSet =
       mutability = Mutable
+      this
 
     def isConst(using Context) = solved >= ccState.iterationId
     def isAlwaysEmpty(using Context) = isConst && elems.isEmpty
@@ -1036,7 +1046,7 @@ object CaptureSet:
     addAsDependentTo(source)
 
     /** Mutability is same as in source, except for readOnly */
-    override def associateWithMutable()(using Context): Unit = ()
+    override def associateWithMutable()(using Context): CaptureSet = this
 
     override def mutableToReader(origin: CaptureSet)(using Context): Boolean =
       super.mutableToReader(origin)

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

@@ -40,9 +40,10 @@ object CapturingType:
       case parent @ CapturingType(parent1, refs1) if boxed || !parent.isBoxed =>
         apply(parent1, refs ++ refs1, boxed)
       case _ =>
-        if parent.derivesFromMutable then refs.associateWithMutable()
-        refs.adoptClassifier(parent.inheritedClassifier)
-        AnnotatedType(parent, CaptureAnnotation(refs, boxed)(defn.RetainsAnnot))
+        val refs1 =
+          if parent.derivesFromMutable then refs.associateWithMutable() else refs
+        refs1.adoptClassifier(parent.inheritedClassifier)
+        AnnotatedType(parent, CaptureAnnotation(refs1, boxed)(defn.RetainsAnnot))
 
   /** An extractor for CapturingTypes. Capturing types are recognized if
    *   - the annotation is a CaptureAnnotation and we are not past CheckCapturingPhase, or

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

@@ -1484,6 +1484,9 @@ class CheckCaptures extends Recheck, SymTransformer:
           else
             trace.force(i"rechecking $tree with pt = $pt", recheckr, show = true):
               super.recheck(tree, pt)
+        catch case ex: AssertionError =>
+          println(i"error while rechecking $tree against $pt")
+          throw ex
         finally curEnv = saved
       if tree.isTerm && !pt.isBoxedCapturing && pt != LhsProto then
         markFree(res.boxedCaptureSet, tree)

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

@@ -862,7 +862,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         def compareCapturing: Boolean =
           val refs1 = tp1.captureSet
           try
-            if refs1.isAlwaysEmpty then recur(tp1, parent2)
+            if refs1.isAlwaysEmpty && refs1.mutability == CaptureSet.Mutability.Ignored then
+              recur(tp1, parent2)
             else
               // The singletonOK branch is because we sometimes have a larger capture set in a singleton
               // than in its underlying type. An example is `f: () -> () ->{x} T`, which might be

tests/neg-custom-args/captures/mut-widen-empty.check

@@ -0,0 +1,12 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-widen-empty.scala:12:24 ------------------------------
+12 |  val c: Arr[String]^ = b  // error
+   |                        ^
+   |                        Found:    (b : Arr[String]^{})
+   |                        Required: Arr[String]^
+   |
+   |                        Note that {cap} is an exclusive capture set of the mutable type Arr[String]^,
+   |                        it cannot subsume a read-only capture set of the mutable type Arr[String]^{}.
+   |
+   |                        where:    ^ and cap refer to a fresh root capability in the type of value c
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/mut-widen-empty.scala

@@ -0,0 +1,14 @@
+import caps.*
+
+class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
+  private val arr: Array[T] = new Array[T](len)
+  def get(i: Int): T = arr(i)
+  update def update(i: Int, x: T): Unit = arr(i) = x
+
+
+def test2 =
+  val a = Arr[String](2)
+  val b: Arr[String]^{} = ???
+  val c: Arr[String]^ = b  // error
+  c(2) = "a"   // boom!
+