diff --git a/compiler/src/dotty/tools/dotc/cc/CCState.scala b/compiler/src/dotty/tools/dotc/cc/CCState.scala
index 5e0ba4627da3..5feae257b97e 100644
--- a/compiler/src/dotty/tools/dotc/cc/CCState.scala
+++ b/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.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.
    */
diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index 3a2d122c8e68..8d668a6d29b7 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -58,6 +58,7 @@ object Capabilities:
   trait RootCapability extends Capability:
     val rootId = nextRootId
     nextRootId += 1
+    def descr(using Context): String
 
   /** The base trait of all capabilties represented as types */
   trait CoreCapability extends TypeProxy, Capability:
@@ -120,6 +121,7 @@ object Capabilities:
    */
   @sharable // We override below all operations that access internal capability state
   object GlobalCap extends RootCapability:
+    def descr(using Context) = "the universal root capability"
     override val maybe = Maybe(this)
     override val readOnly = ReadOnly(this)
     override def reach = unsupported("cap.reach")
@@ -136,13 +138,21 @@ object Capabilities:
    *                 for diagnostics
    */
   case class FreshCap private (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability:
-    val hiddenSet = CaptureSet.HiddenSet(owner)
-    hiddenSet.owningCap = this
+    val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked)
+      // fails initialization check without the @unchecked
 
     override def equals(that: Any) = that match
       case that: FreshCap => this eq that
       case _ => false
 
+    def descr(using Context) =
+      val originStr = origin match
+        case Origin.InDecl(sym) if sym.exists =>
+          origin.explanation
+        case _ =>
+          i" created in ${hiddenSet.owner.sanitizedDescription}${origin.explanation}"
+      i"a fresh root capability$originStr"
+
   object FreshCap:
     def apply(origin: Origin)(using Context): FreshCap | GlobalCap.type =
       if ccConfig.useSepChecks then FreshCap(ctx.owner, origin)
@@ -225,6 +235,9 @@ object Capabilities:
             rcap.myOrigin = primary
             primary.variants += rcap
             rcap
+
+    def descr(using Context) =
+      i"a root capability associated with the result type of $binder"
   end ResultCap
 
   /** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
@@ -545,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
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index de54dea83d75..6f86dd20ab44 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/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
@@ -157,7 +154,7 @@ extension (tp: Type)
    *  the two capture sets are combined.
    */
   def capturing(cs: CaptureSet)(using Context): Type =
-    if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, VarState.Separate).isOK)
+    if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, VarState.Separate))
         && !cs.keepAlways
     then tp
     else tp match
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index eb97d7e1cc6f..b836ca41f290 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/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
@@ -113,6 +114,10 @@ sealed abstract class CaptureSet extends Showable:
 
   final def keepAlways: Boolean = this.isInstanceOf[EmptyWithProvenance]
 
+  def failWith(fail: TypeComparer.ErrorNote)(using Context): false =
+    TypeComparer.addErrorNote(fail)
+    false
+
   /** Try to include an element in this capture set.
    *  @param elem    The element to be added
    *  @param origin  The set that originated the request, or `empty` if the request came from outside.
@@ -132,14 +137,17 @@ sealed abstract class CaptureSet extends Showable:
    *  element is not the root capability, try instead to include its underlying
    *  capture set.
    */
-  protected def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult = reporting.trace(i"try include $elem in $this # ${maybeId}"):
-    if accountsFor(elem) then CompareResult.OK
-    else addNewElem(elem)
+  protected def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean = reporting.trace(i"try include $elem in $this # ${maybeId}"):
+    accountsFor(elem) || addNewElem(elem)
 
   /** Try to include all element in `refs` to this capture set. */
-  protected final def tryInclude(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
-    (CompareResult.OK /: newElems): (r, elem) =>
-      r.andAlso(tryInclude(elem, origin))
+  protected final def tryInclude(newElems: Refs, origin: CaptureSet)(using Context, VarState): Boolean =
+    TypeComparer.inNestedLevel:
+      // Run in nested level so that a error notes for a failure here can be
+      // cancelled in case the whole comparison succeeds.
+      // We do this here because all nested tryInclude and subCaptures calls go
+      // through this method.
+      newElems.forall(tryInclude(_, origin))
 
   /** Add an element to this capture set, assuming it is not already accounted for,
    *  and omitting any mapping or filtering.
@@ -148,34 +156,29 @@ sealed abstract class CaptureSet extends Showable:
    *  element is not the root capability, try instead to include its underlying
    *  capture set.
    */
-  protected final def addNewElem(elem: Capability)(using ctx: Context, vs: VarState): CompareResult =
-    if elem.isTerminalCapability || !vs.isOpen then
-      addThisElem(elem)
-    else
-      addThisElem(elem).orElse:
-        val underlying = elem.captureSetOfInfo
-        tryInclude(underlying.elems, this).andAlso:
-          underlying.addDependent(this)
-          CompareResult.OK
-
-  /** Add new elements one by one using `addNewElem`, abort on first failure */
-  protected final def addNewElems(newElems: Refs)(using Context, VarState): CompareResult =
-    (CompareResult.OK /: newElems): (r, elem) =>
-      r.andAlso(addNewElem(elem))
+  protected final def addNewElem(elem: Capability)(using ctx: Context, vs: VarState): Boolean =
+    addThisElem(elem)
+    || !elem.isTerminalCapability
+        && vs.isOpen
+        && {
+          val underlying = elem.captureSetOfInfo
+          val res = tryInclude(underlying.elems, this)
+          if res then underlying.addDependent(this)
+          res
+        }
 
   /** Add a specific element, assuming it is not already accounted for,
    *  and omitting any mapping or filtering, without possibility to backtrack
    *  to the underlying capture set.
    */
-  protected def addThisElem(elem: Capability)(using Context, VarState): CompareResult
+  protected def addThisElem(elem: Capability)(using Context, VarState): Boolean
 
-  protected def addIfHiddenOrFail(elem: Capability)(using ctx: Context, vs: VarState): CompareResult =
-    if elems.exists(_.maxSubsumes(elem, canAddHidden = true))
-    then CompareResult.OK
-    else CompareResult.Fail(this :: Nil)
+  protected def addIfHiddenOrFail(elem: Capability)(using ctx: Context, vs: VarState): Boolean =
+    elems.exists(_.maxSubsumes(elem, canAddHidden = true))
+    || failWith(IncludeFailure(this, elem))
 
   /** If this is a variable, add `cs` as a dependent set */
-  protected def addDependent(cs: CaptureSet)(using Context, VarState): CompareResult
+  protected def addDependent(cs: CaptureSet)(using Context, VarState): Boolean
 
   /** If `cs` is a variable, add this capture set as one of its dependent sets */
   protected def addAsDependentTo(cs: CaptureSet)(using Context): this.type =
@@ -192,14 +195,15 @@ sealed abstract class CaptureSet extends Showable:
       i"$this accountsFor $x$suffix"
 
     def test(using Context) = reporting.trace(debugInfo):
-      elems.exists(_.subsumes(x))
-      || // Even though subsumes already follows captureSetOfInfo, this is not enough.
-         // For instance x: C^{y, z}. Then neither y nor z subsumes x but {y, z} accounts for x.
-        !x.isTerminalCapability
-        && !x.coreType.derivesFrom(defn.Caps_CapSet)
-        && !(vs.isSeparating && x.captureSetOfInfo.containsTerminalCapability)
-           // in VarState.Separate, don't try to widen to cap since that might succeed with {cap} <: {cap}
-        && x.captureSetOfInfo.subCaptures(this, VarState.Separate).isOK
+      TypeComparer.noNotes: // Any failures in accountsFor should not lead to error notes
+        elems.exists(_.subsumes(x))
+        || // Even though subsumes already follows captureSetOfInfo, this is not enough.
+           // For instance x: C^{y, z}. Then neither y nor z subsumes x but {y, z} accounts for x.
+          !x.isTerminalCapability
+          && !x.coreType.derivesFrom(defn.Caps_CapSet)
+          && !(vs.isSeparating && x.captureSetOfInfo.containsTerminalCapability)
+            // in VarState.Separate, don't try to widen to cap since that might succeed with {cap} <: {cap}
+          && x.captureSetOfInfo.subCaptures(this, VarState.Separate)
 
     comparer match
       case comparer: ExplainingTypeComparer => comparer.traceIndented(debugInfo)(test)
@@ -216,7 +220,8 @@ sealed abstract class CaptureSet extends Showable:
   def mightAccountFor(x: Capability)(using Context): Boolean =
     reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true):
       CCState.withCollapsedFresh: // OK here since we opportunistically choose an alternative which gets checked later
-        elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded))
+        TypeComparer.noNotes:
+          elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded))
       || !x.isTerminalCapability
         && {
           val elems = x.captureSetOfInfo.elems
@@ -233,34 +238,31 @@ sealed abstract class CaptureSet extends Showable:
     && !that.elems.forall(this.mightAccountFor)
 
   /** The subcapturing test, taking an explicit VarState. */
-  final def subCaptures(that: CaptureSet, vs: VarState)(using Context): CompareResult =
+  final def subCaptures(that: CaptureSet, vs: VarState)(using Context): Boolean =
     subCaptures(that)(using ctx, vs)
 
   /** The subcapturing test, using a given VarState */
-  final def subCaptures(that: CaptureSet)(using ctx: Context, vs: VarState = VarState()): CompareResult =
-    val result = that.tryInclude(elems, this)
-    if result.isOK then
+  final def subCaptures(that: CaptureSet)(using ctx: Context, vs: VarState = VarState()): Boolean =
+    if that.tryInclude(elems, this) then
       addDependent(that)
     else
-      result.levelError.foreach(ccState.addNote)
       varState.rollBack()
-      result
-      //.showing(i"subcaptures $this <:< $that = ${result.show}", capt)
+      false
 
   /** Two capture sets are considered =:= equal if they mutually subcapture each other
    *  in a frozen state.
    */
   def =:= (that: CaptureSet)(using Context): Boolean =
-       this.subCaptures(that, VarState.Separate).isOK
-    && that.subCaptures(this, VarState.Separate).isOK
+       this.subCaptures(that, VarState.Separate)
+    && that.subCaptures(this, VarState.Separate)
 
   /** The smallest capture set (via <:<) that is a superset of both
    *  `this` and `that`
    */
   def ++ (that: CaptureSet)(using Context): CaptureSet =
-    if this.subCaptures(that, VarState.HardSeparate).isOK then
+    if this.subCaptures(that, VarState.HardSeparate) then
       if that.isAlwaysEmpty && this.keepAlways then this else that
-    else if that.subCaptures(this, VarState.HardSeparate).isOK then this
+    else if that.subCaptures(this, VarState.HardSeparate) then this
     else if this.isConst && that.isConst then Const(this.elems ++ that.elems)
     else Union(this, that)
 
@@ -275,8 +277,8 @@ sealed abstract class CaptureSet extends Showable:
   /** The largest capture set (via <:<) that is a subset of both `this` and `that`
    */
   def **(that: CaptureSet)(using Context): CaptureSet =
-    if this.subCaptures(that, VarState.Closed()).isOK then this
-    else if that.subCaptures(this, VarState.Closed()).isOK then that
+    if this.subCaptures(that, VarState.Closed()) then this
+    else if that.subCaptures(this, VarState.Closed()) then that
     else if this.isConst && that.isConst then Const(elemIntersection(this, that))
     else Intersection(this, that)
 
@@ -471,13 +473,15 @@ object CaptureSet:
     def isAlwaysEmpty(using Context) = elems.isEmpty
     def isProvisionallySolved(using Context) = false
 
-    def addThisElem(elem: Capability)(using Context, VarState): CompareResult =
-      val res = addIfHiddenOrFail(elem)
-      if !res.isOK && this.isProvisionallySolved then
-        println(i"Cannot add $elem to provisionally solved $this")
-      res
+    def addThisElem(elem: Capability)(using Context, VarState): Boolean =
+      addIfHiddenOrFail(elem)
+      || {
+        if this.isProvisionallySolved then
+          capt.println(i"Cannot add $elem to provisionally solved $this")
+        false
+      }
 
-    def addDependent(cs: CaptureSet)(using Context, VarState) = CompareResult.OK
+    def addDependent(cs: CaptureSet)(using Context, VarState) = true
 
     def upperApprox(origin: CaptureSet)(using Context): CaptureSet = this
 
@@ -504,7 +508,7 @@ object CaptureSet:
    */
   object Fluid extends Const(emptyRefs):
     override def isAlwaysEmpty(using Context) = false
-    override def addThisElem(elem: Capability)(using Context, VarState) = CompareResult.OK
+    override def addThisElem(elem: Capability)(using Context, VarState) = true
     override def accountsFor(x: Capability)(using Context)(using VarState): Boolean = true
     override def mightAccountFor(x: Capability)(using Context): Boolean = true
     override def toString = "<fluid>"
@@ -596,11 +600,11 @@ object CaptureSet:
           assert(elem.subsumes(elem1),
             i"Skipped map ${tm.getClass} maps newly added $elem to $elem1 in $this")
 
-    final def addThisElem(elem: Capability)(using Context, VarState): CompareResult =
+    final def addThisElem(elem: Capability)(using Context, VarState): Boolean =
       if isConst || !recordElemsState() then // Fail if variable is solved or given VarState is frozen
         addIfHiddenOrFail(elem)
       else if !levelOK(elem) then
-        CompareResult.LevelError(this, elem)    // or `elem` is not visible at the level of the set.
+        failWith(IncludeFailure(this, elem, levelError = true))    // or `elem` is not visible at the level of the set.
       else
         // id == 108 then assert(false, i"trying to add $elem to $this")
         assert(elem.isWellformed, elem)
@@ -611,14 +615,15 @@ object CaptureSet:
         newElemAddedHandler(elem)
         val normElem = if isMaybeSet then elem else elem.stripMaybe
         // assert(id != 5 || elems.size != 3, this)
-        val res = (CompareResult.OK /: deps): (r, dep) =>
-          r.andAlso:
-            reporting.trace(i"forward $normElem from $this # $id to $dep # ${dep.maybeId} of class ${dep.getClass.toString}"):
-              dep.tryInclude(normElem, this)
-        if ccConfig.checkSkippedMaps && res.isOK then checkSkippedMaps(elem)
-        res.orElse:
+        val res = deps.forall: dep =>
+          reporting.trace(i"forward $normElem from $this # $id to $dep # ${dep.maybeId} of class ${dep.getClass.toString}"):
+            dep.tryInclude(normElem, this)
+        if ccConfig.checkSkippedMaps && res then checkSkippedMaps(elem)
+        if !res then
           elems -= elem
-          res.addToTrace(this)
+          TypeComparer.updateErrorNotes:
+            case note: IncludeFailure => note.addToTrace(this)
+        res
 
     private def isPartOf(binder: Type)(using Context): Boolean =
       val find = new TypeAccumulator[Boolean]:
@@ -661,14 +666,11 @@ object CaptureSet:
       case _ =>
         true
 
-    def addDependent(cs: CaptureSet)(using Context, VarState): CompareResult =
-      if (cs eq this) || cs.isUniversal || isConst then
-        CompareResult.OK
-      else if recordDepsState() then
-        deps += cs
-        CompareResult.OK
-      else
-        CompareResult.Fail(this :: Nil)
+    def addDependent(cs: CaptureSet)(using Context, VarState): Boolean =
+      (cs eq this)
+      || cs.isUniversal
+      || isConst
+      || recordDepsState() && { deps += cs; true }
 
     override def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
       rootLimit = upto
@@ -720,7 +722,7 @@ object CaptureSet:
         //println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}")
         val newElems = approx.elems -- elems
         given VarState()
-        if tryInclude(newElems, empty).isOK then
+        if tryInclude(newElems, empty) then
           markSolved(provisional = false)
 
     /** Mark set as solved and propagate this info to all dependent sets */
@@ -818,13 +820,12 @@ object CaptureSet:
     (val source: Var, val bimap: BiTypeMap, initialElems: Refs)(using @constructorOnly ctx: Context)
   extends DerivedVar(source.owner, initialElems):
 
-    override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult =
+    override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean =
       if origin eq source then
         val mappedElem = bimap.mapCapability(elem)
-        if accountsFor(mappedElem) then CompareResult.OK
-        else addNewElem(mappedElem)
+        accountsFor(mappedElem) || addNewElem(mappedElem)
       else if accountsFor(elem) then
-        CompareResult.OK
+        true
       else
         // Propagate backwards to source. The element will be added then by another
         // forward propagation from source that hits the first branch `if origin eq source then`.
@@ -858,17 +859,16 @@ object CaptureSet:
     (val source: Var, val p: Context ?=> Capability => Boolean)(using @constructorOnly ctx: Context)
   extends DerivedVar(source.owner, source.elems.filter(p)):
 
-    override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult =
+    override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean =
       if accountsFor(elem) then
-        CompareResult.OK
+        true
       else if origin eq source then
-        if p(elem) then addNewElem(elem)
-        else CompareResult.OK
+        !p(elem) || addNewElem(elem)
       else
         // Filtered elements have to be back-propagated to source.
         // Elements that don't satisfy `p` are not allowed.
         if p(elem) then source.tryInclude(elem, this)
-        else CompareResult.Fail(this :: Nil)
+        else failWith(IncludeFailure(this, elem))
 
     override def computeApprox(origin: CaptureSet)(using Context): CaptureSet =
       if source eq origin then
@@ -890,14 +890,14 @@ object CaptureSet:
     addAsDependentTo(cs1)
     addAsDependentTo(cs2)
 
-    override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult =
-      if accountsFor(elem) then CompareResult.OK
+    override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean =
+      if accountsFor(elem) then true
       else
         val res = super.tryInclude(elem, origin)
         // If this is the union of a constant and a variable,
         // propagate `elem` to the variable part to avoid slack
         // between the operands and the union.
-        if res.isOK && (origin ne cs1) && (origin ne cs2) then
+        if res && (origin ne cs1) && (origin ne cs2) then
           if cs1.isConst then cs2.tryInclude(elem, origin)
           else if cs2.isConst then cs1.tryInclude(elem, origin)
           else res
@@ -914,13 +914,12 @@ object CaptureSet:
     deps += cs1
     deps += cs2
 
-    override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult =
+    override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean =
       val present =
         if origin eq cs1 then cs2.accountsFor(elem)
         else if origin eq cs2 then cs1.accountsFor(elem)
         else true
-      if present && !accountsFor(elem) then addNewElem(elem)
-      else CompareResult.OK
+      !present || accountsFor(elem) || addNewElem(elem)
 
     override def computeApprox(origin: CaptureSet)(using Context): CaptureSet =
       if (origin eq cs1) || (origin eq cs2) then
@@ -951,14 +950,15 @@ object CaptureSet:
    *  which are already subject through snapshotting and rollbacks in VarState.
    *  It's advantageous if we don't need to deal with other pieces of state there.
    */
-  class HiddenSet(initialOwner: Symbol)(using @constructorOnly ictx: Context)
+  class HiddenSet(initialOwner: Symbol, val owningCap: FreshCap)(using @constructorOnly ictx: Context)
   extends Var(initialOwner):
-    var owningCap: FreshCap = uninitialized // initialized when owning FreshCap is created
     var givenOwner: Symbol = initialOwner
 
     override def owner = givenOwner
 
-    //assert(id != 4)
+    //assert(id != 3)
+
+    description = i"of elements subsumed by a fresh cap in $initialOwner"
 
     private def aliasRef: FreshCap | Null =
       if myElems.size == 1 then
@@ -1062,7 +1062,7 @@ object CaptureSet:
     case TypeBounds(CapturingType(lo, loRefs), CapturingType(hi, hiRefs)) if lo =:= hi =>
       given VarState()
       val cs2 = arg2.captureSet
-      hiRefs.subCaptures(cs2).isOK && cs2.subCaptures(loRefs).isOK
+      hiRefs.subCaptures(cs2) && cs2.subCaptures(loRefs)
     case _ =>
       false
 
@@ -1075,55 +1075,24 @@ 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
+  case class IncludeFailure(cs: CaptureSet, elem: Capability, levelError: Boolean = false) extends ErrorNote, Showable:
+    private var myTrace: List[CaptureSet] = cs :: Nil
 
-  enum CompareResult extends Showable:
-    case OK
-    case Fail(trace: List[CaptureSet]) extends CompareResult, CompareFailure
-    case LevelError(cs: CaptureSet, elem: Capability) extends CompareResult, CompareFailure, ErrorNote
+    def trace: List[CaptureSet] = myTrace
+    def addToTrace(cs1: CaptureSet) =
+      val res = IncludeFailure(cs, elem, levelError)
+      res.myTrace = cs1 :: this.myTrace
+      res
 
     override def toText(printer: Printer): Text =
       inContext(printer.printerContext):
-        this match
-          case OK => Str("OK")
-          case Fail(trace) =>
-            if ctx.settings.YccDebug.value then printer.toText(trace, ", ")
-            else blocking.show
-          case LevelError(cs: CaptureSet, elem: Capability) =>
-            Str(i"($elem at wrong level for $cs at level ${cs.level.toString})")
-
-    /** The result is OK */
-    def isOK: Boolean = this == OK
-
-    /** If not isOK, the blocking capture set */
-    def blocking: CaptureSet = (this: @unchecked) match
-      case Fail(cs) => cs.last
-      case LevelError(cs, _) => cs
-
-    /** Optionally, this result if it is a level error */
-    def levelError: Option[LevelError] = this match
-      case result: LevelError => Some(result)
-      case _ => None
-
-    inline def andAlso(op: Context ?=> CompareResult)(using Context): CompareResult =
-      if isOK then op else this
-
-    inline def orElse(op: Context ?=> CompareResult)(using Context): CompareResult =
-      if isOK then this
-      else
-        val alt = op
-        if alt.isOK then alt
-        else this
-
-    inline def addToTrace(cs: CaptureSet): CompareResult = this match
-      case Fail(trace) => Fail(cs :: trace)
-      case _ => this
-  end CompareResult
+        if levelError then
+          i"($elem at wrong level for $cs at level ${cs.level.toString})"
+        else
+          if ctx.settings.YccDebug.value
+          then i"$elem cannot be included in $trace"
+          else i"$elem cannot be included in $cs"
+  end IncludeFailure
 
   /** A VarState serves as a snapshot mechanism that can undo
    *  additions of elements or super sets if an operation fails
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index c7e31b7dd6b8..1bdd7ce92129 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/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, IncludeFailure, ExistentialSubsumesFailure}
 import CCState.*
 import StdNames.nme
 import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
@@ -349,22 +349,24 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     /** Assert subcapturing `cs1 <: cs2` (available for debugging, otherwise unused) */
     def assertSub(cs1: CaptureSet, cs2: CaptureSet)(using Context) =
-      assert(cs1.subCaptures(cs2).isOK, i"$cs1 is not a subset of $cs2")
+      assert(cs1.subCaptures(cs2), 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: IncludeFailure) :: Nil, otherNotes) =
+            notes.partition(_.isInstanceOf[IncludeFailure]): @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
+              val d = res.cs.description
               if d.isEmpty then provenance else ""
             def kind = if provisional then "previously estimated\n" else "allowed "
-            em"$prefix included in the ${kind}capture set ${res.blocking}$descr$toAdd"
+            em"$prefix included in the ${kind}capture set ${res.cs}$descr$toAdd"
           target match
             case target: CaptureSet.Var
-            if res.blocking.isProvisionallySolved =>
+            if res.cs.isProvisionallySolved =>
               report.warning(
                 msg(provisional = true)
                   .prepend(i"Another capture checking run needs to be scheduled because\n"),
@@ -380,7 +382,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     /** 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)),
+          TypeComparer.compareResult(elem.singletonCaptureSet.subCaptures(cs)),
           i"$elem cannot be referenced here; it is not",
           elem, cs, pos, provenance)
 
@@ -388,7 +390,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     def checkSubset(cs1: CaptureSet, cs2: CaptureSet, pos: SrcPos,
         provenance: => String = "", cs1description: String = "")(using Context) =
       checkOK(
-          ccState.test(cs1.subCaptures(cs2)),
+          TypeComparer.compareResult(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,12 +1274,16 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     type BoxErrors = mutable.ListBuffer[Message] | Null
 
-    private def errorNotes(notes: List[ErrorNote])(using Context): Addenda =
-      if notes.isEmpty then NothingToAdd
+    private def errorNotes(notes: List[TypeComparer.ErrorNote])(using Context): Addenda =
+      val printableNotes = notes.filter:
+        case IncludeFailure(_, _, true) => true
+        case _: ExistentialSubsumesFailure => true
+        case _ => false
+      if printableNotes.isEmpty then NothingToAdd
       else new Addenda:
-        override def toAdd(using Context) = notes.map: note =>
+        override def toAdd(using Context) = printableNotes.map: note =>
           val msg = note match
-            case CompareResult.LevelError(cs, ref) =>
+            case IncludeFailure(cs, ref, _) =>
               if ref.core.isCapOrFresh then
                 i"""the universal capability $ref
                    |cannot be included in capture set $cs"""
@@ -1294,7 +1300,6 @@ class CheckCaptures extends Recheck, SymTransformer:
               i"""the existential capture root in ${ex.originalBinder.resType}
                  |cannot subsume the capability $other$since"""
           i"""
-             |
              |Note that ${msg.toString}"""
 
 
@@ -1336,20 +1341,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.compareResult(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. */
@@ -1512,7 +1517,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           val cs = actual.captureSet
           if covariant then cs ++ leaked
           else
-            if !leaked.subCaptures(cs).isOK then
+            if !leaked.subCaptures(cs) then
               report.error(
                 em"""$expected cannot be box-converted to ${actual.capturing(leaked)}
                     |since the additional capture set $leaked resulting from box conversion is not allowed in $actual""", tree.srcPos)
diff --git a/compiler/src/dotty/tools/dotc/core/SymUtils.scala b/compiler/src/dotty/tools/dotc/core/SymUtils.scala
index 1b83014e5735..209f12fa8b87 100644
--- a/compiler/src/dotty/tools/dotc/core/SymUtils.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymUtils.scala
@@ -118,6 +118,16 @@ class SymUtils:
 
     def isGenericProduct(using Context): Boolean = whyNotGenericProduct.isEmpty
 
+    def sanitizedDescription(using Context): String =
+      if self.isConstructor then
+        i"constructor of ${self.owner.sanitizedDescription}"
+      else if self.isAnonymousFunction then
+        i"anonymous function of type ${self.info}"
+      else if self.name.toString.contains('$') then
+        self.owner.sanitizedDescription
+      else
+        self.show
+
     /** Is this an old style implicit conversion?
      *  @param directOnly            only consider explicitly written methods
      *  @param forImplicitClassOnly  only consider methods generated from implicit classes
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 5ecb0ee01ec0..772fea772047 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/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
+  protected 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
@@ -428,7 +433,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
           case _ =>
             if isCaptureVarComparison then
               return CCState.withCapAsRoot:
-                subCaptures(tp1.captureSet, tp2.captureSet).isOK
+                subCaptures(tp1.captureSet, tp2.captureSet)
             if (tp1 eq NothingType) || isBottom(tp1) then
               return true
         }
@@ -536,7 +541,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       case tp1 @ CapturingType(parent1, refs1) =>
         def compareCapturing =
           if tp2.isAny then true
-          else if subCaptures(refs1, tp2.captureSet).isOK && sameBoxed(tp1, tp2, refs1)
+          else if subCaptures(refs1, tp2.captureSet) && sameBoxed(tp1, tp2, refs1)
             || !ctx.mode.is(Mode.CheckBoundsOrSelfType) && tp1.isAlwaysPure
           then
             val tp2a =
@@ -578,7 +583,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
 
         if isCaptureVarComparison then
           return CCState.withCapAsRoot:
-            subCaptures(tp1.captureSet, tp2.captureSet).isOK
+            subCaptures(tp1.captureSet, tp2.captureSet)
 
         isSubApproxHi(tp1, info2.lo) && (trustBounds || isSubApproxHi(tp1, info2.hi))
         || compareGADT
@@ -663,12 +668,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 && isSubInfo(info1.resultType, info2.resultType.subst(info2, info1))
               case (info1 @ CapturingType(parent1, refs1), info2: Type)
               if info2.stripCapturing.isInstanceOf[MethodOrPoly] =>
-                subCaptures(refs1, info2.captureSet).isOK && sameBoxed(info1, info2, refs1)
+                subCaptures(refs1, info2.captureSet) && sameBoxed(info1, info2, refs1)
                   && isSubInfo(parent1, info2)
               case (info1: Type, CapturingType(parent2, refs2))
               if info1.stripCapturing.isInstanceOf[MethodOrPoly] =>
                 val refs1 = info1.captureSet
-                (refs1.isAlwaysEmpty || subCaptures(refs1, refs2).isOK) && sameBoxed(info1, info2, refs1)
+                (refs1.isAlwaysEmpty || subCaptures(refs1, refs2)) && sameBoxed(info1, info2, refs1)
                   && isSubInfo(info1, parent2)
               case _ =>
                 isSubType(info1, info2)
@@ -862,12 +867,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
               // Eamples where this arises is capt-capibility.scala and function-combinators.scala
               val singletonOK = tp1 match
                 case tp1: SingletonType
-                if subCaptures(tp1.underlying.captureSet, refs2, CaptureSet.VarState.Separate).isOK =>
+                if subCaptures(tp1.underlying.captureSet, refs2, CaptureSet.VarState.Separate) =>
                   recur(tp1.widen, tp2)
                 case _ =>
                   false
               singletonOK
-              || subCaptures(refs1, refs2).isOK
+              || subCaptures(refs1, refs2)
                   && sameBoxed(tp1, tp2, refs1)
                   && (recur(tp1.widen.stripCapturing, parent2)
                      || tp1.isInstanceOf[SingletonType] && recur(tp1, parent2)
@@ -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)
@@ -2800,7 +2830,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     if frozenConstraint then CaptureSet.VarState.Closed() else CaptureSet.VarState()
 
   protected def subCaptures(refs1: CaptureSet, refs2: CaptureSet,
-      vs: CaptureSet.VarState = makeVarState())(using Context): CaptureSet.CompareResult =
+      vs: CaptureSet.VarState = makeVarState())(using Context): Boolean =
     try
       refs1.subCaptures(refs2, vs)
     catch case ex: AssertionError =>
@@ -2813,7 +2843,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
    */
   protected def sameBoxed(tp1: Type, tp2: Type, refs1: CaptureSet)(using Context): Boolean =
     (tp1.isBoxedCapturing == tp2.isBoxedCapturing)
-    || refs1.subCaptures(CaptureSet.empty, makeVarState()).isOK
+    || refs1.subCaptures(CaptureSet.empty, makeVarState())
 
   // ----------- Diagnostics --------------------------------------------------
 
@@ -3219,12 +3249,50 @@ 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.kind != note.kind) then
+      errorNotes = (recCount, note) :: errorNotes
+      assert(maxErrorLevel <= recCount)
+      maxErrorLevel = recCount
+
+  private[TypeComparer] inline
+  def isolated[T](inline op: Boolean, inline mapResult: Boolean => T)(using Context): T =
+    val savedNotes = errorNotes
+    val savedLevel = maxErrorLevel
+    errorNotes = Nil
+    maxErrorLevel = -1
+    try mapResult(op)
+    finally
+      errorNotes = savedNotes
+      maxErrorLevel = savedLevel
+
+  /** 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 compareResult(op: => Boolean)(using Context): CompareResult =
+    isolated(op, res =>
+      if res then CompareResult.OK else CompareResult.Fail(errorNotes.map(_._2)))
 }
 
 object TypeComparer {
 
+  /** A base trait for data producing addenda to error messages */
+  trait ErrorNote:
+    /** A disciminating kind. An error note is not added if it has the same kind
+     *  as an already existing error note.
+     */
+    def kind: Class[?] = getClass
+
+  /** 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 {
@@ -3236,7 +3304,6 @@ object TypeComparer {
     else res match
       case ClassInfo(_, cls, _, _, _) => cls.showLocated
       case bounds: TypeBounds => i"type bounds [$bounds]"
-      case CaptureSet.CompareResult.OK => "OK"
       case res: printing.Showable => res.show
       case _ => String.valueOf(res).nn
 
@@ -3391,8 +3458,25 @@ object TypeComparer {
   def reduceMatchWith[T](op: MatchReducer => T)(using Context): T =
     comparing(_.reduceMatchWith(op))
 
-  def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): CaptureSet.CompareResult =
+  def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): Boolean =
     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)
+
+  def updateErrorNotes(f: PartialFunction[ErrorNote, ErrorNote])(using Context): Unit =
+    comparer.errorNotes = comparer.errorNotes.mapConserve: p =>
+      val (level, note) = p
+      if f.isDefinedAt(note) then (level, f(note)) else p
+
+  def compareResult(op: => Boolean)(using Context): CompareResult =
+    comparing(_.compareResult(op))
+
+  inline def noNotes(inline op: Boolean)(using Context): Boolean =
+    comparer.isolated(op, x => x)
 }
 
 object MatchReducer:
@@ -3797,9 +3881,11 @@ class ExplainingTypeComparer(initctx: Context, short: Boolean) extends TypeCompa
   private val b = new StringBuilder
   private var lastForwardGoal: String | Null = null
 
-  private def appendFailure(x: String) =
+  private def appendFailure(notes: List[ErrorNote]) =
     if lastForwardGoal != null then  // last was deepest goal that failed
-      b.append(s"  = $x")
+      b.append(s"  = false")
+      for case note: printing.Showable <- notes do
+        b.append(i": $note")
       lastForwardGoal = null
 
   override def traceIndented[T](str: String)(op: => T): T =
@@ -3815,9 +3901,9 @@ class ExplainingTypeComparer(initctx: Context, short: Boolean) extends TypeCompa
       if short then
         res match
           case false =>
-            appendFailure("false")
-          case res: CaptureSet.CompareResult if res != CaptureSet.CompareResult.OK =>
-            appendFailure(show(res))
+            appendFailure(errorNotes.map(_._2))
+          case CompareResult.Fail(notes) =>
+            appendFailure(notes)
           case _ =>
             b.length = curLength // don't show successful subtraces
       else
@@ -3867,7 +3953,7 @@ class ExplainingTypeComparer(initctx: Context, short: Boolean) extends TypeCompa
       super.gadtAddBound(sym, b, isUpper)
     }
 
-  override def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): CaptureSet.CompareResult =
+  override def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): Boolean =
     traceIndented(i"subcaptures $refs1 <:< $refs2 in ${vs.toString}") {
       super.subCaptures(refs1, refs2, vs)
     }
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index efd4c6e83cd2..67c8186c17d1 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -19,7 +19,7 @@ import typer.Inferencing.*
 import typer.IfBottom
 import reporting.TestingReporter
 import cc.{CapturingType, derivedCapturingType, CaptureSet, captureSet, isBoxed, isBoxedCapturing}
-import CaptureSet.{CompareResult, IdentityCaptRefMap, VarState}
+import CaptureSet.{IdentityCaptRefMap, VarState}
 
 import scala.annotation.internal.sharable
 import scala.annotation.threadUnsafe
@@ -161,7 +161,7 @@ object TypeOps:
         TypeComparer.lub(simplify(l, theMap), simplify(r, theMap), isSoft = tp.isSoft)
       case tp @ CapturingType(parent, refs) =>
         if !ctx.mode.is(Mode.Type)
-            && refs.subCaptures(parent.captureSet, VarState.Separate).isOK
+            && refs.subCaptures(parent.captureSet, VarState.Separate)
             && (tp.isBoxed || !parent.isBoxedCapturing)
               // fuse types with same boxed status and outer boxed with any type
         then
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 728f742ea1ad..2326abf04ad4 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -39,7 +39,7 @@ import reporting.{trace, Message}
 import java.lang.ref.WeakReference
 import compiletime.uninitialized
 import cc.*
-import CaptureSet.{CompareResult, IdentityCaptRefMap}
+import CaptureSet.IdentityCaptRefMap
 import Capabilities.*
 
 import scala.annotation.internal.sharable
diff --git a/compiler/src/dotty/tools/dotc/reporting/Message.scala b/compiler/src/dotty/tools/dotc/reporting/Message.scala
index 25d0c479b8a8..1e313ca749d3 100644
--- a/compiler/src/dotty/tools/dotc/reporting/Message.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/Message.scala
@@ -53,7 +53,7 @@ object Message:
       case None => false
   end Disambiguation
 
-  private type Recorded = Symbol | ParamRef | SkolemType | Capability
+  private type Recorded = Symbol | ParamRef | SkolemType | RootCapability
 
   private case class SeenKey(str: String, isType: Boolean)
 
@@ -183,31 +183,11 @@ object Message:
           s"is a ${ctx.printer.kindString(sym)}${sym.showExtendedLocation}${addendum("bounds", info)}"
         case tp: SkolemType =>
           s"is an unknown value of type ${tp.widen.show}"
-        case ref: Capability =>
+        case ref: RootCapability =>
           val relation =
             if List("^", "=>", "?=>").exists(key.startsWith) then "refers to"
             else "is"
-          def ownerStr(owner: Symbol): String =
-            if owner.isConstructor then
-              i"constructor of ${ownerStr(owner.owner)}"
-            else if owner.isAnonymousFunction then
-              i"anonymous function of type ${owner.info}"
-            else if owner.name.toString.contains('$') then
-              ownerStr(owner.owner)
-            else
-              owner.show
-          val descr =
-            ref match
-              case GlobalCap => "the universal root capability"
-              case ref: FreshCap =>
-                val descr = ref.origin match
-                  case origin @ Origin.InDecl(sym) if sym.exists =>
-                    origin.explanation
-                  case origin =>
-                    i" created in ${ownerStr(ref.hiddenSet.owner)}${origin.explanation}"
-                i"a fresh root capability$descr"
-              case ResultCap(binder) => i"a root capability associated with the result type of $binder"
-          s"$relation $descr"
+          s"$relation ${ref.descr}"
     end explanation
 
     /** Produce a where clause with explanations for recorded iterms.
@@ -274,14 +254,16 @@ object Message:
     override def toTextCapturing(parent: Type, refs: GeneralCaptureSet, boxText: Text) = refs match
       case refs: CaptureSet
       if isUniversalCaptureSet(refs) && !defn.isFunctionType(parent) && !printDebug && seen.isActive =>
-        boxText ~ toTextLocal(parent) ~ seen.record("^", isType = true, refs.elems.nth(0))
+        boxText
+        ~ toTextLocal(parent)
+        ~ seen.record("^", isType = true, refs.elems.nth(0).asInstanceOf[RootCapability])
       case _ =>
         super.toTextCapturing(parent, refs, boxText)
 
     override def funMiddleText(isContextual: Boolean, isPure: Boolean, refs: GeneralCaptureSet | Null): Text =
       refs match
         case refs: CaptureSet if isUniversalCaptureSet(refs) && seen.isActive =>
-          seen.record(arrow(isContextual, isPure = false), isType = true, refs.elems.nth(0))
+          seen.record(arrow(isContextual, isPure = false), isType = true, refs.elems.nth(0).asInstanceOf[RootCapability])
         case _ =>
           super.funMiddleText(isContextual, isPure, refs)
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 3f24f3f8f62b..dd04d6f9478a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/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 _ =>
diff --git a/tests/neg-custom-args/captures/cc-existential-conformance.check b/tests/neg-custom-args/captures/cc-existential-conformance.check
index d3236ce642b0..0719fd2787df 100644
--- a/tests/neg-custom-args/captures/cc-existential-conformance.check
+++ b/tests/neg-custom-args/captures/cc-existential-conformance.check
@@ -19,7 +19,6 @@
   |                           where:    ^  refers to a fresh root capability in the type of value y
   |                                     ^² 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 cap
   |
@@ -45,7 +44,6 @@
    |                        where:    ^  refers to a fresh root capability in the type of value y
    |                                  ^² 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 cap
    |
diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.check b/tests/neg-custom-args/captures/effect-swaps-explicit.check
index c7cbb351318a..469a0c6f14a4 100644
--- a/tests/neg-custom-args/captures/effect-swaps-explicit.check
+++ b/tests/neg-custom-args/captures/effect-swaps-explicit.check
@@ -24,7 +24,6 @@
    |where:    ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make
    |          ^   refers to the universal root capability
    |
-   |
    |Note that reference contextual$9.type
    |cannot be included in outer capture set ?
 70 |            fr.await.ok
diff --git a/tests/neg-custom-args/captures/effect-swaps.check b/tests/neg-custom-args/captures/effect-swaps.check
index d30aa0ca3f21..69cedcde2f75 100644
--- a/tests/neg-custom-args/captures/effect-swaps.check
+++ b/tests/neg-custom-args/captures/effect-swaps.check
@@ -24,7 +24,6 @@
    |where:    ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make
    |          cap is the universal root capability
    |
-   |
    |Note that reference contextual$9.type
    |cannot be included in outer capture set ?
 70 |            fr.await.ok
diff --git a/tests/neg-custom-args/captures/erased-methods2.check b/tests/neg-custom-args/captures/erased-methods2.check
index 80d2db450c40..d7cca4635f20 100644
--- a/tests/neg-custom-args/captures/erased-methods2.check
+++ b/tests/neg-custom-args/captures/erased-methods2.check
@@ -8,7 +8,6 @@
    |          ?=>² refers to a root capability associated with the result type of (using erased x$1: CT[Ex3]^): (erased x$2: CT[Ex2]^) ?=>² Unit
    |          ^    refers to the universal root capability
    |
-   |
    |Note that the existential capture root in (erased x$2: CT[Ex2]^) ?=> Unit
    |cannot subsume the capability x$1.type since that capability is not a SharedCapability
 21 |     ?=> (x$2: CT[Ex2]^)
@@ -28,7 +27,6 @@
    |          ?=>³ refers to a root capability associated with the result type of (using erased x$1: CT[Ex2]^): (erased x$2: CT[Ex1]^) ?=>³ Unit
    |          ^    refers to the universal root capability
    |
-   |
    |Note that the existential capture root in (erased x$1: CT[Ex2]^) ?=> (erased x$2: CT[Ex1]^) ?=> Unit
    |cannot subsume the capability x$1.type since that capability is not a SharedCapability
 32 |     ?=> (erased x$2: CT[Ex2]^)
diff --git a/tests/neg-custom-args/captures/filevar.check b/tests/neg-custom-args/captures/filevar.check
index d0b85408b43a..54f67bce972a 100644
--- a/tests/neg-custom-args/captures/filevar.check
+++ b/tests/neg-custom-args/captures/filevar.check
@@ -7,7 +7,6 @@
    |where:    =>  refers to a root capability associated with the result type of (using l: scala.caps.Capability^{cap.rd}): (f: File^{l}) => Unit
    |          cap is the universal root capability
    |
-   |
    |Note that reference l.type
    |cannot be included in outer capture set ? of parameter f
 16 |    val o = Service()
diff --git a/tests/neg-custom-args/captures/heal-tparam-cs.check b/tests/neg-custom-args/captures/heal-tparam-cs.check
index 10b56d5d6304..0a7c333c9e95 100644
--- a/tests/neg-custom-args/captures/heal-tparam-cs.check
+++ b/tests/neg-custom-args/captures/heal-tparam-cs.check
@@ -7,7 +7,6 @@
    |where:    => refers to a fresh root capability created in value test1 when checking argument to parameter op of method localCap
    |          ^  refers to the universal root capability
    |
-   |
    |Note that reference c.type
    |cannot be included in outer capture set ?
 11 |    () => { c.use() }
@@ -23,7 +22,6 @@
    |    where:    => refers to a root capability associated with the result type of (c: Capp^): () => Unit
    |              ^  refers to the universal root capability
    |
-   |
    |    Note that the existential capture root in () => Unit
    |    cannot subsume the capability x$0.type since that capability is not a SharedCapability
 16 |      (c1: Capp^) => () => { c1.use() }
diff --git a/tests/neg-custom-args/captures/i15923.check b/tests/neg-custom-args/captures/i15923.check
index e234eb579be2..4d3019f92d7a 100644
--- a/tests/neg-custom-args/captures/i15923.check
+++ b/tests/neg-custom-args/captures/i15923.check
@@ -8,7 +8,6 @@
    |          cap  is the universal root capability
    |          cap² is a root capability associated with the result type of (x$0: Cap^{lcap}): box Id[box Cap^{cap².rd}]^?
    |
-   |
    |Note that reference <cap of (x$0: Cap^{lcap}): box Id[box Cap^{cap.rd}]^?>.rd
    |cannot be included in outer capture set ?
    |
diff --git a/tests/neg-custom-args/captures/i15923a.check b/tests/neg-custom-args/captures/i15923a.check
index 9664fb7bfdde..1b4ef98aff20 100644
--- a/tests/neg-custom-args/captures/i15923a.check
+++ b/tests/neg-custom-args/captures/i15923a.check
@@ -9,7 +9,6 @@
   |          ^   refers to the universal root capability
   |          ^²  refers to a root capability associated with the result type of (): box Id[box Cap^²]^?
   |
-  |
   |Note that reference <cap of (): box Id[box Cap^]^?>
   |cannot be included in outer capture set ?
   |
diff --git a/tests/neg-custom-args/captures/i15923b.check b/tests/neg-custom-args/captures/i15923b.check
index 38da3dc798a8..eb67188bcc25 100644
--- a/tests/neg-custom-args/captures/i15923b.check
+++ b/tests/neg-custom-args/captures/i15923b.check
@@ -7,7 +7,6 @@
   |where:    => refers to a fresh root capability created in value leak when checking argument to parameter op of method withCap
   |          ^  refers to the universal root capability
   |
-  |
   |Note that reference lcap.type
   |cannot be included in outer capture set ?
   |
diff --git a/tests/neg-custom-args/captures/i16226.check b/tests/neg-custom-args/captures/i16226.check
index f3b8666c0eb7..4fb4119fdbef 100644
--- a/tests/neg-custom-args/captures/i16226.check
+++ b/tests/neg-custom-args/captures/i16226.check
@@ -21,7 +21,6 @@
    |          =>³ refers to a fresh root capability in the result type of method mapd
    |          ^   refers to a root capability associated with the result type of (ref: LazyRef[A]^{io}, f: A => B): LazyRef[B]^
    |
-   |
    |Note that the existential capture root in LazyRef[B]^
    |cannot subsume the capability f1.type since that capability is not a SharedCapability
    |
diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check
index a24677f0f9d1..5bc01afa4dd0 100644
--- a/tests/neg-custom-args/captures/i21614.check
+++ b/tests/neg-custom-args/captures/i21614.check
@@ -16,7 +16,6 @@
    |where:    =>  refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map
    |          cap is a root capability associated with the result type of (_$1: box File^{files*}): box Logger{val f: File^{_$1}}^{cap.rd, _$1}
    |
-   |
    |Note that reference <cap of (_$1: box File^{files*}): box Logger{val f: File^?}^?>.rd
    |cannot be included in outer capture set ?
    |
diff --git a/tests/neg-custom-args/captures/i21920.check b/tests/neg-custom-args/captures/i21920.check
index 301564d23b79..70327a9e413f 100644
--- a/tests/neg-custom-args/captures/i21920.check
+++ b/tests/neg-custom-args/captures/i21920.check
@@ -7,7 +7,6 @@
    |where:    => refers to a fresh root capability created in value cell when checking argument to parameter f of method open
    |          ^  refers to the universal root capability
    |
-   |
    |Note that reference <cap of (): IterableOnce[box File^?]^>
    |cannot be included in outer capture set ?
    |
diff --git a/tests/neg-custom-args/captures/leaking-iterators.check b/tests/neg-custom-args/captures/leaking-iterators.check
index f2731166e53d..a64934c41360 100644
--- a/tests/neg-custom-args/captures/leaking-iterators.check
+++ b/tests/neg-custom-args/captures/leaking-iterators.check
@@ -7,7 +7,6 @@
    |where:    => refers to a fresh root capability created in method test when checking argument to parameter op of method usingLogFile
    |          ^  refers to the universal root capability
    |
-   |
    |Note that reference log.type
    |cannot be included in outer capture set ?
 57 |    xs.iterator.map: x =>
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
index a54bb05b8222..29ed6503f45c 100644
--- a/tests/neg-custom-args/captures/reaches.check
+++ b/tests/neg-custom-args/captures/reaches.check
@@ -86,7 +86,6 @@
    |                  where:    ^  refers to the universal root capability
    |                            ^² refers to a root capability associated with the result type of (x: File^): File^²
    |
-   |
    |                  Note that the existential capture root in File^
    |                  cannot subsume the capability x.type since that capability is not a SharedCapability
    |
diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.check b/tests/neg-custom-args/captures/scope-extrude-mut.check
new file mode 100644
index 000000000000..1e01ddf834f8
--- /dev/null
+++ b/tests/neg-custom-args/captures/scope-extrude-mut.check
@@ -0,0 +1,9 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scope-extrude-mut.scala:9:8 ------------------------------
+9 |    a = a1  // error
+  |        ^^
+  |        Found:    A^{a1.rd}
+  |        Required: A^
+  |
+  |        where:    ^ refers to a fresh root capability in the type of variable a
+  |
+  | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.scala b/tests/neg-custom-args/captures/scope-extrude-mut.scala
new file mode 100644
index 000000000000..75ff0e11abcb
--- /dev/null
+++ b/tests/neg-custom-args/captures/scope-extrude-mut.scala
@@ -0,0 +1,9 @@
+import language.experimental.captureChecking
+
+class A extends caps.Mutable
+
+class B:
+  private var a: A^ = A()
+  def b() =
+    val a1 = A()
+    a = a1  // error
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/scoped-caps.check b/tests/neg-custom-args/captures/scoped-caps.check
index e35af6b10bb9..b57ff92a8899 100644
--- a/tests/neg-custom-args/captures/scoped-caps.check
+++ b/tests/neg-custom-args/captures/scoped-caps.check
@@ -19,7 +19,6 @@
   |                                   ^² refers to a fresh root capability in the type of value g
   |                                   ^³ 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 cap
   |
@@ -54,7 +53,6 @@
    |                        where:    ^  refers to the universal root capability
    |                                  ^² 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 x.type since that capability is not a SharedCapability
    |
@@ -69,7 +67,6 @@
    |                         ^²  refers to a root capability associated with the result type of (x: S^{cap.rd}): B^²
    |                         cap is the universal root capability
    |
-   |
    |               Note that the existential capture root in B^
    |               cannot subsume the capability cap
    |
diff --git a/tests/neg-custom-args/captures/simple-using.check b/tests/neg-custom-args/captures/simple-using.check
index 6e32260d3322..3f31f6e41dd2 100644
--- a/tests/neg-custom-args/captures/simple-using.check
+++ b/tests/neg-custom-args/captures/simple-using.check
@@ -7,7 +7,6 @@
   |where:    => refers to a fresh root capability created in method test when checking argument to parameter op of method usingLogFile
   |          ^  refers to the universal root capability
   |
-  |
   |Note that reference f.type
   |cannot be included in outer capture set ?
   |
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index 7f420872eb25..7d1f2bc7f31d 100644
--- a/tests/neg-custom-args/captures/try.check
+++ b/tests/neg-custom-args/captures/try.check
@@ -39,7 +39,6 @@
    |where:    => refers to a fresh root capability created in value xx when checking argument to parameter op of method handle
    |          ^  refers to the universal root capability
    |
-   |
    |Note that reference x.type
    |cannot be included in outer capture set ?
 36 |    (x: CanThrow[Exception]) =>
@@ -58,7 +57,6 @@
    |where:    => refers to a fresh root capability created in value global when checking argument to parameter op of method handle
    |          ^  refers to the universal root capability
    |
-   |
    |Note that reference x.type
    |cannot be included in outer capture set ?
 48 |  (x: CanThrow[Exception]) =>
diff --git a/tests/neg-custom-args/captures/usingLogFile.check b/tests/neg-custom-args/captures/usingLogFile.check
index 86ddcb17312d..04df1e7aeca6 100644
--- a/tests/neg-custom-args/captures/usingLogFile.check
+++ b/tests/neg-custom-args/captures/usingLogFile.check
@@ -7,7 +7,6 @@
    |where:    => refers to a fresh root capability created in value later when checking argument to parameter op of method usingLogFile
    |          ^  refers to the universal root capability
    |
-   |
    |Note that reference f.type
    |cannot be included in outer capture set ?
    |
@@ -21,7 +20,6 @@
    |where:    => refers to a fresh root capability created in value later2 when checking argument to parameter op of method usingLogFile
    |          ^  refers to the universal root capability
    |
-   |
    |Note that reference f.type
    |cannot be included in outer capture set ?
    |
@@ -35,7 +33,6 @@
    |where:    => refers to a fresh root capability created in value later when checking argument to parameter op of method usingFile
    |          ^  refers to the universal root capability
    |
-   |
    |Note that reference f.type
    |cannot be included in outer capture set ?
    |
@@ -49,7 +46,6 @@
    |where:    => refers to a fresh root capability created in value later when checking argument to parameter op of method usingFile
    |          ^  refers to the universal root capability
    |
-   |
    |Note that reference _$1.type
    |cannot be included in outer capture set ?
    |
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
index d8b55afd298c..b6504e5e0029 100644
--- a/tests/neg-custom-args/captures/vars.check
+++ b/tests/neg-custom-args/captures/vars.check
@@ -27,7 +27,6 @@
    |
    |        where:    ^ refers to the universal root capability
    |
-   |
    |        Note that reference cap3.type
    |        cannot be included in outer capture set ?
 37 |    def g(x: String): String = if cap3 == cap3 then "" else "a"
diff --git a/tests/pending/neg-custom-args/sep-tvar-follow.scala b/tests/pending/neg-custom-args/sep-tvar-follow.scala
new file mode 100644
index 000000000000..09ee3a17a054
--- /dev/null
+++ b/tests/pending/neg-custom-args/sep-tvar-follow.scala
@@ -0,0 +1,10 @@
+import language.experimental.captureChecking
+trait Ref
+def swap(x1: Ref^, x2: Ref^): Unit = ()
+def foo(a: Ref^)[X](op: (z: Ref^) -> X^{z}): X^{a} = op(a)
+def test1(a: Ref^): Unit =
+  def bad(x: Ref^)(y: Ref^{a}): Unit = swap(x, y)
+  val t1 = bad
+  def t2[X] = foo(a)[X]
+  val t3 = t2[(y: Ref^{a}) -> Unit](t1)
+  t3(a)  // boom