Improve error messages for scope extrusion errors (#24318)

Several improvements for error messages signalling level errors.

- Level errors now come first in the message, followed by the actual
type mismatch
 - More information on owners 
 - Merge ExistentialSubsumes notes with IncludeFailure notes.

Also, several refactorings that simplify and unify the schemas for
processing error notes.

Author: odersky

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

@@ -5,7 +5,6 @@ package cc
 import core.*
 import Types.*, Symbols.*, Contexts.*, Decorators.*
 import util.{SimpleIdentitySet, EqHashMap}
-import typer.ErrorReporting.Addenda
 import util.common.alwaysTrue
 import scala.collection.mutable
 import CCState.*
@@ -787,12 +786,9 @@ object Capabilities:
               && prefixAllowsAddHidden
               && vs.addHidden(x.hiddenSet, y)
         case x: ResultCap =>
-          val result = y match
+          y match
             case y: ResultCap => vs.unify(x, y)
             case _ => y.derivesFromShared
-          if !result then
-            TypeComparer.addErrorNote(CaptureSet.ExistentialSubsumesFailure(x, y))
-          result
         case GlobalCap =>
           y match
             case GlobalCap => true
@@ -900,7 +896,7 @@ object Capabilities:
           case _ => c1
 
     def showAsCapability(using Context) =
-      i"capability ${ctx.printer.toTextCapability(this).show}"
+      i"${ctx.printer.toTextCapability(this).show}"
 
     def toText(printer: Printer): Text = printer.toTextCapability(this)
   end Capability

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

@@ -15,6 +15,7 @@ import CaptureSet.VarState
 import Capabilities.*
 import StdNames.nme
 import config.Feature
+import dotty.tools.dotc.core.NameKinds.TryOwnerName
 
 /** Attachment key for capturing type trees */
 private val Captures: Key[CaptureSet] = Key()
@@ -624,9 +625,13 @@ extension (sym: Symbol)
     || sym.info.hasAnnotation(defn.ConsumeAnnot)
 
   def qualString(prefix: String)(using Context): String =
+    if !sym.exists then "" else i" $prefix ${sym.ownerString}"
+
+  def ownerString(using Context): String =
     if !sym.exists then ""
-    else if sym.isAnonymousFunction then i" $prefix enclosing function"
-    else i" $prefix $sym"
+    else if sym.isAnonymousFunction then i"an enclosing function"
+    else if sym.name.is(TryOwnerName) then i"an enclosing try expression"
+    else sym.show
 
 extension (tp: AnnotatedType)
   /** Is this a boxed capturing type? */

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

@@ -10,12 +10,11 @@ import annotation.threadUnsafe
 import annotation.constructorOnly
 import annotation.internal.sharable
 import reporting.trace
+import reporting.Message.Note
 import printing.{Showable, Printer}
 import printing.Texts.*
 import util.{SimpleIdentitySet, Property, EqHashMap}
-import typer.ErrorReporting.Addenda
 import scala.collection.{mutable, immutable}
-import TypeComparer.ErrorNote
 import CCState.*
 import TypeOps.AvoidMap
 import compiletime.uninitialized
@@ -161,8 +160,8 @@ sealed abstract class CaptureSet extends Showable:
 
   final def keepAlways: Boolean = this.isInstanceOf[EmptyWithProvenance]
 
-  def failWith(fail: TypeComparer.ErrorNote)(using Context): false =
-    TypeComparer.addErrorNote(fail)
+  def failWith(note: Note)(using Context): false =
+    TypeComparer.addErrorNote(note)
     false
 
   /** Try to include an element in this capture set.
@@ -1302,20 +1301,8 @@ object CaptureSet:
   /** A TypeMap that is the identity on capabilities */
   trait IdentityCaptRefMap extends TypeMap
 
-  /** A value of this class is produced and added as a note to ccState
-   *  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:
-    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:
+  case class IncludeFailure(cs: CaptureSet, elem: Capability, levelError: Boolean = false) extends Note, Showable:
     private var myTrace: List[CaptureSet] = cs :: Nil
 
     def trace: List[CaptureSet] = myTrace
@@ -1324,36 +1311,77 @@ object CaptureSet:
       res.myTrace = cs1 :: this.myTrace
       res
 
-    def description(using Context): String =
-      def why =
-        val reasons = cs.elems.toList.collect:
-          case c: FreshCap if !c.acceptsLevelOf(elem) =>
-            i"$elem${elem.levelOwner.qualString("in")} is not visible from $c${c.ccOwner.qualString("in")}"
-          case c: FreshCap if !elem.tryClassifyAs(c.hiddenSet.classifier) =>
-            i"$c is classified as ${c.hiddenSet.classifier} but $elem is not"
-        if reasons.isEmpty then ""
-        else reasons.mkString("\nbecause ", "\nand ", "")
-      cs match
-        case cs: Var =>
-          if !cs.levelOK(elem) then
-            val levelStr = elem match
-              case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}\n"
-              case _ => " "
-            i"""${elem.showAsCapability}${levelStr}cannot be included in outer capture set $cs"""
-          else if !elem.tryClassifyAs(cs.classifier) then
-            i"""${elem.showAsCapability} is not classified as ${cs.classifier}, therefore it
-                |cannot be included in capture set $cs of ${cs.classifier.name} elements"""
-          else if cs.isBadRoot(elem) then
-            elem match
-              case elem: FreshCap =>
-                i"""local ${elem.showAsCapability} created in ${elem.ccOwner}
-                  |cannot be included in outer capture set $cs"""
-              case _ =>
-                i"universal ${elem.showAsCapability} cannot be included in capture set $cs"
-          else
-            i"${elem.showAsCapability} cannot be included in capture set $cs"
-        case _ =>
-          i"${elem.showAsCapability} is not included in capture set $cs$why"
+    override def showAsPrefix(using Context) = cs match
+      case cs: Var =>
+        !cs.levelOK(elem)
+        || cs.isBadRoot(elem) && elem.isInstanceOf[FreshCap]
+      case _ =>
+        false
+
+    /** An include failure F1 covers another include failure F2 unless F2
+     *  strictly subsumes F1, which means they describe the same capture sets
+     *  and the element in F2 is more specific than the element in F1.
+     */
+    override def covers(other: Note)(using Context) = other match
+      case other @ IncludeFailure(cs1, elem1, _) =>
+        val strictlySubsumes =
+          cs.elems == cs1.elems
+          && elem1.singletonCaptureSet.mightSubcapture(elem.singletonCaptureSet)
+        !strictlySubsumes
+      case _ => false
+
+    def trailing(msg: String)(using Context): String =
+      i"""
+         |
+         |Note that $msg."""
+
+    def leading(msg: String)(using Context): String =
+      i"""$msg.
+         |The leakage occurred when trying to match the following types:
+         |
+         |"""
+
+    def render(using Context): String = cs match
+      case cs: Var =>
+        def ownerStr =
+          if !cs.description.isEmpty then "" else cs.owner.qualString("which is owned by")
+        if !cs.levelOK(elem) then
+          val outlivesStr = elem match
+            case ref: TermRef => i"${ref.symbol.maybeOwner.qualString("defined in")} outlives its scope:\n"
+            case _ => " outlives its scope: "
+          leading:
+            i"""Capability ${elem.showAsCapability}${outlivesStr}it leaks into outer capture set $cs$ownerStr"""
+        else if !elem.tryClassifyAs(cs.classifier) then
+          trailing:
+            i"""capability ${elem.showAsCapability} is not classified as ${cs.classifier}, therefore it
+              |cannot be included in capture set $cs of ${cs.classifier.name} elements"""
+        else if cs.isBadRoot(elem) then
+          elem match
+            case elem: FreshCap =>
+              leading:
+                i"""Local capability ${elem.showAsCapability} created in ${elem.ccOwner} outlives its scope:
+                    |It leaks into outer capture set $cs$ownerStr"""
+            case _ =>
+              trailing:
+                i"universal capability ${elem.showAsCapability} cannot be included in capture set $cs"
+        else
+          trailing:
+            i"capability ${elem.showAsCapability} cannot be included in capture set $cs"
+      case _ =>
+        def why =
+          val reasons = cs.elems.toList.collect:
+            case c: FreshCap if !c.acceptsLevelOf(elem) =>
+              i"$elem${elem.levelOwner.qualString("in")} is not visible from $c${c.ccOwner.qualString("in")}"
+            case c: FreshCap if !elem.tryClassifyAs(c.hiddenSet.classifier) =>
+              i"$c is classified as ${c.hiddenSet.classifier} but ${elem.showAsCapability} is not"
+            case c: ResultCap if !c.subsumes(elem) =>
+              val toAdd = if elem.isTerminalCapability then "" else " since that capability is not a SharedCapability"
+              i"$c, which is existentially bound in ${c.originalBinder.resType}, cannot subsume ${elem.showAsCapability}$toAdd"
+          if reasons.isEmpty then ""
+          else reasons.mkString("\nbecause ", "\nand ", "")
+
+        trailing:
+          i"capability ${elem.showAsCapability} is not included in capture set $cs$why"
 
     override def toText(printer: Printer): Text =
       inContext(printer.printerContext):
@@ -1371,11 +1399,19 @@ 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:
-    def description(using Context): String =
+  case class MutAdaptFailure(cs: CaptureSet, lo: Type = NoType, hi: Type = NoType) extends Note:
+
+    def render(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)}"""
+      i"""
+         |
+         |Note that $cs is an exclusive capture set ${ofType(hi)},
+         |it cannot subsume a read-only capture set ${ofType(lo)}."""
+
+    // Show only one failure of this kind
+    override def covers(other: Note)(using Context) =
+      other.isInstanceOf[MutAdaptFailure]
+  end MutAdaptFailure
 
   /** 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

@@ -14,18 +14,19 @@ import typer.ForceDegree
 import typer.Inferencing.isFullyDefined
 import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents, OverridingPairsChecker}
 import typer.Checking.{checkBounds, checkAppliedTypesIn}
-import typer.ErrorReporting.{Addenda, NothingToAdd, err}
+import typer.ErrorReporting.err
 import typer.ProtoTypes.{LhsProto, WildcardSelectionProto, SelectionProto}
 import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property}
 import util.chaining.tap
 import transform.{Recheck, PreRecheck, CapturedVars}
 import Recheck.*
 import scala.collection.mutable
-import CaptureSet.{withCaptureSetsExplained, IncludeFailure, ExistentialSubsumesFailure, MutAdaptFailure}
+import CaptureSet.{withCaptureSetsExplained, IncludeFailure, MutAdaptFailure}
 import CCState.*
 import StdNames.nme
 import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
 import reporting.{trace, Message, OverrideError}
+import reporting.Message.Note
 import Annotations.Annotation
 import Capabilities.*
 import Mutability.*
@@ -200,9 +201,6 @@ object CheckCaptures:
     && !sym.isOneOf(DeferredOrTermParamOrAccessor)
     && !sym.hasAnnotation(defn.UntrackedCapturesAnnot)
 
-  private def ownerStr(owner: Symbol)(using Context): String =
-    if owner.isAnonymousFunction then "enclosing function" else owner.show
-
   trait CheckerAPI:
     /** Complete symbol info of a val or a def */
     def completeDef(tree: ValOrDefDef, sym: Symbol, completer: LazyType)(using Context): Type
@@ -421,7 +419,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             case (fail: IncludeFailure) :: _ => fail.cs
             case _ => target
           def msg(provisional: Boolean) =
-            def toAdd: String = errorNotes(otherNotes).toAdd.mkString
+            def toAdd: String = otherNotes.map(_.render).mkString
             def descr: String =
               val d = realTarget.description
               if d.isEmpty then provenance else ""
@@ -1246,7 +1244,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           // too annoying. This is a hole since a defualt getter's result type
           // might leak into a type variable.
 
-      def fail(tree: Tree, expected: Type, addenda: Addenda): Unit =
+      def fail(tree: Tree, expected: Type, notes: List[Note]): Unit =
         def maybeResult = if sym.is(Method) then " result" else ""
         report.error(
           em"""$sym needs an explicit$maybeResult type because the inferred type does not conform to
@@ -1256,7 +1254,7 @@ class CheckCaptures extends Recheck, SymTransformer:
               | Externally visible type: $expected""",
           tree.srcPos)
 
-      def addenda(expected: Type) = Addenda:
+      def addendum(expected: Type) = Note:
         def result = if tree.isInstanceOf[ValDef] then"" else " result"
         i"""
           |
@@ -1275,7 +1273,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             val expected = tpt.tpe.dropAllRetains
             todoAtPostCheck += { () =>
               withCapAsRoot:
-                testAdapted(tp, expected, tree.rhs, addenda(expected))(fail)
+                testAdapted(tp, expected, tree.rhs, addendum(expected) :: Nil)(fail)
                 // The check that inferred <: expected is done after recheck so that it
                 // does not interfere with normal rechecking by constraining capture set variables.
             }
@@ -1482,34 +1480,27 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     type BoxErrors = mutable.ListBuffer[Message] | Null
 
-    private def errorNotes(notes: List[TypeComparer.ErrorNote])(using Context): Addenda =
-      if notes.isEmpty then NothingToAdd
-      else new Addenda:
-        override def toAdd(using Context) = notes.map: note =>
-          i"""
-             |
-             |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
+     *  mapping of a capability in contravariant position to the empty set because
      *  the original result type of the map was not itself a capability.
      */
-    private def addApproxAddenda(using Context) =
-      new TypeAccumulator[Addenda]:
-        def apply(add: Addenda, t: Type) = t match
+    private def addApproxAddenda(using Context): TypeAccumulator[List[Note]] =
+      new TypeAccumulator:
+        def apply(notes: List[Note], t: Type) = t match
           case CapturingType(t, CaptureSet.EmptyWithProvenance(ref, mapped)) =>
             /* val (origCore, kind) = original match
               case tp @ AnnotatedType(parent, ann) if ann.hasSymbol(defn.ReachCapabilityAnnot) =>
                 (parent, " deep")
               case _ =>
                 (original, "")*/
-            add ++ Addenda:
+            Note:
                 i"""
                    |
                    |Note that a capability $ref in a capture set appearing in contravariant position
                    |was mapped to $mapped which is not a capability. Therefore, it was under-approximated to the empty set."""
+            :: notes
           case _ =>
-            foldOver(add, t)
+            foldOver(notes, t)
 
     /** Massage `actual` and `expected` types before checking conformance.
      *  Massaging is done by the methods following this one:
@@ -1518,8 +1509,8 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  If the resulting types are not compatible, try again with an actual type
      *  where local capture roots are instantiated to root variables.
      */
-    override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type =
-      try testAdapted(actual, expected, tree, addenda)(err.typeMismatch)
+    override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, notes: List[Note])(using Context): Type =
+      try testAdapted(actual, expected, tree, notes: List[Note])(err.typeMismatch)
       catch case ex: AssertionError =>
         println(i"error while checking $tree: $actual against $expected")
         throw ex
@@ -1534,8 +1525,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           case _ => NoType
       case _ => NoType
 
-    inline def testAdapted(actual: Type, expected: Type, tree: Tree, addenda: Addenda)
-        (fail: (Tree, Type, Addenda) => Unit)(using Context): Type =
+    inline def testAdapted(actual: Type, expected: Type, tree: Tree, notes: List[Note])
+        (fail: (Tree, Type, List[Note]) => Unit)(using Context): Type =
 
       var expected1 = alignDependentFunction(expected, actual.stripCapturing)
       val falseDeps = expected1 ne expected
@@ -1582,11 +1573,12 @@ class CheckCaptures extends Recheck, SymTransformer:
         }
 
       TypeComparer.compareResult(tryCurrentType || tryWidenNamed) match
-        case TypeComparer.CompareResult.Fail(notes) =>
+        case TypeComparer.CompareResult.Fail(cmpNotes) =>
           capt.println(i"conforms failed for ${tree}: $actual vs $expected")
           if falseDeps then expected1 = unalignFunction(expected1)
-          fail(tree.withType(actualBoxed), expected1,
-            addApproxAddenda(addenda ++ errorNotes(notes), expected1))
+          val toAdd0 = notes ++ cmpNotes
+          val toAdd1 = addApproxAddenda(toAdd0, expected1)
+          fail(tree.withType(actualBoxed), expected1, toAdd1)
           actual
         case /*OK*/ _ =>
           if debugSuccesses then tree match