Refactor addenda generation

Avoid globally visible vars in CCState. Make sure notes don't leak from one test to another.

Author: odersky

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

@@ -16,7 +16,7 @@ import config.Feature
 import collection.mutable
 import CCState.*
 import reporting.Message
-import CaptureSet.VarState
+import CaptureSet.{VarState, CompareResult}
 
 /** Attachment key for capturing type trees */
 private val Captures: Key[CaptureSet] = Key()
@@ -76,19 +76,32 @@ def depFun(args: List[Type], resultType: Type, isContextual: Boolean, paramNames
 /** An exception thrown if a @retains argument is not syntactically a CaptureRef */
 class IllegalCaptureRef(tpe: Type)(using Context) extends Exception(tpe.show)
 
+/** A base trait for data producing addenda to error messages */
+trait ErrorNote
+
 /** Capture checking state, which is known to other capture checking components */
 class CCState:
 
-  /** The last pair of capture reference and capture set where
-   *  the reference could not be added to the set due to a level conflict.
-   */
-  var levelError: Option[CaptureSet.CompareResult.LevelError] = None
-
-  /** Optionally, a pair of an existential variable and another capability.
-   *  Set when a subsumes check decides that an existential variable cannot be
-   *  instantiated to the other capability.
-   */
-  var existentialSubsumesFailure: Option[(CaptureRef, CaptureRef)] = None
+  /** Error reprting notes produces since the last call to `test` */
+  var notes: List[ErrorNote] = Nil
+
+  def addNote(note: ErrorNote): Unit =
+    if !notes.exists(_.getClass == note.getClass) then
+      notes = note :: notes
+
+  def test(op: => CompareResult): CompareResult =
+    val saved = notes
+    notes = Nil
+    try op.withNotes(notes)
+    finally notes = saved
+
+  def testOK(op: => Boolean): CompareResult =
+    val saved = notes
+    notes = Nil
+    try
+      if op then CompareResult.OK
+      else CompareResult.Fail(Nil).withNotes(notes)
+    finally notes = saved
 
   /** Warnings relating to upper approximations of capture sets with
    *  existentially bound variables.

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

@@ -253,11 +253,10 @@ trait CaptureRef extends TypeProxy, ValueType:
       case root.Fresh(hidden) =>
         vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
         || !y.stripReadOnly.isCap && !yIsExistential && canAddHidden && vs.addHidden(hidden, y)
-      case root.Result(binder) =>
+      case x @ root.Result(binder) =>
         if y.derivesFromSharedCapability then true
         else
-          ccState.existentialSubsumesFailure =
-            ccState.existentialSubsumesFailure.orElse(Some(this, y))
+          ccState.addNote(CaptureSet.ExistentialSubsumesFailure(x, y))
           false
       case _ =>
         y match

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

@@ -233,7 +233,7 @@ sealed abstract class CaptureSet extends Showable:
     if result.isOK then
       addDependent(that)
     else
-      ccState.levelError = ccState.levelError.orElse(result.levelError)
+      result.levelError.foreach(ccState.addNote)
       varState.rollBack()
       result
       //.showing(i"subcaptures $this <:< $that = ${result.show}", capt)
@@ -1077,10 +1077,16 @@ object CaptureSet:
   /** A TypeMap that is the identity on capture references */
   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: root.Result, val other: CaptureRef) extends ErrorNote
+
   enum CompareResult extends Showable:
     case OK
     case Fail(trace: List[CaptureSet])
-    case LevelError(cs: CaptureSet, elem: CaptureRef)
+    case LevelError(cs: CaptureSet, elem: CaptureRef) extends CompareResult, ErrorNote
 
     override def toText(printer: Printer): Text =
       inContext(printer.printerContext):
@@ -1105,6 +1111,16 @@ object CaptureSet:
       case result: LevelError => Some(result)
       case _ => None
 
+    private var myErrorNotes: List[ErrorNote] = Nil
+
+    def errorNotes: List[ErrorNote] = myErrorNotes
+
+    def withNotes(notes: List[ErrorNote]): CompareResult = this match
+      case OK => OK
+      case _ =>
+        myErrorNotes = notes
+        this
+
     inline def andAlso(op: Context ?=> CompareResult)(using Context): CompareResult =
       if isOK then op else this
 
@@ -1412,24 +1428,4 @@ object CaptureSet:
             println(i"  ${cv.show.padTo(20, ' ')} :: ${cv.deps.toList}%, %")
       }
     else op
-
-  def levelErrors: Addenda = new Addenda:
-    override def toAdd(using Context) =
-      for CompareResult.LevelError(cs, ref) <- ccState.levelError.toList yield
-        ccState.levelError = None
-        if ref.stripReadOnly.isCapOrFresh then
-          def capStr = if ref.isReadOnly then "cap.rd" else "cap"
-          i"""
-            |
-            |Note that the universal capability `$capStr`
-            |cannot be included in capture set $cs"""
-        else
-          val levelStr = ref match
-            case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}"
-            case _ => ""
-          i"""
-            |
-            |Note that reference ${ref}$levelStr
-            |cannot be included in outer capture set $cs"""
-
 end CaptureSet

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

@@ -18,7 +18,7 @@ import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property}
 import transform.{Recheck, PreRecheck, CapturedVars}
 import Recheck.*
 import scala.collection.mutable
-import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult}
+import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult, ExistentialSubsumesFailure}
 import CCState.*
 import StdNames.nme
 import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
@@ -354,7 +354,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     def checkOK(res: CompareResult, prefix: => String, added: CaptureRef | CaptureSet, pos: SrcPos, provenance: => String = "")(using Context): Unit =
       if !res.isOK then
         inContext(root.printContext(added, res.blocking)):
-          def toAdd: String = CaptureSet.levelErrors.toAdd.mkString
+          def toAdd: String = errorNotes(res.errorNotes).toAdd.mkString
           def descr: String =
             val d = res.blocking.description
             if d.isEmpty then provenance else ""
@@ -363,15 +363,15 @@ class CheckCaptures extends Recheck, SymTransformer:
     /** Check subcapturing `{elem} <: cs`, report error on failure */
     def checkElem(elem: CaptureRef, cs: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context) =
       checkOK(
-          elem.singletonCaptureSet.subCaptures(cs),
+          ccState.test(elem.singletonCaptureSet.subCaptures(cs)),
           i"$elem cannot be referenced here; it is not",
           elem, pos, provenance)
 
     /** Check subcapturing `cs1 <: cs2`, report error on failure */
     def checkSubset(cs1: CaptureSet, cs2: CaptureSet, pos: SrcPos,
         provenance: => String = "", cs1description: String = "")(using Context) =
       checkOK(
-          cs1.subCaptures(cs2),
+          ccState.test(cs1.subCaptures(cs2)),
           if cs1.elems.size == 1 then i"reference ${cs1.elems.toList.head}$cs1description is not"
           else i"references $cs1$cs1description are not all",
           cs1, pos, provenance)
@@ -1210,27 +1210,29 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     type BoxErrors = mutable.ListBuffer[Message] | Null
 
-    private def boxErrorAddenda(boxErrors: BoxErrors) =
-      if boxErrors == null then NothingToAdd
+    private def errorNotes(notes: List[ErrorNote])(using Context): Addenda =
+      if notes.isEmpty then NothingToAdd
       else new Addenda:
-        override def toAdd(using Context): List[String] =
-          boxErrors.toList.map: msg =>
-            i"""
-              |
-              |Note that ${msg.toString}"""
-
-    private def existentialSubsumesFailureAddenda(using Context): Addenda =
-      ccState.existentialSubsumesFailure match
-        case Some((ex @ root.Result(binder), other)) =>
-          new Addenda:
-            override def toAdd(using Context): List[String] =
-              val ann = ex.rootAnnot
-              i"""
-                |
-                |Note that the existential capture root in ${ex.rootAnnot.originalBinder.resType}
+        override def toAdd(using Context) = notes.map: note =>
+          val msg = note match
+            case CompareResult.LevelError(cs, ref) =>
+              if ref.stripReadOnly.isCapOrFresh then
+                def capStr = if ref.isReadOnly then "cap.rd" else "cap"
+                i"""the universal capability `$capStr`
+                   |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) =>
+              i"""the existential capture root in ${ex.rootAnnot.originalBinder.resType}
                 |cannot subsume the capability $other"""
-              :: Nil
-        case _ => NothingToAdd
+          i"""
+             |
+             |Note that ${msg.toString}"""
+
 
     /** Addendas for error messages that show where we have under-approximated by
      *  mapping a a capture ref in contravariant position to the empty set because
@@ -1264,15 +1266,14 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type =
       var expected1 = alignDependentFunction(expected, actual.stripCapturing)
-      val boxErrors = new mutable.ListBuffer[Message]
-      val actualBoxed = adapt(actual, expected1, tree, boxErrors)
+      val actualBoxed = adapt(actual, expected1, tree)
       //println(i"check conforms $actualBoxed <<< $expected1")
 
       if actualBoxed eq actual then
         // Only `addOuterRefs` when there is no box adaptation
         expected1 = addOuterRefs(expected1, actual, tree.srcPos)
-      ccState.existentialSubsumesFailure = None
-      if isCompatible(actualBoxed, expected1) then
+      val result = ccState.testOK(isCompatible(actualBoxed, expected1))
+      if result.isOK then
         if debugSuccesses then tree match
             case Ident(_) =>
               println(i"SUCCESS $tree for $actual <:< $expected:\n${TypeComparer.explained(_.isSubType(actualBoxed, expected1))}")
@@ -1283,10 +1284,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         inContext(root.printContext(actualBoxed, expected1)):
           err.typeMismatch(tree.withType(actualBoxed), expected1,
               addApproxAddenda(
-                addenda
-                ++ CaptureSet.levelErrors
-                ++ boxErrorAddenda(boxErrors)
-                ++ existentialSubsumesFailureAddenda,
+                addenda ++ errorNotes(result.errorNotes),
                 expected1))
         actual
     end checkConformsExpr
@@ -1397,7 +1395,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      *
      *  @param alwaysConst  always make capture set variables constant after adaptation
      */
-    def adaptBoxed(actual: Type, expected: Type, tree: Tree, covariant: Boolean, alwaysConst: Boolean, boxErrors: BoxErrors)(using Context): Type =
+    def adaptBoxed(actual: Type, expected: Type, tree: Tree, covariant: Boolean, alwaysConst: Boolean)(using Context): Type =
 
       def recur(actual: Type, expected: Type, covariant: Boolean): Type =
 
@@ -1551,15 +1549,15 @@ class CheckCaptures extends Recheck, SymTransformer:
      *   - narrow nested captures of `x`'s underlying type to `{x*}`
      *   - do box adaptation
      */
-    def adapt(actual: Type, expected: Type, tree: Tree, boxErrors: BoxErrors)(using Context): Type =
+    def adapt(actual: Type, expected: Type, tree: Tree)(using Context): Type =
       if noWiden(actual, expected) then
         actual
       else
         val improvedVAR = improveCaptures(actual.widen.dealiasKeepAnnots, actual)
         val improved = improveReadOnly(improvedVAR, expected)
         val adapted = adaptBoxed(
             improved.withReachCaptures(actual), expected, tree,
-            covariant = true, alwaysConst = false, boxErrors)
+            covariant = true, alwaysConst = false)
         if adapted eq improvedVAR // no .rd improvement, no box-adaptation
         then actual               // might as well use actual instead of improved widened
         else adapted.showing(i"adapt $actual vs $expected = $adapted", capt)
@@ -1585,7 +1583,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             try
               curEnv = Env(clazz, EnvKind.NestedInOwner, capturedVars(clazz), outer0 = curEnv)
               val adapted =
-                adaptBoxed(actual, expected1, tree, covariant = true, alwaysConst = true, null)
+                adaptBoxed(actual, expected1, tree, covariant = true, alwaysConst = true)
               actual match
                 case _: MethodType =>
                   // We remove the capture set resulted from box adaptation for method types,