From ece8d96016ffe3a4215bf8696b0ef6d91cd3f601 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 2 Jul 2023 10:03:10 +0200
Subject: [PATCH 01/14] Refactorings

Some new comments, simplifications, syntax tweaks
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 103 ++++++++++--------
 .../src/dotty/tools/dotc/core/Types.scala     |   2 +-
 2 files changed, 56 insertions(+), 49 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 039a9623ff5f..66c1bec37ffd 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -30,9 +30,9 @@ object CheckCaptures:
 
     override def isEnabled(using Context) = true
 
-  	/** Reset `private` flags of parameter accessors so that we can refine them
-     *  in Setup if they have non-empty capture sets. Special handling of some
-     *  symbols defined for case classes.
+  	/**  - Reset `private` flags of parameter accessors so that we can refine them
+     *     in Setup if they have non-empty capture sets.
+     *   - Special handling of some symbols defined for case classes.
      */
     def transformSym(sym: SymDenotation)(using Context): SymDenotation =
       if sym.isAllOf(PrivateParamAccessor) && !sym.hasAnnotation(defn.ConstructorOnlyAnnot) then
@@ -89,6 +89,7 @@ object CheckCaptures:
           tp
         case _ =>
           mapOver(tp)
+  end SubstParamsMap
 
   /** Check that a @retains annotation only mentions references that can be tracked.
    *  This check is performed at Typer.
@@ -115,37 +116,32 @@ object CheckCaptures:
           report.warning(em"redundant capture: $parent already accounts for $ref", pos)
     case _ =>
 
-  /** Warn if `ann`, which is a tree of a @retains annotation, defines some elements that
+  /** Warn if `ann`, which is the tree of a @retains annotation, defines some elements that
    *  are already accounted for by other elements of the same annotation.
    *  Note: We need to perform the check on the original annotation rather than its
    *  capture set since the conversion to a capture set already eliminates redundant elements.
    */
   def warnIfRedundantCaptureSet(ann: Tree)(using Context): Unit =
-    // The lists `elems(i) :: prev.reverse :: elems(0),...,elems(i-1),elems(i+1),elems(n)`
-    // where `n == elems.length-1`, i <- 0..n`.
-    // I.e.
-    // choices(Nil, elems) = [[elems(i), elems(0), ..., elems(i-1), elems(i+1), .... elems(n)] | i <- 0..n]
-    def choices(prev: List[Tree], elems: List[Tree]): List[List[Tree]] = elems match
-      case Nil => Nil
-      case elem :: elems =>
-        List(elem :: (prev reverse_::: elems)) ++ choices(elem :: prev, elems)
-    for case first :: others <- choices(Nil, retainedElems(ann)) do
-      val firstRef = first.toCaptureRef
-      val remaining = CaptureSet(others.map(_.toCaptureRef)*)
-      if remaining.accountsFor(firstRef) then
-        report.warning(em"redundant capture: $remaining already accounts for $firstRef", ann.srcPos)
-
+    var retained = retainedElems(ann).toArray
+    for i <- 0 until retained.length do
+      val ref = retained(i).toCaptureRef
+      val others = for j <- 0 until retained.length if j != i yield retained(j).toCaptureRef
+      val remaining = CaptureSet(others*)
+      if remaining.accountsFor(ref) then
+        report.warning(em"redundant capture: $remaining already accounts for $ref", ann.srcPos)
+
+  /** Report an error if some part of `tp` contains the root capability in its capture set */
   def disallowRootCapabilitiesIn(tp: Type, what: String, have: String, addendum: String, pos: SrcPos)(using Context) =
     val check = new TypeTraverser:
       def traverse(t: Type) =
         if variance >= 0 then
-        t.captureSet.disallowRootCapability: () =>
-          def part = if t eq tp then "" else i"the part $t of "
-          report.error(
-            em"""$what cannot $have $tp since
-                |${part}that type captures the root capability `cap`.
-                |$addendum""",
-            pos)
+          t.captureSet.disallowRootCapability: () =>
+            def part = if t eq tp then "" else i"the part $t of "
+            report.error(
+              em"""$what cannot $have $tp since
+                  |${part}that type captures the root capability `cap`.
+                  |$addendum""",
+              pos)
         traverseChildren(t)
     check.traverse(tp)
 
@@ -235,17 +231,31 @@ class CheckCaptures extends Recheck, SymTransformer:
         if sym.ownersIterator.exists(_.isTerm) then CaptureSet.Var()
         else CaptureSet.empty)
 
+    /**
+    class anon1 extends Function1:
+      def apply: Function1 =
+        use(x)
+        class anon2 extends Function1:
+          use(y)
+          def apply: Function1 = ...
+        anon2()
+    anon1()
+    */
     /** For all nested environments up to `limit` perform `op` */
     def forallOuterEnvsUpTo(limit: Symbol)(op: Env => Unit)(using Context): Unit =
+      def stopsPropagation(env: Env) =
+        val sym = env.owner
+        env.isOutermost
+        || false && sym.is(Method) && sym.owner.isTerm && !sym.isConstructor
       def recur(env: Env): Unit =
         if env.isOpen && env.owner != limit then
           op(env)
-          if !env.isOutermost then
+          if !stopsPropagation(env) then
             var nextEnv = env.outer
             if env.owner.isConstructor then
-              if nextEnv.owner != limit && !nextEnv.isOutermost then
-                recur(nextEnv.outer)
-            else recur(nextEnv)
+              if nextEnv.owner != limit && !stopsPropagation(nextEnv) then
+                nextEnv = nextEnv.outer
+            recur(nextEnv)
       recur(curEnv)
 
     /** Include `sym` in the capture sets of all enclosing environments nested in the
@@ -255,10 +265,9 @@ class CheckCaptures extends Recheck, SymTransformer:
       if sym.exists then
         val ref = sym.termRef
         if ref.isTracked then
-          forallOuterEnvsUpTo(sym.enclosure) { env =>
+          forallOuterEnvsUpTo(sym.enclosure): env =>
             capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}")
             checkElem(ref, env.captured, pos)
-          }
 
     /** Make sure (projected) `cs` is a subset of the capture sets of all enclosing
      *  environments. At each stage, only include references from `cs` that are outside
@@ -266,19 +275,16 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     def markFree(cs: CaptureSet, pos: SrcPos)(using Context): Unit =
       if !cs.isAlwaysEmpty then
-        forallOuterEnvsUpTo(ctx.owner.topLevelClass) { env =>
-          val included = cs.filter {
-            case ref: TermRef =>
-              (env.nestedInOwner || env.owner != ref.symbol.owner)
-                && env.owner.isContainedIn(ref.symbol.owner)
-            case ref: ThisType =>
-              (env.nestedInOwner || env.owner != ref.cls)
-                && env.owner.isContainedIn(ref.cls)
+        forallOuterEnvsUpTo(ctx.owner.topLevelClass): env =>
+          def isVisibleFromEnv(sym: Symbol) =
+            (env.nestedInOwner || env.owner != sym)
+            && env.owner.isContainedIn(sym)
+          val included = cs.filter:
+            case ref: TermRef => isVisibleFromEnv(ref.symbol.owner)
+            case ref: ThisType => isVisibleFromEnv(ref.cls)
             case _ => false
-          }
           capt.println(i"Include call capture $included in ${env.owner}")
           checkSubset(included, env.captured, pos)
-        }
 
     /** Include references captured by the called method in the current environment stack */
     def includeCallCaptures(sym: Symbol, pos: SrcPos)(using Context): Unit =
@@ -305,7 +311,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           // This case can arise when we try to merge multiple types that have different
           // capture sets on some part. For instance an asSeenFrom might produce
           // a bi-mapped capture set arising from a substition. Applying the same substitution
-          // to the same type twice will nevertheless produce different capture setsw which can
+          // to the same type twice will nevertheless produce different capture sets which can
           // lead to a failure in disambiguation since neither alternative is better than the
           // other in a frozen constraint. An example test case is disambiguate-select.scala.
           // We address the problem by disambiguating while ignoring all capture sets as a fallback.
@@ -320,7 +326,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         selType
       else
         val qualCs = qualType.captureSet
-        capt.println(i"intersect $qualType, ${selType.widen}, $qualCs, $selCs in $tree")
+        capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs in $tree")
         if qualCs.mightSubcapture(selCs)
             && !selCs.mightSubcapture(qualCs)
             && !pt.stripCapturing.isInstanceOf[SingletonType]
@@ -345,21 +351,22 @@ class CheckCaptures extends Recheck, SymTransformer:
     override def recheckApply(tree: Apply, pt: Type)(using Context): Type =
       val meth = tree.fun.symbol
       includeCallCaptures(meth, tree.srcPos)
+
+      // Unsafe box/unbox handlng, only for versions < 3.3
       def mapArgUsing(f: Type => Type) =
         val arg :: Nil = tree.args: @unchecked
         val argType0 = f(recheckStart(arg, pt))
         val argType = super.recheckFinish(argType0, arg, pt)
         super.recheckFinish(argType, tree, pt)
-
       if meth == defn.Caps_unsafeBox then
         mapArgUsing(_.forceBoxStatus(true))
       else if meth == defn.Caps_unsafeUnbox then
         mapArgUsing(_.forceBoxStatus(false))
       else if meth == defn.Caps_unsafeBoxFunArg then
-        mapArgUsing {
+        mapArgUsing:
           case defn.FunctionOf(paramtpe :: Nil, restpe, isContectual) =>
             defn.FunctionOf(paramtpe.forceBoxStatus(true) :: Nil, restpe, isContectual)
-        }
+
       else
         super.recheckApply(tree, pt) match
           case appType @ CapturingType(appType1, refs) =>
@@ -371,8 +378,8 @@ class CheckCaptures extends Recheck, SymTransformer:
                   && qual.tpe.captureSet.mightSubcapture(refs)
                   && tree.args.forall(_.tpe.captureSet.mightSubcapture(refs))
               =>
-                val callCaptures = tree.args.foldLeft(qual.tpe.captureSet)((cs, arg) =>
-                  cs ++ arg.tpe.captureSet)
+                val callCaptures = tree.args.foldLeft(qual.tpe.captureSet): (cs, arg) =>
+                  cs ++ arg.tpe.captureSet
                 appType.derivedCapturingType(appType1, callCaptures)
                   .showing(i"narrow $tree: $appType, refs = $refs, qual = ${qual.tpe.captureSet} --> $result", capt)
               case _ => appType
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 59506e3f1419..eeccd9116346 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -6191,7 +6191,7 @@ object Types {
             tp.derivedLambdaType(tp.paramNames, formals, restpe)
       }
 
-    /** Overridden in TypeOps.avoid */
+    /** Overridden in TypeOps.avoid and in CheckCaptures.substParamsMap */
     protected def needsRangeIfInvariant(refs: CaptureSet): Boolean = true
 
     override def mapCapturingType(tp: Type, parent: Type, refs: CaptureSet, v: Int): Type =

From 58ecdc9abebd73a8e0784b221945273898faf8d2 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 2 Jul 2023 11:41:34 +0200
Subject: [PATCH 02/14] Avoid including call captures twice when applying a
 method

---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 66c1bec37ffd..affeb3c326f7 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -291,8 +291,12 @@ class CheckCaptures extends Recheck, SymTransformer:
       if sym.exists && curEnv.isOpen then markFree(capturedVars(sym), pos)
 
     override def recheckIdent(tree: Ident)(using Context): Type =
-      if tree.symbol.is(Method) then includeCallCaptures(tree.symbol, tree.srcPos)
-      else markFree(tree.symbol, tree.srcPos)
+      if tree.symbol.is(Method) then
+        if tree.symbol.info.isParameterless then
+          // there won't be an apply; need to include call captures now
+          includeCallCaptures(tree.symbol, tree.srcPos)
+      else
+        markFree(tree.symbol, tree.srcPos)
       super.recheckIdent(tree)
 
     /** A specialized implementation of the selection rule.

From 83f0bee8955bbfa061dd1999301f1bf7b6d2165a Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 2 Jul 2023 10:08:53 +0200
Subject: [PATCH 03/14] More comments in Recheck

---
 compiler/src/dotty/tools/dotc/transform/Recheck.scala | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 527c73d02250..3c5b4aac91b5 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -155,8 +155,14 @@ abstract class Recheck extends Phase, SymTransformer:
      */
     def keepType(tree: Tree): Boolean = keepAllTypes
 
+    /** A map from NamedTypes to the denotations they had before this phase.
+     *  Needed so that we can `reset` them after this phase.
+     */
     private val prevSelDenots = util.HashMap[NamedType, Denotation]()
 
+    /** Reset all references in `prevSelDenots` to the denotations they had
+     *  before this phase.
+     */
     def reset()(using Context): Unit =
       for (ref, mbr) <- prevSelDenots.iterator do
         ref.withDenot(mbr)
@@ -203,6 +209,7 @@ abstract class Recheck extends Phase, SymTransformer:
             val prevDenot = prevType.denot
             val newType = qualType.select(name, mbr)
             if (newType eq prevType) && (mbr.info ne prevDenot.info) && !prevSelDenots.contains(prevType) then
+              // remember previous denot of NamedType, so that it can be reset after this phase
               prevSelDenots(prevType) = prevDenot
             newType
           case _ =>
@@ -210,7 +217,6 @@ abstract class Recheck extends Phase, SymTransformer:
         constFold(tree, newType)
           //.showing(i"recheck select $qualType . $name : ${mbr.info} = $result")
 
-
     /** Keep the symbol of the `select` but re-infer its type */
     def recheckSelection(tree: Select, qualType: Type, name: Name, pt: Type)(using Context): Type =
       recheckSelection(tree, qualType, name, sharpen = identity[Denotation])

From 8ccebe4ac5de78195f21d78370eb6620cf50d68b Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 2 Jul 2023 11:50:04 +0200
Subject: [PATCH 04/14] Simplify augmentConstructor

---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 29 +++++++++----------
 1 file changed, 14 insertions(+), 15 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index affeb3c326f7..6e374e1f02ed 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -414,15 +414,19 @@ class CheckCaptures extends Recheck, SymTransformer:
          *  Second half: union of all capture sets of arguments to tracked parameters.
          */
         def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
-          mt.paramNames.lazyZip(argTypes).foldLeft((core, initCs)) { (acc, refine) =>
-            val (core, allCaptures) = acc
-            val (getterName, argType) = refine
+          var refined: Type = core
+          var allCaptures: CaptureSet = initCs
+          for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
             val getter = cls.info.member(getterName).suchThat(_.is(ParamAccessor)).symbol
-            if getter.termRef.isTracked && !getter.is(Private)
-            then (RefinedType(core, getterName, argType), allCaptures ++ argType.captureSet)
-            else (core, allCaptures)
-          }
-
+            if getter.termRef.isTracked && !getter.is(Private) then
+              refined = RefinedType(refined, getterName, argType)
+              allCaptures ++= argType.captureSet
+          (refined, allCaptures)
+
+        /** Augment result type of constructor with refinements and captures.
+         *  @param  core   The result type of the constructor
+         *  @param  initCs The initial capture set to add, not yet counting capture sets from arguments
+         */
         def augmentConstructorType(core: Type, initCs: CaptureSet): Type = core match
           case core: MethodType =>
             // more parameters to follow; augment result type
@@ -435,13 +439,8 @@ class CheckCaptures extends Recheck, SymTransformer:
             val (refined, cs) = addParamArgRefinements(core, initCs)
             refined.capturing(cs)
 
-        augmentConstructorType(ownType, CaptureSet.empty) match
-          case augmented: MethodType =>
-            augmented
-          case augmented =>
-            // add capture sets of class and constructor to final result of constructor call
-            augmented.capturing(capturedVars(cls) ++ capturedVars(sym))
-              .showing(i"constr type $mt with $argTypes%, % in $cls = $result", capt)
+        augmentConstructorType(ownType, capturedVars(cls) ++ capturedVars(sym))
+          .showing(i"constr type $mt with $argTypes%, % in $cls = $result", capt)
       else ownType
     end instantiate
 

From 714d4b3d8f8aba77ec3778d25ac3f41a6012a317 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 2 Jul 2023 15:56:16 +0200
Subject: [PATCH 05/14] Fix Recheck.rememberTypeAlways

And further simplifications and comments
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 60 ++++++++++++-------
 .../dotty/tools/dotc/transform/Recheck.scala  |  2 +-
 2 files changed, 39 insertions(+), 23 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 6e374e1f02ed..1119b88e4978 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -301,9 +301,9 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     /** A specialized implementation of the selection rule.
      *
-     *  E |- f: Cf f { m: Cr R }
-     *  ------------------------
-     *  E |- f.m: C R
+     *  E |- f: f{ m: Cr R }^Cf
+     *  -----------------------
+     *  E |- f.m: R^C
      *
      *  The implementation picks as `C` one of `{f}` or `Cr`, depending on the
      *  outcome of a `mightSubcapture` test. It picks `{f}` if this might subcapture Cr
@@ -343,10 +343,10 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     /** A specialized implementation of the apply rule.
      *
-     *  E |- f: Cf (Ra -> Cr Rr)
-     *  E |- a: Ca Ra
-     *  ------------------------
-     *  E |- f a: C Rr
+     *  E |- f: Ra ->Cf Rr^Cr
+     *  E |- a: Ra^Ca
+     *  ---------------------
+     *  E |- f a: Rr^C
      *
      *  The implementation picks as `C` one of `{f, a}` or `Cr`, depending on the
      *  outcome of a `mightSubcapture` test. It picks `{f, a}` if this might subcapture Cr
@@ -368,8 +368,8 @@ class CheckCaptures extends Recheck, SymTransformer:
         mapArgUsing(_.forceBoxStatus(false))
       else if meth == defn.Caps_unsafeBoxFunArg then
         mapArgUsing:
-          case defn.FunctionOf(paramtpe :: Nil, restpe, isContectual) =>
-            defn.FunctionOf(paramtpe.forceBoxStatus(true) :: Nil, restpe, isContectual)
+          case defn.FunctionOf(paramtpe :: Nil, restpe, isContextual) =>
+            defn.FunctionOf(paramtpe.forceBoxStatus(true) :: Nil, restpe, isContextual)
 
       else
         super.recheckApply(tree, pt) match
@@ -474,14 +474,14 @@ class CheckCaptures extends Recheck, SymTransformer:
                 .installAfter(preRecheckPhase)
 
               // Next, update all parameter symbols to match expected formals
-              meth.paramSymss.head.lazyZip(ptformals).foreach { (psym, pformal) =>
+              meth.paramSymss.head.lazyZip(ptformals).foreach: (psym, pformal) =>
                 psym.updateInfoBetween(preRecheckPhase, thisPhase, pformal.mapExprType)
-              }
+
               // Next, update types of parameter ValDefs
-              mdef.paramss.head.lazyZip(ptformals).foreach { (param, pformal) =>
+              mdef.paramss.head.lazyZip(ptformals).foreach: (param, pformal) =>
                 val ValDef(_, tpt, _) = param: @unchecked
                 tpt.rememberTypeAlways(pformal)
-              }
+
               // Next, install a new completer reflecting the new parameters for the anonymous method
               val mt = meth.info.asInstanceOf[MethodType]
               val completer = new LazyType:
@@ -521,6 +521,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      *   2. The capture set of the self type of a class includes the capture set of the class.
      *   3. The capture set of the self type of a class includes the capture set of every class parameter,
      *      unless the parameter is marked @constructorOnly.
+     *   4. If the class extends a pure base class, the capture set of the self type must be empty.
      */
     override def recheckClassDef(tree: TypeDef, impl: Template, cls: ClassSymbol)(using Context): Type =
       val saved = curEnv
@@ -534,7 +535,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         for param <- cls.paramGetters do
           if !param.hasAnnotation(defn.ConstructorOnlyAnnot) then
             checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3)
-        for pureBase <- cls.pureBaseClass do
+        for pureBase <- cls.pureBaseClass do // (4)
           checkSubset(thisSet,
             CaptureSet.empty.withDescription(i"of pure base class $pureBase"),
             tree.srcPos)
@@ -620,9 +621,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       def checkNotUniversal(tp: Type): Unit = tp.widenDealias match
         case wtp @ CapturingType(parent, refs) =>
           refs.disallowRootCapability { () =>
-            val kind = if tree.isInstanceOf[ValDef] then "mutable variable" else "expression"
             report.error(
-              em"""The $kind's type $wtp is not allowed to capture the root capability `cap`.
+              em"""The expression's type $wtp is not allowed to capture the root capability `cap`.
                   |This usually means that a capability persists longer than its allowed lifetime.""",
               tree.srcPos)
           }
@@ -631,6 +631,16 @@ class CheckCaptures extends Recheck, SymTransformer:
       if !allowUniversalInBoxed then checkNotUniversal(typeToCheck)
       super.recheckFinish(tpe, tree, pt)
 
+  // ------------------ Adaptation -------------------------------------
+  //
+  // Adaptations before checking conformance of actual vs expected:
+  //
+  //   - Convert function to dependent function if expected type is a dependent function type
+  //     (c.f. alignDependentFunction).
+  //   - Relax expected capture set containing `this.type`s by adding references only
+  //     accessible through those types (c.f. addOuterRefs, also #14930 for a discussion).
+  //   - Adapt box status and environment capture sets by simulating box/unbox operations.
+
     /** Massage `actual` and `expected` types using the methods below before checking conformance */
     override def checkConformsExpr(actual: Type, expected: Type, tree: Tree)(using Context): Unit =
       val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing)
@@ -656,9 +666,9 @@ class CheckCaptures extends Recheck, SymTransformer:
       recur(expected)
 
     /** For the expected type, implement the rule outlined in #14390:
-     *   - when checking an expression `a: Ca Ta` against an expected type `Ce Te`,
+     *   - when checking an expression `a: Ta^Ca` against an expected type `Te^Ce`,
      *   - where the capture set `Ce` contains Cls.this,
-     *   - and where and all method definitions enclosing `a` inside class `Cls`
+     *   - and where all method definitions enclosing `a` inside class `Cls`
      *     have only pure parameters,
      *   - add to `Ce` all references to variables or this-references in `Ca`
      *     that are outside `Cls`. These are all accessed through `Cls.this`,
@@ -666,16 +676,21 @@ class CheckCaptures extends Recheck, SymTransformer:
      *     them explicitly to `Ce` changes nothing.
      */
     private def addOuterRefs(expected: Type, actual: Type)(using Context): Type =
+
       def isPure(info: Type): Boolean = info match
         case info: PolyType => isPure(info.resType)
         case info: MethodType => info.paramInfos.forall(_.captureSet.isAlwaysEmpty) && isPure(info.resType)
         case _ => true
+
       def isPureContext(owner: Symbol, limit: Symbol): Boolean =
         if owner == limit then true
         else if !owner.exists then false
         else isPure(owner.info) && isPureContext(owner.owner, limit)
+
+      // Augment expeced capture set `erefs` by all references in actual capture
+      // set `arefs` that are outside some `this.type` reference in `erefs`
       def augment(erefs: CaptureSet, arefs: CaptureSet): CaptureSet =
-        (erefs /: erefs.elems) { (erefs, eref) =>
+        (erefs /: erefs.elems): (erefs, eref) =>
           eref match
             case eref: ThisType if isPureContext(ctx.owner, eref.cls) =>
               erefs ++ arefs.filter {
@@ -685,7 +700,7 @@ class CheckCaptures extends Recheck, SymTransformer:
               }
             case _ =>
               erefs
-        }
+
       expected match
         case CapturingType(ecore, erefs) =>
           val erefs1 = augment(erefs, actual.captureSet)
@@ -694,6 +709,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           expected.derivedCapturingType(ecore, erefs1)
         case _ =>
           expected
+    end addOuterRefs
 
     /** Adapt `actual` type to `expected` type by inserting boxing and unboxing conversions
      *
@@ -703,8 +719,8 @@ class CheckCaptures extends Recheck, SymTransformer:
 
       /** Adapt function type `actual`, which is `aargs -> ares` (possibly with dependencies)
        *  to `expected` type.
-       *  It returns the adapted type along with the additionally captured variable
-       *  during adaptation.
+       *  It returns the adapted type along with a capture set consisting of the references
+       *  that were additionally captured during adaptation.
        *   @param reconstruct  how to rebuild the adapted function type
        */
       def adaptFun(actual: Type, aargs: List[Type], ares: Type, expected: Type,
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 3c5b4aac91b5..17aedeec02fd 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -84,7 +84,7 @@ object Recheck:
      *  type stored in the tree itself
      */
     def rememberTypeAlways(tpe: Type)(using Context): Unit =
-      if tpe ne tree.tpe then tree.putAttachment(RecheckedType, tpe)
+      if tpe ne tree.knownType then tree.putAttachment(RecheckedType, tpe)
 
     /** The remembered type of the tree, or if none was installed, the original type */
     def knownType: Type =

From 478b60c622725b330f022ca078635b84f943ab5d Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 2 Jul 2023 15:56:59 +0200
Subject: [PATCH 06/14] Fix CaptureSet's --

---
 compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index fdc4f66beafa..fd07133b55e1 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -210,10 +210,11 @@ sealed abstract class CaptureSet extends Showable:
    *  any of the elements in the constant capture set `that`
    */
   def -- (that: CaptureSet.Const)(using Context): CaptureSet =
-    val elems1 = elems.filter(!that.accountsFor(_))
-    if elems1.size == elems.size then this
-    else if this.isConst then Const(elems1)
-    else Diff(asVar, that)
+    if this.isConst then
+      val elems1 = elems.filter(!that.accountsFor(_))
+      if elems1.size == elems.size then this else Const(elems1)
+    else
+      if that.isAlwaysEmpty then this else Diff(asVar, that)
 
   /** The largest subset (via <:<) of this capture set that does not account for `ref` */
   def - (ref: CaptureRef)(using Context): CaptureSet =

From 10f2d2bf5f5473bdd9b7556a17ff927a814c7c77 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 3 Jul 2023 14:36:42 +0200
Subject: [PATCH 07/14] Follow span of function types when computing
 captureSetOfInfo

---
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  | 63 +++++++++++--------
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  3 +-
 .../src/dotty/tools/dotc/core/Types.scala     |  2 +-
 .../captures/dependent-pure.scala             |  5 ++
 4 files changed, 45 insertions(+), 28 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/dependent-pure.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index fd07133b55e1..9de68220d2cf 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -846,34 +846,45 @@ object CaptureSet:
   /** The capture set of the type underlying a CaptureRef */
   def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
     case ref: TermRef if ref.isRootCapability => ref.singletonCaptureSet
-    case _ => ofType(ref.underlying)
+    case _ => ofType(ref.underlying, followResult = true)
 
   /** Capture set of a type */
-  def ofType(tp: Type)(using Context): CaptureSet =
-    def recur(tp: Type): CaptureSet = tp.dealias match
-      case tp: TermRef =>
-        tp.captureSet
-      case tp: TermParamRef =>
-        tp.captureSet
-      case _: TypeRef =>
-        if tp.classSymbol.hasAnnotation(defn.CapabilityAnnot) then universal else empty
-      case _: TypeParamRef =>
-        empty
-      case CapturingType(parent, refs) =>
-        recur(parent) ++ refs
-      case AppliedType(tycon, args) =>
-        val cs = recur(tycon)
-        tycon.typeParams match
-          case tparams @ (LambdaParam(tl, _) :: _) => cs.substParams(tl, args)
-          case _ => cs
-      case tp: TypeProxy =>
-        recur(tp.underlying)
-      case AndType(tp1, tp2) =>
-        recur(tp1) ** recur(tp2)
-      case OrType(tp1, tp2) =>
-        recur(tp1) ++ recur(tp2)
-      case _ =>
-        empty
+  def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =
+    def recur(tp: Type): CaptureSet = trace(i"ofType $tp, ${tp.getClass} $followResult", show = true):
+      tp.dealias match
+        case tp: TermRef =>
+          tp.captureSet
+        case tp: TermParamRef =>
+          tp.captureSet
+        case _: TypeRef =>
+          if tp.classSymbol.hasAnnotation(defn.CapabilityAnnot) then universal else empty
+        case _: TypeParamRef =>
+          empty
+        case CapturingType(parent, refs) =>
+          recur(parent) ++ refs
+        case tpd @ RefinedType(parent, _, rinfo: MethodType)
+        if followResult && defn.isFunctionType(tpd) =>
+          ofType(parent, followResult = false)                 // pick up capture set from parent type
+          ++ (recur(rinfo.resType)                             // add capture set of result
+          -- CaptureSet(rinfo.paramRefs.filter(_.isTracked)*)) // but disregard bound parameters
+        case tpd @ AppliedType(tycon, args) =>
+          if followResult && defn.isNonRefinedFunction(tpd) then
+            recur(args.last)
+              // must be (pure) FunctionN type since ImpureFunctions have already
+              // been eliminated in selector's dealias. Use capture set of result.
+          else
+            val cs = recur(tycon)
+            tycon.typeParams match
+              case tparams @ (LambdaParam(tl, _) :: _) => cs.substParams(tl, args)
+              case _ => cs
+        case tp: TypeProxy =>
+          recur(tp.underlying)
+        case AndType(tp1, tp2) =>
+          recur(tp1) ** recur(tp2)
+        case OrType(tp1, tp2) =>
+          recur(tp1) ++ recur(tp2)
+        case _ =>
+          empty
     recur(tp)
       .showing(i"capture set of $tp = $result", capt)
 
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 1119b88e4978..77ca962d2c0d 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -854,8 +854,9 @@ class CheckCaptures extends Recheck, SymTransformer:
       actual match
         case ref: CaptureRef if ref.isTracked =>
           actualw match
-            case CapturingType(p, refs) =>
+            case CapturingType(p, refs) if ref.singletonCaptureSet.mightSubcapture(refs) =>
               actualw = actualw.derivedCapturingType(p, ref.singletonCaptureSet)
+                .showing(i"improve $actualw to $result", capt)
                 // given `a: C T`, improve `C T` to `{a} T`
             case _ =>
         case _ =>
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index eeccd9116346..23ad8e7cebda 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1576,7 +1576,7 @@ object Types {
     }
 
     /** The capture set of this type. Overridden and cached in CaptureRef */
-    def captureSet(using Context): CaptureSet = CaptureSet.ofType(this)
+    def captureSet(using Context): CaptureSet = CaptureSet.ofType(this, followResult = false)
 
     // ----- Normalizing typerefs over refined types ----------------------------
 
diff --git a/tests/pos-custom-args/captures/dependent-pure.scala b/tests/pos-custom-args/captures/dependent-pure.scala
new file mode 100644
index 000000000000..ad10d9590f25
--- /dev/null
+++ b/tests/pos-custom-args/captures/dependent-pure.scala
@@ -0,0 +1,5 @@
+import language.experimental.captureChecking
+class ContextCls
+type Context = ContextCls^
+
+class Filtered(p: (c: Context) ?-> () ->{c} Boolean) extends Pure

From 95ffd001a8900a6575f1985262e159164a6d008e Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 3 Jul 2023 20:20:40 +0200
Subject: [PATCH 08/14] Don't propagate captures out of curried nested closures

---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 36 +++++++++----------
 .../captures/curried-closures.scala           | 10 ++++++
 2 files changed, 27 insertions(+), 19 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/curried-closures.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 77ca962d2c0d..57b4ae27e7a5 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -12,7 +12,7 @@ import ast.{tpd, untpd, Trees}
 import Trees.*
 import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents, OverridingPairsChecker}
 import typer.Checking.{checkBounds, checkAppliedTypesIn}
-import util.{SimpleIdentitySet, EqHashMap, SrcPos}
+import util.{SimpleIdentitySet, EqHashMap, SrcPos, Property}
 import transform.SymUtils.*
 import transform.{Recheck, PreRecheck}
 import Recheck.*
@@ -145,6 +145,9 @@ object CheckCaptures:
         traverseChildren(t)
     check.traverse(tp)
 
+  /** Attachment key for boxed curried closures */
+  val BoxedClosure = Property.Key[Type]
+
 class CheckCaptures extends Recheck, SymTransformer:
   thisPhase =>
 
@@ -231,29 +234,15 @@ class CheckCaptures extends Recheck, SymTransformer:
         if sym.ownersIterator.exists(_.isTerm) then CaptureSet.Var()
         else CaptureSet.empty)
 
-    /**
-    class anon1 extends Function1:
-      def apply: Function1 =
-        use(x)
-        class anon2 extends Function1:
-          use(y)
-          def apply: Function1 = ...
-        anon2()
-    anon1()
-    */
-    /** For all nested environments up to `limit` perform `op` */
+    /** For all nested environments up to `limit` or a closed environment perform `op` */
     def forallOuterEnvsUpTo(limit: Symbol)(op: Env => Unit)(using Context): Unit =
-      def stopsPropagation(env: Env) =
-        val sym = env.owner
-        env.isOutermost
-        || false && sym.is(Method) && sym.owner.isTerm && !sym.isConstructor
       def recur(env: Env): Unit =
         if env.isOpen && env.owner != limit then
           op(env)
-          if !stopsPropagation(env) then
+          if !env.isOutermost then
             var nextEnv = env.outer
             if env.owner.isConstructor then
-              if nextEnv.owner != limit && !stopsPropagation(nextEnv) then
+              if nextEnv.owner != limit && !nextEnv.isOutermost then
                 nextEnv = nextEnv.outer
             recur(nextEnv)
       recur(curEnv)
@@ -491,6 +480,15 @@ class CheckCaptures extends Recheck, SymTransformer:
                   recheckDef(mdef, meth)
               meth.updateInfoBetween(preRecheckPhase, thisPhase, completer)
             case _ =>
+          mdef.rhs match
+            case rhs @ closure(_, _, _) =>
+              // In a curried closure `x => y => e` don't leak capabilities retained by
+              // the second closure `y => e` into the first one. This is an approximation
+              // of the CC rule which says that a closure contributes captures to its 
+              // environment only if a let-bound reference to the closure is used. 
+              capt.println(i"boxing $rhs")
+              rhs.putAttachment(BoxedClosure, ())
+            case _ =>
         case _ =>
       super.recheckBlock(block, pt)
 
@@ -588,7 +586,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  adding all references in the boxed capture set to the current environment.
      */
     override def recheck(tree: Tree, pt: Type = WildcardType)(using Context): Type =
-      if tree.isTerm && pt.isBoxedCapturing then
+      if tree.isTerm && (pt.isBoxedCapturing || tree.hasAttachment(BoxedClosure)) then
         val saved = curEnv
 
         tree match
diff --git a/tests/pos-custom-args/captures/curried-closures.scala b/tests/pos-custom-args/captures/curried-closures.scala
new file mode 100644
index 000000000000..7258670c295e
--- /dev/null
+++ b/tests/pos-custom-args/captures/curried-closures.scala
@@ -0,0 +1,10 @@
+import java.io.*
+import annotation.capability
+
+def Test4(g: OutputStream^) =
+  val xs: List[Int] = ???
+  val later = (f: OutputStream^) => (y: Int) => xs.foreach(x => f.write(x + y))
+  val _: (f: OutputStream^) ->{} Int ->{f} Unit = later
+
+  val later2 = () => (y: Int) => xs.foreach(x => g.write(x + y))
+  val _: () ->{} Int ->{g} Unit = later2

From 8d99f4ef328a97904bd40b6f3a2e383eed02a5f3 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 4 Jul 2023 12:16:25 +0200
Subject: [PATCH 09/14] Remove curried function types abbreviations

Remove automatic insertion of captured in curried function types from left to right.
They were sometimes confusing and with deep capture sets are counter-productive now.
---
 compiler/src/dotty/tools/dotc/cc/Setup.scala  | 103 +++++-------------
 .../tools/dotc/config/ScalaSettings.scala     |   1 -
 .../captures/curried-simplified.check         |  42 -------
 .../captures/curried-simplified.scala         |  21 ----
 .../captures/curried-closures.scala           |  25 ++++-
 .../captures/curried-shorthands.scala         |  24 ----
 tests/pos-custom-args/captures/i13816.scala   |  15 ++-
 7 files changed, 67 insertions(+), 164 deletions(-)
 delete mode 100644 tests/neg-custom-args/captures/curried-simplified.check
 delete mode 100644 tests/neg-custom-args/captures/curried-simplified.scala
 delete mode 100644 tests/pos-custom-args/captures/curried-shorthands.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 94219da31bdf..f091142f07bc 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -254,19 +254,36 @@ extends tpd.TreeTraverser:
     val tp1 = mapInferred(tp)
     if boxed then box(tp1) else tp1
 
-  /** Expand some aliases of function types to the underlying functions.
-   *  Right now, these are only $throws aliases, but this could be generalized.
-   */
-  private def expandThrowsAlias(tp: Type)(using Context) = tp match
-    case AppliedType(tycon, res :: exc :: Nil) if tycon.typeSymbol == defn.throwsAlias =>
-      // hard-coded expansion since $throws aliases in stdlib are defined with `?=>` rather than `?->`
-      defn.FunctionOf(
-        AnnotatedType(
+  /** Recognizer for `res $throws exc`, returning `(res, exc)` in case of success */
+  object throwsAlias:
+    def unapply(tp: Type)(using Context): Option[(Type, Type)] = tp match
+      case AppliedType(tycon, res :: exc :: Nil) if tycon.typeSymbol == defn.throwsAlias =>
+        Some((res, exc))
+      case _ =>
+        None
+
+  /** Expand $throws aliases. This is hard-coded here since $throws aliases in stdlib
+    * are defined with `?=>` rather than `?->`.
+    * We also have to add a capture set to the last expanded throws alias. I.e.
+    *       T $throws E1 $throws E2
+    * expands to
+    *       (erased x$0: CanThrow[E1]) ?-> (erased x$1: CanThrow[E1]) ?->{x$0} T
+    */
+  private def expandThrowsAlias(tp: Type, encl: List[MethodType] = Nil)(using Context): Type = tp match
+    case throwsAlias(res, exc) =>
+      val paramType = AnnotatedType(
           defn.CanThrowClass.typeRef.appliedTo(exc),
-          Annotation(defn.ErasedParamAnnot, defn.CanThrowClass.span)) :: Nil,
-        res,
-        isContextual = true
-      )
+          Annotation(defn.ErasedParamAnnot, defn.CanThrowClass.span))
+      val isLast = throwsAlias.unapply(res).isEmpty
+      val paramName = nme.syntheticParamName(encl.length)
+      val mt = ContextualMethodType(paramName :: Nil)(
+        _ => paramType :: Nil,
+        mt => if isLast then res else expandThrowsAlias(res, mt :: encl))
+      val fntpe = RefinedType(defn.ErasedFunctionClass.typeRef, nme.apply, mt)
+      if !encl.isEmpty && isLast then
+        val cs = CaptureSet(encl.map(_.paramRefs.head)*)
+        CapturingType(fntpe, cs, boxed = false)
+      else fntpe
     case _ => tp
 
   private def expandThrowsAliases(using Context) = new TypeMap:
@@ -283,70 +300,10 @@ extends tpd.TreeTraverser:
       case _ =>
         mapOver(t)
 
-  /** Fill in capture sets of curried function types from left to right, using
-   *  a combination of the following two rules:
-   *
-   *   1. Expand `{c} (x: A) -> (y: B) -> C`
-   *          to `{c} (x: A) -> {c} (y: B) -> C`
-   *   2. Expand `(x: A) -> (y: B) -> C` where `x` is tracked
-   *          to `(x: A) -> {x} (y: B) -> C`
-   *
-   *  TODO: Should we also propagate capture sets to the left?
-   */
-  private def expandAbbreviations(using Context) = new TypeMap:
-
-    /** Propagate `outerCs` as well as all tracked parameters as capture set to the result type
-     *  of the dependent function type `tp`.
-     */
-    def propagateDepFunctionResult(tp: Type, outerCs: CaptureSet): Type = tp match
-      case RefinedType(parent, nme.apply, rinfo: MethodType) =>
-        val localCs = CaptureSet(rinfo.paramRefs.filter(_.isTracked)*)
-        val rinfo1 = rinfo.derivedLambdaType(
-          resType = propagateEnclosing(rinfo.resType, CaptureSet.empty, outerCs ++ localCs))
-        if rinfo1 ne rinfo then rinfo1.toFunctionType(isJava = false, alwaysDependent = true)
-        else tp
-
-    /** If `tp` is a function type:
-     *   - add `outerCs` as its capture set,
-     *   - propagate `currentCs`, `outerCs`, and all tracked parameters of `tp` to the right.
-     */
-    def propagateEnclosing(tp: Type, currentCs: CaptureSet, outerCs: CaptureSet): Type = tp match
-      case tp @ AppliedType(tycon, args) if defn.isFunctionClass(tycon.typeSymbol) =>
-        val tycon1 = this(tycon)
-        val args1 = args.init.mapConserve(this)
-        val tp1 =
-          if args1.exists(!_.captureSet.isAlwaysEmpty) then
-            val propagated = propagateDepFunctionResult(
-              depFun(tycon, args1, args.last), currentCs ++ outerCs)
-            propagated match
-              case RefinedType(_, _, mt: MethodType) =>
-                if mt.isCaptureDependent then propagated
-                else
-                  // No need to introduce dependent type, switch back to generic function type
-                  tp.derivedAppliedType(tycon1, args1 :+ mt.resType)
-          else
-            val resType1 = propagateEnclosing(
-              args.last, CaptureSet.empty, currentCs ++ outerCs)
-            tp.derivedAppliedType(tycon1, args1 :+ resType1)
-        tp1.capturing(outerCs)
-      case tp @ RefinedType(parent, nme.apply, rinfo: MethodType) if defn.isFunctionType(tp) =>
-        propagateDepFunctionResult(mapOver(tp), currentCs ++ outerCs)
-          .capturing(outerCs)
-      case _ =>
-        mapOver(tp)
-
-    def apply(tp: Type): Type = tp match
-      case CapturingType(parent, cs) =>
-        tp.derivedCapturingType(propagateEnclosing(parent, cs, CaptureSet.empty), cs)
-      case _ =>
-        propagateEnclosing(tp, CaptureSet.empty, CaptureSet.empty)
-  end expandAbbreviations
-
   private def transformExplicitType(tp: Type, boxed: Boolean)(using Context): Type =
     val tp1 = expandThrowsAliases(if boxed then box(tp) else tp)
     if tp1 ne tp then capt.println(i"expanded: $tp --> $tp1")
-    if ctx.settings.YccNoAbbrev.value then tp1
-    else expandAbbreviations(tp1)
+    tp1
 
   /** Transform type of type tree, and remember the transformed type as the type the tree */
   private def transformTT(tree: TypeTree, boxed: Boolean, exact: Boolean)(using Context): Unit =
diff --git a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
index 27389736757a..f1248daefed0 100644
--- a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
+++ b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
@@ -387,7 +387,6 @@ private sealed trait YSettings:
   val YrequireTargetName: Setting[Boolean] = BooleanSetting("-Yrequire-targetName", "Warn if an operator is defined without a @targetName annotation.")
   val YrecheckTest: Setting[Boolean] = BooleanSetting("-Yrecheck-test", "Run basic rechecking (internal test only).")
   val YccDebug: Setting[Boolean] = BooleanSetting("-Ycc-debug", "Used in conjunction with captureChecking language import, debug info for captured references.")
-  val YccNoAbbrev: Setting[Boolean] = BooleanSetting("-Ycc-no-abbrev", "Used in conjunction with captureChecking language import, suppress type abbreviations.")
 
   /** Area-specific debug output */
   val YexplainLowlevel: Setting[Boolean] = BooleanSetting("-Yexplain-lowlevel", "When explaining type errors, show types at a lower level.")
diff --git a/tests/neg-custom-args/captures/curried-simplified.check b/tests/neg-custom-args/captures/curried-simplified.check
deleted file mode 100644
index 6a792314e4e3..000000000000
--- a/tests/neg-custom-args/captures/curried-simplified.check
+++ /dev/null
@@ -1,42 +0,0 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/curried-simplified.scala:7:28 ----------------------------
-7 |  def y1: () -> () -> Int = x1  // error
-  |                            ^^
-  |                            Found:    () ->? () ->{x} Int
-  |                            Required: () -> () -> Int
-  |
-  | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/curried-simplified.scala:9:28 ----------------------------
-9 |  def y2: () -> () => Int = x2 // error
-  |                            ^^
-  |                            Found:    () ->{x} () => Int
-  |                            Required: () -> () => Int
-  |
-  | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/curried-simplified.scala:11:39 ---------------------------
-11 |  def y3: Cap -> Protect[Int -> Int] = x3 // error
-   |                                       ^^
-   |                                       Found:    (x$0: Cap) ->? Int ->{x$0} Int
-   |                                       Required: Cap -> Protect[Int -> Int]
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/curried-simplified.scala:15:32 ---------------------------
-15 |  def y5: Cap -> Int ->{} Int = x5 // error
-   |                                ^^
-   |                                Found:    Cap ->? Int ->{x} Int
-   |                                Required: Cap -> Int ->{} Int
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/curried-simplified.scala:17:48 ---------------------------
-17 |  def y6: Cap -> Cap ->{} Protect[Int -> Int] = x6 // error
-   |                                                ^^
-   |                                                Found:    (x$0: Cap) ->? (x$0: Cap) ->{x$0} Int ->{x$0, x$0} Int
-   |                                                Required: Cap -> Cap ->{} Protect[Int -> Int]
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/curried-simplified.scala:19:48 ---------------------------
-19 |  def y7: Cap -> Protect[Cap -> Int ->{} Int] = x7 // error
-   |                                                ^^
-   |                                                Found:    (x$0: Cap) ->? (x: Cap) ->{x$0} Int ->{x$0, x} Int
-   |                                                Required: Cap -> Protect[Cap -> Int ->{} Int]
-   |
-   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/curried-simplified.scala b/tests/neg-custom-args/captures/curried-simplified.scala
deleted file mode 100644
index 988cf7c11c45..000000000000
--- a/tests/neg-custom-args/captures/curried-simplified.scala
+++ /dev/null
@@ -1,21 +0,0 @@
-@annotation.capability class Cap
-
-type Protect[T] = T
-
-def test(x: Cap, y: Cap) =
-  def x1: () -> () ->{x} Int = ???
-  def y1: () -> () -> Int = x1  // error
-  def x2: () ->{x} () => Int = ???
-  def y2: () -> () => Int = x2 // error
-  def x3: Cap -> Int -> Int = ???
-  def y3: Cap -> Protect[Int -> Int] = x3 // error
-  def x4: Cap -> Protect[Int -> Int] = ???
-  def y4: Cap -> Int ->{} Int = x4 // ok
-  def x5: Cap -> Int ->{x} Int = ???
-  def y5: Cap -> Int ->{} Int = x5 // error
-  def x6: Cap -> Cap -> Int -> Int = ???
-  def y6: Cap -> Cap ->{} Protect[Int -> Int] = x6 // error
-  def x7: Cap -> (x: Cap) -> Int -> Int = ???
-  def y7: Cap -> Protect[Cap -> Int ->{} Int] = x7 // error
-
-
diff --git a/tests/pos-custom-args/captures/curried-closures.scala b/tests/pos-custom-args/captures/curried-closures.scala
index 7258670c295e..baea8b15075c 100644
--- a/tests/pos-custom-args/captures/curried-closures.scala
+++ b/tests/pos-custom-args/captures/curried-closures.scala
@@ -1,6 +1,26 @@
-import java.io.*
-import annotation.capability
+object Test:
+  def map2(xs: List[Int])(f: Int => Int): List[Int] = xs.map(f)
+  val f1 = map2
+  val fc1: List[Int] -> (Int => Int) -> List[Int] = f1
+
+  def map3(f: Int => Int)(xs: List[Int]): List[Int] = xs.map(f)
+  private val f2 = map3
+  val fc2: (f: Int => Int) -> List[Int] ->{f} List[Int] = f2
+
+  val f3 = (f: Int => Int) =>
+    println(f(3))
+    (xs: List[Int]) => xs.map(_ + 1)
+  val f3c: (Int => Int) -> List[Int] -> List[Int] = f3
+
+  class LL[A]:
+    def drop(n: Int): LL[A]^{this} = ???
 
+  def test(ct: CanThrow[Exception]) =
+    def xs: LL[Int]^{ct} = ???
+    val ys = xs.drop(_)
+    val ysc: Int -> LL[Int]^{ct} = ys
+
+import java.io.*
 def Test4(g: OutputStream^) =
   val xs: List[Int] = ???
   val later = (f: OutputStream^) => (y: Int) => xs.foreach(x => f.write(x + y))
@@ -8,3 +28,4 @@ def Test4(g: OutputStream^) =
 
   val later2 = () => (y: Int) => xs.foreach(x => g.write(x + y))
   val _: () ->{} Int ->{g} Unit = later2
+
diff --git a/tests/pos-custom-args/captures/curried-shorthands.scala b/tests/pos-custom-args/captures/curried-shorthands.scala
deleted file mode 100644
index c68dc4b5cdbf..000000000000
--- a/tests/pos-custom-args/captures/curried-shorthands.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-object Test:
-  def map2(xs: List[Int])(f: Int => Int): List[Int] = xs.map(f)
-  val f1 = map2
-  val fc1: List[Int] -> (Int => Int) -> List[Int] = f1
-
-  def map3(f: Int => Int)(xs: List[Int]): List[Int] = xs.map(f)
-  private val f2 = map3
-  val fc2: (Int => Int) -> List[Int] -> List[Int] = f2
-
-  val f3 = (f: Int => Int) =>
-    println(f(3))
-    (xs: List[Int]) => xs.map(_ + 1)
-  val f3c: (Int => Int) -> List[Int] ->{} List[Int] = f3
-
-  class LL[A]:
-    def drop(n: Int): LL[A]^{this} = ???
-
-  def test(ct: CanThrow[Exception]) =
-    def xs: LL[Int]^{ct} = ???
-    val ys = xs.drop(_)
-    val ysc: Int -> LL[Int]^{ct} = ys
-
-
-
diff --git a/tests/pos-custom-args/captures/i13816.scala b/tests/pos-custom-args/captures/i13816.scala
index 235afef35f1c..9d897b0f4601 100644
--- a/tests/pos-custom-args/captures/i13816.scala
+++ b/tests/pos-custom-args/captures/i13816.scala
@@ -2,12 +2,16 @@ import language.experimental.saferExceptions
 
 class Ex1 extends Exception("Ex1")
 class Ex2 extends Exception("Ex2")
+class Ex3 extends Exception("Ex3")
 
 def foo0(i: Int): (CanThrow[Ex1], CanThrow[Ex2]) ?-> Unit =
   if i > 0 then throw new Ex1 else throw new Ex2
 
-def foo01(i: Int): CanThrow[Ex1] ?-> CanThrow[Ex2] ?-> Unit =
+/* Does not work yet since annotated CFTs are not recognized properly in typer
+
+def foo01(i: Int): (ct: CanThrow[Ex1]) ?-> CanThrow[Ex2] ?->{ct} Unit =
   if i > 0 then throw new Ex1 else throw new Ex2
+*/
 
 def foo1(i: Int): Unit throws Ex1 throws Ex2 =
   if i > 0 then throw new Ex1 else throw new Ex1
@@ -33,6 +37,15 @@ def foo7(i: Int)(using CanThrow[Ex1]): Unit throws Ex1 | Ex2 =
 def foo8(i: Int)(using CanThrow[Ex2]): Unit throws Ex2 | Ex1 =
   if i > 0 then throw new Ex1 else throw new Ex2
 
+/** Does not work yet since the type of the rhs is not hygienic
+
+def foo9(i: Int): Unit throws Ex1 | Ex2 | Ex3 =
+  if i > 0 then throw new Ex1
+  else if i < 0 then throw new Ex2
+  else throw new Ex3
+
+*/
+
 def test(): Unit =
   try
     foo1(1)

From 9000aa88156c5ee906292011173fd8c83682c4b9 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Wed, 5 Jul 2023 19:18:36 +0200
Subject: [PATCH 10/14] Fix comment

---
 tests/pos-custom-args/captures/i13816.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/pos-custom-args/captures/i13816.scala b/tests/pos-custom-args/captures/i13816.scala
index 9d897b0f4601..b6e15023752b 100644
--- a/tests/pos-custom-args/captures/i13816.scala
+++ b/tests/pos-custom-args/captures/i13816.scala
@@ -7,7 +7,7 @@ class Ex3 extends Exception("Ex3")
 def foo0(i: Int): (CanThrow[Ex1], CanThrow[Ex2]) ?-> Unit =
   if i > 0 then throw new Ex1 else throw new Ex2
 
-/* Does not work yet since annotated CFTs are not recognized properly in typer
+/* Does not work yet curried dependent CFTs are not yet handled in typer
 
 def foo01(i: Int): (ct: CanThrow[Ex1]) ?-> CanThrow[Ex2] ?->{ct} Unit =
   if i > 0 then throw new Ex1 else throw new Ex2

From 49668d0b4fae77c18afa953c5887c3e940de146d Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 8 Jul 2023 19:26:09 +0200
Subject: [PATCH 11/14] Fix handling of singleton types

 - Don't widen actual in adaptBoxed if expected is a singleton type
 - Don't allow singleton types with capture sets (the theory does not
   allow them either)
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 40 +++++++++++--------
 .../src/dotty/tools/dotc/typer/Typer.scala    |  2 +-
 .../neg-custom-args/captures/singletons.scala |  6 +++
 3 files changed, 31 insertions(+), 17 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/singletons.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 57b4ae27e7a5..d8ce25f047fe 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -94,7 +94,11 @@ object CheckCaptures:
   /** Check that a @retains annotation only mentions references that can be tracked.
    *  This check is performed at Typer.
    */
-  def checkWellformed(ann: Tree)(using Context): Unit =
+  def checkWellformed(parent: Tree, ann: Tree)(using Context): Unit =
+    parent.tpe match
+      case _: SingletonType =>
+        report.error(em"Singleton type $parent cannot have capture set", parent.srcPos)
+      case _ =>
     for elem <- retainedElems(ann) do
       elem.tpe match
         case ref: CaptureRef =>
@@ -848,21 +852,25 @@ class CheckCaptures extends Recheck, SymTransformer:
             adaptedType(boxed)
       }
 
-      var actualw = actual.widenDealias
-      actual match
-        case ref: CaptureRef if ref.isTracked =>
-          actualw match
-            case CapturingType(p, refs) if ref.singletonCaptureSet.mightSubcapture(refs) =>
-              actualw = actualw.derivedCapturingType(p, ref.singletonCaptureSet)
-                .showing(i"improve $actualw to $result", capt)
-                // given `a: C T`, improve `C T` to `{a} T`
-            case _ =>
-        case _ =>
-      val adapted = adapt(actualw, expected, covariant = true)
-      if adapted ne actualw then
-        capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
-        adapted
-      else actual
+      if expected.isSingleton && actual.isSingleton then
+        println(i"shot $actual $expected")
+        actual
+      else
+        var actualw = actual.widenDealias
+        actual match
+          case ref: CaptureRef if ref.isTracked =>
+            actualw match
+              case CapturingType(p, refs) if ref.singletonCaptureSet.mightSubcapture(refs) =>
+                actualw = actualw.derivedCapturingType(p, ref.singletonCaptureSet)
+                  .showing(i"improve $actualw to $result", capt)
+                  // given `a: T^C`, improve `T^C` to `T^{a}`
+              case _ =>
+          case _ =>
+        val adapted = adapt(actualw, expected, covariant = true)
+        if adapted ne actualw then
+          capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
+          adapted
+        else actual
     end adaptBoxed
 
     /** Check overrides again, taking capture sets into account.
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index c7e413ddb863..6ede4b883c64 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -2897,7 +2897,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
       if Feature.ccEnabled
           && (cls == defn.RetainsAnnot || cls == defn.RetainsByNameAnnot)
       then
-        CheckCaptures.checkWellformed(annot1)
+        CheckCaptures.checkWellformed(arg1, annot1)
       if arg1.isType then
         assignType(cpy.Annotated(tree)(arg1, annot1), arg1, annot1)
       else
diff --git a/tests/neg-custom-args/captures/singletons.scala b/tests/neg-custom-args/captures/singletons.scala
new file mode 100644
index 000000000000..733c771e8b2c
--- /dev/null
+++ b/tests/neg-custom-args/captures/singletons.scala
@@ -0,0 +1,6 @@
+val x = () => ()
+
+val y1: x.type = x          // ok
+val y2: x.type^{} = x       // error: singleton type cannot have capture set
+val y3: x.type^{x} = x      // error: singleton type cannot have capture set // error
+val y4: x.type^{cap} = x    // error: singleton type cannot have capture set

From fb3df0cc768e55ed2d5609b1f59f891fc6594e10 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 14 Jul 2023 12:36:02 +0200
Subject: [PATCH 12/14] Drop redundant statements

# Conflicts:
#	compiler/src/dotty/tools/dotc/transform/Pickler.scala
---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index d8ce25f047fe..ed12251351d1 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -488,8 +488,8 @@ class CheckCaptures extends Recheck, SymTransformer:
             case rhs @ closure(_, _, _) =>
               // In a curried closure `x => y => e` don't leak capabilities retained by
               // the second closure `y => e` into the first one. This is an approximation
-              // of the CC rule which says that a closure contributes captures to its 
-              // environment only if a let-bound reference to the closure is used. 
+              // of the CC rule which says that a closure contributes captures to its
+              // environment only if a let-bound reference to the closure is used.
               capt.println(i"boxing $rhs")
               rhs.putAttachment(BoxedClosure, ())
             case _ =>
@@ -853,7 +853,6 @@ class CheckCaptures extends Recheck, SymTransformer:
       }
 
       if expected.isSingleton && actual.isSingleton then
-        println(i"shot $actual $expected")
         actual
       else
         var actualw = actual.widenDealias

From 482dc782a9e1eabd5fdd4e2c2b17d9dfec1be33c Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 14 Jul 2023 11:15:00 +0200
Subject: [PATCH 13/14] Refactoring: Add EnvKind to replace boolean fields in
 Env

---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 39 +++++++++++--------
 1 file changed, 22 insertions(+), 17 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index ed12251351d1..e8f826edeb5f 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -43,19 +43,24 @@ object CheckCaptures:
         sym
   end Pre
 
+  enum EnvKind:
+    case Regular        // normal case
+    case NestedInOwner  // environment is  a temporary one nested in the owner's environment,
+                        // and does not have a different actual owner symbol
+                        // (this happens when doing box adaptation).
+    case ClosureResult  // environment is for the result of a closure
+    case Boxed          // envrionment is inside a box (in which case references are not counted)
+
   /** A class describing environments.
-   *  @param owner         the current owner
-   *  @param nestedInOwner true if the environment is a temporary one nested in the owner's environment,
-   *                       and does not have a different actual owner symbol (this happens when doing box adaptation).
-   *  @param captured      the caputure set containing all references to tracked free variables outside of boxes
-   *  @param isBoxed       true if the environment is inside a box (in which case references are not counted)
-   *  @param outer0        the next enclosing environment
+   *  @param owner     the current owner
+   *  @param kind      the environment's kind
+   *  @param captured  the caputure set containing all references to tracked free variables outside of boxes
+   *  @param outer0    the next enclosing environment
    */
   case class Env(
       owner: Symbol,
-      nestedInOwner: Boolean,
+      kind: EnvKind,
       captured: CaptureSet,
-      isBoxed: Boolean,
       outer0: Env | Null):
 
     def outer = outer0.nn
@@ -63,7 +68,7 @@ object CheckCaptures:
     def isOutermost = outer0 == null
 
     /** If an environment is open it tracks free references */
-    def isOpen = !captured.isAlwaysEmpty && !isBoxed
+    def isOpen = !captured.isAlwaysEmpty && kind != EnvKind.Boxed
   end Env
 
   /** Similar normal substParams, but this is an approximating type map that
@@ -226,7 +231,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         report.error(em"$header included in allowed capture set ${res.blocking}", pos)
 
     /** The current environment */
-    private var curEnv: Env = Env(NoSymbol, nestedInOwner = false, CaptureSet.empty, isBoxed = false, null)
+    private var curEnv: Env = Env(NoSymbol, EnvKind.Regular, CaptureSet.empty, null)
 
     private val myCapturedVars: util.EqHashMap[Symbol, CaptureSet] = EqHashMap()
 
@@ -270,7 +275,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       if !cs.isAlwaysEmpty then
         forallOuterEnvsUpTo(ctx.owner.topLevelClass): env =>
           def isVisibleFromEnv(sym: Symbol) =
-            (env.nestedInOwner || env.owner != sym)
+            (env.kind == EnvKind.NestedInOwner || env.owner != sym)
             && env.owner.isContainedIn(sym)
           val included = cs.filter:
             case ref: TermRef => isVisibleFromEnv(ref.symbol.owner)
@@ -512,7 +517,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       if !Synthetics.isExcluded(sym) then
         val saved = curEnv
         val localSet = capturedVars(sym)
-        if !localSet.isAlwaysEmpty then curEnv = Env(sym, nestedInOwner = false, localSet, isBoxed = false, curEnv)
+        if !localSet.isAlwaysEmpty then curEnv = Env(sym, EnvKind.Regular, localSet, curEnv)
         try super.recheckDefDef(tree, sym)
         finally
           interpolateVarsIn(tree.tpt)
@@ -530,7 +535,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       val localSet = capturedVars(cls)
       for parent <- impl.parents do // (1)
         checkSubset(capturedVars(parent.tpe.classSymbol), localSet, parent.srcPos)
-      if !localSet.isAlwaysEmpty then curEnv = Env(cls, nestedInOwner = false, localSet, isBoxed = false, curEnv)
+      if !localSet.isAlwaysEmpty then curEnv = Env(cls, EnvKind.Regular, localSet, curEnv)
       try
         val thisSet = cls.classInfo.selfType.captureSet.withDescription(i"of the self type of $cls")
         checkSubset(localSet, thisSet, tree.srcPos) // (2)
@@ -595,7 +600,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
         tree match
           case _: RefTree | closureDef(_) =>
-            curEnv = Env(curEnv.owner, nestedInOwner = false, CaptureSet.Var(), isBoxed = true, curEnv)
+            curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(), curEnv)
           case _ =>
 
         try super.recheck(tree, pt)
@@ -729,7 +734,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           covariant: Boolean, boxed: Boolean,
           reconstruct: (List[Type], Type) => Type): (Type, CaptureSet) =
         val saved = curEnv
-        curEnv = Env(curEnv.owner, nestedInOwner = true, CaptureSet.Var(), isBoxed = false, if boxed then null else curEnv)
+        curEnv = Env(curEnv.owner, EnvKind.NestedInOwner, CaptureSet.Var(), if boxed then null else curEnv)
 
         try
           val (eargs, eres) = expected.dealias.stripCapturing match
@@ -756,7 +761,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           covariant: Boolean, boxed: Boolean,
           reconstruct: Type => Type): (Type, CaptureSet) =
         val saved = curEnv
-        curEnv = Env(curEnv.owner, nestedInOwner = true, CaptureSet.Var(), isBoxed = false, if boxed then null else curEnv)
+        curEnv = Env(curEnv.owner, EnvKind.NestedInOwner, CaptureSet.Var(), if boxed then null else curEnv)
 
         try
           val eres = expected.dealias.stripCapturing match
@@ -888,7 +893,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           val actual1 =
             val saved = curEnv
             try
-              curEnv = Env(clazz, nestedInOwner = true, capturedVars(clazz), isBoxed = false, outer0 = curEnv)
+              curEnv = Env(clazz, EnvKind.NestedInOwner, capturedVars(clazz), outer0 = curEnv)
               val adapted = adaptBoxed(actual, expected1, srcPos, alwaysConst = true)
               actual match
                 case _: MethodType =>

From c7a5350d338a3df89b913170b36df45e5f436850 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 14 Jul 2023 12:31:19 +0200
Subject: [PATCH 14/14] Fix leaking problem detected in review

---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 42 +++++++++----------
 .../captures/leaked-curried.check             |  4 ++
 .../captures/leaked-curried.scala             | 14 +++++++
 3 files changed, 39 insertions(+), 21 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/leaked-curried.check
 create mode 100644 tests/neg-custom-args/captures/leaked-curried.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index e8f826edeb5f..c8c1180abd51 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -154,8 +154,8 @@ object CheckCaptures:
         traverseChildren(t)
     check.traverse(tp)
 
-  /** Attachment key for boxed curried closures */
-  val BoxedClosure = Property.Key[Type]
+  /** Attachment key for bodies of closures, provided they are values */
+  val ClosureBodyValue = Property.Key[Unit]
 
 class CheckCaptures extends Recheck, SymTransformer:
   thisPhase =>
@@ -243,18 +243,20 @@ class CheckCaptures extends Recheck, SymTransformer:
         if sym.ownersIterator.exists(_.isTerm) then CaptureSet.Var()
         else CaptureSet.empty)
 
-    /** For all nested environments up to `limit` or a closed environment perform `op` */
+    /** For all nested environments up to `limit` or a closed environment perform `op`,
+     *  but skip environmenrts directly enclosing environments of kind ClosureResult.
+     */
     def forallOuterEnvsUpTo(limit: Symbol)(op: Env => Unit)(using Context): Unit =
-      def recur(env: Env): Unit =
+      def recur(env: Env, skip: Boolean): Unit =
         if env.isOpen && env.owner != limit then
-          op(env)
+          if !skip then op(env)
           if !env.isOutermost then
             var nextEnv = env.outer
             if env.owner.isConstructor then
               if nextEnv.owner != limit && !nextEnv.isOutermost then
                 nextEnv = nextEnv.outer
-            recur(nextEnv)
-      recur(curEnv)
+            recur(nextEnv, skip = env.kind == EnvKind.ClosureResult)
+      recur(curEnv, skip = false)
 
     /** Include `sym` in the capture sets of all enclosing environments nested in the
      *  the environment in which `sym` is defined.
@@ -495,8 +497,7 @@ class CheckCaptures extends Recheck, SymTransformer:
               // the second closure `y => e` into the first one. This is an approximation
               // of the CC rule which says that a closure contributes captures to its
               // environment only if a let-bound reference to the closure is used.
-              capt.println(i"boxing $rhs")
-              rhs.putAttachment(BoxedClosure, ())
+              mdef.rhs.putAttachment(ClosureBodyValue, ())
             case _ =>
         case _ =>
       super.recheckBlock(block, pt)
@@ -595,20 +596,19 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  adding all references in the boxed capture set to the current environment.
      */
     override def recheck(tree: Tree, pt: Type = WildcardType)(using Context): Type =
-      if tree.isTerm && (pt.isBoxedCapturing || tree.hasAttachment(BoxedClosure)) then
-        val saved = curEnv
-
-        tree match
-          case _: RefTree | closureDef(_) =>
-            curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(), curEnv)
-          case _ =>
-
+      val saved = curEnv
+      tree match
+        case _: RefTree | closureDef(_) if pt.isBoxedCapturing =>
+          curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(), curEnv)
+        case _ if tree.hasAttachment(ClosureBodyValue) =>
+          curEnv = Env(curEnv.owner, EnvKind.ClosureResult, CaptureSet.Var(), curEnv)
+        case _ =>
+      val res =
         try super.recheck(tree, pt)
         finally curEnv = saved
-      else
-        val res = super.recheck(tree, pt)
-        if tree.isTerm then markFree(res.boxedCaptureSet, tree.srcPos)
-        res
+      if tree.isTerm && !pt.isBoxedCapturing then
+        markFree(res.boxedCaptureSet, tree.srcPos)
+      res
 
     /** If `tree` is a reference or an application where the result type refers
      *  to an enclosing class or method parameter of the reference, check that the result type
diff --git a/tests/neg-custom-args/captures/leaked-curried.check b/tests/neg-custom-args/captures/leaked-curried.check
new file mode 100644
index 000000000000..590f871c57d5
--- /dev/null
+++ b/tests/neg-custom-args/captures/leaked-curried.check
@@ -0,0 +1,4 @@
+-- Error: tests/neg-custom-args/captures/leaked-curried.scala:12:52 ----------------------------------------------------
+12 |      val get: () ->{} () ->{io} Cap^ = () => () => io // error
+   |                                                    ^^
+   |(io : Cap^) cannot be referenced here; it is not included in the allowed capture set {} of pure base class trait Pure
diff --git a/tests/neg-custom-args/captures/leaked-curried.scala b/tests/neg-custom-args/captures/leaked-curried.scala
new file mode 100644
index 000000000000..000f2ef72cb0
--- /dev/null
+++ b/tests/neg-custom-args/captures/leaked-curried.scala
@@ -0,0 +1,14 @@
+trait Cap:
+  def use(): Unit
+
+def withCap[sealed T](op: (x: Cap^) => T): T = ???
+
+trait Box:
+  val get: () ->{} () ->{cap} Cap^
+
+def main(): Unit =
+  val leaked = withCap: (io: Cap^) =>
+    class Foo extends Box, Pure:
+      val get: () ->{} () ->{io} Cap^ = () => () => io // error
+    new Foo
+  val bad = leaked.get()().use()  // using a leaked capability