diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index b52b52ba8b1a..55e7762a9269 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -198,7 +198,7 @@ object Capabilities:
       i"a fresh root capability$classifierStr$originStr"
 
   object FreshCap:
-    def apply(origin: Origin)(using Context): FreshCap | GlobalCap.type =
+    def apply(origin: Origin)(using Context): FreshCap =
       FreshCap(ctx.owner, origin)
 
   /** A root capability associated with a function type. These are conceptually
@@ -837,6 +837,7 @@ object Capabilities:
     case Formal(pref: ParamRef, app: tpd.Apply)
     case ResultInstance(methType: Type, meth: Symbol)
     case UnapplyInstance(info: MethodType)
+    case LocalInstance(restpe: Type)
     case NewMutable(tp: Type)
     case NewCapability(tp: Type)
     case LambdaExpected(respt: Type)
@@ -865,6 +866,8 @@ object Capabilities:
         i" when instantiating $methDescr$mt"
       case UnapplyInstance(info) =>
         i" when instantiating argument of unapply with type $info"
+      case LocalInstance(restpe) =>
+        i" when instantiating expected result type $restpe of function literal"
       case NewMutable(tp) =>
         i" when constructing mutable $tp"
       case NewCapability(tp) =>
@@ -948,6 +951,69 @@ object Capabilities:
   def freshToCap(param: Symbol, tp: Type)(using Context): Type =
     CapToFresh(Origin.Parameter(param)).inverse(tp)
 
+  /** The local dual of a result type of a closure type.
+   *  @param binder  the method type of the anonymous function whose result is mapped
+   *  @pre           the context's owner is the anonymous function
+   */
+  class Internalize(binder: MethodType)(using Context) extends BiTypeMap:
+    thisMap =>
+
+    val sym = ctx.owner
+    assert(sym.isAnonymousFunction)
+    val paramSyms = atPhase(ctx.phase.prev):
+      // We need to ask one phase before since `sym` should not be completed as a side effect.
+      // The result of Internalize is used to se the result type of an anonymous function, and
+      // the new info of that function is built with the result.
+      sym.paramSymss.head
+    val resultToFresh = EqHashMap[ResultCap, FreshCap]()
+    val freshToResult = EqHashMap[FreshCap, ResultCap]()
+
+    override def apply(t: Type) =
+      if variance < 0 then t
+      else t match
+        case t: ParamRef =>
+          if t.binder == this.binder then paramSyms(t.paramNum).termRef else t
+        case _ => mapOver(t)
+
+    override def mapCapability(c: Capability, deep: Boolean): Capability = c match
+      case r: ResultCap if r.binder == this.binder =>
+        resultToFresh.get(r) match
+          case Some(f) => f
+          case None =>
+            val f = FreshCap(Origin.LocalInstance(binder.resType))
+            resultToFresh(r) = f
+            freshToResult(f) = r
+            f
+      case _ =>
+        super.mapCapability(c, deep)
+
+    class Inverse extends BiTypeMap:
+      def apply(t: Type): Type =
+        if variance < 0 then t
+        else t match
+          case t: TermRef if paramSyms.contains(t) =>
+            binder.paramRefs(paramSyms.indexOf(t.symbol))
+          case _ => mapOver(t)
+
+      override def mapCapability(c: Capability, deep: Boolean): Capability = c match
+        case f: FreshCap if f.owner == sym =>
+          freshToResult.get(f) match
+            case Some(r) => r
+            case None =>
+              val r = ResultCap(binder)
+              resultToFresh(r) = f
+              freshToResult(f) = r
+              r
+        case _ => super.mapCapability(c, deep)
+
+      def inverse = thisMap
+      override def toString = thisMap.toString + ".inverse"
+    end Inverse
+
+    override def toString = "InternalizeClosureResult"
+    def inverse = Inverse()
+  end Internalize
+
   /** Map top-level free existential variables one-to-one to Fresh instances */
   def resultToFresh(tp: Type, origin: Origin)(using Context): Type =
     val subst = new TypeMap:
@@ -977,78 +1043,76 @@ object Capabilities:
     subst(tp)
   end resultToFresh
 
-  /** Replace all occurrences of `cap` (or fresh) in parts of this type by an existentially bound
-   *  variable bound by `mt`.
-   *  Stop at function or method types since these have been mapped before.
-   */
-  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
-        case t @ FunctionOrMethod(args, res) if variance > 0 && !t.isAliasFun =>
-          t // `t` should be mapped in this case by a different call to `toResult`. See [[toResultInResults]].
-        case t: (LazyRef | TypeVar) =>
-          mapConserveSuper(t)
-        case _ =>
-          super.mapOver(t)
+  abstract class CapMap(using Context) extends BiTypeMap:
+    override def mapOver(t: Type): Type = t match
+      case t @ FunctionOrMethod(args, res) if variance > 0 && !t.isAliasFun =>
+        t // `t` should be mapped in this case by a different call to `toResult`. See [[toResultInResults]].
+      case t: (LazyRef | TypeVar) =>
+        mapConserveSuper(t)
+      case _ =>
+        super.mapOver(t)
+
+  class ToResult(localResType: Type, mt: MethodicType, fail: Message => Unit)(using Context) extends CapMap:
+
+    def apply(t: Type) = t match
+      case defn.FunctionNOf(args, res, contextual) if t.typeSymbol.name.isImpureFunction =>
+        if variance > 0 then
+          super.mapOver:
+            defn.FunctionNOf(args, res, contextual)
+              .capturing(ResultCap(mt).singletonCaptureSet)
+        else mapOver(t)
+      case _ =>
+        mapOver(t)
+
+    override def mapCapability(c: Capability, deep: Boolean) = c match
+      case c: (FreshCap | GlobalCap.type) =>
+        if variance > 0 then
+          val res = ResultCap(mt)
+          c match
+            case c: FreshCap => res.setOrigin(c)
+            case _ =>
+          res
+        else
+          if variance == 0 then
+            fail(em"""$localResType captures the root capability `cap` in invariant position.
+                      |This capability cannot be converted to an existential in the result type of a function.""")
+          // we accept variance < 0, and leave the cap as it is
+          c
+      case _ =>
+        super.mapCapability(c, deep)
 
-    object toVar extends CapMap:
+      //.showing(i"mapcap $t = $result")
+    override def toString = "toVar"
 
-      def apply(t: Type) = t match
-        case defn.FunctionNOf(args, res, contextual) if t.typeSymbol.name.isImpureFunction =>
-          if variance > 0 then
-            super.mapOver:
-              defn.FunctionNOf(args, res, contextual)
-                .capturing(ResultCap(mt).singletonCaptureSet)
-          else mapOver(t)
-        case _ =>
-          mapOver(t)
+    object inverse extends BiTypeMap:
+      def apply(t: Type) = mapOver(t)
 
       override def mapCapability(c: Capability, deep: Boolean) = c match
-        case c: (FreshCap | GlobalCap.type) =>
-          if variance > 0 then
-            val res = ResultCap(mt)
-            c match
-              case c: FreshCap => res.setOrigin(c)
-              case _ =>
-            res
-          else
-            if variance == 0 then
-              fail(em"""$tp captures the root capability `cap` in invariant position.
-                       |This capability cannot be converted to an existential in the result type of a function.""")
-            // we accept variance < 0, and leave the cap as it is
-            c
+        case c @ ResultCap(`mt`) =>
+          // do a reverse getOrElseUpdate on `seen` to produce the
+          // `Fresh` assosicated with `t`
+          val primary = c.primaryResultCap
+          primary.origin match
+            case GlobalCap =>
+              val fresh = FreshCap(Origin.LocalInstance(mt.resType))
+              primary.setOrigin(fresh)
+              fresh
+            case origin: FreshCap =>
+              origin
         case _ =>
           super.mapCapability(c, deep)
 
-        //.showing(i"mapcap $t = $result")
-      override def toString = "toVar"
-
-      object inverse extends BiTypeMap:
-        def apply(t: Type) = mapOver(t)
-
-        override def mapCapability(c: Capability, deep: Boolean) = c match
-          case c @ ResultCap(`mt`) =>
-            // do a reverse getOrElseUpdate on `seen` to produce the
-            // `Fresh` assosicated with `t`
-            val primary = c.primaryResultCap
-            primary.origin match
-              case GlobalCap =>
-                val fresh = FreshCap(Origin.Unknown)
-                primary.setOrigin(fresh)
-                fresh
-              case origin: FreshCap =>
-                origin
-          case _ =>
-            super.mapCapability(c, deep)
-
-        def inverse = toVar.this
-        override def toString = "toVar.inverse"
-      end inverse
-    end toVar
+      def inverse = ToResult.this
+      override def toString = "toVar.inverse"
+    end inverse
+  end ToResult
 
-    toVar(tp)
-  end toResult
+  /** Replace all occurrences of `cap` (or fresh) in parts of this type by an existentially bound
+   *  variable bound by `mt`.
+   *  Stop at function or method types since these have been mapped before.
+   */
+  def toResult(tp: Type, mt: MethodicType, fail: Message => Unit)(using Context): Type =
+    ToResult(tp, mt, fail)(tp)
 
   /** Map global roots in function results to result roots. Also,
    *  map roots in the types of def methods that are parameterless
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index ca094437800f..2e64e94d4de9 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -10,6 +10,8 @@ import config.Printers.{capt, recheckr, noPrinter}
 import config.{Config, Feature}
 import ast.{tpd, untpd, Trees}
 import Trees.*
+import typer.ForceDegree
+import typer.Inferencing.isFullyDefined
 import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents, OverridingPairsChecker}
 import typer.Checking.{checkBounds, checkAppliedTypesIn}
 import typer.ErrorReporting.{Addenda, NothingToAdd, err}
@@ -25,7 +27,7 @@ import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
 import reporting.{trace, Message, OverrideError}
 import Annotations.Annotation
 import Capabilities.*
-import dotty.tools.dotc.util.common.alwaysTrue
+import util.common.alwaysTrue
 
 /** The capture checker */
 object CheckCaptures:
@@ -916,14 +918,15 @@ class CheckCaptures extends Recheck, SymTransformer:
      *      { def $anonfun(...) = ...; closure($anonfun, ...)}
      */
     override def recheckClosureBlock(mdef: DefDef, expr: Closure, pt: Type)(using Context): Type =
+      val anonfun = mdef.symbol
 
-      def matchParams(paramss: List[ParamClause], pt: Type): Unit =
+      def matchParamsAndResult(paramss: List[ParamClause], pt: Type): Unit =
         //println(i"match $mdef against $pt")
         paramss match
         case params :: paramss1 => pt match
           case defn.PolyFunctionOf(poly: PolyType) =>
             assert(params.hasSameLengthAs(poly.paramInfos))
-            matchParams(paramss1, poly.instantiate(params.map(_.symbol.typeRef)))
+            matchParamsAndResult(paramss1, poly.instantiate(params.map(_.symbol.typeRef)))
           case FunctionOrMethod(argTypes, resType) =>
             assert(params.hasSameLengthAs(argTypes), i"$mdef vs $pt, ${params}")
             for (argType, param) <- argTypes.lazyZip(params) do
@@ -931,36 +934,29 @@ class CheckCaptures extends Recheck, SymTransformer:
               val paramType = freshToCap(param.symbol, paramTpt.nuType)
               checkConformsExpr(argType, paramType, param)
                 .showing(i"compared expected closure formal $argType against $param with ${paramTpt.nuType}", capt)
-            if !pt.isInstanceOf[RefinedType]
-                && !(isEtaExpansion(mdef) && ccConfig.handleEtaExpansionsSpecially)
-            then
-              // If the closure is not an eta expansion and the expected type is a parametric
-              // function type, check whether the closure's result conforms to the expected
-              // result type. This constrains parameter types of the closure which can give better
-              // error messages. It also prevents mapping fresh to result caps in the closure's
-              // result type.
-              // If the closure is an eta expanded method reference it's better to not constrain
-              // its internals early since that would give error messages in generated code
-              // which are less intelligible. An example is the line `a = x` in
-              // 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)
-              capt.println(i"pre-check closure $expr of type ${mdef.tpt.nuType} against $resType")
-              checkConformsExpr(mdef.tpt.nuType, resType, expr)
+            if resType.isValueType && isFullyDefined(resType, ForceDegree.none) then
+              val localResType = pt match
+                case RefinedType(_, _, mt: MethodType) =>
+                  inContext(ctx.withOwner(anonfun)):
+                    Internalize(mt)(resType)
+                case _ => resType
+              mdef.tpt.updNuType(localResType)
+              // Make sure we affect the info of the anonfun by the previous updNuType
+              // unless the info is already defined in a previous phase and does not change.
+              assert(!anonfun.isCompleted || anonfun.denot.validFor.firstPhaseId != thisPhase.id)
+              //println(i"updating ${mdef.tpt} to $localResType/${mdef.tpt.nuType}")
           case _ =>
         case Nil =>
 
-      openClosures = (mdef.symbol, pt) :: openClosures
+      openClosures = (anonfun, pt) :: openClosures
         // openClosures is needed for errors but currently makes no difference
         // TODO follow up on this
       try
-        matchParams(mdef.paramss, pt)
-        capt.println(i"recheck closure block $mdef: ${mdef.symbol.infoOrCompleter}")
-        if !mdef.symbol.isCompleted then
-          mdef.symbol.ensureCompleted() // this will recheck def
-        else
-          recheckDef(mdef, mdef.symbol)
-
+        matchParamsAndResult(mdef.paramss, pt)
+        capt.println(i"recheck closure block $mdef: ${anonfun.infoOrCompleter}")
+        if !anonfun.isCompleted
+        then anonfun.ensureCompleted() // this will recheck def
+        else recheckDef(mdef, anonfun)
         recheckClosure(expr, pt, forceDependent = true)
       finally
         openClosures = openClosures.tail
@@ -1463,7 +1459,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           case FunctionOrMethod(aargs, ares) =>
             val saved = curEnv
             curEnv = Env(
-              curEnv.owner, EnvKind.NestedInOwner,
+              curEnv.owner,
+              if boxed then EnvKind.Boxed else EnvKind.NestedInOwner,
               CaptureSet.Var(curEnv.owner, level = ccState.currentLevel),
               if boxed then null else curEnv)
             try
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 51ccdfe57274..fff8f3e94762 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -165,11 +165,12 @@ abstract class Recheck extends Phase, SymTransformer:
        *  from the current type.
        */
       def setNuType(tpe: Type): Unit =
-        if nuTypes.lookup(tree) == null then updNuType(tpe)
+        if nuTypes.lookup(tree) == null && (tpe ne tree.tpe) then
+          updNuType(tpe)
 
       /** Set new type of the tree unconditionally. */
       def updNuType(tpe: Type): Unit =
-        if tpe ne tree.tpe then nuTypes(tree) = tpe
+        nuTypes(tree) = tpe
 
       /** The new type of the tree, or if none was installed, the original type */
       def nuType(using Context): Type =
diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check
index dc163dc75f6a..0cd908d081ee 100644
--- a/tests/neg-custom-args/captures/capt1.check
+++ b/tests/neg-custom-args/captures/capt1.check
@@ -1,7 +1,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:5:2 ------------------------------------------
 5 |  () => if x == null then y else y  // error
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  |  Found:    () ->{x} C^?
+  |  Found:    () ->{x} C
   |  Required: () -> C
   |  Note that capability (x : C^) is not included in capture set {}.
   |
@@ -52,12 +52,27 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:36:24 ----------------------------------------
 36 |  val z2 = h[() -> Cap](() => x) // error // error
    |                        ^^^^^^^
-   |Found:    () ->{x} C^{x}
-   |Required: () -> C^
+   |Found:    () ->? C^
+   |Required: () -> C^²
+   |
+   |where:    ^  refers to a root capability associated with the result type of (): C^
+   |          ^² refers to a fresh root capability created in value z2 when checking argument to parameter a of method h
+   |
+   |Note that capability <cap of (): C^> is not included in capture set {cap}
+   |because <cap of (): C^> is not visible from cap in value z2.
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:37:5 -----------------------------------------
+37 |    (() => C()) // error
+   |     ^^^^^^^^^
+   |Found:    () ->? C^
+   |Required: () -> C^²
    |
-   |where:    ^ refers to a fresh root capability created in value z2 when checking argument to parameter a of method h
+   |where:    ^  refers to a root capability associated with the result type of (): C^
+   |          ^² refers to a fresh root capability created in value z2 when checking argument to parameter b of method h
    |
-   |Note that capability (x : C^) is not included in capture set {}.
+   |Note that capability <cap of (): C^> is not included in capture set {cap}
+   |because <cap of (): C^> is not visible from cap in value z2.
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/capt1.scala:38:13 -------------------------------------------------------------
diff --git a/tests/neg-custom-args/captures/capt1.scala b/tests/neg-custom-args/captures/capt1.scala
index 7b612363958e..b8df78a869a1 100644
--- a/tests/neg-custom-args/captures/capt1.scala
+++ b/tests/neg-custom-args/captures/capt1.scala
@@ -34,7 +34,7 @@ def foo() =
   def h[X](a: X)(b: X) = a
 
   val z2 = h[() -> Cap](() => x) // error // error
-    (() => C())
+    (() => C()) // error
   val z3 = h[(() -> Cap) @retains[x.type]](() => x)(() => C())  // error
 
   val z1: () => Cap = f1(x)
diff --git a/tests/neg-custom-args/captures/closure-result-typing.check b/tests/neg-custom-args/captures/closure-result-typing.check
new file mode 100644
index 000000000000..64ee81dce7b5
--- /dev/null
+++ b/tests/neg-custom-args/captures/closure-result-typing.check
@@ -0,0 +1,11 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/closure-result-typing.scala:2:30 -------------------------
+2 |  val x: () -> Object = () => c // error
+  |                              ^
+  |                              Found:    (c : Object^)
+  |                              Required: Object
+  |
+  |                              where:    ^ refers to a fresh root capability in the type of parameter c
+  |
+  |                              Note that capability cap is not included in capture set {}.
+  |
+  | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/closure-result-typing.scala b/tests/neg-custom-args/captures/closure-result-typing.scala
new file mode 100644
index 000000000000..7435f36012d8
--- /dev/null
+++ b/tests/neg-custom-args/captures/closure-result-typing.scala
@@ -0,0 +1,2 @@
+def test(c: Object^): Unit =
+  val x: () -> Object = () => c // error
diff --git a/tests/neg-custom-args/captures/eta.check b/tests/neg-custom-args/captures/eta.check
index 840c3845b236..c0123ec59ae4 100644
--- a/tests/neg-custom-args/captures/eta.check
+++ b/tests/neg-custom-args/captures/eta.check
@@ -6,11 +6,3 @@
   |         Note that capability (f : Proc^) is not included in capture set {}.
   |
   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/eta.scala:6:14 -------------------------------------------
-6 |         bar( () => f )  // error
-  |              ^^^^^^^
-  |              Found:    () ->{f} () ->{f} Unit
-  |              Required: () -> () ->{f} Unit
-  |              Note that capability (f : Proc^) is not included in capture set {}.
-  |
-  | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/eta.scala b/tests/neg-custom-args/captures/eta.scala
index 5cc0196a04c6..d192d7baedf8 100644
--- a/tests/neg-custom-args/captures/eta.scala
+++ b/tests/neg-custom-args/captures/eta.scala
@@ -3,5 +3,5 @@
        def bar[A <: Proc^{f}](g: () -> A): () -> Proc^{f} =
          g  // error
        val stowaway: () -> Proc^{f} =
-         bar( () => f )  // error
+         bar( () => f )  // was error now OK
        () => { stowaway.apply().apply() }
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/filevar.check b/tests/neg-custom-args/captures/filevar.check
index 795b471ecd10..84101f64b963 100644
--- a/tests/neg-custom-args/captures/filevar.check
+++ b/tests/neg-custom-args/captures/filevar.check
@@ -1,11 +1,10 @@
 -- [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^) ?->? File^? ->? Unit
-   |Required: (l: scala.caps.Capability^) ?-> (f: File^{l}) => Unit
+   |Found:    (f: File^?) ->? Unit
+   |Required: (f: File^{l}) => Unit
    |
-   |where:    => refers to a root capability associated with the result type of (using l: scala.caps.Capability^): (f: File^{l}) => Unit
-   |          ^  refers to the universal root capability
+   |where:    => refers to a fresh root capability created in anonymous function of type (using l²: scala.caps.Capability): File^{l²} -> Unit when instantiating expected result type (f: File^{l}) ->{cap} Unit of function literal
    |
    |Note that capability l.type
    |cannot be included in outer capture set ? of parameter f.
diff --git a/tests/neg-custom-args/captures/heal-tparam-cs.check b/tests/neg-custom-args/captures/heal-tparam-cs.check
index c696efee626c..8a149664ffe7 100644
--- a/tests/neg-custom-args/captures/heal-tparam-cs.check
+++ b/tests/neg-custom-args/captures/heal-tparam-cs.check
@@ -37,22 +37,19 @@
 27 |    }
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:41:4 --------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:41:10 -------------------------------
 41 |    io => () => io.use()  // error
-   |    ^^^^^^^^^^^^^^^^^^^^
-   |    Found:    (io: Capp^) ->? () ->{io} Unit
-   |    Required: (io: Capp^) -> () -> Unit
-   |
-   |    where:    ^ refers to the universal root capability
-   |
-   |    Note that capability io.type is not included in capture set {}.
+   |          ^^^^^^^^^^^^^^
+   |          Found:    () ->{io} Unit
+   |          Required: () -> Unit
+   |          Note that capability (io : Capp^) is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:44:10 -------------------------------
 44 |    io => () => io.use()  // error
    |          ^^^^^^^^^^^^^^
    |          Found:    () ->{io} Unit
-   |          Required: () ->? Unit
+   |          Required: () -> Unit
    |          Note that capability (io : Capp^) is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i15923.check b/tests/neg-custom-args/captures/i15923.check
index ea3349ef2c61..70d8acffd227 100644
--- a/tests/neg-custom-args/captures/i15923.check
+++ b/tests/neg-custom-args/captures/i15923.check
@@ -1,14 +1,27 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923.scala:27:23 ---------------------------------------
+27 |    val leak = withCap(cap => mkId(cap))  // error (was: no error here since type aliases don't box)
+   |                       ^^^^^^^^^^^^^^^^
+   |Found:    (cap: test2.Cap^?) ->? [T] => (op: test2.Cap^? ->? T) ->? T
+   |Required: test2.Cap^{lcap} => [T] => (op²: test2.Cap^? ->? T) ->? T
+   |
+   |where:    =>  refers to a fresh root capability created in anonymous function of type (using lcap²: scala.caps.Capability): test2.Cap^{lcap²} -> [T] => (op³: test2.Cap^{lcap²} => T) -> T when instantiating expected result type test2.Cap^{lcap} ->{cap²} [T] => (op²: test2.Cap^? ->? T) ->? T of function literal
+   |          op  is a reference to a value parameter
+   |          op² is a reference to a value parameter
+   |
+   |Note that capability lcap.type
+   |cannot be included in outer capture set ? of parameter cap.
+   |
+   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923.scala:12:21 ---------------------------------------
 12 |  val leak = withCap(cap => mkId(cap)) // error
    |                     ^^^^^^^^^^^^^^^^
-   |Found:    (lcap: scala.caps.Capability^) ?->? Cap^? ->? Id[Cap^?]^?
-   |Required: (lcap: scala.caps.Capability^) ?-> Cap^{lcap} => Id[Cap^?]^?
+   |Found:    (cap: Cap^?) ->? Id[Cap^?]^?
+   |Required: Cap^{lcap} => Id[Cap^?]^?
    |
-   |where:    => refers to a root capability associated with the result type of (using lcap: scala.caps.Capability^): Cap^{lcap} => Id[Cap^?]^?
-   |          ^  refers to the universal root capability
+   |where:    => refers to a fresh root capability created in anonymous function of type (using lcap²: scala.caps.Capability): Cap^{lcap²} -> Id[Cap] when instantiating expected result type Cap^{lcap} ->{cap²} Id[Cap^?]^? of function literal
    |
-   |Note that capability <cap of (x$0: Cap^?): Id[Cap^?]^?>
-   |cannot be included in outer capture set ?.
+   |Note that capability lcap.type
+   |cannot be included in outer capture set ? of parameter cap.
    |
    | longer explanation available when compiling with `-explain`
 -- Warning: tests/neg-custom-args/captures/i15923.scala:21:56 ----------------------------------------------------------
diff --git a/tests/neg-custom-args/captures/i15923.scala b/tests/neg-custom-args/captures/i15923.scala
index 8287be150761..9f7d176c6e14 100644
--- a/tests/neg-custom-args/captures/i15923.scala
+++ b/tests/neg-custom-args/captures/i15923.scala
@@ -24,6 +24,6 @@ object test2:
       result
     }
 
-    val leak = withCap(cap => mkId(cap))  // no error here since type aliases don't box
+    val leak = withCap(cap => mkId(cap))  // error (was: no error here since type aliases don't box)
     leak { cap => cap.use() }
   }
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/i21401.check b/tests/neg-custom-args/captures/i21401.check
index bc1a1143239b..52be12983cbb 100644
--- a/tests/neg-custom-args/captures/i21401.check
+++ b/tests/neg-custom-args/captures/i21401.check
@@ -50,13 +50,14 @@
 -- [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[IO^]^?) ->? Boxed[IO^{x*}]^?
-   |                                              Required: Boxed[IO^] -> Boxed[IO^²]
+   |      Found:    (x: Boxed[IO^]^?) ->? Boxed[IO^²]
+   |      Required: Boxed[IO^] -> Boxed[IO^³]
    |
-   |                                              where:    ^  refers to the universal root capability
-   |                                                        ^² refers to a fresh root capability created in value x²
+   |      where:    ^  refers to the universal root capability
+   |                ^² refers to a root capability associated with the result type of (x: Boxed[IO^]^?): Boxed[IO^²]
+   |                ^³ refers to a fresh root capability created in value x²
    |
-   |                                              Note that capability x* is not included in capture set {cap}
-   |                                              because x* is not visible from cap in value x.
+   |      Note that capability <cap of (x: Boxed[IO^]^?): Boxed[IO^]> is not included in capture set {cap}
+   |      because <cap of (x: Boxed[IO^]^?): Boxed[IO^]> is not visible from cap in value x.
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
index 64672fd36a3f..d3847b13e870 100644
--- a/tests/neg-custom-args/captures/reaches.check
+++ b/tests/neg-custom-args/captures/reaches.check
@@ -68,30 +68,19 @@
 -- [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: File^ -> File^²
-   |
-   |                           where:    ^  refers to the universal root capability
-   |                                     ^² refers to a fresh root capability in the type of value id
-   |
-   |                           Note that capability x.type is not included in capture set {cap}
-   |                           because x.type is not visible from cap in value id.
-   |
-   | longer explanation available when compiling with `-explain`
--- [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^²
+   |                  Found:    (x: File^) ->? File^²
+   |                  Required: File^ -> File^³
    |
    |                  where:    ^  refers to the universal root capability
    |                            ^² refers to a root capability associated with the result type of (x: File^): File^²
+   |                            ^³ refers to a fresh root capability in the type of value id
    |
-   |                  Note that capability x.type is not included in capture set {<cap of (x: File^): File^{x}>}.
+   |                  Note that capability <cap of (x: File^): File^> is not included in capture set {cap}
+   |                  because <cap of (x: File^): File^> is not visible from cap in value id.
    |
    | 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
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:69:38 --------------------------------------
+69 |  val leaked = usingFile[File^{id*}]: f => // error
    |                                      ^
    |Found:    (f: File^?) ->? File^{id*}
    |Required: File^ => File^{id*}
@@ -100,12 +89,12 @@
    |          ^  refers to the universal root capability
    |
    |Note that capability cap is not included in capture set {id*}.
-71 |    val f1: File^{id*} = id(f)
-72 |    f1
+70 |    val f1: File^{id*} = id(f)
+71 |    f1
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:88:10 --------------------------------------
-88 |  ps.map((x, y) => compose1(x, y)) // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:87:10 --------------------------------------
+87 |  ps.map((x, y) => compose1(x, y)) // error
    |          ^^^^^^^^^^^^^^^^^^^^^^^
    |Found:    (x$1: (A^ ->? A^?, A^ ->? A^?)^?) ->? A^? ->? A^?
    |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^? ->? A^?
@@ -116,8 +105,8 @@
    |Note that capability ps* cannot be included in capture set {} of value x.
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:91:10 --------------------------------------
-91 |  ps.map((x, y) => compose1(x, y)) // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:90:10 --------------------------------------
+90 |  ps.map((x, y) => compose1(x, y)) // error
    |          ^^^^^^^^^^^^^^^^^^^^^^^
    |Found:    (x$1: (A^ ->? A^?, A^ ->? A^?)^?) ->? A^? ->? A^?
    |Required: ((A ->{C} A, A ->{C} A)) => A^? ->? A^?
@@ -129,7 +118,7 @@
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/reaches.scala:39:31 -----------------------------------------------------------
-39 |    val next: () => Unit = cur.head   // error
+39 |    val next: () => Unit = cur.head   // error, use
    |                           ^^^^^^^^
    |                           Local reach capability xs* leaks into capture scope of method runAll2.
    |                           You could try to abstract the capabilities referred to by xs* in a capset variable.
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
index 7ffa36d38b18..d59bc4a7994b 100644
--- a/tests/neg-custom-args/captures/reaches.scala
+++ b/tests/neg-custom-args/captures/reaches.scala
@@ -36,7 +36,7 @@ def runAll1[C^](xs: List[() ->{C} Unit]): Unit =
 def runAll2(@consume xs: List[Proc]): Unit =
   var cur: List[Proc] = xs
   while cur.nonEmpty do
-    val next: () => Unit = cur.head   // error
+    val next: () => Unit = cur.head   // error, use
     next()
     cur = cur.tail
 
@@ -64,8 +64,7 @@ def attack2 =
     f1
 
 def attack3 =
-  val id: (x: File^) -> File^ = x => x // error
-    // val id: File^ -> EX C.File^C
+  val id: (x: File^) -> File^ = x => x // was error, now OK
 
   val leaked = usingFile[File^{id*}]: f => // error
     val f1: File^{id*} = id(f)
diff --git a/tests/neg-custom-args/captures/scoped-caps.check b/tests/neg-custom-args/captures/scoped-caps.check
index d0fbdccd1305..90b957c4cb43 100644
--- a/tests/neg-custom-args/captures/scoped-caps.check
+++ b/tests/neg-custom-args/captures/scoped-caps.check
@@ -41,27 +41,16 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:12:20 ----------------------------------
 12 |  val _: A^ -> B^ = x => g(x)      // error: g is no longer pure, since it contains the ^ of B
    |                    ^^^^^^^^^
-   |                    Found:    (x: A^) ->{g} B^{g*}
-   |                    Required: A^ -> B^²
+   |                    Found:    (x: A^) ->{g} B^²
+   |                    Required: A^ -> B^³
    |
    |                    where:    ^  refers to the universal root capability
-   |                              ^² refers to a fresh root capability in the type of value _$5
+   |                              ^² 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 _$5
    |
    |                    Note that capability (g : A^ -> B^) is not included in capture set {}.
    |
    | 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 capability x.type is not included in capture set {<cap of (x: A^): B^{x}>}.
-   |
-   | 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
    |                        ^
@@ -77,11 +66,12 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:17:24 ----------------------------------
 17 |  val _: (x: S) -> B^ = (x: S) => h(x)  // error: eta expansion fails
    |                        ^^^^^^^^^^^^^^
-   |                        Found:    (x: S^) ->{h} B^{h*}
-   |                        Required: (x: S^) -> B^²
+   |                        Found:    (x: S^) ->{h} B^²
+   |                        Required: (x: S^) -> B^³
    |
    |                        where:    ^  refers to the universal root capability
    |                                  ^² refers to a root capability associated with the result type of (x: S^): B^²
+   |                                  ^³ refers to a root capability associated with the result type of (x: S^): B^³
    |
    |                        Note that capability (h : S -> B^) is not included in capture set {}.
    |
@@ -89,11 +79,12 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:21:23 ----------------------------------
 21 |  val _: (x: S) -> S = (x: S) => h2(x)  // error: eta conversion fails since `h2` is now impure (result type S is a capability)
    |                       ^^^^^^^^^^^^^^^
-   |                       Found:    (x: S^) ->{h2} S^{h2*}
-   |                       Required: (x: S^) -> S^²
+   |                       Found:    (x: S^) ->{h2} S^²
+   |                       Required: (x: S^) -> S^³
    |
    |                       where:    ^  refers to the universal root capability
    |                                 ^² refers to a root capability associated with the result type of (x: S^): S^²
+   |                                 ^³ refers to a root capability associated with the result type of (x: S^): S^³
    |
    |                       Note that capability (h2 : S -> S) is not included in capture set {}.
    |
@@ -115,13 +106,14 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:28:19 ----------------------------------
 28 |  val _: S -> B^ = x => j(x)       // error
    |                   ^^^^^^^^^
-   |                   Found:    (x: S^) ->? B^{x}
-   |                   Required: S^ -> B^²
+   |                   Found:    (x: S^) ->? B^²
+   |                   Required: S^ -> B^³
    |
    |                   where:    ^  refers to the universal root capability
-   |                             ^² refers to a fresh root capability in the type of value _$15
+   |                             ^² refers to a root capability associated with the result type of (x: S^): B^²
+   |                             ^³ refers to a fresh root capability in the type of value _$15
    |
-   |                   Note that capability x.type is not included in capture set {cap}
-   |                   because x.type is not visible from cap in value _$15.
+   |                   Note that capability <cap of (x: S^): B^> is not included in capture set {cap}
+   |                   because <cap of (x: S^): B^> is not visible from cap in value _$15.
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/scoped-caps.scala b/tests/neg-custom-args/captures/scoped-caps.scala
index 128e8c095086..d285b7ef79f5 100644
--- a/tests/neg-custom-args/captures/scoped-caps.scala
+++ b/tests/neg-custom-args/captures/scoped-caps.scala
@@ -10,7 +10,7 @@ def test(io: Object^): Unit =
   val _: A^ -> B^ = f // error
   val _: A^ -> B^ = g
   val _: A^ -> B^ = x => g(x)      // error: g is no longer pure, since it contains the ^ of B
-  val _: (x: A^) -> B^ = x => f(x) // error: existential in B cannot subsume `x` since `x` is not shared
+  val _: (x: A^) -> B^ = x => f(x) // now OK, was error: existential in B cannot subsume `x` since `x` is not shared
 
   val h: S -> B^ = ???
   val _: (x: S) -> B^ = h          // error: direct conversion fails
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
index b08d27cf14e5..0ce74f481b56 100644
--- a/tests/neg-custom-args/captures/vars.check
+++ b/tests/neg-custom-args/captures/vars.check
@@ -27,13 +27,14 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:36:8 ------------------------------------------
 36 |  local { cap3 => // error
    |        ^
-   |Found:    (cap3: CC^) ->? String ->{cap3} String
-   |Required: CC^ -> String => String
+   |Found:    (cap3: CC^) ->? String => String
+   |Required: CC^ -> String =>² String
    |
-   |where:    => refers to a fresh root capability created in method test of parameter parameter cap3² of method $anonfun
-   |          ^  refers to the universal root capability
+   |where:    =>  refers to a root capability associated with the result type of (cap3: CC^): String => String
+   |          =>² refers to a fresh root capability created in method test of parameter parameter cap3² of method $anonfun
+   |          ^   refers to the universal root capability
    |
-   |Note that capability cap3.type
+   |Note that capability <cap of (cap3: CC^): String => String>
    |cannot be included in outer capture set {cap}.
 37 |    def g(x: String): String = if cap3 == cap3 then "" else "a"
 38 |    g
diff --git a/tests/neg-custom-args/captures/widen-reach.check b/tests/neg-custom-args/captures/widen-reach.check
index 07a8c301a0c0..7e25b96d87b1 100644
--- a/tests/neg-custom-args/captures/widen-reach.check
+++ b/tests/neg-custom-args/captures/widen-reach.check
@@ -8,14 +8,15 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:9:24 -----------------------------------
 9 |  val foo: IO^ -> IO^ = x => x // error
   |                        ^^^^^^
-  |                        Found:    (x: IO^) ->? IO^{x}
-  |                        Required: IO^ -> IO^²
+  |                        Found:    (x: IO^) ->? IO^²
+  |                        Required: IO^ -> IO^³
   |
   |                        where:    ^  refers to the universal root capability
-  |                                  ^² refers to a fresh root capability in the type of value foo
+  |                                  ^² refers to a root capability associated with the result type of (x: IO^): IO^²
+  |                                  ^³ refers to a fresh root capability in the type of value foo
   |
-  |                        Note that capability x.type is not included in capture set {cap}
-  |                        because x.type is not visible from cap in value foo.
+  |                        Note that capability <cap of (x: IO^): IO^> is not included in capture set {cap}
+  |                        because <cap of (x: IO^): IO^> is not visible from cap in value foo.
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 ----------------------------------
diff --git a/tests/pos-custom-args/captures/closure-result-typing.scala b/tests/pos-custom-args/captures/closure-result-typing.scala
new file mode 100644
index 000000000000..fe8efff9861d
--- /dev/null
+++ b/tests/pos-custom-args/captures/closure-result-typing.scala
@@ -0,0 +1,2 @@
+def test(c: Object^): Unit =
+  val y: (x: Object^{c}) -> Object^ = x => x