From 1cc5cf3cef29aca64e8870240b8da001fd026678 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 17 Aug 2021 13:02:09 +0200
Subject: [PATCH 01/25] Cleanups

---
 compiler/src/dotty/tools/dotc/Compiler.scala             | 4 ++--
 compiler/src/dotty/tools/dotc/typer/RefineTypes.overflow | 0
 2 files changed, 2 insertions(+), 2 deletions(-)
 delete mode 100644 compiler/src/dotty/tools/dotc/typer/RefineTypes.overflow

diff --git a/compiler/src/dotty/tools/dotc/Compiler.scala b/compiler/src/dotty/tools/dotc/Compiler.scala
index 1f5302fe6198..1337457c273b 100644
--- a/compiler/src/dotty/tools/dotc/Compiler.scala
+++ b/compiler/src/dotty/tools/dotc/Compiler.scala
@@ -101,8 +101,8 @@ class Compiler {
          new TupleOptimizations,     // Optimize generic operations on tuples
          new LetOverApply,           // Lift blocks from receivers of applications
          new ArrayConstructors) ::   // Intercept creation of (non-generic) arrays and intrinsify.
-    List(new PreRecheck) ::
-    List(new TestRecheck) ::
+    List(new PreRecheck) ::          // Preparations for recheck phase, enabled under -Yrecheck
+    List(new TestRecheck) ::         // Test rechecking, enabled under -Yrecheck
     List(new Erasure) ::             // Rewrite types to JVM model, erasing all type parameters, abstract types and refinements.
     List(new ElimErasedValueType,    // Expand erased value types to their underlying implmementation types
          new PureStats,              // Remove pure stats from blocks
diff --git a/compiler/src/dotty/tools/dotc/typer/RefineTypes.overflow b/compiler/src/dotty/tools/dotc/typer/RefineTypes.overflow
deleted file mode 100644
index e69de29bb2d1..000000000000

From 418368574b2d5cfd22f00affc3e98fdab648f20a Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sat, 26 Jun 2021 10:48:59 +0200
Subject: [PATCH 02/25] Support for CapturingTypes

---
 compiler/src/dotty/tools/dotc/ast/Trees.scala |   8 +-
 .../dotty/tools/dotc/config/Printers.scala    |   1 +
 .../tools/dotc/config/ScalaSettings.scala     |   1 +
 .../dotty/tools/dotc/core/CaptureSet.scala    | 127 +++++++++++
 .../dotty/tools/dotc/core/Definitions.scala   |  15 +-
 compiler/src/dotty/tools/dotc/core/Mode.scala |   2 +
 .../tools/dotc/core/OrderingConstraint.scala  |   3 +
 .../src/dotty/tools/dotc/core/StdNames.scala  |   4 +-
 .../tools/dotc/core/SymDenotations.scala      |   8 +-
 .../dotty/tools/dotc/core/TypeComparer.scala  |  49 ++++-
 .../src/dotty/tools/dotc/core/TypeOps.scala   |  21 +-
 .../src/dotty/tools/dotc/core/Types.scala     | 200 +++++++++++++++---
 .../src/dotty/tools/dotc/core/Variances.scala |   2 +
 .../tools/dotc/core/tasty/TreePickler.scala   |   7 +
 .../tools/dotc/core/tasty/TreeUnpickler.scala |  18 +-
 .../tools/dotc/printing/PlainPrinter.scala    |   7 +
 .../dotty/tools/dotc/printing/Printer.scala   |   3 +
 .../src/dotty/tools/dotc/sbt/ExtractAPI.scala |   4 +
 .../dotc/transform/GenericSignatures.scala    |  10 +-
 .../tools/dotc/transform/TreeChecker.scala    |   4 +-
 .../dotc/transform/TryCatchPatterns.scala     |   2 +-
 .../tools/dotc/transform/TypeTestsCasts.scala |   4 +-
 .../src/dotty/tools/dotc/typer/Checking.scala |  13 +-
 .../dotty/tools/dotc/typer/Inferencing.scala  |   5 +-
 .../dotty/tools/dotc/typer/TypeAssigner.scala |  47 +++-
 library/src-bootstrapped/scala/Retains.scala  |   7 +
 .../scala/annotation/ability.scala            |   8 +
 .../scala/runtime/stdLibPatches/Predef.scala  |   4 +
 28 files changed, 498 insertions(+), 86 deletions(-)
 create mode 100644 compiler/src/dotty/tools/dotc/core/CaptureSet.scala
 create mode 100644 library/src-bootstrapped/scala/Retains.scala
 create mode 100644 library/src-bootstrapped/scala/annotation/ability.scala

diff --git a/compiler/src/dotty/tools/dotc/ast/Trees.scala b/compiler/src/dotty/tools/dotc/ast/Trees.scala
index 5bdd18705051..267c6b114a8c 100644
--- a/compiler/src/dotty/tools/dotc/ast/Trees.scala
+++ b/compiler/src/dotty/tools/dotc/ast/Trees.scala
@@ -260,16 +260,10 @@ object Trees {
   /** Tree's denotation can be derived from its type */
   abstract class DenotingTree[-T >: Untyped](implicit @constructorOnly src: SourceFile) extends Tree[T] {
     type ThisTree[-T >: Untyped] <: DenotingTree[T]
-    override def denot(using Context): Denotation = typeOpt match {
+    override def denot(using Context): Denotation = typeOpt.stripped match
       case tpe: NamedType => tpe.denot
       case tpe: ThisType => tpe.cls.denot
-      case tpe: AnnotatedType => tpe.stripAnnots match {
-        case tpe: NamedType => tpe.denot
-        case tpe: ThisType => tpe.cls.denot
-        case _ => NoDenotation
-      }
       case _ => NoDenotation
-    }
   }
 
   /** Tree's denot/isType/isTerm properties come from a subtree
diff --git a/compiler/src/dotty/tools/dotc/config/Printers.scala b/compiler/src/dotty/tools/dotc/config/Printers.scala
index b71e1e7f188a..d20d482b062e 100644
--- a/compiler/src/dotty/tools/dotc/config/Printers.scala
+++ b/compiler/src/dotty/tools/dotc/config/Printers.scala
@@ -12,6 +12,7 @@ object Printers {
 
   val default = new Printer
 
+  val capt = noPrinter
   val constr = noPrinter
   val core = noPrinter
   val checks = noPrinter
diff --git a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
index fcd6bcb34b2e..18e816f0f92f 100644
--- a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
+++ b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
@@ -239,6 +239,7 @@ private sealed trait YSettings:
   val YcheckInit: Setting[Boolean] = BooleanSetting("-Ysafe-init", "Ensure safe initialization of objects")
   val YrequireTargetName: Setting[Boolean] = BooleanSetting("-Yrequire-targetName", "Warn if an operator is defined without a @targetName annotation")
   val Yrecheck: Setting[Boolean] = BooleanSetting("-Yrecheck", "Run type rechecks (test only)")
+  val Ycc: Setting[Boolean] = BooleanSetting("-Ycc", "Check captured references")
 
   /** Area-specific debug output */
   val YexplainLowlevel: Setting[Boolean] = BooleanSetting("-Yexplain-lowlevel", "When explaining type errors, show types at a lower level.")
diff --git a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
new file mode 100644
index 000000000000..d28d271fc3b9
--- /dev/null
+++ b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
@@ -0,0 +1,127 @@
+package dotty.tools
+package dotc
+package core
+
+import util.*
+import Types.*, Symbols.*, Flags.*, Contexts.*, Decorators.*
+import config.Printers.capt
+import annotation.threadUnsafe
+import annotation.internal.sharable
+import reporting.trace
+import printing.{Showable, Printer}
+import printing.Texts.*
+
+case class CaptureSet private (elems: CaptureSet.Refs) extends Showable:
+  import CaptureSet.*
+
+  def isEmpty: Boolean = elems.isEmpty
+  def nonEmpty: Boolean = !isEmpty
+
+  private var myClosure: Refs | Null = null
+
+  def closure(using Context): Refs =
+    if myClosure == null then
+      var cl = elems
+      var seen: Refs = SimpleIdentitySet.empty
+      while
+        val prev = cl
+        for ref <- cl do
+          if !seen.contains(ref) then
+            seen += ref
+            cl = cl ++ ref.captureSetOfInfo.elems
+        prev ne cl
+      do ()
+      myClosure = cl
+    myClosure
+
+  def ++ (that: CaptureSet): CaptureSet =
+    if this.isEmpty then that
+    else if that.isEmpty then this
+    else CaptureSet(elems ++ that.elems)
+
+  def + (ref: CaptureRef) =
+    if elems.contains(ref) then this
+    else CaptureSet(elems + ref)
+
+  def intersect (that: CaptureSet): CaptureSet =
+    CaptureSet(this.elems.intersect(that.elems))
+
+  /** {x} <:< this   where <:< is subcapturing */
+  def accountsFor(x: CaptureRef)(using Context) =
+    elems.contains(x) || !x.isRootCapability && x.captureSetOfInfo <:< this
+
+  /** The subcapturing test */
+  def <:< (that: CaptureSet)(using Context): Boolean =
+    elems.isEmpty || elems.forall(that.accountsFor)
+
+  def flatMap(f: CaptureRef => CaptureSet)(using Context): CaptureSet =
+    (empty /: elems)((cs, ref) => cs ++ f(ref))
+
+  def substParams(tl: BindingType, to: List[Type])(using Context) =
+    flatMap {
+      case ref: ParamRef if ref.binder eq tl => to(ref.paramNum).captureSet
+      case ref => ref.singletonCaptureSet
+    }
+
+  override def toString = elems.toString
+
+  override def toText(printer: Printer): Text =
+    Str("{") ~ Text(elems.toList.map(printer.toTextCaptureRef), ", ") ~ Str("}")
+
+object CaptureSet:
+  type Refs = SimpleIdentitySet[CaptureRef]
+
+   @sharable val empty: CaptureSet = CaptureSet(SimpleIdentitySet.empty)
+
+  /** Used as a recursion brake */
+  @sharable private[core] val Pending = CaptureSet(SimpleIdentitySet.empty)
+
+  def apply(elems: CaptureRef*)(using Context): CaptureSet =
+    if elems.isEmpty then empty
+    else CaptureSet(SimpleIdentitySet(elems.map(_.normalizedRef)*))
+
+  def ofClass(cinfo: ClassInfo, argTypes: List[Type])(using Context): CaptureSet =
+    def captureSetOf(tp: Type): CaptureSet = tp match
+      case tp: TypeRef if tp.symbol.is(ParamAccessor) =>
+        def mapArg(accs: List[Symbol], tps: List[Type]): CaptureSet = accs match
+          case acc :: accs1 if tps.nonEmpty =>
+            if acc == tp.symbol then tps.head.captureSet
+            else mapArg(accs1, tps.tail)
+          case _ =>
+            empty
+        mapArg(cinfo.cls.paramAccessors, argTypes)
+      case _ =>
+        tp.captureSet
+    val css =
+      for
+        parent <- cinfo.parents if parent.classSymbol == defn.RetainsClass
+        arg <- parent.argInfos
+      yield captureSetOf(arg)
+    css.foldLeft(empty)(_ ++ _)
+
+  def ofType(tp: Type)(using Context): CaptureSet =
+    def recur(tp: Type): CaptureSet = tp match
+      case tp: NamedType =>
+        tp.captureSet
+      case tp: ParamRef =>
+        tp.captureSet
+      case CapturingType(parent, ref) =>
+        recur(parent) + ref
+      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).intersect(recur(tp2))
+      case OrType(tp1, tp2) =>
+        recur(tp1) ++ recur(tp2)
+      case tp: ClassInfo =>
+        ofClass(tp, Nil)
+      case _ =>
+        empty
+    recur(tp)
+      .showing(i"capture set of $tp = $result", capt)
+
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 7c1c2494d323..12576840671e 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -143,11 +143,13 @@ class Definitions {
   private def enterMethod(cls: ClassSymbol, name: TermName, info: Type, flags: FlagSet = EmptyFlags): TermSymbol =
     newMethod(cls, name, info, flags).entered
 
-  private def enterAliasType(name: TypeName, tpe: Type, flags: FlagSet = EmptyFlags): TypeSymbol = {
-    val sym = newPermanentSymbol(ScalaPackageClass, name, flags, TypeAlias(tpe))
+  private def enterType(name: TypeName, info: Type, flags: FlagSet = EmptyFlags): TypeSymbol =
+    val sym = newPermanentSymbol(ScalaPackageClass, name, flags, info)
     ScalaPackageClass.currentPackageDecls.enter(sym)
     sym
-  }
+
+  private def enterAliasType(name: TypeName, tpe: Type, flags: FlagSet = EmptyFlags): TypeSymbol =
+    enterType(name, TypeAlias(tpe), flags)
 
   private def enterBinaryAlias(name: TypeName, op: (Type, Type) => Type): TypeSymbol =
     enterAliasType(name,
@@ -262,6 +264,7 @@ class Definitions {
    */
   @tu lazy val AnyClass: ClassSymbol = completeClass(enterCompleteClassSymbol(ScalaPackageClass, tpnme.Any, Abstract, Nil), ensureCtor = false)
   def AnyType: TypeRef = AnyClass.typeRef
+  @tu lazy val TopType: Type = CapturingType(AnyType, captureRootType.typeRef)
   @tu lazy val MatchableClass: ClassSymbol = completeClass(enterCompleteClassSymbol(ScalaPackageClass, tpnme.Matchable, Trait, AnyType :: Nil), ensureCtor = false)
   def MatchableType: TypeRef = MatchableClass.typeRef
   @tu lazy val AnyValClass: ClassSymbol =
@@ -440,6 +443,7 @@ class Definitions {
 
   @tu lazy val andType: TypeSymbol = enterBinaryAlias(tpnme.AND, AndType(_, _))
   @tu lazy val orType: TypeSymbol = enterBinaryAlias(tpnme.OR, OrType(_, _, soft = false))
+  @tu lazy val captureRootType: TypeSymbol = enterType(tpnme.CAPTURE_ROOT, TypeBounds.empty, Deferred)
 
   /** Marker method to indicate an argument to a call-by-name parameter.
    *  Created by byNameClosures and elimByName, eliminated by Erasure,
@@ -470,6 +474,7 @@ class Definitions {
     @tu lazy val Predef_classOf  : Symbol = ScalaPredefModule.requiredMethod(nme.classOf)
     @tu lazy val Predef_identity : Symbol = ScalaPredefModule.requiredMethod(nme.identity)
     @tu lazy val Predef_undefined: Symbol = ScalaPredefModule.requiredMethod(nme.???)
+    @tu lazy val Predef_retainsType: Symbol = ScalaPredefModule.requiredType(tpnme.retains)
   @tu lazy val ScalaPredefModuleClass: ClassSymbol = ScalaPredefModule.moduleClass.asClass
 
   @tu lazy val SubTypeClass: ClassSymbol = requiredClass("scala.<:<")
@@ -881,6 +886,8 @@ class Definitions {
     lazy val RuntimeTuples_isInstanceOfEmptyTuple: Symbol = RuntimeTuplesModule.requiredMethod("isInstanceOfEmptyTuple")
     lazy val RuntimeTuples_isInstanceOfNonEmptyTuple: Symbol = RuntimeTuplesModule.requiredMethod("isInstanceOfNonEmptyTuple")
 
+  @tu lazy val RetainsClass: ClassSymbol = requiredClass("scala.Retains")
+
   // Annotation base classes
   @tu lazy val AnnotationClass: ClassSymbol = requiredClass("scala.annotation.Annotation")
   @tu lazy val ClassfileAnnotationClass: ClassSymbol = requiredClass("scala.annotation.ClassfileAnnotation")
@@ -934,6 +941,7 @@ class Definitions {
   @tu lazy val FunctionalInterfaceAnnot: ClassSymbol = requiredClass("java.lang.FunctionalInterface")
   @tu lazy val TargetNameAnnot: ClassSymbol = requiredClass("scala.annotation.targetName")
   @tu lazy val VarargsAnnot: ClassSymbol = requiredClass("scala.annotation.varargs")
+  @tu lazy val AbilityAnnot: ClassSymbol = requiredClass("scala.annotation.ability")
 
   @tu lazy val JavaRepeatableAnnot: ClassSymbol = requiredClass("java.lang.annotation.Repeatable")
 
@@ -1759,6 +1767,7 @@ class Definitions {
       AnyKindClass,
       andType,
       orType,
+      captureRootType,
       RepeatedParamClass,
       ByNameParamClass2x,
       AnyValClass,
diff --git a/compiler/src/dotty/tools/dotc/core/Mode.scala b/compiler/src/dotty/tools/dotc/core/Mode.scala
index 9f5b8a9a1c05..a752a7e7f5b4 100644
--- a/compiler/src/dotty/tools/dotc/core/Mode.scala
+++ b/compiler/src/dotty/tools/dotc/core/Mode.scala
@@ -124,4 +124,6 @@ object Mode {
    *  This mode forces expansion of inline calls in those positions even during typing.
    */
   val ForceInline: Mode = newMode(29, "ForceInline")
+
+  val RelaxedCapturing: Mode = newMode(30, "RelaxedCapturing")
 }
diff --git a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
index 89bf84d1ed03..4302a9f54fb8 100644
--- a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
@@ -329,6 +329,9 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
       case tp: AnnotatedType =>
         val parent1 = recur(tp.parent, fromBelow)
         if parent1 ne tp.parent then tp.derivedAnnotatedType(parent1, tp.annot) else tp
+      case tp: CapturingType =>
+        val parent1 = recur(tp.parent, fromBelow)
+        if parent1 ne tp.parent then tp.derivedCapturingType(parent1, tp.ref) else tp
       case _ =>
         val tp1 = tp.dealiasKeepAnnots
         if tp1 ne tp then
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index b6aea21bee8b..b90407b3de8e 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -275,6 +275,7 @@ object StdNames {
 
     // Compiler-internal
     val ANYname: N                  = "<anyname>"
+    val CAPTURE_ROOT: N             = "*"
     val COMPANION: N                = "<companion>"
     val CONSTRUCTOR: N              = "<init>"
     val STATIC_CONSTRUCTOR: N       = "<clinit>"
@@ -361,6 +362,7 @@ object StdNames {
     val AppliedTypeTree: N      = "AppliedTypeTree"
     val ArrayAnnotArg: N        = "ArrayAnnotArg"
     val CAP: N                  = "CAP"
+    val ClassManifestFactory: N = "ClassManifestFactory"
     val Constant: N             = "Constant"
     val ConstantType: N         = "ConstantType"
     val Eql: N                  = "Eql"
@@ -438,7 +440,6 @@ object StdNames {
     val canEqualAny : N         = "canEqualAny"
     val cbnArg: N               = "<cbn-arg>"
     val checkInitialized: N     = "checkInitialized"
-    val ClassManifestFactory: N = "ClassManifestFactory"
     val classOf: N              = "classOf"
     val classType: N            = "classType"
     val clone_ : N              = "clone"
@@ -570,6 +571,7 @@ object StdNames {
     val reflectiveSelectable: N = "reflectiveSelectable"
     val reify : N               = "reify"
     val releaseFence : N        = "releaseFence"
+    val retains: N              = "retains"
     val rootMirror : N          = "rootMirror"
     val run: N                  = "run"
     val runOrElse: N            = "runOrElse"
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index a7d45abd7a41..b795b788f598 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -1496,9 +1496,8 @@ object SymDenotations {
       case tp: ExprType => hasSkolems(tp.resType)
       case tp: AppliedType => hasSkolems(tp.tycon) || tp.args.exists(hasSkolems)
       case tp: LambdaType => tp.paramInfos.exists(hasSkolems) || hasSkolems(tp.resType)
-      case tp: AndType => hasSkolems(tp.tp1) || hasSkolems(tp.tp2)
-      case tp: OrType  => hasSkolems(tp.tp1) || hasSkolems(tp.tp2)
-      case tp: AnnotatedType => hasSkolems(tp.parent)
+      case tp: AndOrType => hasSkolems(tp.tp1) || hasSkolems(tp.tp2)
+      case tp: AnnotOrCaptType => hasSkolems(tp.parent)
       case _ => false
     }
 
@@ -2153,6 +2152,9 @@ object SymDenotations {
           case tp: TypeParamRef =>  // uncachable, since baseType depends on context bounds
             recur(TypeComparer.bounds(tp).hi)
 
+          case tp: CapturingType =>
+            tp.derivedCapturingType(recur(tp.parent), tp.ref)
+
           case tp: TypeProxy =>
             def computeTypeProxy = {
               val superTp = tp.superType
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 5774f750ce44..4f867ba72b25 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -489,7 +489,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             // and then need to check that they are indeed supertypes of the original types
             // under -Ycheck. Test case is i7965.scala.
 
-     case tp1: MatchType =>
+      case tp1: CapturingType =>
+        if tp2.captureSet.accountsFor(tp1.ref) then recur(tp1.parent, tp2)
+        else thirdTry
+      case tp1: MatchType =>
         val reduced = tp1.reduced
         if (reduced.exists) recur(reduced, tp2) else thirdTry
       case _: FlexType =>
@@ -527,8 +530,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
               // Note: We would like to replace this by `if (tp1.hasHigherKind)`
               // but right now we cannot since some parts of the standard library rely on the
               // idiom that e.g. `List <: Any`. We have to bootstrap without scalac first.
-            if (cls2 eq AnyClass) return true
-            if (cls2 == defn.SingletonClass && tp1.isStable) return true
+            if (cls2 eq AnyClass) && tp1.noCaptures then return true
+            if cls2 == defn.SingletonClass && tp1.isStable then return true
             return tryBaseType(cls2)
           }
           else if (cls2.is(JavaDefined)) {
@@ -727,7 +730,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         def compareTypeBounds = tp1 match {
           case tp1 @ TypeBounds(lo1, hi1) =>
             ((lo2 eq NothingType) || isSubType(lo2, lo1)) &&
-            ((hi2 eq AnyType) && !hi1.isLambdaSub || (hi2 eq AnyKindType) || isSubType(hi1, hi2))
+            ((hi2 eq AnyType) && !hi1.isLambdaSub && hi1.noCaptures
+             || (hi2 eq AnyKindType) || isSubType(hi1, hi2))
           case tp1: ClassInfo =>
             tp2 contains tp1
           case _ =>
@@ -737,6 +741,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       case tp2: AnnotatedType if tp2.isRefining =>
         (tp1.derivesAnnotWith(tp2.annot.sameAnnotation) || tp1.isBottomType) &&
         recur(tp1, tp2.parent)
+      case tp2: CapturingType =>
+        recur(tp1, tp2.parent) || fourthTry
       case ClassInfo(pre2, cls2, _, _, _) =>
         def compareClassInfo = tp1 match {
           case ClassInfo(pre1, cls1, _, _, _) =>
@@ -770,7 +776,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
               tp1.symbol.onGadtBounds(gbounds1 =>
                 isSubTypeWhenFrozen(gbounds1.hi, tp2)
                 || narrowGADTBounds(tp1, tp2, approx, isUpper = true))
-              && (tp2.isAny || GADTusage(tp1.symbol))
+              && (tp2.isAny && tp1.noCaptures || GADTusage(tp1.symbol))
 
             isSubType(hi1, tp2, approx.addLow) || compareGADT || tryLiftedToThis1
           case _ =>
@@ -780,6 +786,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
               case tp: AppliedType => isNullable(tp.tycon)
               case AndType(tp1, tp2) => isNullable(tp1) && isNullable(tp2)
               case OrType(tp1, tp2) => isNullable(tp1) || isNullable(tp2)
+              case CapturingType(tp1, _) => isNullable(tp1)
               case _ => false
             }
             val sym1 = tp1.symbol
@@ -798,7 +805,25 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 case _ => false
             }
           case _ => false
-        comparePaths || isSubType(tp1.underlying.widenExpr, tp2, approx.addLow)
+        comparePaths || {
+          val tp2n = tp1 match
+            case tp1: CaptureRef if tp1.isTracked =>
+              // New rule dealing with singleton types on the left:
+              //
+              //   E |- x: S   E |- S <: {*} T
+              //   ---------------------------
+              //         E |- x.type <:< T
+              //
+              // Note: This would map to the following (Var) rule in deep capture calculus:
+              //
+              //   E |- x: S   E |- S <: {*} T
+              //   ---------------------------
+              //      E |- x: {x} T
+              //
+              CapturingType(tp2, defn.captureRootType.typeRef)
+            case _ => tp2
+          isSubType(tp1.underlying.widenExpr, tp2n, approx.addLow)
+        }
       case tp1: RefinedType =>
         isNewSubType(tp1.parent)
       case tp1: RecType =>
@@ -2022,8 +2047,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     if (tp1 eq tp2) tp1
     else if (!tp1.exists) tp2
     else if (!tp2.exists) tp1
-    else if tp1.isAny && !tp2.isLambdaSub || tp1.isAnyKind || isBottom(tp2) then tp2
-    else if tp2.isAny && !tp1.isLambdaSub || tp2.isAnyKind || isBottom(tp1) then tp1
+    else if tp1.isAny && !tp2.isLambdaSub && tp2.noCaptures || tp1.isAnyKind || isBottom(tp2) then tp2
+    else if tp2.isAny && !tp1.isLambdaSub && tp1.noCaptures || tp2.isAnyKind || isBottom(tp1) then tp1
     else tp2 match
       case tp2: LazyRef =>
         glb(tp1, tp2.ref)
@@ -2072,8 +2097,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     if (tp1 eq tp2) tp1
     else if (!tp1.exists) tp1
     else if (!tp2.exists) tp2
-    else if tp1.isAny && !tp2.isLambdaSub || tp1.isAnyKind || isBottom(tp2) then tp1
-    else if tp2.isAny && !tp1.isLambdaSub || tp2.isAnyKind || isBottom(tp1) then tp2
+    else if tp1.isAny && !tp2.isLambdaSub && tp2.noCaptures || tp1.isAnyKind || isBottom(tp2) then tp1
+    else if tp2.isAny && !tp1.isLambdaSub && tp1.noCaptures || tp2.isAnyKind || isBottom(tp1) then tp2
     else
       def mergedLub(tp1: Type, tp2: Type): Type = {
         tp1.atoms match
@@ -2343,6 +2368,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       tp1.underlying & tp2
     case tp1: AnnotatedType if !tp1.isRefining =>
       tp1.underlying & tp2
+    case tp1: CapturingType if !tp2.captureSet.accountsFor(tp1.ref) =>
+      tp1.parent & tp2
     case _ =>
       NoType
   }
@@ -2750,7 +2777,7 @@ object TypeComparer {
 
   /** The greatest lower bound of a list types */
   def glb(tps: List[Type])(using Context): Type =
-    tps.foldLeft(defn.AnyType: Type)(glb)
+    tps.foldLeft(defn.TopType: Type)(glb)
 
   def orType(using Context)(tp1: Type, tp2: Type, isSoft: Boolean = true, isErased: Boolean = ctx.erasedTypes): Type =
     comparing(_.orType(tp1, tp2, isSoft = isSoft, isErased = isErased))
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index 75a5816c3164..6362e2d89543 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -168,6 +168,9 @@ object TypeOps:
       case _: MatchType =>
         val normed = tp.tryNormalize
         if (normed.exists) normed else mapOver
+      case tp: CapturingType
+      if !ctx.mode.is(Mode.Type) && tp.parent.captureSet.accountsFor(tp.ref) =>
+        simplify(tp.parent, theMap)
       case tp: MethodicType =>
         tp // See documentation of `Types#simplified`
       case tp: SkolemType =>
@@ -267,15 +270,23 @@ object TypeOps:
         case _ => false
       }
 
-      // Step 1: Get RecTypes and ErrorTypes out of the way,
+      // Step 1: Get RecTypes and ErrorTypes and CapturingTypes out of the way,
       tp1 match {
-        case tp1: RecType => return tp1.rebind(approximateOr(tp1.parent, tp2))
-        case err: ErrorType => return err
+        case tp1: RecType =>
+          return tp1.rebind(approximateOr(tp1.parent, tp2))
+        case tp1: CapturingType =>
+          return tp1.derivedCapturingType(approximateOr(tp1.parent, tp2), tp1.ref)
+        case err: ErrorType =>
+          return err
         case _ =>
       }
       tp2 match {
-        case tp2: RecType => return tp2.rebind(approximateOr(tp1, tp2.parent))
-        case err: ErrorType => return err
+        case tp2: RecType =>
+          return tp2.rebind(approximateOr(tp1, tp2.parent))
+        case tp2: CapturingType =>
+          return tp2.derivedCapturingType(approximateOr(tp1, tp2.parent), tp2.ref)
+        case err: ErrorType =>
+          return err
         case _ =>
       }
 
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 0d01668be2f5..f5279f271e4a 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -67,11 +67,12 @@ object Types {
    *        |              |                +--- SkolemType
    *        |              +- TypeParamRef
    *        |              +- RefinedOrRecType -+-- RefinedType
-   *        |              |                   -+-- RecType
+   *        |              |                    +-- RecType
    *        |              +- AppliedType
    *        |              +- TypeBounds
    *        |              +- ExprType
-   *        |              +- AnnotatedType
+   *        |              +- AnnotOrCaptType -+-- AnnotatedType
+   *        |              |                   +-- CapturingType
    *        |              +- TypeVar
    *        |              +- HKTypeLambda
    *        |              +- MatchType
@@ -173,6 +174,7 @@ object Types {
         // not on types. Allowing it on types is a Scala 3 extension. See:
         // https://www.scala-lang.org/files/archive/spec/2.11/11-annotations.html#scala-compiler-annotations
         tp.annot.symbol == defn.UncheckedStableAnnot || tp.parent.isStable
+      case tp: CapturingType => tp.parent.isStable
       case tp: AndType =>
         // TODO: fix And type check when tp contains type parames for explicit-nulls flow-typing
         // see: tests/explicit-nulls/pos/flow-stable.scala.disabled
@@ -187,18 +189,24 @@ object Types {
      *        It makes no sense for it to be an alias type because isRef would always
      *        return false in that case.
      */
-    def isRef(sym: Symbol, skipRefined: Boolean = true)(using Context): Boolean = stripped match {
+    def isRef(sym: Symbol, skipRefined: Boolean = true, skipCapturing: Boolean = false)(using Context): Boolean = this match {
       case this1: TypeRef =>
         this1.info match { // see comment in Namer#typeDefSig
-          case TypeAlias(tp) => tp.isRef(sym, skipRefined)
+          case TypeAlias(tp) => tp.isRef(sym, skipRefined, skipCapturing)
           case _ => this1.symbol eq sym
         }
       case this1: RefinedOrRecType if skipRefined =>
-        this1.parent.isRef(sym, skipRefined)
+        this1.parent.isRef(sym, skipRefined, skipCapturing)
       case this1: AppliedType =>
         val this2 = this1.dealias
-        if (this2 ne this1) this2.isRef(sym, skipRefined)
-        else this1.underlying.isRef(sym, skipRefined)
+        if (this2 ne this1) this2.isRef(sym, skipRefined, skipCapturing)
+        else this1.underlying.isRef(sym, skipRefined, skipCapturing)
+      case this1: TypeVar =>
+        this1.instanceOpt.isRef(sym, skipRefined, skipCapturing)
+      case this1: AnnotatedType =>
+        this1.parent.isRef(sym, skipRefined, skipCapturing)
+      case this1: CapturingType if skipCapturing =>
+        this1.parent.isRef(sym, skipRefined, skipCapturing)
       case _ => false
     }
 
@@ -365,6 +373,7 @@ object Types {
       case tp: AndOrType => tp.tp1.unusableForInference || tp.tp2.unusableForInference
       case tp: LambdaType => tp.resultType.unusableForInference || tp.paramInfos.exists(_.unusableForInference)
       case WildcardType(optBounds) => optBounds.unusableForInference
+      case CapturingType(parent, ref) => parent.unusableForInference || ref.unusableForInference
       case _: ErrorType => true
       case _ => false
 
@@ -1177,7 +1186,7 @@ object Types {
      */
     def stripAnnots(using Context): Type = this
 
-    /** Strip TypeVars and Annotation wrappers */
+    /** Strip TypeVars and Annotation and CapturingType wrappers */
     def stripped(using Context): Type = this
 
     def rewrapAnnots(tp: Type)(using Context): Type = tp.stripTypeVar match {
@@ -1372,6 +1381,8 @@ object Types {
       case tp: AnnotatedType =>
         val tp1 = tp.parent.dealias1(keep)
         if keep(tp) then tp.derivedAnnotatedType(tp1, tp.annot) else tp1
+      case tp: CapturingType =>
+        tp.derivedCapturingType(tp.parent.dealias1(keep), tp.ref)
       case tp: LazyRef =>
         tp.ref.dealias1(keep)
       case _ => this
@@ -1452,8 +1463,8 @@ object Types {
       case tp: AppliedType =>
         if (tp.tycon.isLambdaSub) NoType
         else tp.superType.underlyingClassRef(refinementOK)
-      case tp: AnnotatedType =>
-        tp.underlying.underlyingClassRef(refinementOK)
+      case tp: AnnotOrCaptType =>
+        tp.parent.underlyingClassRef(refinementOK)
       case tp: RefinedType =>
         if (refinementOK) tp.underlying.underlyingClassRef(refinementOK) else NoType
       case tp: RecType =>
@@ -1496,6 +1507,10 @@ object Types {
       case _                  => if (isRepeatedParam) this.argTypesHi.head else this
     }
 
+    def captureSet(using Context): CaptureSet = CaptureSet.ofType(this)
+    def noCaptures(using Context): Boolean =
+      ctx.mode.is(Mode.RelaxedCapturing) || captureSet.isEmpty
+
     // ----- Normalizing typerefs over refined types ----------------------------
 
     /** If this normalizes* to a refinement type that has a refinement for `name` (which might be followed
@@ -1827,6 +1842,12 @@ object Types {
       case _ => this
     }
 
+    def capturing(ref: CaptureRef)(using Context): Type =
+      if captureSet.accountsFor(ref) then this else CapturingType(this, ref)
+
+    def capturing(cs: CaptureSet)(using Context): Type =
+      (this /: cs.elems)(_.capturing(_))
+
     /** The set of distinct symbols referred to by this type, after all aliases are expanded */
     def coveringSet(using Context): Set[Symbol] =
       (new CoveringSetAccumulator).apply(Set.empty[Symbol], this)
@@ -2007,6 +2028,42 @@ object Types {
     def isOverloaded(using Context): Boolean = false
   }
 
+  /** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs */
+  trait CaptureRef extends TypeProxy, ValueType:
+    private var myCaptureSet: CaptureSet = _
+    private var myCaptureSetRunId: Int = NoRunId
+    private var mySingletonCaptureSet: CaptureSet = null
+
+    def canBeTracked(using Context): Boolean
+    final def isTracked(using Context): Boolean = canBeTracked && captureSetOfInfo.nonEmpty
+    def isRootCapability(using Context): Boolean = false
+    def normalizedRef(using Context): CaptureRef = this
+
+    def singletonCaptureSet(using Context): CaptureSet =
+      if mySingletonCaptureSet == null then
+        mySingletonCaptureSet = CaptureSet(this.normalizedRef)
+      mySingletonCaptureSet
+
+    def captureSetOfInfo(using Context): CaptureSet =
+      if ctx.runId == myCaptureSetRunId then myCaptureSet
+      else if myCaptureSet eq CaptureSet.Pending then CaptureSet.empty
+      else
+        myCaptureSet = CaptureSet.Pending
+        val computed =
+          if isRootCapability then singletonCaptureSet
+          else CaptureSet.ofType(underlying)
+        if underlying.isProvisional then
+          myCaptureSet = null
+        else
+          myCaptureSet = computed
+          myCaptureSetRunId = ctx.runId
+        computed
+
+    override def captureSet(using Context): CaptureSet =
+      val cs = captureSetOfInfo
+      if canBeTracked && cs.nonEmpty then singletonCaptureSet else cs
+  end CaptureRef
+
   /** A trait for types that bind other types that refer to them.
    *  Instances are: LambdaType, RecType.
    */
@@ -2054,7 +2111,7 @@ object Types {
 
 // --- NamedTypes ------------------------------------------------------------------
 
-  abstract class NamedType extends CachedProxyType with ValueType { self =>
+  abstract class NamedType extends CachedProxyType, CaptureRef { self =>
 
     type ThisType >: this.type <: NamedType
     type ThisName <: Name
@@ -2073,6 +2130,9 @@ object Types {
     private var mySignature: Signature = _
     private var mySignatureRunId: Int = NoRunId
 
+    private var myCaptureSet: CaptureSet = _
+    private var myCaptureSetRunId: Int = NoRunId
+
     // Invariants:
     // (1) checkedPeriod != Nowhere     =>  lastDenotation != null
     // (2) lastDenotation != null       =>  lastSymbol != null
@@ -2328,6 +2388,23 @@ object Types {
       checkDenot()
     }
 
+    /** A reference can be tracked if it is
+     *   (1) a local term ref
+     *   (2) a type parameter,
+     *   (3) a method term parameter
+     *  References to term parameters of classes cannot be tracked individually.
+     *  They are subsumed in the capture sets of the enclosing class.
+     */
+    def canBeTracked(using Context) =
+      if isTerm then (prefix eq NoPrefix) || symbol.hasAnnotation(defn.AbilityAnnot)
+      else symbol.is(TypeParam) || isRootCapability
+
+    override def isRootCapability(using Context): Boolean =
+      name == tpnme.CAPTURE_ROOT && symbol == defn.captureRootType
+
+    override def normalizedRef(using Context): CaptureRef =
+      if canBeTracked then symbol.namedType else this
+
     private def checkDenot()(using Context) = {}
 
     private def checkSymAssign(sym: Symbol)(using Context) = {
@@ -2425,7 +2502,7 @@ object Types {
       val tparam = symbol
       val cls = tparam.owner
       val base = pre.baseType(cls)
-      base match {
+      base.stripped match {
         case AppliedType(_, allArgs) =>
           var tparams = cls.typeParams
           var args = allArgs
@@ -2764,7 +2841,7 @@ object Types {
    *  Note: we do not pass a class symbol directly, because symbols
    *  do not survive runs whereas typerefs do.
    */
-  abstract case class ThisType(tref: TypeRef) extends CachedProxyType with SingletonType {
+  abstract case class ThisType(tref: TypeRef) extends CachedProxyType, SingletonType, CaptureRef {
     def cls(using Context): ClassSymbol = tref.stableInRunSymbol match {
       case cls: ClassSymbol => cls
       case _ if ctx.mode.is(Mode.Interactive) => defn.AnyClass // was observed to happen in IDE mode
@@ -2778,6 +2855,12 @@ object Types {
           // can happen in IDE if `cls` is stale
       }
 
+    override def canBeTracked(using Context) = cls.owner.isTerm
+
+    override def captureSetOfInfo(using Context): CaptureSet =
+      super.captureSetOfInfo
+      ++ CaptureSet.ofClass(cls.classInfo, cls.paramAccessors.map(_.info))
+
     override def computeHash(bs: Binders): Int = doHash(bs, tref)
 
     override def eql(that: Type): Boolean = that match {
@@ -3604,6 +3687,11 @@ object Types {
           case tp: AppliedType => tp.fold(status, compute(_, _, theAcc))
           case tp: TypeVar if !tp.isInstantiated => combine(status, Provisional)
           case tp: TermParamRef if tp.binder eq thisLambdaType => TrueDeps
+          case tp: CapturingType =>
+            val status1 = compute(status, tp.parent, theAcc)
+            tp.ref match
+              case tp: TermParamRef if tp.binder eq thisLambdaType => combine(status1, CaptureDeps)
+              case _ => status1
           case _: ThisType | _: BoundType | NoPrefix => status
           case _ =>
             (if theAcc != null then theAcc else DepAcc()).foldOver(status, tp)
@@ -3642,18 +3730,24 @@ object Types {
     /** Does result type contain references to parameters of this method type,
      *  which cannot be eliminated by de-aliasing?
      */
-    def isResultDependent(using Context): Boolean = dependencyStatus == TrueDeps
+    def isResultDependent(using Context): Boolean =
+      dependencyStatus == TrueDeps || dependencyStatus == CaptureDeps
 
     /** Does one of the parameter types contain references to earlier parameters
      *  of this method type which cannot be eliminated by de-aliasing?
      */
     def isParamDependent(using Context): Boolean = paramDependencyStatus == TrueDeps
 
+    /** Is there either a true or false type dependency, or does the result
+     *  type capture a parameter?
+     */
+    def isCaptureDependent(using Context) = dependencyStatus == CaptureDeps
+
     def newParamRef(n: Int): TermParamRef = new TermParamRefImpl(this, n)
 
     /** The least supertype of `resultType` that does not contain parameter dependencies */
     def nonDependentResultApprox(using Context): Type =
-      if (isResultDependent) {
+      if isResultDependent then
         val dropDependencies = new ApproximatingTypeMap {
           def apply(tp: Type) = tp match {
             case tp @ TermParamRef(thisLambdaType, _) =>
@@ -3662,7 +3756,6 @@ object Types {
           }
         }
         dropDependencies(resultType)
-      }
       else resultType
   }
 
@@ -4031,9 +4124,10 @@ object Types {
     final val Unknown: DependencyStatus = 0   // not yet computed
     final val NoDeps: DependencyStatus = 1    // no dependent parameters found
     final val FalseDeps: DependencyStatus = 2 // all dependent parameters are prefixes of non-depended alias types
-    final val TrueDeps: DependencyStatus = 3  // some truly dependent parameters exist
-    final val StatusMask: DependencyStatus = 3 // the bits indicating actual dependency status
-    final val Provisional: DependencyStatus = 4  // set if dependency status can still change due to type variable instantiations
+    final val CaptureDeps: DependencyStatus = 3
+    final val TrueDeps: DependencyStatus = 4  // some truly dependent parameters exist
+    final val StatusMask: DependencyStatus = 7 // the bits indicating actual dependency status
+    final val Provisional: DependencyStatus = 8  // set if dependency status can still change due to type variable instantiations
   }
 
   // ----- Type application: LambdaParam, AppliedType ---------------------
@@ -4324,7 +4418,7 @@ object Types {
     override def hashIsStable: Boolean = false
   }
 
-  abstract class ParamRef extends BoundType {
+  abstract class ParamRef extends BoundType, CaptureRef {
     type BT <: LambdaType
     def paramNum: Int
     def paramName: binder.ThisName = binder.paramNames(paramNum)
@@ -4335,6 +4429,8 @@ object Types {
       else infos(paramNum)
     }
 
+    override def canBeTracked(using Context) = true
+
     override def computeHash(bs: Binders): Int = doHash(paramNum, binder.identityHash(bs))
 
     override def equals(that: Any): Boolean = equals(that, null)
@@ -5025,8 +5121,12 @@ object Types {
 
   // ----- Annotated and Import types -----------------------------------------------
 
+  abstract class AnnotOrCaptType extends CachedProxyType with ValueType:
+    def parent: Type
+    override def stripped(using Context): Type = parent.stripped
+
   /** An annotated type tpe @ annot */
-  abstract case class AnnotatedType(parent: Type, annot: Annotation) extends CachedProxyType with ValueType {
+  abstract case class AnnotatedType(parent: Type, annot: Annotation) extends AnnotOrCaptType {
 
     override def underlying(using Context): Type = parent
 
@@ -5039,8 +5139,6 @@ object Types {
 
     override def stripAnnots(using Context): Type = parent.stripAnnots
 
-    override def stripped(using Context): Type = parent.stripped
-
     private var isRefiningKnown = false
     private var isRefiningCache: Boolean = _
 
@@ -5075,6 +5173,42 @@ object Types {
       annots.foldLeft(underlying)(apply(_, _))
     def apply(parent: Type, annot: Annotation)(using Context): AnnotatedType =
       unique(CachedAnnotatedType(parent, annot))
+  end AnnotatedType
+
+  abstract case class CapturingType(parent: Type, ref: CaptureRef) extends AnnotOrCaptType:
+    override def underlying(using Context): Type = parent
+
+    def derivedCapturingType(parent: Type, ref: CaptureRef)(using Context): CapturingType =
+      if (parent eq this.parent) && (ref eq this.ref) then this
+      else CapturingType(parent, ref)
+
+    def derivedCapturing(parent: Type, capt: Type)(using Context): Type =
+      if (parent eq this.parent) && (capt eq this.ref) then this
+      else parent.capturing(capt.captureSet)
+
+    // equals comes from case class; no matching override is needed
+
+    override def computeHash(bs: Binders): Int =
+      doHash(bs, parent, ref)
+    override def hashIsStable: Boolean =
+      parent.hashIsStable && ref.hashIsStable
+
+    override def eql(that: Type): Boolean = that match
+      case that: CapturingType => (parent eq that.parent) && (ref eq that.ref)
+      case _ => false
+
+    override def iso(that: Any, bs: BinderPairs): Boolean = that match
+      case that: CapturingType => parent.equals(that.parent, bs) && ref.equals(that.ref, bs)
+      case _ => false
+
+  class CachedCapturingType(parent: Type, ref: CaptureRef) extends CapturingType(parent, ref)
+
+  object CapturingType:
+    def apply(parent: Type, ref: CaptureRef)(using Context): CapturingType =
+      unique(CachedCapturingType(parent, ref.normalizedRef))
+    def checked(parent: Type, ref: Type)(using Context): CapturingType = ref match
+      case ref: CaptureRef => apply(parent, ref)
+  end CapturingType
 
   // Special type objects and classes -----------------------------------------------------
 
@@ -5212,7 +5346,7 @@ object Types {
         zeroParamClass(tp.underlying)
       case tp: TypeVar =>
         zeroParamClass(tp.underlying)
-      case tp: AnnotatedType =>
+      case tp: AnnotOrCaptType =>
         zeroParamClass(tp.underlying)
       case _ =>
         NoType
@@ -5347,6 +5481,8 @@ object Types {
       tp.derivedMatchType(bound, scrutinee, cases)
     protected def derivedAnnotatedType(tp: AnnotatedType, underlying: Type, annot: Annotation): Type =
       tp.derivedAnnotatedType(underlying, annot)
+    protected def derivedCapturing(tp: CapturingType, parent: Type, capt: Type): Type =
+      tp.derivedCapturing(parent, capt)
     protected def derivedWildcardType(tp: WildcardType, bounds: Type): Type =
       tp.derivedWildcardType(bounds)
     protected def derivedSkolemType(tp: SkolemType, info: Type): Type =
@@ -5426,6 +5562,9 @@ object Types {
           if (underlying1 eq underlying) tp
           else derivedAnnotatedType(tp, underlying1, mapOver(annot))
 
+        case tp @ CapturingType(parent, ref) =>
+          derivedCapturing(tp, this(parent), this(ref))
+
         case _: ThisType
           | _: BoundType
           | NoPrefix =>
@@ -5745,6 +5884,16 @@ object Types {
           if (underlying.isExactlyNothing) underlying
           else tp.derivedAnnotatedType(underlying, annot)
       }
+    override protected def derivedCapturing(tp: CapturingType, parent: Type, capt: Type): Type =
+      capt match
+        case Range(lo, hi) =>
+          range(derivedCapturing(tp, parent, hi), derivedCapturing(tp, parent, lo))
+        case _ => parent match
+          case Range(lo, hi) =>
+            range(derivedCapturing(tp, lo, capt), derivedCapturing(tp, hi, capt))
+          case _ =>
+            tp.derivedCapturing(parent, capt)
+
     override protected def derivedWildcardType(tp: WildcardType, bounds: Type): WildcardType =
       tp.derivedWildcardType(rangeToBounds(bounds))
 
@@ -5884,6 +6033,9 @@ object Types {
       case AnnotatedType(underlying, annot) =>
         this(applyToAnnot(x, annot), underlying)
 
+      case CapturingType(parent, ref) =>
+        this(this(x, parent), ref)
+
       case tp: ProtoType =>
         tp.fold(x, this)
 
diff --git a/compiler/src/dotty/tools/dotc/core/Variances.scala b/compiler/src/dotty/tools/dotc/core/Variances.scala
index 122c7a10e4b7..5dbee234adca 100644
--- a/compiler/src/dotty/tools/dotc/core/Variances.scala
+++ b/compiler/src/dotty/tools/dotc/core/Variances.scala
@@ -101,6 +101,8 @@ object Variances {
       varianceInArgs(varianceInType(tycon)(tparam), args, tycon.typeParams)
     case AnnotatedType(tp, annot) =>
       varianceInType(tp)(tparam) & varianceInAnnot(annot)(tparam)
+    case CapturingType(tp, _) =>
+      varianceInType(tp)(tparam)
     case AndType(tp1, tp2) =>
       varianceInType(tp1)(tparam) & varianceInType(tp2)(tparam)
     case OrType(tp1, tp2) =>
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index 78a2c73de3ea..8ab81fdac6d1 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -277,6 +277,13 @@ class TreePickler(pickler: TastyPickler) {
         pickleType(tpe.scrutinee)
         tpe.cases.foreach(pickleType(_))
       }
+    case tp: CapturingType =>
+      writeByte(APPLIEDtype)
+      withLength {
+        pickleType(defn.Predef_retainsType.typeRef)
+        pickleType(tp.parent)
+        pickleType(tp.ref)
+      }
     case tpe: PolyType if richTypes =>
       pickleMethodic(POLYtype, tpe, EmptyFlags)
     case tpe: MethodType if richTypes =>
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
index cf6fc142b8af..96d80a86e697 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
@@ -357,7 +357,13 @@ class TreeUnpickler(reader: TastyReader,
                 // Note that the lambda "rt => ..." is not equivalent to a wildcard closure!
                 // Eta expansion of the latter puts readType() out of the expression.
             case APPLIEDtype =>
-              readType().appliedTo(until(end)(readType()))
+              val tycon = readType()
+              val args = until(end)(readType())
+              tycon match
+                case tycon: TypeRef if tycon.symbol == defn.Predef_retainsType =>
+                  CapturingType.checked(args(0), args(1))
+                case _ =>
+                  tycon.appliedTo(args)
             case TYPEBOUNDS =>
               val lo = readType()
               if nothingButMods(end) then
@@ -821,7 +827,7 @@ class TreeUnpickler(reader: TastyReader,
       def TypeDef(rhs: Tree) =
         ta.assignType(untpd.TypeDef(sym.name.asTypeName, rhs), sym)
 
-      def ta =  ctx.typeAssigner
+      def ta = ctx.typeAssigner
 
       val name = readName()
       pickling.println(s"reading def of $name at $start")
@@ -1265,11 +1271,9 @@ class TreeUnpickler(reader: TastyReader,
               // types. This came up in #137 of collection strawman.
               val tycon = readTpt()
               val args = until(end)(readTpt())
-              val ownType =
-                if (tycon.symbol == defn.andType) AndType(args(0).tpe, args(1).tpe)
-                else if (tycon.symbol == defn.orType) OrType(args(0).tpe, args(1).tpe, soft = false)
-                else tycon.tpe.safeAppliedTo(args.tpes)
-              untpd.AppliedTypeTree(tycon, args).withType(ownType)
+              val tree = untpd.AppliedTypeTree(tycon, args)
+              val ownType = ctx.typeAssigner.processAppliedType(tree, tycon.tpe.safeAppliedTo(args.tpes))
+              tree.withType(ownType)
             case ANNOTATEDtpt =>
               Annotated(readTpt(), readTerm())
             case LAMBDAtpt =>
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 7009a55d3aeb..63c5345c0947 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -187,6 +187,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
           keywordStr(" match ") ~ "{" ~ casesText ~ "}" ~
           (" <: " ~ toText(bound) provided !bound.isAny)
         }.close
+      case CapturingType(parent, ref) =>
+        changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toTextCaptureRef(ref))
       case tp: PreviousErrorType if ctx.settings.XprintTypes.value =>
         "<error>" // do not print previously reported error message because they may try to print this error type again recuresevely
       case tp: ErrorType =>
@@ -335,6 +337,11 @@ class PlainPrinter(_ctx: Context) extends Printer {
     }
   }
 
+  def toTextCaptureRef(tp: Type): Text =
+    homogenize(tp) match
+      case tp: SingletonType => toTextRef(tp)
+      case _ => toText(tp)
+
   protected def isOmittablePrefix(sym: Symbol): Boolean =
     defn.unqualifiedOwnerTypes.exists(_.symbol == sym) || isEmptyPrefix(sym)
 
diff --git a/compiler/src/dotty/tools/dotc/printing/Printer.scala b/compiler/src/dotty/tools/dotc/printing/Printer.scala
index 2079bc7cc1cd..2bfaf51f9b40 100644
--- a/compiler/src/dotty/tools/dotc/printing/Printer.scala
+++ b/compiler/src/dotty/tools/dotc/printing/Printer.scala
@@ -104,6 +104,9 @@ abstract class Printer {
   /** Textual representation of a prefix of some reference, ending in `.` or `#` */
   def toTextPrefix(tp: Type): Text
 
+  /** Textual representation of a reference in a capture set */
+  def toTextCaptureRef(tp: Type): Text
+
   /** Textual representation of symbol's declaration */
   def dclText(sym: Symbol): Text
 
diff --git a/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala b/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
index 6e198bbeada9..a171dfc0ee51 100644
--- a/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
+++ b/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
@@ -175,6 +175,7 @@ private class ExtractAPICollector(using Context) extends ThunkHolder {
   private val byNameMarker = marker("ByName")
   private val matchMarker = marker("Match")
   private val superMarker = marker("Super")
+  private val retainsMarker = marker("Retains")
 
   /** Extract the API representation of a source file */
   def apiSource(tree: Tree): Seq[api.ClassLike] = {
@@ -520,6 +521,9 @@ private class ExtractAPICollector(using Context) extends ThunkHolder {
       case SuperType(thistpe, supertpe) =>
         val s = combineApiTypes(apiType(thistpe), apiType(supertpe))
         withMarker(s, superMarker)
+      case CapturingType(parent, ref) =>
+        val s = combineApiTypes(apiType(parent), apiType(ref))
+        withMarker(s, retainsMarker)
       case _ => {
         internalError(i"Unhandled type $tp of class ${tp.getClass}")
         Constants.emptyType
diff --git a/compiler/src/dotty/tools/dotc/transform/GenericSignatures.scala b/compiler/src/dotty/tools/dotc/transform/GenericSignatures.scala
index 9392d9038574..bb1f0bb3d0d3 100644
--- a/compiler/src/dotty/tools/dotc/transform/GenericSignatures.scala
+++ b/compiler/src/dotty/tools/dotc/transform/GenericSignatures.scala
@@ -347,8 +347,8 @@ object GenericSignatures {
           if (toplevel) polyParamSig(tParams)
           superSig(ci.typeSymbol, ci.parents)
 
-        case AnnotatedType(atp, _) =>
-          jsig(atp, toplevel, primitiveOK)
+        case tp: AnnotOrCaptType =>
+          jsig(tp.parent, toplevel, primitiveOK)
 
         case hktl: HKTypeLambda =>
           jsig(hktl.finalResultType, toplevel, primitiveOK)
@@ -469,10 +469,8 @@ object GenericSignatures {
             true
           case ClassInfo(_, _, parents, _, _) =>
             foldOver(tp.typeParams.nonEmpty, parents)
-          case AnnotatedType(tpe, _) =>
-            foldOver(x, tpe)
-          case proxy: TypeProxy =>
-            foldOver(x, proxy)
+          case tp: AnnotOrCaptType =>
+            foldOver(x, tp.parent)
           case _ =>
             foldOver(x, tp)
         }
diff --git a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
index 29fd1adb6688..a274555c754b 100644
--- a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
@@ -375,14 +375,14 @@ class TreeChecker extends Phase with SymTransformer {
       val tpe = tree.typeOpt
 
       // Polymorphic apply methods stay structural until Erasure
-      val isPolyFunctionApply = (tree.name eq nme.apply) && (tree.qualifier.typeOpt <:< defn.PolyFunctionType)
+      val isPolyFunctionApply = (tree.name eq nme.apply) && tree.qualifier.typeOpt.derivesFrom(defn.PolyFunctionClass)
       // Outer selects are pickled specially so don't require a symbol
       val isOuterSelect = tree.name.is(OuterSelectName)
       val isPrimitiveArrayOp = ctx.erasedTypes && nme.isPrimitiveName(tree.name)
       if !(tree.isType || isPolyFunctionApply || isOuterSelect || isPrimitiveArrayOp) then
         val denot = tree.denot
         assert(denot.exists, i"Selection $tree with type $tpe does not have a denotation")
-        assert(denot.symbol.exists, i"Denotation $denot of selection $tree with type $tpe does not have a symbol")
+        assert(denot.symbol.exists, i"Denotation $denot of selection $tree with type $tpe does not have a symbol, ${tree.qualifier.typeOpt}")
 
       val sym = tree.symbol
       val symIsFixed = tpe match {
diff --git a/compiler/src/dotty/tools/dotc/transform/TryCatchPatterns.scala b/compiler/src/dotty/tools/dotc/transform/TryCatchPatterns.scala
index 6be58352e6dc..26bea001d1eb 100644
--- a/compiler/src/dotty/tools/dotc/transform/TryCatchPatterns.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TryCatchPatterns.scala
@@ -70,7 +70,7 @@ class TryCatchPatterns extends MiniPhase {
     case _                                                               => isDefaultCase(cdef)
   }
 
-  private def isSimpleThrowable(tp: Type)(using Context): Boolean = tp.stripAnnots match {
+  private def isSimpleThrowable(tp: Type)(using Context): Boolean = tp.stripped match {
     case tp @ TypeRef(pre, _) =>
       (pre == NoPrefix || pre.typeSymbol.isStatic) && // Does not require outer class check
       !tp.symbol.is(Flags.Trait) && // Traits not supported by JVM
diff --git a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
index a4951b99f599..0e6e4c125ff2 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
@@ -148,7 +148,7 @@ object TypeTestsCasts {
         }
       case AndType(tp1, tp2)    => recur(X, tp1) && recur(X, tp2)
       case OrType(tp1, tp2)     => recur(X, tp1) && recur(X, tp2)
-      case AnnotatedType(t, _)  => recur(X, t)
+      case tp: AnnotOrCaptType  => recur(X, tp.parent)
       case _: RefinedType       => false
       case _                    => true
     })
@@ -217,7 +217,7 @@ object TypeTestsCasts {
            *  can be true in some cases. Issues a warning or an error otherwise.
            */
           def checkSensical(foundClasses: List[Symbol])(using Context): Boolean =
-            def exprType = i"type ${expr.tpe.widen.stripAnnots}"
+            def exprType = i"type ${expr.tpe.widen.stripped}"
             def check(foundCls: Symbol): Boolean =
               if (!isCheckable(foundCls)) true
               else if (!foundCls.derivesFrom(testCls)) {
diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala
index 5534d0c795fc..90be1f5bed7c 100644
--- a/compiler/src/dotty/tools/dotc/typer/Checking.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala
@@ -70,11 +70,13 @@ object Checking {
         errorTree(arg,
           showInferred(MissingTypeParameterInTypeApp(arg.tpe), app, tpt))
     }
-    for (arg, which, bound) <- TypeOps.boundsViolations(args, boundss, instantiate, app) do
-      report.error(
-          showInferred(DoesNotConformToBound(arg.tpe, which, bound),
-              app, tpt),
-          arg.srcPos.focus)
+    withMode(Mode.RelaxedCapturing) {
+      for (arg, which, bound) <- TypeOps.boundsViolations(args, boundss, instantiate, app) do
+        report.error(
+            showInferred(DoesNotConformToBound(arg.tpe, which, bound),
+                app, tpt),
+            arg.srcPos.focus)
+    }
 
   /** Check that type arguments `args` conform to corresponding bounds in `tl`
    *  Note: This does not check the bounds of AppliedTypeTrees. These
@@ -308,6 +310,7 @@ object Checking {
             case AndType(tp1, tp2) => isInteresting(tp1) || isInteresting(tp2)
             case OrType(tp1, tp2) => isInteresting(tp1) && isInteresting(tp2)
             case _: RefinedOrRecType | _: AppliedType => true
+            case tp: AnnotOrCaptType => isInteresting(tp.parent)
             case _ => false
           }
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
index 6f65d81c1635..51cadd6e698a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -126,8 +126,8 @@ object Inferencing {
       couldInstantiateTypeVar(parent)
     case tp: AndOrType =>
       couldInstantiateTypeVar(tp.tp1) || couldInstantiateTypeVar(tp.tp2)
-    case AnnotatedType(tp, _) =>
-      couldInstantiateTypeVar(tp)
+    case tp: AnnotOrCaptType =>
+      couldInstantiateTypeVar(tp.parent)
     case _ =>
       false
 
@@ -526,6 +526,7 @@ object Inferencing {
     case tp: RecType => tp.derivedRecType(captureWildcards(tp.parent))
     case tp: LazyRef => captureWildcards(tp.ref)
     case tp: AnnotatedType => tp.derivedAnnotatedType(captureWildcards(tp.parent), tp.annot)
+    case tp: CapturingType => tp.derivedCapturingType(captureWildcards(tp.parent), tp.ref)
     case _ => tp
   }
 }
diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
index 2a5a9ca284ac..997bdb0d98a1 100644
--- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -191,6 +191,36 @@ trait TypeAssigner {
     if tpe.isError then tpe
     else errorType(ex"$whatCanNot be accessed as a member of $pre$where.$whyNot", pos)
 
+  def processAppliedType(tree: untpd.Tree, tp: Type)(using Context): Type =
+    def captType(tp: Type, refs: Type): Type = refs match
+      case ref: NamedType =>
+        if ref.isTracked then
+          if tp.captureSet.accountsFor(ref) then
+            report.warning(em"redundant capture: $tp already contains $ref with capture set ${ref.captureSet} in its capture set ${tp.captureSet}", tree.srcPos)
+          CapturingType(tp, ref)
+        else
+          val reason =
+            if ref.canBeTracked then "its capture set is empty"
+            else "it is not a parameter or a local variable"
+          report.error(em"$ref cannot be tracked since $reason", tree.srcPos)
+          tp
+      case OrType(refs1, refs2) =>
+        captType(captType(tp, refs1), refs2)
+      case _ =>
+        report.error(em"$refs is not a legal type for a capture set", tree.srcPos)
+        tp
+    tp match
+      case AppliedType(tycon, args) =>
+        val constr = tycon.typeSymbol
+        if constr == defn.andType then AndType(args(0), args(1))
+        else if constr == defn.orType then OrType(args(0), args(1), soft = false)
+        else if constr == defn.Predef_retainsType then
+          if ctx.settings.Ycc.value then captType(args(0), args(1))
+          else args(0)
+        else tp
+      case _ => tp
+  end processAppliedType
+
   /** Type assignment method. Each method takes as parameters
    *   - an untpd.Tree to which it assigns a type,
    *   - typed child trees it needs to access to cpmpute that type,
@@ -288,8 +318,12 @@ trait TypeAssigner {
     val ownType = fn.tpe.widen match {
       case fntpe: MethodType =>
         if (sameLength(fntpe.paramInfos, args) || ctx.phase.prev.relaxedTyping)
-          if (fntpe.isResultDependent) safeSubstParams(fntpe.resultType, fntpe.paramRefs, args.tpes)
-          else fntpe.resultType
+          if fntpe.isCaptureDependent then
+            fntpe.resultType.substParams(fntpe, args.tpes)
+          else if fntpe.isResultDependent then
+            safeSubstParams(fntpe.resultType, fntpe.paramRefs, args.tpes)
+          else
+            fntpe.resultType
         else
           errorType(i"wrong number of arguments at ${ctx.phase.prev} for $fntpe: ${fn.tpe}, expected: ${fntpe.paramInfos.length}, found: ${args.length}", tree.srcPos)
       case t =>
@@ -461,11 +495,10 @@ trait TypeAssigner {
     assert(!hasNamedArg(args) || ctx.reporter.errorsReported, tree)
     val tparams = tycon.tpe.typeParams
     val ownType =
-      if (sameLength(tparams, args))
-        if (tycon.symbol == defn.andType) AndType(args(0).tpe, args(1).tpe)
-        else if (tycon.symbol == defn.orType) OrType(args(0).tpe, args(1).tpe, soft = false)
-        else tycon.tpe.appliedTo(args.tpes)
-      else wrongNumberOfTypeArgs(tycon.tpe, tparams, args, tree.srcPos)
+      if !sameLength(tparams, args) then
+        wrongNumberOfTypeArgs(tycon.tpe, tparams, args, tree.srcPos)
+      else
+        processAppliedType(tree, tycon.tpe.appliedTo(args.tpes))
     tree.withType(ownType)
   }
 
diff --git a/library/src-bootstrapped/scala/Retains.scala b/library/src-bootstrapped/scala/Retains.scala
new file mode 100644
index 000000000000..ebb825ecd12b
--- /dev/null
+++ b/library/src-bootstrapped/scala/Retains.scala
@@ -0,0 +1,7 @@
+package scala
+
+/** Parent trait that indicates capturing. Example usage:
+ *
+ *   class Foo(using ctx: Context) extends Holds[ctx | CanThrow[Exception]]
+ */
+trait Retains[T]
diff --git a/library/src-bootstrapped/scala/annotation/ability.scala b/library/src-bootstrapped/scala/annotation/ability.scala
new file mode 100644
index 000000000000..150a62ee00c7
--- /dev/null
+++ b/library/src-bootstrapped/scala/annotation/ability.scala
@@ -0,0 +1,8 @@
+package scala.annotation
+
+/** An annotation inidcating that a val should be tracked as its own ability.
+ *  Example:
+ *
+ *   @ability erased val canThrow: * = ???
+ */
+class ability extends StaticAnnotation
\ No newline at end of file
diff --git a/library/src/scala/runtime/stdLibPatches/Predef.scala b/library/src/scala/runtime/stdLibPatches/Predef.scala
index 13dfc77ac60b..1e9dc2303155 100644
--- a/library/src/scala/runtime/stdLibPatches/Predef.scala
+++ b/library/src/scala/runtime/stdLibPatches/Predef.scala
@@ -47,4 +47,8 @@ object Predef:
    */
   extension [T](x: T | Null) inline def nn: x.type & T =
     scala.runtime.Scala3RunTime.nn(x)
+
+  /** type `A` with capture set `B` */
+  infix type retains[A, B]
+
 end Predef

From 445eac73444017491db3342e3cac148fa354438b Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sat, 26 Jun 2021 11:01:59 +0200
Subject: [PATCH 03/25] Suppress Mima checking in build

---
 .github/workflows/ci.yaml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index 1f60ab5b0236..4e91d14c4d88 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -114,9 +114,9 @@ jobs:
           ./project/scripts/sbt ";scala3-bootstrapped/compile; scala3-bootstrapped/test;sjsSandbox/run;sjsSandbox/test;sjsJUnitTests/test;sjsCompilerTests/test ;sbt-test/scripted scala2-compat/* ;configureIDE ;stdlib-bootstrapped/test:run ;stdlib-bootstrapped-tasty-tests/test; scala3-compiler-bootstrapped/scala3CompilerCoursierTest:test"
           ./project/scripts/bootstrapCmdTests
 
-      - name: MiMa
-        run: |
-          ./project/scripts/sbt ";scala3-interfaces/mimaReportBinaryIssues ;scala3-library-bootstrapped/mimaReportBinaryIssues ;scala3-library-bootstrappedJS/mimaReportBinaryIssues"
+      #- name: MiMa
+      #  run: |
+      #    ./project/scripts/sbt ";scala3-interfaces/mimaReportBinaryIssues ;scala3-library-bootstrapped/mimaReportBinaryIssues ;scala3-library-bootstrappedJS/mimaReportBinaryIssues"
 
   test_windows_fast:
     runs-on: [self-hosted, Windows]

From 6e30a15b8a033cb5840efdb061e4cceb707ab13c Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 8 Aug 2021 12:43:33 +0200
Subject: [PATCH 04/25] Add capture set constraints

 - Introduce monadic capture set constraint handling
 - Change CapturingType to take a capture set instead of a single capture reference
---
 compiler/src/dotty/tools/dotc/Compiler.scala  |   2 +-
 .../dotty/tools/dotc/core/CaptureSet.scala    | 176 ++++++++++++++----
 .../dotty/tools/dotc/core/Definitions.scala   |   2 +-
 .../tools/dotc/core/OrderingConstraint.scala  |   2 +-
 .../tools/dotc/core/SymDenotations.scala      |   2 +-
 .../dotty/tools/dotc/core/TypeComparer.scala  |   9 +-
 .../src/dotty/tools/dotc/core/TypeOps.scala   |   6 +-
 .../src/dotty/tools/dotc/core/Types.scala     |  74 ++++----
 .../tools/dotc/core/tasty/TreePickler.scala   |   2 +-
 .../tools/dotc/core/tasty/TreeUnpickler.scala |   2 +-
 .../tools/dotc/printing/PlainPrinter.scala    |   4 +-
 .../src/dotty/tools/dotc/sbt/ExtractAPI.scala |   4 +-
 .../tools/dotc/typer/CheckCaptures.scala      | 146 +++++++++++++++
 .../dotty/tools/dotc/typer/Inferencing.scala  |   4 +-
 .../dotty/tools/dotc/typer/TypeAssigner.scala |  23 +--
 .../dotty/tools/dotc/typer/TyperPhase.scala   |   2 +-
 16 files changed, 353 insertions(+), 107 deletions(-)
 create mode 100644 compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala

diff --git a/compiler/src/dotty/tools/dotc/Compiler.scala b/compiler/src/dotty/tools/dotc/Compiler.scala
index 1337457c273b..434c4fcf1942 100644
--- a/compiler/src/dotty/tools/dotc/Compiler.scala
+++ b/compiler/src/dotty/tools/dotc/Compiler.scala
@@ -3,7 +3,7 @@ package dotc
 
 import core._
 import Contexts._
-import typer.{TyperPhase, RefChecks}
+import typer.{TyperPhase, RefChecks, CheckCaptures}
 import parsing.Parser
 import Phases.Phase
 import transform._
diff --git a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
index d28d271fc3b9..bafaba655cc6 100644
--- a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
@@ -11,40 +11,50 @@ import reporting.trace
 import printing.{Showable, Printer}
 import printing.Texts.*
 
-case class CaptureSet private (elems: CaptureSet.Refs) extends Showable:
+/** A class for capture sets. Capture sets can be constants or variables.
+ */
+sealed abstract class CaptureSet extends Showable:
   import CaptureSet.*
 
-  def isEmpty: Boolean = elems.isEmpty
+  /** The elements of this capture set. For capture variables,
+   *  the elements known so far.
+   */
+  def elems: Refs
+
+  /** Is this capture set constant (i.e. not a capture variable)?
+   */
+  def isConst: Boolean
+
+  /** Is this capture set (always) empty? For capture veraiables, returns
+   *  always false
+   */
+  def isEmpty: Boolean
   def nonEmpty: Boolean = !isEmpty
 
-  private var myClosure: Refs | Null = null
-
-  def closure(using Context): Refs =
-    if myClosure == null then
-      var cl = elems
-      var seen: Refs = SimpleIdentitySet.empty
-      while
-        val prev = cl
-        for ref <- cl do
-          if !seen.contains(ref) then
-            seen += ref
-            cl = cl ++ ref.captureSetOfInfo.elems
-        prev ne cl
-      do ()
-      myClosure = cl
-    myClosure
-
-  def ++ (that: CaptureSet): CaptureSet =
-    if this.isEmpty then that
-    else if that.isEmpty then this
-    else CaptureSet(elems ++ that.elems)
-
-  def + (ref: CaptureRef) =
-    if elems.contains(ref) then this
-    else CaptureSet(elems + ref)
-
-  def intersect (that: CaptureSet): CaptureSet =
-    CaptureSet(this.elems.intersect(that.elems))
+  /** Add new elements to this capture set if allowed.
+   *  @pre `newElems` is not empty and does not overlap with `this.elems`.
+   *  Constant capture sets never allow to add new elements.
+   *  Variables allow it if and only if the new elements can be included
+   *  in all their supersets.
+   *  @return true iff elements were added
+   */
+  protected def addNewElems(newElems: Refs)(using Context): Boolean
+
+  /** If this is a variable, add `cs` as a super set */
+  protected def addSuper(cs: CaptureSet): this.type
+
+  /** If `cs` is a variable, add this capture set as one of its super sets */
+  protected def addSub(cs: CaptureSet): this.type =
+    cs.addSuper(this)
+    this
+
+  /** Try to include all references of `elems` that are not yet accounted by this
+   *  capture set. Inclusion is via `addElems`.
+   *  @return true iff elements were added
+   */
+  protected def tryInclude(elems: Refs)(using Context): Boolean =
+    val unaccounted = elems.filter(!accountsFor(_))
+    unaccounted.isEmpty || addNewElems(unaccounted)
 
   /** {x} <:< this   where <:< is subcapturing */
   def accountsFor(x: CaptureRef)(using Context) =
@@ -52,10 +62,37 @@ case class CaptureSet private (elems: CaptureSet.Refs) extends Showable:
 
   /** The subcapturing test */
   def <:< (that: CaptureSet)(using Context): Boolean =
-    elems.isEmpty || elems.forall(that.accountsFor)
-
+    that.tryInclude(elems) && { addSuper(that); true }
+
+  /** The smallest capture set (via <:<) that is a superset of both
+   *  `this` and `that`
+   */
+  def ++ (that: CaptureSet)(using Context): CaptureSet =
+    if this.isConst && this.elems.forall(that.accountsFor) then that
+    else if that.isConst && that.elems.forall(this.accountsFor) then this
+    else if this.isConst && that.isConst then Const(this.elems ++ that.elems)
+    else Var(this.elems ++ that.elems).addSub(this).addSub(that)
+
+  /** The smallest superset (via <:<) of this capture set that also contains `ref`.
+   */
+  def + (ref: CaptureRef)(using Context) = ++ (ref.singletonCaptureSet)
+
+  /** The largest capture set (via <:<) that is a subset of both `this` and `that`
+   */
+  def intersect(that: CaptureSet)(using Context): CaptureSet =
+    if this.isConst && this.elems.forall(that.accountsFor) then this
+    else if that.isConst && that.elems.forall(this.accountsFor) then that
+    else if this.isConst && that.isConst then Const(this.elems.intersect(that.elems))
+    else Var(this.elems.intersect(that.elems)).addSuper(this).addSuper(that)
+
+  /** capture set obtained by applying `f` to all elements of the current capture set
+   *  and joining the results. If the current capture set is a variable, the same
+   *  transformation is applied to all future additions of new elements.
+   */
   def flatMap(f: CaptureRef => CaptureSet)(using Context): CaptureSet =
-    (empty /: elems)((cs, ref) => cs ++ f(ref))
+    mapRefs(elems, f) match
+      case cs: Const => cs
+      case cs: Var => Mapped(cs, f)
 
   def substParams(tl: BindingType, to: List[Type])(using Context) =
     flatMap {
@@ -63,22 +100,78 @@ case class CaptureSet private (elems: CaptureSet.Refs) extends Showable:
       case ref => ref.singletonCaptureSet
     }
 
-  override def toString = elems.toString
+  def toRetainsTypeArg(using Context): Type =
+    assert(isConst)
+    ((NoType: Type) /: elems) ((tp, ref) =>
+      if tp.exists then OrType(tp, ref, soft = false) else ref)
 
   override def toText(printer: Printer): Text =
     Str("{") ~ Text(elems.toList.map(printer.toTextCaptureRef), ", ") ~ Str("}")
 
 object CaptureSet:
   type Refs = SimpleIdentitySet[CaptureRef]
+  type Vars = SimpleIdentitySet[Var]
+  type Deps = SimpleIdentitySet[CaptureSet]
+
+  private val emptySet = SimpleIdentitySet.empty
+  @sharable private var varId = 0
+
+  val empty: CaptureSet = Const(emptySet)
 
-   @sharable val empty: CaptureSet = CaptureSet(SimpleIdentitySet.empty)
+  /** The universal capture set `{*}` */
+  def universal(using Context): CaptureSet =
+    defn.captureRootType.typeRef.singletonCaptureSet
 
   /** Used as a recursion brake */
-  @sharable private[core] val Pending = CaptureSet(SimpleIdentitySet.empty)
+  @sharable private[core] val Pending = Const(SimpleIdentitySet.empty)
 
   def apply(elems: CaptureRef*)(using Context): CaptureSet =
     if elems.isEmpty then empty
-    else CaptureSet(SimpleIdentitySet(elems.map(_.normalizedRef)*))
+    else Const(SimpleIdentitySet(elems.map(_.normalizedRef)*))
+
+  class Const private[CaptureSet] (val elems: Refs) extends CaptureSet:
+    assert(elems != null)
+    def isConst = true
+    def isEmpty: Boolean = elems.isEmpty
+
+    def addNewElems(elems: Refs)(using Context): Boolean = false
+    def addSuper(cs: CaptureSet) = this
+
+    override def toString = elems.toString
+  end Const
+
+  class Var private[CaptureSet] (initialElems: Refs) extends CaptureSet:
+    val id =
+      varId += 1
+      varId
+
+    var elems: Refs = initialElems
+    var deps: Deps = emptySet
+    def isConst = false
+    def isEmpty = false
+
+    def addNewElems(newElems: Refs)(using Context): Boolean =
+      deps.forall(_.tryInclude(newElems)) && { elems ++= newElems; true }
+
+    def addSuper(cs: CaptureSet) = { deps += cs; this }
+
+    override def toString = s"Var$id$elems"
+  end Var
+
+  class Mapped private[CaptureSet] (cv: Var, f: CaptureRef => CaptureSet) extends Var(cv.elems):
+    addSub(cv)
+
+    override def accountsFor(x: CaptureRef)(using Context): Boolean =
+      f(x).elems.forall(super.accountsFor)
+
+    override def addNewElems(newElems: Refs)(using Context): Boolean =
+      super.addNewElems(mapRefs(newElems, f).elems)
+
+    override def toString = s"Mapped$id$elems"
+  end Mapped
+
+  def mapRefs(xs: Refs, f: CaptureRef => CaptureSet)(using Context): CaptureSet =
+    (empty /: xs)((cs, x) => cs ++ f(x))
 
   def ofClass(cinfo: ClassInfo, argTypes: List[Type])(using Context): CaptureSet =
     def captureSetOf(tp: Type): CaptureSet = tp match
@@ -105,8 +198,8 @@ object CaptureSet:
         tp.captureSet
       case tp: ParamRef =>
         tp.captureSet
-      case CapturingType(parent, ref) =>
-        recur(parent) + ref
+      case CapturingType(parent, refs) =>
+        recur(parent) ++ refs
       case AppliedType(tycon, args) =>
         val cs = recur(tycon)
         tycon.typeParams match
@@ -125,3 +218,8 @@ object CaptureSet:
     recur(tp)
       .showing(i"capture set of $tp = $result", capt)
 
+  def fromRetainsTypeArg(tp: Type)(using Context): CaptureSet = tp match
+    case tp: CaptureRef => tp.singletonCaptureSet
+    case OrType(tp1, tp2) => fromRetainsTypeArg(tp1) ++ fromRetainsTypeArg(tp2)
+
+end CaptureSet
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 12576840671e..f8d71c26d7cd 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -264,7 +264,7 @@ class Definitions {
    */
   @tu lazy val AnyClass: ClassSymbol = completeClass(enterCompleteClassSymbol(ScalaPackageClass, tpnme.Any, Abstract, Nil), ensureCtor = false)
   def AnyType: TypeRef = AnyClass.typeRef
-  @tu lazy val TopType: Type = CapturingType(AnyType, captureRootType.typeRef)
+  @tu lazy val TopType: Type = CapturingType(AnyType, CaptureSet.universal)
   @tu lazy val MatchableClass: ClassSymbol = completeClass(enterCompleteClassSymbol(ScalaPackageClass, tpnme.Matchable, Trait, AnyType :: Nil), ensureCtor = false)
   def MatchableType: TypeRef = MatchableClass.typeRef
   @tu lazy val AnyValClass: ClassSymbol =
diff --git a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
index 4302a9f54fb8..04a135a16bcd 100644
--- a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
@@ -331,7 +331,7 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
         if parent1 ne tp.parent then tp.derivedAnnotatedType(parent1, tp.annot) else tp
       case tp: CapturingType =>
         val parent1 = recur(tp.parent, fromBelow)
-        if parent1 ne tp.parent then tp.derivedCapturingType(parent1, tp.ref) else tp
+        if parent1 ne tp.parent then tp.derivedCapturingType(parent1, tp.refs) else tp
       case _ =>
         val tp1 = tp.dealiasKeepAnnots
         if tp1 ne tp then
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index b795b788f598..f26ee14f8ccf 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -2153,7 +2153,7 @@ object SymDenotations {
             recur(TypeComparer.bounds(tp).hi)
 
           case tp: CapturingType =>
-            tp.derivedCapturingType(recur(tp.parent), tp.ref)
+            tp.derivedCapturingType(recur(tp.parent), tp.refs)
 
           case tp: TypeProxy =>
             def computeTypeProxy = {
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 4f867ba72b25..723b2402331a 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -490,7 +490,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             // under -Ycheck. Test case is i7965.scala.
 
       case tp1: CapturingType =>
-        if tp2.captureSet.accountsFor(tp1.ref) then recur(tp1.parent, tp2)
+        if tp1.refs <:< tp2.captureSet then recur(tp1.parent, tp2)
         else thirdTry
       case tp1: MatchType =>
         val reduced = tp1.reduced
@@ -820,7 +820,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
               //   ---------------------------
               //      E |- x: {x} T
               //
-              CapturingType(tp2, defn.captureRootType.typeRef)
+              CapturingType(tp2, CaptureSet.universal)
             case _ => tp2
           isSubType(tp1.underlying.widenExpr, tp2n, approx.addLow)
         }
@@ -2368,8 +2368,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       tp1.underlying & tp2
     case tp1: AnnotatedType if !tp1.isRefining =>
       tp1.underlying & tp2
-    case tp1: CapturingType if !tp2.captureSet.accountsFor(tp1.ref) =>
-      tp1.parent & tp2
+    case tp1: CapturingType =>
+      if tp2.captureSet <:< tp1.refs then tp1.parent & tp2
+      else tp1.derivedCapturingType(tp1.parent & tp2, tp1.refs)
     case _ =>
       NoType
   }
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index 6362e2d89543..ed0f710028df 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -169,7 +169,7 @@ object TypeOps:
         val normed = tp.tryNormalize
         if (normed.exists) normed else mapOver
       case tp: CapturingType
-      if !ctx.mode.is(Mode.Type) && tp.parent.captureSet.accountsFor(tp.ref) =>
+      if !ctx.mode.is(Mode.Type) && tp.refs <:< tp.parent.captureSet =>
         simplify(tp.parent, theMap)
       case tp: MethodicType =>
         tp // See documentation of `Types#simplified`
@@ -275,7 +275,7 @@ object TypeOps:
         case tp1: RecType =>
           return tp1.rebind(approximateOr(tp1.parent, tp2))
         case tp1: CapturingType =>
-          return tp1.derivedCapturingType(approximateOr(tp1.parent, tp2), tp1.ref)
+          return tp1.derivedCapturingType(approximateOr(tp1.parent, tp2), tp1.refs)
         case err: ErrorType =>
           return err
         case _ =>
@@ -284,7 +284,7 @@ object TypeOps:
         case tp2: RecType =>
           return tp2.rebind(approximateOr(tp1, tp2.parent))
         case tp2: CapturingType =>
-          return tp2.derivedCapturingType(approximateOr(tp1, tp2.parent), tp2.ref)
+          return tp2.derivedCapturingType(approximateOr(tp1, tp2.parent), tp2.refs)
         case err: ErrorType =>
           return err
         case _ =>
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index f5279f271e4a..730b3d877183 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -373,7 +373,7 @@ object Types {
       case tp: AndOrType => tp.tp1.unusableForInference || tp.tp2.unusableForInference
       case tp: LambdaType => tp.resultType.unusableForInference || tp.paramInfos.exists(_.unusableForInference)
       case WildcardType(optBounds) => optBounds.unusableForInference
-      case CapturingType(parent, ref) => parent.unusableForInference || ref.unusableForInference
+      case CapturingType(parent, refs) => parent.unusableForInference || refs.elems.exists(_.unusableForInference)
       case _: ErrorType => true
       case _ => false
 
@@ -1382,7 +1382,7 @@ object Types {
         val tp1 = tp.parent.dealias1(keep)
         if keep(tp) then tp.derivedAnnotatedType(tp1, tp.annot) else tp1
       case tp: CapturingType =>
-        tp.derivedCapturingType(tp.parent.dealias1(keep), tp.ref)
+        tp.derivedCapturingType(tp.parent.dealias1(keep), tp.refs)
       case tp: LazyRef =>
         tp.ref.dealias1(keep)
       case _ => this
@@ -1843,7 +1843,7 @@ object Types {
     }
 
     def capturing(ref: CaptureRef)(using Context): Type =
-      if captureSet.accountsFor(ref) then this else CapturingType(this, ref)
+      if captureSet.accountsFor(ref) then this else CapturingType(this, ref.singletonCaptureSet)
 
     def capturing(cs: CaptureSet)(using Context): Type =
       (this /: cs.elems)(_.capturing(_))
@@ -3688,10 +3688,13 @@ object Types {
           case tp: TypeVar if !tp.isInstantiated => combine(status, Provisional)
           case tp: TermParamRef if tp.binder eq thisLambdaType => TrueDeps
           case tp: CapturingType =>
-            val status1 = compute(status, tp.parent, theAcc)
-            tp.ref match
-              case tp: TermParamRef if tp.binder eq thisLambdaType => combine(status1, CaptureDeps)
-              case _ => status1
+            var status1 = compute(status, tp.parent, theAcc)
+            for ref <- tp.refs.elems do
+              ref match
+                case tp: TermParamRef if tp.binder eq thisLambdaType =>
+                  status1 = combine(status1, CaptureDeps)
+                case _ =>
+            status1
           case _: ThisType | _: BoundType | NoPrefix => status
           case _ =>
             (if theAcc != null then theAcc else DepAcc()).foldOver(status, tp)
@@ -5175,39 +5178,39 @@ object Types {
       unique(CachedAnnotatedType(parent, annot))
   end AnnotatedType
 
-  abstract case class CapturingType(parent: Type, ref: CaptureRef) extends AnnotOrCaptType:
+  abstract case class CapturingType(parent: Type, refs: CaptureSet) extends AnnotOrCaptType:
     override def underlying(using Context): Type = parent
 
-    def derivedCapturingType(parent: Type, ref: CaptureRef)(using Context): CapturingType =
-      if (parent eq this.parent) && (ref eq this.ref) then this
-      else CapturingType(parent, ref)
+    override def captureSet(using Context) = refs
 
-    def derivedCapturing(parent: Type, capt: Type)(using Context): Type =
-      if (parent eq this.parent) && (capt eq this.ref) then this
-      else parent.capturing(capt.captureSet)
+    def derivedCapturingType(parent: Type, refs: CaptureSet)(using Context): Type =
+      if (parent eq this.parent) && (refs eq this.refs) then this
+      else CapturingType(parent, refs)
+
+    def derivedCapturingType(parent: Type, capt: Type)(using Context): Type =
+      parent.capturing(capt.captureSet)
 
     // equals comes from case class; no matching override is needed
 
     override def computeHash(bs: Binders): Int =
-      doHash(bs, parent, ref)
+      doHash(bs, refs, parent)
     override def hashIsStable: Boolean =
-      parent.hashIsStable && ref.hashIsStable
+      parent.hashIsStable
 
     override def eql(that: Type): Boolean = that match
-      case that: CapturingType => (parent eq that.parent) && (ref eq that.ref)
+      case that: CapturingType => (parent eq that.parent) && (refs eq that.refs)
       case _ => false
 
     override def iso(that: Any, bs: BinderPairs): Boolean = that match
-      case that: CapturingType => parent.equals(that.parent, bs) && ref.equals(that.ref, bs)
+      case that: CapturingType => parent.equals(that.parent, bs) && (refs eq that.refs)
       case _ => false
 
-  class CachedCapturingType(parent: Type, ref: CaptureRef) extends CapturingType(parent, ref)
+  class CachedCapturingType(parent: Type, refs: CaptureSet) extends CapturingType(parent, refs)
 
   object CapturingType:
-    def apply(parent: Type, ref: CaptureRef)(using Context): CapturingType =
-      unique(CachedCapturingType(parent, ref.normalizedRef))
-    def checked(parent: Type, ref: Type)(using Context): CapturingType = ref match
-      case ref: CaptureRef => apply(parent, ref)
+    def apply(parent: Type, refs: CaptureSet)(using Context): Type =
+      if refs.isEmpty then parent
+      else unique(CachedCapturingType(parent, refs))
   end CapturingType
 
   // Special type objects and classes -----------------------------------------------------
@@ -5481,8 +5484,8 @@ object Types {
       tp.derivedMatchType(bound, scrutinee, cases)
     protected def derivedAnnotatedType(tp: AnnotatedType, underlying: Type, annot: Annotation): Type =
       tp.derivedAnnotatedType(underlying, annot)
-    protected def derivedCapturing(tp: CapturingType, parent: Type, capt: Type): Type =
-      tp.derivedCapturing(parent, capt)
+    protected def derivedCapturingType(tp: CapturingType, parent: Type, refs: CaptureSet): Type =
+      tp.derivedCapturingType(parent, refs)
     protected def derivedWildcardType(tp: WildcardType, bounds: Type): Type =
       tp.derivedWildcardType(bounds)
     protected def derivedSkolemType(tp: SkolemType, info: Type): Type =
@@ -5562,8 +5565,8 @@ object Types {
           if (underlying1 eq underlying) tp
           else derivedAnnotatedType(tp, underlying1, mapOver(annot))
 
-        case tp @ CapturingType(parent, ref) =>
-          derivedCapturing(tp, this(parent), this(ref))
+        case tp @ CapturingType(parent, refs) =>
+          derivedCapturingType(tp, this(parent), refs.flatMap(this(_).captureSet))
 
         case _: ThisType
           | _: BoundType
@@ -5884,15 +5887,12 @@ object Types {
           if (underlying.isExactlyNothing) underlying
           else tp.derivedAnnotatedType(underlying, annot)
       }
-    override protected def derivedCapturing(tp: CapturingType, parent: Type, capt: Type): Type =
-      capt match
+    override protected def derivedCapturingType(tp: CapturingType, parent: Type, refs: CaptureSet): Type =
+      parent match
         case Range(lo, hi) =>
-          range(derivedCapturing(tp, parent, hi), derivedCapturing(tp, parent, lo))
-        case _ => parent match
-          case Range(lo, hi) =>
-            range(derivedCapturing(tp, lo, capt), derivedCapturing(tp, hi, capt))
-          case _ =>
-            tp.derivedCapturing(parent, capt)
+          range(derivedCapturingType(tp, lo, refs), derivedCapturingType(tp, hi, refs))
+        case _ =>
+          tp.derivedCapturingType(parent, refs)
 
     override protected def derivedWildcardType(tp: WildcardType, bounds: Type): WildcardType =
       tp.derivedWildcardType(rangeToBounds(bounds))
@@ -6033,8 +6033,8 @@ object Types {
       case AnnotatedType(underlying, annot) =>
         this(applyToAnnot(x, annot), underlying)
 
-      case CapturingType(parent, ref) =>
-        this(this(x, parent), ref)
+      case CapturingType(parent, refs) =>
+        (this(x, parent) /: refs.elems)(this)
 
       case tp: ProtoType =>
         tp.fold(x, this)
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index 8ab81fdac6d1..735b8105ee34 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -282,7 +282,7 @@ class TreePickler(pickler: TastyPickler) {
       withLength {
         pickleType(defn.Predef_retainsType.typeRef)
         pickleType(tp.parent)
-        pickleType(tp.ref)
+        pickleType(tp.refs.toRetainsTypeArg)
       }
     case tpe: PolyType if richTypes =>
       pickleMethodic(POLYtype, tpe, EmptyFlags)
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
index 96d80a86e697..66a3be79fd23 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
@@ -361,7 +361,7 @@ class TreeUnpickler(reader: TastyReader,
               val args = until(end)(readType())
               tycon match
                 case tycon: TypeRef if tycon.symbol == defn.Predef_retainsType =>
-                  CapturingType.checked(args(0), args(1))
+                  CapturingType(args(0), CaptureSet.fromRetainsTypeArg(args(1)))
                 case _ =>
                   tycon.appliedTo(args)
             case TYPEBOUNDS =>
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 63c5345c0947..7ed97a65c2e4 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -187,8 +187,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
           keywordStr(" match ") ~ "{" ~ casesText ~ "}" ~
           (" <: " ~ toText(bound) provided !bound.isAny)
         }.close
-      case CapturingType(parent, ref) =>
-        changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toTextCaptureRef(ref))
+      case CapturingType(parent, refs) =>
+        changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toText(refs.toRetainsTypeArg))
       case tp: PreviousErrorType if ctx.settings.XprintTypes.value =>
         "<error>" // do not print previously reported error message because they may try to print this error type again recuresevely
       case tp: ErrorType =>
diff --git a/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala b/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
index a171dfc0ee51..87a64e90da02 100644
--- a/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
+++ b/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
@@ -521,8 +521,8 @@ private class ExtractAPICollector(using Context) extends ThunkHolder {
       case SuperType(thistpe, supertpe) =>
         val s = combineApiTypes(apiType(thistpe), apiType(supertpe))
         withMarker(s, superMarker)
-      case CapturingType(parent, ref) =>
-        val s = combineApiTypes(apiType(parent), apiType(ref))
+      case CapturingType(parent, refs) =>
+        val s = combineApiTypes(apiType(parent), apiType(refs.toRetainsTypeArg))
         withMarker(s, retainsMarker)
       case _ => {
         internalError(i"Unhandled type $tp of class ${tp.getClass}")
diff --git a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
new file mode 100644
index 000000000000..a43332a1d42b
--- /dev/null
+++ b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
@@ -0,0 +1,146 @@
+package dotty.tools
+package dotc
+package typer
+
+import core._
+import Phases.*, DenotTransformers.*, SymDenotations.*
+import Contexts.*, Names.*, Flags.*, Symbols.*, Decorators.*
+import Types._
+import Symbols._
+import StdNames._
+import Decorators._
+import ProtoTypes._
+import Inferencing.isFullyDefined
+import config.Printers.capt
+import ast.{tpd, untpd, Trees}
+import NameKinds.{DocArtifactName, OuterSelectName, DefaultGetterName}
+import Trees._
+import scala.util.control.NonFatal
+import typer.ErrorReporting._
+import util.Spans.Span
+import util.{SimpleIdentitySet, SrcPos}
+import util.Chars.*
+import Nullables._
+import transform.*
+import scala.collection.mutable
+import reporting._
+import ProtoTypes._
+import dotty.tools.backend.jvm.DottyBackendInterface.symExtensions
+
+class CheckCaptures extends Phase:
+  import ast.tpd.*
+
+  def phaseName: String = "cc"
+  override def isEnabled(using Context) = ctx.settings.Ycc.value
+
+  def newRefiner() = CaptureChecker()
+
+  def run(using Context): Unit =
+    val unit = ctx.compilationUnit
+    CaptureChecker().check(unit.tpdTree)
+
+  class CaptureChecker:
+    import ast.tpd.*
+
+    private var myDeps: Dependencies = null
+
+    def deps(using Context): Dependencies =
+      if myDeps == null then
+        myDeps = new Dependencies(ctx.compilationUnit.tpdTree, ctx):
+          def isExpr(sym: Symbol)(using Context): Boolean =
+            sym.isRealClass || sym.isOneOf(MethodOrLazy)
+          def enclosure(using Context) =
+            def recur(owner: Symbol): Symbol =
+              if isExpr(owner) || !owner.exists then owner else recur(owner.owner)
+            recur(ctx.owner)
+      myDeps
+
+    def check(tree: Tree)(using Context): Type = NoType
+
+    private def capturedVars(sym: Symbol)(using Context): CaptureSet =
+      CaptureSet(deps.freeVars(sym).toList.map(_.termRef).filter(_.isTracked)*)
+
+/*
+
+    override def typedClosure(tree: untpd.Closure, pt: Type)(using Context): Tree =
+      super.typedClosure(tree, pt) match
+        case tree1: Closure =>
+          refinr.println(i"typing closure ${tree1.meth.symbol} with fvs ${capturedVars(tree1.meth.symbol)}")
+          tree1.withType(tree1.tpe.capturing(capturedVars(tree1.meth.symbol)))
+        case tree1 => tree1
+
+    override def typedApply(tree: untpd.Apply, pt: Type)(using Context): Tree =
+      super.typedApply(tree, pt) match
+        case tree1 @ Apply(fn, args) =>
+          if tree.fun.symbol.isConstructor then
+            //println(i"typing $tree1, ${capturedVars(tree1.tpe.classSymbol)}")
+            tree1.withType(tree1.tpe.capturing(capturedVars(tree1.tpe.classSymbol)))
+          else
+            tree1
+        case tree1 => tree1
+
+*/
+
+  end CaptureChecker
+
+  inline val disallowGlobal = true
+
+  def checkWellFormed(whole: Type, pos: SrcPos)(using Context): Unit =
+    def checkRelativeVariance(mt: MethodType) = new TypeTraverser:
+      def traverse(tp: Type): Unit = tp match
+        case CapturingType(parent, refs) =>
+          for ref <- refs.elems do
+            ref match
+              case TermParamRef(`mt`, _) =>
+                if variance <= 0 then
+                  val direction = if variance < 0 then "contra" else "in"
+                  report.error(em"captured reference $ref appears ${direction}variantly in type $whole", pos)
+              case _ =>
+          traverse(parent)
+        case _ =>
+          traverseChildren(tp)
+    val checkVariance = new TypeTraverser:
+      def traverse(tp: Type): Unit = tp match
+        case mt: MethodType if mt.isResultDependent =>
+          checkRelativeVariance(mt).traverse(mt)
+        case _ =>
+          traverseChildren(tp)
+    checkVariance.traverse(whole)
+
+  object PostRefinerCheck extends TreeTraverser:
+    def traverse(tree: Tree)(using Context) =
+      tree match
+        case tree1 @ TypeApply(fn, args) if disallowGlobal =>
+          for arg <- args do
+            //println(i"checking $arg in $tree: ${arg.tpe.captureSet}")
+            for ref <- arg.tpe.captureSet.elems do
+              val isGlobal = ref match
+                case ref: TypeRef => ref.isRootCapability
+                case ref: TermRef => ref.prefix != NoPrefix && ref.symbol.hasAnnotation(defn.AbilityAnnot)
+                case _ => false
+              val what = if ref.isRootCapability then "universal" else "global"
+              if isGlobal then
+                val notAllowed = i" is not allowed to capture the $what capability $ref"
+                def msg = arg match
+                  case arg: InferredTypeTree =>
+                    i"""inferred type argument ${arg.tpe}$notAllowed
+                       |
+                       |The inferred arguments are: [$args%, %]"""
+                  case _ => s"type argument$notAllowed"
+                report.error(msg, arg.srcPos)
+        case tree: TypeTree =>
+          // it's inferred, no need to check
+        case _: TypTree | _: Closure =>
+          checkWellFormed(tree.tpe, tree.srcPos)
+        case tree: DefDef =>
+          def check(tp: Type): Unit = tp match
+            case tp: MethodOrPoly => check(tp.resType)
+            case _ =>
+          check(tree.symbol.info)
+        case _ =>
+      traverseChildren(tree)
+
+  def postRefinerCheck(tree: tpd.Tree)(using Context): Unit =
+    PostRefinerCheck.traverse(tree)
+
+end CheckCaptures
diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
index 51cadd6e698a..f779ab1d41ee 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -526,7 +526,7 @@ object Inferencing {
     case tp: RecType => tp.derivedRecType(captureWildcards(tp.parent))
     case tp: LazyRef => captureWildcards(tp.ref)
     case tp: AnnotatedType => tp.derivedAnnotatedType(captureWildcards(tp.parent), tp.annot)
-    case tp: CapturingType => tp.derivedCapturingType(captureWildcards(tp.parent), tp.ref)
+    case tp: CapturingType => tp.derivedCapturingType(captureWildcards(tp.parent), tp.refs)
     case _ => tp
   }
 }
@@ -695,6 +695,7 @@ trait Inferencing { this: Typer =>
           if !argType.isSingleton then argType = SkolemType(argType)
           argType <:< tvar
       case _ =>
+        () // scala-meta complains if this is missing, but I could not mimimize further
   end constrainIfDependentParamRef
 }
 
@@ -709,4 +710,3 @@ trait Inferencing { this: Typer =>
 
 enum IfBottom:
   case ok, fail, flip
-
diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
index 997bdb0d98a1..95724f2f4ece 100644
--- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -192,30 +192,31 @@ trait TypeAssigner {
     else errorType(ex"$whatCanNot be accessed as a member of $pre$where.$whyNot", pos)
 
   def processAppliedType(tree: untpd.Tree, tp: Type)(using Context): Type =
-    def captType(tp: Type, refs: Type): Type = refs match
-      case ref: NamedType =>
+    def include(cs: CaptureSet, tp: Type): CaptureSet = tp match
+      case ref: CaptureRef =>
         if ref.isTracked then
-          if tp.captureSet.accountsFor(ref) then
-            report.warning(em"redundant capture: $tp already contains $ref with capture set ${ref.captureSet} in its capture set ${tp.captureSet}", tree.srcPos)
-          CapturingType(tp, ref)
+          if cs.accountsFor(ref) then
+            report.warning(em"redundant capture: $tp already contains $ref in its capture set $cs", tree.srcPos)
+          cs + ref
         else
           val reason =
             if ref.canBeTracked then "its capture set is empty"
             else "it is not a parameter or a local variable"
           report.error(em"$ref cannot be tracked since $reason", tree.srcPos)
-          tp
-      case OrType(refs1, refs2) =>
-        captType(captType(tp, refs1), refs2)
+          cs
+      case OrType(tp1, tp2) =>
+        include(include(cs, tp1), tp2)
       case _ =>
-        report.error(em"$refs is not a legal type for a capture set", tree.srcPos)
-        tp
+        report.error(em"$tp is not a legal type for a capture set", tree.srcPos)
+        cs
     tp match
       case AppliedType(tycon, args) =>
         val constr = tycon.typeSymbol
         if constr == defn.andType then AndType(args(0), args(1))
         else if constr == defn.orType then OrType(args(0), args(1), soft = false)
         else if constr == defn.Predef_retainsType then
-          if ctx.settings.Ycc.value then captType(args(0), args(1))
+          if ctx.settings.Ycc.value
+          then CapturingType(args(0), include(CaptureSet.empty, args(1)))
           else args(0)
         else tp
       case _ => tp
diff --git a/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala b/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala
index 01082ba7dcbf..0a33faf7a2aa 100644
--- a/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala
@@ -112,7 +112,7 @@ class TyperPhase(addRootImports: Boolean = true) extends Phase {
   def run(using Context): Unit = unsupported("run")
 }
 
-object TyperPhase {
+object  TyperPhase {
   val name: String = "typer"
 }
 

From fd753da0d4ea65911a992ba132b7aa5c9bb93909 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 2 Jul 2021 13:33:58 +0200
Subject: [PATCH 05/25] Make <:< all-or-nothing

Don't allow capture variables to be changed if `<:<` returns false.
---
 .../dotty/tools/dotc/core/CaptureSet.scala    | 40 +++++++++++++++----
 1 file changed, 32 insertions(+), 8 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
index bafaba655cc6..927953169a8b 100644
--- a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
@@ -38,7 +38,7 @@ sealed abstract class CaptureSet extends Showable:
    *  in all their supersets.
    *  @return true iff elements were added
    */
-  protected def addNewElems(newElems: Refs)(using Context): Boolean
+  protected def addNewElems(newElems: Refs)(using Context, VarState): Boolean
 
   /** If this is a variable, add `cs` as a super set */
   protected def addSuper(cs: CaptureSet): this.type
@@ -52,17 +52,25 @@ sealed abstract class CaptureSet extends Showable:
    *  capture set. Inclusion is via `addElems`.
    *  @return true iff elements were added
    */
-  protected def tryInclude(elems: Refs)(using Context): Boolean =
+  protected def tryInclude(elems: Refs)(using Context, VarState): Boolean =
     val unaccounted = elems.filter(!accountsFor(_))
     unaccounted.isEmpty || addNewElems(unaccounted)
 
-  /** {x} <:< this   where <:< is subcapturing */
+  /** {x} <:< this   where <:< is subcapturing, but treating all variables
+   *                 as frozen.
+   */
   def accountsFor(x: CaptureRef)(using Context) =
     elems.contains(x) || !x.isRootCapability && x.captureSetOfInfo <:< this
 
   /** The subcapturing test */
   def <:< (that: CaptureSet)(using Context): Boolean =
-    that.tryInclude(elems) && { addSuper(that); true }
+    given VarState = new VarState
+    val result = that.tryInclude(elems)
+    if result then addSuper(that) else abort()
+    result
+
+  private def abort()(using state: VarState): Unit =
+    state.keysIterator.foreach(_.reset())
 
   /** The smallest capture set (via <:<) that is a superset of both
    *  `this` and `that`
@@ -134,7 +142,7 @@ object CaptureSet:
     def isConst = true
     def isEmpty: Boolean = elems.isEmpty
 
-    def addNewElems(elems: Refs)(using Context): Boolean = false
+    def addNewElems(elems: Refs)(using Context, VarState): Boolean = false
     def addSuper(cs: CaptureSet) = this
 
     override def toString = elems.toString
@@ -150,8 +158,20 @@ object CaptureSet:
     def isConst = false
     def isEmpty = false
 
-    def addNewElems(newElems: Refs)(using Context): Boolean =
-      deps.forall(_.tryInclude(newElems)) && { elems ++= newElems; true }
+    private def recordState()(using VarState) = varState.get(this) match
+      case None => varState(this) = elems
+      case _ =>
+
+    def reset()(using state: VarState): Unit =
+      elems = state(this)
+
+    def addNewElems(newElems: Refs)(using Context, VarState): Boolean =
+      deps.forall(_.tryInclude(newElems))
+      && {
+        recordState()
+        elems ++= newElems
+        true
+      }
 
     def addSuper(cs: CaptureSet) = { deps += cs; this }
 
@@ -164,12 +184,16 @@ object CaptureSet:
     override def accountsFor(x: CaptureRef)(using Context): Boolean =
       f(x).elems.forall(super.accountsFor)
 
-    override def addNewElems(newElems: Refs)(using Context): Boolean =
+    override def addNewElems(newElems: Refs)(using Context, VarState): Boolean =
       super.addNewElems(mapRefs(newElems, f).elems)
 
     override def toString = s"Mapped$id$elems"
   end Mapped
 
+  type VarState = util.EqHashMap[Var, Refs]
+
+  def varState(using state: VarState): VarState = state
+
   def mapRefs(xs: Refs, f: CaptureRef => CaptureSet)(using Context): CaptureSet =
     (empty /: xs)((cs, x) => cs ++ f(x))
 

From 32a5e149c39193448f142b01f8f5171517f3b4e6 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 2 Jul 2021 13:35:50 +0200
Subject: [PATCH 06/25] Add element validation

Add element validation for capture variables. This can be used to
disallow * in instances, or to give better error messages if variable
bounds are violated.
---
 .../dotty/tools/dotc/core/CaptureSet.scala    | 26 ++++++++++++++-----
 1 file changed, 20 insertions(+), 6 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
index 927953169a8b..245fdb7dd0a4 100644
--- a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
@@ -2,7 +2,6 @@ package dotty.tools
 package dotc
 package core
 
-import util.*
 import Types.*, Symbols.*, Flags.*, Contexts.*, Decorators.*
 import config.Printers.capt
 import annotation.threadUnsafe
@@ -10,8 +9,20 @@ import annotation.internal.sharable
 import reporting.trace
 import printing.{Showable, Printer}
 import printing.Texts.*
+import util.SimpleIdentitySet
+import util.common.alwaysTrue
 
 /** A class for capture sets. Capture sets can be constants or variables.
+ *  Capture sets support inclusion constraints <:< where <:< is subcapturing.
+ *  They also allow mapping with arbitrary functions from elements to capture sets,
+ *  by supporting a monadic flatMap operation. That is, constraints can be
+ *  of one of the following forms
+ *
+ *    cs1 <:< cs2
+ *    cs1 = ∪ {f(x) | x ∈ cs2}
+ *
+ *  where the `f`s are arbitrary functions from capture references to capture sets.
+ *  We call the resulting constraint system "monadic set constraints".
  */
 sealed abstract class CaptureSet extends Showable:
   import CaptureSet.*
@@ -148,7 +159,7 @@ object CaptureSet:
     override def toString = elems.toString
   end Const
 
-  class Var private[CaptureSet] (initialElems: Refs) extends CaptureSet:
+  class Var private[CaptureSet] (initialElems: Refs, validate: Refs => Boolean = alwaysTrue) extends CaptureSet:
     val id =
       varId += 1
       varId
@@ -158,6 +169,8 @@ object CaptureSet:
     def isConst = false
     def isEmpty = false
 
+    assert(validate(elems))
+
     private def recordState()(using VarState) = varState.get(this) match
       case None => varState(this) = elems
       case _ =>
@@ -166,7 +179,8 @@ object CaptureSet:
       elems = state(this)
 
     def addNewElems(newElems: Refs)(using Context, VarState): Boolean =
-      deps.forall(_.tryInclude(newElems))
+      validate(newElems)
+      && deps.forall(_.tryInclude(newElems))
       && {
         recordState()
         elems ++= newElems
@@ -190,13 +204,13 @@ object CaptureSet:
     override def toString = s"Mapped$id$elems"
   end Mapped
 
+  def mapRefs(xs: Refs, f: CaptureRef => CaptureSet)(using Context): CaptureSet =
+    (empty /: xs)((cs, x) => cs ++ f(x))
+
   type VarState = util.EqHashMap[Var, Refs]
 
   def varState(using state: VarState): VarState = state
 
-  def mapRefs(xs: Refs, f: CaptureRef => CaptureSet)(using Context): CaptureSet =
-    (empty /: xs)((cs, x) => cs ++ f(x))
-
   def ofClass(cinfo: ClassInfo, argTypes: List[Type])(using Context): CaptureSet =
     def captureSetOf(tp: Type): CaptureSet = tp match
       case tp: TypeRef if tp.symbol.is(ParamAccessor) =>

From dd31f2036a8e5a9cbfce12b935c89d0eece3cd0e Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 2 Jul 2021 16:39:06 +0200
Subject: [PATCH 07/25] Integrate CheckCaptures with Rechecker

---
 compiler/src/dotty/tools/dotc/core/CaptureSet.scala  |  2 +-
 .../src/dotty/tools/dotc/typer/CheckCaptures.scala   | 12 +++---------
 2 files changed, 4 insertions(+), 10 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
index 245fdb7dd0a4..77f4c7221cd2 100644
--- a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
@@ -159,7 +159,7 @@ object CaptureSet:
     override def toString = elems.toString
   end Const
 
-  class Var private[CaptureSet] (initialElems: Refs, validate: Refs => Boolean = alwaysTrue) extends CaptureSet:
+  class Var private[CaptureSet] (initialElems: Refs = emptySet, validate: Refs => Boolean = alwaysTrue) extends CaptureSet:
     val id =
       varId += 1
       varId
diff --git a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
index a43332a1d42b..8d3f6dbe15da 100644
--- a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
@@ -27,19 +27,15 @@ import reporting._
 import ProtoTypes._
 import dotty.tools.backend.jvm.DottyBackendInterface.symExtensions
 
-class CheckCaptures extends Phase:
+class CheckCaptures extends Recheck:
   import ast.tpd.*
 
   def phaseName: String = "cc"
   override def isEnabled(using Context) = ctx.settings.Ycc.value
 
-  def newRefiner() = CaptureChecker()
+  def newRechecker()(using Context) = CaptureChecker(ctx)
 
-  def run(using Context): Unit =
-    val unit = ctx.compilationUnit
-    CaptureChecker().check(unit.tpdTree)
-
-  class CaptureChecker:
+  class CaptureChecker(ictx: Context) extends Rechecker(ictx):
     import ast.tpd.*
 
     private var myDeps: Dependencies = null
@@ -55,8 +51,6 @@ class CheckCaptures extends Phase:
             recur(ctx.owner)
       myDeps
 
-    def check(tree: Tree)(using Context): Type = NoType
-
     private def capturedVars(sym: Symbol)(using Context): CaptureSet =
       CaptureSet(deps.freeVars(sym).toList.map(_.termRef).filter(_.isTracked)*)
 

From bf5f161b1767c768d9c1b6be1d29b46d58175e19 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 8 Aug 2021 19:04:51 +0200
Subject: [PATCH 08/25] Add tests and some fixes

---
 .../src/dotty/tools/dotc/typer/Typer.scala    |  2 +-
 .../dotty/tools/dotc/CompilationTests.scala   |  2 +
 .../allow-deep-subtypes}/i9325.scala          |  0
 tests/neg-custom-args/captures/boxmap.check   |  9 ++++
 tests/neg-custom-args/captures/boxmap.scala   | 15 ++++++
 tests/neg-custom-args/captures/capt-wf.scala  | 18 +++++++
 tests/neg-custom-args/captures/capt1.check    | 42 +++++++++++++++
 tests/neg-custom-args/captures/capt1.scala    | 35 ++++++++++++
 tests/neg-custom-args/captures/capt2.scala    |  8 +++
 tests/neg-custom-args/captures/cc1.scala      |  4 ++
 tests/neg-custom-args/captures/io.scala       | 21 ++++++++
 tests/neg-custom-args/captures/try.check      | 38 +++++++++++++
 tests/neg-custom-args/captures/try.scala      | 52 ++++++++++++++++++
 tests/neg-custom-args/captures/try2.check     | 38 +++++++++++++
 tests/neg-custom-args/captures/try2.scala     | 54 +++++++++++++++++++
 tests/neg-custom-args/captures/try3.scala     | 26 +++++++++
 tests/neg/polymorphic-functions1.check        |  7 +++
 tests/neg/polymorphic-functions1.scala        |  1 +
 tests/pos-custom-args/captures/boxmap.scala   | 21 ++++++++
 .../captures/capt-depfun.scala                | 11 ++++
 tests/pos-custom-args/captures/capt1.scala    | 28 ++++++++++
 .../captures/list-encoding.scala              | 22 ++++++++
 tests/pos-custom-args/captures/try.scala      | 26 +++++++++
 tests/pos-custom-args/captures/try3.scala     | 51 ++++++++++++++++++
 tests/pos/capturing.scala                     |  8 +++
 25 files changed, 538 insertions(+), 1 deletion(-)
 rename tests/{neg => neg-custom-args/allow-deep-subtypes}/i9325.scala (100%)
 create mode 100644 tests/neg-custom-args/captures/boxmap.check
 create mode 100644 tests/neg-custom-args/captures/boxmap.scala
 create mode 100644 tests/neg-custom-args/captures/capt-wf.scala
 create mode 100644 tests/neg-custom-args/captures/capt1.check
 create mode 100644 tests/neg-custom-args/captures/capt1.scala
 create mode 100644 tests/neg-custom-args/captures/capt2.scala
 create mode 100644 tests/neg-custom-args/captures/cc1.scala
 create mode 100644 tests/neg-custom-args/captures/io.scala
 create mode 100644 tests/neg-custom-args/captures/try.check
 create mode 100644 tests/neg-custom-args/captures/try.scala
 create mode 100644 tests/neg-custom-args/captures/try2.check
 create mode 100644 tests/neg-custom-args/captures/try2.scala
 create mode 100644 tests/neg-custom-args/captures/try3.scala
 create mode 100644 tests/neg/polymorphic-functions1.check
 create mode 100644 tests/neg/polymorphic-functions1.scala
 create mode 100644 tests/pos-custom-args/captures/boxmap.scala
 create mode 100644 tests/pos-custom-args/captures/capt-depfun.scala
 create mode 100644 tests/pos-custom-args/captures/capt1.scala
 create mode 100644 tests/pos-custom-args/captures/list-encoding.scala
 create mode 100644 tests/pos-custom-args/captures/try.scala
 create mode 100644 tests/pos-custom-args/captures/try3.scala
 create mode 100644 tests/pos/capturing.scala

diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 906d4e561f95..9ff97cbed778 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1130,7 +1130,7 @@ class Typer extends Namer
         case _ => mapOver(t)
     }
 
-    val pt1 = pt.stripTypeVar.dealias
+    val pt1 = pt.stripped.dealias
     if (pt1 ne pt1.dropDependentRefinement)
        && defn.isContextFunctionType(pt1.nonPrivateMember(nme.apply).info.finalResultType)
     then
diff --git a/compiler/test/dotty/tools/dotc/CompilationTests.scala b/compiler/test/dotty/tools/dotc/CompilationTests.scala
index f2f93ad9165d..583edee5298a 100644
--- a/compiler/test/dotty/tools/dotc/CompilationTests.scala
+++ b/compiler/test/dotty/tools/dotc/CompilationTests.scala
@@ -39,6 +39,7 @@ class CompilationTests {
       compileFilesInDir("tests/pos-special/isInstanceOf", allowDeepSubtypes.and("-Xfatal-warnings")),
       compileFilesInDir("tests/new", defaultOptions),
       compileFilesInDir("tests/pos-scala2", scala2CompatMode),
+      compileFilesInDir("tests/pos-custom-args/captures", defaultOptions.and("-Ycc")),
       compileFilesInDir("tests/pos-custom-args/erased", defaultOptions.and("-language:experimental.erasedDefinitions")),
       compileFilesInDir("tests/pos", defaultOptions.and("-Ysafe-init")),
       compileFilesInDir("tests/pos-deep-subtype", allowDeepSubtypes),
@@ -134,6 +135,7 @@ class CompilationTests {
       compileFilesInDir("tests/neg-custom-args/allow-deep-subtypes", allowDeepSubtypes),
       compileFilesInDir("tests/neg-custom-args/explicit-nulls", defaultOptions.and("-Yexplicit-nulls")),
       compileFilesInDir("tests/neg-custom-args/no-experimental", defaultOptions.and("-Yno-experimental")),
+      compileFilesInDir("tests/neg-custom-args/captures", defaultOptions.and("-Ycc")),
       compileDir("tests/neg-custom-args/impl-conv", defaultOptions.and("-Xfatal-warnings", "-feature")),
       compileFile("tests/neg-custom-args/implicit-conversions.scala", defaultOptions.and("-Xfatal-warnings", "-feature")),
       compileFile("tests/neg-custom-args/implicit-conversions-old.scala", defaultOptions.and("-Xfatal-warnings", "-feature")),
diff --git a/tests/neg/i9325.scala b/tests/neg-custom-args/allow-deep-subtypes/i9325.scala
similarity index 100%
rename from tests/neg/i9325.scala
rename to tests/neg-custom-args/allow-deep-subtypes/i9325.scala
diff --git a/tests/neg-custom-args/captures/boxmap.check b/tests/neg-custom-args/captures/boxmap.check
new file mode 100644
index 000000000000..bbf1879464de
--- /dev/null
+++ b/tests/neg-custom-args/captures/boxmap.check
@@ -0,0 +1,9 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boxmap.scala:15:2 ----------------------------------------
+15 |  () => b[Box[B]]((x: A) => box(f(x)))  // error
+   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |  Found:    (() => Box[B]) retains b retains f
+   |  Required: () => Box[B]
+   |
+   |  where:    B is a type in method lazymap with bounds <: Top
+
+longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/boxmap.scala b/tests/neg-custom-args/captures/boxmap.scala
new file mode 100644
index 000000000000..cb77c6794cb1
--- /dev/null
+++ b/tests/neg-custom-args/captures/boxmap.scala
@@ -0,0 +1,15 @@
+type Top = Any retains *
+class Cap extends Retains[*]
+
+infix type ==> [A, B] = (A => B) retains *
+
+type Box[+T <: Top] = ([K <: Top] => (T ==> K) => K) retains T
+
+def box[T <: Top](x: T): Box[T] =
+  [K <: Top] => (k: T ==> K) => k(x)
+
+def map[A <: Top, B <: Top](b: Box[A])(f: A ==> B): Box[B] =
+  b[Box[B]]((x: A) => box(f(x)))
+
+def lazymap[A <: Top, B <: Top](b: Box[A])(f: A ==> B): () => Box[B] =
+  () => b[Box[B]]((x: A) => box(f(x)))  // error
diff --git a/tests/neg-custom-args/captures/capt-wf.scala b/tests/neg-custom-args/captures/capt-wf.scala
new file mode 100644
index 000000000000..41ed177e853d
--- /dev/null
+++ b/tests/neg-custom-args/captures/capt-wf.scala
@@ -0,0 +1,18 @@
+class C
+type Cap = C retains *
+type Top = Any retains *
+
+type T = (x: Cap) => List[String retains x.type] => Unit // error
+val x: (x: Cap) => Array[String retains x.type] = ??? // error
+val y = x
+
+def test: Unit =
+  def f(x: Cap) = // ok
+    val g = (xs: List[String retains x.type]) => ()
+    g
+  def f2(x: Cap)(xs: List[String retains x.type]) = ()
+  val x = f // error
+  val x2 = f2 // error
+  val y = f(C()) // ok
+  val y2 = f2(C()) // ok
+  ()
diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check
new file mode 100644
index 000000000000..15ba35a52e91
--- /dev/null
+++ b/tests/neg-custom-args/captures/capt1.check
@@ -0,0 +1,42 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:3:2 ------------------------------------------
+3 |  () => if x == null then y else y  // error
+  |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  |  Found:    (() => C) retains x
+  |  Required: () => C
+
+longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:6:2 ------------------------------------------
+6 |  () => if x == null then y else y  // error
+  |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  |  Found:    (() => C) retains x
+  |  Required: Any
+
+longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:14:2 -----------------------------------------
+14 |  f  // error
+   |  ^
+   |  Found:    (Int => Int) retains x
+   |  Required: Any
+
+longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:23:3 -----------------------------------------
+23 |  F(22)  // error
+   |  ^^^^^
+   |  Found:    F retains x
+   |  Required: A
+
+longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:27:40 ----------------------------------------
+27 |    def m() = if x == null then y else y  // error
+   |                                        ^
+   |                                        Found:    A {...} retains x
+   |                                        Required: A
+
+longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:32:24 ----------------------------------------
+32 |  val z2 = h[() => Cap](() => x)(() => C())  // error
+   |                        ^^^^^^^
+   |                        Found:    (() => Cap) retains x
+   |                        Required: () => Cap
+
+longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/capt1.scala b/tests/neg-custom-args/captures/capt1.scala
new file mode 100644
index 000000000000..6f9c02d1540f
--- /dev/null
+++ b/tests/neg-custom-args/captures/capt1.scala
@@ -0,0 +1,35 @@
+class C
+def f(x: C retains *, y: C): () => C =
+  () => if x == null then y else y  // error
+
+def g(x: C retains *, y: C): Any =
+  () => if x == null then y else y  // error
+
+def h1(x: C retains *, y: C): Any retains x.type =
+  def f() = if x == null then y else y
+  () => f()  // ok
+
+def h2(x: C retains *): Any =
+  def f(y: Int) = if x == null then y else y
+  f  // error
+
+class A
+type Cap = C retains *
+type Top = Any retains *
+
+def h3(x: Cap): A =
+  class F(y: Int) extends A:
+    def m() = if x == null then y else y
+  F(22)  // error
+
+def h4(x: Cap, y: Int): A =
+  new A:
+    def m() = if x == null then y else y  // error
+
+def foo() =
+  val x: C retains * = ???
+  def h[X <:Top](a: X)(b: X) = a
+  val z2 = h[() => Cap](() => x)(() => C())  // error
+  val z3 = h[(() => Cap) retains x.type](() => x)(() => C())  // ok
+  val z4 = h[(() => Cap) retains x.type](() => x)(() => C())  // what was inferred for z3
+
diff --git a/tests/neg-custom-args/captures/capt2.scala b/tests/neg-custom-args/captures/capt2.scala
new file mode 100644
index 000000000000..31c549828ad0
--- /dev/null
+++ b/tests/neg-custom-args/captures/capt2.scala
@@ -0,0 +1,8 @@
+class C
+type Cap = C retains *
+
+def f1(c: Cap): (() => C retains c.type) = () => c // ok
+def f2(c: Cap): (() => C) retains c.type = () => c // error
+
+def h5(x: Cap): () => C =
+  f1(x)  // error
diff --git a/tests/neg-custom-args/captures/cc1.scala b/tests/neg-custom-args/captures/cc1.scala
new file mode 100644
index 000000000000..41098a9a3ab6
--- /dev/null
+++ b/tests/neg-custom-args/captures/cc1.scala
@@ -0,0 +1,4 @@
+object Test:
+
+  def f[A <: Any retains *](x: A): Any = x // error
+
diff --git a/tests/neg-custom-args/captures/io.scala b/tests/neg-custom-args/captures/io.scala
new file mode 100644
index 000000000000..a9636b045694
--- /dev/null
+++ b/tests/neg-custom-args/captures/io.scala
@@ -0,0 +1,21 @@
+sealed trait IO:
+  def puts(msg: Any): Unit = println(msg)
+
+def test1 =
+  val IO : IO retains * = new IO {}
+  def foo = IO.puts("hello")
+  val x : () => Unit = () => foo  // error: Found: (() => Unit) retains IO; Required: () => Unit
+
+def test2 =
+  val IO : IO retains * = new IO {}
+  def puts(msg: Any, io: IO retains *) = println(msg)
+  def foo() = puts("hello", IO)
+  val x : () => Unit = () => foo()  // error: Found: (() => Unit) retains IO; Required: () => Unit
+
+type Capability[T] = T retains *
+
+def test3 =
+  val IO : Capability[IO] = new IO {}
+  def puts(msg: Any, io: Capability[IO]) = println(msg)
+  def foo() = puts("hello", IO)
+  val x : () => Unit = () => foo()  // error: Found: (() => Unit) retains IO; Required: () => Unit
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
new file mode 100644
index 000000000000..2a28933971c7
--- /dev/null
+++ b/tests/neg-custom-args/captures/try.check
@@ -0,0 +1,38 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:32 ------------------------------------------
+29 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)  // error
+   |                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |                                Found:    (() => Nothing) retains x
+   |                                Required: () => Nothing
+
+longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:43:2 -------------------------------------------
+43 |  yy  // error
+   |  ^^
+   |  Found:    (yy : List[(xx : (() => Int) retains *)])
+   |  Required: List[() => Int]
+
+longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:50:2 -------------------------------------------
+45 |val global = handle {
+46 |  (x: CanThrow[Exception]) =>
+47 |    () =>
+48 |      raise(new Exception)(using x)
+49 |      22
+50 |} {  // error
+   |             ^
+   |             Found:    (() => Int) retains *
+   |             Required: () => Int
+51 |  (ex: Exception) => () => 22
+52 |}
+
+longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/try.scala:22:28 ---------------------------------------------------------------
+22 |  val a = handle[Exception, CanThrow[Exception]] { // error
+   |                            ^^^^^^^^^^^^^^^^^^^
+   |                            type argument is not allowed to capture the universal capability *
+-- Error: tests/neg-custom-args/captures/try.scala:34:11 ---------------------------------------------------------------
+34 |  val xx = handle { // error
+   |           ^^^^^^
+   |           inferred type argument ((() => Int) retains *) is not allowed to capture the universal capability *
+   |
+   |           The inferred arguments are: [Exception, ((() => Int) retains *)]
diff --git a/tests/neg-custom-args/captures/try.scala b/tests/neg-custom-args/captures/try.scala
new file mode 100644
index 000000000000..4784d055fccc
--- /dev/null
+++ b/tests/neg-custom-args/captures/try.scala
@@ -0,0 +1,52 @@
+import language.experimental.erasedDefinitions
+
+class CT[E <: Exception]
+type CanThrow[E <: Exception] = CT[E] retains *
+type Top  = Any retains *
+
+infix type throws[R, E <: Exception] = (erased CanThrow[E]) ?=> R
+
+class Fail extends Exception
+
+def raise[E <: Exception](e: E): Nothing throws E = throw e
+
+def foo(x: Boolean): Int throws Fail =
+  if x then 1 else raise(Fail())
+
+def handle[E <: Exception, R <: Top](op: CanThrow[E] => R)(handler: E => R): R =
+  val x: CanThrow[E] = ???
+  try op(x)
+  catch case ex: E => handler(ex)
+
+def test: List[() => Int] =
+  val a = handle[Exception, CanThrow[Exception]] { // error
+    (x: CanThrow[Exception]) => x
+  }{
+    (ex: Exception) => ???
+  }
+
+  val b = handle[Exception, () => Nothing] {
+    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)  // error
+  } {
+    (ex: Exception) => ???
+  }
+
+  val xx = handle { // error
+    (x: CanThrow[Exception]) =>
+      () =>
+        raise(new Exception)(using x)
+        22
+  } {
+    (ex: Exception) => () => 22
+  }
+  val yy = xx :: Nil
+  yy  // error
+
+val global = handle {
+  (x: CanThrow[Exception]) =>
+    () =>
+      raise(new Exception)(using x)
+      22
+} {  // error
+  (ex: Exception) => () => 22
+}
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/try2.check b/tests/neg-custom-args/captures/try2.check
new file mode 100644
index 000000000000..a73ee901406d
--- /dev/null
+++ b/tests/neg-custom-args/captures/try2.check
@@ -0,0 +1,38 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try2.scala:31:32 -----------------------------------------
+31 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)  // error
+   |                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |                                Found:    (() => Nothing) retains x
+   |                                Required: () => Nothing
+
+longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try2.scala:45:2 ------------------------------------------
+45 |  yy  // error
+   |  ^^
+   |  Found:    (yy : List[(xx : (() => Int) retains canThrow)])
+   |  Required: List[() => Int]
+
+longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try2.scala:52:2 ------------------------------------------
+47 |val global = handle {
+48 |  (x: CanThrow[Exception]) =>
+49 |    () =>
+50 |      raise(new Exception)(using x)
+51 |      22
+52 |} {  // error
+   |             ^
+   |             Found:    (() => Int) retains canThrow
+   |             Required: () => Int
+53 |  (ex: Exception) => () => 22
+54 |}
+
+longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/try2.scala:24:28 --------------------------------------------------------------
+24 |  val a = handle[Exception, CanThrow[Exception]] { // error
+   |                            ^^^^^^^^^^^^^^^^^^^
+   |                            type argument is not allowed to capture the global capability (canThrow : *)
+-- Error: tests/neg-custom-args/captures/try2.scala:36:11 --------------------------------------------------------------
+36 |  val xx = handle { // error
+   |           ^^^^^^
+   |inferred type argument ((() => Int) retains canThrow) is not allowed to capture the global capability (canThrow : *)
+   |
+   |The inferred arguments are: [Exception, ((() => Int) retains canThrow)]
diff --git a/tests/neg-custom-args/captures/try2.scala b/tests/neg-custom-args/captures/try2.scala
new file mode 100644
index 000000000000..469d9cf8d2f2
--- /dev/null
+++ b/tests/neg-custom-args/captures/try2.scala
@@ -0,0 +1,54 @@
+import language.experimental.erasedDefinitions
+import annotation.ability
+
+@ability erased val canThrow: * = ???
+
+class CanThrow[E <: Exception] extends Retains[canThrow.type]
+type Top  = Any retains *
+
+infix type throws[R, E <: Exception] = (erased CanThrow[E]) ?=> R
+
+class Fail extends Exception
+
+def raise[E <: Exception](e: E): Nothing throws E = throw e
+
+def foo(x: Boolean): Int throws Fail =
+  if x then 1 else raise(Fail())
+
+def handle[E <: Exception, R <: Top](op: CanThrow[E] => R)(handler: E => R): R =
+  val x: CanThrow[E] = ???
+  try op(x)
+  catch case ex: E => handler(ex)
+
+def test: List[() => Int] =
+  val a = handle[Exception, CanThrow[Exception]] { // error
+    (x: CanThrow[Exception]) => x
+  }{
+    (ex: Exception) => ???
+  }
+
+  val b = handle[Exception, () => Nothing] {
+    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)  // error
+  } {
+    (ex: Exception) => ???
+  }
+
+  val xx = handle { // error
+    (x: CanThrow[Exception]) =>
+      () =>
+        raise(new Exception)(using x)
+        22
+  } {
+    (ex: Exception) => () => 22
+  }
+  val yy = xx :: Nil
+  yy  // error
+
+val global = handle {
+  (x: CanThrow[Exception]) =>
+    () =>
+      raise(new Exception)(using x)
+      22
+} {  // error
+  (ex: Exception) => () => 22
+}
diff --git a/tests/neg-custom-args/captures/try3.scala b/tests/neg-custom-args/captures/try3.scala
new file mode 100644
index 000000000000..f90ad6aff0aa
--- /dev/null
+++ b/tests/neg-custom-args/captures/try3.scala
@@ -0,0 +1,26 @@
+import java.io.IOException
+
+class CanThrow[E] extends Retains[*]
+type Top  = Any retains *
+
+def handle[E <: Exception, T <: Top](op: CanThrow[E] ?=> T)(handler: E => T): T =
+  val x: CanThrow[E] = ???
+  try op(using x)
+  catch case ex: E => handler(ex)
+
+def raise[E <: Exception](ex: E)(using CanThrow[E]): Nothing =
+  throw ex
+
+@main def Test: Int =
+  def f(a: Boolean) =
+    handle { // error
+      if !a then raise(IOException())
+      (b: Boolean) =>
+        if !b then raise(IOException())
+        0
+    } {
+      ex => (b: Boolean) => -1
+    }
+  val g = f(true)
+  g(false) // would raise an uncaught exception
+  f(true)(false) // would raise an uncaught exception
diff --git a/tests/neg/polymorphic-functions1.check b/tests/neg/polymorphic-functions1.check
new file mode 100644
index 000000000000..b9459340fac7
--- /dev/null
+++ b/tests/neg/polymorphic-functions1.check
@@ -0,0 +1,7 @@
+-- [E007] Type Mismatch Error: tests/neg/polymorphic-functions1.scala:1:53 ---------------------------------------------
+1 |val f: [T] => (x: T) => x.type = [T] => (x: Int) => x // error
+  |                                                     ^
+  |                                                     Found:    [T] => (Int) => Int
+  |                                                     Required: [T] => (x: T) => x.type
+
+longer explanation available when compiling with `-explain`
diff --git a/tests/neg/polymorphic-functions1.scala b/tests/neg/polymorphic-functions1.scala
new file mode 100644
index 000000000000..de887f3b8c50
--- /dev/null
+++ b/tests/neg/polymorphic-functions1.scala
@@ -0,0 +1 @@
+val f: [T] => (x: T) => x.type = [T] => (x: Int) => x // error
diff --git a/tests/pos-custom-args/captures/boxmap.scala b/tests/pos-custom-args/captures/boxmap.scala
new file mode 100644
index 000000000000..50a84e5c6ae5
--- /dev/null
+++ b/tests/pos-custom-args/captures/boxmap.scala
@@ -0,0 +1,21 @@
+type Top = Any retains *
+class Cap extends Retains[*]
+
+infix type ==> [A, B] = (A => B) retains *
+
+type Box[+T <: Top] = ([K <: Top] => (T ==> K) => K) retains T
+
+def box[T <: Top](x: T): Box[T] =
+  [K <: Top] => (k: T ==> K) => k(x)
+
+def map[A <: Top, B <: Top](b: Box[A])(f: A ==> B): Box[B] =
+  b[Box[B]]((x: A) => box(f(x)))
+
+def lazymap[A <: Top, B <: Top](b: Box[A])(f: A ==> B): (() => Box[B]) retains b.type | f.type =
+  () => b[Box[B]]((x: A) => box(f(x)))
+
+def test[A <: Top, B <: Top] =
+  def lazymap[A <: Top, B <: Top](b: Box[A])(f: A ==> B) =
+    () => b[Box[B]]((x: A) => box(f(x)))
+  val x: (b: Box[A]) => ((f: A ==> B) => (() => Box[B]) retains b.type | f.type) retains b.type = lazymap[A, B]
+  ()
diff --git a/tests/pos-custom-args/captures/capt-depfun.scala b/tests/pos-custom-args/captures/capt-depfun.scala
new file mode 100644
index 000000000000..ac69d72c1af2
--- /dev/null
+++ b/tests/pos-custom-args/captures/capt-depfun.scala
@@ -0,0 +1,11 @@
+class C
+type Cap = C retains *
+type Top = Any retains *
+
+type T = (x: Cap) => String retains x.type
+
+def f(y: Cap): String retains * =
+  val a: T = (x: Cap) => ""
+  val b = a(y)
+  val c: String retains y.type = b
+  c
diff --git a/tests/pos-custom-args/captures/capt1.scala b/tests/pos-custom-args/captures/capt1.scala
new file mode 100644
index 000000000000..58560f940cc9
--- /dev/null
+++ b/tests/pos-custom-args/captures/capt1.scala
@@ -0,0 +1,28 @@
+class C
+type Cap = C retains *
+type Top = Any retains *
+def f1(c: Cap): (() => c.type) retains c.type = () => c // ok
+/*
+def f2: Int =
+  val g: (Boolean => Int) retains * = ???
+  val x = g(true)
+  x
+
+def f3: Int =
+  def g: (Boolean => Int) retains * = ???
+  def h = g
+  val x = g.apply(true)
+  x
+
+def foo() =
+  val x: C retains * = ???
+  val y: C retains x.type = x
+  val x2: (() => C) retains x.type = ???
+  val y2: (() => C retains x.type) retains x.type = x2
+
+  val z1: (() => Cap) retains * = f1(x)
+  def h[X <:Top](a: X)(b: X) = a
+
+  val z2 =
+    if x == null then () => x else () => C()
+*/
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/list-encoding.scala b/tests/pos-custom-args/captures/list-encoding.scala
new file mode 100644
index 000000000000..91cf6d92c08f
--- /dev/null
+++ b/tests/pos-custom-args/captures/list-encoding.scala
@@ -0,0 +1,22 @@
+type Top = Any retains *
+class Cap extends Retains[*]
+
+type Op[T <: Top, C <: Top] =
+  ((v: T) => ((s: C) => C) retains *) retains *
+
+type List[T <: Top] =
+  ([C <: Top] => (op: Op[T, C]) => ((s: C) => C) retains op.type) retains T
+
+def nil[T <: Top]: List[T] =
+  [C <: Top] => (op: Op[T, C]) => (s: C) => s
+
+def cons[T <: Top](hd: T, tl: List[T]): List[T] =
+  [C <: Top] => (op: Op[T, C]) => (s: C) => op(hd)(tl(op)(s))
+
+def foo(c: Cap) =
+  def f(x: String retains c.type, y: String retains c.type) =
+    cons(x, cons(y, nil))
+  def g(x: String retains c.type, y: Any) =
+    cons(x, cons(y, nil))
+  def h(x: String, y: Any retains c.type) =
+    cons(x, cons(y, nil))
diff --git a/tests/pos-custom-args/captures/try.scala b/tests/pos-custom-args/captures/try.scala
new file mode 100644
index 000000000000..e251ed72e48d
--- /dev/null
+++ b/tests/pos-custom-args/captures/try.scala
@@ -0,0 +1,26 @@
+import language.experimental.erasedDefinitions
+
+class CT[E <: Exception]
+type CanThrow[E <: Exception] = CT[E] retains *
+
+infix type throws[R, E <: Exception] = (erased CanThrow[E]) ?=> R
+
+class Fail extends Exception
+
+def raise[E <: Exception](e: E): Nothing throws E = throw e
+
+def foo(x: Boolean): Int throws Fail =
+  if x then 1 else raise(Fail())
+
+def handle[E <: Exception, R](op: (erased CanThrow[E]) => R)(handler: E => R): R =
+  erased val x: CanThrow[E] = ???
+  try op(x)
+  catch case ex: E => handler(ex)
+
+val _ = handle { (erased x) =>
+    if true then
+      raise(new Exception)(using x)
+      22
+    else
+      11
+  }
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/try3.scala b/tests/pos-custom-args/captures/try3.scala
new file mode 100644
index 000000000000..1d1e9925da33
--- /dev/null
+++ b/tests/pos-custom-args/captures/try3.scala
@@ -0,0 +1,51 @@
+import language.experimental.erasedDefinitions
+import annotation.ability
+import java.io.IOException
+
+class CanThrow[E] extends Retains[*]
+type Top  = Any retains *
+
+def handle[E <: Exception, T <: Top](op: CanThrow[E] ?=> T)(handler: E => T): T =
+  val x: CanThrow[E] = ???
+  try op(using x)
+  catch case ex: E => handler(ex)
+
+def raise[E <: Exception](ex: E)(using CanThrow[E]): Nothing =
+  throw ex
+
+def test1: Int =
+  def f(a: Boolean): Boolean => CanThrow[IOException] ?=> Int =
+    handle { // error
+      if !a then raise(IOException())
+      (b: Boolean) => (_: CanThrow[IOException]) ?=>
+        if !b then raise(IOException())
+        0
+    } {
+      ex => (b: Boolean) => (_: CanThrow[IOException]) ?=> -1
+    }
+  handle {
+    val g = f(true)
+    g(false) // would raise an uncaught exception
+    f(true)(false) // would raise an uncaught exception
+  } {
+    ex => -1
+  }
+/*
+def test2: Int =
+  def f(a: Boolean): Boolean => CanThrow[IOException] ?=> Int =
+    handle { // error
+      if !a then raise(IOException())
+      (b: Boolean) =>
+        if !b then raise(IOException())
+        0
+    } {
+      ex => (b: Boolean) => -1
+    }
+  handle {
+    val g = f(true)
+    g(false) // would raise an uncaught exception
+    f(true)(false) // would raise an uncaught exception
+  } {
+    ex => -1
+  }
+*/
\ No newline at end of file
diff --git a/tests/pos/capturing.scala b/tests/pos/capturing.scala
new file mode 100644
index 000000000000..6c1fbaada739
--- /dev/null
+++ b/tests/pos/capturing.scala
@@ -0,0 +1,8 @@
+object Test:
+
+  extension [A <: Any retains *] (xs: LazyList[A])
+    def lazyMap[B <: Any retains *] (f: (A => B) retains *): LazyList[B] retains f.type | A | B =
+      val x: Int retains f.type | A = ???
+      val y = x
+      val z: Int retains A retains f.type = y
+      ???

From 6ab93dddc0c14e573c8fb05488d9bdca89ffb02a Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 11 Aug 2021 12:54:47 +0200
Subject: [PATCH 09/25] Add iterator method to SimpleIdentitySet

---
 .../dotty/tools/dotc/util/SimpleIdentitySet.scala   | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/compiler/src/dotty/tools/dotc/util/SimpleIdentitySet.scala b/compiler/src/dotty/tools/dotc/util/SimpleIdentitySet.scala
index ffca320d53d3..5e8ae0ed872c 100644
--- a/compiler/src/dotty/tools/dotc/util/SimpleIdentitySet.scala
+++ b/compiler/src/dotty/tools/dotc/util/SimpleIdentitySet.scala
@@ -14,6 +14,7 @@ abstract class SimpleIdentitySet[+Elem <: AnyRef] {
   def exists[E >: Elem <: AnyRef](p: E => Boolean): Boolean
   def /: [A, E >: Elem <: AnyRef](z: A)(f: (A, E) => A): A
   def toList: List[Elem]
+  def iterator: Iterator[Elem]
 
   final def isEmpty: Boolean = size == 0
 
@@ -57,6 +58,7 @@ object SimpleIdentitySet {
     def exists[E <: AnyRef](p: E => Boolean): Boolean = false
     def /: [A, E <: AnyRef](z: A)(f: (A, E) => A): A = z
     def toList = Nil
+    def iterator = Iterator.empty
   }
 
   private class Set1[+Elem <: AnyRef](x0: AnyRef) extends SimpleIdentitySet[Elem] {
@@ -72,6 +74,7 @@ object SimpleIdentitySet {
     def /: [A, E >: Elem <: AnyRef](z: A)(f: (A, E) => A): A =
       f(z, x0.asInstanceOf[E])
     def toList = x0.asInstanceOf[Elem] :: Nil
+    def iterator = Iterator.single(x0.asInstanceOf[Elem])
   }
 
   private class Set2[+Elem <: AnyRef](x0: AnyRef, x1: AnyRef) extends SimpleIdentitySet[Elem] {
@@ -89,6 +92,10 @@ object SimpleIdentitySet {
     def /: [A, E >: Elem <: AnyRef](z: A)(f: (A, E) => A): A =
       f(f(z, x0.asInstanceOf[E]), x1.asInstanceOf[E])
     def toList = x0.asInstanceOf[Elem] :: x1.asInstanceOf[Elem] :: Nil
+    def iterator = Iterator.tabulate(2) {
+      case 0 => x0.asInstanceOf[Elem]
+      case 1 => x1.asInstanceOf[Elem]
+    }
   }
 
   private class Set3[+Elem <: AnyRef](x0: AnyRef, x1: AnyRef, x2: AnyRef) extends SimpleIdentitySet[Elem] {
@@ -117,6 +124,11 @@ object SimpleIdentitySet {
     def /: [A, E >: Elem <: AnyRef](z: A)(f: (A, E) => A): A =
       f(f(f(z, x0.asInstanceOf[E]), x1.asInstanceOf[E]), x2.asInstanceOf[E])
     def toList = x0.asInstanceOf[Elem] :: x1.asInstanceOf[Elem] :: x2.asInstanceOf[Elem] :: Nil
+    def iterator = Iterator.tabulate(3) {
+      case 0 => x0.asInstanceOf[Elem]
+      case 1 => x1.asInstanceOf[Elem]
+      case 2 => x2.asInstanceOf[Elem]
+    }
   }
 
   private class SetN[+Elem <: AnyRef](val xs: Array[AnyRef]) extends SimpleIdentitySet[Elem] {
@@ -163,6 +175,7 @@ object SimpleIdentitySet {
       foreach(buf += _)
       buf.toList
     }
+    def iterator = xs.iterator.asInstanceOf[Iterator[Elem]]
     override def ++ [E >: Elem <: AnyRef](that: SimpleIdentitySet[E]): SimpleIdentitySet[E] =
       that match {
         case that: SetN[?] =>

From e03ef8c7fe3bcce4ab4067b1c8de44e1d69425ce Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 13 Aug 2021 16:05:43 +0200
Subject: [PATCH 10/25] Cleanups and annotations suggesting changes and
 removals

---
 .../src/dotty/tools/dotc/core/CaptureSet.scala     |  2 ++
 compiler/src/dotty/tools/dotc/core/Mode.scala      |  2 +-
 compiler/src/dotty/tools/dotc/core/Types.scala     | 14 ++++++--------
 .../src/dotty/tools/dotc/typer/CheckCaptures.scala |  1 +
 compiler/src/dotty/tools/dotc/typer/Checking.scala |  2 +-
 .../src/dotty/tools/dotc/typer/TyperPhase.scala    |  2 +-
 .../scala/annotation/ability.scala                 |  1 +
 7 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
index 77f4c7221cd2..c480c46523d9 100644
--- a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
@@ -192,9 +192,11 @@ object CaptureSet:
     override def toString = s"Var$id$elems"
   end Var
 
+  /** The set `Union { f(x) | x <- cv }` */
   class Mapped private[CaptureSet] (cv: Var, f: CaptureRef => CaptureSet) extends Var(cv.elems):
     addSub(cv)
 
+    // ^^^ ???, seems wrong
     override def accountsFor(x: CaptureRef)(using Context): Boolean =
       f(x).elems.forall(super.accountsFor)
 
diff --git a/compiler/src/dotty/tools/dotc/core/Mode.scala b/compiler/src/dotty/tools/dotc/core/Mode.scala
index a752a7e7f5b4..b984ccce095a 100644
--- a/compiler/src/dotty/tools/dotc/core/Mode.scala
+++ b/compiler/src/dotty/tools/dotc/core/Mode.scala
@@ -125,5 +125,5 @@ object Mode {
    */
   val ForceInline: Mode = newMode(29, "ForceInline")
 
-  val RelaxedCapturing: Mode = newMode(30, "RelaxedCapturing")
+  val RelaxedCapturing: Mode = newMode(30, "RelaxedCapturing") // ^^^ needed?
 }
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 730b3d877183..e0e98096b5e5 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -3688,13 +3688,11 @@ object Types {
           case tp: TypeVar if !tp.isInstantiated => combine(status, Provisional)
           case tp: TermParamRef if tp.binder eq thisLambdaType => TrueDeps
           case tp: CapturingType =>
-            var status1 = compute(status, tp.parent, theAcc)
-            for ref <- tp.refs.elems do
-              ref match
-                case tp: TermParamRef if tp.binder eq thisLambdaType =>
-                  status1 = combine(status1, CaptureDeps)
-                case _ =>
-            status1
+            (compute(status, tp.parent, theAcc) /: tp.refs.elems) {
+              (s, ref) => ref match
+                case tp: TermParamRef if tp.binder eq thisLambdaType => combine(s, CaptureDeps)
+                case _ => s
+            }
           case _: ThisType | _: BoundType | NoPrefix => status
           case _ =>
             (if theAcc != null then theAcc else DepAcc()).foldOver(status, tp)
@@ -5888,7 +5886,7 @@ object Types {
           else tp.derivedAnnotatedType(underlying, annot)
       }
     override protected def derivedCapturingType(tp: CapturingType, parent: Type, refs: CaptureSet): Type =
-      parent match
+      parent match // ^^^ handle ranges in capture sets as well
         case Range(lo, hi) =>
           range(derivedCapturingType(tp, lo, refs), derivedCapturingType(tp, hi, refs))
         case _ =>
diff --git a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
index 8d3f6dbe15da..141e17207167 100644
--- a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
@@ -79,6 +79,7 @@ class CheckCaptures extends Recheck:
 
   inline val disallowGlobal = true
 
+  // ^^^ todo: drop wf condition; work into parameter substitution
   def checkWellFormed(whole: Type, pos: SrcPos)(using Context): Unit =
     def checkRelativeVariance(mt: MethodType) = new TypeTraverser:
       def traverse(tp: Type): Unit = tp match
diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala
index 90be1f5bed7c..5726f5939694 100644
--- a/compiler/src/dotty/tools/dotc/typer/Checking.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala
@@ -70,7 +70,7 @@ object Checking {
         errorTree(arg,
           showInferred(MissingTypeParameterInTypeApp(arg.tpe), app, tpt))
     }
-    withMode(Mode.RelaxedCapturing) {
+    withMode(Mode.RelaxedCapturing) { // ^^^ todo: remove
       for (arg, which, bound) <- TypeOps.boundsViolations(args, boundss, instantiate, app) do
         report.error(
             showInferred(DoesNotConformToBound(arg.tpe, which, bound),
diff --git a/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala b/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala
index 0a33faf7a2aa..01082ba7dcbf 100644
--- a/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala
@@ -112,7 +112,7 @@ class TyperPhase(addRootImports: Boolean = true) extends Phase {
   def run(using Context): Unit = unsupported("run")
 }
 
-object  TyperPhase {
+object TyperPhase {
   val name: String = "typer"
 }
 
diff --git a/library/src-bootstrapped/scala/annotation/ability.scala b/library/src-bootstrapped/scala/annotation/ability.scala
index 150a62ee00c7..8b327a2f8b02 100644
--- a/library/src-bootstrapped/scala/annotation/ability.scala
+++ b/library/src-bootstrapped/scala/annotation/ability.scala
@@ -4,5 +4,6 @@ package scala.annotation
  *  Example:
  *
  *   @ability erased val canThrow: * = ???
+ *  ^^^ rename to capability
  */
 class ability extends StaticAnnotation
\ No newline at end of file

From e76cb7d3f97aed156165665b710f29cde44cc254 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 15 Aug 2021 15:44:13 +0200
Subject: [PATCH 11/25] Initial capture checker with boxes

---
 .../dotty/tools/dotc/core/CaptureSet.scala    | 190 ++++++++++----
 .../dotty/tools/dotc/core/Definitions.scala   |  10 +-
 .../dotty/tools/dotc/core/TypeComparer.scala  |   5 +-
 .../dotty/tools/dotc/core/TypeErrors.scala    |   1 +
 .../src/dotty/tools/dotc/core/TypeOps.scala   |   3 +-
 .../src/dotty/tools/dotc/core/Types.scala     |  51 ++--
 .../tools/dotc/printing/PlainPrinter.scala    |   5 +-
 .../dotty/tools/dotc/transform/Recheck.scala  |   3 +-
 .../tools/dotc/typer/CheckCaptures.scala      | 235 +++++++++++-------
 .../dotty/tools/dotc/typer/TypeAssigner.scala |   2 +-
 tests/pos-custom-args/captures/boxmap.scala   |   7 +-
 11 files changed, 335 insertions(+), 177 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
index c480c46523d9..796db92344ba 100644
--- a/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/core/CaptureSet.scala
@@ -47,9 +47,10 @@ sealed abstract class CaptureSet extends Showable:
    *  Constant capture sets never allow to add new elements.
    *  Variables allow it if and only if the new elements can be included
    *  in all their supersets.
-   *  @return true iff elements were added
+   *  @return CompareResult.OK if elements were added, or a conflicting
+   *          capture set that prevents addition otherwise.
    */
-  protected def addNewElems(newElems: Refs)(using Context, VarState): Boolean
+  protected def addNewElems(newElems: Refs)(using Context, VarState): CompareResult
 
   /** If this is a variable, add `cs` as a super set */
   protected def addSuper(cs: CaptureSet): this.type
@@ -60,29 +61,34 @@ sealed abstract class CaptureSet extends Showable:
     this
 
   /** Try to include all references of `elems` that are not yet accounted by this
-   *  capture set. Inclusion is via `addElems`.
-   *  @return true iff elements were added
+   *  capture set. Inclusion is via `addNewElems`.
+   *  @return  CompareResult.OK if all unaccounted elements could be added,
+   *           capture set that prevents addition otherwise.
    */
-  protected def tryInclude(elems: Refs)(using Context, VarState): Boolean =
+  protected def tryInclude(elems: Refs)(using Context, VarState): CompareResult =
     val unaccounted = elems.filter(!accountsFor(_))
-    unaccounted.isEmpty || addNewElems(unaccounted)
+    if unaccounted.isEmpty then CompareResult.OK else addNewElems(unaccounted)
 
   /** {x} <:< this   where <:< is subcapturing, but treating all variables
    *                 as frozen.
    */
-  def accountsFor(x: CaptureRef)(using Context) =
-    elems.contains(x) || !x.isRootCapability && x.captureSetOfInfo <:< this
+  def accountsFor(x: CaptureRef)(using Context): Boolean =
+    elems.contains(x)
+    || !x.isRootCapability && (x.captureSetOfInfo frozen_<:< this) == CompareResult.OK
 
   /** The subcapturing test */
-  def <:< (that: CaptureSet)(using Context): Boolean =
-    given VarState = new VarState
+  def <:< (that: CaptureSet)(using Context): CompareResult =
+    subcaptures(that)(using ctx, VarState())
+
+  /** The subcapturing test, where all variables are treated as frozen */
+  def frozen_<:<(that: CaptureSet)(using Context): CompareResult =
+    subcaptures(that)(using ctx, FrozenState)
+
+  private def subcaptures(that: CaptureSet)(using Context, VarState): CompareResult =
     val result = that.tryInclude(elems)
-    if result then addSuper(that) else abort()
+    if result == CompareResult.OK then addSuper(that) else varState.abort()
     result
 
-  private def abort()(using state: VarState): Unit =
-    state.keysIterator.foreach(_.reset())
-
   /** The smallest capture set (via <:<) that is a superset of both
    *  `this` and `that`
    */
@@ -98,20 +104,34 @@ sealed abstract class CaptureSet extends Showable:
 
   /** The largest capture set (via <:<) that is a subset of both `this` and `that`
    */
-  def intersect(that: CaptureSet)(using Context): CaptureSet =
+  def **(that: CaptureSet)(using Context): CaptureSet =
     if this.isConst && this.elems.forall(that.accountsFor) then this
     else if that.isConst && that.elems.forall(this.accountsFor) then that
-    else if this.isConst && that.isConst then Const(this.elems.intersect(that.elems))
-    else Var(this.elems.intersect(that.elems)).addSuper(this).addSuper(that)
+    else (this, that) match
+      case (cs1: Const, cs2: Const) => Const(cs1.elems.intersect(cs2.elems))
+      case (cs1: Var, cs2) => Intersected(cs1, cs2)
+      case (cs1, cs2: Var) => Intersected(cs2, cs1)
+
+  def -- (that: CaptureSet.Const)(using Context): CaptureSet =
+    val elems1 = elems.filter(!that.accountsFor(_))
+    if elems1.size == elems.size then this
+    else this match
+      case cs1: Const => Const(elems1)
+      case cs1: Var => Diff(cs1, that)
+
+  def filter(p: CaptureRef => Boolean)(using Context): CaptureSet = this match
+    case cs1: Const => Const(elems.filter(p))
+    case cs1: Var => Filtered(cs1, p)
 
   /** capture set obtained by applying `f` to all elements of the current capture set
    *  and joining the results. If the current capture set is a variable, the same
    *  transformation is applied to all future additions of new elements.
    */
   def flatMap(f: CaptureRef => CaptureSet)(using Context): CaptureSet =
-    mapRefs(elems, f) match
-      case cs: Const => cs
-      case cs: Var => Mapped(cs, f)
+    val mapped = mapRefs(elems, f)
+    this match
+      case cs: Const => mapped
+      case cs: Var => Mapped(cs, f, mapped)
 
   def substParams(tl: BindingType, to: List[Type])(using Context) =
     flatMap {
@@ -139,7 +159,7 @@ object CaptureSet:
 
   /** The universal capture set `{*}` */
   def universal(using Context): CaptureSet =
-    defn.captureRootType.typeRef.singletonCaptureSet
+    defn.captureRoot.termRef.singletonCaptureSet
 
   /** Used as a recursion brake */
   @sharable private[core] val Pending = Const(SimpleIdentitySet.empty)
@@ -153,13 +173,15 @@ object CaptureSet:
     def isConst = true
     def isEmpty: Boolean = elems.isEmpty
 
-    def addNewElems(elems: Refs)(using Context, VarState): Boolean = false
+    def addNewElems(elems: Refs)(using Context, VarState): CompareResult =
+      CompareResult.fail(this)
+
     def addSuper(cs: CaptureSet) = this
 
     override def toString = elems.toString
   end Const
 
-  class Var private[CaptureSet] (initialElems: Refs = emptySet, validate: Refs => Boolean = alwaysTrue) extends CaptureSet:
+  class Var(initialElems: Refs = emptySet) extends CaptureSet:
     val id =
       varId += 1
       varId
@@ -169,47 +191,113 @@ object CaptureSet:
     def isConst = false
     def isEmpty = false
 
-    assert(validate(elems))
+    private def recordElemsState()(using VarState): Boolean =
+      varState.getElems(this) match
+        case None => varState.putElems(this, elems)
+        case _ => true
 
-    private def recordState()(using VarState) = varState.get(this) match
-      case None => varState(this) = elems
-      case _ =>
+    private[CaptureSet] def recordDepsState()(using VarState): Boolean =
+      varState.getDeps(this) match
+        case None => varState.putDeps(this, deps)
+        case _ => true
+
+    def resetElems()(using state: VarState): Unit =
+      elems = state.elems(this)
 
-    def reset()(using state: VarState): Unit =
-      elems = state(this)
+    def resetDeps()(using state: VarState): Unit =
+      deps = state.deps(this)
 
-    def addNewElems(newElems: Refs)(using Context, VarState): Boolean =
-      validate(newElems)
-      && deps.forall(_.tryInclude(newElems))
-      && {
-        recordState()
+    def addNewElems(newElems: Refs)(using Context, VarState): CompareResult =
+      if recordElemsState() then
         elems ++= newElems
-        true
-      }
+        val depsIt = deps.iterator
+        while depsIt.hasNext do
+          val result = depsIt.next.tryInclude(newElems)
+          if result != CompareResult.OK then return result
+        CompareResult.OK
+      else
+        CompareResult.fail(this)
 
     def addSuper(cs: CaptureSet) = { deps += cs; this }
 
     override def toString = s"Var$id$elems"
   end Var
 
-  /** The set `Union { f(x) | x <- cv }` */
-  class Mapped private[CaptureSet] (cv: Var, f: CaptureRef => CaptureSet) extends Var(cv.elems):
+  /** A variable that changes when `cv` changes, where all additional new elements are mapped
+   *  using   ∪ { f(x) | x <- elems }
+   */
+  class Mapped private[CaptureSet] (cv: Var, f: CaptureRef => CaptureSet, initial: CaptureSet) extends Var(initial.elems):
     addSub(cv)
+    addSub(initial)
+
+    override def addNewElems(newElems: Refs)(using Context, VarState): CompareResult =
+      val added = mapRefs(newElems, f)
+      val result = super.addNewElems(added.elems)
+      if result == CompareResult.OK then
+        added match
+          case added: Var =>
+            added.recordDepsState()
+            addSub(added)
+          case _ =>
+      result
 
-    // ^^^ ???, seems wrong
-    override def accountsFor(x: CaptureRef)(using Context): Boolean =
-      f(x).elems.forall(super.accountsFor)
+    override def toString = s"Mapped$id($cv, elems = $elems)"
+  end Mapped
 
-    override def addNewElems(newElems: Refs)(using Context, VarState): Boolean =
-      super.addNewElems(mapRefs(newElems, f).elems)
+  /** A variable with elements given at any time as { x <- cv.elems | p(x) } */
+  class Filtered private[CaptureSet] (cv: Var, p: CaptureRef => Boolean)
+  extends Var(cv.elems.filter(p)):
+    addSub(cv)
 
-    override def toString = s"Mapped$id$elems"
-  end Mapped
+    override def addNewElems(newElems: Refs)(using Context, VarState): CompareResult =
+      super.addNewElems(newElems.filter(p))
+
+    override def toString = s"${getClass.getSimpleName}$id($cv, elems = $elems)"
+  end Filtered
+
+  /** A variable with elements given at any time as { x <- cv.elems | !other.accountsFor(x) } */
+  class Diff(cv: Var, other: Const)(using Context)
+  extends Filtered(cv, !other.accountsFor(_))
+
+  /** A variable with elements given at any time as { x <- cv.elems | other.accountsFor(x) } */
+  class Intersected(cv: Var, other: CaptureSet)(using Context)
+  extends Filtered(cv, other.accountsFor(_)):
+    addSub(other)
 
   def mapRefs(xs: Refs, f: CaptureRef => CaptureSet)(using Context): CaptureSet =
     (empty /: xs)((cs, x) => cs ++ f(x))
 
-  type VarState = util.EqHashMap[Var, Refs]
+  type CompareResult = CompareResult.Type
+
+  /** None = ok, Some(cs) = failure since not a subset of cs */
+  object CompareResult:
+    opaque type Type = CaptureSet
+    val OK: Type = Const(emptySet)
+    def fail(cs: CaptureSet): Type = cs
+    extension (result: Type) def blocking: CaptureSet = result
+
+  class VarState:
+    private val elemsMap: util.EqHashMap[Var, Refs] = new util.EqHashMap
+    private val depsMap: util.EqHashMap[Var, Deps] = new util.EqHashMap
+
+    def elems(v: Var): Refs = elemsMap(v)
+    def getElems(v: Var): Option[Refs] = elemsMap.get(v)
+    def putElems(v: Var, elems: Refs): Boolean = { elemsMap(v) = elems; true }
+
+    def deps(v: Var): Deps = depsMap(v)
+    def getDeps(v: Var): Option[Deps] = depsMap.get(v)
+    def putDeps(v: Var, deps: Deps): Boolean = { depsMap(v) = deps; true }
+
+    def abort(): Unit =
+      elemsMap.keysIterator.foreach(_.resetElems()(using this))
+      depsMap.keysIterator.foreach(_.resetDeps()(using this))
+  end VarState
+
+  @sharable
+  object FrozenState extends VarState:
+    override def putElems(v: Var, refs: Refs) = false
+    override def putDeps(v: Var, deps: Deps) = false
+    override def abort(): Unit = ()
 
   def varState(using state: VarState): VarState = state
 
@@ -233,11 +321,13 @@ object CaptureSet:
     css.foldLeft(empty)(_ ++ _)
 
   def ofType(tp: Type)(using Context): CaptureSet =
-    def recur(tp: Type): CaptureSet = tp match
-      case tp: NamedType =>
+    def recur(tp: Type): CaptureSet = tp.dealias match
+      case tp: TermRef =>
         tp.captureSet
-      case tp: ParamRef =>
+      case tp: TermParamRef =>
         tp.captureSet
+      case _: TypeRef | _: TypeParamRef =>
+        empty
       case CapturingType(parent, refs) =>
         recur(parent) ++ refs
       case AppliedType(tycon, args) =>
@@ -248,7 +338,7 @@ object CaptureSet:
       case tp: TypeProxy =>
         recur(tp.underlying)
       case AndType(tp1, tp2) =>
-        recur(tp1).intersect(recur(tp2))
+        recur(tp1) ** recur(tp2)
       case OrType(tp1, tp2) =>
         recur(tp1) ++ recur(tp2)
       case tp: ClassInfo =>
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index f8d71c26d7cd..dcf077906754 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -143,13 +143,13 @@ class Definitions {
   private def enterMethod(cls: ClassSymbol, name: TermName, info: Type, flags: FlagSet = EmptyFlags): TermSymbol =
     newMethod(cls, name, info, flags).entered
 
-  private def enterType(name: TypeName, info: Type, flags: FlagSet = EmptyFlags): TypeSymbol =
+  private def enterPermanentSymbol(name: Name, info: Type, flags: FlagSet = EmptyFlags): Symbol =
     val sym = newPermanentSymbol(ScalaPackageClass, name, flags, info)
     ScalaPackageClass.currentPackageDecls.enter(sym)
     sym
 
   private def enterAliasType(name: TypeName, tpe: Type, flags: FlagSet = EmptyFlags): TypeSymbol =
-    enterType(name, TypeAlias(tpe), flags)
+    enterPermanentSymbol(name, TypeAlias(tpe), flags).asType
 
   private def enterBinaryAlias(name: TypeName, op: (Type, Type) => Type): TypeSymbol =
     enterAliasType(name,
@@ -443,7 +443,8 @@ class Definitions {
 
   @tu lazy val andType: TypeSymbol = enterBinaryAlias(tpnme.AND, AndType(_, _))
   @tu lazy val orType: TypeSymbol = enterBinaryAlias(tpnme.OR, OrType(_, _, soft = false))
-  @tu lazy val captureRootType: TypeSymbol = enterType(tpnme.CAPTURE_ROOT, TypeBounds.empty, Deferred)
+  @tu lazy val captureRoot: TermSymbol = enterPermanentSymbol(nme.CAPTURE_ROOT, AnyType).asTerm
+  @tu lazy val captureRootAlias: TypeSymbol = enterAliasType(tpnme.CAPTURE_ROOT, captureRoot.termRef)
 
   /** Marker method to indicate an argument to a call-by-name parameter.
    *  Created by byNameClosures and elimByName, eliminated by Erasure,
@@ -1767,7 +1768,6 @@ class Definitions {
       AnyKindClass,
       andType,
       orType,
-      captureRootType,
       RepeatedParamClass,
       ByNameParamClass2x,
       AnyValClass,
@@ -1791,7 +1791,7 @@ class Definitions {
     this.initCtx = ctx
     if (!isInitialized) {
       // force initialization of every symbol that is synthesized or hijacked by the compiler
-      val forced = syntheticCoreClasses ++ syntheticCoreMethods ++ ScalaValueClasses() :+ JavaEnumClass
+      val forced = syntheticCoreClasses ++ syntheticCoreMethods ++ ScalaValueClasses() ++ List(JavaEnumClass, captureRoot, captureRootAlias)
 
       isInitialized = true
     }
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 723b2402331a..2282fc69883f 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -23,6 +23,7 @@ import typer.ProtoTypes.constrained
 import typer.Applications.productSelectorTypes
 import reporting.trace
 import NullOpsDecorator._
+import CaptureSet.CompareResult as CaptCompareResult
 import annotation.constructorOnly
 
 /** Provides methods to compare types.
@@ -490,7 +491,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             // under -Ycheck. Test case is i7965.scala.
 
       case tp1: CapturingType =>
-        if tp1.refs <:< tp2.captureSet then recur(tp1.parent, tp2)
+        if tp1.refs <:< tp2.captureSet == CaptCompareResult.OK then recur(tp1.parent, tp2)
         else thirdTry
       case tp1: MatchType =>
         val reduced = tp1.reduced
@@ -2369,7 +2370,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     case tp1: AnnotatedType if !tp1.isRefining =>
       tp1.underlying & tp2
     case tp1: CapturingType =>
-      if tp2.captureSet <:< tp1.refs then tp1.parent & tp2
+      if tp2.captureSet <:< tp1.refs == CaptCompareResult.OK then tp1.parent & tp2
       else tp1.derivedCapturingType(tp1.parent & tp2, tp1.refs)
     case _ =>
       NoType
diff --git a/compiler/src/dotty/tools/dotc/core/TypeErrors.scala b/compiler/src/dotty/tools/dotc/core/TypeErrors.scala
index 950963497fbc..38366e5c0c93 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeErrors.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeErrors.scala
@@ -73,6 +73,7 @@ class RecursionOverflow(val op: String, details: => String, val previous: Throwa
     s"""Recursion limit exceeded.
        |Maybe there is an illegal cyclic reference?
        |If that's not the case, you could also try to increase the stacksize using the -Xss JVM option.
+       |For the unprocessed stack trace, compile with -Yno-decode-stacktraces.
        |A recurring operation is (inner to outer):
        |${opsString(mostCommon)}""".stripMargin
   }
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index ed0f710028df..a9b2a56ddf8e 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -19,6 +19,7 @@ import typer.ForceDegree
 import typer.Inferencing._
 import typer.IfBottom
 import reporting.TestingReporter
+import CaptureSet.CompareResult
 
 import scala.annotation.internal.sharable
 import scala.annotation.threadUnsafe
@@ -169,7 +170,7 @@ object TypeOps:
         val normed = tp.tryNormalize
         if (normed.exists) normed else mapOver
       case tp: CapturingType
-      if !ctx.mode.is(Mode.Type) && tp.refs <:< tp.parent.captureSet =>
+      if !ctx.mode.is(Mode.Type) && tp.refs <:< tp.parent.captureSet == CompareResult.OK =>
         simplify(tp.parent, theMap)
       case tp: MethodicType =>
         tp // See documentation of `Types#simplified`
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index e0e98096b5e5..440359715078 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -38,6 +38,7 @@ import scala.util.hashing.{ MurmurHash3 => hashing }
 import config.Printers.{core, typr, matchTypes}
 import reporting.{trace, Message}
 import java.lang.ref.WeakReference
+import CaptureSet.CompareResult
 
 import scala.annotation.internal.sharable
 import scala.annotation.threadUnsafe
@@ -1846,7 +1847,10 @@ object Types {
       if captureSet.accountsFor(ref) then this else CapturingType(this, ref.singletonCaptureSet)
 
     def capturing(cs: CaptureSet)(using Context): Type =
-      (this /: cs.elems)(_.capturing(_))
+      if cs.isConst && (cs frozen_<:< captureSet) == CompareResult.OK then this
+      else this match
+        case CapturingType(parent, cs1) => parent.capturing(cs1 ++ cs)
+        case _ => CapturingType(this, cs)
 
     /** The set of distinct symbols referred to by this type, after all aliases are expanded */
     def coveringSet(using Context): Set[Symbol] =
@@ -2029,7 +2033,7 @@ object Types {
   }
 
   /** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs */
-  trait CaptureRef extends TypeProxy, ValueType:
+  trait CaptureRef extends SingletonType:
     private var myCaptureSet: CaptureSet = _
     private var myCaptureSetRunId: Int = NoRunId
     private var mySingletonCaptureSet: CaptureSet = null
@@ -2111,7 +2115,7 @@ object Types {
 
 // --- NamedTypes ------------------------------------------------------------------
 
-  abstract class NamedType extends CachedProxyType, CaptureRef { self =>
+  abstract class NamedType extends CachedProxyType, ValueType { self =>
 
     type ThisType >: this.type <: NamedType
     type ThisName <: Name
@@ -2388,23 +2392,6 @@ object Types {
       checkDenot()
     }
 
-    /** A reference can be tracked if it is
-     *   (1) a local term ref
-     *   (2) a type parameter,
-     *   (3) a method term parameter
-     *  References to term parameters of classes cannot be tracked individually.
-     *  They are subsumed in the capture sets of the enclosing class.
-     */
-    def canBeTracked(using Context) =
-      if isTerm then (prefix eq NoPrefix) || symbol.hasAnnotation(defn.AbilityAnnot)
-      else symbol.is(TypeParam) || isRootCapability
-
-    override def isRootCapability(using Context): Boolean =
-      name == tpnme.CAPTURE_ROOT && symbol == defn.captureRootType
-
-    override def normalizedRef(using Context): CaptureRef =
-      if canBeTracked then symbol.namedType else this
-
     private def checkDenot()(using Context) = {}
 
     private def checkSymAssign(sym: Symbol)(using Context) = {
@@ -2682,7 +2669,7 @@ object Types {
    */
   abstract case class TermRef(override val prefix: Type,
                               private var myDesignator: Designator)
-    extends NamedType with SingletonType with ImplicitRef {
+    extends NamedType, ImplicitRef, CaptureRef {
 
     type ThisType = TermRef
     type ThisName = TermName
@@ -2706,6 +2693,19 @@ object Types {
 
     def implicitName(using Context): TermName = name
     def underlyingRef: TermRef = this
+
+    /** A term reference can be tracked if it is a local term ref or a method term parameter.
+     *  References to term parameters of classes cannot be tracked individually.
+     *  They are subsumed in the capture sets of the enclosing class.
+     */
+    def canBeTracked(using Context) =
+      (prefix eq NoPrefix) || symbol.hasAnnotation(defn.AbilityAnnot) || isRootCapability
+
+    override def isRootCapability(using Context): Boolean =
+      name == nme.CAPTURE_ROOT && symbol == defn.captureRoot
+
+    override def normalizedRef(using Context): CaptureRef =
+      if canBeTracked then symbol.termRef else this
   }
 
   abstract case class TypeRef(override val prefix: Type,
@@ -2841,7 +2841,7 @@ object Types {
    *  Note: we do not pass a class symbol directly, because symbols
    *  do not survive runs whereas typerefs do.
    */
-  abstract case class ThisType(tref: TypeRef) extends CachedProxyType, SingletonType, CaptureRef {
+  abstract case class ThisType(tref: TypeRef) extends CachedProxyType, CaptureRef {
     def cls(using Context): ClassSymbol = tref.stableInRunSymbol match {
       case cls: ClassSymbol => cls
       case _ if ctx.mode.is(Mode.Interactive) => defn.AnyClass // was observed to happen in IDE mode
@@ -4419,7 +4419,7 @@ object Types {
     override def hashIsStable: Boolean = false
   }
 
-  abstract class ParamRef extends BoundType, CaptureRef {
+  abstract class ParamRef extends BoundType {
     type BT <: LambdaType
     def paramNum: Int
     def paramName: binder.ThisName = binder.paramNames(paramNum)
@@ -4430,8 +4430,6 @@ object Types {
       else infos(paramNum)
     }
 
-    override def canBeTracked(using Context) = true
-
     override def computeHash(bs: Binders): Int = doHash(paramNum, binder.identityHash(bs))
 
     override def equals(that: Any): Boolean = equals(that, null)
@@ -4453,8 +4451,9 @@ object Types {
   /** Only created in `binder.paramRefs`. Use `binder.paramRefs(paramNum)` to
    *  refer to `TermParamRef(binder, paramNum)`.
    */
-  abstract case class TermParamRef(binder: TermLambda, paramNum: Int) extends ParamRef with SingletonType {
+  abstract case class TermParamRef(binder: TermLambda, paramNum: Int) extends ParamRef, CaptureRef {
     type BT = TermLambda
+    override def canBeTracked(using Context) = true
     def kindString: String = "Term"
     def copyBoundType(bt: BT): Type = bt.paramRefs(paramNum)
   }
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 7ed97a65c2e4..c23b79e561a2 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -188,7 +188,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
           (" <: " ~ toText(bound) provided !bound.isAny)
         }.close
       case CapturingType(parent, refs) =>
-        changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toText(refs.toRetainsTypeArg))
+        if refs.isConst then
+          changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toText(refs.toRetainsTypeArg))
+        else
+          s"$refs " ~ toText(parent) // ^^^ improve
       case tp: PreviousErrorType if ctx.settings.XprintTypes.value =>
         "<error>" // do not print previously reported error message because they may try to print this error type again recuresevely
       case tp: ErrorType =>
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 76f89cb65757..224d25fb11b5 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -58,7 +58,7 @@ abstract class Recheck extends Phase, IdentityDenotTransformer:
 
     def reinferResult(info: Type)(using Context): Type = info match
       case info: MethodOrPoly =>
-        info.derivedLambdaType(resType = reinferResult(info.resultType))
+        info.derivedLambdaType(resType = reinferResult(info.resType))
       case _ =>
         reinfer(info)
 
@@ -317,7 +317,6 @@ abstract class Recheck extends Phase, IdentityDenotTransformer:
           || expected.isRepeatedParam
              && actual <:< expected.translateFromRepeated(toArray = tree.tpe.isRef(defn.ArrayClass))
         if !isCompatible then
-          println(i"err at ${ctx.phase}")
           err.typeMismatch(tree.withType(tpe), pt)
 
     def checkUnit(unit: CompilationUnit)(using Context): Unit =
diff --git a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
index 141e17207167..d34ddaad389e 100644
--- a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
@@ -11,24 +11,65 @@ import StdNames._
 import Decorators._
 import ProtoTypes._
 import Inferencing.isFullyDefined
-import config.Printers.capt
+import config.Printers.{capt, recheckr}
 import ast.{tpd, untpd, Trees}
 import NameKinds.{DocArtifactName, OuterSelectName, DefaultGetterName}
 import Trees._
 import scala.util.control.NonFatal
 import typer.ErrorReporting._
 import util.Spans.Span
-import util.{SimpleIdentitySet, SrcPos}
+import util.{SimpleIdentitySet, EqHashMap, SrcPos}
 import util.Chars.*
 import Nullables._
 import transform.*
+import transform.SymUtils.*
 import scala.collection.mutable
 import reporting._
 import ProtoTypes._
 import dotty.tools.backend.jvm.DottyBackendInterface.symExtensions
+import CaptureSet.CompareResult
+
+object CheckCaptures:
+  case class Env(owner: Symbol, captured: CaptureSet, isBoxed: Boolean, outer: Env):
+    def isOpen = !captured.isEmpty && !isBoxed
+
+  extension (tp: Type)
+
+    /** If this is  type variable instantiated or upper bounded with a capturing type,
+     *  the capture set associated with that type. Extended to and-or types and
+     *  type proxies in the obvious way. If a term has a type with a boxed captureset,
+     *  that captureset counts towards the capture variables of the envirionment.
+     */
+    def boxedCaptured(using Context): CaptureSet =
+      def getBoxed(tp: Type, enabled: Boolean): CaptureSet = tp match
+        case tp: CapturingType if enabled => tp.refs
+        case tp: TypeVar => getBoxed(tp.underlying, enabled = true)
+        case tp: TypeProxy => getBoxed(tp.superType, enabled)
+        case tp: AndType => getBoxed(tp.tp1, enabled) ++ getBoxed(tp.tp2, enabled)
+        case tp: OrType => getBoxed(tp.tp1, enabled) ** getBoxed(tp.tp2, enabled)
+        case _ => CaptureSet.empty
+      getBoxed(tp, enabled = false)
+
+    /** If this type appears as an expected type of a term, does it imply
+     *  that the term should be boxed?
+     */
+    def needsBox(using Context): Boolean = tp match
+      case _: TypeVar => true
+      case tp: TypeRef =>
+        tp.info match
+          case TypeBounds(lo, _) => lo.needsBox
+          case _ => false
+      case tp: RefinedOrRecType => tp.parent.needsBox
+      case tp: AnnotatedType => tp.parent.needsBox
+      case tp: LazyRef => tp.ref.needsBox
+      case tp: AndType => tp.tp1.needsBox || tp.tp2.needsBox
+      case tp: OrType => tp.tp1.needsBox && tp.tp2.needsBox
+      case _ => false
+  end extension
 
 class CheckCaptures extends Recheck:
   import ast.tpd.*
+  import CheckCaptures.*
 
   def phaseName: String = "cc"
   override def isEnabled(using Context) = ctx.settings.Ycc.value
@@ -38,100 +79,124 @@ class CheckCaptures extends Recheck:
   class CaptureChecker(ictx: Context) extends Rechecker(ictx):
     import ast.tpd.*
 
-    private var myDeps: Dependencies = null
-
-    def deps(using Context): Dependencies =
-      if myDeps == null then
-        myDeps = new Dependencies(ctx.compilationUnit.tpdTree, ctx):
-          def isExpr(sym: Symbol)(using Context): Boolean =
-            sym.isRealClass || sym.isOneOf(MethodOrLazy)
-          def enclosure(using Context) =
-            def recur(owner: Symbol): Symbol =
-              if isExpr(owner) || !owner.exists then owner else recur(owner.owner)
-            recur(ctx.owner)
-      myDeps
-
-    private def capturedVars(sym: Symbol)(using Context): CaptureSet =
-      CaptureSet(deps.freeVars(sym).toList.map(_.termRef).filter(_.isTracked)*)
-
-/*
-
-    override def typedClosure(tree: untpd.Closure, pt: Type)(using Context): Tree =
-      super.typedClosure(tree, pt) match
-        case tree1: Closure =>
-          refinr.println(i"typing closure ${tree1.meth.symbol} with fvs ${capturedVars(tree1.meth.symbol)}")
-          tree1.withType(tree1.tpe.capturing(capturedVars(tree1.meth.symbol)))
-        case tree1 => tree1
-
-    override def typedApply(tree: untpd.Apply, pt: Type)(using Context): Tree =
-      super.typedApply(tree, pt) match
-        case tree1 @ Apply(fn, args) =>
-          if tree.fun.symbol.isConstructor then
-            //println(i"typing $tree1, ${capturedVars(tree1.tpe.classSymbol)}")
-            tree1.withType(tree1.tpe.capturing(capturedVars(tree1.tpe.classSymbol)))
-          else
-            tree1
-        case tree1 => tree1
-
-*/
+    override def reinfer(tp: Type)(using Context): Type =
+      CapturingType(tp, CaptureSet.Var())
+
+    private var curEnv: Env = Env(NoSymbol, CaptureSet.empty, false, null)
+
+    private val myCapturedVars: util.EqHashMap[Symbol, CaptureSet] = EqHashMap()
+    def capturedVars(sym: Symbol)(using Context) =
+      myCapturedVars.getOrElseUpdate(sym,
+        if sym.ownersIterator.exists(_.isTerm) then CaptureSet.Var()
+        else CaptureSet.empty)
+
+    def markFree(sym: Symbol, pos: SrcPos)(using Context): Unit =
+      if sym.exists then
+        val ref = sym.termRef
+        def recur(env: Env): Unit =
+          if env.isOpen && env.owner != sym.enclosure then
+            checkElem(ref, env.captured, pos)
+            recur(env.outer)
+        if ref.isTracked then recur(curEnv)
+
+    def assertSub(cs1: CaptureSet, cs2: CaptureSet)(using Context) =
+      assert((cs1 <:< cs2) == CompareResult.OK, i"$cs1 is not a subset of $cs2")
+
+    def checkElem(elem: CaptureRef, cs: CaptureSet, pos: SrcPos)(using Context) =
+      val res = elem.singletonCaptureSet <:< cs
+      if res != CompareResult.OK then
+        report.error(i"$elem cannot be referenced here; it is not included in allowed capture set ${res.blocking}", pos)
+
+    def checkSubset(cs1: CaptureSet, cs2: CaptureSet, pos: SrcPos)(using Context) =
+      val res = cs1 <:< cs2
+      if res != CompareResult.OK then
+        report.error(i"references $cs1 are not all included in allowed capture set ${res.blocking}", pos)
+
+    override def recheckClosure(tree: Closure, pt: Type)(using Context): Type =
+      val cs = capturedVars(tree.meth.symbol)
+      recheckr.println(i"typing closure $tree with cvs $cs")
+      super.recheckClosure(tree, pt).capturing(cs)
+        .showing(i"rechecked $tree, $result", capt)
+
+    override def recheckIdent(tree: Ident)(using Context): Type =
+      markFree(tree.symbol, tree.srcPos)
+      super.recheckIdent(tree)
+
+    override def recheckDefDef(tree: DefDef, sym: Symbol)(using Context): Type =
+      val saved = curEnv
+      val localSet = capturedVars(sym)
+      if !localSet.isEmpty then curEnv = Env(sym, localSet, false, curEnv)
+      try super.recheckDefDef(tree, sym)
+      finally curEnv = saved
+
+    override def recheckClassDef(tree: TypeDef, impl: Template, sym: ClassSymbol)(using Context): Type =
+      val saved = curEnv
+      val localSet = capturedVars(sym)
+      if !localSet.isEmpty then curEnv = Env(sym, localSet, false, curEnv)
+      try super.recheckClassDef(tree, impl, sym)
+      finally curEnv = saved
+
+    override def recheckApply(tree: Apply, pt: Type)(using Context): Type =
+      if curEnv.isOpen then
+        val ownEnclosure = ctx.owner.enclosingMethodOrClass
+        var targetSet = capturedVars(tree.symbol)
+        if !targetSet.isEmpty && tree.symbol.enclosure == ownEnclosure then
+          targetSet = targetSet.filter {
+            case ref: TermRef => ref.symbol.enclosure != ownEnclosure
+            case _ => true
+          }
+
+        checkSubset(targetSet, curEnv.captured, tree.srcPos)
+      val sym = tree.symbol
+      val cs = if sym.isConstructor then capturedVars(sym.owner) else CaptureSet.empty
+      super.recheckApply(tree, pt).capturing(cs)
+
+    override def recheck(tree: Tree, pt: Type = WildcardType)(using Context): Type =
+      val saved = curEnv
+      if pt.needsBox && !curEnv.isBoxed then
+        curEnv = Env(NoSymbol, CaptureSet.Var(), true, curEnv)
+      try
+        val res = super.recheck(tree, pt)
+        if curEnv.isOpen then assertSub(res.boxedCaptured, curEnv.captured)
+        res
+      finally curEnv = saved
+
+    override def checkUnit(unit: CompilationUnit)(using Context): Unit =
+      super.checkUnit(unit)
+      PostRefinerCheck.traverse(unit.tpdTree)
 
   end CaptureChecker
 
   inline val disallowGlobal = true
 
-  // ^^^ todo: drop wf condition; work into parameter substitution
-  def checkWellFormed(whole: Type, pos: SrcPos)(using Context): Unit =
-    def checkRelativeVariance(mt: MethodType) = new TypeTraverser:
-      def traverse(tp: Type): Unit = tp match
-        case CapturingType(parent, refs) =>
-          for ref <- refs.elems do
-            ref match
-              case TermParamRef(`mt`, _) =>
-                if variance <= 0 then
-                  val direction = if variance < 0 then "contra" else "in"
-                  report.error(em"captured reference $ref appears ${direction}variantly in type $whole", pos)
-              case _ =>
-          traverse(parent)
-        case _ =>
-          traverseChildren(tp)
-    val checkVariance = new TypeTraverser:
-      def traverse(tp: Type): Unit = tp match
-        case mt: MethodType if mt.isResultDependent =>
-          checkRelativeVariance(mt).traverse(mt)
+  def checkNotGlobal(tree: Tree, allArgs: Tree*)(using Context): Unit =
+    if disallowGlobal then
+      //println(i"checking $arg in $tree: ${arg.tpe.captureSet}")
+      tree match
+        case LambdaTypeTree(_, restpt) =>
+          checkNotGlobal(restpt, allArgs*)
         case _ =>
-          traverseChildren(tp)
-    checkVariance.traverse(whole)
+          for ref <- tree.tpe.captureSet.elems do
+            val isGlobal = ref match
+              case ref: TypeRef => ref.isRootCapability
+              case ref: TermRef => ref.prefix != NoPrefix && ref.symbol.hasAnnotation(defn.AbilityAnnot)
+              case _ => false
+            val what = if ref.isRootCapability then "universal" else "global"
+            if isGlobal then
+              val notAllowed = i" is not allowed to capture the $what capability $ref"
+              def msg = tree match
+                case tree: InferredTypeTree =>
+                  i"""inferred type argument ${tree.tpe}$notAllowed
+                      |
+                      |The inferred arguments are: [$allArgs%, %]"""
+                case _ => s"type argument$notAllowed"
+              report.error(msg, tree.srcPos)
 
   object PostRefinerCheck extends TreeTraverser:
     def traverse(tree: Tree)(using Context) =
       tree match
         case tree1 @ TypeApply(fn, args) if disallowGlobal =>
-          for arg <- args do
-            //println(i"checking $arg in $tree: ${arg.tpe.captureSet}")
-            for ref <- arg.tpe.captureSet.elems do
-              val isGlobal = ref match
-                case ref: TypeRef => ref.isRootCapability
-                case ref: TermRef => ref.prefix != NoPrefix && ref.symbol.hasAnnotation(defn.AbilityAnnot)
-                case _ => false
-              val what = if ref.isRootCapability then "universal" else "global"
-              if isGlobal then
-                val notAllowed = i" is not allowed to capture the $what capability $ref"
-                def msg = arg match
-                  case arg: InferredTypeTree =>
-                    i"""inferred type argument ${arg.tpe}$notAllowed
-                       |
-                       |The inferred arguments are: [$args%, %]"""
-                  case _ => s"type argument$notAllowed"
-                report.error(msg, arg.srcPos)
-        case tree: TypeTree =>
-          // it's inferred, no need to check
-        case _: TypTree | _: Closure =>
-          checkWellFormed(tree.tpe, tree.srcPos)
-        case tree: DefDef =>
-          def check(tp: Type): Unit = tp match
-            case tp: MethodOrPoly => check(tp.resType)
-            case _ =>
-          check(tree.symbol.info)
+          for arg <- args do checkNotGlobal(arg, args*)
         case _ =>
       traverseChildren(tree)
 
diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
index 95724f2f4ece..d709b52f30b2 100644
--- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -192,7 +192,7 @@ trait TypeAssigner {
     else errorType(ex"$whatCanNot be accessed as a member of $pre$where.$whyNot", pos)
 
   def processAppliedType(tree: untpd.Tree, tp: Type)(using Context): Type =
-    def include(cs: CaptureSet, tp: Type): CaptureSet = tp match
+    def include(cs: CaptureSet, tp: Type): CaptureSet = tp.dealias match
       case ref: CaptureRef =>
         if ref.isTracked then
           if cs.accountsFor(ref) then
diff --git a/tests/pos-custom-args/captures/boxmap.scala b/tests/pos-custom-args/captures/boxmap.scala
index 50a84e5c6ae5..c229a7b26c26 100644
--- a/tests/pos-custom-args/captures/boxmap.scala
+++ b/tests/pos-custom-args/captures/boxmap.scala
@@ -1,9 +1,8 @@
 type Top = Any retains *
-class Cap extends Retains[*]
 
 infix type ==> [A, B] = (A => B) retains *
 
-type Box[+T <: Top] = ([K <: Top] => (T ==> K) => K) retains T
+type Box[+T <: Top] = ([K <: Top] => (T ==> K) => K)
 
 def box[T <: Top](x: T): Box[T] =
   [K <: Top] => (k: T ==> K) => k(x)
@@ -11,11 +10,11 @@ def box[T <: Top](x: T): Box[T] =
 def map[A <: Top, B <: Top](b: Box[A])(f: A ==> B): Box[B] =
   b[Box[B]]((x: A) => box(f(x)))
 
-def lazymap[A <: Top, B <: Top](b: Box[A])(f: A ==> B): (() => Box[B]) retains b.type | f.type =
+def lazymap[A <: Top, B <: Top](b: Box[A])(f: A ==> B): (() => Box[B]) retains f.type =
   () => b[Box[B]]((x: A) => box(f(x)))
 
 def test[A <: Top, B <: Top] =
   def lazymap[A <: Top, B <: Top](b: Box[A])(f: A ==> B) =
     () => b[Box[B]]((x: A) => box(f(x)))
-  val x: (b: Box[A]) => ((f: A ==> B) => (() => Box[B]) retains b.type | f.type) retains b.type = lazymap[A, B]
+  val x: (b: Box[A]) => (f: A ==> B) => (() => Box[B]) retains f.type = lazymap[A, B]
   ()

From a76b035fcb1cf61fd3abe5ed2b08fdb73f59654b Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 15 Aug 2021 16:51:18 +0200
Subject: [PATCH 12/25] Print capturing types as in paper

# Conflicts:
#	compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
#	tests/neg-custom-args/captures/boxmap.check
#	tests/neg-custom-args/captures/try.check
#	tests/neg-custom-args/captures/try2.check
---
 compiler/src/dotty/tools/dotc/config/Config.scala      |  2 ++
 .../src/dotty/tools/dotc/printing/PlainPrinter.scala   |  6 +++++-
 tests/neg-custom-args/captures/boxmap.check            |  4 ++--
 tests/neg-custom-args/captures/capt1.check             | 10 +++++-----
 tests/neg-custom-args/captures/try.check               |  2 +-
 tests/neg-custom-args/captures/try2.check              |  2 +-
 6 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala
index ac1708378e73..6ca09e9f8f7a 100644
--- a/compiler/src/dotty/tools/dotc/config/Config.scala
+++ b/compiler/src/dotty/tools/dotc/config/Config.scala
@@ -227,4 +227,6 @@ object Config {
    *  reduces the number of allocated denotations by ~50%.
    */
   inline val reuseSymDenotations = true
+
+  inline val printCaptureSetsAsPrefix = true
 }
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index c23b79e561a2..b5b2bbc2e05f 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -15,6 +15,7 @@ import util.SourcePosition
 import java.lang.Integer.toOctalString
 import scala.util.control.NonFatal
 import scala.annotation.switch
+import config.Config
 
 class PlainPrinter(_ctx: Context) extends Printer {
   /** The context of all public methods in Printer and subclasses.
@@ -189,7 +190,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
         }.close
       case CapturingType(parent, refs) =>
         if refs.isConst then
-          changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toText(refs.toRetainsTypeArg))
+          if Config.printCaptureSetsAsPrefix then
+            changePrec(GlobalPrec)("{" ~ toTextCaptureRef(ref) ~ "} " ~ toText(parent))
+          else
+            changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toTextCaptureRef(ref))
         else
           s"$refs " ~ toText(parent) // ^^^ improve
       case tp: PreviousErrorType if ctx.settings.XprintTypes.value =>
diff --git a/tests/neg-custom-args/captures/boxmap.check b/tests/neg-custom-args/captures/boxmap.check
index bbf1879464de..da1c38b4a887 100644
--- a/tests/neg-custom-args/captures/boxmap.check
+++ b/tests/neg-custom-args/captures/boxmap.check
@@ -1,8 +1,8 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boxmap.scala:15:2 ----------------------------------------
 15 |  () => b[Box[B]]((x: A) => box(f(x)))  // error
    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |  Found:    (() => Box[B]) retains b retains f
-   |  Required: () => Box[B]
+   |  Found:    {f} {b} () => Box[B]
+   |  Required: {B} () => Box[B]
    |
    |  where:    B is a type in method lazymap with bounds <: Top
 
diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check
index 15ba35a52e91..f143f930e8f2 100644
--- a/tests/neg-custom-args/captures/capt1.check
+++ b/tests/neg-custom-args/captures/capt1.check
@@ -1,35 +1,35 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:3:2 ------------------------------------------
 3 |  () => if x == null then y else y  // error
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  |  Found:    (() => C) retains x
+  |  Found:    {x} () => C
   |  Required: () => C
 
 longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:6:2 ------------------------------------------
 6 |  () => if x == null then y else y  // error
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  |  Found:    (() => C) retains x
+  |  Found:    {x} () => C
   |  Required: Any
 
 longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:14:2 -----------------------------------------
 14 |  f  // error
    |  ^
-   |  Found:    (Int => Int) retains x
+   |  Found:    {x} Int => Int
    |  Required: Any
 
 longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:23:3 -----------------------------------------
 23 |  F(22)  // error
    |  ^^^^^
-   |  Found:    F retains x
+   |  Found:    {x} F
    |  Required: A
 
 longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:27:40 ----------------------------------------
 27 |    def m() = if x == null then y else y  // error
    |                                        ^
-   |                                        Found:    A {...} retains x
+   |                                        Found:    {x} A {...}
    |                                        Required: A
 
 longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index 2a28933971c7..22d761642d05 100644
--- a/tests/neg-custom-args/captures/try.check
+++ b/tests/neg-custom-args/captures/try.check
@@ -1,7 +1,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:32 ------------------------------------------
 29 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)  // error
    |                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                                Found:    (() => Nothing) retains x
+   |                                Found:    {x} () => Nothing
    |                                Required: () => Nothing
 
 longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/try2.check b/tests/neg-custom-args/captures/try2.check
index a73ee901406d..c7b20d0f7c5e 100644
--- a/tests/neg-custom-args/captures/try2.check
+++ b/tests/neg-custom-args/captures/try2.check
@@ -1,7 +1,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try2.scala:31:32 -----------------------------------------
 31 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)  // error
    |                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                                Found:    (() => Nothing) retains x
+   |                                Found:    {x} () => Nothing
    |                                Required: () => Nothing
 
 longer explanation available when compiling with `-explain`

From 21e1ae6e7bd538559bd668cf90d694517c9a0d04 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 15 Aug 2021 17:25:43 +0200
Subject: [PATCH 13/25] Allow paper syntax to parse capturing types

# Conflicts:
#	compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
#	compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
#	compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
#	tests/pos-custom-args/captures/boxmap.scala
#	tests/pos-custom-args/captures/cc-expand.scala
---
 .../dotty/tools/dotc/core/Definitions.scala   |  1 +
 .../src/dotty/tools/dotc/core/StdNames.scala  |  1 +
 .../tools/dotc/core/tasty/TreeUnpickler.scala |  3 +-
 .../dotty/tools/dotc/parsing/Parsers.scala    | 37 ++++++++++++++++++-
 .../src/dotty/tools/dotc/parsing/Tokens.scala |  4 +-
 .../tools/dotc/printing/PlainPrinter.scala    |  8 ++--
 .../tools/dotc/printing/RefinedPrinter.scala  |  4 ++
 .../dotty/tools/dotc/typer/TypeAssigner.scala |  4 ++
 .../scala/runtime/stdLibPatches/Predef.scala  |  2 +
 .../pos-custom-args/captures/cc-expand.scala  | 21 +++++++++++
 10 files changed, 76 insertions(+), 9 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/cc-expand.scala

diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index dcf077906754..707c3f6f7e49 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -476,6 +476,7 @@ class Definitions {
     @tu lazy val Predef_identity : Symbol = ScalaPredefModule.requiredMethod(nme.identity)
     @tu lazy val Predef_undefined: Symbol = ScalaPredefModule.requiredMethod(nme.???)
     @tu lazy val Predef_retainsType: Symbol = ScalaPredefModule.requiredType(tpnme.retains)
+    @tu lazy val Predef_capturing: Symbol = ScalaPredefModule.requiredType(tpnme.CAPTURING)
   @tu lazy val ScalaPredefModuleClass: ClassSymbol = ScalaPredefModule.moduleClass.asClass
 
   @tu lazy val SubTypeClass: ClassSymbol = requiredClass("scala.<:<")
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index b90407b3de8e..cba3486dac9e 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -119,6 +119,7 @@ object StdNames {
     val BITMAP_TRANSIENT: N           = s"${BITMAP_PREFIX}trans$$"    // initialization bitmap for transient lazy vals
     val BITMAP_CHECKINIT: N           = s"${BITMAP_PREFIX}init$$"      // initialization bitmap for checkinit values
     val BITMAP_CHECKINIT_TRANSIENT: N = s"${BITMAP_PREFIX}inittrans$$" // initialization bitmap for transient checkinit values
+    val CAPTURING                     = "|>"
     val DEFAULT_GETTER: N             = str.DEFAULT_GETTER
     val DEFAULT_GETTER_INIT: N        = "$lessinit$greater"
     val DO_WHILE_PREFIX: N            = "doWhile$"
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
index 66a3be79fd23..5749221e3925 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
@@ -361,7 +361,8 @@ class TreeUnpickler(reader: TastyReader,
               val args = until(end)(readType())
               tycon match
                 case tycon: TypeRef if tycon.symbol == defn.Predef_retainsType =>
-                  CapturingType(args(0), CaptureSet.fromRetainsTypeArg(args(1)))
+                  if ctx.settings.Ycc.value then CapturingType(args(0), CaptureSet.fromRetainsTypeArg(args(1)))
+                  else args(0)
                 case _ =>
                   tycon.appliedTo(args)
             case TYPEBOUNDS =>
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 399eabfff0f1..f652693a5b58 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -890,6 +890,24 @@ object Parsers {
            }
       }
 
+    def followingIsCaptureSet(): Boolean =
+      val lookahead = in.LookaheadScanner()
+      def recur(): Boolean =
+        lookahead.isIdent && {
+          lookahead.nextToken()
+          if lookahead.token == COMMA then
+            lookahead.nextToken()
+            recur()
+          else
+            lookahead.token == RBRACE && {
+              lookahead.nextToken()
+              canStartInfixTypeTokens.contains(lookahead.token)
+              || lookahead.token == LBRACKET
+            }
+        }
+      lookahead.nextToken()
+      recur()
+
   /* --------- OPERAND/OPERATOR STACK --------------------------------------- */
 
     var opStack: List[OpInfo] = Nil
@@ -1329,17 +1347,27 @@ object Parsers {
       case _ => false
     }
 
+    def captureRef(): Tree =
+      atSpan(in.offset) {
+        val name = ident()
+        if name.isVarPattern then SingletonTypeTree(Ident(name))
+        else Ident(name.toTypeName)
+      }
+
     /** Type           ::=  FunType
      *                   |  HkTypeParamClause ‘=>>’ Type
      *                   |  FunParamClause ‘=>>’ Type
      *                   |  MatchType
      *                   |  InfixType
+     *                   |  CaptureSet Type
      *  FunType        ::=  (MonoFunType | PolyFunType)
      *  MonoFunType    ::=  FunTypeArgs (‘=>’ | ‘?=>’) Type
      *  PolyFunType    ::=  HKTypeParamClause '=>' Type
      *  FunTypeArgs    ::=  InfixType
      *                   |  `(' [ [ ‘[using]’ ‘['erased']  FunArgType {`,' FunArgType } ] `)'
      *                   |  '(' [ ‘[using]’ ‘['erased'] TypedFunParam {',' TypedFunParam } ')'
+     *  CaptureSet     ::=  `{` CaptureRef {`,` CaptureRef} `}`
+     *  CaptureRef     ::=  Ident
      */
     def typ(): Tree = {
       val start = in.offset
@@ -1445,6 +1473,11 @@ object Parsers {
           }
           else { accept(TLARROW); typ() }
         }
+        else if in.token == LBRACE && followingIsCaptureSet() then
+          val refs = inBraces { commaSeparated(captureRef) }
+          val t = typ()
+          val captured = refs.reduce(InfixOp(_, Ident(tpnme.raw.BAR), _))
+          AppliedTypeTree(TypeTree(defn.Predef_capturing.typeRef), captured :: t :: Nil)
         else if (in.token == INDENT) enclosed(INDENT, typ())
         else infixType()
 
@@ -1513,7 +1546,7 @@ object Parsers {
     def infixType(): Tree = infixTypeRest(refinedType())
 
     def infixTypeRest(t: Tree): Tree =
-      infixOps(t, canStartTypeTokens, refinedTypeFn, Location.ElseWhere,
+      infixOps(t, canStartInfixTypeTokens, refinedTypeFn, Location.ElseWhere,
         isType = true,
         isOperator = !followingIsVararg())
 
@@ -3154,7 +3187,7 @@ object Parsers {
         ImportSelector(
           atSpan(in.skipToken()) { Ident(nme.EMPTY) },
           bound =
-            if canStartTypeTokens.contains(in.token) then rejectWildcardType(infixType())
+            if canStartInfixTypeTokens.contains(in.token) then rejectWildcardType(infixType())
             else EmptyTree)
 
       /** id [‘as’ (id | ‘_’) */
diff --git a/compiler/src/dotty/tools/dotc/parsing/Tokens.scala b/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
index cba07a6e5a34..7fadf341905d 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
@@ -230,8 +230,8 @@ object Tokens extends TokensCommon {
 
   final val canStartExprTokens2: TokenSet = canStartExprTokens3 | BitSet(DO)
 
-  final val canStartTypeTokens: TokenSet = literalTokens | identifierTokens | BitSet(
-    THIS, SUPER, USCORE, LPAREN, AT)
+  final val canStartInfixTypeTokens: TokenSet = literalTokens | identifierTokens | BitSet(
+    THIS, SUPER, USCORE, LPAREN, LBRACE, AT)
 
   final val templateIntroTokens: TokenSet = BitSet(CLASS, TRAIT, OBJECT, ENUM, CASECLASS, CASEOBJECT)
 
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index b5b2bbc2e05f..969e0540cdc8 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -191,9 +191,9 @@ class PlainPrinter(_ctx: Context) extends Printer {
       case CapturingType(parent, refs) =>
         if refs.isConst then
           if Config.printCaptureSetsAsPrefix then
-            changePrec(GlobalPrec)("{" ~ toTextCaptureRef(ref) ~ "} " ~ toText(parent))
+            changePrec(GlobalPrec)("{" ~ Text(refs.elems.toList.map(toTextCaptureRef), ", ") ~ "} " ~ toText(parent))
           else
-            changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toTextCaptureRef(ref))
+            changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toText(refs.toRetainsTypeArg))
         else
           s"$refs " ~ toText(parent) // ^^^ improve
       case tp: PreviousErrorType if ctx.settings.XprintTypes.value =>
@@ -283,7 +283,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
 
   /** If -uniqid is set, the unique id of symbol, after a # */
   protected def idString(sym: Symbol): String =
-    if (showUniqueIds || Printer.debugPrintUnique) "#" + sym.id else ""
+    if showUniqueIds then "#" + sym.id else ""
 
   def nameString(sym: Symbol): String =
     simpleNameString(sym) + idString(sym) // + "<" + (if (sym.exists) sym.owner else "") + ">"
@@ -323,7 +323,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
       case tp @ ConstantType(value) =>
         toText(value)
       case pref: TermParamRef =>
-        nameString(pref.binder.paramNames(pref.paramNum))
+        nameString(pref.binder.paramNames(pref.paramNum)) ~ lambdaHash(pref.binder)
       case tp: RecThis =>
         val idx = openRecs.reverse.indexOf(tp.binder)
         if (idx >= 0) selfRecName(idx + 1)
diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index 0bf825a6baa0..96b14508584f 100644
--- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -532,6 +532,10 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
           changePrec(OrTypePrec) { toText(args(0)) ~ " | " ~ atPrec(OrTypePrec + 1) { toText(args(1)) } }
         else if (tpt.symbol == defn.andType && args.length == 2)
           changePrec(AndTypePrec) { toText(args(0)) ~ " & " ~ atPrec(AndTypePrec + 1) { toText(args(1)) } }
+        else if tpt.symbol == defn.Predef_retainsType && args.length == 2 then
+          changePrec(InfixPrec) { toText(args(0)) ~ " retains " ~ toText(args(1)) }
+        else if tpt.symbol == defn.Predef_capturing && args.length == 2 then
+          changePrec(GlobalPrec) { "{" ~ toText(args(0)) ~ "}" ~ toText(args(1)) }
         else if defn.isFunctionClass(tpt.symbol)
             && tpt.isInstanceOf[TypeTree] && tree.hasType && !printDebug
         then changePrec(GlobalPrec) { toText(tree.typeOpt) }
diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
index d709b52f30b2..f2b6c513899b 100644
--- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -218,6 +218,10 @@ trait TypeAssigner {
           if ctx.settings.Ycc.value
           then CapturingType(args(0), include(CaptureSet.empty, args(1)))
           else args(0)
+        else if constr == defn.Predef_capturing then
+          if ctx.settings.Ycc.value
+          then CapturingType(args(1), include(CaptureSet.empty, args(0)))
+          else args(1)
         else tp
       case _ => tp
   end processAppliedType
diff --git a/library/src/scala/runtime/stdLibPatches/Predef.scala b/library/src/scala/runtime/stdLibPatches/Predef.scala
index 1e9dc2303155..7882024bb43a 100644
--- a/library/src/scala/runtime/stdLibPatches/Predef.scala
+++ b/library/src/scala/runtime/stdLibPatches/Predef.scala
@@ -51,4 +51,6 @@ object Predef:
   /** type `A` with capture set `B` */
   infix type retains[A, B]
 
+  /** An alternative notation for capturing types. TODO: needed? Or maybe mangle the name? */
+  infix type |> [A, B]
 end Predef
diff --git a/tests/pos-custom-args/captures/cc-expand.scala b/tests/pos-custom-args/captures/cc-expand.scala
new file mode 100644
index 000000000000..bb94f8fd3ba1
--- /dev/null
+++ b/tests/pos-custom-args/captures/cc-expand.scala
@@ -0,0 +1,21 @@
+object Test:
+
+  class A
+  class B
+  class C
+  class CTC
+  type CT = CTC retains *
+
+  def test(ct: CT, dt: CT) =
+
+    def x0: A => {ct} B = ???
+
+    def x1: A => B retains ct.type = ???
+    def x2: A => B => C retains ct.type = ???
+    def x3: A => () => B => C retains ct.type = ???
+
+    def x4: (x: A retains ct.type) => B => C = ???
+
+    def x5: A => (x: B retains ct.type) => () => C retains dt.type = ???
+    def x6: A => (x: B retains ct.type) => (() => C retains dt.type) retains x.type | dt.type = ???
+    def x7: A => (x: B retains ct.type) => (() => C retains dt.type) retains x.type = ???
\ No newline at end of file

From c7e5ddb45a66c6c678b9a08094dfe4dc2f9226ce Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 15 Aug 2021 17:59:03 +0200
Subject: [PATCH 14/25] Add boxmap test from paper

---
 .../tools/dotc/typer/CheckCaptures.scala      |  2 +-
 .../captures/boxmap-paper.scala               | 38 +++++++++++++++++++
 2 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 tests/pos-custom-args/captures/boxmap-paper.scala

diff --git a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
index d34ddaad389e..2e300b1e2e20 100644
--- a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
@@ -80,7 +80,7 @@ class CheckCaptures extends Recheck:
     import ast.tpd.*
 
     override def reinfer(tp: Type)(using Context): Type =
-      CapturingType(tp, CaptureSet.Var())
+      CapturingType(tp, CaptureSet.Var()) // ^^^ go deep
 
     private var curEnv: Env = Env(NoSymbol, CaptureSet.empty, false, null)
 
diff --git a/tests/pos-custom-args/captures/boxmap-paper.scala b/tests/pos-custom-args/captures/boxmap-paper.scala
new file mode 100644
index 000000000000..6b67fac567cd
--- /dev/null
+++ b/tests/pos-custom-args/captures/boxmap-paper.scala
@@ -0,0 +1,38 @@
+infix type ==> [A, B] = (A => B) retains *
+
+type Cell[+T] = [K] => (T ==> K) => K
+
+def cell[T](x: T): Cell[T] =
+  [K] => (k: T ==> K) => k(x)
+
+def get[T](c: Cell[T]): T = c[T](identity[T]) // TODO: drop [T]
+
+def map[A, B](c: Cell[A])(f: A ==> B): Cell[B]
+  = c[Cell[B]]((x: A) => cell(f(x)))
+
+def pureMap[A, B](c: Cell[A])(f: A => B): Cell[B]
+  = c[Cell[B]]((x: A) => cell(f(x)))
+
+def lazyMap[A, B](c: Cell[A])(f: A ==> B): {f} () => Cell[B]
+  = () => c[Cell[B]]((x: A) => cell(f(x)))
+
+trait IO:
+  def print(s: String): Unit
+
+def test(io: {*} IO) =
+
+  val loggedOne: {io} () => Int = () => { io.print("1"); 1 }
+
+  val c: Cell[{io} () => Int]
+      = cell[{io} () => Int](loggedOne)
+
+  val g = (f: {io} () => Int) =>
+    val x = f(); io.print(" + ")
+    val y = f(); io.print(s" = ${x + y}")
+
+  val r = lazyMap[{io} () => Int, Unit](c)(f => g(f))
+  val r2 = lazyMap[{io} () => Int, Unit](c)(g)
+  //  val r3 = lazyMap(c)(g)  not yet
+  val _ = r()
+  val _ = r2()
+  // val _ = r3()

From ea884bdabed23aeef349b667415ba158d67df911 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 15 Aug 2021 18:32:20 +0200
Subject: [PATCH 15/25] Fix problem in decomposeProtoFunction

Need to strip again after dealiasing
---
 compiler/src/dotty/tools/dotc/core/Types.scala    | 4 ++++
 compiler/src/dotty/tools/dotc/typer/Typer.scala   | 2 +-
 tests/pos-custom-args/captures/boxmap-paper.scala | 4 ++--
 3 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 440359715078..95f931f78eb8 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1190,6 +1190,10 @@ object Types {
     /** Strip TypeVars and Annotation and CapturingType wrappers */
     def stripped(using Context): Type = this
 
+    def strippedDealias(using Context): Type =
+      val tp1 = stripped.dealias
+      if tp1 ne this then tp1.strippedDealias else this
+
     def rewrapAnnots(tp: Type)(using Context): Type = tp.stripTypeVar match {
       case AnnotatedType(tp1, annot) => AnnotatedType(rewrapAnnots(tp1), annot)
       case _ => this
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 9ff97cbed778..9bd569a52138 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1130,7 +1130,7 @@ class Typer extends Namer
         case _ => mapOver(t)
     }
 
-    val pt1 = pt.stripped.dealias
+    val pt1 = pt.strippedDealias
     if (pt1 ne pt1.dropDependentRefinement)
        && defn.isContextFunctionType(pt1.nonPrivateMember(nme.apply).info.finalResultType)
     then
diff --git a/tests/pos-custom-args/captures/boxmap-paper.scala b/tests/pos-custom-args/captures/boxmap-paper.scala
index 6b67fac567cd..fe77fa9a6627 100644
--- a/tests/pos-custom-args/captures/boxmap-paper.scala
+++ b/tests/pos-custom-args/captures/boxmap-paper.scala
@@ -5,7 +5,7 @@ type Cell[+T] = [K] => (T ==> K) => K
 def cell[T](x: T): Cell[T] =
   [K] => (k: T ==> K) => k(x)
 
-def get[T](c: Cell[T]): T = c[T](identity[T]) // TODO: drop [T]
+def get[T](c: Cell[T]): T = c[T](identity)
 
 def map[A, B](c: Cell[A])(f: A ==> B): Cell[B]
   = c[Cell[B]]((x: A) => cell(f(x)))
@@ -32,7 +32,7 @@ def test(io: {*} IO) =
 
   val r = lazyMap[{io} () => Int, Unit](c)(f => g(f))
   val r2 = lazyMap[{io} () => Int, Unit](c)(g)
-  //  val r3 = lazyMap(c)(g)  not yet
+  // val r3 = lazyMap(c)(g)
   val _ = r()
   val _ = r2()
   // val _ = r3()

From 203391c250eb0f48f79456ad3b8e2556eb1530b7 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 16 Aug 2021 11:09:43 +0200
Subject: [PATCH 16/25] Use explicit Top bounds for boxmap example

Can be reverted once we assume type variables have by default a {*} Any upper bound.
---
 .../captures/boxmap-paper.scala               | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/tests/pos-custom-args/captures/boxmap-paper.scala b/tests/pos-custom-args/captures/boxmap-paper.scala
index fe77fa9a6627..65f76bac9f05 100644
--- a/tests/pos-custom-args/captures/boxmap-paper.scala
+++ b/tests/pos-custom-args/captures/boxmap-paper.scala
@@ -1,19 +1,20 @@
-infix type ==> [A, B] = (A => B) retains *
+type Top = {*} Any retains *
+infix type ==> [A, B] = {*} (A => B)
 
-type Cell[+T] = [K] => (T ==> K) => K
+type Cell[+T <: Top] = [K] => (T ==> K) => K
 
-def cell[T](x: T): Cell[T] =
+def cell[T <: Top](x: T): Cell[T] =
   [K] => (k: T ==> K) => k(x)
 
-def get[T](c: Cell[T]): T = c[T](identity)
+def get[T <: Top](c: Cell[T]): T = c[T](identity)
 
-def map[A, B](c: Cell[A])(f: A ==> B): Cell[B]
+def map[A <: Top, B <: Top](c: Cell[A])(f: A ==> B): Cell[B]
   = c[Cell[B]]((x: A) => cell(f(x)))
 
-def pureMap[A, B](c: Cell[A])(f: A => B): Cell[B]
+def pureMap[A <: Top, B <: Top](c: Cell[A])(f: A => B): Cell[B]
   = c[Cell[B]]((x: A) => cell(f(x)))
 
-def lazyMap[A, B](c: Cell[A])(f: A ==> B): {f} () => Cell[B]
+def lazyMap[A <: Top, B <: Top](c: Cell[A])(f: A ==> B): {f} () => Cell[B]
   = () => c[Cell[B]]((x: A) => cell(f(x)))
 
 trait IO:
@@ -32,7 +33,7 @@ def test(io: {*} IO) =
 
   val r = lazyMap[{io} () => Int, Unit](c)(f => g(f))
   val r2 = lazyMap[{io} () => Int, Unit](c)(g)
-  // val r3 = lazyMap(c)(g)
+  val r3 = lazyMap(c)(g)
   val _ = r()
   val _ = r2()
-  // val _ = r3()
+  val _ = r3()

From 99dc50a83e3275376ca9c9780bca83d845bd3404 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 16 Aug 2021 18:44:58 +0200
Subject: [PATCH 17/25] Move checkCaptures before pruneErasedDefs

pruneErasedDef's normalizations interfere with it.
---
 compiler/src/dotty/tools/dotc/Compiler.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/Compiler.scala b/compiler/src/dotty/tools/dotc/Compiler.scala
index 434c4fcf1942..4aad085fb80f 100644
--- a/compiler/src/dotty/tools/dotc/Compiler.scala
+++ b/compiler/src/dotty/tools/dotc/Compiler.scala
@@ -84,6 +84,8 @@ class Compiler {
          new ExplicitSelf,           // Make references to non-trivial self types explicit as casts
          new ElimByName,             // Expand by-name parameter references
          new StringInterpolatorOpt) :: // Optimizes raw and s string interpolators by rewriting them to string concatenations
+    List(new PreRecheck) ::          // Preparations for check captures phase, enabled under -Ycc
+    List(new CheckCaptures) ::       // Check captures, enabled under -Ycc
     List(new PruneErasedDefs,        // Drop erased definitions from scopes and simplify erased expressions
          new UninitializedDefs,      // Replaces `compiletime.uninitialized` by `_`
          new InlinePatterns,         // Remove placeholders of inlined patterns
@@ -101,8 +103,6 @@ class Compiler {
          new TupleOptimizations,     // Optimize generic operations on tuples
          new LetOverApply,           // Lift blocks from receivers of applications
          new ArrayConstructors) ::   // Intercept creation of (non-generic) arrays and intrinsify.
-    List(new PreRecheck) ::          // Preparations for recheck phase, enabled under -Yrecheck
-    List(new TestRecheck) ::         // Test rechecking, enabled under -Yrecheck
     List(new Erasure) ::             // Rewrite types to JVM model, erasing all type parameters, abstract types and refinements.
     List(new ElimErasedValueType,    // Expand erased value types to their underlying implmementation types
          new PureStats,              // Remove pure stats from blocks

From 0515a866f9be218ce6dac30ca68c9af45896a5a5 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 16 Aug 2021 19:02:08 +0200
Subject: [PATCH 18/25] Clean up printing of capture sets

---
 .../dotty/tools/dotc/printing/PlainPrinter.scala    | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 969e0540cdc8..8a01bc64f2e6 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -189,13 +189,14 @@ class PlainPrinter(_ctx: Context) extends Printer {
           (" <: " ~ toText(bound) provided !bound.isAny)
         }.close
       case CapturingType(parent, refs) =>
-        if refs.isConst then
-          if Config.printCaptureSetsAsPrefix then
-            changePrec(GlobalPrec)("{" ~ Text(refs.elems.toList.map(toTextCaptureRef), ", ") ~ "} " ~ toText(parent))
-          else
-            changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toText(refs.toRetainsTypeArg))
+        if printDebug && !refs.isConst then
+          s"$refs " ~ toText(parent)
+        else if refs.elems.isEmpty then
+          toText(parent)
+        else if Config.printCaptureSetsAsPrefix then
+          changePrec(GlobalPrec)("{" ~ Text(refs.elems.toList.map(toTextCaptureRef), ", ") ~ "} " ~ toText(parent))
         else
-          s"$refs " ~ toText(parent) // ^^^ improve
+          changePrec(InfixPrec)(toText(parent) ~ " retains " ~ toText(refs.toRetainsTypeArg))
       case tp: PreviousErrorType if ctx.settings.XprintTypes.value =>
         "<error>" // do not print previously reported error message because they may try to print this error type again recuresevely
       case tp: ErrorType =>

From da82287ecac2f7d01073cde272911dc7d217c935 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 16 Aug 2021 19:02:55 +0200
Subject: [PATCH 19/25] Give Closure trees the span of the underling function

---
 compiler/src/dotty/tools/dotc/ast/Desugar.scala | 4 +++-
 tests/neg/i7746.scala                           | 2 +-
 tests/neg/i9299.scala                           | 4 ++--
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/ast/Desugar.scala b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
index 057a93196154..7b29c21dba6a 100644
--- a/compiler/src/dotty/tools/dotc/ast/Desugar.scala
+++ b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
@@ -1339,7 +1339,9 @@ object desugar {
       DefDef(nme.ANON_FUN, params :: Nil, if (tpt == null) TypeTree() else tpt, body)
         .withSpan(span)
         .withMods(synthetic | Artifact),
-      Closure(Nil, Ident(nme.ANON_FUN), if (isContextual) ContextualEmptyTree else EmptyTree))
+      Closure(Nil, Ident(nme.ANON_FUN), if (isContextual) ContextualEmptyTree else EmptyTree)
+        .withSpan(span)
+    )
 
   /** If `nparams` == 1, expand partial function
    *
diff --git a/tests/neg/i7746.scala b/tests/neg/i7746.scala
index f0990e86d94a..502861c2ffbb 100644
--- a/tests/neg/i7746.scala
+++ b/tests/neg/i7746.scala
@@ -1,3 +1,3 @@
 class A {
-    def foo = (x : Int, y => x) => () // error // error
+    def foo = (x : Int, y => x) => () // error: not a gel formal parameter
 }
\ No newline at end of file
diff --git a/tests/neg/i9299.scala b/tests/neg/i9299.scala
index 6c23d11553ff..119b268a842e 100644
--- a/tests/neg/i9299.scala
+++ b/tests/neg/i9299.scala
@@ -1,4 +1,4 @@
-type F <: F = 1 match { // error
-  case _ => foo.foo // error // error
+type F <: F = 1 match { // error: Recursion limit exceeded.
+  case _ => foo.foo // error: Recursion limit exceeded.
 }
 def foo(a: Int): Unit = ???

From c89072c5552ab3d763907e66d2da6c76f9b90687 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 16 Aug 2021 19:04:08 +0200
Subject: [PATCH 20/25] Fix checkNotGlobal condition for root capture set

---
 .../src/dotty/tools/dotc/typer/CheckCaptures.scala   | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
index 2e300b1e2e20..07f2f34b10be 100644
--- a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
@@ -95,6 +95,7 @@ class CheckCaptures extends Recheck:
         val ref = sym.termRef
         def recur(env: Env): Unit =
           if env.isOpen && env.owner != sym.enclosure then
+            capt.println(i"Mark $sym free in ${env.owner}")
             checkElem(ref, env.captured, pos)
             recur(env.outer)
         if ref.isTracked then recur(curEnv)
@@ -153,7 +154,7 @@ class CheckCaptures extends Recheck:
 
     override def recheck(tree: Tree, pt: Type = WildcardType)(using Context): Type =
       val saved = curEnv
-      if pt.needsBox && !curEnv.isBoxed then
+      if pt.needsBox && !curEnv.isBoxed && false then // ^^^ refine
         curEnv = Env(NoSymbol, CaptureSet.Var(), true, curEnv)
       try
         val res = super.recheck(tree, pt)
@@ -171,15 +172,14 @@ class CheckCaptures extends Recheck:
 
   def checkNotGlobal(tree: Tree, allArgs: Tree*)(using Context): Unit =
     if disallowGlobal then
-      //println(i"checking $arg in $tree: ${arg.tpe.captureSet}")
       tree match
         case LambdaTypeTree(_, restpt) =>
           checkNotGlobal(restpt, allArgs*)
         case _ =>
           for ref <- tree.tpe.captureSet.elems do
             val isGlobal = ref match
-              case ref: TypeRef => ref.isRootCapability
-              case ref: TermRef => ref.prefix != NoPrefix && ref.symbol.hasAnnotation(defn.AbilityAnnot)
+              case ref: TermRef =>
+                ref.isRootCapability || ref.prefix != NoPrefix && ref.symbol.hasAnnotation(defn.AbilityAnnot)
               case _ => false
             val what = if ref.isRootCapability then "universal" else "global"
             if isGlobal then
@@ -196,7 +196,9 @@ class CheckCaptures extends Recheck:
     def traverse(tree: Tree)(using Context) =
       tree match
         case tree1 @ TypeApply(fn, args) if disallowGlobal =>
-          for arg <- args do checkNotGlobal(arg, args*)
+          for arg <- args do
+            //println(i"checking $arg in $tree: ${arg.tpe.captureSet}")
+            checkNotGlobal(arg, args*)
         case _ =>
       traverseChildren(tree)
 

From 636c57cac81eb9c79799c7f8c250ff4bdcdfa06d Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 16 Aug 2021 19:08:37 +0200
Subject: [PATCH 21/25] Fix tests

---
 .../neg-custom-args/captures/try2.check       |  0
 .../neg-custom-args/captures/try2.scala       |  1 +
 tests/neg-custom-args/captures/capt1.check    | 14 +++----
 tests/neg-custom-args/captures/try.check      | 37 +++++++------------
 tests/neg-custom-args/captures/try.scala      | 10 ++---
 tests/neg/multiLineOps.scala                  |  2 +-
 .../captures/list-encoding.scala              |  8 ++--
 7 files changed, 33 insertions(+), 39 deletions(-)
 rename tests/{ => disabled}/neg-custom-args/captures/try2.check (100%)
 rename tests/{ => disabled}/neg-custom-args/captures/try2.scala (96%)

diff --git a/tests/neg-custom-args/captures/try2.check b/tests/disabled/neg-custom-args/captures/try2.check
similarity index 100%
rename from tests/neg-custom-args/captures/try2.check
rename to tests/disabled/neg-custom-args/captures/try2.check
diff --git a/tests/neg-custom-args/captures/try2.scala b/tests/disabled/neg-custom-args/captures/try2.scala
similarity index 96%
rename from tests/neg-custom-args/captures/try2.scala
rename to tests/disabled/neg-custom-args/captures/try2.scala
index 469d9cf8d2f2..a8ca48b6de32 100644
--- a/tests/neg-custom-args/captures/try2.scala
+++ b/tests/disabled/neg-custom-args/captures/try2.scala
@@ -1,3 +1,4 @@
+// Retains syntax for classes not (yet?) supported
 import language.experimental.erasedDefinitions
 import annotation.ability
 
diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check
index f143f930e8f2..df48efae1551 100644
--- a/tests/neg-custom-args/captures/capt1.check
+++ b/tests/neg-custom-args/captures/capt1.check
@@ -1,11 +1,11 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:3:2 ------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:3:5 ------------------------------------------
 3 |  () => if x == null then y else y  // error
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |  Found:    {x} () => C
   |  Required: () => C
 
 longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:6:2 ------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:6:5 ------------------------------------------
 6 |  () => if x == null then y else y  // error
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |  Found:    {x} () => C
@@ -19,24 +19,24 @@ longer explanation available when compiling with `-explain`
    |  Required: Any
 
 longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:23:3 -----------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:23:2 -----------------------------------------
 23 |  F(22)  // error
    |  ^^^^^
-   |  Found:    {x} F
+   |  Found:    {x} A
    |  Required: A
 
 longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:27:40 ----------------------------------------
 27 |    def m() = if x == null then y else y  // error
    |                                        ^
-   |                                        Found:    {x} A {...}
+   |                                        Found:    {x} A
    |                                        Required: A
 
 longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:32:24 ----------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:32:27 ----------------------------------------
 32 |  val z2 = h[() => Cap](() => x)(() => C())  // error
    |                        ^^^^^^^
-   |                        Found:    (() => Cap) retains x
+   |                        Found:    {x} () => Cap
    |                        Required: () => Cap
 
 longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index 22d761642d05..da490586d115 100644
--- a/tests/neg-custom-args/captures/try.check
+++ b/tests/neg-custom-args/captures/try.check
@@ -1,38 +1,29 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:32 ------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:35 ------------------------------------------
 29 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)  // error
    |                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |                                Found:    {x} () => Nothing
    |                                Required: () => Nothing
 
 longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:43:2 -------------------------------------------
-43 |  yy  // error
-   |  ^^
-   |  Found:    (yy : List[(xx : (() => Int) retains *)])
-   |  Required: List[() => Int]
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:36:9 -------------------------------------------
+36 |      () => // error
+   |      ^
+   |      Found:    {x} () => Int
+   |      Required: () => Int
+37 |        raise(new Exception)(using x)
+38 |        22
 
 longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:50:2 -------------------------------------------
-45 |val global = handle {
-46 |  (x: CanThrow[Exception]) =>
-47 |    () =>
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:47:7 -------------------------------------------
+47 |    () => // error
+   |    ^
+   |    Found:    {x} () => Int
+   |    Required: () => Int
 48 |      raise(new Exception)(using x)
 49 |      22
-50 |} {  // error
-   |             ^
-   |             Found:    (() => Int) retains *
-   |             Required: () => Int
-51 |  (ex: Exception) => () => 22
-52 |}
 
 longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/try.scala:22:28 ---------------------------------------------------------------
 22 |  val a = handle[Exception, CanThrow[Exception]] { // error
    |                            ^^^^^^^^^^^^^^^^^^^
-   |                            type argument is not allowed to capture the universal capability *
--- Error: tests/neg-custom-args/captures/try.scala:34:11 ---------------------------------------------------------------
-34 |  val xx = handle { // error
-   |           ^^^^^^
-   |           inferred type argument ((() => Int) retains *) is not allowed to capture the universal capability *
-   |
-   |           The inferred arguments are: [Exception, ((() => Int) retains *)]
+   |                            type argument is not allowed to capture the universal capability (* : Any)
diff --git a/tests/neg-custom-args/captures/try.scala b/tests/neg-custom-args/captures/try.scala
index 4784d055fccc..9e08cc055471 100644
--- a/tests/neg-custom-args/captures/try.scala
+++ b/tests/neg-custom-args/captures/try.scala
@@ -31,22 +31,22 @@ def test: List[() => Int] =
     (ex: Exception) => ???
   }
 
-  val xx = handle { // error
+  val xx = handle {
     (x: CanThrow[Exception]) =>
-      () =>
+      () => // error
         raise(new Exception)(using x)
         22
   } {
     (ex: Exception) => () => 22
   }
   val yy = xx :: Nil
-  yy  // error
+  yy // OK
 
 val global = handle {
   (x: CanThrow[Exception]) =>
-    () =>
+    () => // error
       raise(new Exception)(using x)
       22
-} {  // error
+} {
   (ex: Exception) => () => 22
 }
\ No newline at end of file
diff --git a/tests/neg/multiLineOps.scala b/tests/neg/multiLineOps.scala
index 8499cc9fe710..08a0a3925fd1 100644
--- a/tests/neg/multiLineOps.scala
+++ b/tests/neg/multiLineOps.scala
@@ -5,7 +5,7 @@ val x = 1
 val b1 = {
   22
   * 22  // ok
-  */*one more*/22 // error: end of statement expected // error: not found: *
+  */*one more*/22 // error: end of statement expected
 }
 
 val b2: Boolean = {
diff --git a/tests/pos-custom-args/captures/list-encoding.scala b/tests/pos-custom-args/captures/list-encoding.scala
index 91cf6d92c08f..7aba62cb6d60 100644
--- a/tests/pos-custom-args/captures/list-encoding.scala
+++ b/tests/pos-custom-args/captures/list-encoding.scala
@@ -1,11 +1,13 @@
+package listEncoding
+
 type Top = Any retains *
-class Cap extends Retains[*]
+class Cap
 
 type Op[T <: Top, C <: Top] =
   ((v: T) => ((s: C) => C) retains *) retains *
 
 type List[T <: Top] =
-  ([C <: Top] => (op: Op[T, C]) => ((s: C) => C) retains op.type) retains T
+  ([C <: Top] => (op: Op[T, C]) => ({op} (s: C) => C))
 
 def nil[T <: Top]: List[T] =
   [C <: Top] => (op: Op[T, C]) => (s: C) => s
@@ -13,7 +15,7 @@ def nil[T <: Top]: List[T] =
 def cons[T <: Top](hd: T, tl: List[T]): List[T] =
   [C <: Top] => (op: Op[T, C]) => (s: C) => op(hd)(tl(op)(s))
 
-def foo(c: Cap) =
+def foo(c: {*} Cap) =
   def f(x: String retains c.type, y: String retains c.type) =
     cons(x, cons(y, nil))
   def g(x: String retains c.type, y: Any) =

From 1214a6783dcc16d43b9e4d40eb58c926ddb6f0a1 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 16 Aug 2021 22:25:39 +0200
Subject: [PATCH 22/25] Fix noCaptures condition

---
 compiler/src/dotty/tools/dotc/core/Types.scala     | 9 ++++++++-
 tests/pos-custom-args/captures/boxmap-paper.scala  | 2 ++
 tests/pos-custom-args/captures/list-encoding.scala | 2 +-
 3 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 95f931f78eb8..2fffa42fd12e 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1514,7 +1514,14 @@ object Types {
 
     def captureSet(using Context): CaptureSet = CaptureSet.ofType(this)
     def noCaptures(using Context): Boolean =
-      ctx.mode.is(Mode.RelaxedCapturing) || captureSet.isEmpty
+      ctx.mode.is(Mode.RelaxedCapturing) || allCaptures.isEmpty
+
+    def allCaptures(using Context): CaptureSet = this match // ^^^^ optimize, relate with boxedCaptures?
+      case tp: CapturingType => tp.refs
+      case tp: TypeProxy => tp.superType.allCaptures
+      case tp: AndType => tp.tp1.allCaptures ++ tp.tp2.allCaptures
+      case tp: OrType => tp.tp1.allCaptures ** tp.tp2.allCaptures
+      case _ => CaptureSet.empty
 
     // ----- Normalizing typerefs over refined types ----------------------------
 
diff --git a/tests/pos-custom-args/captures/boxmap-paper.scala b/tests/pos-custom-args/captures/boxmap-paper.scala
index 65f76bac9f05..242b7ea95b78 100644
--- a/tests/pos-custom-args/captures/boxmap-paper.scala
+++ b/tests/pos-custom-args/captures/boxmap-paper.scala
@@ -6,6 +6,8 @@ type Cell[+T <: Top] = [K] => (T ==> K) => K
 def cell[T <: Top](x: T): Cell[T] =
   [K] => (k: T ==> K) => k(x)
 
+def identity[T <: Top](x: T): T = x
+
 def get[T <: Top](c: Cell[T]): T = c[T](identity)
 
 def map[A <: Top, B <: Top](c: Cell[A])(f: A ==> B): Cell[B]
diff --git a/tests/pos-custom-args/captures/list-encoding.scala b/tests/pos-custom-args/captures/list-encoding.scala
index 7aba62cb6d60..28b52372d497 100644
--- a/tests/pos-custom-args/captures/list-encoding.scala
+++ b/tests/pos-custom-args/captures/list-encoding.scala
@@ -19,6 +19,6 @@ def foo(c: {*} Cap) =
   def f(x: String retains c.type, y: String retains c.type) =
     cons(x, cons(y, nil))
   def g(x: String retains c.type, y: Any) =
-    cons(x, cons(y, nil))
+    cons[{c} Any](x, cons[Any](y, nil))  // TODO: drop type arguments
   def h(x: String, y: Any retains c.type) =
     cons(x, cons(y, nil))

From 550de29bcf690afadcce7e8b3c43d4455417a252 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 17 Aug 2021 10:58:12 +0200
Subject: [PATCH 23/25] Include call captures for parameterless methods

---
 .../src/dotty/tools/dotc/core/Types.scala     |  6 ++---
 .../dotty/tools/dotc/transform/Recheck.scala  |  4 ++-
 .../tools/dotc/typer/CheckCaptures.scala      | 25 +++++++++++--------
 .../neg-custom-args/captures/capt-wf.scala    |  1 +
 tests/neg-custom-args/captures/boxmap.check   | 10 +++-----
 tests/neg-custom-args/captures/boxmap.scala   |  3 +--
 tests/neg-custom-args/captures/io.scala       |  3 ++-
 tests/neg-custom-args/captures/try3.scala     |  9 ++++---
 8 files changed, 33 insertions(+), 28 deletions(-)
 rename tests/{ => disabled}/neg-custom-args/captures/capt-wf.scala (95%)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 2fffa42fd12e..ba8fae7bc0f9 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1513,8 +1513,8 @@ object Types {
     }
 
     def captureSet(using Context): CaptureSet = CaptureSet.ofType(this)
-    def noCaptures(using Context): Boolean =
-      ctx.mode.is(Mode.RelaxedCapturing) || allCaptures.isEmpty
+    def noCaptures(using Context): Boolean = // ^^^ drop
+      ctx.mode.is(Mode.RelaxedCapturing) || !ctx.settings.Ycc.value || allCaptures.isEmpty
 
     def allCaptures(using Context): CaptureSet = this match // ^^^^ optimize, relate with boxedCaptures?
       case tp: CapturingType => tp.refs
@@ -2709,7 +2709,7 @@ object Types {
      *  References to term parameters of classes cannot be tracked individually.
      *  They are subsumed in the capture sets of the enclosing class.
      */
-    def canBeTracked(using Context) =
+    def canBeTracked(using Context) = // ^^^ exclude methods
       (prefix eq NoPrefix) || symbol.hasAnnotation(defn.AbilityAnnot) || isRootCapability
 
     override def isRootCapability(using Context): Boolean =
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 224d25fb11b5..c3be1fc86ef3 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -59,6 +59,8 @@ abstract class Recheck extends Phase, IdentityDenotTransformer:
     def reinferResult(info: Type)(using Context): Type = info match
       case info: MethodOrPoly =>
         info.derivedLambdaType(resType = reinferResult(info.resType))
+      case info: ExprType =>
+        info.derivedExprType(resType = reinferResult(info.resType))
       case _ =>
         reinfer(info)
 
@@ -317,7 +319,7 @@ abstract class Recheck extends Phase, IdentityDenotTransformer:
           || expected.isRepeatedParam
              && actual <:< expected.translateFromRepeated(toArray = tree.tpe.isRef(defn.ArrayClass))
         if !isCompatible then
-          err.typeMismatch(tree.withType(tpe), pt)
+          err.typeMismatch(tree.withType(tpe), expected)
 
     def checkUnit(unit: CompilationUnit)(using Context): Unit =
       recheck(unit.tpdTree)
diff --git a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
index 07f2f34b10be..fcd8ca0b9b2c 100644
--- a/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala
@@ -95,11 +95,22 @@ class CheckCaptures extends Recheck:
         val ref = sym.termRef
         def recur(env: Env): Unit =
           if env.isOpen && env.owner != sym.enclosure then
-            capt.println(i"Mark $sym free in ${env.owner}")
+            capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}")
             checkElem(ref, env.captured, pos)
             recur(env.outer)
         if ref.isTracked then recur(curEnv)
 
+    def includeCallCaptures(sym: Symbol, pos: SrcPos)(using Context): Unit =
+      if curEnv.isOpen then
+        val ownEnclosure = ctx.owner.enclosingMethodOrClass
+        var targetSet = capturedVars(sym)
+        if !targetSet.isEmpty && sym.enclosure == ownEnclosure then
+          targetSet = targetSet.filter {
+            case ref: TermRef => ref.symbol.enclosure != ownEnclosure
+            case _ => true
+          }
+        checkSubset(targetSet, curEnv.captured, pos)
+
     def assertSub(cs1: CaptureSet, cs2: CaptureSet)(using Context) =
       assert((cs1 <:< cs2) == CompareResult.OK, i"$cs1 is not a subset of $cs2")
 
@@ -121,6 +132,7 @@ class CheckCaptures extends Recheck:
 
     override def recheckIdent(tree: Ident)(using Context): Type =
       markFree(tree.symbol, tree.srcPos)
+      if tree.symbol.is(Method) then includeCallCaptures(tree.symbol, tree.srcPos)
       super.recheckIdent(tree)
 
     override def recheckDefDef(tree: DefDef, sym: Symbol)(using Context): Type =
@@ -138,17 +150,8 @@ class CheckCaptures extends Recheck:
       finally curEnv = saved
 
     override def recheckApply(tree: Apply, pt: Type)(using Context): Type =
-      if curEnv.isOpen then
-        val ownEnclosure = ctx.owner.enclosingMethodOrClass
-        var targetSet = capturedVars(tree.symbol)
-        if !targetSet.isEmpty && tree.symbol.enclosure == ownEnclosure then
-          targetSet = targetSet.filter {
-            case ref: TermRef => ref.symbol.enclosure != ownEnclosure
-            case _ => true
-          }
-
-        checkSubset(targetSet, curEnv.captured, tree.srcPos)
       val sym = tree.symbol
+      includeCallCaptures(sym, tree.srcPos)
       val cs = if sym.isConstructor then capturedVars(sym.owner) else CaptureSet.empty
       super.recheckApply(tree, pt).capturing(cs)
 
diff --git a/tests/neg-custom-args/captures/capt-wf.scala b/tests/disabled/neg-custom-args/captures/capt-wf.scala
similarity index 95%
rename from tests/neg-custom-args/captures/capt-wf.scala
rename to tests/disabled/neg-custom-args/captures/capt-wf.scala
index 41ed177e853d..7c654dfc0533 100644
--- a/tests/neg-custom-args/captures/capt-wf.scala
+++ b/tests/disabled/neg-custom-args/captures/capt-wf.scala
@@ -1,3 +1,4 @@
+// No longer valid
 class C
 type Cap = C retains *
 type Top = Any retains *
diff --git a/tests/neg-custom-args/captures/boxmap.check b/tests/neg-custom-args/captures/boxmap.check
index da1c38b4a887..5da51abd30d1 100644
--- a/tests/neg-custom-args/captures/boxmap.check
+++ b/tests/neg-custom-args/captures/boxmap.check
@@ -1,9 +1,7 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boxmap.scala:15:2 ----------------------------------------
-15 |  () => b[Box[B]]((x: A) => box(f(x)))  // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boxmap.scala:14:5 ----------------------------------------
+14 |  () => b[Box[B]]((x: A) => box(f(x)))  // error
    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |  Found:    {f} {b} () => Box[B]
-   |  Required: {B} () => Box[B]
-   |
-   |  where:    B is a type in method lazymap with bounds <: Top
+   |  Found:    {f} () => Box[B]
+   |  Required: () => Box[B]
 
 longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/boxmap.scala b/tests/neg-custom-args/captures/boxmap.scala
index cb77c6794cb1..b62c48630c70 100644
--- a/tests/neg-custom-args/captures/boxmap.scala
+++ b/tests/neg-custom-args/captures/boxmap.scala
@@ -1,9 +1,8 @@
 type Top = Any retains *
-class Cap extends Retains[*]
 
 infix type ==> [A, B] = (A => B) retains *
 
-type Box[+T <: Top] = ([K <: Top] => (T ==> K) => K) retains T
+type Box[+T <: Top] = ([K <: Top] => (T ==> K) => K)
 
 def box[T <: Top](x: T): Box[T] =
   [K <: Top] => (k: T ==> K) => k(x)
diff --git a/tests/neg-custom-args/captures/io.scala b/tests/neg-custom-args/captures/io.scala
index a9636b045694..18986d600719 100644
--- a/tests/neg-custom-args/captures/io.scala
+++ b/tests/neg-custom-args/captures/io.scala
@@ -3,7 +3,7 @@ sealed trait IO:
 
 def test1 =
   val IO : IO retains * = new IO {}
-  def foo = IO.puts("hello")
+  def foo = {IO; IO.puts("hello") }
   val x : () => Unit = () => foo  // error: Found: (() => Unit) retains IO; Required: () => Unit
 
 def test2 =
@@ -19,3 +19,4 @@ def test3 =
   def puts(msg: Any, io: Capability[IO]) = println(msg)
   def foo() = puts("hello", IO)
   val x : () => Unit = () => foo()  // error: Found: (() => Unit) retains IO; Required: () => Unit
+
diff --git a/tests/neg-custom-args/captures/try3.scala b/tests/neg-custom-args/captures/try3.scala
index f90ad6aff0aa..0e149d7b440a 100644
--- a/tests/neg-custom-args/captures/try3.scala
+++ b/tests/neg-custom-args/captures/try3.scala
@@ -1,7 +1,8 @@
 import java.io.IOException
 
-class CanThrow[E] extends Retains[*]
-type Top  = Any retains *
+class CT[E]
+type CanThrow[E] = {*} CT[E]
+type Top  = {*} Any
 
 def handle[E <: Exception, T <: Top](op: CanThrow[E] ?=> T)(handler: E => T): T =
   val x: CanThrow[E] = ???
@@ -13,9 +14,9 @@ def raise[E <: Exception](ex: E)(using CanThrow[E]): Nothing =
 
 @main def Test: Int =
   def f(a: Boolean) =
-    handle { // error
+    handle {
       if !a then raise(IOException())
-      (b: Boolean) =>
+      (b: Boolean) => // error
         if !b then raise(IOException())
         0
     } {

From f3153a42b7142af67b29df4a40c43cb9f3837d73 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 17 Aug 2021 11:32:48 +0200
Subject: [PATCH 24/25] Revert "Give Closure trees the span of the underling
 function"

This reverts commit 99d83957ba4d87beeabb825a23a2db78850f3a4a.
---
 compiler/src/dotty/tools/dotc/ast/Desugar.scala | 4 +---
 tests/neg/i7746.scala                           | 2 +-
 tests/neg/i9299.scala                           | 4 ++--
 3 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/ast/Desugar.scala b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
index 7b29c21dba6a..057a93196154 100644
--- a/compiler/src/dotty/tools/dotc/ast/Desugar.scala
+++ b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
@@ -1339,9 +1339,7 @@ object desugar {
       DefDef(nme.ANON_FUN, params :: Nil, if (tpt == null) TypeTree() else tpt, body)
         .withSpan(span)
         .withMods(synthetic | Artifact),
-      Closure(Nil, Ident(nme.ANON_FUN), if (isContextual) ContextualEmptyTree else EmptyTree)
-        .withSpan(span)
-    )
+      Closure(Nil, Ident(nme.ANON_FUN), if (isContextual) ContextualEmptyTree else EmptyTree))
 
   /** If `nparams` == 1, expand partial function
    *
diff --git a/tests/neg/i7746.scala b/tests/neg/i7746.scala
index 502861c2ffbb..f0990e86d94a 100644
--- a/tests/neg/i7746.scala
+++ b/tests/neg/i7746.scala
@@ -1,3 +1,3 @@
 class A {
-    def foo = (x : Int, y => x) => () // error: not a gel formal parameter
+    def foo = (x : Int, y => x) => () // error // error
 }
\ No newline at end of file
diff --git a/tests/neg/i9299.scala b/tests/neg/i9299.scala
index 119b268a842e..6c23d11553ff 100644
--- a/tests/neg/i9299.scala
+++ b/tests/neg/i9299.scala
@@ -1,4 +1,4 @@
-type F <: F = 1 match { // error: Recursion limit exceeded.
-  case _ => foo.foo // error: Recursion limit exceeded.
+type F <: F = 1 match { // error
+  case _ => foo.foo // error // error
 }
 def foo(a: Int): Unit = ???

From ea313fdafe47a0abf372746fba5dbfb3601c69fc Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 17 Aug 2021 11:47:25 +0200
Subject: [PATCH 25/25] Skip closure nodes when checking conformance

---
 compiler/src/dotty/tools/dotc/transform/Recheck.scala | 4 +++-
 tests/neg-custom-args/captures/boxmap.check           | 2 +-
 tests/neg-custom-args/captures/capt1.check            | 6 +++---
 tests/neg-custom-args/captures/try.check              | 6 +++---
 4 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index c3be1fc86ef3..bff5a4442100 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -310,7 +310,9 @@ abstract class Recheck extends Phase, IdentityDenotTransformer:
     end recheck
 
     def checkConforms(tpe: Type, pt: Type, tree: Tree)(using Context): Unit = tree match
-      case _: DefTree | EmptyTree | _: TypeTree =>
+      case _: DefTree | EmptyTree | _: TypeTree | _: Closure =>
+        // Don't report closure nodes, since their span is a point; wait instead
+        // for enclosing block to preduce an error
       case _ =>
         val actual = tpe.widenExpr
         val expected = pt.widenExpr
diff --git a/tests/neg-custom-args/captures/boxmap.check b/tests/neg-custom-args/captures/boxmap.check
index 5da51abd30d1..11be4ef33da8 100644
--- a/tests/neg-custom-args/captures/boxmap.check
+++ b/tests/neg-custom-args/captures/boxmap.check
@@ -1,4 +1,4 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boxmap.scala:14:5 ----------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boxmap.scala:14:2 ----------------------------------------
 14 |  () => b[Box[B]]((x: A) => box(f(x)))  // error
    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |  Found:    {f} () => Box[B]
diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check
index df48efae1551..b486fabf61fd 100644
--- a/tests/neg-custom-args/captures/capt1.check
+++ b/tests/neg-custom-args/captures/capt1.check
@@ -1,11 +1,11 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:3:5 ------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:3:2 ------------------------------------------
 3 |  () => if x == null then y else y  // error
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |  Found:    {x} () => C
   |  Required: () => C
 
 longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:6:5 ------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:6:2 ------------------------------------------
 6 |  () => if x == null then y else y  // error
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |  Found:    {x} () => C
@@ -33,7 +33,7 @@ longer explanation available when compiling with `-explain`
    |                                        Required: A
 
 longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:32:27 ----------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:32:24 ----------------------------------------
 32 |  val z2 = h[() => Cap](() => x)(() => C())  // error
    |                        ^^^^^^^
    |                        Found:    {x} () => Cap
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index da490586d115..7db077311085 100644
--- a/tests/neg-custom-args/captures/try.check
+++ b/tests/neg-custom-args/captures/try.check
@@ -1,11 +1,11 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:35 ------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:32 ------------------------------------------
 29 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)  // error
    |                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |                                Found:    {x} () => Nothing
    |                                Required: () => Nothing
 
 longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:36:9 -------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:36:6 -------------------------------------------
 36 |      () => // error
    |      ^
    |      Found:    {x} () => Int
@@ -14,7 +14,7 @@ longer explanation available when compiling with `-explain`
 38 |        22
 
 longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:47:7 -------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:47:4 -------------------------------------------
 47 |    () => // error
    |    ^
    |    Found:    {x} () => Int