Use addenda mechanism to report level violations

Author: odersky

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

@@ -11,10 +11,14 @@ import config.Printers.capt
 import util.Property.Key
 import tpd.*
 import config.Feature
+import collection.mutable
 
 private val Captures: Key[CaptureSet] = Key()
 private val BoxedType: Key[BoxedTypeCache] = Key()
 
+/** Attachment key for the nesting level cache */
+val ccState: Key[CCState] = Key()
+
 /** Switch whether unpickled function types and byname types should be mapped to
  *  impure types. With the new gradual typing using Fluid capture sets, this should
  *  be no longer needed. Also, it has bad interactions with pickling tests.
@@ -32,6 +36,11 @@ def allowUniversalInBoxed(using Context) =
 /** An exception thrown if a @retains argument is not syntactically a CaptureRef */
 class IllegalCaptureRef(tpe: Type) extends Exception
 
+class CCState:
+  val nestingLevels: mutable.HashMap[Symbol, Int] = new mutable.HashMap
+  val localRoots: mutable.HashMap[Symbol, CaptureRef] = new mutable.HashMap
+  var levelError: Option[(CaptureRef, CaptureSet)] = None
+
 extension (tree: Tree)
 
   /** Map tree with CaptureRef type to its type, throw IllegalCaptureRef otherwise */
@@ -269,7 +278,7 @@ extension (sym: Symbol)
   def ccNestingLevel(using Context): Int =
     if sym.exists then
       val lowner = sym.levelOwner
-      val cache = ctx.property(CheckCaptures.NestingLevels).get
+      val cache = ctx.property(ccState).get.nestingLevels
       cache.getOrElseUpdate(lowner,
         if lowner.isRoot then 0 else lowner.owner.ccNestingLevel + 1)
     else -1
@@ -278,7 +287,7 @@ extension (sym: Symbol)
    *  a capture checker is running.
    */
   def ccNestingLevelOpt(using Context): Option[Int] =
-    if ctx.property(CheckCaptures.NestingLevels).isDefined then
+    if ctx.property(ccState).isDefined then
       Some(ccNestingLevel)
     else None
 

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

@@ -13,6 +13,7 @@ import reporting.trace
 import printing.{Showable, Printer}
 import printing.Texts.*
 import util.{SimpleIdentitySet, Property, optional}, optional.{break, ?}
+import typer.ErrorReporting.Addenda
 import util.common.alwaysTrue
 import scala.collection.mutable
 import config.Config.ccAllowUnsoundMaps
@@ -421,6 +422,8 @@ object CaptureSet:
 
     var description: String = ""
 
+    private var triedElem: Option[CaptureRef] = None
+
     /** Record current elements in given VarState provided it does not yet
      *  contain an entry for this variable.
      */
@@ -457,9 +460,15 @@ object CaptureSet:
         (CompareResult.OK /: deps) { (r, dep) =>
           r.andAlso(dep.tryInclude(newElems, this))
         }
-      else widenCaptures(newElems) match
-        case Some(newElems1) => tryInclude(newElems1, origin)
-        case None => CompareResult.fail(this)
+      else
+        val res = widenCaptures(newElems) match
+          case Some(newElems1) => tryInclude(newElems1, origin)
+          case None => CompareResult.fail(this)
+        if !res.isOK then recordLevelError()
+        res
+
+    private def recordLevelError()(using Context): Unit =
+      ctx.property(ccState).get.levelError = Some((triedElem.get, this))
 
     private def levelsOK(elems: Refs)(using Context): Boolean =
       !elems.exists(_.ccNestingLevel > ownLevel)
@@ -469,8 +478,13 @@ object CaptureSet:
         (SimpleIdentitySet[CaptureRef]() /: elems): (acc, elem) =>
           if elem.ccNestingLevel <= ownLevel then acc + elem
           else if elem.isRootCapability then break()
-          else acc ++ widenCaptures(elem.captureSetOfInfo.elems).?
-      val resStr = res match
+          else
+            val saved = triedElem
+            triedElem = triedElem.orElse(Some(elem))
+            val res = acc ++ widenCaptures(elem.captureSetOfInfo.elems).?
+            triedElem = saved  // reset only in case of success, leave as is on error
+            res
+      def resStr = res match
         case Some(refs) => i"${refs.toList}"
         case None => "FAIL"
       capt.println(i"widen captures ${elems.toList} for $this at $owner = $resStr")
@@ -974,4 +988,17 @@ object CaptureSet:
             println(i"  ${cv.show.padTo(20, ' ')} :: ${cv.deps.toList}%, %")
       }
     else op
+
+  def levelErrors: Addenda = new Addenda:
+    override def toAdd(using Context) =
+      for
+        state <- ctx.property(ccState).toList
+        (ref, cs) <- state.levelError
+      yield
+        val level = ref.ccNestingLevel
+        i"""
+           |
+           |Note that reference ${ref}, defined at level $level
+           |cannot be included in outer capture set $cs, defined at level ${cs.owner.nestingLevel} in ${cs.owner}"""
+
 end CaptureSet

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

@@ -12,6 +12,7 @@ import ast.{tpd, untpd, Trees}
 import Trees.*
 import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents, OverridingPairsChecker}
 import typer.Checking.{checkBounds, checkAppliedTypesIn}
+import typer.ErrorReporting.Addenda
 import util.{SimpleIdentitySet, EqHashMap, SrcPos, Property}
 import transform.SymUtils.*
 import transform.{Recheck, PreRecheck}
@@ -189,9 +190,6 @@ object CheckCaptures:
   /** Attachment key for bodies of closures, provided they are values */
   val ClosureBodyValue = Property.Key[Unit]
 
-  /** Attachment key for the nesting level cache */
-  val NestingLevels = Property.Key[mutable.HashMap[Symbol, Int]]
-
 class CheckCaptures extends Recheck, SymTransformer:
   thisPhase =>
 
@@ -709,11 +707,11 @@ class CheckCaptures extends Recheck, SymTransformer:
   //   - Adapt box status and environment capture sets by simulating box/unbox operations.
 
     /** Massage `actual` and `expected` types using the methods below before checking conformance */
-    override def checkConformsExpr(actual: Type, expected: Type, tree: Tree)(using Context): Unit =
+    override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Unit =
       val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing)
       val actual1 = adaptBoxed(actual, expected1, tree.srcPos)
       //println(i"check conforms $actual1 <<< $expected1")
-      super.checkConformsExpr(actual1, expected1, tree)
+      super.checkConformsExpr(actual1, expected1, tree, addenda ++ CaptureSet.levelErrors)
 
     private def toDepFun(args: List[Type], resultType: Type, isContextual: Boolean)(using Context): Type =
       MethodType.companion(isContextual = isContextual)(args, resultType)
@@ -977,7 +975,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         traverseChildren(t)
 
     override def checkUnit(unit: CompilationUnit)(using Context): Unit =
-      inContext(ctx.withProperty(NestingLevels, Some(new mutable.HashMap[Symbol, Int]))):
+      inContext(ctx.withProperty(ccState, Some(new CCState))):
         Setup(preRecheckPhase, thisPhase, this)(ctx.compilationUnit.tpdTree)
         //println(i"SETUP:\n${Recheck.addRecheckedTypes.transform(ctx.compilationUnit.tpdTree)}")
         withCaptureSetsExplained:

compiler/src/dotty/tools/dotc/transform/Recheck.scala

@@ -15,6 +15,7 @@ import typer.ErrorReporting.err
 import typer.ProtoTypes.*
 import typer.TypeAssigner.seqLitType
 import typer.ConstFold
+import typer.ErrorReporting.{Addenda, NothingToAdd}
 import NamerOps.methodType
 import config.Printers.recheckr
 import util.Property
@@ -561,7 +562,7 @@ abstract class Recheck extends Phase, SymTransformer:
       case _ =>
         checkConformsExpr(tpe.widenExpr, pt.widenExpr, tree)
 
-    def checkConformsExpr(actual: Type, expected: Type, tree: Tree)(using Context): Unit =
+    def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda = NothingToAdd)(using Context): Unit =
       //println(i"check conforms $actual <:< $expected")
 
       def isCompatible(expected: Type): Boolean =
@@ -574,7 +575,7 @@ abstract class Recheck extends Phase, SymTransformer:
         }
       if !isCompatible(expected) then
         recheckr.println(i"conforms failed for ${tree}: $actual vs $expected")
-        err.typeMismatch(tree.withType(actual), expected)
+        err.typeMismatch(tree.withType(actual), expected, addenda)
       else if debugSuccesses then
         tree match
           case _: Ident =>