Implement and use central error notes logic in TypeComparer

Needs some adaption for subCaptures tests for now.

Author: odersky

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

@@ -3,7 +3,7 @@ package dotc
 package cc
 
 import core.*
-import CaptureSet.{CompareResult, CompareFailure, VarState}
+import CaptureSet.{CompareResult, VarState}
 import collection.mutable
 import reporting.Message
 import Contexts.Context
@@ -16,24 +16,6 @@ class CCState:
 
   // ------ Error diagnostics -----------------------------
 
-  /** 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 match
-      case res: CompareFailure => res.withNotes(notes)
-      case res => res
-    finally notes = saved
-
-  def testOK(op: => Boolean): CompareResult =
-    test(if op then CompareResult.OK else CompareResult.Fail(Nil))
-
   /** Warnings relating to upper approximations of capture sets with
    *  existentially bound variables.
    */

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

@@ -558,7 +558,7 @@ object Capabilities:
             case y: ResultCap => vs.unify(x, y)
             case _ => y.derivesFromSharedCapability
           if !result then
-            ccState.addNote(CaptureSet.ExistentialSubsumesFailure(x, y))
+            TypeComparer.addErrorNote(CaptureSet.ExistentialSubsumesFailure(x, y))
           result
         case GlobalCap =>
           y match

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

@@ -41,9 +41,6 @@ def depFun(args: List[Type], resultType: Type, isContextual: Boolean, paramNames
 /** An exception thrown if a @retains argument is not syntactically a Capability */
 class IllegalCaptureRef(tpe: Type)(using Context) extends Exception(tpe.show)
 
-/** A base trait for data producing addenda to error messages */
-trait ErrorNote
-
 /** The currently valid CCState */
 def ccState(using Context): CCState =
   Phases.checkCapturesPhase.asInstanceOf[CheckCaptures].ccState1

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

@@ -16,6 +16,7 @@ import util.{SimpleIdentitySet, Property}
 import typer.ErrorReporting.Addenda
 import util.common.alwaysTrue
 import scala.collection.{mutable, immutable}
+import TypeComparer.ErrorNote
 import CCState.*
 import TypeOps.AvoidMap
 import compiletime.uninitialized
@@ -242,7 +243,7 @@ sealed abstract class CaptureSet extends Showable:
     if result.isOK then
       addDependent(that)
     else
-      result.levelError.foreach(ccState.addNote)
+      result.levelError.foreach(TypeComparer.addErrorNote)
       varState.rollBack()
       result
       //.showing(i"subcaptures $this <:< $that = ${result.show}", capt)
@@ -960,6 +961,8 @@ object CaptureSet:
 
     //assert(id != 4)
 
+    description = i"elements subsumed by $owningCap"
+
     private def aliasRef: FreshCap | Null =
       if myElems.size == 1 then
         myElems.nth(0) match
@@ -1075,17 +1078,10 @@ object CaptureSet:
    */
   case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote
 
-  trait CompareFailure:
-    private var myErrorNotes: List[ErrorNote] = Nil
-    def errorNotes: List[ErrorNote] = myErrorNotes
-    def withNotes(notes: List[ErrorNote]): this.type =
-      myErrorNotes = notes
-      this
-
   enum CompareResult extends Showable:
     case OK
-    case Fail(trace: List[CaptureSet]) extends CompareResult, CompareFailure
-    case LevelError(cs: CaptureSet, elem: Capability) extends CompareResult, CompareFailure, ErrorNote
+    case Fail(trace: List[CaptureSet]) extends CompareResult, ErrorNote
+    case LevelError(cs: CaptureSet, elem: Capability) extends CompareResult, ErrorNote
 
     override def toText(printer: Printer): Text =
       inContext(printer.printerContext):

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, CompareResult, CompareFailure, ExistentialSubsumesFailure}
+import CaptureSet.{withCaptureSetsExplained, CompareResult, ExistentialSubsumesFailure}
 import CCState.*
 import StdNames.nme
 import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
@@ -352,11 +352,12 @@ class CheckCaptures extends Recheck, SymTransformer:
       assert(cs1.subCaptures(cs2).isOK, i"$cs1 is not a subset of $cs2")
 
     /** If `res` is not CompareResult.OK, report an error */
-    def checkOK(res: CompareResult, prefix: => String, added: Capability | CaptureSet, target: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context): Unit =
+    def checkOK(res: TypeComparer.CompareResult, prefix: => String, added: Capability | CaptureSet, target: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context): Unit =
       res match
-        case res: CompareFailure =>
+        case TypeComparer.CompareResult.Fail(notes) =>
+          val ((res: CompareResult) :: Nil, otherNotes) = notes.partition(_.isInstanceOf[CompareResult]): @unchecked
           def msg(provisional: Boolean) =
-            def toAdd: String = errorNotes(res.errorNotes).toAdd.mkString
+            def toAdd: String = errorNotes(otherNotes).toAdd.mkString
             def descr: String =
               val d = res.blocking.description
               if d.isEmpty then provenance else ""
@@ -377,18 +378,27 @@ class CheckCaptures extends Recheck, SymTransformer:
               report.error(msg(provisional = false), pos)
         case _ =>
 
+    def convertResult(op: => CompareResult)(using Context): TypeComparer.CompareResult =
+      TypeComparer.test:
+        op match
+          case res: TypeComparer.ErrorNote =>
+            TypeComparer.addErrorNote(res)
+            false
+          case CompareResult.OK =>
+            true
+
     /** Check subcapturing `{elem} <: cs`, report error on failure */
     def checkElem(elem: Capability, cs: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context) =
       checkOK(
-          ccState.test(elem.singletonCaptureSet.subCaptures(cs)),
+          convertResult(elem.singletonCaptureSet.subCaptures(cs)),
           i"$elem cannot be referenced here; it is not",
           elem, cs, 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(
-          ccState.test(cs1.subCaptures(cs2)),
+          convertResult(cs1.subCaptures(cs2)),
           if cs1.elems.size == 1 then i"reference ${cs1.elems.nth(0)}$cs1description is not"
           else i"references $cs1$cs1description are not all",
           cs1, cs2, pos, provenance)
@@ -1272,7 +1282,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     type BoxErrors = mutable.ListBuffer[Message] | Null
 
-    private def errorNotes(notes: List[ErrorNote])(using Context): Addenda =
+    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 =>
@@ -1336,20 +1346,20 @@ class CheckCaptures extends Recheck, SymTransformer:
       if actualBoxed eq actual then
         // Only `addOuterRefs` when there is no box adaptation
         expected1 = addOuterRefs(expected1, actual, tree.srcPos)
-      ccState.testOK(isCompatible(actualBoxed, expected1)) match
-        case CompareResult.OK =>
-          if debugSuccesses then tree match
-              case Ident(_) =>
-                println(i"SUCCESS $tree for $actual <:< $expected:\n${TypeComparer.explained(_.isSubType(actualBoxed, expected1))}")
-              case _ =>
-          actualBoxed
-        case fail: CompareFailure =>
+      TypeComparer.test(isCompatible(actualBoxed, expected1)) match
+        case TypeComparer.CompareResult.Fail(notes) =>
           capt.println(i"conforms failed for ${tree}: $actual vs $expected")
           err.typeMismatch(tree.withType(actualBoxed), expected1,
               addApproxAddenda(
-                  addenda ++ errorNotes(fail.errorNotes),
+                  addenda ++ errorNotes(notes),
                   expected1))
           actual
+        case /*OK*/ _ =>
+          if debugSuccesses then tree match
+              case Ident(_) =>
+                println(i"SUCCESS $tree for $actual <:< $expected:\n${TypeComparer.explained(_.isSubType(actualBoxed, expected1))}")
+              case _ =>
+          actualBoxed
     end checkConformsExpr
 
     /** Turn `expected` into a dependent function when `actual` is dependent. */

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

@@ -50,12 +50,17 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     opaquesUsed = false
     recCount = 0
     needsGc = false
+    maxErrorLevel = -1
+    errorNotes = Nil
     if Config.checkTypeComparerReset then checkReset()
 
   private var pendingSubTypes: util.MutableSet[(Type, Type)] | Null = null
   private var recCount = 0
   private var monitored = false
 
+  private var maxErrorLevel: Int = -1
+  private var errorNotes: List[(Int, ErrorNote)] = Nil
+
   private var needsGc = false
 
   private var canCompareAtoms: Boolean = true // used for internal consistency checking
@@ -148,7 +153,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   def testSubType(tp1: Type, tp2: Type): CompareResult =
     GADTused = false
     opaquesUsed = false
-    if !topLevelSubType(tp1, tp2) then CompareResult.Fail
+    if !topLevelSubType(tp1, tp2) then CompareResult.Fail(Nil)
     else if GADTused then CompareResult.OKwithGADTUsed
     else if opaquesUsed then CompareResult.OKwithOpaquesUsed // we cast on GADTused, so handles if both are used
     else CompareResult.OK
@@ -1584,10 +1589,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         ctx.gadtState.restore(savedGadt)
       val savedSuccessCount = successCount
       try
-        recCount += 1
-        if recCount >= Config.LogPendingSubTypesThreshold then monitored = true
-        val result = if monitored then monitoredIsSubType else firstTry
-        recCount -= 1
+        val result = inNestedLevel:
+          if recCount >= Config.LogPendingSubTypesThreshold then monitored = true
+          if monitored then monitoredIsSubType else firstTry
         if !result then restore()
         else if recCount == 0 && needsGc then
           state.gc()
@@ -1602,6 +1606,32 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         throw ex
   }
 
+  /** Run `op` in a recursion level (indicated by `recCount`) increased by one.
+   *  This affects when monitoring starts and how error notes are propagated.
+   *  On exit, error notes added at the current level are either
+   *   - promoted to the next outer level (in case of failure),
+   *   - cancelled (in case of success).
+   */
+  inline def inNestedLevel(inline op: Boolean): Boolean =
+    recCount += 1
+    val result = op
+    recCount -= 1
+    if maxErrorLevel > recCount then
+      if result then
+        maxErrorLevel = -1
+        errorNotes = errorNotes.filterConserve: p =>
+          val (level, note) = p
+          if level <= recCount then
+            if level > maxErrorLevel then maxErrorLevel = level
+            true
+          else false
+      else
+        errorNotes = errorNotes.mapConserve: p =>
+          val (level, note) = p
+          if level > recCount then (recCount, note) else p
+        maxErrorLevel = recCount
+    result
+
   private def nonExprBaseType(tp: Type, cls: Symbol)(using Context): Type =
     if tp.isInstanceOf[ExprType] then NoType
     else tp.baseType(cls)
@@ -3219,12 +3249,26 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
 
   def reduceMatchWith[T](op: MatchReducer => T)(using Context): T =
     inSubComparer(matchReducer)(op)
+
+  /** Add given ErrorNote note, provided there is not yet an error note with
+   *  the same class as `note`.
+   */
+  def addErrorNote(note: ErrorNote): Unit =
+    if errorNotes.forall(_._2.getClass != note.getClass) then
+      errorNotes = (recCount, note) :: errorNotes
+      assert(maxErrorLevel <= recCount)
+      maxErrorLevel = recCount
 }
 
 object TypeComparer {
 
+  /** A base trait for data producing addenda to error messages */
+  trait ErrorNote
+
+  /** A richer compare result, returned by `testSubType` and `test`. */
   enum CompareResult:
-    case OK, Fail, OKwithGADTUsed, OKwithOpaquesUsed
+    case OK, OKwithGADTUsed, OKwithOpaquesUsed
+    case Fail(errorNotes: List[ErrorNote])
 
   /** Class for unification variables used in `natValue`. */
   private class AnyConstantType extends UncachedGroundType with ValueType {
@@ -3393,6 +3437,22 @@ object TypeComparer {
 
   def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): CaptureSet.CompareResult =
     comparing(_.subCaptures(refs1, refs2, vs))
+
+  def inNestedLevel(op: => Boolean)(using Context): Boolean =
+    comparer.inNestedLevel(op)
+
+  def addErrorNote(note: ErrorNote)(using Context): Unit =
+    comparer.addErrorNote(note)
+
+  /** Run `op` on current type comparer, maping its Boolean result to
+   *  a CompareResult with possible outcomes OK and Fail(...)`. In case
+   *  of failure pass the accumulated errorNotes of this type comparer to
+   *  in the Fail value.
+   */
+  def test(op: => Boolean)(using Context): CompareResult =
+    comparing: comparer =>
+      if op then CompareResult.OK
+      else CompareResult.Fail(comparer.errorNotes.map(_._2))
 }
 
 object MatchReducer:

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -4581,7 +4581,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
             tree
           }
         else TypeComparer.testSubType(tree.tpe.widenExpr, pt) match
-          case CompareResult.Fail =>
+          case CompareResult.Fail(_) =>
             wtp match
               case wtp: MethodType => missingArgs(wtp)
               case _ =>

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

@@ -6,6 +6,10 @@
    |
    |                                         where:    => refers to a fresh root capability in the type of value dc
    |
+   |
+   |                                         Note that the existential capture root in Str^{x} => Str^{x}
+   |                                         cannot subsume the capability <cap of (x: C^): Str^{x} => Str^{x}>
+   |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/capt-depfun.scala:11:24 -------------------------------------------------------
 11 |  val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon