diff --git a/compiler/src/dotty/tools/dotc/cc/CCState.scala b/compiler/src/dotty/tools/dotc/cc/CCState.scala
index c92c9faa6fe6..9fecf1076bf0 100644
--- a/compiler/src/dotty/tools/dotc/cc/CCState.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CCState.scala
@@ -118,6 +118,8 @@ class CCState:
 
   private var capIsRoot: Boolean = false
 
+  private var ignoreFreshLevels: Boolean = false
+
 object CCState:
 
   opaque type Level = Int
@@ -162,4 +164,20 @@ object CCState:
   /** Is `caps.cap` a root capability that is allowed to subsume other capabilities? */
   def capIsRoot(using Context): Boolean = ccState.capIsRoot
 
+  /** Run `op` under the assumption that all root.Fresh instances are equal.
+   *  Needed to make override checking of types containing fresh work.
+   *  Asserted in override checking, tested in maxSubsumes.
+   *  Is this sound? Test case is neg-custom-args/captures/leaked-curried.scala.
+   */
+  inline def ignoringFreshLevels[T](op: => T)(using Context): T =
+    if isCaptureCheckingOrSetup then
+      val ccs = ccState
+      val saved = ccs.ignoreFreshLevels
+      ccs.ignoreFreshLevels = true
+      try op finally ccs.ignoreFreshLevels = saved
+    else op
+
+  /** Should all root.Fresh instances be treated equal? */
+  def ignoreFreshLevels(using Context): Boolean = ccState.ignoreFreshLevels
+
 end CCState
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index afe0cfb6a8ff..f53650f425b2 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -4,20 +4,18 @@ package cc
 
 import core.*
 import Types.*, Symbols.*, Contexts.*, Annotations.*, Flags.*
-import Names.TermName
+import Names.{Name, TermName}
 import ast.{tpd, untpd}
 import Decorators.*, NameOps.*
 import config.Printers.capt
 import util.Property.Key
 import tpd.*
+import Annotations.Annotation
 import CaptureSet.VarState
 
 /** Attachment key for capturing type trees */
 private val Captures: Key[CaptureSet] = Key()
 
-/** Context property to print root.Fresh(...) as "fresh" instead of "cap" */
-val PrintFresh: Key[Unit] = Key()
-
 /** Are we at checkCaptures phase? */
 def isCaptureChecking(using Context): Boolean =
   ctx.phaseId == Phases.checkCapturesPhase.id
@@ -465,7 +463,9 @@ extension (tp: Type)
             if args.forall(_.isAlwaysPure) then
               // Also map existentials in results to reach capabilities if all
               // preceding arguments are known to be always pure
-              t.derivedFunctionOrMethod(args, apply(root.resultToFresh(res)))
+              t.derivedFunctionOrMethod(
+                args,
+                apply(root.resultToFresh(res, root.Origin.ResultInstance(t, NoSymbol))))
             else
               t
           case _ =>
@@ -505,6 +505,10 @@ extension (tp: Type)
     case tp: ThisType => ccState.symLevel(tp.cls).nextInner
     case _ => CCState.undefinedLevel
 
+  def refinedOverride(name: Name, rinfo: Type)(using Context): Type =
+    RefinedType(tp, name,
+      AnnotatedType(rinfo, Annotation(defn.RefineOverrideAnnot, util.Spans.NoSpan)))
+
 extension (tp: MethodType)
   /** A method marks an existential scope unless it is the prefix of a curried method */
   def marksExistentialScope(using Context): Boolean =
@@ -694,6 +698,12 @@ abstract class AnnotatedCapability(annotCls: Context ?=> ClassSymbol):
   protected def unwrappable(using Context): Set[Symbol]
 end AnnotatedCapability
 
+object QualifiedCapability:
+  def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
+    case AnnotatedType(parent: CaptureRef, ann)
+    if defn.capabilityQualifierAnnots.contains(ann.symbol) => Some(parent)
+    case _ => None
+
 /** An extractor for `ref @maybeCapability`, which is used to express
  *  the maybe capability `ref?` as a type.
  */
@@ -792,7 +802,8 @@ abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]:
       case AnnotatedType(parent, _) =>
         this(acc, parent)
       case t @ FunctionOrMethod(args, res) =>
-        if args.forall(_.isAlwaysPure) then this(acc, root.resultToFresh(res))
+        if args.forall(_.isAlwaysPure) then
+          this(acc, root.resultToFresh(res, root.Origin.ResultInstance(t, NoSymbol)))
         else acc
       case _ =>
         foldOver(acc, t)
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index 98f1502a0c1c..21e05e4663b3 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -14,7 +14,9 @@ import compiletime.uninitialized
 import StdNames.nme
 import CaptureSet.VarState
 import Annotations.Annotation
+import Flags.*
 import config.Printers.capt
+import CCState.{Level, undefinedLevel}
 
 object CaptureRef:
   opaque type Validity = Int
@@ -106,6 +108,10 @@ trait CaptureRef extends TypeProxy, ValueType:
     case root.Fresh(_) => true
     case _ => false
 
+  final def isResultRoot(using Context): Boolean = this match
+    case root.Result(_) => true
+    case _ => false
+
   /** Is this reference the generic root capability `cap` or a Fresh instance? */
   final def isCapOrFresh(using Context): Boolean = isCap || isFresh
 
@@ -122,6 +128,41 @@ trait CaptureRef extends TypeProxy, ValueType:
   final def isExclusive(using Context): Boolean =
     !isReadOnly && (isRootCapability || captureSetOfInfo.isExclusive)
 
+  /** The owning symbol associated with a capability this is
+   *   - for Fresh capabilities: the owner of the hidden set
+   *   - for TermRefs and TypeRefs: the symbol it refers to
+   *   - for derived and path capabilities: the owner of the underlying capability
+   *   - otherwise NoSymbol
+   */
+  final def ccOwner(using Context): Symbol = this match
+    case root.Fresh(hidden) =>
+      hidden.owner
+    case ref: NamedType =>
+      if ref.isCap then NoSymbol
+      else ref.prefix match
+        case prefix: CaptureRef => prefix.ccOwner
+        case _ => ref.symbol
+    case ref: ThisType =>
+      ref.cls
+    case QualifiedCapability(ref1) =>
+      ref1.ccOwner
+    case _ =>
+      NoSymbol
+
+  /** The symbol that represents the level closest-enclosing ccOwner.
+   *  Symbols representing levels are
+   *   - class symbols, but not inner (non-static) module classes
+   *   - method symbols, but not accessors or constructors
+   */
+  final def levelOwner(using Context): Symbol =
+    def adjust(owner: Symbol): Symbol =
+      if !owner.exists
+        || owner.isClass && (!owner.is(Flags.Module) || owner.isStatic)
+        || owner.is(Flags.Method, butNot = Flags.Accessor) && !owner.isConstructor
+      then owner
+      else adjust(owner.owner)
+    adjust(ccOwner)
+
   // With the support of paths, we don't need to normalize the `TermRef`s anymore.
   // /** Normalize reference so that it can be compared with `eq` for equality */
   // final def normalizedRef(using Context): CaptureRef = this match
@@ -263,11 +304,18 @@ trait CaptureRef extends TypeProxy, ValueType:
       case _ => false
     (this eq y)
     || this.match
-      case root.Fresh(hidden) =>
-        vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
-        || !y.stripReadOnly.isCap
+      case x @ root.Fresh(hidden) =>
+        def levelOK =
+          if ccConfig.useFreshLevels && !CCState.ignoreFreshLevels then
+            val yOwner = y.levelOwner
+            yOwner.isStaticOwner || x.ccOwner.isContainedIn(yOwner)
+          else
+            !y.stripReadOnly.isCap
             && !yIsExistential
-            && !y.isInstanceOf[TermParamRef]
+            && !y.isInstanceOf[ParamRef]
+
+        vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
+        || levelOK
             && canAddHidden
             && vs.addHidden(hidden, y)
       case x @ root.Result(binder) =>
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 93ca0956baed..58b08b077eba 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -183,7 +183,7 @@ sealed abstract class CaptureSet extends Showable:
    */
   def accountsFor(x: CaptureRef)(using ctx: Context)(using vs: VarState = VarState.Separate): Boolean =
 
-    def debugInfo(using Context) = i"$this accountsFor $x, which has capture set ${x.captureSetOfInfo}"
+    def debugInfo(using Context) = i"$this accountsFor $x"
 
     def test(using Context) = reporting.trace(debugInfo):
       elems.exists(_.subsumes(x))
@@ -209,8 +209,9 @@ sealed abstract class CaptureSet extends Showable:
    */
   def mightAccountFor(x: CaptureRef)(using Context): Boolean =
     reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true):
-      CCState.withCapAsRoot: // OK here since we opportunistically choose an alternative which gets checked later
-        elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded))
+      CCState.withCapAsRoot:
+        CCState.ignoringFreshLevels: // OK here since we opportunistically choose an alternative which gets checked later
+          elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded))
       || !x.isRootCapability
         && {
           val elems = x.captureSetOfInfo.elems
@@ -351,9 +352,27 @@ sealed abstract class CaptureSet extends Showable:
 
   def readOnly(using Context): CaptureSet = map(ReadOnlyMap())
 
-  /** Invoke handler if this set has (or later aquires) the root capability `cap` */
-  def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
-    if containsRootCapability then handler()
+  /** A bad root `elem` is inadmissible as a member of this set. What is a bad roots depends
+   *  on the value of `rootLimit`.
+   *  If the limit is null, all capture roots are good.
+   *  If the limit is NoSymbol, all Fresh roots are good, but cap and Result roots are bad.
+   *  If the limit is some other symbol, cap and Result roots are bad, as well as
+   *  all Fresh roots that are contained (via ccOwner) in `rootLimit`.
+   */
+  protected def isBadRoot(rootLimit: Symbol | Null, elem: CaptureRef)(using Context): Boolean =
+    if rootLimit == null then false
+    else
+      val elem1 = elem.stripReadOnly
+      elem1.isCap
+      || elem1.isResultRoot
+      || elem1.isFresh && elem1.ccOwner.isContainedIn(rootLimit)
+
+  /** Invoke `handler` if this set has (or later aquires) a root capability.
+   *  Excluded are Fresh instances unless their ccOwner is contained in `upto`.
+   *  If `upto` is NoSymbol, all Fresh instances are admitted.
+   */
+  def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
+    if elems.exists(isBadRoot(upto, _)) then handler()
     this
 
   /** Invoke handler on the elements to ensure wellformedness of the capture set.
@@ -423,8 +442,8 @@ object CaptureSet:
   def universalImpliedByCapability(using Context) =
     defn.universalCSImpliedByCapability
 
-  def fresh(owner: Symbol = NoSymbol)(using Context): CaptureSet =
-    root.Fresh.withOwner(owner).singletonCaptureSet
+  def fresh(origin: root.Origin)(using Context): CaptureSet =
+    root.Fresh(origin).singletonCaptureSet
 
   /** The shared capture set `{cap.rd}` */
   def shared(using Context): CaptureSet =
@@ -499,7 +518,7 @@ object CaptureSet:
       ccs.varId += 1
       ccs.varId
 
-    //assert(id != 40)
+    //assert(id != 8, this)
 
     /** A variable is solved if it is aproximated to a from-then-on constant set.
      *  Interpretation:
@@ -529,7 +548,10 @@ object CaptureSet:
     /** A handler to be invoked if the root reference `cap` is added to this set */
     var rootAddedHandler: () => Context ?=> Unit = () => ()
 
-    private[CaptureSet] var noUniversal = false
+    /** The limit deciding which capture roots are bad (i.e. cannot be contained in this set).
+     *  @see isBadRoot for details.
+     */
+    private[CaptureSet] var rootLimit: Symbol | Null = null
 
     /** A handler to be invoked when new elems are added to this set */
     var newElemAddedHandler: CaptureRef => Context ?=> Unit = _ => ()
@@ -580,7 +602,7 @@ object CaptureSet:
         assert(elem.isTrackableRef, elem)
         assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState])
         elems += elem
-        if elem.isRootCapability then
+        if isBadRoot(rootLimit, elem) then
           rootAddedHandler()
         newElemAddedHandler(elem)
         val normElem = if isMaybeSet then elem else elem.stripMaybe
@@ -600,37 +622,38 @@ object CaptureSet:
             case _ => foldOver(b, t)
       find(false, binder)
 
-    // TODO: Also track allowable TermParamRefs and root.Results in capture sets
-    private def levelOK(elem: CaptureRef)(using Context): Boolean =
-      if elem.isRootCapability then
-        !noUniversal
-      else elem match
-        case elem @ root.Result(mt) =>
-          !noUniversal && isPartOf(mt.resType)
-        case elem: TermRef if level.isDefined =>
-          elem.prefix match
-            case prefix: CaptureRef =>
-              levelOK(prefix)
-            case _ =>
-              ccState.symLevel(elem.symbol) <= level
-        case elem: ThisType if level.isDefined =>
-          ccState.symLevel(elem.cls).nextInner <= level
-        case elem: ParamRef if !this.isInstanceOf[BiMapped] =>
-          isPartOf(elem.binder.resType)
-          || {
-            capt.println(
-              i"""LEVEL ERROR $elem for $this
-                 |elem binder = ${elem.binder}""")
-            false
-          }
-        case ReachCapability(elem1) =>
-          levelOK(elem1)
-        case ReadOnlyCapability(elem1) =>
-          levelOK(elem1)
-        case MaybeCapability(elem1) =>
-          levelOK(elem1)
-        case _ =>
-          true
+    private def levelOK(elem: CaptureRef)(using Context): Boolean = elem match
+      case elem @ root.Fresh(_) =>
+        !level.isDefined
+        || ccState.symLevel(elem.ccOwner) <= level
+        || {
+          capt.println(i"LEVEL ERROR $elem cannot be included in $this of $owner")
+          false
+        }
+      case elem @ root.Result(mt) =>
+        rootLimit == null && (this.isInstanceOf[BiMapped] || isPartOf(mt.resType))
+      case elem: TermRef if elem.isCap =>
+        rootLimit == null
+      case elem: TermRef if level.isDefined =>
+        elem.prefix match
+          case prefix: CaptureRef =>
+            levelOK(prefix)
+          case _ =>
+            ccState.symLevel(elem.symbol) <= level
+      case elem: ThisType if level.isDefined =>
+        ccState.symLevel(elem.cls).nextInner <= level
+      case elem: ParamRef if !this.isInstanceOf[BiMapped] =>
+        isPartOf(elem.binder.resType)
+        || {
+          capt.println(
+            i"""LEVEL ERROR $elem for $this
+                |elem binder = ${elem.binder}""")
+          false
+        }
+      case QualifiedCapability(elem1) =>
+        levelOK(elem1)
+      case _ =>
+        true
 
     def addDependent(cs: CaptureSet)(using Context, VarState): CompareResult =
       if (cs eq this) || cs.isUniversal || isConst then
@@ -641,10 +664,10 @@ object CaptureSet:
       else
         CompareResult.Fail(this :: Nil)
 
-    override def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
-      noUniversal = true
+    override def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
+      rootLimit = upto
       rootAddedHandler = handler
-      super.disallowRootCapability(handler)
+      super.disallowRootCapability(upto)(handler)
 
     override def ensureWellformed(handler: CaptureRef => (Context) ?=> Unit)(using Context): this.type =
       newElemAddedHandler = handler
@@ -689,7 +712,7 @@ object CaptureSet:
     def solve()(using Context): Unit =
       CCState.withCapAsRoot: // // OK here since we infer parameter types that get checked later
         val approx = upperApprox(empty)
-          .map(root.CapToFresh(NoSymbol).inverse)    // Fresh --> cap
+          .map(root.CapToFresh(root.Origin.Unknown).inverse)    // Fresh --> cap
           .showing(i"solve $this = $result", capt)
         //println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}")
         val newElems = approx.elems -- elems
@@ -747,7 +770,7 @@ object CaptureSet:
    *  Test case: Without that tweak, logger.scala would not compile.
    */
   class RefiningVar(owner: Symbol)(using Context) extends Var(owner):
-    override def disallowRootCapability(handler: () => Context ?=> Unit)(using Context) = this
+    override def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) = this
 
   /** A variable that is derived from some other variable via a map or filter. */
   abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)
@@ -805,7 +828,7 @@ object CaptureSet:
             .showing(i"propagating new elem $elem backward from $this to $source = $result", captDebug)
             .andAlso(addNewElem(elem))
         catch case ex: AssertionError =>
-          println(i"fail while tryInclude $elem of ${elem.getClass} in $this / ${this.summarize}")
+          println(i"fail while prop backwards tryInclude $elem of ${elem.getClass} in $this / ${this.summarize}")
           throw ex
 
     /** For a BiTypeMap, supertypes of the mapped type also constrain
@@ -930,7 +953,7 @@ object CaptureSet:
 
     override def owner = givenOwner
 
-    // assert(id != 34, i"$initialHidden")
+    //assert(id != 4)
 
     private def aliasRef: AnnotatedType | Null =
       if myElems.size == 1 then
@@ -1162,11 +1185,19 @@ object CaptureSet:
      *  substBinder when comparing two method types. In that case we can unify
      *  the two roots1, provided none of the two roots have already been unified
      *  themselves. So unification must be 1-1.
+     *
+     *  Note, see (**) below: We also allow unifications of results that have different ExprType
+     *  binders. This is necessary because ExprTypes don't get updated with SubstBindingMaps.
+     *  It's sound since ExprTypes always appear alone and at the top-level, so there is
+     *  no problem with confusing results at different levels.
+     *  See pos-customargs/captures/overrides.scala for a test case.
      */
     def unify(root1: root.Result, root2: root.Result)(using Context): Boolean =
       (root1, root2) match
         case (root1 @ root.Result(binder1), root2 @ root.Result(binder2))
-        if (binder1 eq binder2)
+        if ((binder1 eq binder2)
+            || binder1.isInstanceOf[ExprType] && binder2.isInstanceOf[ExprType] // (**)
+            )
           && (root1.rootAnnot.originalBinder ne root2.rootAnnot.originalBinder)
           && eqResultMap(root1) == null
           && eqResultMap(root2) == null
@@ -1392,7 +1423,7 @@ object CaptureSet:
       def capturingCase(acc: CaptureSet, parent: Type, refs: CaptureSet) =
         this(acc, parent) ++ refs
       def abstractTypeCase(acc: CaptureSet, t: TypeRef, upperBound: Type) =
-        if includeTypevars && upperBound.isExactlyAny then CaptureSet.fresh(t.symbol)
+        if includeTypevars && upperBound.isExactlyAny then fresh(root.Origin.DeepCS(t))
         else this(acc, upperBound)
     collect(CaptureSet.empty, tp)
 
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 358b99c58078..d15fa06e64fc 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -123,7 +123,7 @@ object CheckCaptures:
    *  root capability in its capture set or if it refers to a type parameter that
    *  could possibly be instantiated with cap in a way that's visible at the type.
    */
-  private def disallowRootCapabilitiesIn(tp: Type, carrier: Symbol, what: String, have: String, addendum: String, pos: SrcPos)(using Context) =
+  private def disallowRootCapabilitiesIn(tp: Type, upto: Symbol, what: String, have: String, addendum: String, pos: SrcPos)(using Context) =
     val check = new TypeTraverser:
 
       private val seen = new EqHashSet[TypeRef]
@@ -150,7 +150,7 @@ object CheckCaptures:
           case CapturingType(parent, refs) =>
             if variance >= 0 then
               val openScopes = openExistentialScopes
-              refs.disallowRootCapability: () =>
+              refs.disallowRootCapability(upto): () =>
                 def part =
                   if t eq tp then ""
                   else
@@ -373,8 +373,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                 case added: CaptureRef => target.elems += added
                 case added: CaptureSet => target.elems ++= added.elems
             case _ =>
-              inContext(root.printContext(added, res.blocking)):
-                report.error(msg(provisional = false), pos)
+              report.error(msg(provisional = false), pos)
         case _ =>
 
     /** Check subcapturing `{elem} <: cs`, report error on failure */
@@ -489,7 +488,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             case _ =>
               CaptureSet.ofType(c.widen, followResult = false)
             capt.println(i"Widen reach $c to $underlying in ${env.owner}")
-          underlying.disallowRootCapability: () =>
+          underlying.disallowRootCapability(NoSymbol): () =>
             report.error(em"Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set", tree.srcPos)
           recur(underlying, env, lastEnv)
 
@@ -518,7 +517,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                 // fresh capabilities. We don't need to also follow the hidden set since separation
                 // checking makes ure that locally hidden references need to go to @consume parameters.
             else
-              underlying.disallowRootCapability: () =>
+              underlying.disallowRootCapability(ctx.owner): () =>
                 report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", tree.srcPos)
               recur(underlying, env, null)
         case c: TypeRef if c.isParamPath =>
@@ -557,6 +556,16 @@ class CheckCaptures extends Recheck, SymTransformer:
         if sym.exists && curEnv.isOpen then
           markFree(capturedVars(sym).filter(isRetained), tree)
 
+    /** If `tp` (possibly after widening singletons) is an ExprType
+     *  of a parameterless method, map Result instances in it to Fresh instances
+     */
+    def mapResultRoots(tp: Type, sym: Symbol)(using Context): Type =
+      tp.widenSingleton match
+        case tp: ExprType if sym.is(Method) =>
+          root.resultToFresh(tp, root.Origin.ResultInstance(tp, sym))
+        case _ =>
+          tp
+
     /** Under the sealed policy, disallow the root capability in type arguments.
      *  Type arguments come either from a TypeApply node or from an AppliedType
      *  which represents a trait parent in a template.
@@ -581,7 +590,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           def where = if sym.exists then i" in an argument of $sym" else ""
           val (addendum, errTree) =
             if arg.isInferred
-            then ("\nThis is often caused by a local capability$where\nleaking as part of its result.", fn)
+            then (i"\nThis is often caused by a local capability$where\nleaking as part of its result.", fn)
             else if arg.span.exists then ("", arg)
             else ("", fn)
           disallowRootCapabilitiesIn(arg.nuType, NoSymbol,
@@ -619,7 +628,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         if pathRef.derivesFrom(defn.Caps_Mutable) && pt.isValueType && !pt.isMutableType then
           pathRef = pathRef.readOnly
         markFree(sym, pathRef, tree)
-      super.recheckIdent(tree, pt)
+      mapResultRoots(super.recheckIdent(tree, pt), tree.symbol)
 
     /** The expected type for the qualifier of a selection. If the selection
      *  could be part of a capability path or is a a read-only method, we return
@@ -666,7 +675,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                 |since its capture set ${qualType.captureSet} is read-only""",
             tree.srcPos)
 
-      val selType = recheckSelection(tree, qualType, name, disambiguate)
+      val selType = mapResultRoots(recheckSelection(tree, qualType, name, disambiguate), tree.symbol)
       val selWiden = selType.widen
 
       // Don't apply the rule
@@ -715,7 +724,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       val meth = tree.fun.symbol
       if meth == defn.Caps_unsafeAssumePure then
         val arg :: Nil = tree.args: @unchecked
-        val argType0 = recheck(arg, pt.stripCapturing.capturing(root.Fresh()))
+        val argType0 = recheck(arg, pt.stripCapturing.capturing(root.Fresh(root.Origin.UnsafeAssumePure)))
         val argType =
           if argType0.captureSet.isAlwaysEmpty then argType0
           else argType0.widen.stripCapturing
@@ -730,8 +739,8 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  occurrences are replaced by `Fresh` instances. Also, if formal parameter carries a `@use`,
      *  charge the deep capture set of the actual argument to the environment.
      */
-    protected override def recheckArg(arg: Tree, formal: Type)(using Context): Type =
-      val freshenedFormal = root.capToFresh(formal)
+    protected override def recheckArg(arg: Tree, formal: Type, pref: ParamRef, app: Apply)(using Context): Type =
+      val freshenedFormal = root.capToFresh(formal, root.Origin.Formal(pref, app))
       val argType = recheck(arg, freshenedFormal)
         .showing(i"recheck arg $arg vs $freshenedFormal = $result", capt)
       if formal.hasAnnotation(defn.UseAnnot) || formal.hasAnnotation(defn.ConsumeAnnot) then
@@ -765,7 +774,9 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     protected override
     def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
-      val appType = root.resultToFresh(super.recheckApplication(tree, qualType, funType, argTypes))
+      val appType = root.resultToFresh(
+        super.recheckApplication(tree, qualType, funType, argTypes),
+        root.Origin.ResultInstance(funType, tree.symbol))
       val qualCaptures = qualType.captureSet
       val argCaptures =
         for (argType, formal) <- argTypes.lazyZip(funType.paramInfos) yield
@@ -824,14 +835,15 @@ class CheckCaptures extends Recheck, SymTransformer:
       def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
         var refined: Type = core
         var allCaptures: CaptureSet =
-          if core.derivesFromMutable then initCs ++ CaptureSet.fresh()
-          else if core.derivesFromCapability then initCs ++ root.Fresh.withOwner(core.classSymbol).readOnly.singletonCaptureSet
+          if core.derivesFromMutable then
+            initCs ++ root.Fresh(root.Origin.NewMutable(core)).singletonCaptureSet
+          else if core.derivesFromCapability then
+            initCs ++ root.Fresh(root.Origin.NewCapability(core)).readOnly.singletonCaptureSet
           else initCs
         for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
           val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol
           if !getter.is(Private) && getter.hasTrackedParts then
-            refined = RefinedType(refined, getterName,
-              AnnotatedType(argType.unboxed, Annotation(defn.RefineOverrideAnnot, util.Spans.NoSpan))) // Yichen you might want to check this
+            refined = refined.refinedOverride(getterName, argType.unboxed) // Yichen you might want to check this
             allCaptures ++= argType.captureSet
         (refined, allCaptures)
 
@@ -865,8 +877,10 @@ class CheckCaptures extends Recheck, SymTransformer:
       val meth = tree.fun match
         case fun @ Select(qual, nme.apply) => qual.symbol.orElse(fun.symbol)
         case fun => fun.symbol
+      def methDescr = if meth.exists then i"$meth's type " else ""
       disallowCapInTypeArgs(tree.fun, meth, tree.args)
-      val res = root.resultToFresh(super.recheckTypeApply(tree, pt))
+      val funType = super.recheckTypeApply(tree, pt)
+      val res = root.resultToFresh(funType, root.Origin.ResultInstance(funType, meth))
       includeCallCaptures(tree.symbol, res, tree)
       checkContains(tree)
       res
@@ -887,9 +901,6 @@ class CheckCaptures extends Recheck, SymTransformer:
             report.error(em"$refArg is not a tracked capability", refArg.srcPos)
       case _ =>
 
-    override def recheckBlock(tree: Block, pt: Type)(using Context): Type =
-      ccState.inNestedLevel(super.recheckBlock(tree, pt))
-
     /** Recheck Closure node: add the captured vars of the anonymoys function
      *  to the result type. See also `recheckClosureBlock` which rechecks the
      *  block containing the anonymous function and the Closure node.
@@ -929,14 +940,14 @@ class CheckCaptures extends Recheck, SymTransformer:
               // neg-custom-args/captures/vars.scala. That's why this code is conditioned.
               // to apply only to closures that are not eta expansions.
               assert(paramss1.isEmpty)
-              val respt = root.resultToFresh:
-                pt match
-                  case defn.RefinedFunctionOf(rinfo) =>
-                    val paramTypes = params.map(_.asInstanceOf[ValDef].tpt.nuType)
-                    rinfo.instantiate(paramTypes)
-                  case _ =>
-                    resType
-              val res = root.resultToFresh(mdef.tpt.nuType)
+              val respt0 = pt match
+                case defn.RefinedFunctionOf(rinfo) =>
+                  val paramTypes = params.map(_.asInstanceOf[ValDef].tpt.nuType)
+                  rinfo.instantiate(paramTypes)
+                case _ =>
+                  resType
+              val respt = root.resultToFresh(respt0, root.Origin.LambdaExpected(respt0))
+              val res = root.resultToFresh(mdef.tpt.nuType, root.Origin.LambdaActual(mdef.tpt.nuType))
               // We need to open existentials here in order not to get vars mixed up in them
               // We do the proper check with existentials when we are finished with the closure block.
               capt.println(i"pre-check closure $expr of type $res against $respt")
@@ -977,7 +988,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         if sym.is(Module) then sym.info // Modules are checked by checking the module class
         else
           if sym.is(Mutable) && !sym.hasAnnotation(defn.UncheckedCapturesAnnot) then
-            val (carrier, addendum) = capturedBy.get(sym) match
+            val addendum = capturedBy.get(sym) match
               case Some(encl) =>
                 val enclStr =
                   if encl.isAnonymousFunction then
@@ -986,11 +997,11 @@ class CheckCaptures extends Recheck, SymTransformer:
                       case _ => ""
                     s"an anonymous function$location"
                   else encl.show
-                (NoSymbol, i"\n\nNote that $sym does not count as local since it is captured by $enclStr")
+                i"\n\nNote that $sym does not count as local since it is captured by $enclStr"
               case _ =>
-                (sym, "")
+                ""
             disallowRootCapabilitiesIn(
-              tree.tpt.nuType, carrier, i"Mutable $sym", "have type", addendum, sym.srcPos)
+              tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos)
           checkInferredResult(super.recheckValDef(tree, sym), tree)
       finally
         if !sym.is(Param) then
@@ -1189,7 +1200,12 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  result type of a try
      */
     override def recheckTry(tree: Try, pt: Type)(using Context): Type =
-      val tp = super.recheckTry(tree, pt)
+      val tryOwner = Setup.firstCanThrowEvidence(tree.expr) match
+        case Some(vd) => vd.symbol.owner
+        case None => ctx.owner
+      val bodyType = inContext(ctx.withOwner(tryOwner)):
+        recheck(tree.expr, pt)
+      val tp = recheckTryRest(bodyType, tree.cases, tree.finalizer, pt)
       if Feature.enabled(Feature.saferExceptions) then
         disallowRootCapabilitiesIn(tp, ctx.owner,
           "The result of `try`", "have type",
@@ -1261,8 +1277,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           val msg = note match
             case CompareResult.LevelError(cs, ref) =>
               if ref.stripReadOnly.isCapOrFresh then
-                def capStr = if ref.isReadOnly then "cap.rd" else "cap"
-                i"""the universal capability `$capStr`
+                i"""the universal capability $ref
                    |cannot be included in capture set $cs"""
               else
                 val levelStr = ref match
@@ -1328,9 +1343,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           actualBoxed
         case fail: CompareFailure =>
           capt.println(i"conforms failed for ${tree}: $actual vs $expected")
-          inContext(root.printContext(actualBoxed, expected1)):
-            err.typeMismatch(tree.withType(actualBoxed), expected1,
-                addApproxAddenda(
+          err.typeMismatch(tree.withType(actualBoxed), expected1,
+              addApproxAddenda(
                   addenda ++ errorNotes(fail.errorNotes),
                   expected1))
           actual
@@ -1496,9 +1510,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           val cs = actual.captureSet
           if covariant then cs ++ leaked
           else
-            if // CCState.withCapAsRoot: // Not sure withCapAsRoot is OK here, actually
-              !leaked.subCaptures(cs).isOK
-            then
+            if !leaked.subCaptures(cs).isOK 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)
@@ -1637,7 +1649,8 @@ class CheckCaptures extends Recheck, SymTransformer:
                           memberTp,
                           otherTp.derivedTypeBounds(
                             otherTp.lo,
-                            hi.derivedCapturingType(parent, root.Fresh().singletonCaptureSet))))
+                            hi.derivedCapturingType(parent,
+                                CaptureSet.fresh(root.Origin.OverriddenType(member))))))
                       case _ => None
                   case _ => None
               case _ => None
@@ -1696,7 +1709,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       def traverse(t: Tree)(using Context) =
         t match
           case t: Template =>
-            checkAllOverrides(ctx.owner.asClass, OverridingPairsCheckerCC(_, _, t))
+            ignoringFreshLevels:
+              checkAllOverrides(ctx.owner.asClass, OverridingPairsCheckerCC(_, _, t))
           case _ =>
         traverseChildren(t)
     end checkOverrides
@@ -1900,7 +1914,8 @@ class CheckCaptures extends Recheck, SymTransformer:
                   arg.withType(arg.nuType.forceBoxStatus(
                     bounds.hi.isBoxedCapturing | bounds.lo.isBoxedCapturing))
                 CCState.withCapAsRoot: // OK? We need this since bounds use `cap` instead of `fresh`
-                  checkBounds(normArgs, tl)
+                  CCState.ignoringFreshLevels:
+                    checkBounds(normArgs, tl)
                 if ccConfig.postCheckCapturesets then
                   args.lazyZip(tl.paramNames).foreach(checkTypeParam(_, _, fun.symbol))
               case _ =>
@@ -1920,7 +1935,8 @@ class CheckCaptures extends Recheck, SymTransformer:
             case tree: New =>
             case tree: TypeTree =>
               CCState.withCapAsRoot:
-                checkAppliedTypesIn(tree.withType(tree.nuType))
+                CCState.ignoringFreshLevels:
+                  checkAppliedTypesIn(tree.withType(tree.nuType))
             case _ => traverseChildren(t)
         checkApplied.traverse(unit)
     end postCheck
diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index 6434db0638a3..af3c70a0a491 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -915,7 +915,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           traverseChildren(tree)
           checkValOrDefDef(tree)
         case tree: DefDef =>
-          inSection:
+          if tree.symbol.isInlineMethod then
+            // We currently skip inline method since these seem to generate
+            // spurious recheck completions. Test case is i20237.scala
+            capt.println(i"skipping sep check of inline def ${tree.symbol}")
+          else inSection:
             consumed.segment:
               for params <- tree.paramss; case param: ValDef <- params do
                 pushDef(param, emptyRefs)
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 21c58385b58a..7dd9c1e0cd30 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -21,6 +21,7 @@ import CCState.*
 import dotty.tools.dotc.util.NoSourcePosition
 import CheckCaptures.CheckerAPI
 import NamerOps.methodType
+import NameKinds.{CanThrowEvidenceName, TryOwnerName}
 
 /** Operations accessed from CheckCaptures */
 trait SetupAPI:
@@ -51,6 +52,15 @@ object Setup:
         Some((res, exc))
       case _ =>
         None
+
+  def firstCanThrowEvidence(body: Tree)(using Context): Option[Tree] = body match
+    case Block(stats, expr) =>
+      if stats.isEmpty then firstCanThrowEvidence(expr)
+      else stats.find:
+        case vd: ValDef => vd.symbol.name.is(CanThrowEvidenceName)
+        case _ => false
+    case _ => None
+
 end Setup
 import Setup.*
 
@@ -211,9 +221,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           case AppliedType(`tycon`, args0) => args0.last ne args.last
           case _ => false
         if expand then
-          depFun(args.init, args.last,
+          val fn = depFun(
+            args.init, args.last,
             isContextual = defn.isContextFunctionClass(tycon.classSymbol))
               .showing(i"add function refinement $tp ($tycon, ${args.init}, ${args.last}) --> $result", capt)
+          AnnotatedType(fn, Annotation(defn.InferredDepFunAnnot, util.Spans.NoSpan))
         else tp
       case _ => tp
 
@@ -323,7 +335,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
     try
       val tp1 = mapInferred(refine = true)(tp)
-      val tp2 = root.toResultInResults(_ => assert(false))(tp1)
+      val tp2 = root.toResultInResults(NoSymbol, _ => assert(false))(tp1)
       if tp2 ne tp then capt.println(i"expanded inferred in ${ctx.owner}: $tp  -->  $tp1  -->  $tp2")
       tp2
     catch case ex: AssertionError =>
@@ -458,7 +470,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
     def transform(tp: Type): Type =
       val tp1 = toCapturing(tp)
-      val tp2 = root.toResultInResults(fail, toCapturing.keepFunAliases)(tp1)
+      val tp2 = root.toResultInResults(sym, fail, toCapturing.keepFunAliases)(tp1)
       val snd = if toCapturing.keepFunAliases then "" else " 2nd time"
       if tp2 ne tp then capt.println(i"expanded explicit$snd in ${ctx.owner}: $tp  -->  $tp1  -->  $tp2")
       tp2
@@ -472,14 +484,15 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     val tp3 =
       if sym.isType then stripImpliedCaptureSet(tp2)
       else tp2
-    if freshen then root.capToFresh(tp3).tap(addOwnerAsHidden(_, sym))
+    if freshen then
+      root.capToFresh(tp3, root.Origin.InDecl(sym)).tap(addOwnerAsHidden(_, sym))
     else tp3
   end transformExplicitType
 
   /** Update info of `sym` for CheckCaptures phase only */
-  private def updateInfo(sym: Symbol, info: Type)(using Context) =
+  private def updateInfo(sym: Symbol, info: Type, owner: Symbol)(using Context) =
     toBeUpdated += sym
-    sym.updateInfo(thisPhase, info, newFlagsFor(sym))
+    sym.updateInfo(thisPhase, info, newFlagsFor(sym), owner)
     toBeUpdated -= sym
 
   /** The info of `sym` at the CheckCaptures phase */
@@ -568,7 +581,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           traverse(fn)
           for case arg: TypeTree <- args do
             if defn.isTypeTestOrCast(fn.symbol) then
-              arg.setNuType(root.capToFresh(arg.tpe))
+              arg.setNuType(
+                root.capToFresh(arg.tpe, root.Origin.TypeArg(arg.tpe)))
             else
               transformTT(arg, NoSymbol, boxed = true) // type arguments in type applications are boxed
 
@@ -586,9 +600,17 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           traverse(elems)
           tpt.setNuType(box(transformInferredType(tpt.tpe)))
 
-        case tree: Block =>
-          ccState.inNestedLevel(traverseChildren(tree))
-
+        case tree @ Try(body, catches, finalizer) =>
+          val tryOwner = firstCanThrowEvidence(body) match
+            case Some(vd) =>
+              newSymbol(ctx.owner, TryOwnerName.fresh(),
+                Method | Synthetic, ExprType(defn.NothingType), coord = tree.span)
+            case _ =>
+              ctx.owner
+          inContext(ctx.withOwner(tryOwner)):
+            traverse(body)
+          catches.foreach(traverse)
+          traverse(finalizer)
         case _ =>
           traverseChildren(tree)
       postProcess(tree)
@@ -633,6 +655,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
         // have a new type installed here (meaning hasRememberedType is true)
         def signatureChanges =
           tree.tpt.hasNuType || paramSignatureChanges
+        def ownerChanges =
+          ctx.owner.name.is(TryOwnerName)
 
         def paramsToCap(mt: Type)(using Context): Type = mt match
           case mt: MethodType =>
@@ -643,38 +667,40 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
             mt.derivedLambdaType(resType = paramsToCap(mt.resType))
           case _ => mt
 
-        // If there's a change in the signature, update the info of `sym`
-        if sym.exists && signatureChanges then
+        // If there's a change in the signature or owner, update the info of `sym`
+        if sym.exists && (signatureChanges || ownerChanges) then
           val updatedInfo =
-
-            val paramSymss = sym.paramSymss
-            def newInfo(using Context) = // will be run in this or next phase
-              root.toResultInResults(report.error(_, tree.srcPos)):
-                if sym.is(Method) then
-                  paramsToCap(methodType(paramSymss, localReturnType))
-                else tree.tpt.nuType
-            if tree.tpt.isInstanceOf[InferredTypeTree]
-                && !sym.is(Param) && !sym.is(ParamAccessor)
-            then
-              val prevInfo = sym.info
-              new LazyType:
-                def complete(denot: SymDenotation)(using Context) =
-                  assert(ctx.phase == thisPhase.next, i"$sym")
-                  sym.info = prevInfo // set info provisionally so we can analyze the symbol in recheck
-                  completeDef(tree, sym, this)
-                  sym.info = newInfo
-                    .showing(i"new info of $sym = $result", capt)
-            else if sym.is(Method) then
-              new LazyType:
-                def complete(denot: SymDenotation)(using Context) =
-                  sym.info = newInfo
-                    .showing(i"new info of $sym = $result", capt)
-            else newInfo
-          updateInfo(sym, updatedInfo)
+            if signatureChanges then
+              val paramSymss = sym.paramSymss
+              def newInfo(using Context) = // will be run in this or next phase
+                root.toResultInResults(sym, report.error(_, tree.srcPos)):
+                  if sym.is(Method) then
+                    paramsToCap(methodType(paramSymss, localReturnType))
+                  else tree.tpt.nuType
+              if tree.tpt.isInstanceOf[InferredTypeTree]
+                  && !sym.is(Param) && !sym.is(ParamAccessor)
+              then
+                val prevInfo = sym.info
+                new LazyType:
+                  def complete(denot: SymDenotation)(using Context) =
+                    assert(ctx.phase == thisPhase.next, i"$sym")
+                    sym.info = prevInfo // set info provisionally so we can analyze the symbol in recheck
+                    completeDef(tree, sym, this)
+                    sym.info = newInfo
+                      .showing(i"new info of $sym = $result", capt)
+              else if sym.is(Method) then
+                new LazyType:
+                  def complete(denot: SymDenotation)(using Context) =
+                    sym.info = newInfo
+                      .showing(i"new info of $sym = $result", capt)
+              else newInfo
+            else sym.info
+          val updatedOwner = if ownerChanges then ctx.owner else sym.owner
+          updateInfo(sym, updatedInfo, updatedOwner)
 
       case tree: Bind =>
         val sym = tree.symbol
-        updateInfo(sym, transformInferredType(sym.info))
+        updateInfo(sym, transformInferredType(sym.info), sym.owner)
       case tree: TypeDef =>
         tree.symbol match
           case cls: ClassSymbol =>
@@ -707,7 +733,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
               // Install new types and if it is a module class also update module object
               if (selfInfo1 ne selfInfo) || (ps1 ne ps) then
                 val newInfo = ClassInfo(prefix, cls, ps1, decls, selfInfo1)
-                updateInfo(cls, newInfo)
+                updateInfo(cls, newInfo, cls.owner)
                 capt.println(i"update class info of $cls with parents $ps selfinfo $selfInfo to $newInfo")
                 cls.thisType.asInstanceOf[ThisType].invalidateCaches()
                 if cls.is(ModuleClass) then
@@ -720,7 +746,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                   // This would potentially give stackoverflows when setup is run repeatedly.
                   // One test case is pos-custom-args/captures/checkbounds.scala under
                   // ccConfig.alwaysRepeatRun = true.
-                  updateInfo(modul, CapturingType(modul.info, selfCaptures))
+                  updateInfo(modul, CapturingType(modul.info, selfCaptures), modul.owner)
                   modul.termRef.invalidateCaches()
           case _ =>
       case _ =>
diff --git a/compiler/src/dotty/tools/dotc/cc/Synthetics.scala b/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
index cdc3afff8a2d..0f7a3a3ee022 100644
--- a/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
@@ -77,12 +77,11 @@ object Synthetics:
           case tp: MethodOrPoly =>
             tp.derivedLambdaType(resType = augmentResult(tp.resType))
           case _ =>
-            val refined = trackedParams.foldLeft(tp) { (parent, pref) =>
-              RefinedType(parent, pref.paramName,
+            val refined = trackedParams.foldLeft(tp): (parent, pref) =>
+              parent.refinedOverride(pref.paramName,
                 CapturingType(
                   atPhase(ctx.phase.next)(pref.underlying.stripCapturing),
                   CaptureSet(pref)))
-            }
             CapturingType(refined, CaptureSet(trackedParams*))
         if trackedParams.isEmpty then info
         else augmentResult(info).showing(i"augment apply/copy type $info to $result", capt)
@@ -116,7 +115,7 @@ object Synthetics:
     def transformUnapplyCaptures(info: Type)(using Context): Type = info match
       case info: MethodType =>
         val paramInfo :: Nil = info.paramInfos: @unchecked
-        val newParamInfo = CapturingType(paramInfo, CaptureSet.fresh())
+        val newParamInfo = CapturingType(paramInfo, CaptureSet.universal)
         val trackedParam = info.paramRefs.head
         def newResult(tp: Type): Type = tp match
           case tp: MethodOrPoly =>
diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
index 4c06f4a0843d..c66c7972eaf5 100644
--- a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
+++ b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
@@ -50,8 +50,12 @@ object ccConfig:
   def useSepChecks(using Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
 
+  /** If true, do level checking for root.Fresh instances */
+  def useFreshLevels(using Context): Boolean =
+    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
+
   /** Not used currently. Handy for trying out new features */
   def newScheme(using Context): Boolean =
-    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.8`)
+    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
 
 end ccConfig
\ No newline at end of file
diff --git a/compiler/src/dotty/tools/dotc/cc/root.scala b/compiler/src/dotty/tools/dotc/cc/root.scala
index 472dd37aa543..3c6620678b09 100644
--- a/compiler/src/dotty/tools/dotc/cc/root.scala
+++ b/compiler/src/dotty/tools/dotc/cc/root.scala
@@ -13,7 +13,7 @@ import NameKinds.ExistentialBinderName
 import NameOps.isImpureFunction
 import reporting.Message
 import util.{SimpleIdentitySet, EqHashMap}
-import util.Spans.NoSpan
+import ast.tpd
 import annotation.constructorOnly
 
 /** A module defining three kinds of root capabilities
@@ -59,9 +59,58 @@ import annotation.constructorOnly
  */
 object root:
 
+  enum Origin:
+    case InDecl(sym: Symbol)
+    case TypeArg(tp: Type)
+    case UnsafeAssumePure
+    case Formal(pref: ParamRef, app: tpd.Apply)
+    case ResultInstance(methType: Type, meth: Symbol)
+    case UnapplyInstance(info: MethodType)
+    case NewMutable(tp: Type)
+    case NewCapability(tp: Type)
+    case LambdaExpected(respt: Type)
+    case LambdaActual(restp: Type)
+    case OverriddenType(member: Symbol)
+    case DeepCS(ref: TypeRef)
+    case Unknown
+
+    def explanation(using Context): String = this match
+      case InDecl(sym: Symbol) =>
+        if sym.is(Method) then i" in the result type of $sym"
+        else if sym.exists then i" in the type of $sym"
+        else ""
+      case TypeArg(tp: Type) =>
+        i" of type argument $tp"
+      case UnsafeAssumePure =>
+        " when instantiating argument of unsafeAssumePure"
+      case Formal(pref, app) =>
+        val meth = app.symbol
+        if meth.exists
+        then i" when checking argument to parameter ${pref.paramName} of $meth"
+        else ""
+      case ResultInstance(mt, meth) =>
+        val methDescr = if meth.exists then i"$meth's type " else ""
+        i" when instantiating $methDescr$mt"
+      case UnapplyInstance(info) =>
+        i" when instantiating argument of unapply with type $info"
+      case NewMutable(tp) =>
+        i" when constructing mutable $tp"
+      case NewCapability(tp) =>
+        i" when constructing Capability instance $tp"
+      case LambdaExpected(respt) =>
+        i" when instantiating expected result type $respt of lambda"
+      case LambdaActual(restp: Type) =>
+        i" when instantiating result type $restp of lambda"
+      case OverriddenType(member: Symbol) =>
+        i" when instantiating upper bound of member overridden by $member"
+      case DeepCS(ref: TypeRef) =>
+        i" when computing deep capture set of $ref"
+      case Unknown =>
+        ""
+
   enum Kind:
-    case Result(binder: MethodType)
-    case Fresh(hidden: CaptureSet.HiddenSet)
+    case Result(binder: MethodicType)
+    case Fresh(hidden: CaptureSet.HiddenSet)(val origin: Origin)
     case Global
 
     override def equals(other: Any): Boolean =
@@ -84,12 +133,14 @@ object root:
       ccs.rootId += 1
       ccs.rootId
 
+    //assert(id != 4, kind)
+
     override def symbol(using Context) = defn.RootCapabilityAnnot
     override def tree(using Context) = New(symbol.typeRef, Nil)
     override def derivedAnnotation(tree: Tree)(using Context): Annotation = this
 
     private var myOriginalKind = kind
-    def originalBinder: MethodType = myOriginalKind.asInstanceOf[Kind.Result].binder
+    def originalBinder: MethodicType = myOriginalKind.asInstanceOf[Kind.Result].binder
 
     def derivedAnnotation(binder: MethodType)(using Context): Annotation = kind match
       case Kind.Result(b) if b ne binder =>
@@ -104,7 +155,7 @@ object root:
       case Annot(kind) => this.kind eq kind
       case _ => false
 
-    /** Special treatment of `SubstBindingMaps` which can change the binder of a
+    /** Special treatment of `SubstBindingMaps` which can change the binder of
      *  Result instances
      */
     override def mapWith(tm: TypeMap)(using Context) = kind match
@@ -125,21 +176,18 @@ object root:
   /** The type of fresh references */
   type Fresh = AnnotatedType
 
+  /** Constructor and extractor methods for "fresh" capabilities */
   object Fresh:
-    /** Constructor and extractor methods for "fresh" capabilities */
-    private def make(owner: Symbol)(using Context): CaptureRef =
+    def apply(using Context)(origin: Origin, owner: Symbol = ctx.owner): CaptureRef =
       if ccConfig.useSepChecks then
         val hiddenSet = CaptureSet.HiddenSet(owner)
-        val res = AnnotatedType(cap, Annot(Kind.Fresh(hiddenSet)))
+        val res = AnnotatedType(cap, Annot(Kind.Fresh(hiddenSet)(origin)))
         hiddenSet.owningCap = res
         //assert(hiddenSet.id != 3)
         res
       else
         cap
 
-    def withOwner(owner: Symbol)(using Context): CaptureRef = make(owner)
-    def apply()(using Context): CaptureRef = make(NoSymbol)
-
     def unapply(tp: AnnotatedType): Option[CaptureSet.HiddenSet] = tp.annot match
       case Annot(Kind.Fresh(hidden)) => Some(hidden)
       case _ => None
@@ -149,13 +197,13 @@ object root:
   type Result = AnnotatedType
 
   object Result:
-    def apply(binder: MethodType)(using Context): Result =
+    def apply(binder: MethodicType)(using Context): Result =
       val hiddenSet = CaptureSet.HiddenSet(NoSymbol)
       val res = AnnotatedType(cap, Annot(Kind.Result(binder)))
       hiddenSet.owningCap = res
       res
 
-    def unapply(tp: Result)(using Context): Option[MethodType] = tp.annot match
+    def unapply(tp: Result)(using Context): Option[MethodicType] = tp.annot match
       case Annot(Kind.Result(binder)) => Some(binder)
       case _ => None
   end Result
@@ -168,14 +216,14 @@ object root:
   /** Map each occurrence of cap to a different Fresh instance
    *  Exception: CapSet^ stays as it is.
    */
-  class CapToFresh(owner: Symbol)(using Context) extends BiTypeMap, FollowAliasesMap:
+  class CapToFresh(origin: Origin)(using Context) extends BiTypeMap, FollowAliasesMap:
     thisMap =>
 
     override def apply(t: Type) =
       if variance <= 0 then t
       else t match
         case t: CaptureRef if t.isCap =>
-          Fresh.withOwner(owner)
+          Fresh(origin)
         case t @ CapturingType(parent: TypeRef, _) if parent.symbol == defn.Caps_CapSet =>
           t
         case t @ CapturingType(_, _) =>
@@ -212,16 +260,24 @@ object root:
 
   end CapToFresh
 
-  /** Maps cap to fresh */
-  def capToFresh(tp: Type, owner: Symbol = NoSymbol)(using Context): Type =
-    if ccConfig.useSepChecks then CapToFresh(owner)(tp) else tp
+  /** Maps cap to fresh. CapToFresh is a BiTypeMap since we don't want to
+   *  freeze a set when it is mapped. On the other hand, we do not want Fresh
+   *  values to flow back to cap since that would fail disallowRootCapability
+   *  tests elsewhere. We therefore use `withoutMappedFutureElems` to prevent
+   *  the map being installed for future use.
+   */
+  def capToFresh(tp: Type, origin: Origin)(using Context): Type =
+    if ccConfig.useSepChecks then
+      ccState.withoutMappedFutureElems:
+        CapToFresh(origin)(tp)
+    else tp
 
   /** Maps fresh to cap */
   def freshToCap(tp: Type)(using Context): Type =
-    if ccConfig.useSepChecks then CapToFresh(NoSymbol).inverse(tp) else tp
+    if ccConfig.useSepChecks then CapToFresh(Origin.Unknown).inverse(tp) else tp
 
   /** Map top-level free existential variables one-to-one to Fresh instances */
-  def resultToFresh(tp: Type)(using Context): Type =
+  def resultToFresh(tp: Type, origin: Origin)(using Context): Type =
     val subst = new TypeMap:
       val seen = EqHashMap[Annotation, CaptureRef]()
       var localBinders: SimpleIdentitySet[MethodType] = SimpleIdentitySet.empty
@@ -229,7 +285,7 @@ object root:
       def apply(t: Type): Type = t match
         case t @ Result(binder) =>
           if localBinders.contains(binder) then t // keep bound references
-          else seen.getOrElseUpdate(t.annot, Fresh()) // map free references to Fresh()
+          else seen.getOrElseUpdate(t.annot, Fresh(origin)) // map free references to Fresh()
         case t: MethodType =>
           // skip parameters
           val saved = localBinders
@@ -249,7 +305,7 @@ object root:
    *  variable bound by `mt`.
    *  Stop at function or method types since these have been mapped before.
    */
-  def toResult(tp: Type, mt: MethodType, fail: Message => Unit)(using Context): Type =
+  def toResult(tp: Type, mt: MethodicType, fail: Message => Unit)(using Context): Type =
 
     abstract class CapMap extends BiTypeMap:
       override def mapOver(t: Type): Type = t match
@@ -295,7 +351,7 @@ object root:
               val (k, v) = it.next
               if v.annot eq t.annot then ref = k
             if ref == null then
-              ref = Fresh()
+              ref = Fresh(Origin.Unknown)
               seen(ref) = t
             ref
           case _ => mapOver(t)
@@ -306,53 +362,38 @@ object root:
     toVar(tp)
   end toResult
 
-  /** Map global roots in function results to result roots */
-  def toResultInResults(fail: Message => Unit, keepAliases: Boolean = false)(using Context): TypeMap = new TypeMap with FollowAliasesMap:
-    def apply(t: Type): Type = t match
-      case defn.RefinedFunctionOf(mt) =>
-        val mt1 = apply(mt)
-        if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
-        else t
-      case t: MethodType if variance > 0 && t.marksExistentialScope =>
-        val t1 = mapOver(t).asInstanceOf[MethodType]
-        t1.derivedLambdaType(resType = toResult(t1.resType, t1, fail))
-      case CapturingType(parent, refs) =>
-        t.derivedCapturingType(this(parent), refs)
-      case t: (LazyRef | TypeVar) =>
-        mapConserveSuper(t)
-      case _ =>
-        try
-          if keepAliases then mapOver(t)
-          else mapFollowingAliases(t)
-        catch case ex: AssertionError =>
-          println(i"error while mapping $t")
-          throw ex
+  /** Map global roots in function results to result roots. Also,
+   *  map roots in the types of parameterless def methods.
+   */
+  def toResultInResults(sym: Symbol, fail: Message => Unit, keepAliases: Boolean = false)(tp: Type)(using Context): Type =
+    val m = new TypeMap with FollowAliasesMap:
+      def apply(t: Type): Type = t match
+        case AnnotatedType(parent @ defn.RefinedFunctionOf(mt), ann) if ann.symbol == defn.InferredDepFunAnnot =>
+          val mt1 = mapOver(mt).asInstanceOf[MethodType]
+          if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
+          else parent
+        case defn.RefinedFunctionOf(mt) =>
+          val mt1 = apply(mt)
+          if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
+          else t
+        case t: MethodType if variance > 0 && t.marksExistentialScope =>
+          val t1 = mapOver(t).asInstanceOf[MethodType]
+          t1.derivedLambdaType(resType = toResult(t1.resType, t1, fail))
+        case CapturingType(parent, refs) =>
+          t.derivedCapturingType(this(parent), refs)
+        case t: (LazyRef | TypeVar) =>
+          mapConserveSuper(t)
+        case _ =>
+          try
+            if keepAliases then mapOver(t)
+            else mapFollowingAliases(t)
+          catch case ex: AssertionError =>
+            println(i"error while mapping $t")
+            throw ex
+    m(tp) match
+      case tp1: ExprType if sym.is(Method, butNot = Accessor) =>
+        tp1.derivedExprType(toResult(tp1.resType, tp1, fail))
+      case tp1 => tp1
   end toResultInResults
 
-  /** If `refs` contains an occurrence of `cap` or `cap.rd`, the current context
-   *  with an added property PrintFresh. This addition causes all occurrences of
-   *  `Fresh` to be printed as `fresh` instead of `cap`, so that one avoids
-   *  confusion in error messages.
-   */
-  def printContext(refs: (Type | CaptureSet)*)(using Context): Context =
-    def hasCap = new TypeAccumulator[Boolean]:
-      def apply(x: Boolean, t: Type) =
-        x || t.dealiasKeepAnnots.match
-          case Fresh(_) => false
-          case t: TermRef => t.isCap || this(x, t.widen)
-          case CapturingType(t1, refs) => refs.containsCap || this(x, t1)
-          case x: ThisType => false
-          case _ => foldOver(x, t)
-
-    def containsCap(x: Type | CaptureSet): Boolean = x match
-      case tp: Type =>
-        hasCap(false, tp)
-      case refs: CaptureSet =>
-        refs.elems.exists(_.stripReadOnly.isCap)
-
-    if refs.exists(containsCap) then
-      ctx.withProperty(PrintFresh, Some(()))
-    else
-      ctx
-  end printContext
 end root
\ No newline at end of file
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 14f2491214e2..ed231c1e9ca9 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -1038,6 +1038,7 @@ class Definitions {
   @tu lazy val DeprecatedInheritanceAnnot: ClassSymbol = requiredClass("scala.deprecatedInheritance")
   @tu lazy val ImplicitAmbiguousAnnot: ClassSymbol = requiredClass("scala.annotation.implicitAmbiguous")
   @tu lazy val ImplicitNotFoundAnnot: ClassSymbol = requiredClass("scala.annotation.implicitNotFound")
+  @tu lazy val InferredDepFunAnnot: ClassSymbol = requiredClass("scala.caps.internal.inferredDepFun")
   @tu lazy val InlineParamAnnot: ClassSymbol = requiredClass("scala.annotation.internal.InlineParam")
   @tu lazy val IntoAnnot: ClassSymbol = requiredClass("scala.annotation.into")
   @tu lazy val IntoParamAnnot: ClassSymbol = requiredClass("scala.annotation.internal.$into")
@@ -1561,8 +1562,10 @@ class Definitions {
   @tu lazy val pureSimpleClasses =
     Set(StringClass, NothingClass, NullClass) ++ ScalaValueClasses()
 
+  @tu lazy val capabilityQualifierAnnots: Set[Symbol] =
+    Set(ReachCapabilityAnnot, ReadOnlyCapabilityAnnot, MaybeCapabilityAnnot)
   @tu lazy val capabilityWrapperAnnots: Set[Symbol] =
-    Set(ReachCapabilityAnnot, ReadOnlyCapabilityAnnot, MaybeCapabilityAnnot, RootCapabilityAnnot)
+    capabilityQualifierAnnots + RootCapabilityAnnot
 
   @tu lazy val AbstractFunctionType: Array[TypeRef] = mkArityArray("scala.runtime.AbstractFunction", MaxImplementedFunctionArity, 0).asInstanceOf[Array[TypeRef]]
   val AbstractFunctionClassPerRun: PerRun[Array[Symbol]] = new PerRun(AbstractFunctionType.map(_.symbol.asClass))
diff --git a/compiler/src/dotty/tools/dotc/core/NameKinds.scala b/compiler/src/dotty/tools/dotc/core/NameKinds.scala
index e9575c7d6c4a..ff41eeb81ca0 100644
--- a/compiler/src/dotty/tools/dotc/core/NameKinds.scala
+++ b/compiler/src/dotty/tools/dotc/core/NameKinds.scala
@@ -312,6 +312,7 @@ object NameKinds {
 
   /** Other unique names */
   val CanThrowEvidenceName: UniqueNameKind   = new UniqueNameKind("canThrow$")
+  val TryOwnerName: UniqueNameKind           = new UniqueNameKind("try$")
   val TempResultName: UniqueNameKind         = new UniqueNameKind("ev$")
   val DepParamName: UniqueNameKind           = new UniqueNameKind("(param)")
   val LazyImplicitName: UniqueNameKind       = new UniqueNameKind("$_lazy_implicit_$")
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 2cd66464da3c..a1cfe7addf60 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -868,10 +868,11 @@ object Types extends TypeUtils {
             pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, overridingRefinement)
           else
             val isRefinedMethod = rinfo.isInstanceOf[MethodOrPoly]
-            val joint = pdenot.meet(
-              new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),
-              pre,
-              safeIntersection = ctx.base.pendingMemberSearches.contains(name))
+            val joint = CCState.ignoringFreshLevels:
+                pdenot.meet(
+                  new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),
+                  pre,
+                  safeIntersection = ctx.base.pendingMemberSearches.contains(name))
             joint match
               case joint: SingleDenotation
               if isRefinedMethod
@@ -3721,7 +3722,8 @@ object Types extends TypeUtils {
   // is that most poly types are cyclic via poly params,
   // and therefore two different poly types would never be equal.
 
-  trait MethodicType extends TermType
+  trait MethodicType extends TermType:
+    def resType: Type
 
   /** A by-name parameter type of the form `=> T`, or the type of a method with no parameter list. */
   abstract case class ExprType(resType: Type)
@@ -4279,7 +4281,7 @@ object Types extends TypeUtils {
                       ps.get(elemName) match
                         case Some(elemRef) => assert(elemRef eq elem, i"bad $mt")
                         case _ =>
-                    case root.Result(binder) if binder ne mt =>
+                    case root.Result(binder: MethodType) if binder ne mt =>
                       assert(binder.paramNames.toList != mt.paramNames.toList, i"bad $mt")
                     case _ =>
               checkRefs(refs)
@@ -6148,6 +6150,12 @@ object Types extends TypeUtils {
   trait BiTypeMap extends TypeMap:
     thisMap =>
 
+    /** Hook to control behavior on capture set variables.
+     *  If true, install the map on capture set variables so that future elements are also mapped.
+     *  If false, just map the elements currently present in the capture set variable.
+     */
+    def mapFutureElements: Boolean = true
+
     /** The inverse of the type map */
     def inverse: BiTypeMap
 
diff --git a/compiler/src/dotty/tools/dotc/printing/Formatting.scala b/compiler/src/dotty/tools/dotc/printing/Formatting.scala
index 741b997d9926..10365c1a3d95 100644
--- a/compiler/src/dotty/tools/dotc/printing/Formatting.scala
+++ b/compiler/src/dotty/tools/dotc/printing/Formatting.scala
@@ -13,6 +13,17 @@ import Highlighting.*
 
 object Formatting {
 
+  /** Essentially, a function Context => T, which can be created with `delay` */
+  abstract class Delay[T]:
+    def apply(c: Context): T
+
+  /** Delay a Context => T computation so that it is generated from the embedded
+   *  context of a string formatter instead of the enclosing context. This is needed
+   *  to make disambiguation work for such embedded computatons.
+   */
+  def delay[T](fn: Context ?=> T): Delay[T] = new Delay[T]:
+    def apply(c: Context) = fn(using c)
+
   object ShownDef:
     /** Represents a value that has been "shown" and can be consumed by StringFormatter.
      *  Not just a string because it may be a Seq that StringFormatter will intersperse with the trailing separator.
@@ -76,6 +87,9 @@ object Formatting {
       given [X: Show]: Show[Seq[X]] with
         def show(x: Seq[X]) = CtxShow(x.map(toStr))
 
+      given [X: Show]: Show[Delay[X]] = new Show:
+        def show(x: Delay[X]) = CtxShow(c ?=> x(c))
+
       given Show[Seq[Nothing]] with
         def show(x: Seq[Nothing]) = CtxShow(x)
 
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index a5843b545117..ceab670ff862 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -15,6 +15,7 @@ import util.SourcePosition
 import scala.util.control.NonFatal
 import scala.annotation.switch
 import config.{Config, Feature}
+import ast.tpd
 import cc.*
 
 class PlainPrinter(_ctx: Context) extends Printer {
@@ -30,8 +31,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
   /** Print Fresh instances as <cap hiding ...> */
   protected def ccVerbose = ctx.settings.YccVerbose.value
 
-  /** Print Fresh instances as "fresh" */
-  protected def printFresh = ccVerbose || ctx.property(PrintFresh).isDefined
+  /** Elide redundant ^ and ^{cap.rd} when printing instances of Capability
+   *  classes. Gets set when singletons are printed as `(x: T)` to reduce verbosity.
+   */
+  private var elideCapabilityCaps = false
 
   private var openRecs: List[RecType] = Nil
 
@@ -182,14 +185,41 @@ class PlainPrinter(_ctx: Context) extends Printer {
   private def toTextRetainedElems[T <: Untyped](refs: List[Tree[T]]): Text =
     "{" ~ Text(refs.map(ref => toTextRetainedElem(ref)), ", ") ~ "}"
 
+  type GeneralCaptureSet = CaptureSet | List[tpd.Tree]
+
+  protected def isUniversalCaptureSet(refs: GeneralCaptureSet): Boolean = refs match
+    case refs: CaptureSet =>
+      // The set if universal if it consists only of caps.cap or
+      // only of an existential Fresh that is bound to the immediately enclosing method.
+      val isUniversal =
+        refs.elems.size == 1
+        && (refs.isUniversal
+            || !printDebug && !ccVerbose && !showUniqueIds && refs.elems.nth(0).match
+                  case root.Result(binder) =>
+                    CCState.openExistentialScopes match
+                      case b :: _ => binder eq b
+                      case _ => false
+                  case _ =>
+                    false
+        )
+      isUniversal
+      || !refs.elems.isEmpty && refs.elems.forall(_.isCapOrFresh) && !ccVerbose
+    case (ref: tpd.Tree) :: Nil => ref.symbol == defn.captureRoot
+    case _ => false
+
+  protected def toTextGeneralCaptureSet(refs: GeneralCaptureSet): Text = refs match
+    case refs: CaptureSet => toTextCaptureSet(refs)
+    case refs: List[tpd.Tree] => toTextRetainedElems(refs)
+
   /** Print capturing type, overridden in RefinedPrinter to account for
    *  capturing function types.
    */
-  protected def toTextCapturing(parent: Type, refsText: Text, boxText: Text): Text =
+  protected def toTextCapturing(parent: Type, refs: GeneralCaptureSet, boxText: Text): Text =
     changePrec(InfixPrec):
-      boxText ~ toTextLocal(parent) ~ "^" ~ (refsText provided refsText != rootSetText)
-
-  final protected def rootSetText = Str("{cap}") // TODO Use disambiguation
+      boxText
+      ~ toTextLocal(parent)
+      ~ "^"
+      ~ toTextGeneralCaptureSet(refs).provided(!isUniversalCaptureSet(refs))
 
   def toText(tp: Type): Text = controlled {
     homogenize(tp) match {
@@ -251,38 +281,15 @@ class PlainPrinter(_ctx: Context) extends Printer {
         }.close
       case tp @ CapturingType(parent, refs) =>
         val boxText: Text = Str("box ") provided tp.isBoxed //&& ctx.settings.YccDebug.value
-        if parent.derivesFrom(defn.Caps_Capability)
-              && refs.containsRootCapability && refs.isReadOnly && !printDebug
-        then
-          toText(parent)
-        else
-          // The set if universal if it consists only of caps.cap or
-          // only of an existential Fresh that is bound to the immediately enclosing method.
-          def isUniversal =
-            refs.elems.size == 1
-            && (refs.isUniversal
-                || !printDebug && !printFresh && !showUniqueIds && refs.elems.nth(0).match
-                      case root.Result(binder) =>
-                        CCState.openExistentialScopes match
-                          case b :: _ => binder eq b
-                          case _ => false
-                      case _ =>
-                        false
-            )
-          val refsText =
-            if isUniversal then
-              rootSetText
-            else if !refs.elems.isEmpty && refs.elems.forall(_.isCapOrFresh) && !printFresh then
-              rootSetText
-            else
-              toTextCaptureSet(refs)
-          toTextCapturing(parent, refsText, boxText)
+        if elideCapabilityCaps
+            && parent.derivesFrom(defn.Caps_Capability)
+            && refs.containsRootCapability
+            && refs.isReadOnly
+        then toText(parent)
+        else toTextCapturing(parent, refs, boxText)
       case tp @ RetainingType(parent, refs) =>
         if Feature.ccEnabledSomewhere then
-          val refsText = refs match
-            case ref :: Nil if ref.symbol == defn.captureRoot => rootSetText
-            case _ => toTextRetainedElems(refs)
-          toTextCapturing(parent, refsText, "") ~ Str("R").provided(printDebug)
+          toTextCapturing(parent, refs, "") ~ Str("R").provided(printDebug)
         else toText(parent)
       case tp: PreviousErrorType if ctx.settings.XprintTypes.value =>
         "<error>" // do not print previously reported error message because they may try to print this error type again recursively
@@ -365,7 +372,11 @@ class PlainPrinter(_ctx: Context) extends Printer {
   }.close
 
   def toTextSingleton(tp: SingletonType): Text =
-    "(" ~ toTextRef(tp) ~ " : " ~ toTextGlobal(tp.underlying) ~ ")"
+    val saved = elideCapabilityCaps
+    elideCapabilityCaps = !ccVerbose && !ctx.settings.explain.value
+      // don't elide capability capture sets under -Ycc-verbose or -explain
+    try "(" ~ toTextRef(tp) ~ " : " ~ toTextGlobal(tp.underlying) ~ ")"
+    finally elideCapabilityCaps = saved
 
   protected def paramsText(lam: LambdaType): Text = {
     def paramText(ref: ParamRef) =
@@ -461,12 +472,11 @@ class PlainPrinter(_ctx: Context) extends Printer {
         val vbleText: Text = CCState.openExistentialScopes.indexOf(binder) match
           case -1 =>
             "<cap of " ~ toText(binder) ~ ">"
-          case n => "outer_" * n ++ (if printFresh then "localcap" else "cap")
+          case n => "outer_" * n ++ (if ccVerbose then "localcap" else "cap")
         vbleText ~ hashStr(binder) ~ Str(idStr).provided(showUniqueIds)
       case tp @ root.Fresh(hidden) =>
         val idStr = if showUniqueIds then s"#${tp.rootAnnot.id}" else ""
-        if ccVerbose then s"<fresh$idStr hiding " ~ toTextCaptureSet(hidden) ~ ">"
-        else if printFresh then "fresh"
+        if ccVerbose then s"<fresh$idStr in ${tp.ccOwner} hiding " ~ toTextCaptureSet(hidden) ~ ">"
         else "cap"
       case tp => toText(tp)
 
diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index 3d987982cc20..ecc1250cbe7a 100644
--- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -156,20 +156,25 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       else simpleNameString(tsym)
     }
 
-  private def arrow(isGiven: Boolean, isPure: Boolean): String =
+  protected def arrow(isGiven: Boolean, isPure: Boolean): String =
     (if isGiven then "?" else "") + (if isPure then "->" else "=>")
 
-  private def toTextFunction(tp: AppliedType, refs: Text = Str("")): Text =
+  private def toTextFunction(tp: AppliedType, refs: GeneralCaptureSet | Null): Text =
     val AppliedType(tycon, args) = (tp: @unchecked)
     val tsym = tycon.typeSymbol
-    val isContextual = tsym.name.isContextFunction
-    val capturesRoot = refs == rootSetText
-    val isPure =
-      Feature.pureFunsEnabled && !tsym.name.isImpureFunction && !capturesRoot
-    toTextFunction(args.init, args.last, tp, refs.provided(!capturesRoot), isContextual, isPure)
-
-  private def toTextFunction(args: List[Type], res: Type, fn: MethodType | AppliedType, refs: Text,
-      isContextual: Boolean, isPure: Boolean): Text =
+    toTextFunction(args.init, args.last, tp, refs,
+      isContextual = tsym.name.isContextFunction,
+      isPure = Feature.pureFunsEnabled && !tsym.name.isImpureFunction)
+
+  protected def funMiddleText(isContextual: Boolean, isPure: Boolean, refs: GeneralCaptureSet | Null): Text =
+    val (printPure, refsText) =
+      if refs == null then (isPure, Str(""))
+      else if isUniversalCaptureSet(refs) then (false, Str(""))
+      else (isPure, toTextGeneralCaptureSet(refs))
+    arrow(isContextual, printPure) ~ refsText
+
+  private def toTextFunction(args: List[Type], res: Type, fn: MethodType | AppliedType,
+      refs: GeneralCaptureSet | Null, isContextual: Boolean, isPure: Boolean): Text =
     changePrec(GlobalPrec):
       val argStr: Text = args match
         case arg :: Nil if !defn.isDirectTupleNType(arg) && !isContextual =>
@@ -179,30 +184,29 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
           "("
           ~ argsText(args)
           ~ ")"
-      argStr ~ " " ~ arrow(isContextual, isPure) ~ refs ~ " "
+      argStr ~ " "
+      ~ funMiddleText(isContextual, isPure, refs) ~ " "
       ~ fn.match
           case fn: MethodType => CCState.inNewExistentialScope(fn)(argText(res))
           case _ => argText(res)
 
-  protected def toTextMethodAsFunction(info: Type, isPure: Boolean, refs: Text = Str("")): Text =
+  protected def toTextMethodAsFunction(info: Type, isPure: Boolean, refs: GeneralCaptureSet | Null): Text =
     def recur(tp: Type, enclInfo: MethodType | Null): Text = tp match
       case tp: MethodType =>
         val isContextual = tp.isImplicitMethod
-        val capturesRoot = refs == rootSetText
         if cc.isCaptureCheckingOrSetup
             && tp.allParamNamesSynthetic
             && !tp.looksResultDependent && !tp.looksParamDependent
-            && !showUniqueIds && !printDebug && !printFresh
-          then
+            && !showUniqueIds && !printDebug && !ccVerbose
+        then
           // cc.Setup converts all functions to dependent functions. Undo that when printing.
-          toTextFunction(tp.paramInfos, tp.resType, tp, refs.provided(!capturesRoot), isContextual, isPure && !capturesRoot)
+          toTextFunction(tp.paramInfos, tp.resType, tp, refs, isContextual, isPure)
         else
           changePrec(GlobalPrec):
             "("
             ~ paramsText(tp)
             ~ ") "
-            ~ arrow(isContextual, isPure && !capturesRoot)
-            ~ refs.provided(!capturesRoot)
+            ~ funMiddleText(isContextual, isPure, refs)
             ~ " "
             ~ recur(tp.resultType, tp)
       case tp: PolyType =>
@@ -274,7 +278,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
           case _ =>
             val tsym = tycon.typeSymbol
             if tycon.isRepeatedParam then toTextLocal(args.head) ~ "*"
-            else if defn.isFunctionSymbol(tsym) then toTextFunction(tp)
+            else if defn.isFunctionSymbol(tsym) then toTextFunction(tp, null)
             else if isInfixType(tp) then
               val l :: r :: Nil = args: @unchecked
               val opName = tyconName(tycon)
@@ -303,8 +307,8 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         toTextMethodAsFunction(tp.refinedInfo,
           isPure = Feature.pureFunsEnabled && !tp.typeSymbol.name.isImpureFunction,
           refs = tp.parent match
-            case CapturingType(_, cs) => toTextCaptureSet(cs)
-            case _ => "")
+            case CapturingType(_, cs) => cs
+            case _ => null)
       case tp: TypeRef =>
         if (tp.symbol.isAnonymousClass && !showUniqueIds)
           toText(tp.info)
@@ -320,7 +324,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       case tp: ClassInfo =>
         if tp.cls.derivesFrom(defn.PolyFunctionClass) then
           tp.member(nme.apply).info match
-            case info: PolyType => toTextMethodAsFunction(info, isPure = false)
+            case info: PolyType => toTextMethodAsFunction(info, isPure = false, refs = null)
             case _ => toTextParents(tp.parents) ~~ "{...}"
         else toTextParents(tp.parents) ~~ "{...}"
       case JavaArrayType(elemtp) =>
@@ -849,13 +853,13 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
     }
   }
 
-  override protected def toTextCapturing(tp: Type, refsText: Text, boxText: Text): Text = tp match
+  override protected def toTextCapturing(tp: Type, refs: GeneralCaptureSet, boxText: Text): Text = tp match
     case tp: AppliedType if defn.isFunctionSymbol(tp.typeSymbol) && !printDebug =>
-      boxText ~ toTextFunction(tp, refsText)
+      boxText ~ toTextFunction(tp, refs)
     case tp: RefinedType if defn.isFunctionType(tp) && !printDebug =>
-      boxText ~ toTextMethodAsFunction(tp.refinedInfo, isPure = !tp.typeSymbol.name.isImpureFunction, refsText)
+      boxText ~ toTextMethodAsFunction(tp.refinedInfo, isPure = !tp.typeSymbol.name.isImpureFunction, refs)
     case _ =>
-      super.toTextCapturing(tp, refsText, boxText)
+      super.toTextCapturing(tp, refs, boxText)
 
   override def toText[T <: Untyped](tree: Tree[T]): Text = controlled {
     import untpd.*
diff --git a/compiler/src/dotty/tools/dotc/printing/Texts.scala b/compiler/src/dotty/tools/dotc/printing/Texts.scala
index 475e2c6900d5..63f6c0aff895 100644
--- a/compiler/src/dotty/tools/dotc/printing/Texts.scala
+++ b/compiler/src/dotty/tools/dotc/printing/Texts.scala
@@ -137,7 +137,7 @@ object Texts {
       case _ => relems.foldLeft(-1)((acc, relem) => acc max relem.maxLine)
     }
 
-    def mkString(width: Int, withLineNumbers: Boolean): String = {
+    def mkString(width: Int = Int.MaxValue, withLineNumbers: Boolean = false): String = {
       val sb = new StringBuilder
       val numberWidth = if (withLineNumbers) (2 * maxLine.toString.length) + 2 else 0
       layout(width - numberWidth).print(sb, numberWidth)
diff --git a/compiler/src/dotty/tools/dotc/reporting/Message.scala b/compiler/src/dotty/tools/dotc/reporting/Message.scala
index 1ac5c6ecf407..d098df628a54 100644
--- a/compiler/src/dotty/tools/dotc/reporting/Message.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/Message.scala
@@ -8,6 +8,7 @@ import printing.{RefinedPrinter, MessageLimiter, ErrorMessageLimiter}
 import printing.Texts.Text
 import printing.Formatting.hl
 import config.SourceVersion
+import cc.{CaptureRef, CaptureSet, root, rootAnnot}
 
 import scala.language.unsafeNulls
 import scala.annotation.threadUnsafe
@@ -40,7 +41,18 @@ object Message:
       i"\n$what can be rewritten automatically under -rewrite $optionStr."
     else ""
 
-  private type Recorded = Symbol | ParamRef | SkolemType
+  enum Disambiguation:
+    case All
+    case AllExcept(strs: List[String])
+    case None
+
+    def recordOK(str: String): Boolean = this match
+      case All => true
+      case AllExcept(strs) => !strs.contains(str)
+      case None => false
+  end Disambiguation
+
+  private type Recorded = Symbol | ParamRef | SkolemType | CaptureRef
 
   private case class SeenKey(str: String, isType: Boolean)
 
@@ -48,7 +60,7 @@ object Message:
    *  adds superscripts for disambiguations, and can explain recorded symbols
    *  in ` where` clause
    */
-  private class Seen(disambiguate: Boolean):
+  private class Seen(disambiguate: Disambiguation):
 
     /** The set of lambdas that were opened at some point during printing. */
     private val openedLambdas = new collection.mutable.HashSet[LambdaType]
@@ -62,12 +74,14 @@ object Message:
     var nonSensical = false
 
     /** If false, stop all recordings */
-    private var recordOK = disambiguate
+    private var disambi = disambiguate
+
+    def isActive = disambi != Disambiguation.None
 
     /** Clear all entries and stop further entries to be added */
     def disable() =
       seen.clear()
-      recordOK = false
+      disambi = Disambiguation.None
 
     /** Record an entry `entry` with given String representation `str` and a
      *  type/term namespace identified by `isType`.
@@ -76,63 +90,65 @@ object Message:
      *  and following recordings get consecutive superscripts starting with 2.
      *  @return  The possibly superscripted version of `str`.
      */
-    def record(str: String, isType: Boolean, entry: Recorded)(using Context): String = if !recordOK then str else
-      //println(s"recording $str, $isType, $entry")
-
-      /** If `e1` is an alias of another class of the same name, return the other
-       *  class symbol instead. This normalization avoids recording e.g. scala.List
-       *  and scala.collection.immutable.List as two different types
-       */
-      def followAlias(e1: Recorded): Recorded = e1 match {
-        case e1: Symbol if e1.isAliasType =>
-          val underlying = e1.typeRef.underlyingClassRef(refinementOK = false).typeSymbol
-          if (underlying.name == e1.name) underlying else e1.namedType.dealias.typeSymbol
-        case _ => e1
-      }
-      val key = SeenKey(str, isType)
-      val existing = seen(key)
-      lazy val dealiased = followAlias(entry)
-
-      /** All lambda parameters with the same name are given the same superscript as
-       *  long as their corresponding binder has been printed.
-       *  See tests/neg/lambda-rename.scala for test cases.
-       */
-      def sameSuperscript(cur: Recorded, existing: Recorded) =
-        (cur eq existing) ||
-        (cur, existing).match
-          case (cur: ParamRef, existing: ParamRef) =>
-            (cur.paramName eq existing.paramName) &&
-            openedLambdas.contains(cur.binder) &&
-            openedLambdas.contains(existing.binder)
-          case _ =>
-            false
-
-      // The length of alts corresponds to the number of superscripts we need to print.
-      var alts = existing.dropWhile(alt => !sameSuperscript(dealiased, followAlias(alt)))
-      if alts.isEmpty then
-        alts = entry :: existing
-        seen(key) = alts
-
-      val suffix = alts.length match {
-        case 1 => ""
-        case n => n.toString.toCharArray.map {
-          case '0' => '⁰'
-          case '1' => '¹'
-          case '2' => '²'
-          case '3' => '³'
-          case '4' => '⁴'
-          case '5' => '⁵'
-          case '6' => '⁶'
-          case '7' => '⁷'
-          case '8' => '⁸'
-          case '9' => '⁹'
-        }.mkString
-      }
-      str + suffix
+    def record(str: String, isType: Boolean, entry: Recorded)(using Context): String =
+      if disambi.recordOK(str) then
+        //println(s"recording $str, $isType, $entry")
+
+        /** If `e1` is an alias of another class of the same name, return the other
+         *  class symbol instead. This normalization avoids recording e.g. scala.List
+         *  and scala.collection.immutable.List as two different types
+         */
+        def followAlias(e1: Recorded): Recorded = e1 match {
+          case e1: Symbol if e1.isAliasType =>
+            val underlying = e1.typeRef.underlyingClassRef(refinementOK = false).typeSymbol
+            if (underlying.name == e1.name) underlying else e1.namedType.dealias.typeSymbol
+          case _ => e1
+        }
+        val key = SeenKey(str, isType)
+        val existing = seen(key)
+        lazy val dealiased = followAlias(entry)
+
+        /** All lambda parameters with the same name are given the same superscript as
+         *  long as their corresponding binder has been printed.
+         *  See tests/neg/lambda-rename.scala for test cases.
+         */
+        def sameSuperscript(cur: Recorded, existing: Recorded) =
+          (cur eq existing) ||
+          (cur, existing).match
+            case (cur: ParamRef, existing: ParamRef) =>
+              (cur.paramName eq existing.paramName) &&
+              openedLambdas.contains(cur.binder) &&
+              openedLambdas.contains(existing.binder)
+            case _ =>
+              false
+
+        // The length of alts corresponds to the number of superscripts we need to print.
+        var alts = existing.dropWhile(alt => !sameSuperscript(dealiased, followAlias(alt)))
+        if alts.isEmpty then
+          alts = entry :: existing
+          seen(key) = alts
+
+        val suffix = alts.length match {
+          case 1 => ""
+          case n => n.toString.toCharArray.map {
+            case '0' => '⁰'
+            case '1' => '¹'
+            case '2' => '²'
+            case '3' => '³'
+            case '4' => '⁴'
+            case '5' => '⁵'
+            case '6' => '⁶'
+            case '7' => '⁷'
+            case '8' => '⁸'
+            case '9' => '⁹'
+          }.mkString
+        }
+        str + suffix
+      else str
     end record
 
     /** Create explanation for single `Recorded` type or symbol */
-    private def explanation(entry: AnyRef)(using Context): String =
+    private def explanation(entry: AnyRef, key: String)(using Context): String =
       def boundStr(bound: Type, default: ClassSymbol, cmp: String) =
         if (bound.isRef(default)) "" else i"$cmp $bound"
 
@@ -152,7 +168,7 @@ object Message:
           ""
       }
 
-      entry match {
+      entry match
         case param: TypeParamRef =>
           s"is a type variable${addendum("constraint", TypeComparer.bounds(param))}"
         case param: TermParamRef =>
@@ -166,7 +182,32 @@ 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: CaptureRef =>
+          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 =
+            if ref.isCap then "the universal root capability"
+            else ref match
+              case ref @ root.Fresh(hidden) =>
+                val (kind: root.Kind.Fresh) = ref.rootAnnot.kind: @unchecked
+                val descr = kind.origin match
+                  case origin @ root.Origin.InDecl(sym) if sym.exists =>
+                    origin.explanation
+                  case origin =>
+                    i" created in ${ownerStr(hidden.owner)}${origin.explanation}"
+                i"a fresh root capability$descr"
+              case root.Result(binder) => i"a root capability associated with the result type of $binder"
+          s"$relation $descr"
     end explanation
 
     /** Produce a where clause with explanations for recorded iterms.
@@ -177,6 +218,7 @@ object Message:
         case param: ParamRef     => false
         case skolem: SkolemType  => true
         case sym: Symbol         => ctx.gadt.contains(sym) && ctx.gadt.fullBounds(sym) != TypeBounds.empty
+        case ref: CaptureRef     => ref.isRootCapability
       }
 
       val toExplain: List[(String, Recorded)] = seen.toList.flatMap { kvs =>
@@ -201,7 +243,7 @@ object Message:
         }
       }
 
-      val explainParts = toExplain.map { case (str, entry) => (str, explanation(entry)) }
+      val explainParts = toExplain.map { case (str, entry) => (str, explanation(entry, str)) }
       val explainLines = columnar(explainParts)
       if (explainLines.isEmpty) "" else i"where:    $explainLines%\n          %\n"
     end explanations
@@ -225,7 +267,26 @@ object Message:
       case tp: SkolemType => seen.record(tp.repr.toString, isType = true, tp)
       case _ => super.toTextRef(tp)
 
-    override def toTextMethodAsFunction(info: Type, isPure: Boolean, refs: Text): Text =
+    override def toTextCaptureRef(tp: Type): Text = tp match
+      case tp: CaptureRef if tp.isRootCapability && !tp.isReadOnly && seen.isActive =>
+        seen.record("cap", isType = false, tp)
+      case _ => super.toTextCaptureRef(tp)
+
+    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))
+      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))
+        case _ =>
+          super.funMiddleText(isContextual, isPure, refs)
+
+    override def toTextMethodAsFunction(info: Type, isPure: Boolean, refs: GeneralCaptureSet): Text =
       info match
         case info: LambdaType =>
           seen.openLambda(info)
@@ -348,13 +409,15 @@ abstract class Message(val errorId: ErrorMessageID)(using Context) { self =>
    */
   def isNonSensical: Boolean = { message; myIsNonSensical }
 
-  private var disambiguate: Boolean = true
+  private var disambiguate: Disambiguation = Disambiguation.All
 
-  def withoutDisambiguation(): this.type =
-    disambiguate = false
+  def withDisambiguation(disambi: Disambiguation): this.type =
+    disambiguate = disambi
     this
 
-  private def inMessageContext(disambiguate: Boolean)(op: Context ?=> String): String =
+  def withoutDisambiguation(): this.type = withDisambiguation(Disambiguation.None)
+
+  private def inMessageContext(disambiguate: Disambiguation)(op: Context ?=> String): String =
     if ctx eq NoContext then op
     else
       val msgContext = ctx.printer match
@@ -373,7 +436,7 @@ abstract class Message(val errorId: ErrorMessageID)(using Context) { self =>
 
   /** The explanation to report. <nonsensical> tags are filtered out */
   @threadUnsafe lazy val explanation: String =
-    inMessageContext(disambiguate = false)(explain)
+    inMessageContext(disambiguate = Disambiguation.None)(explain)
 
   /** The implicit `Context` in messages is a large thing that we don't want
     * persisted. This method gets around that by duplicating the message,
diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala
index 0db766d4e337..aa2332f98c10 100644
--- a/compiler/src/dotty/tools/dotc/reporting/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala
@@ -23,7 +23,7 @@ import typer.Implicits.*
 import typer.Inferencing
 import scala.util.control.NonFatal
 import StdNames.nme
-import printing.Formatting.hl
+import Formatting.{hl, delay}
 import ast.Trees.*
 import ast.untpd
 import ast.tpd
@@ -37,6 +37,7 @@ import scala.jdk.CollectionConverters.*
 import dotty.tools.dotc.util.SourceFile
 import dotty.tools.dotc.config.SourceVersion
 import DidYouMean.*
+import Message.Disambiguation
 
 /**  Messages
   *  ========
@@ -1172,6 +1173,7 @@ class OverrideError(
     member: Symbol, other: Symbol,
     memberTp: Type, otherTp: Type)(using Context)
 extends DeclarationMsg(OverrideErrorID), NoDisambiguation:
+  withDisambiguation(Disambiguation.AllExcept(List(member.name.toString)))
   def msg(using Context) =
     val isConcreteOverAbstract =
       (other.owner isSubClass member.owner) && other.is(Deferred) && !member.is(Deferred)
@@ -1181,8 +1183,8 @@ extends DeclarationMsg(OverrideErrorID), NoDisambiguation:
             |(Note that ${err.infoStringWithLocation(other, base)} is abstract,
             |and is therefore overridden by concrete ${err.infoStringWithLocation(member, base)})"""
         else ""
-    i"""error overriding ${err.infoStringWithLocation(other, base)};
-        |  ${err.infoString(member, base, showLocation = member.owner != base.typeSymbol)} $core$addendum"""
+    i"""error overriding ${delay(err.infoStringWithLocation(other, base))};
+        |  ${delay(err.infoString(member, base, showLocation = member.owner != base.typeSymbol))} $core$addendum"""
   override def canExplain =
     memberTp.exists && otherTp.exists
   def explain(using Context) =
diff --git a/compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala b/compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala
index 20b0c8534920..16c50b9cd474 100644
--- a/compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala
+++ b/compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala
@@ -225,6 +225,7 @@ object OverridingPairs:
       )
     else
       member.name.is(DefaultGetterName) // default getters are not checked for compatibility
-      || memberTp.overrides(otherTp, member.matchNullaryLoosely || other.matchNullaryLoosely || fallBack)
+      ||
+      memberTp.overrides(otherTp, member.matchNullaryLoosely || other.matchNullaryLoosely || fallBack)
 
 end OverridingPairs
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index b891df666c6c..a37035cab9f0 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -304,7 +304,7 @@ abstract class Recheck extends Phase, SymTransformer:
     /** A hook to massage the type of an applied method */
     protected def prepareFunction(funtpe: MethodType, meth: Symbol)(using Context): MethodType = funtpe
 
-    protected def recheckArg(arg: Tree, formal: Type)(using Context): Type =
+    protected def recheckArg(arg: Tree, formal: Type, pref: ParamRef, app: Apply)(using Context): Type =
       recheck(arg, formal)
 
     /** A hook to check all the parts of an application:
@@ -336,7 +336,7 @@ abstract class Recheck extends Phase, SymTransformer:
             else fntpe.paramInfos
           def recheckArgs(args: List[Tree], formals: List[Type], prefs: List[ParamRef]): List[Type] = args match
             case arg :: args1 =>
-              val argType = recheckArg(arg, normalizeByName(formals.head))
+              val argType = recheckArg(arg, normalizeByName(formals.head), prefs.head, tree)
               val formals1 =
                 if fntpe.isParamDependent
                 then formals.tail.map(_.substParam(prefs.head, argType))
@@ -449,9 +449,11 @@ abstract class Recheck extends Phase, SymTransformer:
       defn.UnitType
 
     def recheckTry(tree: Try, pt: Type)(using Context): Type =
-      val bodyType = recheck(tree.expr, pt)
-      val casesTypes = tree.cases.map(recheckCase(_, defn.ThrowableType, pt))
-      val finalizerType = recheck(tree.finalizer, defn.UnitType)
+      recheckTryRest(recheck(tree.expr, pt), tree.cases, tree.finalizer, pt)
+
+    protected def recheckTryRest(bodyType: Type, cases: List[CaseDef], finalizer: Tree, pt: Type)(using Context): Type =
+      val casesTypes = cases.map(recheckCase(_, defn.ThrowableType, pt))
+      val finalizerType = recheck(finalizer, defn.UnitType)
       TypeComparer.lub(bodyType :: casesTypes)
 
     def seqLiteralElemProto(tree: SeqLiteral, pt: Type, declared: Type)(using Context): Type =
diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala
index 7f8b184c1c95..3016cb4ebe14 100644
--- a/library/src/scala/caps/package.scala
+++ b/library/src/scala/caps/package.scala
@@ -122,6 +122,14 @@ object internal:
    */
   final class rootCapability extends annotation.StaticAnnotation
 
+  /** An annotation used internally to mark a function type that was
+   *  converted to a dependent function type during setup of inferred types.
+   *  Such function types should not map roots to result variables.
+   */
+  final class inferredDepFun extends annotation.StaticAnnotation
+
+end internal
+
 @experimental
 object unsafe:
   /**
diff --git a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
index 45186e7c13b2..726b011c6929 100644
--- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
+++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
@@ -25,7 +25,7 @@ import scala.runtime.Statics
 import language.experimental.captureChecking
 import annotation.unchecked.uncheckedCaptures
 import caps.cap
-import caps.unsafe.{unsafeAssumeSeparate, untrackedCaptures}
+import caps.unsafe.{unsafeAssumeSeparate, unsafeAssumePure, untrackedCaptures}
 
 /**  This class implements an immutable linked list. We call it "lazy"
   *  because it computes its elements only when they are needed.
@@ -989,7 +989,12 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
 
   private sealed trait State[+A] extends Serializable {
     def head: A
-    def tail: LazyListIterable[A]^
+    def tail: LazyListIterable[A]/*^*/
+      // should be ^ but this fails checking. The problem is that
+      // the ^ in LazyListIterable[A]^ is treated as a result reference.
+      // But then it cannot be subsumed by
+      //   val tail: LazyListIterable[A]^
+      // in class State.Cons.
   }
 
   private object State {
@@ -1000,14 +1005,15 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
     }
 
     @SerialVersionUID(3L)
-    final class Cons[A](val head: A, val tail: LazyListIterable[A]^) extends State[A]
+    final class Cons[A](val head: A, val tail: LazyListIterable[A]/*^*/) extends State[A]
   }
 
   /** Creates a new LazyListIterable. */
   @inline private def newLL[A](state: => State[A]^): LazyListIterable[A]^{state} = new LazyListIterable[A](() => state)
 
   /** Creates a new State.Cons. */
-  @inline private def sCons[A](hd: A, tl: LazyListIterable[A]^): State[A]^{tl} = new State.Cons[A](hd, tl)
+  @inline private def sCons[A](hd: A, tl: LazyListIterable[A]^): State[A]^{tl} =
+    new State.Cons[A](hd, tl.unsafeAssumePure)
 
   private val anyToMarker: Any => Any = _ => Statics.pfMarker
 
diff --git a/tests/neg-custom-args/captures/boundschecks3.check b/tests/neg-custom-args/captures/boundschecks3.check
index 035d327e3d71..3121ee229cf6 100644
--- a/tests/neg-custom-args/captures/boundschecks3.check
+++ b/tests/neg-custom-args/captures/boundschecks3.check
@@ -3,22 +3,30 @@
   |           ^
   |    Type argument box test.Tree^ does not conform to upper bound test.Tree in inferred type test.C[box test.Tree^]
   |
+  |    where:    ^ refers to the universal root capability
+  |
   | longer explanation available when compiling with `-explain`
 -- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:10:11 --------------------------------
 10 |  type T = C[Tree^] // error
    |           ^
    |  Type argument box test.Tree^ does not conform to upper bound test.Tree in inferred type test.C[box test.Tree^]
    |
+   |  where:    ^ refers to the universal root capability
+   |
    | longer explanation available when compiling with `-explain`
 -- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:11:11 --------------------------------
 11 |  val bar: T -> T = ??? // error
    |           ^
    |Type argument box test.Tree^ does not conform to upper bound test.Tree in subpart test.C[box test.Tree^] of inferred type test.C[box test.Tree^] -> test.C[box test.Tree^]
    |
+   |where:    ^ refers to the universal root capability
+   |
    | longer explanation available when compiling with `-explain`
 -- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:12:11 --------------------------------
 12 |  val baz: C[Tree^] -> Unit = ??? // error
    |           ^
    |Type argument box test.Tree^ does not conform to upper bound test.Tree in subpart test.C[box test.Tree^] of inferred type test.C[box test.Tree^] -> Unit
    |
+   |where:    ^ refers to the universal root capability
+   |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/box-adapt-cases.check b/tests/neg-custom-args/captures/box-adapt-cases.check
index c89f7a09f293..a3902a96994d 100644
--- a/tests/neg-custom-args/captures/box-adapt-cases.check
+++ b/tests/neg-custom-args/captures/box-adapt-cases.check
@@ -2,7 +2,11 @@
 8 |  x.value(cap => cap.use())  // error, was OK
   |          ^^^^^^^^^^^^^^^^
   |          Found:    (cap: box Cap^?) => Int
-  |          Required: (cap: box Cap^) ->{fresh} Int
+  |          Required: (cap: box Cap^) =>² Int
+  |
+  |          where:    =>  refers to the universal root capability
+  |                    =>² refers to a fresh root capability created in method test1
+  |                    ^   refers to the universal root capability
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:15:10 ------------------------------
diff --git a/tests/neg-custom-args/captures/box-adapt-contra.check b/tests/neg-custom-args/captures/box-adapt-contra.check
index fd36f23aa999..b0bdc1d51ce1 100644
--- a/tests/neg-custom-args/captures/box-adapt-contra.check
+++ b/tests/neg-custom-args/captures/box-adapt-contra.check
@@ -8,6 +8,9 @@
    |                                         ^^^^^^^^^^^^^^^^^^^
    |        Cap^{c} => Unit cannot be box-converted to box Cap^{c} ->{cap, c} Unit
    |        since the additional capture set {c} resulting from box conversion is not allowed in box Cap^{c} => Unit
+   |
+   |        where:    =>  refers to the universal root capability
+   |                  cap is the universal root capability
 -- Error: tests/neg-custom-args/captures/box-adapt-contra.scala:19:54 --------------------------------------------------
 19 |  val f3: (Cap^{c} -> Unit) => Unit = useCap3[Cap^{c}](c)  // error
    |                                      ^^^^^^^^^^^^^^^^^^^
diff --git a/tests/neg-custom-args/captures/byname.check b/tests/neg-custom-args/captures/byname.check
index a6d04354bbbf..f3ce717db467 100644
--- a/tests/neg-custom-args/captures/byname.check
+++ b/tests/neg-custom-args/captures/byname.check
@@ -7,8 +7,10 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:10:6 ----------------------------------------
 10 |  h(f2())  // error
    |    ^^^^
-   |    Found:    () ?->{cap1} Int ->{cap1} Int
-   |    Required: () ?=> Int ->{cap2} Int
+   |Found:    () ?->{cap1} Int ->{cap1} Int
+   |Required: () ?=> Int ->{cap2} Int
+   |
+   |where:    ?=> refers to a fresh root capability created in method test when checking argument to parameter ff of method h
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:19:5 ----------------------------------------
diff --git a/tests/neg-custom-args/captures/capt-capability.scala b/tests/neg-custom-args/captures/capt-capability.scala
new file mode 100644
index 000000000000..7813ad8144b8
--- /dev/null
+++ b/tests/neg-custom-args/captures/capt-capability.scala
@@ -0,0 +1,9 @@
+import caps.{Capability, SharedCapability}
+
+def foo() =
+  val x: SharedCapability = ???
+
+  val z3 =
+    if x == null then (y: Unit) => x else (y: Unit) => new Capability() {} // error
+
+
diff --git a/tests/neg-custom-args/captures/capt-depfun.check b/tests/neg-custom-args/captures/capt-depfun.check
index d7ad819fb423..a5db4da7a319 100644
--- a/tests/neg-custom-args/captures/capt-depfun.check
+++ b/tests/neg-custom-args/captures/capt-depfun.check
@@ -4,6 +4,8 @@
    |                                         Found:    Str^{} ->{ac, y, z} Str^{y, z}
    |                                         Required: Str^{y, z} => Str^{y, z}
    |
+   |                                         where:    => refers to a fresh root capability in the type of value dc
+   |
    | 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
diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check
index e0eb8731b3de..b0a27b134b60 100644
--- a/tests/neg-custom-args/captures/capt1.check
+++ b/tests/neg-custom-args/captures/capt1.check
@@ -42,11 +42,15 @@
    |             ^^^^^^^^^
    |             Type variable X of method h cannot be instantiated to () -> box C^ since
    |             the part box C^ of that type captures the root capability `cap`.
+   |
+   |             where:    ^ refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:36:24 ----------------------------------------
 36 |  val z2 = h[() -> Cap](() => x) // error // error
    |                        ^^^^^^^
-   |                        Found:    () ->{x} box C^{x}
-   |                        Required: () -> box C^
+   |Found:    () ->{x} box C^{x}
+   |Required: () -> box C^
+   |
+   |where:    ^ refers to a fresh root capability created in value z2 when checking argument to parameter a of method h
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/capt1.scala:38:13 -------------------------------------------------------------
@@ -54,21 +58,32 @@
    |             ^^^^^^^^^^^^^^^^^^^^^^^
    |             Type variable X of method h cannot be instantiated to box () ->{x} C^ since
    |             the part C^ of that type captures the root capability `cap`.
+   |
+   |             where:    ^ refers to the universal root capability
 -- Error: tests/neg-custom-args/captures/capt1.scala:43:7 --------------------------------------------------------------
 43 |    if x == null then  // error: separation
    |       ^
    |       Separation failure: Illegal access to {x} which is hidden by the previous definition
    |       of value z1 with type () => C^.
    |       This type hides capabilities  {x}
+   |
+   |       where:    => refers to a fresh root capability in the type of value z1
+   |                 ^  refers to a fresh root capability in the type of value z1
 -- Error: tests/neg-custom-args/captures/capt1.scala:44:12 -------------------------------------------------------------
 44 |      () => x  // error: separation
    |            ^
    |            Separation failure: Illegal access to {x} which is hidden by the previous definition
    |            of value z1 with type () => C^.
    |            This type hides capabilities  {x}
+   |
+   |            where:    => refers to a fresh root capability in the type of value z1
+   |                      ^  refers to a fresh root capability in the type of value z1
 -- Error: tests/neg-custom-args/captures/capt1.scala:47:2 --------------------------------------------------------------
 47 |  x // error: separation
    |  ^
    |  Separation failure: Illegal access to {x} which is hidden by the previous definition
    |  of value z1 with type () => C^.
    |  This type hides capabilities  {x}
+   |
+   |  where:    => refers to a fresh root capability in the type of value z1
+   |            ^  refers to a fresh root capability in the type of value z1
diff --git a/tests/neg-custom-args/captures/cc-existential-conformance.check b/tests/neg-custom-args/captures/cc-existential-conformance.check
index 65367fad1df1..d3236ce642b0 100644
--- a/tests/neg-custom-args/captures/cc-existential-conformance.check
+++ b/tests/neg-custom-args/captures/cc-existential-conformance.check
@@ -2,29 +2,37 @@
 8 |  val y: A -> Fun[B^] = x // error
   |                        ^
   |                        Found:    (x : A -> (x²: A) -> B^)
-  |                        Required: A -> A -> B^
+  |                        Required: A -> A -> B^²
   |
-  |                        where:    x  is a value in method test
+  |                        where:    ^  refers to a root capability associated with the result type of (x²: A): B^
+  |                                  ^² refers to a fresh root capability in the type of value y
+  |                                  x  is a value in method test
   |                                  x² is a reference to a value parameter
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:9:29 --------------------
 9 |  val z: A -> (x: A) -> B^ = y // error
   |                             ^
-  |                             Found:    (y : A -> A -> B^)
-  |                             Required: A -> (x: A) -> B^
+  |                           Found:    (y : A -> A -> B^)
+  |                           Required: A -> (x: A) -> B^²
   |
-  |                             Note that the existential capture root in B^
-  |                             cannot subsume the capability cap
+  |                           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
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:13:19 -------------------
 13 |  val y: Fun[B^] = x // error
    |                   ^
    |                   Found:    (x : (x²: A) -> B^)
-   |                   Required: A -> B^
+   |                   Required: A -> B^²
    |
-   |                   where:    x  is a value in method test2
+   |                   where:    ^  refers to a root capability associated with the result type of (x²: A): B^
+   |                             ^² refers to a fresh root capability in the type of value y
+   |                             x  is a value in method test2
    |                             x² is a reference to a value parameter
    |
    | longer explanation available when compiling with `-explain`
@@ -32,7 +40,11 @@
 14 |  val z: (x: A) -> B^ = y // error
    |                        ^
    |                        Found:    (y : A -> B^)
-   |                        Required: (x: A) -> B^
+   |                        Required: (x: A) -> B^²
+   |
+   |                        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/cc-poly-2.check b/tests/neg-custom-args/captures/cc-poly-2.check
index 90568de385b3..28e0e1863760 100644
--- a/tests/neg-custom-args/captures/cc-poly-2.check
+++ b/tests/neg-custom-args/captures/cc-poly-2.check
@@ -4,6 +4,8 @@
    |                   Found:    (d : Test.D^)
    |                   Required: Test.D^{c1}
    |
+   |                   where:    ^ refers to a fresh root capability in the type of value d
+   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-poly-2.scala:16:20 ------------------------------------
 16 |    val _: D^{c1} = x // error
diff --git a/tests/neg-custom-args/captures/cc-this2.check b/tests/neg-custom-args/captures/cc-this2.check
index dc61fe2e0396..932e7c336ef0 100644
--- a/tests/neg-custom-args/captures/cc-this2.check
+++ b/tests/neg-custom-args/captures/cc-this2.check
@@ -9,4 +9,6 @@
   |      illegal inheritance: self type D^ of class D does not conform to self type C
   |      of parent class C
   |
+  |      where:    ^ refers to the universal root capability
+  |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/cc-this3.check b/tests/neg-custom-args/captures/cc-this3.check
index d57471c6872e..cdd91767ce22 100644
--- a/tests/neg-custom-args/captures/cc-this3.check
+++ b/tests/neg-custom-args/captures/cc-this3.check
@@ -4,6 +4,8 @@
   |      illegal inheritance: self type B^ of class B does not conform to self type A^{}
   |      of parent class A
   |
+  |      where:    ^ refers to the universal root capability
+  |
   | longer explanation available when compiling with `-explain`
 -- [E058] Type Mismatch Error: tests/neg-custom-args/captures/cc-this3.scala:11:6 --------------------------------------
 11 |class C(val f: () => Int) extends A // error
diff --git a/tests/neg-custom-args/captures/cc-this4.check b/tests/neg-custom-args/captures/cc-this4.check
index d650d905f9b5..d97c304a9cd3 100644
--- a/tests/neg-custom-args/captures/cc-this4.check
+++ b/tests/neg-custom-args/captures/cc-this4.check
@@ -4,4 +4,6 @@
   |             Found:    (C.this : C^)
   |             Required: C
   |
+  |             where:    ^ refers to the universal root capability
+  |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/class-level-attack.scala b/tests/neg-custom-args/captures/class-level-attack.scala
new file mode 100644
index 000000000000..19d681198e8c
--- /dev/null
+++ b/tests/neg-custom-args/captures/class-level-attack.scala
@@ -0,0 +1,25 @@
+import language.experimental.captureChecking
+import caps.*
+
+class IO
+
+class Ref[X](init: X):
+  var x = init
+  def get: X = x
+  def put(y: X): Unit = x = y
+
+class C(io: IO^):
+  val r: Ref[IO^] = Ref[IO^](io) // error:
+    //Type variable X of constructor Ref cannot be instantiated to box IO^ since
+    //that type captures the root capability `cap`.
+    // where: ^ refers to the universal root capability
+  val r2: Ref[IO^] = Ref(io) // error:
+    //Error: Ref[IO^{io}] does not conform to Ref[IO^] (since Refs are invariant)
+  def set(x: IO^) = r.put(x)
+
+def outer(outerio: IO^) =
+  val c = C(outerio)
+  def test(innerio: IO^) =
+    c.set(innerio)
+
+
diff --git a/tests/neg-custom-args/captures/contracap.check b/tests/neg-custom-args/captures/contracap.check
index 31b58acb80d5..e2a3e0958674 100644
--- a/tests/neg-custom-args/captures/contracap.check
+++ b/tests/neg-custom-args/captures/contracap.check
@@ -4,4 +4,6 @@
    |                                                Found:    (f : (Ref[Int]^, Ref[Int]^) -> Unit)
    |                                                Required: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit
    |
+   |                                                where:    ^ refers to the universal root capability
+   |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/depfun-reach.check b/tests/neg-custom-args/captures/depfun-reach.check
index c4b74c5123c6..9f47722078aa 100644
--- a/tests/neg-custom-args/captures/depfun-reach.check
+++ b/tests/neg-custom-args/captures/depfun-reach.check
@@ -1,22 +1,30 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:12:27 ---------------------------------
 12 |    List(() => op.foreach((f,g) => { f(); g() })) // error (???)
    |                           ^^^^^^^^^^^^^^^^^^^^
-   |                           Found:    (x$1: (box () ->? Unit, box () ->? Unit)^?) ->? Unit
-   |                           Required: (x$1: (box () ->{op*} Unit, box () ->{op*} Unit)) => Unit
+   |Found:    (x$1: (box () ->? Unit, box () ->? Unit)^?) ->? Unit
+   |Required: (x$1: (box () ->{op*} Unit, box () ->{op*} Unit)) => Unit
+   |
+   |where:    => refers to a fresh root capability created in anonymous function of type (): Unit when checking argument to parameter op of method foreach
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:19:4 ----------------------------------
 19 |    op // error
    |    ^^
    |    Found:    (op : (xs: List[(X, box () ->{io} Unit)]) => List[box () ->{xs*} Unit])
-   |    Required: (xs: List[(X, box () ->{io} Unit)]) => List[() -> Unit]
+   |    Required: (xs: List[(X, box () ->{io} Unit)]) =>² List[() -> Unit]
+   |
+   |    where:    =>  refers to a fresh root capability in the type of parameter op
+   |              =>² refers to a fresh root capability in the result type of method foo
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:26:60 ---------------------------------
 26 |  val b: (xs: List[() ->{io} Unit]) => List[() ->{} Unit] = a // error
    |                                                            ^
    |                                     Found:    (a : (xs: List[box () ->{io} Unit]) => List[box () ->{xs*} Unit])
-   |                                     Required: (xs: List[box () ->{io} Unit]) => List[() -> Unit]
+   |                                     Required: (xs: List[box () ->{io} Unit]) =>² List[() -> Unit]
+   |
+   |                                     where:    =>  refers to a fresh root capability in the type of value a
+   |                                               =>² refers to a fresh root capability in the type of value b
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/depfun-reach.scala:18:17 ------------------------------------------------------
diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.check b/tests/neg-custom-args/captures/effect-swaps-explicit.check
index 9fc99f1a10d2..c7cbb351318a 100644
--- a/tests/neg-custom-args/captures/effect-swaps-explicit.check
+++ b/tests/neg-custom-args/captures/effect-swaps-explicit.check
@@ -19,7 +19,11 @@
    |          ^
    |Found:    (contextual$9: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^) ?->{fr, async}
    |  box Future[box T^?]^{fr, contextual$9}
-   |Required: (contextual$9: boundary.Label[Result[box Future[box T^?]^?, box E^?]]^) ?->{fresh} box Future[box T^?]^?
+   |Required: (contextual$9: boundary.Label[Result[box Future[box T^?]^?, box E^?]]^) ?=> box Future[box T^?]^?
+   |
+   |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 ?
@@ -30,7 +34,10 @@
 73 |        Result.make[Future[T], E]: lbl ?=> // error: type mismatch
    |                                   ^
    |Found:    (lbl: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^) ?->{fr, async} Future[box T^?]^{fr, lbl}
-   |Required: (lbl: boundary.Label[Result[Future[T], E]]^) ?->{fresh} Future[T]
+   |Required: (lbl: boundary.Label[Result[Future[T], E]]^) ?=> Future[T]
+   |
+   |where:    ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make
+   |          ^   refers to the universal root capability
 74 |          Future: fut ?=>
 75 |            fr.await.ok
    |
diff --git a/tests/neg-custom-args/captures/effect-swaps.check b/tests/neg-custom-args/captures/effect-swaps.check
index dc832fca0ee9..d30aa0ca3f21 100644
--- a/tests/neg-custom-args/captures/effect-swaps.check
+++ b/tests/neg-custom-args/captures/effect-swaps.check
@@ -17,9 +17,13 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:69:10 ---------------------------------
 69 |          Future: fut ?=> // error, type mismatch
    |          ^
-   |Found:    (contextual$9: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]) ?->{fr, async}
+   |Found:    (contextual$9: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^{cap.rd}) ?->{fr, async}
    |  box Future[box T^?]^{fr, contextual$9}
-   |Required: (contextual$9: boundary.Label[Result[box Future[box T^?]^?, box E^?]]) ?->{fresh} box Future[box T^?]^?
+   |Required: (contextual$9: boundary.Label[Result[box Future[box T^?]^?, box E^?]]^{cap.rd}) ?=> box Future[box T^?]^?
+   |
+   |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 ?
@@ -29,8 +33,11 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:73:35 ---------------------------------
 73 |        Result.make[Future[T], E]: lbl ?=> // error: type mismatch
    |                                   ^
-   |Found:    (lbl: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]) ?->{fr, async} Future[box T^?]^{fr, lbl}
-   |Required: (lbl: boundary.Label[Result[Future[T], E]]) ?->{fresh} Future[T]
+   |Found:    (lbl: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^{cap.rd}) ?->{fr, async} Future[box T^?]^{fr, lbl}
+   |Required: (lbl: boundary.Label[Result[Future[T], E]]^{cap.rd}) ?=> Future[T]
+   |
+   |where:    ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make
+   |          cap is the universal root capability
 74 |          Future: fut ?=>
 75 |            fr.await.ok
    |
diff --git a/tests/neg-custom-args/captures/erased-methods2.check b/tests/neg-custom-args/captures/erased-methods2.check
index 876ff36b3696..80d2db450c40 100644
--- a/tests/neg-custom-args/captures/erased-methods2.check
+++ b/tests/neg-custom-args/captures/erased-methods2.check
@@ -1,11 +1,16 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/erased-methods2.scala:20:4 -------------------------------
 20 |  = (x$1: CT[Ex3]^)  // error
    |    ^
-   |    Found:    (erased x$1: CT[Ex3]^) ?->? (erased x$2: CT[Ex2]^?) ?->{x$1} Unit
-   |    Required: (erased x$1: CT[Ex3]^) ?->{fresh} (erased x$2: CT[Ex2]^) ?->{localcap} Unit
+   |Found:    (erased x$1: CT[Ex3]^) ?->? (erased x$2: CT[Ex2]^?) ?->{x$1} Unit
+   |Required: (erased x$1: CT[Ex3]^) ?=> (erased x$2: CT[Ex2]^) ?=>² Unit
    |
-   |    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
+   |where:    ?=>  refers to a fresh root capability in the result type of method foo9a
+   |          ?=>² 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]^)
 22 |     ?=>
 23 |      //given (CT[Ex3]^) = x$1
@@ -16,9 +21,15 @@
 31 |  = (erased x$1: CT[Ex3]^) // error
    |    ^
    |Found:    (erased x$1: CT[Ex3]^) ?->? (erased x$1: CT[Ex2]^?) ?->{x$1} (erased x$2: CT[Ex1]^?) ?->{x$1} Unit
-   |Required: (erased x$1: CT[Ex3]^) ?->{fresh} (erased x$1: CT[Ex2]^) ?->{localcap} (erased x$2: CT[Ex1]^) ?->{localcap} Unit
+   |Required: (erased x$1: CT[Ex3]^) ?=> (erased x$1: CT[Ex2]^) ?=>² (erased x$2: CT[Ex1]^) ?=>³ Unit
+   |
+   |where:    ?=>  refers to a fresh root capability in the result type of method foo10a
+   |          ?=>² refers to a root capability associated with the result type of (using erased x$1: CT[Ex3]^): (erased x$1: CT[Ex2]^) ?=>² (erased x$2: CT[Ex1]^) ?=>³ Unit
+   |          ?=>³ 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]^) ?->{localcap} Unit
+   |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]^)
 33 |     ?=> (erased x$3: CT[Ex1]^)
diff --git a/tests/neg-custom-args/captures/existential-mapping.check b/tests/neg-custom-args/captures/existential-mapping.check
index 974c5c38f74c..54f2b1f6a1a0 100644
--- a/tests/neg-custom-args/captures/existential-mapping.check
+++ b/tests/neg-custom-args/captures/existential-mapping.check
@@ -3,87 +3,145 @@
    |          ^^^^^^^^^^^^^^^^^^^^
    |          Array[box C^] captures the root capability `cap` in invariant position.
    |          This capability cannot be converted to an existential in the result type of a function.
+   |
+   |          where:    ^ refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:9:25 ---------------------------
 9 |  val _:  (x: C^) -> C = x1 // error
   |                         ^^
-  |                         Found:    (x1 : (x: C^) -> C^{localcap})
+  |                         Found:    (x1 : (x: C^) -> C^²)
   |                         Required: (x: C^) -> C
   |
+  |                         where:    ^  refers to the universal root capability
+  |                                   ^² refers to a root capability associated with the result type of (x: C^): C^²
+  |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:12:20 --------------------------
 12 |  val _:  C^ -> C = x2 // error
    |                    ^^
-   |                    Found:    (x2 : C^ -> C^{fresh})
+   |                    Found:    (x2 : C^ -> C^²)
    |                    Required: C^ -> C
    |
+   |                    where:    ^  refers to the universal root capability
+   |                              ^² refers to a fresh root capability in the type of value x2
+   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:15:30 --------------------------
 15 |  val _: A^ -> (x: C^) -> C = x3 // error
    |                              ^^
-   |                              Found:    (x3 : A^ -> (x: C^) -> C^{localcap})
-   |                              Required: A^ -> (x: C^) -> C
+   |                        Found:    (x3 : A^ -> (x: C^) -> C^²)
+   |                        Required: A^ -> (x: C^) -> C
+   |
+   |                        where:    ^  refers to the universal root capability
+   |                                  ^² refers to a root capability associated with the result type of (x: C^): C^²
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:18:25 --------------------------
 18 |  val _: A^ -> C^ -> C = x4 // error
    |                         ^^
-   |                         Found:    (x4 : A^ -> C^ -> C^{fresh})
+   |                         Found:    (x4 : A^ -> C^ -> C^²)
    |                         Required: A^ -> C^ -> C
    |
+   |                         where:    ^  refers to the universal root capability
+   |                                   ^² refers to a fresh root capability in the type of value x4
+   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:21:30 --------------------------
 21 |  val _: A^ -> (x: C^) -> C = x5 // error
    |                              ^^
-   |                              Found:    (x5 : A^ -> (x: C^) -> C^{localcap})
-   |                              Required: A^ -> (x: C^) -> C
+   |                        Found:    (x5 : A^ -> (x: C^) -> C^²)
+   |                        Required: A^ -> (x: C^) -> C
+   |
+   |                        where:    ^  refers to the universal root capability
+   |                                  ^² refers to a root capability associated with the result type of (x: C^): C^²
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:24:30 --------------------------
 24 |  val _: A^ -> (x: C^) => C = x6 // error
    |                              ^^
-   |                              Found:    (x6 : A^ -> (x: C^) ->{fresh} C^{localcap})
-   |                              Required: A^ -> (x: C^) ->{fresh} C
+   |                       Found:    (x6 : A^ -> (x: C^) => C^²)
+   |                       Required: A^ -> (x: C^) =>² C
+   |
+   |                       where:    =>  refers to a fresh root capability in the type of value x6
+   |                                 =>² refers to a fresh root capability in the type of value _$6
+   |                                 ^   refers to the universal root capability
+   |                                 ^²  refers to a root capability associated with the result type of (x: C^): C^²
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:27:25 --------------------------
 27 |  val _:  (x: C^) => C = y1 // error
    |                         ^^
-   |                         Found:    (y1 : (x: C^) ->{fresh} C^{localcap})
-   |                         Required: (x: C^) ->{fresh} C
+   |                       Found:    (y1 : (x: C^) => C^²)
+   |                       Required: (x: C^) =>² C
+   |
+   |                       where:    =>  refers to a fresh root capability in the type of value y1
+   |                                 =>² refers to a fresh root capability in the type of value _$7
+   |                                 ^   refers to the universal root capability
+   |                                 ^²  refers to a root capability associated with the result type of (x: C^): C^²
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:30:20 --------------------------
 30 |  val _:  C^ => C = y2 // error
    |                    ^^
-   |                    Found:    (y2 : C^ ->{fresh} C^{fresh})
-   |                    Required: C^ ->{fresh} C
+   |                    Found:    (y2 : C^ => C^²)
+   |                    Required: C^ =>² C
+   |
+   |                    where:    =>  refers to a fresh root capability in the type of value y2
+   |                              =>² refers to a fresh root capability in the type of value _$8
+   |                              ^   refers to the universal root capability
+   |                              ^²  refers to a fresh root capability in the type of value y2
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:33:30 --------------------------
 33 |  val _: A^ => (x: C^) => C = y3 // error
    |                              ^^
-   |                              Found:    (y3 : A^ ->{fresh} (x: C^) ->{fresh} C^{localcap})
-   |                              Required: A^ ->{fresh} (x: C^) ->{fresh} C
+   |                       Found:    (y3 : A^ => (x: C^) =>² C^²)
+   |                       Required: A^ =>³ (x: C^) =>⁴ C
+   |
+   |                       where:    =>  refers to a fresh root capability in the type of value y3
+   |                                 =>² refers to a fresh root capability in the type of value y3
+   |                                 =>³ refers to a fresh root capability in the type of value _$9
+   |                                 =>⁴ refers to a fresh root capability in the type of value _$9
+   |                                 ^   refers to the universal root capability
+   |                                 ^²  refers to a root capability associated with the result type of (x: C^): C^²
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:36:25 --------------------------
 36 |  val _: A^ => C^ => C = y4 // error
    |                         ^^
-   |                         Found:    (y4 : A^ ->{fresh} C^ ->{fresh} C^{fresh})
-   |                         Required: A^ ->{fresh} C^ ->{fresh} C
+   |                         Found:    (y4 : A^ => C^ =>² C^²)
+   |                         Required: A^ =>³ C^ =>⁴ C
+   |
+   |                         where:    =>  refers to a fresh root capability in the type of value y4
+   |                                   =>² refers to a fresh root capability in the type of value y4
+   |                                   =>³ refers to a fresh root capability in the type of value _$10
+   |                                   =>⁴ refers to a fresh root capability in the type of value _$10
+   |                                   ^   refers to the universal root capability
+   |                                   ^²  refers to a fresh root capability in the type of value y4
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:39:30 --------------------------
 39 |  val _: A^ => (x: C^) -> C = y5 // error
    |                              ^^
-   |                              Found:    (y5 : A^ ->{fresh} (x: C^) -> C^{localcap})
-   |                              Required: A^ ->{fresh} (x: C^) -> C
+   |                       Found:    (y5 : A^ => (x: C^) -> C^²)
+   |                       Required: A^ =>² (x: C^) -> C
+   |
+   |                       where:    =>  refers to a fresh root capability in the type of value y5
+   |                                 =>² refers to a fresh root capability in the type of value _$11
+   |                                 ^   refers to the universal root capability
+   |                                 ^²  refers to a root capability associated with the result type of (x: C^): C^²
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:42:30 --------------------------
 42 |  val _: A^ => (x: C^) => C = y6 // error
    |                              ^^
-   |                              Found:    (y6 : A^ ->{fresh} (x: C^) ->{fresh} C^{localcap})
-   |                              Required: A^ ->{fresh} (x: C^) ->{fresh} C
+   |                       Found:    (y6 : A^ => (x: C^) =>² C^²)
+   |                       Required: A^ =>³ (x: C^) =>⁴ C
+   |
+   |                       where:    =>  refers to a fresh root capability in the type of value y6
+   |                                 =>² refers to a fresh root capability in the type of value y6
+   |                                 =>³ refers to a fresh root capability in the type of value _$12
+   |                                 =>⁴ refers to a fresh root capability in the type of value _$12
+   |                                 ^   refers to the universal root capability
+   |                                 ^²  refers to a root capability associated with the result type of (x: C^): C^²
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/extending-cap-classes.check b/tests/neg-custom-args/captures/extending-cap-classes.check
index 4a77a638a4d8..fb77546dd8e5 100644
--- a/tests/neg-custom-args/captures/extending-cap-classes.check
+++ b/tests/neg-custom-args/captures/extending-cap-classes.check
@@ -1,15 +1,19 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:7:15 -------------------------
 7 |  val x2: C1 = new C2 // error
   |               ^^^^^^
-  |               Found:    C2
-  |               Required: C1
+  |             Found:    C2^{cap.rd}
+  |             Required: C1
+  |
+  |             where:    cap is a fresh root capability created in value x2 when constructing Capability instance C2
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:8:15 -------------------------
 8 |  val x3: C1 = new C3 // error
   |               ^^^^^^
-  |               Found:    C3
-  |               Required: C1
+  |             Found:    C3^{cap.rd}
+  |             Required: C1
+  |
+  |             where:    cap is a fresh root capability created in value x3 when constructing Capability instance C3
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:13:15 ------------------------
diff --git a/tests/neg-custom-args/captures/filevar-expanded.check b/tests/neg-custom-args/captures/filevar-expanded.check
index f48736984a36..516d03b5ed7c 100644
--- a/tests/neg-custom-args/captures/filevar-expanded.check
+++ b/tests/neg-custom-args/captures/filevar-expanded.check
@@ -1,14 +1,17 @@
 -- Error: tests/neg-custom-args/captures/filevar-expanded.scala:34:13 --------------------------------------------------
 34 |    withFile(io3): f => // error: separation failure
    |             ^^^
-   |   Separation failure: argument of type  (io3 : test2.IO^)
-   |   to method withFile: [T](io2: test2.IO^)(op: (f: test2.File^{io2}) => T): T
-   |   corresponds to capture-polymorphic formal parameter io2 of type  test2.IO^
-   |   and hides capabilities  {io3}.
-   |   Some of these overlap with the captures of the second argument with type  (f: test2.File^{io3}) ->{io3} Unit.
+   |Separation failure: argument of type  (io3 : test2.IO^)
+   |to method withFile: [T](io2: test2.IO^)(op: (f: test2.File^{io2}) => T): T
+   |corresponds to capture-polymorphic formal parameter io2 of type  test2.IO^²
+   |and hides capabilities  {io3}.
+   |Some of these overlap with the captures of the second argument with type  (f: test2.File^{io3}) ->{io3} Unit.
    |
-   |     Hidden set of current argument        : {io3}
-   |     Hidden footprint of current argument  : {io3}
-   |     Capture set of second argument        : {io3}
-   |     Footprint set of second argument      : {io3}
-   |     The two sets overlap at               : {io3}
+   |  Hidden set of current argument        : {io3}
+   |  Hidden footprint of current argument  : {io3}
+   |  Capture set of second argument        : {io3}
+   |  Footprint set of second argument      : {io3}
+   |  The two sets overlap at               : {io3}
+   |
+   |where:    ^  refers to a fresh root capability in the type of parameter io3
+   |          ^² refers to a fresh root capability created in method test when checking argument to parameter io2 of method withFile
diff --git a/tests/neg-custom-args/captures/filevar.check b/tests/neg-custom-args/captures/filevar.check
index 22efd36053b4..d0b85408b43a 100644
--- a/tests/neg-custom-args/captures/filevar.check
+++ b/tests/neg-custom-args/captures/filevar.check
@@ -1,8 +1,20 @@
--- Error: tests/neg-custom-args/captures/filevar.scala:8:6 -------------------------------------------------------------
-8 |  var file: File^ = uninitialized  // error, was OK under unsealed
-  |      ^
-  |      Mutable variable file cannot have type File^ since
-  |      that type captures the root capability `cap`.
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/filevar.scala:15:12 --------------------------------------
+15 |  withFile: f =>       // error with level checking, was OK under both schemes before
+   |            ^
+   |Found:    (l: scala.caps.Capability^{cap.rd}) ?->? File^? ->? Unit
+   |Required: (l: scala.caps.Capability^{cap.rd}) ?-> (f: File^{l}) => Unit
+   |
+   |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()
+17 |    o.file = f
+18 |    o.log
+   |
+   | longer explanation available when compiling with `-explain`
 -- Warning: tests/neg-custom-args/captures/filevar.scala:11:55 ---------------------------------------------------------
 11 |def withFile[T](op: (l: caps.Capability) ?-> (f: File^{l}) => T): T =
    |                                                       ^
diff --git a/tests/neg-custom-args/captures/filevar.scala b/tests/neg-custom-args/captures/filevar.scala
index 5b83f1d29380..047c41c6af05 100644
--- a/tests/neg-custom-args/captures/filevar.scala
+++ b/tests/neg-custom-args/captures/filevar.scala
@@ -5,14 +5,14 @@ class File:
   def write(x: String): Unit = ???
 
 class Service:
-  var file: File^ = uninitialized  // error, was OK under unsealed
+  var file: File^ = uninitialized  //OK, was  error under sealed
   def log = file.write("log") // OK, was error under unsealed
 
 def withFile[T](op: (l: caps.Capability) ?-> (f: File^{l}) => T): T =
   op(using caps.cap)(new File)
 
 def test =
-  withFile: f =>
+  withFile: f =>       // error with level checking, was OK under both schemes before
     val o = Service()
     o.file = f
     o.log
diff --git a/tests/neg-custom-args/captures/heal-tparam-cs.check b/tests/neg-custom-args/captures/heal-tparam-cs.check
index 4cd30d74f4dc..10b56d5d6304 100644
--- a/tests/neg-custom-args/captures/heal-tparam-cs.check
+++ b/tests/neg-custom-args/captures/heal-tparam-cs.check
@@ -1,11 +1,15 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:10:23 -------------------------------
 10 |  val test1 = localCap { c => // error
    |                       ^
-   |                       Found:    (c: Capp^) ->? box () ->{c} Unit
-   |                       Required: (c: Capp^) ->{fresh} box () ->? Unit
+   |Found:    (c: Capp^) ->? box () ->{c} Unit
+   |Required: (c: Capp^) => box () ->? Unit
    |
-   |                       Note that reference c.type
-   |                       cannot be included in outer capture set ?
+   |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() }
 12 |  }
    |
@@ -14,7 +18,11 @@
 15 |    localCap { c =>  // error
    |    ^
    |    Found:    (x$0: Capp^) ->? () ->{x$0} Unit
-   |    Required: (c: Capp^) -> () ->{localcap} Unit
+   |    Required: (c: Capp^) -> () => Unit
+   |
+   |    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
@@ -37,6 +45,8 @@
    |    Found:    (io: Capp^) ->? () ->{io} Unit
    |    Required: (io: Capp^) -> () -> Unit
    |
+   |    where:    ^ refers to the universal root capability
+   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:44:4 --------------------------------
 44 |    io => () => io.use()  // error
@@ -44,4 +54,6 @@
    |    Found:    (io: Capp^) ->? () ->{io} Unit
    |    Required: (io: Capp^) -> () -> Unit
    |
+   |    where:    ^ refers to the universal root capability
+   |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i15116.check b/tests/neg-custom-args/captures/i15116.check
index 0a16af9f6704..50784d393162 100644
--- a/tests/neg-custom-args/captures/i15116.check
+++ b/tests/neg-custom-args/captures/i15116.check
@@ -1,11 +1,12 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:3:13 ----------------------------------------
 3 |  val x = Foo(m)   // error
   |          ^^^^^^
-  |          Found:    Foo{val m²: (Bar.this.m : String^)}^{Bar.this.m}
+  |          Found:    Foo{val m: (Bar.this.m² : String^)}^{Bar.this.m²}
   |          Required: Foo
   |
-  |          where:    m  is a value in class Bar
-  |                    m² is a value in class Foo
+  |          where:    ^  refers to a fresh root capability in the type of value m²
+  |                    m  is a value in class Foo
+  |                    m² is a value in class Bar
   |
   |
   |          Note that the expected type Foo
@@ -18,11 +19,12 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:5:13 ----------------------------------------
 5 |  val x = Foo(m)   // error
   |          ^^^^^^
-  |          Found:    Foo{val m²: (Baz.this.m : String^)}^{Baz.this.m}
+  |          Found:    Foo{val m: (Baz.this.m² : String^)}^{Baz.this.m²}
   |          Required: Foo
   |
-  |          where:    m  is a value in trait Baz
-  |                    m² is a value in class Foo
+  |          where:    ^  refers to a fresh root capability in the type of value m²
+  |                    m  is a value in class Foo
+  |                    m² is a value in trait Baz
   |
   |
   |          Note that the expected type Foo
@@ -35,11 +37,12 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:7:13 ----------------------------------------
 7 |  val x = Foo(m)   // error
   |          ^^^^^^
-  |          Found:    Foo{val m²: (Bar1.this.m : String^)}^{Bar1.this.m}
+  |          Found:    Foo{val m: (Bar1.this.m² : String^)}^{Bar1.this.m²}
   |          Required: Foo
   |
-  |          where:    m  is a value in class Bar1
-  |                    m² is a value in class Foo
+  |          where:    ^  refers to a fresh root capability in the type of value m²
+  |                    m  is a value in class Foo
+  |                    m² is a value in class Bar1
   |
   |
   |          Note that the expected type Foo
@@ -52,11 +55,12 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:9:13 ----------------------------------------
 9 |  val x = Foo(m)   // error
   |          ^^^^^^
-  |          Found:    Foo{val m²: (Baz2.this.m : String^)}^{Baz2.this.m}
+  |          Found:    Foo{val m: (Baz2.this.m² : String^)}^{Baz2.this.m²}
   |          Required: Foo
   |
-  |          where:    m  is a value in trait Baz2
-  |                    m² is a value in class Foo
+  |          where:    ^  refers to a fresh root capability in the type of value m²
+  |                    m  is a value in class Foo
+  |                    m² is a value in trait Baz2
   |
   |
   |          Note that the expected type Foo
diff --git a/tests/neg-custom-args/captures/i15772.check b/tests/neg-custom-args/captures/i15772.check
index 98791d729c16..574040685ad4 100644
--- a/tests/neg-custom-args/captures/i15772.check
+++ b/tests/neg-custom-args/captures/i15772.check
@@ -1,23 +1,31 @@
 -- Error: tests/neg-custom-args/captures/i15772.scala:22:46 ------------------------------------------------------------
 22 |    val boxed1 : ((C^) => Unit) -> Unit = box1(c)  // error
    |                                          ^^^^^^^
-   |C^ => Unit cannot be box-converted to box C{val arg: C^}^{c} ->{cap, c} Unit
-   |since the additional capture set {c} resulting from box conversion is not allowed in box C{val arg: C^}^{c} => Unit
+   |C^ => Unit cannot be box-converted to box C{val arg: C^²}^{c} ->{cap, c} Unit
+   |since the additional capture set {c} resulting from box conversion is not allowed in box C{val arg: C^²}^{c} => Unit
+   |
+   |where:    =>  refers to the universal root capability
+   |          ^   refers to the universal root capability
+   |          ^²  refers to a fresh root capability in the type of value arg
+   |          cap is the universal root capability
 -- Error: tests/neg-custom-args/captures/i15772.scala:29:35 ------------------------------------------------------------
 29 |    val boxed2 : Observe[C^] = box2(c)  // error
    |                               ^^^^^^^
-   |C^ => Unit cannot be box-converted to box C{val arg: C^}^{c} ->{cap, c} Unit
-   |since the additional capture set {c} resulting from box conversion is not allowed in box C{val arg: C^}^{c} => Unit
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:35:34 ---------------------------------------
-35 |  val boxed2 : Observe[C]^ = box2(c) // error
-   |                                  ^
-   |                                  Found:    box C^
-   |                                  Required: box C{val arg: C^?}^?
+   |C^ => Unit cannot be box-converted to box C{val arg: C^²}^{c} ->{cap, c} Unit
+   |since the additional capture set {c} resulting from box conversion is not allowed in box C{val arg: C^²}^{c} => Unit
    |
-   |                                  Note that the universal capability `cap`
-   |                                  cannot be included in capture set ?
+   |where:    =>  refers to the universal root capability
+   |          ^   refers to the universal root capability
+   |          ^²  refers to a fresh root capability in the type of value arg
+   |          cap is the universal root capability
+-- Error: tests/neg-custom-args/captures/i15772.scala:35:33 ------------------------------------------------------------
+35 |  val boxed2 : Observe[C]^ = box2(c) // error
+   |                             ^^^^^^^
+   |                             reference cap is not included in the allowed capture set ?
+   |                             of the enclosing method main3
    |
-   | longer explanation available when compiling with `-explain`
+   |                             Note that the universal capability cap
+   |                             cannot be included in capture set ?
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:46:2 ----------------------------------------
 46 |  x: (() -> Unit) // error
    |  ^
diff --git a/tests/neg-custom-args/captures/i16114.check b/tests/neg-custom-args/captures/i16114.check
index e7ae191dbf14..b83631660b9d 100644
--- a/tests/neg-custom-args/captures/i16114.check
+++ b/tests/neg-custom-args/captures/i16114.check
@@ -3,23 +3,33 @@
    |             ^^^^
    |             Type variable T of method expect cannot be instantiated to box Cap^ since
    |             that type captures the root capability `cap`.
+   |
+   |             where:    ^ refers to the universal root capability
 -- Error: tests/neg-custom-args/captures/i16114.scala:24:13 ------------------------------------------------------------
 24 |      expect[Cap^] { // error
    |             ^^^^
    |             Type variable T of method expect cannot be instantiated to box Cap^ since
    |             that type captures the root capability `cap`.
+   |
+   |             where:    ^ refers to the universal root capability
 -- Error: tests/neg-custom-args/captures/i16114.scala:30:13 ------------------------------------------------------------
 30 |      expect[Cap^] {  // error
    |             ^^^^
    |             Type variable T of method expect cannot be instantiated to box Cap^ since
    |             that type captures the root capability `cap`.
+   |
+   |             where:    ^ refers to the universal root capability
 -- Error: tests/neg-custom-args/captures/i16114.scala:36:13 ------------------------------------------------------------
 36 |      expect[Cap^](io) // error
    |             ^^^^
    |             Type variable T of method expect cannot be instantiated to box Cap^ since
    |             that type captures the root capability `cap`.
+   |
+   |             where:    ^ refers to the universal root capability
 -- Error: tests/neg-custom-args/captures/i16114.scala:39:13 ------------------------------------------------------------
 39 |      expect[Cap^] { // error
    |             ^^^^
    |             Type variable T of method expect cannot be instantiated to box Cap^ since
    |             that type captures the root capability `cap`.
+   |
+   |             where:    ^ refers to the universal root capability
diff --git a/tests/neg-custom-args/captures/i16226.check b/tests/neg-custom-args/captures/i16226.check
index 5a3c3b690f6d..f3b8666c0eb7 100644
--- a/tests/neg-custom-args/captures/i16226.check
+++ b/tests/neg-custom-args/captures/i16226.check
@@ -1,19 +1,28 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:13:4 ----------------------------------------
 13 |    (ref1, f1) => map[A, B](ref1, f1) // error
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |    Found:    (ref1: LazyRef[box A^?]{val elem: () ->{cap, fresh} A^?}^{io}, f1: (x$0: A^?) => B^?) ->?
-   |      LazyRef[box B^?]{val elem: () ->{localcap} B^?}^{f1, ref1}
-   |    Required: (ref1: LazyRef[A]^{io}, f1: A => B) ->{fresh} LazyRef[B]^{fresh}
+   |Found:    (ref1: LazyRef[box A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?) ->? LazyRef[box B^?]{val elem: () =>² B^?}^{f1, ref1}
+   |Required: (ref1: LazyRef[A]^{io}, f1: A => B) =>³ LazyRef[B]^
+   |
+   |where:    =>  refers to the universal root capability
+   |          =>² refers to a root capability associated with the result type of (ref1: LazyRef[box A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?): LazyRef[box B^?]{val elem: () =>² B^?}^{f1, ref1}
+   |          =>³ refers to a fresh root capability in the result type of method mapc
+   |          ^   refers to a fresh root capability in the result type of method mapc
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:15:4 ----------------------------------------
 15 |    (ref1, f1) => map[A, B](ref1, f1) // error
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |    Found:    (ref1: LazyRef[box A^?]{val elem: () ->{cap, fresh} A^?}^{io}, f1: (x$0: A^?) => B^?) ->?
-   |      LazyRef[box B^?]{val elem: () ->{localcap} B^?}^{f1, ref1}
-   |    Required: (ref: LazyRef[A]^{io}, f: A => B) ->{fresh} LazyRef[B]^{localcap}
+   |Found:    (ref1: LazyRef[box A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?) ->? LazyRef[box B^?]{val elem: () =>² B^?}^{f1, ref1}
+   |Required: (ref: LazyRef[A]^{io}, f: A => B) =>³ LazyRef[B]^
+   |
+   |where:    =>  refers to the universal root capability
+   |          =>² refers to a root capability associated with the result type of (ref1: LazyRef[box A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?): LazyRef[box B^?]{val elem: () =>² B^?}^{f1, ref1}
+   |          =>³ 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
+   |Note that the existential capture root in LazyRef[B]^
+   |cannot subsume the capability f1.type since that capability is not a SharedCapability
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i19330.check b/tests/neg-custom-args/captures/i19330.check
index 91ba7f234845..5a7dc525af4d 100644
--- a/tests/neg-custom-args/captures/i19330.check
+++ b/tests/neg-custom-args/captures/i19330.check
@@ -14,7 +14,10 @@
 22 |  val bad: bar.T = foo(bar) // error
    |                   ^^^^^^^^
    |                   Found:    bar.T
-   |                   Required: () ->{fresh} Logger^{fresh}
+   |                   Required: () => Logger^
+   |
+   |                   where:    => refers to a fresh root capability in the type of value bad
+   |                             ^  refers to a fresh root capability in the type of value bad
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/i19330.scala:16:14 ------------------------------------------------------------
diff --git a/tests/neg-custom-args/captures/i21313.check b/tests/neg-custom-args/captures/i21313.check
index f087c1f86d63..2a90a1f7aa47 100644
--- a/tests/neg-custom-args/captures/i21313.check
+++ b/tests/neg-custom-args/captures/i21313.check
@@ -5,7 +5,9 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21313.scala:15:12 ---------------------------------------
 15 |  ac1.await(src2) // error
    |            ^^^^
-   |            Found:    (src2 : Source[Int, scala.caps.CapSet^{ac2}]^{})
-   |            Required: Source[Int, scala.caps.CapSet^{ac1}]^
+   |Found:    (src2 : Source[Int, scala.caps.CapSet^{ac2}]^{})
+   |Required: Source[Int, scala.caps.CapSet^{ac1}]^
+   |
+   |where:    ^ refers to a fresh root capability created in method test when checking argument to parameter src of method await
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i21401.check b/tests/neg-custom-args/captures/i21401.check
index 8eade64e372f..2f0443e90ed9 100644
--- a/tests/neg-custom-args/captures/i21401.check
+++ b/tests/neg-custom-args/captures/i21401.check
@@ -3,16 +3,24 @@
    |              ^^^
    |              Type variable T of object Boxed cannot be instantiated to box IO^ since
    |              that type captures the root capability `cap`.
+   |
+   |              where:    ^ refers to the universal root capability
 -- Error: tests/neg-custom-args/captures/i21401.scala:15:18 ------------------------------------------------------------
 15 |  val a = usingIO[IO^](x => x) // error // error
    |                  ^^^
    |                  Type variable R of method usingIO cannot be instantiated to box IO^ since
    |                  that type captures the root capability `cap`.
+   |
+   |                  where:    ^ refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:15:23 ---------------------------------------
 15 |  val a = usingIO[IO^](x => x) // error // error
    |                       ^^^^^^
-   |                       Found:    (x: IO^) ->? box IO^{x}
-   |                       Required: (x: IO^) ->{fresh} box IO^{fresh}
+   |Found:    (x: IO^) ->? box IO^{x}
+   |Required: (x: IO^) => box IO^²
+   |
+   |where:    => refers to a fresh root capability created in value a when checking argument to parameter op of method usingIO
+   |          ^  refers to the universal root capability
+   |          ^² refers to a fresh root capability created in value a when checking argument to parameter op of method usingIO
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------
@@ -20,13 +28,29 @@
    |                                                                  ^^^
    | Type variable R of method usingIO cannot be instantiated to [R, X <: Boxed[box IO^] -> R] => (op: X) -> R since
    | the part box IO^ of that type captures the root capability `cap`.
+   |
+   | where:    ^ refers to the universal root capability
 -- Error: tests/neg-custom-args/captures/i21401.scala:17:29 ------------------------------------------------------------
-17 |  val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
+17 |  val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error
    |                             ^^^^^^^^^^
    |                             Type variable R of value leaked cannot be instantiated to Boxed[box IO^] since
    |                             the part box IO^ of that type captures the root capability `cap`.
+   |
+   |                             where:    ^ refers to the universal root capability
 -- Error: tests/neg-custom-args/captures/i21401.scala:17:52 ------------------------------------------------------------
-17 |  val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
+17 |  val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error
    |                                         ^^^^^^^^^^^^^^^^^^^^^^^^
    |                Type variable X of value leaked cannot be instantiated to Boxed[box IO^] -> Boxed[box IO^] since
    |                the part box IO^ of that type captures the root capability `cap`.
+   |
+   |                where:    ^ refers to the universal root capability
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:17:67 ---------------------------------------
+17 |  val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error
+   |                                                                   ^^^^^^
+   |                                              Found:    (x: Boxed[box IO^]^?) ->? Boxed[box IO^{x*}]^?
+   |                                              Required: (x: Boxed[box IO^]) -> Boxed[box IO^²]
+   |
+   |                                              where:    ^  refers to the universal root capability
+   |                                                        ^² refers to a fresh root capability created in value x²
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i21401.scala b/tests/neg-custom-args/captures/i21401.scala
index bd10a97952a2..af82fb88002d 100644
--- a/tests/neg-custom-args/captures/i21401.scala
+++ b/tests/neg-custom-args/captures/i21401.scala
@@ -14,6 +14,6 @@ def mkRes(x: IO^): Res =
 def test2() =
   val a = usingIO[IO^](x => x) // error // error
   val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error
-  val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
+  val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error
   val y: IO^{x*} = x.unbox // was error
   y.println("boom")
diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check
index e8d4c9f03102..a24677f0f9d1 100644
--- a/tests/neg-custom-args/captures/i21614.check
+++ b/tests/neg-custom-args/captures/i21614.check
@@ -1,17 +1,23 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:33 ---------------------------------------
 12 |  files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?
    |                                 ^
-   |                                 Found:    (f : F)
-   |                                 Required: File^
+   |Found:    (f : F)
+   |Required: File^
+   |
+   |where:    ^ refers to a fresh root capability created in anonymous function of type (f²: F): Logger when checking argument to parameter f of constructor Logger
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
 15 |  files.map(new Logger(_)) // error, Q: can we improve the error message?
    |            ^^^^^^^^^^^^^
-   |            Found:    (_$1: box File^{files*}) ->{files*} box Logger{val f: File^{_$1}}^{cap.rd, _$1}
-   |            Required: (_$1: box File^{files*}) => box Logger{val f: File^?}^?
+   |Found:    (_$1: box File^{files*}) ->{files*} box Logger{val f: File^{_$1}}^{cap.rd, _$1}
+   |Required: (_$1: box File^{files*}) => box Logger{val f: File^?}^?
+   |
+   |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 ?
+   |Note that reference <cap of (_$1: box File^{files*}): box Logger{val f: File^?}^?>.rd
+   |cannot be included in outer capture set ?
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i21920.check b/tests/neg-custom-args/captures/i21920.check
index 70efe6990d4c..301564d23b79 100644
--- a/tests/neg-custom-args/captures/i21920.check
+++ b/tests/neg-custom-args/captures/i21920.check
@@ -1,10 +1,14 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21920.scala:34:35 ---------------------------------------
 34 |  val cell: Cell[File] = File.open(f => Cell(() => Seq(f))) // error
    |                                   ^^^^^^^^^^^^^^^^^^^^^^^
-   |              Found:    (f: File^?) ->? box Cell[box File^?]{val head: () ->? IterableOnce[box File^?]^?}^?
-   |              Required: (f: File^) ->{fresh} box Cell[box File^?]{val head: () ->? IterableOnce[box File^?]^?}^?
+   |Found:    (f: File^?) ->? box Cell[box File^?]{val head: () ->? IterableOnce[box File^?]^?}^?
+   |Required: (f: File^) => box Cell[box File^?]{val head: () ->? IterableOnce[box File^?]^?}^?
    |
-   |              Note that the universal capability `cap`
-   |              cannot be included in capture set ?
+   |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 ?
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/lazyListState.check b/tests/neg-custom-args/captures/lazyListState.check
new file mode 100644
index 000000000000..bb84f3d7f006
--- /dev/null
+++ b/tests/neg-custom-args/captures/lazyListState.check
@@ -0,0 +1,10 @@
+-- [E164] Declaration Error: tests/neg-custom-args/captures/lazyListState.scala:12:39 ----------------------------------
+12 |  final class Cons[A](val head: A, val tail: LazyListIterable[A]^) extends State[A] // error
+   |                                       ^
+   |                 error overriding method tail in trait State of type -> LazyListIterable[A]^{cap};
+   |                   value tail of type LazyListIterable[A]^ has incompatible type
+   |
+   |                 where:    ^   refers to a fresh root capability in the type of value tail
+   |                           cap is a root capability associated with the result type of -> LazyListIterable[A²]^²
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/lazyListState.scala b/tests/neg-custom-args/captures/lazyListState.scala
new file mode 100644
index 000000000000..43e8ba19bb2f
--- /dev/null
+++ b/tests/neg-custom-args/captures/lazyListState.scala
@@ -0,0 +1,13 @@
+class LazyListIterable[+A]
+
+private sealed trait State[+A]:
+  def head: A
+  def tail: LazyListIterable[A]^
+
+private object State:
+  object Empty extends State[Nothing]:
+    def head: Nothing = throw new NoSuchElementException("head of empty lazy list")
+    def tail: LazyListIterable[Nothing] = throw new UnsupportedOperationException("tail of empty lazy list")
+
+  final class Cons[A](val head: A, val tail: LazyListIterable[A]^) extends State[A] // error
+
diff --git a/tests/neg-custom-args/captures/lazylist.check b/tests/neg-custom-args/captures/lazylist.check
index acdbfaaca3e0..455d72e9fd37 100644
--- a/tests/neg-custom-args/captures/lazylist.check
+++ b/tests/neg-custom-args/captures/lazylist.check
@@ -37,6 +37,8 @@
 22 |  def tail: LazyList[Nothing]^ = ???  // error overriding
    |      ^
    |      error overriding method tail in class LazyList of type -> lazylists.LazyList[Nothing];
-   |        method tail of type -> lazylists.LazyList[Nothing]^ has incompatible type
+   |        method tail of type -> lazylists.LazyList[Nothing]^{cap} has incompatible type
+   |
+   |      where:    cap is a root capability associated with the result type of -> lazylists.LazyList[Nothing]^
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/lazylists-exceptions.check b/tests/neg-custom-args/captures/lazylists-exceptions.check
index bdd053910ac8..a16c852750a3 100644
--- a/tests/neg-custom-args/captures/lazylists-exceptions.check
+++ b/tests/neg-custom-args/captures/lazylists-exceptions.check
@@ -4,6 +4,8 @@
    |  The result of `try` cannot have type LazyList[Int]^{cap.rd} since
    |  that type captures the root capability `cap`.
    |  This is often caused by a locally generated exception capability leaking as part of its result.
+   |
+   |  where:    cap is a fresh root capability in the type of given instance canThrow$1
 37 |    tabulate(10) { i =>
 38 |      if i > 9 then throw Ex1()
 39 |      i * i
diff --git a/tests/neg-custom-args/captures/lazyref.check b/tests/neg-custom-args/captures/lazyref.check
index 8db8791d1123..9c2f1a2d1a50 100644
--- a/tests/neg-custom-args/captures/lazyref.check
+++ b/tests/neg-custom-args/captures/lazyref.check
@@ -32,39 +32,53 @@
   |              Separation failure: Illegal access to {LazyRef.this.elem} which is hidden by the previous definition
   |              of value get with type () => T.
   |              This type hides capabilities  {LazyRef.this.elem}
+  |
+  |              where:    => refers to a fresh root capability in the type of value get
 -- Error: tests/neg-custom-args/captures/lazyref.scala:23:13 -----------------------------------------------------------
 23 |  val ref3 = ref1.map(g) // error: separation failure
    |             ^^^^
    |             Separation failure: Illegal access to {cap1} which is hidden by the previous definition
    |             of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
    |             This type hides capabilities  {cap1}
+   |
+   |             where:    => refers to a fresh root capability in the type of value elem
 -- Error: tests/neg-custom-args/captures/lazyref.scala:26:9 ------------------------------------------------------------
 26 |      if cap1 == cap2   // error: separation failure // error: separation failure
    |         ^^^^
    |         Separation failure: Illegal access to {cap1} which is hidden by the previous definition
    |         of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
    |         This type hides capabilities  {ref2*, cap1}
+   |
+   |         where:    => refers to a fresh root capability in the type of value elem
 -- Error: tests/neg-custom-args/captures/lazyref.scala:26:17 -----------------------------------------------------------
 26 |      if cap1 == cap2   // error: separation failure // error: separation failure
    |                 ^^^^
    |                 Separation failure: Illegal access to {cap2} which is hidden by the previous definition
    |                 of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
    |                 This type hides capabilities  {ref2*, cap1}
+   |
+   |                 where:    => refers to a fresh root capability in the type of value elem
 -- Error: tests/neg-custom-args/captures/lazyref.scala:27:11 -----------------------------------------------------------
 27 |      then ref1 // error: separation failure
    |           ^^^^
    |           Separation failure: Illegal access to {cap1, ref1} which is hidden by the previous definition
    |           of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
    |           This type hides capabilities  {ref2*, cap1}
+   |
+   |           where:    => refers to a fresh root capability in the type of value elem
 -- Error: tests/neg-custom-args/captures/lazyref.scala:28:11 -----------------------------------------------------------
 28 |      else ref2) // error: separation failure
    |           ^^^^
    |           Separation failure: Illegal access to {cap1, cap2, ref1} which is hidden by the previous definition
    |           of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
    |           This type hides capabilities  {ref2*, cap1}
+   |
+   |           where:    => refers to a fresh root capability in the type of value elem
 -- Error: tests/neg-custom-args/captures/lazyref.scala:29:9 ------------------------------------------------------------
 29 |    .map(g) // error: separation failure
    |         ^
    |         Separation failure: Illegal access to {cap2} which is hidden by the previous definition
    |         of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
    |         This type hides capabilities  {ref2*, cap1}
+   |
+   |         where:    => refers to a fresh root capability in the type of value elem
diff --git a/tests/neg-custom-args/captures/leaking-iterators.check b/tests/neg-custom-args/captures/leaking-iterators.check
index 54a8d6ccea9e..f2731166e53d 100644
--- a/tests/neg-custom-args/captures/leaking-iterators.check
+++ b/tests/neg-custom-args/captures/leaking-iterators.check
@@ -1,11 +1,15 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaking-iterators.scala:56:16 ----------------------------
 56 |  usingLogFile: log => // error
    |                ^
-   |                Found:    (log: java.io.FileOutputStream^) ->? box cctest.Iterator[Int]^{log}
-   |                Required: (log: java.io.FileOutputStream^) ->{fresh} box cctest.Iterator[Int]^?
+   |Found:    (log: java.io.FileOutputStream^) ->? box cctest.Iterator[Int]^{log}
+   |Required: (log: java.io.FileOutputStream^) => box cctest.Iterator[Int]^?
    |
-   |                Note that reference log.type
-   |                cannot be included in outer capture set ?
+   |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 =>
 58 |      log.write(x)
 59 |      x * x
diff --git a/tests/neg-custom-args/captures/levels.check b/tests/neg-custom-args/captures/levels.check
index 7ef29c36efc3..dd195c9085aa 100644
--- a/tests/neg-custom-args/captures/levels.check
+++ b/tests/neg-custom-args/captures/levels.check
@@ -3,6 +3,8 @@
    |              ^^^^^^^^^^^^^^^^
    |              Type variable T of constructor Ref cannot be instantiated to box String => String since
    |              that type captures the root capability `cap`.
+   |
+   |              where:    => refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/levels.scala:22:11 ---------------------------------------
 22 |    r.setV(g) // error
    |           ^
diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check
index 3d64c432d116..0d9f6b500770 100644
--- a/tests/neg-custom-args/captures/linear-buffer-2.check
+++ b/tests/neg-custom-args/captures/linear-buffer-2.check
@@ -4,26 +4,36 @@
    |             Separation failure: Illegal access to {buf} which is hidden by the previous definition
    |             of value buf1 with type Buffer[Int]^.
    |             This type hides capabilities  {buf}
+   |
+   |             where:    ^ refers to a fresh root capability in the type of value buf1
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 ---------------------------------------------------
 20 |  val buf3 = buf1.append(4) // error
    |             ^^^^
    |             Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
    |             @consume parameter or was used as a prefix to a @consume method on line 18
    |             and therefore is no longer available.
+   |
+   |             where:    ^ refers to a fresh root capability in the type of value buf1
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 ---------------------------------------------------
 28 |  val buf3 = buf1.append(4) // error
    |             ^^^^
    |             Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
    |             @consume parameter or was used as a prefix to a @consume method on line 25
    |             and therefore is no longer available.
+   |
+   |             where:    ^ refers to a fresh root capability in the type of value buf1
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 ---------------------------------------------------
 38 |  val buf3 = buf1.append(4) // error
    |             ^^^^
    |             Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
    |             @consume parameter or was used as a prefix to a @consume method on line 33
    |             and therefore is no longer available.
+   |
+   |             where:    ^ refers to a fresh root capability in the type of value buf1
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ----------------------------------------------------
 42 |    buf.append(1)  // error
    |    ^^^
    |    Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot
    |    be passed to a @consume parameter or be used as a prefix of a @consume method call.
+   |
+   |    where:    ^ refers to a fresh root capability in the type of parameter buf
diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check
index 55af88406356..86e6aaaa81a3 100644
--- a/tests/neg-custom-args/captures/linear-buffer.check
+++ b/tests/neg-custom-args/captures/linear-buffer.check
@@ -8,37 +8,42 @@
   |             ^^^^^^^^^^^^^
   |         Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
   |         The access must be in a @consume method to allow this.
--- Error: tests/neg-custom-args/captures/linear-buffer.scala:6:9 -------------------------------------------------------
-6 |  def foo = // error
-  |         ^
-  |Separation failure: method foo's inferred result type BadBuffer[box T^{}]^ hides non-local this of class class BadBuffer.
-  |The access must be in a @consume method to allow this.
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:19:17 -----------------------------------------------------
 19 |  val buf3 = app(buf, 3) // error
    |                 ^^^
    |                 Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a
    |                 @consume parameter or was used as a prefix to a @consume method on line 17
    |                 and therefore is no longer available.
+   |
+   |                 where:    ^ refers to a fresh root capability in the type of parameter buf
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:26:17 -----------------------------------------------------
 26 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
    |                 Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
    |                 @consume parameter or was used as a prefix to a @consume method on line 24
    |                 and therefore is no longer available.
+   |
+   |                 where:    ^ refers to a fresh root capability in the type of value buf1
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:34:17 -----------------------------------------------------
 34 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
    |                 Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
    |                 @consume parameter or was used as a prefix to a @consume method on line 31
    |                 and therefore is no longer available.
+   |
+   |                 where:    ^ refers to a fresh root capability in the type of value buf1
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:44:17 -----------------------------------------------------
 44 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
    |                 Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
    |                 @consume parameter or was used as a prefix to a @consume method on line 39
    |                 and therefore is no longer available.
+   |
+   |                 where:    ^ refers to a fresh root capability in the type of value buf1
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:8 ------------------------------------------------------
 48 |    app(buf, 1)  // error
    |        ^^^
    |        Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot
    |        be passed to a @consume parameter or be used as a prefix of a @consume method call.
+   |
+   |        where:    ^ refers to a fresh root capability in the type of parameter buf
diff --git a/tests/neg-custom-args/captures/linear-buffer.scala b/tests/neg-custom-args/captures/linear-buffer.scala
index 97315c1aa0fb..a72f69a22dbd 100644
--- a/tests/neg-custom-args/captures/linear-buffer.scala
+++ b/tests/neg-custom-args/captures/linear-buffer.scala
@@ -3,7 +3,7 @@ import language.experimental.captureChecking
 
 class BadBuffer[T] extends Mutable:
   mut def append(x: T): BadBuffer[T]^ = this // error
-  def foo = // error
+  def foo =
     def bar: BadBuffer[T]^ = this // error
     bar
 
diff --git a/tests/neg-custom-args/captures/outer-var.check b/tests/neg-custom-args/captures/outer-var.check
index a49722eb4bb9..fc6662fd7795 100644
--- a/tests/neg-custom-args/captures/outer-var.check
+++ b/tests/neg-custom-args/captures/outer-var.check
@@ -4,7 +4,8 @@
    |        Found:    (q : () => Unit)
    |        Required: () ->{p, q²} Unit
    |
-   |        where:    q  is a parameter in method inner
+   |        where:    => refers to a fresh root capability in the type of parameter q
+   |                  q  is a parameter in method inner
    |                  q² is a parameter in method test
    |
    | longer explanation available when compiling with `-explain`
@@ -14,6 +15,8 @@
    |         Found:    () => Unit
    |         Required: () ->{p, q} Unit
    |
+   |         where:    => refers to a fresh root capability created in method inner
+   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:14:9 -------------------------------------
 14 |    y = (q: Proc)   // error
@@ -21,6 +24,8 @@
    |         Found:    () => Unit
    |         Required: () ->{p} Unit
    |
+   |         where:    => refers to a fresh root capability created in method inner
+   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:15:8 -------------------------------------
 15 |    y = q           // error, was OK under unsealed
@@ -28,9 +33,13 @@
    |        Found:    (q : () => Unit)
    |        Required: () ->{p} Unit
    |
+   |        where:    => refers to a fresh root capability in the type of parameter q
+   |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/outer-var.scala:17:57 ---------------------------------------------------------
 17 |  var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // error, was OK under unsealed
    |                                                      ^^^^^^^^^^
    |                             Type variable A of object ListBuffer cannot be instantiated to box () => Unit since
    |                             that type captures the root capability `cap`.
+   |
+   |                             where:    => refers to the universal root capability
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
index 8dc433afc979..1cbd53de836c 100644
--- a/tests/neg-custom-args/captures/reaches.check
+++ b/tests/neg-custom-args/captures/reaches.check
@@ -1,42 +1,59 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:22:13 --------------------------------------
 22 |  usingFile: f => // error
    |             ^
-   |             Found:    (f: File^?) ->? Unit
-   |             Required: (f: File^) ->{fresh} Unit
+   |Found:    (f: File^?) ->? Unit
+   |Required: (f: File^) => Unit
+   |
+   |where:    => refers to a fresh root capability created in method runAll0 when checking argument to parameter f of method usingFile
+   |          ^  refers to the universal root capability
 23 |    cur = (() => f.write()) :: Nil
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:32:13 --------------------------------------
 32 |  usingFile: f => // error
    |             ^
-   |             Found:    (f: File^?) ->? Unit
-   |             Required: (f: File^) ->{fresh} Unit
+   |Found:    (f: File^?) ->? Unit
+   |Required: (f: File^) => Unit
+   |
+   |where:    => refers to a fresh root capability created in method runAll1 when checking argument to parameter f of method usingFile
+   |          ^  refers to the universal root capability
 33 |    cur.set:
 34 |      (() => f.write()) :: Nil
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/reaches.scala:37:6 ------------------------------------------------------------
-37 |  var cur: List[Proc] = xs   // error
-   |      ^
-   |      Mutable variable cur cannot have type List[box () => Unit] since
-   |      the part box () => Unit of that type captures the root capability `cap`.
+-- Error: tests/neg-custom-args/captures/reaches.scala:39:31 -----------------------------------------------------------
+39 |    val next: () => Unit = cur.head   // error
+   |                           ^^^^^^^^
+   |                           reference cap is not included in the allowed capture set ?
+   |                           of the enclosing method runAll2
+   |
+   |                           Note that the universal capability cap
+   |                           cannot be included in capture set ?
 -- Error: tests/neg-custom-args/captures/reaches.scala:44:16 -----------------------------------------------------------
 44 |  val cur = Ref[List[Proc]](xs) // error
    |                ^^^^^^^^^^
    |                Type variable T of constructor Ref cannot be instantiated to List[box () => Unit] since
    |                the part box () => Unit of that type captures the root capability `cap`.
+   |
+   |                where:    => refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:46:35 --------------------------------------
 46 |    val next: () => Unit = cur.get.head // error
    |                           ^^^^^^^^^^^^
    |                           Found:    () => Unit
-   |                           Required: () ->{fresh} Unit
+   |                           Required: () =>² Unit
+   |
+   |                           where:    =>  refers to the universal root capability
+   |                                     =>² refers to a fresh root capability in the type of value next
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:48:20 --------------------------------------
 48 |    cur.set(cur.get.tail: List[Proc]) // error
    |            ^^^^^^^^^^^^
    |            Found:    List[box () => Unit]
-   |            Required: List[box () ->{fresh} Unit]
+   |            Required: List[box () =>² Unit]
+   |
+   |            where:    =>  refers to the universal root capability
+   |                      =>² refers to a fresh root capability created in method runAll3
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/reaches.scala:54:51 -----------------------------------------------------------
@@ -44,18 +61,26 @@
    |                                                   ^
    |                                Type variable A of constructor Id cannot be instantiated to box () => Unit since
    |                                that type captures the root capability `cap`.
+   |
+   |                                where:    => refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:59:27 --------------------------------------
 59 |  val id: File^ -> File^ = x => x // error
    |                           ^^^^^^
    |                           Found:    (x: File^) ->? File^{x}
-   |                           Required: (x: File^) -> File^{fresh}
+   |                           Required: (x: File^) -> File^²
+   |
+   |                           where:    ^  refers to the universal root capability
+   |                                     ^² refers to a fresh root capability in the type of value id
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:38 --------------------------------------
 62 |  val leaked = usingFile[File^{id*}]: f => // error // error
    |                                      ^
-   |                                      Found:    (f: File^?) ->? box File^?
-   |                                      Required: (f: File^) ->{fresh} box File^{id*}
+   |Found:    (f: File^?) ->? box File^?
+   |Required: (f: File^) => box File^{id*}
+   |
+   |where:    => refers to a fresh root capability created in value leaked when checking argument to parameter f of method usingFile
+   |          ^  refers to the universal root capability
 63 |    val f1: File^{id*} = id(f)
 64 |    f1
    |
@@ -63,18 +88,25 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:67:32 --------------------------------------
 67 |  val id: (x: File^) -> File^ = x => x // error
    |                                ^^^^^^
-   |                            Found:    (x: File^) ->? File^{x}
-   |                            Required: (x: File^) -> File^{localcap}
+   |                  Found:    (x: File^) ->? File^{x}
+   |                  Required: (x: File^) -> File^²
+   |
+   |                  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
+   |
+   |                  Note that the existential capture root in File^
+   |                  cannot subsume the capability x.type since that capability is not a SharedCapability
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:70:38 --------------------------------------
 70 |  val leaked = usingFile[File^{id*}]: f => // error // error
    |                                      ^
-   |                                      Found:    (f: File^?) ->? box File^?
-   |                                      Required: (f: File^) ->{fresh} box File^{id*}
+   |Found:    (f: File^?) ->? box File^?
+   |Required: (f: File^) => box File^{id*}
+   |
+   |where:    => refers to a fresh root capability created in value leaked when checking argument to parameter f of method usingFile
+   |          ^  refers to the universal root capability
 71 |    val f1: File^{id*} = id(f)
 72 |    f1
    |
@@ -87,8 +119,11 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:91:10 --------------------------------------
 91 |  ps.map((x, y) => compose1(x, y)) // error
    |          ^^^^^^^^^^^^^^^^^^^^^^^
-   |          Found:    (x$1: (box (x$0: A^) ->? A^?, box (x$0: A^) ->? A^?)^?) ->? box (x$0: A^?) ->? A^?
-   |          Required: (x$1: (box A ->{ps*} A, box A ->{ps*} A)) ->{fresh} box (x$0: A^?) ->? A^?
+   |Found:    (x$1: (box A^ ->? A^?, box A^ ->? A^?)^?) ->? box A^? ->? A^?
+   |Required: (x$1: (box A ->{ps*} A, box A ->{ps*} A)) => box A^? ->? A^?
+   |
+   |where:    => refers to a fresh root capability created in method mapCompose2 when checking argument to parameter f of method map
+   |          ^  refers to the universal root capability
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/reaches.scala:62:31 -----------------------------------------------------------
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
index 709f818a02a8..edec54719e4c 100644
--- a/tests/neg-custom-args/captures/reaches.scala
+++ b/tests/neg-custom-args/captures/reaches.scala
@@ -34,9 +34,9 @@ def runAll1(@use xs: List[Proc]): Unit =
       (() => f.write()) :: Nil
 
 def runAll2(@consume xs: List[Proc]): Unit =
-  var cur: List[Proc] = xs   // error
+  var cur: List[Proc] = xs
   while cur.nonEmpty do
-    val next: () => Unit = cur.head
+    val next: () => Unit = cur.head   // error
     next()
     cur = cur.tail
 
diff --git a/tests/neg-custom-args/captures/reaches2.check b/tests/neg-custom-args/captures/reaches2.check
index e9238365ec18..e6009b95d581 100644
--- a/tests/neg-custom-args/captures/reaches2.check
+++ b/tests/neg-custom-args/captures/reaches2.check
@@ -11,14 +11,16 @@
 -- Error: tests/neg-custom-args/captures/reaches2.scala:10:28 ----------------------------------------------------------
 10 |  ps.map((x, y) => compose1(x, y)) // error // error // error
    |                            ^
-   |                            Separation failure: argument of type  A ->{x} A
-   |                            to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
-   |                            corresponds to capture-polymorphic formal parameter f of type  box A^? => box A^?
-   |                            and hides capabilities  {x}.
-   |                            Some of these overlap with the captures of the second argument with type  A ->{y} A.
+   |Separation failure: argument of type  A ->{x} A
+   |to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
+   |corresponds to capture-polymorphic formal parameter f of type  box A^? => box A^?
+   |and hides capabilities  {x}.
+   |Some of these overlap with the captures of the second argument with type  A ->{y} A.
    |
-   |                              Hidden set of current argument        : {x}
-   |                              Hidden footprint of current argument  : {x, ps*}
-   |                              Capture set of second argument        : {y}
-   |                              Footprint set of second argument      : {y, ps*}
-   |                              The two sets overlap at               : {ps*}
+   |  Hidden set of current argument        : {x}
+   |  Hidden footprint of current argument  : {x, ps*}
+   |  Capture set of second argument        : {y}
+   |  Footprint set of second argument      : {y, ps*}
+   |  The two sets overlap at               : {ps*}
+   |
+   |where:    => refers to a fresh root capability created in anonymous function of type (x$1: (box A^? ->{ps*} A^?, box A^? ->{ps*} A^?)^?): A^? ->{ps*} A^? when checking argument to parameter f of method compose1
diff --git a/tests/neg-custom-args/captures/real-try.check b/tests/neg-custom-args/captures/real-try.check
index 6b478b48515a..4dd51e13f270 100644
--- a/tests/neg-custom-args/captures/real-try.check
+++ b/tests/neg-custom-args/captures/real-try.check
@@ -10,6 +10,8 @@
    |  The result of `try` cannot have type () ->{cap.rd} Unit since
    |  that type captures the root capability `cap`.
    |  This is often caused by a locally generated exception capability leaking as part of its result.
+   |
+   |  where:    cap is a fresh root capability in the type of given instance canThrow$1
 15 |    () => foo(1)
 16 |  catch
 17 |    case _: Ex1 => ???
@@ -20,6 +22,8 @@
    |          The result of `try` cannot have type () ->{cap.rd} Unit since
    |          that type captures the root capability `cap`.
    |          This is often caused by a locally generated exception capability leaking as part of its result.
+   |
+   |          where:    cap is a fresh root capability in the type of given instance canThrow$2
 21 |    () => foo(1)
 22 |  catch
 23 |    case _: Ex1 => ???
@@ -30,6 +34,8 @@
    |          The result of `try` cannot have type () ->{cap.rd} Cell[Unit]^? since
    |          that type captures the root capability `cap`.
    |          This is often caused by a locally generated exception capability leaking as part of its result.
+   |
+   |          where:    cap is a fresh root capability in the type of given instance canThrow$3
 27 |    () => Cell(foo(1))
 28 |  catch
 29 |    case _: Ex1 => ???
@@ -40,6 +46,8 @@
    |          The result of `try` cannot have type Cell[box () ->{cap.rd} Unit]^? since
    |          the part box () ->{cap.rd} Unit of that type captures the root capability `cap`.
    |          This is often caused by a locally generated exception capability leaking as part of its result.
+   |
+   |          where:    cap is a fresh root capability in the type of given instance canThrow$4
 33 |    Cell(() => foo(1))
 34 |  catch
 35 |    case _: Ex1 => ???
diff --git a/tests/neg-custom-args/captures/scoped-caps.check b/tests/neg-custom-args/captures/scoped-caps.check
new file mode 100644
index 000000000000..e35af6b10bb9
--- /dev/null
+++ b/tests/neg-custom-args/captures/scoped-caps.check
@@ -0,0 +1,108 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:7:20 -----------------------------------
+7 |  val g: A^ -> B^ = f // error
+  |                    ^
+  |                    Found:    (f : (x: A^) -> B^²)
+  |                    Required: A^ -> B^³
+  |
+  |                    where:    ^  refers to the universal root capability
+  |                              ^² refers to a root capability associated with the result type of (x: A^): B^²
+  |                              ^³ refers to a fresh root capability in the type of value g
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:9:25 -----------------------------------
+9 |  val _: (x: A^) -> B^ = g // error
+  |                         ^
+  |                         Found:    (g : A^ -> B^²)
+  |                         Required: (x: A^) -> B^³
+  |
+  |                         where:    ^  refers to the universal root capability
+  |                                   ^² 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
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:10:20 ----------------------------------
+10 |  val _: A^ -> B^ = f // error
+   |                    ^
+   |                    Found:    (f : (x: A^) -> B^²)
+   |                    Required: A^ -> B^³
+   |
+   |                    where:    ^  refers to the universal root capability
+   |                              ^² refers to a root capability associated with the result type of (x: A^): B^²
+   |                              ^³ refers to a fresh root capability in the type of value _$3
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:12:20 ----------------------------------
+12 |  val _: A^ -> B^ = x => g(x)      // error, since g is pure, g(x): B^{x} , which does not match B^{fresh}
+   |                    ^^^^^^^^^
+   |                    Found:    (x: A^) ->? B^{x}
+   |                    Required: (x: A^) -> B^²
+   |
+   |                    where:    ^  refers to the universal root capability
+   |                              ^² refers to a fresh root capability in the type of value _$5
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:13:25 ----------------------------------
+13 |  val _: (x: A^) -> B^ = x => f(x) // error: existential in B cannot subsume `x` since `x` is not shared
+   |                         ^^^^^^^^^
+   |                        Found:    (x: A^) ->? B^{x}
+   |                        Required: (x: A^) -> B^²
+   |
+   |                        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
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:16:24 ----------------------------------
+16 |  val _: (x: S) -> B^ = h          // error: direct conversion fails
+   |                        ^
+   |               Found:    (h : S -> B^)
+   |               Required: (x: S^{cap.rd}) -> B^²
+   |
+   |               where:    ^   refers to a fresh root capability in the type of value h
+   |                         ^²  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
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:22:19 ----------------------------------
+22 |  val _: S -> B^ = j               // error
+   |                   ^
+   |                Found:    (j : (x: S) -> B^)
+   |                Required: S^{cap.rd} -> B^²
+   |
+   |                where:    ^   refers to a root capability associated with the result type of (x: S^{cap.rd}): B^
+   |                          ^²  refers to a fresh root capability in the type of value _$11
+   |                          cap is the universal root capability
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:23:19 ----------------------------------
+23 |  val _: S -> B^ = x => j(x)       // error
+   |                   ^^^^^^^^^
+   |                   Found:    (x: S^{cap.rd}) ->? B^{x}
+   |                   Required: (x: S^{cap.rd}) -> B^
+   |
+   |                   where:    ^   refers to a fresh root capability in the type of value _$12
+   |                             cap is the universal root capability
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:26:20 ----------------------------------
+26 |  val _: A^ => B^ = x => g2(x)  // error: g2(x): B^{g2, x}, and the `x` cannot be subsumed by fresh
+   |                    ^^^^^^^^^^
+   |                    Found:    (x: A^) ->{g2} B^{g2, x}
+   |                    Required: (x: A^) => B^²
+   |
+   |                    where:    => refers to a fresh root capability in the type of value _$13
+   |                              ^  refers to the universal root capability
+   |                              ^² refers to a fresh root capability in the type of value _$13
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/sep-box.check b/tests/neg-custom-args/captures/sep-box.check
index f60f09d906a8..c3f0bed0df4e 100644
--- a/tests/neg-custom-args/captures/sep-box.check
+++ b/tests/neg-custom-args/captures/sep-box.check
@@ -1,14 +1,16 @@
 -- Error: tests/neg-custom-args/captures/sep-box.scala:41:9 ------------------------------------------------------------
 41 |  par(h1.value, h2.value) // error
    |      ^^^^^^^^
-   |      Separation failure: argument of type  Ref^{h1.value*}
-   |      to method par: (x: Ref^, y: Ref^): Unit
-   |      corresponds to capture-polymorphic formal parameter x of type  Ref^
-   |      and hides capabilities  {h1.value*}.
-   |      Some of these overlap with the captures of the second argument with type  Ref^{h2.value*}.
+   |Separation failure: argument of type  Ref^{h1.value*}
+   |to method par: (x: Ref^, y: Ref^): Unit
+   |corresponds to capture-polymorphic formal parameter x of type  Ref^
+   |and hides capabilities  {h1.value*}.
+   |Some of these overlap with the captures of the second argument with type  Ref^{h2.value*}.
    |
-   |        Hidden set of current argument        : {h1.value*}
-   |        Hidden footprint of current argument  : {h1.value*, xs*}
-   |        Capture set of second argument        : {h2.value*}
-   |        Footprint set of second argument      : {h2.value*, xs*}
-   |        The two sets overlap at               : {xs*}
+   |  Hidden set of current argument        : {h1.value*}
+   |  Hidden footprint of current argument  : {h1.value*, xs*}
+   |  Capture set of second argument        : {h2.value*}
+   |  Footprint set of second argument      : {h2.value*, xs*}
+   |  The two sets overlap at               : {xs*}
+   |
+   |where:    ^ refers to a fresh root capability created in method test when checking argument to parameter x of method par
diff --git a/tests/neg-custom-args/captures/sep-compose.check b/tests/neg-custom-args/captures/sep-compose.check
index 3bd1e5b08eeb..b53bc3036d4e 100644
--- a/tests/neg-custom-args/captures/sep-compose.check
+++ b/tests/neg-custom-args/captures/sep-compose.check
@@ -1,112 +1,128 @@
 -- Error: tests/neg-custom-args/captures/sep-compose.scala:32:7 --------------------------------------------------------
 32 |  seq3(f)(f) // error
    |       ^
-   |       Separation failure: argument of type  (f : () ->{a} Unit)
-   |       to method seq3: (x: () => Unit)(y: () ->{a, cap} Unit): Unit
-   |       corresponds to capture-polymorphic formal parameter x of type  () => Unit
-   |       and hides capabilities  {f}.
-   |       Some of these overlap with the captures of the second argument with type  (f : () ->{a} Unit).
-   |
-   |         Hidden set of current argument        : {f}
-   |         Hidden footprint of current argument  : {f, a, io}
-   |         Capture set of second argument        : {f}
-   |         Footprint set of second argument      : {f, a, io}
-   |         The two sets overlap at               : {f, a, io}
+   |Separation failure: argument of type  (f : () ->{a} Unit)
+   |to method seq3: (x: () => Unit)(y: () ->{a, cap} Unit): Unit
+   |corresponds to capture-polymorphic formal parameter x of type  () => Unit
+   |and hides capabilities  {f}.
+   |Some of these overlap with the captures of the second argument with type  (f : () ->{a} Unit).
+   |
+   |  Hidden set of current argument        : {f}
+   |  Hidden footprint of current argument  : {f, a, io}
+   |  Capture set of second argument        : {f}
+   |  Footprint set of second argument      : {f, a, io}
+   |  The two sets overlap at               : {f, a, io}
+   |
+   |where:    => refers to a fresh root capability created in method test when checking argument to parameter x of method seq3
 -- Error: tests/neg-custom-args/captures/sep-compose.scala:33:10 -------------------------------------------------------
 33 |  seq4(f)(f) // error
    |          ^
-   |          Separation failure: argument of type  (f : () ->{a} Unit)
-   |          to method seq4: (x: () ->{a, cap} Unit)(y: () => Unit): Unit
-   |          corresponds to capture-polymorphic formal parameter y of type  () => Unit
-   |          and hides capabilities  {f}.
-   |          Some of these overlap with the captures of the first argument with type  (f : () ->{a} Unit).
-   |
-   |            Hidden set of current argument        : {f}
-   |            Hidden footprint of current argument  : {f, a, io}
-   |            Capture set of first argument         : {f}
-   |            Footprint set of first argument       : {f, a, io}
-   |            The two sets overlap at               : {f, a, io}
+   |Separation failure: argument of type  (f : () ->{a} Unit)
+   |to method seq4: (x: () ->{a, cap} Unit)(y: () => Unit): Unit
+   |corresponds to capture-polymorphic formal parameter y of type  () => Unit
+   |and hides capabilities  {f}.
+   |Some of these overlap with the captures of the first argument with type  (f : () ->{a} Unit).
+   |
+   |  Hidden set of current argument        : {f}
+   |  Hidden footprint of current argument  : {f, a, io}
+   |  Capture set of first argument         : {f}
+   |  Footprint set of first argument       : {f, a, io}
+   |  The two sets overlap at               : {f, a, io}
+   |
+   |where:    => refers to a fresh root capability created in method test when checking argument to parameter y of method seq4
 -- Error: tests/neg-custom-args/captures/sep-compose.scala:34:7 --------------------------------------------------------
 34 |  seq5(f)(f) // error
    |       ^
-   |       Separation failure: argument of type  (f : () ->{a} Unit)
-   |       to method seq5: (x: () => Unit)(y: () => Unit): Unit
-   |       corresponds to capture-polymorphic formal parameter x of type  () => Unit
-   |       and hides capabilities  {f}.
-   |       Some of these overlap with the captures of the second argument with type  (f : () ->{a} Unit).
-   |
-   |         Hidden set of current argument        : {f}
-   |         Hidden footprint of current argument  : {f, a, io}
-   |         Capture set of second argument        : {f}
-   |         Footprint set of second argument      : {f, a, io}
-   |         The two sets overlap at               : {f, a, io}
+   |Separation failure: argument of type  (f : () ->{a} Unit)
+   |to method seq5: (x: () => Unit)(y: () => Unit): Unit
+   |corresponds to capture-polymorphic formal parameter x of type  () => Unit
+   |and hides capabilities  {f}.
+   |Some of these overlap with the captures of the second argument with type  (f : () ->{a} Unit).
+   |
+   |  Hidden set of current argument        : {f}
+   |  Hidden footprint of current argument  : {f, a, io}
+   |  Capture set of second argument        : {f}
+   |  Footprint set of second argument      : {f, a, io}
+   |  The two sets overlap at               : {f, a, io}
+   |
+   |where:    => refers to a fresh root capability created in method test when checking argument to parameter x of method seq5
 -- Error: tests/neg-custom-args/captures/sep-compose.scala:35:7 --------------------------------------------------------
 35 |  seq6(f, f) // error
    |       ^
-   |       Separation failure: argument of type  (f : () ->{a} Unit)
-   |       to method seq6: (x: () => Unit, y: () ->{a, cap} Unit): Unit
-   |       corresponds to capture-polymorphic formal parameter x of type  () => Unit
-   |       and hides capabilities  {f}.
-   |       Some of these overlap with the captures of the second argument with type  (f : () ->{a} Unit).
-   |
-   |         Hidden set of current argument        : {f}
-   |         Hidden footprint of current argument  : {f, a, io}
-   |         Capture set of second argument        : {f}
-   |         Footprint set of second argument      : {f, a, io}
-   |         The two sets overlap at               : {f, a, io}
+   |Separation failure: argument of type  (f : () ->{a} Unit)
+   |to method seq6: (x: () => Unit, y: () ->{a, cap} Unit): Unit
+   |corresponds to capture-polymorphic formal parameter x of type  () => Unit
+   |and hides capabilities  {f}.
+   |Some of these overlap with the captures of the second argument with type  (f : () ->{a} Unit).
+   |
+   |  Hidden set of current argument        : {f}
+   |  Hidden footprint of current argument  : {f, a, io}
+   |  Capture set of second argument        : {f}
+   |  Footprint set of second argument      : {f, a, io}
+   |  The two sets overlap at               : {f, a, io}
+   |
+   |where:    => refers to a fresh root capability created in method test when checking argument to parameter x of method seq6
 -- Error: tests/neg-custom-args/captures/sep-compose.scala:36:10 -------------------------------------------------------
 36 |  seq7(f, f) // error
    |          ^
-   |          Separation failure: argument of type  (f : () ->{a} Unit)
-   |          to method seq7: (x: () ->{a, cap} Unit, y: () => Unit): Unit
-   |          corresponds to capture-polymorphic formal parameter y of type  () => Unit
-   |          and hides capabilities  {f}.
-   |          Some of these overlap with the captures of the first argument with type  (f : () ->{a} Unit).
-   |
-   |            Hidden set of current argument        : {f}
-   |            Hidden footprint of current argument  : {f, a, io}
-   |            Capture set of first argument         : {f}
-   |            Footprint set of first argument       : {f, a, io}
-   |            The two sets overlap at               : {f, a, io}
+   |Separation failure: argument of type  (f : () ->{a} Unit)
+   |to method seq7: (x: () ->{a, cap} Unit, y: () => Unit): Unit
+   |corresponds to capture-polymorphic formal parameter y of type  () => Unit
+   |and hides capabilities  {f}.
+   |Some of these overlap with the captures of the first argument with type  (f : () ->{a} Unit).
+   |
+   |  Hidden set of current argument        : {f}
+   |  Hidden footprint of current argument  : {f, a, io}
+   |  Capture set of first argument         : {f}
+   |  Footprint set of first argument       : {f, a, io}
+   |  The two sets overlap at               : {f, a, io}
+   |
+   |where:    => refers to a fresh root capability created in method test when checking argument to parameter y of method seq7
 -- Error: tests/neg-custom-args/captures/sep-compose.scala:37:7 --------------------------------------------------------
 37 |  seq8(f)(f) // error
    |       ^
-   |       Separation failure: argument of type  (f : () ->{a} Unit)
-   |       to method seq8: (x: () => Unit)(y: () ->{a} Unit): Unit
-   |       corresponds to capture-polymorphic formal parameter x of type  () => Unit
-   |       and hides capabilities  {f}.
-   |       Some of these overlap with the captures of the second argument with type  (f : () ->{a} Unit).
-   |
-   |         Hidden set of current argument        : {f}
-   |         Hidden footprint of current argument  : {f, a, io}
-   |         Capture set of second argument        : {f}
-   |         Footprint set of second argument      : {f, a, io}
-   |         The two sets overlap at               : {f, a, io}
+   |Separation failure: argument of type  (f : () ->{a} Unit)
+   |to method seq8: (x: () => Unit)(y: () ->{a} Unit): Unit
+   |corresponds to capture-polymorphic formal parameter x of type  () => Unit
+   |and hides capabilities  {f}.
+   |Some of these overlap with the captures of the second argument with type  (f : () ->{a} Unit).
+   |
+   |  Hidden set of current argument        : {f}
+   |  Hidden footprint of current argument  : {f, a, io}
+   |  Capture set of second argument        : {f}
+   |  Footprint set of second argument      : {f, a, io}
+   |  The two sets overlap at               : {f, a, io}
+   |
+   |where:    => refers to a fresh root capability created in method test when checking argument to parameter x of method seq8
 -- Error: tests/neg-custom-args/captures/sep-compose.scala:40:5 --------------------------------------------------------
 40 |  p1(f) // error
    |     ^
-   |     Separation failure: argument of type  (f : () ->{a} Unit)
-   |     to a function of type (() => Unit) ->{f} Unit
-   |     corresponds to capture-polymorphic formal parameter v1 of type  () => Unit
-   |     and hides capabilities  {f}.
-   |     Some of these overlap with the captures of the function prefix.
-   |
-   |       Hidden set of current argument        : {f}
-   |       Hidden footprint of current argument  : {f, a, io}
-   |       Capture set of function prefix        : {p1}
-   |       Footprint set of function prefix      : {p1, f, a, io}
-   |       The two sets overlap at               : {f, a, io}
+   |Separation failure: argument of type  (f : () ->{a} Unit)
+   |to a function of type (() => Unit) ->{f} Unit
+   |corresponds to capture-polymorphic formal parameter v1 of type  () => Unit
+   |and hides capabilities  {f}.
+   |Some of these overlap with the captures of the function prefix.
+   |
+   |  Hidden set of current argument        : {f}
+   |  Hidden footprint of current argument  : {f, a, io}
+   |  Capture set of function prefix        : {p1}
+   |  Footprint set of function prefix      : {p1, f, a, io}
+   |  The two sets overlap at               : {f, a, io}
+   |
+   |where:    => refers to a fresh root capability created in method test when checking argument to parameter v1 of method apply
 -- Error: tests/neg-custom-args/captures/sep-compose.scala:41:38 -------------------------------------------------------
 41 |  val p8 = (x: () ->{a} Unit) => seq8(f)(x) // error
    |                                      ^
-   |                  Separation failure: argument of type  (f : () ->{a} Unit)
-   |                  to method seq8: (x: () => Unit)(y: () ->{a} Unit): Unit
-   |                  corresponds to capture-polymorphic formal parameter x of type  () => Unit
-   |                  and hides capabilities  {f}.
-   |                  Some of these overlap with the captures of the second argument with type  (x : () ->{a} Unit).
-   |
-   |                    Hidden set of current argument        : {f}
-   |                    Hidden footprint of current argument  : {f, a, io}
-   |                    Capture set of second argument        : {x}
-   |                    Footprint set of second argument      : {x, a, io}
-   |                    The two sets overlap at               : {a, io}
+   |Separation failure: argument of type  (f : () ->{a} Unit)
+   |to method seq8: (x: () => Unit)(y: () ->{a} Unit): Unit
+   |corresponds to capture-polymorphic formal parameter x of type  () => Unit
+   |and hides capabilities  {f}.
+   |Some of these overlap with the captures of the second argument with type  (x : () ->{a} Unit).
+   |
+   |  Hidden set of current argument        : {f}
+   |  Hidden footprint of current argument  : {f, a, io}
+   |  Capture set of second argument        : {x}
+   |  Footprint set of second argument      : {x, a, io}
+   |  The two sets overlap at               : {a, io}
+   |
+   |where:    => refers to a fresh root capability created in anonymous function of type (x²: () ->{a} Unit): Unit when checking argument to parameter x of method seq8
diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check
index d8ee2c5ed43e..200b5b458070 100644
--- a/tests/neg-custom-args/captures/sep-consume.check
+++ b/tests/neg-custom-args/captures/sep-consume.check
@@ -4,12 +4,16 @@
    |  Separation failure: Illegal access to (x : Ref^), which was passed to a
    |  @consume parameter or was used as a prefix to a @consume method on line 18
    |  and therefore is no longer available.
+   |
+   |  where:    ^ refers to a fresh root capability in the type of parameter x
 -- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 -------------------------------------------------------
 21 |  par(rx, () => x.put(42))  // error
    |                ^
    |                Separation failure: Illegal access to (x : Ref^), which was passed to a
    |                @consume parameter or was used as a prefix to a @consume method on line 18
    |                and therefore is no longer available.
+   |
+   |                where:    ^ refers to a fresh root capability in the type of parameter x
 -- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 -------------------------------------------------------
 26 |  def foo = bad(f) // error
    |                ^
diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check
index 230c1e6f6e53..ee38eba5eab9 100644
--- a/tests/neg-custom-args/captures/sep-counter.check
+++ b/tests/neg-custom-args/captures/sep-counter.check
@@ -1,7 +1,11 @@
 -- Error: tests/neg-custom-args/captures/sep-counter.scala:12:19 -------------------------------------------------------
 12 |  def mkCounter(): Pair[Ref^, Ref^] =  // error
    |                   ^^^^^^^^^^^^^^^^
-   |                   Separation failure in method mkCounter's result type Pair[box Ref^, box Ref^].
+   |                   Separation failure in method mkCounter's result type Pair[box Ref^, box Ref^²].
    |                   One part,  box Ref^, hides capabilities  {cap}.
-   |                   Another part,  box Ref^,  captures capabilities  {cap}.
+   |                   Another part,  box Ref^²,  captures capabilities  {cap}.
    |                   The two sets overlap at  cap of value c.
+   |
+   |                   where:    ^   refers to a fresh root capability in the result type of method mkCounter
+   |                             ^²  refers to a fresh root capability in the result type of method mkCounter
+   |                             cap is a fresh root capability created in value c when constructing mutable Ref
diff --git a/tests/neg-custom-args/captures/sep-curried.check b/tests/neg-custom-args/captures/sep-curried.check
index edf359c4be14..1cdce6b2bb99 100644
--- a/tests/neg-custom-args/captures/sep-curried.check
+++ b/tests/neg-custom-args/captures/sep-curried.check
@@ -4,74 +4,91 @@
    |                                        Found:    (y: Ref[Int]^) ->{a} Unit
    |                                        Required: (y: Ref[Int]^{a}) ->{a} Unit
    |
+   |                                        where:    ^ refers to the universal root capability
+   |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/sep-curried.scala:16:6 --------------------------------------------------------
 16 |  foo(a)(a)  // error
    |      ^
-   |      Separation failure: argument of type  (a : Ref[Int]^)
-   |      to method foo: (x: Ref[Int]^)(y: Ref[Int]^{a}): Unit
-   |      corresponds to capture-polymorphic formal parameter x of type  Ref[Int]^
-   |      and hides capabilities  {a}.
-   |      Some of these overlap with the captures of the second argument with type  (a : Ref[Int]^).
+   |Separation failure: argument of type  (a : Ref[Int]^)
+   |to method foo: (x: Ref[Int]^)(y: Ref[Int]^{a}): Unit
+   |corresponds to capture-polymorphic formal parameter x of type  Ref[Int]^²
+   |and hides capabilities  {a}.
+   |Some of these overlap with the captures of the second argument with type  (a : Ref[Int]^).
+   |
+   |  Hidden set of current argument        : {a}
+   |  Hidden footprint of current argument  : {a}
+   |  Capture set of second argument        : {a}
+   |  Footprint set of second argument      : {a}
+   |  The two sets overlap at               : {a}
    |
-   |        Hidden set of current argument        : {a}
-   |        Hidden footprint of current argument  : {a}
-   |        Capture set of second argument        : {a}
-   |        Footprint set of second argument      : {a}
-   |        The two sets overlap at               : {a}
+   |where:    ^  refers to a fresh root capability in the type of value a
+   |          ^² refers to a fresh root capability created in method test0 when checking argument to parameter x of method foo
 -- Error: tests/neg-custom-args/captures/sep-curried.scala:22:44 -------------------------------------------------------
 22 |  val f: (y: Ref[Int]^{a}) ->{a} Unit = foo(a) // error
    |                                            ^
-   |         Separation failure: argument of type  (a : Ref[Int]^)
-   |         to a function of type (x: Ref[Int]^) -> (y: Ref[Int]^{a}) ->{x} Unit
-   |         corresponds to capture-polymorphic formal parameter x of type  Ref[Int]^
-   |         and hides capabilities  {a}.
-   |         Some of these overlap with the captures of the function result with type  (y: Ref[Int]^{a}) ->{a} Unit.
+   |Separation failure: argument of type  (a : Ref[Int]^)
+   |to a function of type (x: Ref[Int]^) -> (y: Ref[Int]^{a}) ->{x} Unit
+   |corresponds to capture-polymorphic formal parameter x of type  Ref[Int]^²
+   |and hides capabilities  {a}.
+   |Some of these overlap with the captures of the function result with type  (y: Ref[Int]^{a}) ->{a} Unit.
+   |
+   |  Hidden set of current argument        : {a}
+   |  Hidden footprint of current argument  : {a}
+   |  Capture set of function result        : {a}
+   |  Footprint set of function result      : {a}
+   |  The two sets overlap at               : {a}
    |
-   |           Hidden set of current argument        : {a}
-   |           Hidden footprint of current argument  : {a}
-   |           Capture set of function result        : {a}
-   |           Footprint set of function result      : {a}
-   |           The two sets overlap at               : {a}
+   |where:    ^  refers to a fresh root capability in the type of value a
+   |          ^² refers to a fresh root capability created in value f when checking argument to parameter x of method apply
 -- Error: tests/neg-custom-args/captures/sep-curried.scala:29:6 --------------------------------------------------------
 29 |  foo(a)(a)  // error
    |      ^
-   |      Separation failure: argument of type  (a : Ref[Int]^)
-   |      to a function of type (x: Ref[Int]^) -> (y: Ref[Int]^{a}) ->{x} Unit
-   |      corresponds to capture-polymorphic formal parameter x of type  Ref[Int]^
-   |      and hides capabilities  {a}.
-   |      Some of these overlap with the captures of the function result with type  (y: Ref[Int]^{a}) ->{a} Unit.
+   |Separation failure: argument of type  (a : Ref[Int]^)
+   |to a function of type (x: Ref[Int]^) -> (y: Ref[Int]^{a}) ->{x} Unit
+   |corresponds to capture-polymorphic formal parameter x of type  Ref[Int]^²
+   |and hides capabilities  {a}.
+   |Some of these overlap with the captures of the function result with type  (y: Ref[Int]^{a}) ->{a} Unit.
    |
-   |        Hidden set of current argument        : {a}
-   |        Hidden footprint of current argument  : {a}
-   |        Capture set of function result        : {a}
-   |        Footprint set of function result      : {a}
-   |        The two sets overlap at               : {a}
+   |  Hidden set of current argument        : {a}
+   |  Hidden footprint of current argument  : {a}
+   |  Capture set of function result        : {a}
+   |  Footprint set of function result      : {a}
+   |  The two sets overlap at               : {a}
+   |
+   |where:    ^  refers to a fresh root capability in the type of value a
+   |          ^² refers to a fresh root capability created in method test2 when checking argument to parameter x of method apply
 -- Error: tests/neg-custom-args/captures/sep-curried.scala:35:9 --------------------------------------------------------
 35 |  foo(a)(a)  // error
    |         ^
-   |         Separation failure: argument of type  (a : Ref[Int]^)
-   |         to a function of type (y: Ref[Int]^) ->{a} Unit
-   |         corresponds to capture-polymorphic formal parameter y of type  Ref[Int]^
-   |         and hides capabilities  {a}.
-   |         Some of these overlap with the captures of the function prefix.
+   |Separation failure: argument of type  (a : Ref[Int]^)
+   |to a function of type (y: Ref[Int]^) ->{a} Unit
+   |corresponds to capture-polymorphic formal parameter y of type  Ref[Int]^²
+   |and hides capabilities  {a}.
+   |Some of these overlap with the captures of the function prefix.
+   |
+   |  Hidden set of current argument        : {a}
+   |  Hidden footprint of current argument  : {a}
+   |  Capture set of function prefix        : {a}
+   |  Footprint set of function prefix      : {a}
+   |  The two sets overlap at               : {a}
    |
-   |           Hidden set of current argument        : {a}
-   |           Hidden footprint of current argument  : {a}
-   |           Capture set of function prefix        : {a}
-   |           Footprint set of function prefix      : {a}
-   |           The two sets overlap at               : {a}
+   |where:    ^  refers to a fresh root capability in the type of value a
+   |          ^² refers to a fresh root capability created in method test3 when checking argument to parameter y of method apply
 -- Error: tests/neg-custom-args/captures/sep-curried.scala:42:4 --------------------------------------------------------
 42 |  f(a) // error
    |    ^
-   |    Separation failure: argument of type  (a : Ref[Int]^)
-   |    to a function of type (y: Ref[Int]^) ->{a} Unit
-   |    corresponds to capture-polymorphic formal parameter y of type  Ref[Int]^
-   |    and hides capabilities  {a}.
-   |    Some of these overlap with the captures of the function prefix.
+   |Separation failure: argument of type  (a : Ref[Int]^)
+   |to a function of type (y: Ref[Int]^) ->{a} Unit
+   |corresponds to capture-polymorphic formal parameter y of type  Ref[Int]^²
+   |and hides capabilities  {a}.
+   |Some of these overlap with the captures of the function prefix.
+   |
+   |  Hidden set of current argument        : {a}
+   |  Hidden footprint of current argument  : {a}
+   |  Capture set of function prefix        : {f}
+   |  Footprint set of function prefix      : {f, a}
+   |  The two sets overlap at               : {a}
    |
-   |      Hidden set of current argument        : {a}
-   |      Hidden footprint of current argument  : {a}
-   |      Capture set of function prefix        : {f}
-   |      Footprint set of function prefix      : {f, a}
-   |      The two sets overlap at               : {a}
+   |where:    ^  refers to a fresh root capability in the type of value a
+   |          ^² refers to a fresh root capability created in method test4 when checking argument to parameter y of method apply
diff --git a/tests/neg-custom-args/captures/sep-lazyListState.check b/tests/neg-custom-args/captures/sep-lazyListState.check
new file mode 100644
index 000000000000..519d143983bf
--- /dev/null
+++ b/tests/neg-custom-args/captures/sep-lazyListState.check
@@ -0,0 +1,5 @@
+-- Error: tests/neg-custom-args/captures/sep-lazyListState.scala:13:14 -------------------------------------------------
+13 |    def tail: LazyListIterable[A]^ = tl // error
+   |              ^^^^^^^^^^^^^^^^^^^^
+   |    Separation failure: method tail's result type LazyListIterable[A]^ hides non-local this of class class Cons.
+   |    The access must be in a @consume method to allow this.
diff --git a/tests/neg-custom-args/captures/sep-lazyListState.scala b/tests/neg-custom-args/captures/sep-lazyListState.scala
new file mode 100644
index 000000000000..4ef39eb4912d
--- /dev/null
+++ b/tests/neg-custom-args/captures/sep-lazyListState.scala
@@ -0,0 +1,14 @@
+class LazyListIterable[+A]
+
+private sealed trait State[+A]:
+  def head: A
+  def tail: LazyListIterable[A]^
+
+private object State:
+  object Empty extends State[Nothing]:
+    def head: Nothing = throw new NoSuchElementException("head of empty lazy list")
+    def tail: LazyListIterable[Nothing] = throw new UnsupportedOperationException("tail of empty lazy list")
+
+  final class Cons[A](val head: A, tl: LazyListIterable[A]^) extends State[A]:
+    def tail: LazyListIterable[A]^ = tl // error
+
diff --git a/tests/neg-custom-args/captures/sep-list.check b/tests/neg-custom-args/captures/sep-list.check
index 86d4937677e8..5ecde5d6d2bd 100644
--- a/tests/neg-custom-args/captures/sep-list.check
+++ b/tests/neg-custom-args/captures/sep-list.check
@@ -1,14 +1,16 @@
 -- Error: tests/neg-custom-args/captures/sep-list.scala:39:6 -----------------------------------------------------------
 39 |  par(h1, h2) // error
    |      ^^
-   |      Separation failure: argument of type  (h1 : Ref^{xs*})
-   |      to method par: (x: Ref^, y: Ref^): Unit
-   |      corresponds to capture-polymorphic formal parameter x of type  Ref^
-   |      and hides capabilities  {h1}.
-   |      Some of these overlap with the captures of the second argument with type  (h2 : Ref^{xs*}).
+   |Separation failure: argument of type  (h1 : Ref^{xs*})
+   |to method par: (x: Ref^, y: Ref^): Unit
+   |corresponds to capture-polymorphic formal parameter x of type  Ref^
+   |and hides capabilities  {h1}.
+   |Some of these overlap with the captures of the second argument with type  (h2 : Ref^{xs*}).
    |
-   |        Hidden set of current argument        : {h1}
-   |        Hidden footprint of current argument  : {h1, xs*}
-   |        Capture set of second argument        : {h2}
-   |        Footprint set of second argument      : {h2, xs*}
-   |        The two sets overlap at               : {xs*}
+   |  Hidden set of current argument        : {h1}
+   |  Hidden footprint of current argument  : {h1, xs*}
+   |  Capture set of second argument        : {h2}
+   |  Footprint set of second argument      : {h2, xs*}
+   |  The two sets overlap at               : {xs*}
+   |
+   |where:    ^ refers to a fresh root capability created in method test when checking argument to parameter x of method par
diff --git a/tests/neg-custom-args/captures/sep-pairs-2.scala b/tests/neg-custom-args/captures/sep-pairs-2.scala
new file mode 100644
index 000000000000..cfe6bfbf8014
--- /dev/null
+++ b/tests/neg-custom-args/captures/sep-pairs-2.scala
@@ -0,0 +1,21 @@
+import caps.Mutable
+import caps.cap
+
+class Ref extends Mutable:
+  var x = 0
+  def get: Int = x
+  mut def put(y: Int): Unit = x = y
+
+class Pair[+X, +Y](val fst: X, val snd: Y)
+
+def twoRefs1(): Pair[Ref^, Ref^] =
+  Pair(Ref(), Ref())
+
+def twoRefs2(): Pair[Ref^, Ref^] =
+  val p = Pair(Ref(), Ref())
+  Pair(p.fst, p.snd)
+
+def twoRefs3(): Pair[Ref^, Ref^] = // error but should work
+  val p = Pair(Ref(), Ref())
+  p
+
diff --git a/tests/neg-custom-args/captures/sep-pairs.check b/tests/neg-custom-args/captures/sep-pairs.check
index fd3e00c138bf..07460db49656 100644
--- a/tests/neg-custom-args/captures/sep-pairs.check
+++ b/tests/neg-custom-args/captures/sep-pairs.check
@@ -1,41 +1,32 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/sep-pairs.scala:32:10 ------------------------------------
-32 |  Pair(Ref(), Ref()) // error // error: universal capability cannot be included in capture set
-   |       ^^^^^
-   |       Found:    box Ref^
-   |       Required: box Ref^?
-   |
-   |       Note that the universal capability `cap`
-   |       cannot be included in capture set ?
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/sep-pairs.scala:32:17 ------------------------------------
-32 |  Pair(Ref(), Ref()) // error // error: universal capability cannot be included in capture set
-   |              ^^^^^
-   |              Found:    box Ref^
-   |              Required: box Ref^?
-   |
-   |              Note that the universal capability `cap`
-   |              cannot be included in capture set ?
-   |
-   | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/sep-pairs.scala:15:10 ---------------------------------------------------------
 15 |  val r1: Pair[Ref^, Ref^] = mkPair(r0) // error: overlap at r0
    |          ^^^^^^^^^^^^^^^^
-   |          Separation failure in value r1's type Pair[box Ref^, box Ref^].
+   |          Separation failure in value r1's type Pair[box Ref^, box Ref^²].
    |          One part,  box Ref^, hides capabilities  {r0}.
-   |          Another part,  box Ref^,  captures capabilities  {r0}.
+   |          Another part,  box Ref^²,  captures capabilities  {r0}.
    |          The two sets overlap at  {r0}.
+   |
+   |          where:    ^  refers to a fresh root capability in the type of value r1
+   |                    ^² refers to a fresh root capability in the type of value r1
 -- Error: tests/neg-custom-args/captures/sep-pairs.scala:13:9 ----------------------------------------------------------
 13 |def bad: Pair[Ref^, Ref^] =  // error: overlap at r1*, r0
    |         ^^^^^^^^^^^^^^^^
-   |         Separation failure in method bad's result type Pair[box Ref^, box Ref^].
-   |         One part,  box Ref^, hides capabilities  {cap, cap, r1*, r0}.
-   |         Another part,  box Ref^,  captures capabilities  {cap, cap, r1*, r0}.
+   |         Separation failure in method bad's result type Pair[box Ref^, box Ref^²].
+   |         One part,  box Ref^, hides capabilities  {cap, cap², r1*, r0}.
+   |         Another part,  box Ref^²,  captures capabilities  {cap, cap², r1*, r0}.
    |         The two sets overlap at  {r1*, r0}.
--- Error: tests/neg-custom-args/captures/sep-pairs.scala:44:18 ---------------------------------------------------------
-44 |  val sameToPair: Pair[Ref^, Ref^] = Pair(fstSame, sndSame) // error
+   |
+   |         where:    ^    refers to a fresh root capability in the result type of method bad
+   |                   ^²   refers to a fresh root capability in the result type of method bad
+   |                   cap  is a fresh root capability in the type of value r1
+   |                   cap² is a fresh root capability in the type of value r1
+-- Error: tests/neg-custom-args/captures/sep-pairs.scala:43:18 ---------------------------------------------------------
+43 |  val sameToPair: Pair[Ref^, Ref^] = Pair(fstSame, sndSame) // error
    |                  ^^^^^^^^^^^^^^^^
-   |                  Separation failure in value sameToPair's type Pair[box Ref^, box Ref^].
+   |                  Separation failure in value sameToPair's type Pair[box Ref^, box Ref^²].
    |                  One part,  box Ref^, hides capabilities  {fstSame}.
-   |                  Another part,  box Ref^,  captures capabilities  {sndSame}.
+   |                  Another part,  box Ref^²,  captures capabilities  {sndSame}.
    |                  The two sets overlap at  cap of value same.
+   |
+   |                  where:    ^  refers to a fresh root capability in the type of value sameToPair
+   |                            ^² refers to a fresh root capability in the type of value sameToPair
diff --git a/tests/neg-custom-args/captures/sep-pairs.scala b/tests/neg-custom-args/captures/sep-pairs.scala
index 582c635ce27d..298dc2e563c1 100644
--- a/tests/neg-custom-args/captures/sep-pairs.scala
+++ b/tests/neg-custom-args/captures/sep-pairs.scala
@@ -29,8 +29,7 @@ def twoRefs2(): SamePair[Ref^] =
   r3
 
 def twoRefsBad(): Pair[Ref^, Ref^] =
-  Pair(Ref(), Ref()) // error // error: universal capability cannot be included in capture set
-                     // but should work since this is morally equivalent to `twoRefs`
+  Pair(Ref(), Ref()) // ok now
 
 def test(io: Object^): Unit =
   val two = twoRefs()
diff --git a/tests/neg-custom-args/captures/sep-use.check b/tests/neg-custom-args/captures/sep-use.check
index 64e2bd7800bc..5d8636007fdc 100644
--- a/tests/neg-custom-args/captures/sep-use.check
+++ b/tests/neg-custom-args/captures/sep-use.check
@@ -4,6 +4,8 @@
   |          Separation failure: Illegal access to {io} which is hidden by the previous definition
   |          of value x with type () => Unit.
   |          This type hides capabilities  {io}
+  |
+  |          where:    => refers to a fresh root capability in the type of value x
 -- Error: tests/neg-custom-args/captures/sep-use.scala:12:12 -----------------------------------------------------------
 12 |  def x: () => Unit = () => println(io)  // error
    |         ^^^^^^^^^^
@@ -14,6 +16,8 @@
    |          Separation failure: Illegal access to {io} which is hidden by the previous definition
    |          of method x with result type () => Unit.
    |          This type hides capabilities  {io}
+   |
+   |          where:    => refers to a fresh root capability in the result type of method x
 -- Error: tests/neg-custom-args/captures/sep-use.scala:18:10 -----------------------------------------------------------
 18 |  def xx: (y: Int) => Unit = _ => println(io)  // error
    |          ^^^^^^^^^^^^^^^^
@@ -24,6 +28,8 @@
    |          Separation failure: Illegal access to {io} which is hidden by the previous definition
    |          of method xx with result type (y: Int) => Unit.
    |          This type hides capabilities  {io}
+   |
+   |          where:    => refers to a fresh root capability in the result type of method xx
 -- Error: tests/neg-custom-args/captures/sep-use.scala:24:19 -----------------------------------------------------------
 24 |  def xxx(y: Int): Object^ = io  // error
    |                   ^^^^^^^
@@ -34,3 +40,5 @@
    |          Separation failure: Illegal access to {io} which is hidden by the previous definition
    |          of method xxx with result type Object^.
    |          This type hides capabilities  {io}
+   |
+   |          where:    ^ refers to a fresh root capability in the result type of method xxx
diff --git a/tests/neg-custom-args/captures/sep-use2.check b/tests/neg-custom-args/captures/sep-use2.check
index a8e3aa884fd5..7dfdfaf1e498 100644
--- a/tests/neg-custom-args/captures/sep-use2.check
+++ b/tests/neg-custom-args/captures/sep-use2.check
@@ -8,6 +8,8 @@
    |        Separation failure: Illegal access to {c} which is hidden by the previous definition
    |        of method cc with result type Object^.
    |        This type hides capabilities  {c}
+   |
+   |        where:    ^ refers to a fresh root capability in the result type of method cc
 -- Error: tests/neg-custom-args/captures/sep-use2.scala:12:10 ----------------------------------------------------------
 12 |  val x4: Object^ = // error
    |          ^^^^^^^
@@ -18,48 +20,43 @@
    |          ^^^^^^^
    |          Separation failure: method cc's result type Object^ hides non-local parameter c
 -- Error: tests/neg-custom-args/captures/sep-use2.scala:18:6 -----------------------------------------------------------
-18 |    { f(cc) } // error // error
+18 |    { f(cc) } // error
    |      ^
    |      Separation failure: Illegal access to {c} which is hidden by the previous definition
    |      of method cc with result type Object^.
    |      This type hides capabilities  {c}
--- Error: tests/neg-custom-args/captures/sep-use2.scala:18:8 -----------------------------------------------------------
-18 |    { f(cc) } // error // error
-   |        ^^
-   |        Separation failure: argument of type  (cc : -> Object^)
-   |        to a function of type (x: Object^) ->{c} Object^
-   |        corresponds to capture-polymorphic formal parameter x of type  Object^
-   |        and hides capabilities  {cap, c}.
-   |        Some of these overlap with the captures of the function prefix.
    |
-   |          Hidden set of current argument        : {cap, c}
-   |          Hidden footprint of current argument  : {c}
-   |          Capture set of function prefix        : {f}
-   |          Footprint set of function prefix      : {f, c}
-   |          The two sets overlap at               : {c}
+   |      where:    ^ refers to a fresh root capability in the result type of method cc
 -- Error: tests/neg-custom-args/captures/sep-use2.scala:20:6 -----------------------------------------------------------
 20 |    { f(c) } // error // error
    |      ^
    |      Separation failure: Illegal access to {c} which is hidden by the previous definition
    |      of method cc with result type Object^.
    |      This type hides capabilities  {c}
+   |
+   |      where:    ^ refers to a fresh root capability in the result type of method cc
 -- Error: tests/neg-custom-args/captures/sep-use2.scala:20:8 -----------------------------------------------------------
 20 |    { f(c) } // error // error
    |        ^
    |        Separation failure: Illegal access to {c} which is hidden by the previous definition
    |        of method cc with result type Object^.
    |        This type hides capabilities  {c}
+   |
+   |        where:    ^ refers to a fresh root capability in the result type of method cc
 -- Error: tests/neg-custom-args/captures/sep-use2.scala:24:8 -----------------------------------------------------------
 24 |    { f(c) } // error
    |        ^
-   |        Separation failure: argument of type  (c : Object^)
-   |        to a function of type Object^ ->{c} Object^
-   |        corresponds to capture-polymorphic formal parameter v1 of type  Object^
-   |        and hides capabilities  {c}.
-   |        Some of these overlap with the captures of the function prefix.
+   |Separation failure: argument of type  (c : Object^)
+   |to a function of type Object^ ->{c} Object^
+   |corresponds to capture-polymorphic formal parameter v1 of type  Object^²
+   |and hides capabilities  {c}.
+   |Some of these overlap with the captures of the function prefix.
+   |
+   |  Hidden set of current argument        : {c}
+   |  Hidden footprint of current argument  : {c}
+   |  Capture set of function prefix        : {f}
+   |  Footprint set of function prefix      : {f, c}
+   |  The two sets overlap at               : {c}
    |
-   |          Hidden set of current argument        : {c}
-   |          Hidden footprint of current argument  : {c}
-   |          Capture set of function prefix        : {f}
-   |          Footprint set of function prefix      : {f, c}
-   |          The two sets overlap at               : {c}
+   |where:    ^  refers to a fresh root capability in the type of parameter c
+   |          ^² refers to a fresh root capability created in value x4 when checking argument to parameter v1 of method apply
diff --git a/tests/neg-custom-args/captures/sep-use2.scala b/tests/neg-custom-args/captures/sep-use2.scala
index a31fb098a719..fcebc5f5b5ed 100644
--- a/tests/neg-custom-args/captures/sep-use2.scala
+++ b/tests/neg-custom-args/captures/sep-use2.scala
@@ -15,7 +15,7 @@ def test1(@consume c: Object^, f: (x: Object^) => Object^) =
 def test2(@consume c: Object^, f: (x: Object^) ->{c} Object^) =
   def cc: Object^ = c // error
   val x1 =
-    { f(cc) } // error // error
+    { f(cc) } // error
   val x4: Object^ = // ^ hides just c, since the Object^ in the result of `f` is existential
     { f(c) } // error // error
 
diff --git a/tests/neg-custom-args/captures/sepchecks2.check b/tests/neg-custom-args/captures/sepchecks2.check
index 47a80306f3b7..bb1c2bcaa0bd 100644
--- a/tests/neg-custom-args/captures/sepchecks2.check
+++ b/tests/neg-custom-args/captures/sepchecks2.check
@@ -4,27 +4,34 @@
    |          Separation failure: Illegal access to {c} which is hidden by the previous definition
    |          of value xs with type List[box () => Unit].
    |          This type hides capabilities  {c}
+   |
+   |          where:    => refers to a fresh root capability in the type of value xs
 -- Error: tests/neg-custom-args/captures/sepchecks2.scala:13:7 ---------------------------------------------------------
 13 |  foo((() => println(c)) :: Nil, c) // error
    |       ^^^^^^^^^^^^^^^^^^^^^^^^
-   |       Separation failure: argument of type  List[box () ->{c} Unit]
-   |       to method foo: (xs: List[box () => Unit], y: Object^): Nothing
-   |       corresponds to capture-polymorphic formal parameter xs of type  List[box () => Unit]
-   |       and hides capabilities  {c}.
-   |       Some of these overlap with the captures of the second argument with type  (c : Object^).
+   |Separation failure: argument of type  List[box () ->{c} Unit]
+   |to method foo: (xs: List[box () => Unit], y: Object^): Nothing
+   |corresponds to capture-polymorphic formal parameter xs of type  List[box () => Unit]
+   |and hides capabilities  {c}.
+   |Some of these overlap with the captures of the second argument with type  (c : Object^).
+   |
+   |  Hidden set of current argument        : {c}
+   |  Hidden footprint of current argument  : {c}
+   |  Capture set of second argument        : {c}
+   |  Footprint set of second argument      : {c}
+   |  The two sets overlap at               : {c}
    |
-   |         Hidden set of current argument        : {c}
-   |         Hidden footprint of current argument  : {c}
-   |         Capture set of second argument        : {c}
-   |         Footprint set of second argument      : {c}
-   |         The two sets overlap at               : {c}
+   |where:    => refers to a fresh root capability created in method Test2 when checking argument to parameter xs of method foo
 -- Error: tests/neg-custom-args/captures/sepchecks2.scala:14:10 --------------------------------------------------------
 14 |  val x1: (Object^, Object^) = (c, c) // error
    |          ^^^^^^^^^^^^^^^^^^
-   |          Separation failure in value x1's type (box Object^, box Object^).
+   |          Separation failure in value x1's type (box Object^, box Object^²).
    |          One part,  box Object^, hides capabilities  {c}.
-   |          Another part,  box Object^,  captures capabilities  {c}.
+   |          Another part,  box Object^²,  captures capabilities  {c}.
    |          The two sets overlap at  {c}.
+   |
+   |          where:    ^  refers to a fresh root capability in the type of value x1
+   |                    ^² refers to a fresh root capability in the type of value x1
 -- Error: tests/neg-custom-args/captures/sepchecks2.scala:15:10 --------------------------------------------------------
 15 |  val x2: (Object^, Object^{d}) = (d, d) // error
    |          ^^^^^^^^^^^^^^^^^^^^^
@@ -32,13 +39,18 @@
    |          One part,  box Object^, hides capabilities  {d}.
    |          Another part,  box Object^{d},  captures capabilities  {d}.
    |          The two sets overlap at  {d}.
+   |
+   |          where:    ^ refers to a fresh root capability in the type of value x2
 -- Error: tests/neg-custom-args/captures/sepchecks2.scala:27:6 ---------------------------------------------------------
 27 |  bar((c, c)) // error
    |      ^^^^^^
-   |      Separation failure in the argument's adapted type (box Object^, box Object^).
-   |      One part,  box Object^, hides capabilities  {c}.
-   |      Another part,  box Object^,  captures capabilities  {c}.
-   |      The two sets overlap at  {c}.
+   |Separation failure in the argument's adapted type (box Object^, box Object^²).
+   |One part,  box Object^, hides capabilities  {c}.
+   |Another part,  box Object^²,  captures capabilities  {c}.
+   |The two sets overlap at  {c}.
+   |
+   |where:    ^  refers to a fresh root capability created in method Test6 when checking argument to parameter x of method bar
+   |          ^² refers to a fresh root capability created in method Test6 when checking argument to parameter x of method bar
 -- Error: tests/neg-custom-args/captures/sepchecks2.scala:30:9 ---------------------------------------------------------
 30 |  val x: (Object^, Object^{c}) = (d, c) // error
    |         ^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/neg-custom-args/captures/sepchecks4.check b/tests/neg-custom-args/captures/sepchecks4.check
index 5934be1ff637..7b587363d1cd 100644
--- a/tests/neg-custom-args/captures/sepchecks4.check
+++ b/tests/neg-custom-args/captures/sepchecks4.check
@@ -11,14 +11,16 @@
 -- Error: tests/neg-custom-args/captures/sepchecks4.scala:12:6 ---------------------------------------------------------
 12 |  par(() => println(io))(() => println(io)) // error // (1)
    |      ^^^^^^^^^^^^^^^^^
-   |      Separation failure: argument of type  () ->{io} Unit
-   |      to method par: (op1: () => Unit)(op2: () => Unit): Unit
-   |      corresponds to capture-polymorphic formal parameter op1 of type  () => Unit
-   |      and hides capabilities  {io}.
-   |      Some of these overlap with the captures of the second argument with type  () ->{io} Unit.
+   |Separation failure: argument of type  () ->{io} Unit
+   |to method par: (op1: () => Unit)(op2: () => Unit): Unit
+   |corresponds to capture-polymorphic formal parameter op1 of type  () => Unit
+   |and hides capabilities  {io}.
+   |Some of these overlap with the captures of the second argument with type  () ->{io} Unit.
    |
-   |        Hidden set of current argument        : {io}
-   |        Hidden footprint of current argument  : {io}
-   |        Capture set of second argument        : {io}
-   |        Footprint set of second argument      : {io}
-   |        The two sets overlap at               : {io}
+   |  Hidden set of current argument        : {io}
+   |  Hidden footprint of current argument  : {io}
+   |  Capture set of second argument        : {io}
+   |  Footprint set of second argument      : {io}
+   |  The two sets overlap at               : {io}
+   |
+   |where:    => refers to a fresh root capability created in method test when checking argument to parameter op1 of method par
diff --git a/tests/neg-custom-args/captures/sepchecks5.check b/tests/neg-custom-args/captures/sepchecks5.check
index aae5cb89da53..63ec3bc73431 100644
--- a/tests/neg-custom-args/captures/sepchecks5.check
+++ b/tests/neg-custom-args/captures/sepchecks5.check
@@ -14,3 +14,5 @@
    |                        Separation failure: Illegal access to (io : Object^), which was passed to a
    |                        @consume parameter or was used as a prefix to a @consume method on line 19
    |                        and therefore is no longer available.
+   |
+   |                        where:    ^ refers to a fresh root capability in the type of parameter io
diff --git a/tests/neg-custom-args/captures/shared-capability.check b/tests/neg-custom-args/captures/shared-capability.check
index 64fb3eb39d44..15355a9fc5b9 100644
--- a/tests/neg-custom-args/captures/shared-capability.check
+++ b/tests/neg-custom-args/captures/shared-capability.check
@@ -2,3 +2,5 @@
 9 |def test2(a: Async^): Object^ = a // error
   |             ^^^^^^
   |             Async^ extends SharedCapability, so it cannot capture `cap`
+  |
+  |             where:    ^ refers to the universal root capability
diff --git a/tests/neg-custom-args/captures/simple-using.check b/tests/neg-custom-args/captures/simple-using.check
index e46b9e50b58d..6e32260d3322 100644
--- a/tests/neg-custom-args/captures/simple-using.check
+++ b/tests/neg-custom-args/captures/simple-using.check
@@ -1,10 +1,14 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/simple-using.scala:8:15 ----------------------------------
 8 |  usingLogFile { f => () => f.write(2) } // error
   |               ^^^^^^^^^^^^^^^^^^^^^^^^^
-  |               Found:    (f: java.io.FileOutputStream^) ->? box () ->{f} Unit
-  |               Required: (f: java.io.FileOutputStream^) ->{fresh} box () ->? Unit
+  |Found:    (f: java.io.FileOutputStream^) ->? box () ->{f} Unit
+  |Required: (f: java.io.FileOutputStream^) => box () ->? Unit
   |
-  |               Note that reference f.type
-  |               cannot be included in outer capture set ?
+  |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 ?
   |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index 9cd40a8bc8c4..7f420872eb25 100644
--- a/tests/neg-custom-args/captures/try.check
+++ b/tests/neg-custom-args/captures/try.check
@@ -3,11 +3,17 @@
    |                            ^^^^^^^^^^^^^^^^^^^
    |                            Type variable R of method handle cannot be instantiated to box CT[Exception]^ since
    |                            that type captures the root capability `cap`.
+   |
+   |                            where:    ^ refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:23:49 ------------------------------------------
 23 |  val a = handle[Exception, CanThrow[Exception]] { // error // error
    |                                                 ^
-   |                                               Found:    (x: CT[Exception]^) ->? box CT[Exception]^{x}
-   |                                               Required: (x: CT[Exception]^) ->{fresh} box CT[Exception]^{fresh}
+   |Found:    (x: CT[Exception]^) ->? box CT[Exception]^{x}
+   |Required: (x: CT[Exception]^) => box CT[Exception]^²
+   |
+   |where:    => refers to a fresh root capability created in value a when checking argument to parameter op of method handle
+   |          ^  refers to the universal root capability
+   |          ^² refers to a fresh root capability created in value a when checking argument to parameter op of method handle
 24 |    (x: CanThrow[Exception]) => x
 25 |  }{
    |
@@ -15,8 +21,11 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:43 ------------------------------------------
 29 |  val b = handle[Exception, () -> Nothing] { // error
    |                                           ^
-   |                                           Found:    (x: CT[Exception]^) ->? () ->{x} Nothing
-   |                                           Required: (x: CT[Exception]^) ->{fresh} () -> Nothing
+   |Found:    (x: CT[Exception]^) ->? () ->{x} Nothing
+   |Required: (x: CT[Exception]^) => () -> Nothing
+   |
+   |where:    => refers to a fresh root capability created in value b when checking argument to parameter op of method handle
+   |          ^  refers to the universal root capability
 30 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
 31 |  } {
    |
@@ -24,11 +33,15 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:35:18 ------------------------------------------
 35 |  val xx = handle {  // error
    |                  ^
-   |                  Found:    (x: CT[Exception]^) ->? box () ->{x} Int
-   |                  Required: (x: CT[Exception]^) ->{fresh} box () ->? Int
+   |Found:    (x: CT[Exception]^) ->? box () ->{x} Int
+   |Required: (x: CT[Exception]^) => box () ->? Int
+   |
+   |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 ?
+   |
+   |Note that reference x.type
+   |cannot be included in outer capture set ?
 36 |    (x: CanThrow[Exception]) =>
 37 |      () =>
 38 |        raise(new Exception)(using x)
@@ -39,11 +52,15 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:47:31 ------------------------------------------
 47 |val global: () -> Int = handle { // error
    |                               ^
-   |                               Found:    (x: CT[Exception]^) ->? box () ->{x} Int
-   |                               Required: (x: CT[Exception]^) ->{fresh} box () ->? Int
+   |Found:    (x: CT[Exception]^) ->? box () ->{x} Int
+   |Required: (x: CT[Exception]^) => box () ->? Int
+   |
+   |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 ?
+   |Note that reference x.type
+   |cannot be included in outer capture set ?
 48 |  (x: CanThrow[Exception]) =>
 49 |    () =>
 50 |      raise(new Exception)(using x)
diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check
index f21d1403eb3d..0e9acbea1afa 100644
--- a/tests/neg-custom-args/captures/unsound-reach-4.check
+++ b/tests/neg-custom-args/captures/unsound-reach-4.check
@@ -3,17 +3,24 @@
    |                  ^^^^^^^^^^
    |                  Type variable X of trait Foo cannot be instantiated to File^ since
    |                  that type captures the root capability `cap`.
+   |
+   |                  where:    ^ refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach-4.scala:20:29 ------------------------------
 20 |  val backdoor: Foo[File^] = new Bar // error (follow-on, since the parent Foo[File^] of bar is illegal).
    |                             ^^^^^^^
    |                             Found:    Bar^?
    |                             Required: Foo[box File^]
    |
+   |                             where:    ^ refers to a fresh root capability in the type of value backdoor
+   |
    | longer explanation available when compiling with `-explain`
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach-4.scala:17:6 ---------------------------------
 17 |  def use(@consume x: F): File^ = x // error @consume override
    |      ^
    |      error overriding method use in trait Foo of type (x: File^): box File^;
-   |        method use of type (x: File^): File^ has incompatible type
+   |        method use of type (x: File^): File^² has incompatible type
+   |
+   |      where:    ^  refers to the universal root capability
+   |                ^² refers to a root capability associated with the result type of (x: File^): File^²
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/unsound-reach-6.check b/tests/neg-custom-args/captures/unsound-reach-6.check
index ed81271efa90..2afe9ba0e1dd 100644
--- a/tests/neg-custom-args/captures/unsound-reach-6.check
+++ b/tests/neg-custom-args/captures/unsound-reach-6.check
@@ -25,4 +25,4 @@
 -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 ---------------------------------------------------
 19 |    val z = f(ys)  // error @consume failure
    |              ^^
-   |Separation failure: argument to @consume parameter with type (ys : -> List[box () ->{io} Unit]) refers to non-local parameter io
+   |Separation failure: argument to @consume parameter with type List[box () ->{io} Unit] refers to non-local parameter io
diff --git a/tests/neg-custom-args/captures/unsound-reach.check b/tests/neg-custom-args/captures/unsound-reach.check
index a1ebd30e4915..f8ddb725598d 100644
--- a/tests/neg-custom-args/captures/unsound-reach.check
+++ b/tests/neg-custom-args/captures/unsound-reach.check
@@ -3,15 +3,21 @@
   |                  ^^^^^^^^^^
   |                  Type variable X of trait Foo cannot be instantiated to File^ since
   |                  that type captures the root capability `cap`.
+  |
+  |                  where:    ^ refers to the universal root capability
 -- Error: tests/neg-custom-args/captures/unsound-reach.scala:14:19 -----------------------------------------------------
 14 |class Bar2 extends Foo2[File^]: // error
    |                   ^
    |                   Type variable X of constructor Foo2 cannot be instantiated to box File^ since
    |                   that type captures the root capability `cap`.
+   |
+   |                   where:    ^ refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach.scala:18:31 --------------------------------
 18 |    val backdoor: Foo[File^] = new Bar   // error (follow-on, since the parent Foo[File^] of bar is illegal).
    |                               ^^^^^^^
    |                               Found:    Bar^?
    |                               Required: Foo[box File^]
    |
+   |                               where:    ^ refers to a fresh root capability in the type of value backdoor
+   |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/usingLogFile.check b/tests/neg-custom-args/captures/usingLogFile.check
index 1c77435685c7..86ddcb17312d 100644
--- a/tests/neg-custom-args/captures/usingLogFile.check
+++ b/tests/neg-custom-args/captures/usingLogFile.check
@@ -1,40 +1,56 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:22:27 ---------------------------------
 22 |  val later = usingLogFile { f => () => f.write(0) } // error
    |                           ^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                           Found:    (f: java.io.FileOutputStream^) ->? box () ->{f} Unit
-   |                           Required: (f: java.io.FileOutputStream^) ->{fresh} box () ->? Unit
+   |Found:    (f: java.io.FileOutputStream^) ->? box () ->{f} Unit
+   |Required: (f: java.io.FileOutputStream^) => box () ->? Unit
    |
-   |                           Note that reference f.type
-   |                           cannot be included in outer capture set ?
+   |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 ?
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:27:36 ---------------------------------
 27 |  private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error
    |                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                            Found:    (f: java.io.FileOutputStream^) ->? box Test2.Cell[box () ->{f} Unit]^?
-   |                            Required: (f: java.io.FileOutputStream^) ->{fresh} box Test2.Cell[box () ->? Unit]^?
+   |Found:    (f: java.io.FileOutputStream^) ->? box Test2.Cell[box () ->{f} Unit]^?
+   |Required: (f: java.io.FileOutputStream^) => box Test2.Cell[box () ->? Unit]^?
+   |
+   |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 ?
+   |Note that reference f.type
+   |cannot be included in outer capture set ?
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:43:33 ---------------------------------
 43 |    val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
    |                                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                                 Found:    (f: java.io.OutputStream^) ->? box Int ->{f} Unit
-   |                                 Required: (f: java.io.OutputStream^) ->{fresh} box Int ->? Unit
+   |Found:    (f: java.io.OutputStream^) ->? box Int ->{f} Unit
+   |Required: (f: java.io.OutputStream^) => box Int ->? Unit
    |
-   |                                 Note that reference f.type
-   |                                 cannot be included in outer capture set ?
+   |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 ?
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:52:6 ----------------------------------
 52 |      usingLogger(_, l => () => l.log("test")))  // error after checking mapping scheme
    |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |      Found:    (_$1: java.io.OutputStream^) ->? box () ->{_$1} Unit
-   |      Required: (_$1: java.io.OutputStream^) ->{fresh} box () ->? Unit
+   |Found:    (_$1: java.io.OutputStream^) ->? box () ->{_$1} Unit
+   |Required: (_$1: java.io.OutputStream^) => box () ->? Unit
+   |
+   |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 ?
+   |Note that reference _$1.type
+   |cannot be included in outer capture set ?
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/vars-simple.check b/tests/neg-custom-args/captures/vars-simple.check
index 71fab0dcf7d2..5f5c6c365638 100644
--- a/tests/neg-custom-args/captures/vars-simple.check
+++ b/tests/neg-custom-args/captures/vars-simple.check
@@ -4,6 +4,8 @@
    |         Found:    String => String
    |         Required: String ->{cap1, cap2} String
    |
+   |         where:    => refers to a fresh root capability created in method scope
+   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars-simple.scala:16:8 -----------------------------------
 16 |    a = g  // error
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
index fae2645fcb8b..d8b55afd298c 100644
--- a/tests/neg-custom-args/captures/vars.check
+++ b/tests/neg-custom-args/captures/vars.check
@@ -25,6 +25,9 @@
    |        Found:    (cap3: CC^) ->? box String ->{cap3} String
    |        Required: (cap3: CC^) -> box String ->? String
    |
+   |        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/neg-custom-args/captures/widen-reach.check b/tests/neg-custom-args/captures/widen-reach.check
index e2028941a009..a8148e02bad1 100644
--- a/tests/neg-custom-args/captures/widen-reach.check
+++ b/tests/neg-custom-args/captures/widen-reach.check
@@ -3,11 +3,16 @@
   |                  ^^^^^^^^
   |                  Type variable T of trait Foo cannot be instantiated to IO^ since
   |                  that type captures the root capability `cap`.
+  |
+  |                  where:    ^ refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:9:24 -----------------------------------
 9 |  val foo: IO^ -> IO^ = x => x // error // error
   |                        ^^^^^^
   |                        Found:    (x: IO^) ->? IO^{x}
-  |                        Required: (x: IO^) -> IO^{fresh}
+  |                        Required: (x: IO^) -> IO^²
+  |
+  |                        where:    ^  refers to the universal root capability
+  |                                  ^² refers to a fresh root capability in the type of value foo
   |
   | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 -------------------------------------------------------
@@ -24,6 +29,9 @@
 9 |  val foo: IO^ -> IO^ = x => x // error // error
   |      ^
   |      error overriding value foo in trait Foo of type IO^ -> box IO^;
-  |        value foo of type IO^ -> IO^ has incompatible type
+  |        value foo of type IO^ -> IO^² has incompatible type
+  |
+  |      where:    ^  refers to the universal root capability
+  |                ^² refers to a fresh root capability in the type of value foo
   |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/withFile.scala b/tests/neg-custom-args/captures/withFile.scala
index b8cdf96f9143..8e287d8631ba 100644
--- a/tests/neg-custom-args/captures/withFile.scala
+++ b/tests/neg-custom-args/captures/withFile.scala
@@ -1,10 +1,19 @@
-import java.io.*
 object Test2:
+  class File:
+    def write(): Unit = ()
+    def close(): Unit = ()
+  class Box[+T](x: T)
 
-  def usingLogFile[T](op: FileOutputStream^ => T): T =
-    val logFile = FileOutputStream("log")
+  def usingLogFile[T](op: File^ => T): T =
+    val logFile = File()
     val result = op(logFile)
     logFile.close()
     result
 
-  private val later = usingLogFile { f => () => f.write(0) } // error
+
+  private val later1 = usingLogFile { f => () => f.write() } // error
+  private val later2 = usingLogFile { f => Box(f) } // error
+  private val later3 = usingLogFile[() => Unit]: // error
+    f => () => f.write() // error
+  private val later4 = usingLogFile[Box[File^]]: // error
+    f => Box(f) // error
diff --git a/tests/neg/abstract-givens.check b/tests/neg/abstract-givens.check
index 1430c5b6e950..51f50db266c2 100644
--- a/tests/neg/abstract-givens.check
+++ b/tests/neg/abstract-givens.check
@@ -10,7 +10,10 @@
 -- [E164] Declaration Error: tests/neg/abstract-givens.scala:9:8 -------------------------------------------------------
 9 |  given z[T](using T): Seq[T] = List(summon[T]) // error
   |        ^
-  |        error overriding given instance z in trait T of type [T](using x$1: T): List[T];
+  |        error overriding given instance z in trait T² of type [T](using x$1: T): List[T];
   |          given instance z of type [T](using x$1: T): Seq[T] has incompatible type
   |
+  |        where:    T  is a type variable
+  |                  T² is a trait in the empty package
+  |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/pos-custom-args/captures/capt-capability.scala b/tests/pos-custom-args/captures/capt-capability.scala
index 03b5cb1bbabf..d82f78263d18 100644
--- a/tests/pos-custom-args/captures/capt-capability.scala
+++ b/tests/pos-custom-args/captures/capt-capability.scala
@@ -1,4 +1,4 @@
-import caps.Capability
+import caps.{Capability, SharedCapability}
 
 def f1(c: Capability): () ->{c} c.type = () => c // ok
 
@@ -14,7 +14,7 @@ def f3: Int =
   x
 
 def foo() =
-  val x: Capability = ???
+  val x: SharedCapability = ???
   val y: Capability = x
   val x2: () ->{x} Capability = ???
   val y2: () ->{x} Capability = x2
@@ -22,7 +22,10 @@ def foo() =
   val z1: () => Capability = f1(x)
   def h[X](a: X)(b: X) = a
 
-  val z2 =
-    if x == null then () => x else () => new Capability() {}
+  val z2: (y: Unit) ->{x} Capability^ =
+    if x == null then (y: Unit) => x else (y: Unit) => new Capability() {}
+  // z2's type cannot be inferred, see neg test
+  //val z3 =
+  //  if x == null then (y: Unit) => x else (y: Unit) => new Capability() {}
   val _ = x
 
diff --git a/tests/pos-custom-args/captures/rinaudo.scala b/tests/pos-custom-args/captures/rinaudo.scala
new file mode 100644
index 000000000000..7091f8e94d6d
--- /dev/null
+++ b/tests/pos-custom-args/captures/rinaudo.scala
@@ -0,0 +1,12 @@
+import language.experimental.captureChecking
+import caps.*
+
+trait FileSystem extends Capability:
+  def print(msg: String): Unit
+
+class Logger(using fs: FileSystem):
+    def info(msg: String): Unit = fs.print(msg)
+
+def log(msg: String): FileSystem ?-> Unit =
+  val l = new Logger
+  l.info(msg)
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/skolems2.scala b/tests/pos-custom-args/captures/skolems2.scala
index a9ff6e258317..53fbe935e362 100644
--- a/tests/pos-custom-args/captures/skolems2.scala
+++ b/tests/pos-custom-args/captures/skolems2.scala
@@ -13,6 +13,17 @@ def Test(@consume c: Object^, @consume f: Object^ => Object^) =
   val x4: Object^ =
     { unsafeAssumeSeparate(f)(cc) }
 
+def Test2(@consume c: Object^, @consume f: Object^ => Object^) =
+  def cc(): Object^ = unsafeAssumeSeparate(c)
+  val x1 =
+    { f(cc()) }
+  val x2 =
+    f(cc())
+  val x3: Object^ =
+    f(cc())
+  val x4: Object^ =
+    { unsafeAssumeSeparate(f)(cc()) }
+