More detailed notes in error messages.

We now always give a reason in a TypeMismatch about which capture set inclusion failed.

Author: odersky

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

@@ -692,6 +692,9 @@ object CaptureSet:
      */
     private[CaptureSet] var rootLimit: Symbol | Null = null
 
+    def isBadRoot(elem: Capability)(using Context): Boolean =
+      isBadRoot(rootLimit, elem)
+
     private var myClassifier: ClassSymbol = defn.AnyClass
     def classifier: ClassSymbol = myClassifier
 
@@ -749,7 +752,7 @@ object CaptureSet:
         assert(elem.isWellformed, elem)
         assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState])
         includeElem(elem)
-        if isBadRoot(rootLimit, elem) then
+        if isBadRoot(elem) then
           rootAddedHandler()
         val normElem = if isMaybeSet then elem else elem.stripMaybe
         // assert(id != 5 || elems.size != 3, this)
@@ -778,7 +781,7 @@ object CaptureSet:
             case _ => foldOver(b, t)
       find(false, binder)
 
-    private def levelOK(elem: Capability)(using Context): Boolean = elem match
+    def levelOK(elem: Capability)(using Context): Boolean = elem match
       case _: FreshCap =>
         !level.isDefined
         || ccState.symLevel(elem.ccOwner) <= level
@@ -1246,7 +1249,13 @@ object CaptureSet:
    *  when a subsumes check decides that an existential variable `ex` cannot be
    *  instantiated to the other capability `other`.
    */
-  case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote
+  case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote:
+    def description(using Context): String =
+      def reason =
+        if other.isTerminalCapability then ""
+        else " since that capability is not a `Sharable` capability"
+      i"""the existential capture root in ${ex.originalBinder.resType}
+         |cannot subsume the capability $other$reason."""
 
   /** Failure indicating that `elem` cannot be included in `cs` */
   case class IncludeFailure(cs: CaptureSet, elem: Capability, levelError: Boolean = false) extends ErrorNote, Showable:
@@ -1258,6 +1267,29 @@ object CaptureSet:
       res.myTrace = cs1 :: this.myTrace
       res
 
+    def description(using Context): String = cs match
+      case cs: Var =>
+        if !cs.levelOK(elem) then
+          val levelStr = elem match
+            case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}"
+            case _ => ""
+          i"""capability ${elem}$levelStr
+              |cannot be included in outer capture set $cs"""
+        else if !elem.tryClassifyAs(cs.classifier) then
+          i"""capability ${elem} is not classified as ${cs.classifier}, therefore it
+              |cannot be included in capture set $cs of ${cs.classifier} elements"""
+        else if cs.isBadRoot(elem) then
+          elem match
+            case elem: FreshCap =>
+              i"""local capability $elem created in ${elem.ccOwner}
+                 |cannot be included in outer capture set $cs"""
+            case _ =>
+              i"universal capability $elem cannot be included in capture set $cs"
+        else
+          i"capability $elem cannot be included in capture set $cs"
+      case _ =>
+        i"capability $elem is not included in capture set $cs"
+
     override def toText(printer: Printer): Text =
       inContext(printer.printerContext):
         if levelError then
@@ -1274,7 +1306,11 @@ object CaptureSet:
    *  @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
+  case class MutAdaptFailure(cs: CaptureSet, lo: Type = NoType, hi: Type = NoType) extends ErrorNote:
+    def description(using Context): String =
+      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)}."""
 
   /** 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

@@ -1278,37 +1278,11 @@ class CheckCaptures extends Recheck, SymTransformer:
     type BoxErrors = mutable.ListBuffer[Message] | Null
 
     private def errorNotes(notes: List[TypeComparer.ErrorNote])(using Context): Addenda =
-      val printableNotes = notes.filter:
-        case IncludeFailure(_, _, true) => true
-        case _: ExistentialSubsumesFailure | _: MutAdaptFailure => true
-        case _ => false
-      if printableNotes.isEmpty then NothingToAdd
+      if notes.isEmpty then NothingToAdd
       else new Addenda:
-        override def toAdd(using Context) = printableNotes.map: note =>
-          val msg = note match
-            case IncludeFailure(cs, ref, _) =>
-              if ref.core.isCapOrFresh then
-                i"""the universal capability $ref
-                   |cannot be included in capture set $cs"""
-              else
-                val levelStr = ref match
-                  case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}"
-                  case _ => ""
-                i"""reference ${ref}$levelStr
-                    |cannot be included in outer capture set $cs"""
-            case ExistentialSubsumesFailure(ex, other) =>
-              def since =
-                if other.isTerminalCapability then ""
-                else " since that capability is not a `Sharable` capability"
-              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)}."""
+        override def toAdd(using Context) = notes.map: note =>
           i"""
-             |Note that ${msg.toString}"""
-
+             |Note that ${note.description}."""
 
     /** Addendas for error messages that show where we have under-approximated by
      *  mapping a a capability in contravariant position to the empty set because

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

@@ -3361,6 +3361,9 @@ object TypeComparer {
      */
     def kind: Class[?] = getClass
 
+    def description(using Context): String
+  end ErrorNote
+
   /** A richer compare result, returned by `testSubType` and `test`. */
   enum CompareResult:
     case OK, OKwithGADTUsed, OKwithOpaquesUsed

tests/neg-custom-args/captures/box-adapt-cases.check

@@ -3,12 +3,14 @@
    |          ^^^^^^^^^^^^^^^^
    |          Found:    (cap: Cap^{io}) ->{io} Int
    |          Required: Cap^{io} -> Int
+   |          Note that capability (io : Cap^) is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:29:10 ------------------------------
 29 |  x.value(cap => cap.use())  // error
    |          ^^^^^^^^^^^^^^^^
    |          Found:    (cap: Cap^?) ->{io, fs} Int
    |          Required: Cap^{io, fs} ->{io} Int
+   |          Note that capability (fs : Cap^) is not included in capture set {io}.
    |
    | longer explanation available when compiling with `-explain`

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

@@ -12,18 +12,22 @@
    |
    |where:    ?=> refers to a fresh root capability created in method test when checking argument to parameter ff of method h
    |
+   |Note that capability (cap1 : Cap) is not included in capture set {cap2}.
+   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:19:5 ----------------------------------------
 19 |  h(g()) // error
    |    ^^^
    |    Found:    () ?->{cap2} I^?
    |    Required: () ?->{cap1} I
+   |    Note that capability (cap2 : Cap) is not included in capture set {cap1}.
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:22:5 ----------------------------------------
 22 |  h2(() => g())() // error
    |     ^^^^^^^^^
    |     Found:    () ->{cap2} I^?
    |     Required: () ->{cap1} I
+   |     Note that capability (cap2 : Cap) is not included in capture set {cap1}.
    |
    | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/capt-depfun.check

@@ -6,4 +6,6 @@
    |
    |                                         where:    => refers to a fresh root capability in the type of value dc
    |
+   |                                         Note that capability (y : C^) is not included in capture set {}.
+   |
    | longer explanation available when compiling with `-explain`

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

@@ -3,20 +3,23 @@
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |  Found:    () ->{x} C^?
   |  Required: () -> C
+  |  Note that capability (x : C^) is not included in capture set {}.
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:8:2 ------------------------------------------
 8 |  () => if x == null then y else y  // error
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |  Found:    () ->{x} C^?
   |  Required: Matchable
+  |  Note that capability (x : C^) is not included in capture set {}.
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:15:2 -----------------------------------------
 15 |  def f(y: Int) = if x == null then y else y  // error
    |  ^
    |  Found:    (y: Int) ->{x} Int
    |  Required: Matchable
+   |  Note that capability (x : C^) is not included in capture set {}.
 16 |  f
    |
    | longer explanation available when compiling with `-explain`
@@ -25,6 +28,7 @@
    |  ^
    |  Found:    A^{x}
    |  Required: A
+   |  Note that capability (x : C^) is not included in capture set {}.
 23 |    def m() = if x == null then y else y
 24 |  F(22)
    |
@@ -34,6 +38,7 @@
    |  ^
    |  Found:    A^{x}
    |  Required: A
+   |  Note that capability (x : C^) is not included in capture set {}.
 28 |    def m() = if x == null then y else y
    |
    | longer explanation available when compiling with `-explain`
@@ -52,6 +57,8 @@
    |
    |where:    ^ refers to a fresh root capability created in value z2 when checking argument to parameter a of method h
    |
+   |Note that capability (x : C^) is not included in capture set {}.
+   |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/capt1.scala:38:13 -------------------------------------------------------------
 38 |  val z3 = h[(() -> Cap) @retains[x.type]](() => x)(() => C())  // error

tests/neg-custom-args/captures/cc-existential-conformance.check

@@ -9,6 +9,8 @@
   |                                  x  is a value in method test
   |                                  x² is a reference to a value parameter
   |
+  |                        Note that capability <cap of (x: A): B^> is not included in capture set {cap}.
+  |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:9:29 --------------------
 9 |  val z: A -> (x: A) -> B^ = y // error
@@ -18,8 +20,7 @@
   |
   |                             where:    ^ refers to a root capability associated with the result type of (x: A): B^
   |
-  |                             Note that the existential capture root in B^
-  |                             cannot subsume the capability y* since that capability is not a `Sharable` capability
+  |                             Note that capability y* is not included in capture set {<cap of (x: A): B^>}.
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:13:19 -------------------
@@ -33,6 +34,8 @@
    |                             x  is a value in method test2
    |                             x² is a reference to a value parameter
    |
+   |                   Note that capability <cap of (x: A): B^> is not included in capture set {cap}.
+   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:14:24 -------------------
 14 |  val z: (x: A) -> B^ = y // error
@@ -42,7 +45,6 @@
    |
    |                        where:    ^ refers to a root capability associated with the result type of (x: A): B^
    |
-   |                        Note that the existential capture root in B^
-   |                        cannot subsume the capability y* since that capability is not a `Sharable` capability
+   |                        Note that capability y* is not included in capture set {<cap of (x: A): B^>}.
    |
    | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/cc-glb.check

@@ -3,5 +3,6 @@
   |                   ^^
   |                   Found:    (x1 : (Foo[T] & Foo[Any])^{io})
   |                   Required: Foo[T]
+  |                   Note that capability (io : Cap^) is not included in capture set {}.
   |
   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/cc-poly-2.check

@@ -6,11 +6,14 @@
    |
    |                   where:    ^ refers to a fresh root capability in the type of value d
    |
+   |                   Note that capability cap is not included in capture set {c1}.
+   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-poly-2.scala:16:20 ------------------------------------
 16 |    val _: D^{c1} = x // error
    |                    ^
    |                    Found:    (x : Test.D^{d})
    |                    Required: Test.D^{c1}
+   |                    Note that capability (d : Test.D^) is not included in capture set {c1}.
    |
    | longer explanation available when compiling with `-explain`