Improve error message for failures of mutable capture sets

Author: odersky

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

@@ -553,7 +553,7 @@ object CaptureSet:
         false
       }
 
-    def toReader()(using Context) = false
+    def toReader()(using Context) = failWith(MutAdaptFailure(this))
 
     def addDependent(cs: CaptureSet)(using Context, VarState) = true
 
@@ -721,7 +721,7 @@ object CaptureSet:
         res
 
     final def toReader()(using Context) =
-      if isConst then false // TODO add error note when failing?
+      if isConst then failWith(MutAdaptFailure(this))
       else
         mutability = Reader
         TypeComparer.logUndoAction(() => mutability = Mutable)
@@ -1205,6 +1205,7 @@ object CaptureSet:
    */
   case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote
 
+  /** Failure indicating that `elem` cannot be included in `cs` */
   case class IncludeFailure(cs: CaptureSet, elem: Capability, levelError: Boolean = false) extends ErrorNote, Showable:
     private var myTrace: List[CaptureSet] = cs :: Nil
 
@@ -1224,6 +1225,14 @@ object CaptureSet:
           else i"$elem cannot be included in $cs"
   end IncludeFailure
 
+  /** Failure indicating that a read-only capture set of a mutable type cannot be
+   *  widened to an exclusive set.
+   *  @param  cs    the exclusive set in question
+   *  @param  lo    the lower type of the orginal type comparison, or NoType if not known
+   *  @param  hi    the upper type of the orginal type comparison, or NoType if not known
+   */
+  case class MutAdaptFailure(cs: CaptureSet, lo: Type = NoType, hi: Type = NoType) extends ErrorNote
+
   /** A VarState serves as a snapshot mechanism that can undo
    *  additions of elements or super sets if an operation fails
    */

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

@@ -25,6 +25,7 @@ import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
 import reporting.{trace, Message, OverrideError}
 import Annotations.Annotation
 import Capabilities.*
+import dotty.tools.dotc.cc.CaptureSet.MutAdaptFailure
 
 /** The capture checker */
 object CheckCaptures:
@@ -1265,7 +1266,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     private def errorNotes(notes: List[TypeComparer.ErrorNote])(using Context): Addenda =
       val printableNotes = notes.filter:
         case IncludeFailure(_, _, true) => true
-        case _: ExistentialSubsumesFailure => true
+        case _: ExistentialSubsumesFailure | _: MutAdaptFailure => true
         case _ => false
       if printableNotes.isEmpty then NothingToAdd
       else new Addenda:
@@ -1287,6 +1288,10 @@ class CheckCaptures extends Recheck, SymTransformer:
                 else " since that capability is not a SharedCapability"
               i"""the existential capture root in ${ex.originalBinder.resType}
                  |cannot subsume the capability $other$since"""
+            case MutAdaptFailure(cs, lo, hi) =>
+              def ofType(tp: Type) = if tp.exists then i"of the mutable type $tp" else "of a mutable type"
+              i"""$cs is an exclusive capture set ${ofType(hi)},
+                 |it cannot subsume a read-only capture set ${ofType(lo)}."""
           i"""
              |Note that ${msg.toString}"""
 

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

@@ -2902,7 +2902,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       if tp1.derivesFromMutable && !tp2.derivesFromMutable
       then refs1.readOnly
       else refs1
-    subCaptures(refs1Adapted, refs2)
+    val subc = subCaptures(refs1Adapted, refs2)
+    if !subc then
+      errorNotes match
+        case (level, CaptureSet.MutAdaptFailure(cs, NoType, NoType)) :: rest =>
+          errorNotes = (level, CaptureSet.MutAdaptFailure(cs, tp1, tp2)) :: rest
+        case _ =>
+    subc
     && (tp1.isBoxedCapturing == tp2.isBoxedCapturing)
         || refs1.subCaptures(CaptureSet.empty, makeVarState())
 

tests/neg-custom-args/captures/ro-mut-conformance.check

@@ -11,4 +11,7 @@
    |
    |                     where:    ^ refers to a fresh root capability in the type of value t
    |
+   |                     Note that {cap} is an exclusive capture set of the mutable type Ref^,
+   |                     it cannot subsume a read-only capture set of the mutable type (a : Ref).
+   |
    | longer explanation available when compiling with `-explain`