From 1d2e16e4f04096deec3234fabd7f81ef4cd17ff8 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:09:17 +0100
Subject: [PATCH 01/37] Bugfix: generate same kind of MethodType when capture
 checking anonymous functions

---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 3 ++-
 tests/pos/byname-purefuns-adapt/A_1.scala            | 3 ++-
 tests/pos/byname-purefuns-adapt/B_2.scala            | 3 +++
 3 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index cf1d4266e89b..a17beca5af78 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -452,9 +452,10 @@ class CheckCaptures extends Recheck, SymTransformer:
                 tpt.rememberTypeAlways(pformal)
               }
               // Next, install a new completer reflecting the new parameters for the anonymous method
+              val mt = meth.info.asInstanceOf[MethodType]
               val completer = new LazyType:
                 def complete(denot: SymDenotation)(using Context) =
-                  denot.info = MethodType(ptformals, mdef.tpt.knownType)
+                  denot.info = mt.companion(ptformals, mdef.tpt.knownType)
                     .showing(i"simplify info of $meth to $result", capt)
                   recheckDef(mdef, meth)
               meth.copySymDenotation(info = completer, initFlags = meth.flags &~ Touched)
diff --git a/tests/pos/byname-purefuns-adapt/A_1.scala b/tests/pos/byname-purefuns-adapt/A_1.scala
index c98664a91a71..441dc24a8ef0 100644
--- a/tests/pos/byname-purefuns-adapt/A_1.scala
+++ b/tests/pos/byname-purefuns-adapt/A_1.scala
@@ -1,3 +1,4 @@
+class Ctx
 object A:
   def f(x: => Int) = ()
-
+  def g(op: Ctx ?=> Int) = op(using Ctx())
diff --git a/tests/pos/byname-purefuns-adapt/B_2.scala b/tests/pos/byname-purefuns-adapt/B_2.scala
index 4bcaa2e6c69b..842161c0fcbd 100644
--- a/tests/pos/byname-purefuns-adapt/B_2.scala
+++ b/tests/pos/byname-purefuns-adapt/B_2.scala
@@ -1,5 +1,8 @@
 import language.experimental.captureChecking
 object B:
   def test(x: => Int) = A.f(x)
+  def opp(using Ctx) = 0
+  A.g(opp)
+
 
 

From 5496ef1f02f06e32fa4ff81598f997575e23f0ae Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:12:16 +0100
Subject: [PATCH 02/37] Bugfix: Avoid crash in cc/Synthetics

The crash can happen if we compile some modules without capture checking when
other modules are compiled in the same run with capture checking.
---
 .../src/dotty/tools/dotc/cc/Synthetics.scala    | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Synthetics.scala b/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
index e8f7fd502baa..c94b1cd383e2 100644
--- a/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
@@ -141,13 +141,16 @@ object Synthetics:
   /** Drop added capture information from the type of an `unapply` */
   private def dropUnapplyCaptures(info: Type)(using Context): Type = info match
     case info: MethodType =>
-      val CapturingType(oldParamInfo, _) :: Nil = info.paramInfos: @unchecked
-      def oldResult(tp: Type): Type = tp match
-        case tp: MethodOrPoly =>
-          tp.derivedLambdaType(resType = oldResult(tp.resType))
-        case CapturingType(tp, _) =>
-          tp
-      info.derivedLambdaType(paramInfos = oldParamInfo :: Nil, resType = oldResult(info.resType))
+      info.paramInfos match
+        case CapturingType(oldParamInfo, _) :: Nil =>
+          def oldResult(tp: Type): Type = tp match
+            case tp: MethodOrPoly =>
+              tp.derivedLambdaType(resType = oldResult(tp.resType))
+            case CapturingType(tp, _) =>
+              tp
+          info.derivedLambdaType(paramInfos = oldParamInfo :: Nil, resType = oldResult(info.resType))
+        case _ =>
+          info
     case info: PolyType =>
       info.derivedLambdaType(resType = dropUnapplyCaptures(info.resType))
 

From 65d8b19a4fad439a2c89ae464d82a7fd877cb721 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:13:32 +0100
Subject: [PATCH 03/37] Performance: Run capture checking transformers only if
 cc is enabled somewhere

---
 compiler/src/dotty/tools/dotc/Run.scala         | 13 ++++++++++++-
 .../src/dotty/tools/dotc/config/Feature.scala   | 17 +++++++++++++++--
 compiler/src/dotty/tools/dotc/core/Phases.scala |  8 ++++++++
 3 files changed, 35 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/Run.scala b/compiler/src/dotty/tools/dotc/Run.scala
index 022ffbed5408..f7a08d1640ee 100644
--- a/compiler/src/dotty/tools/dotc/Run.scala
+++ b/compiler/src/dotty/tools/dotc/Run.scala
@@ -164,10 +164,15 @@ class Run(comp: Compiler, ictx: Context) extends ImplicitRunInfo with Constraint
   private var finalizeActions = mutable.ListBuffer[() => Unit]()
 
   /** Will be set to true if any of the compiled compilation units contains
-   *  a pureFunctions or captureChecking language import.
+   *  a pureFunctions language import.
    */
   var pureFunsImportEncountered = false
 
+  /** Will be set to true if any of the compiled compilation units contains
+   *  a captureChecking language import.
+   */
+  var ccImportEncountered = false
+
   def compile(files: List[AbstractFile]): Unit =
     try
       val sources = files.map(runContext.getSource(_))
@@ -229,6 +234,7 @@ class Run(comp: Compiler, ictx: Context) extends ImplicitRunInfo with Constraint
     def runPhases(using Context) = {
       var lastPrintedTree: PrintedTree = NoPrintedTree
       val profiler = ctx.profiler
+      var phasesWereAdjusted = false
 
       for (phase <- ctx.base.allPhases)
         if (phase.isRunnable)
@@ -247,6 +253,11 @@ class Run(comp: Compiler, ictx: Context) extends ImplicitRunInfo with Constraint
               Stats.record(s"retained typed trees at end of $phase", unit.tpdTree.treeSize)
             ctx.typerState.gc()
           }
+          if !phasesWereAdjusted then
+            phasesWereAdjusted = true
+            if !Feature.ccEnabledSomewhere then
+              ctx.base.unlinkPhaseAsDenotTransformer(Phases.checkCapturesPhase.prev)
+              ctx.base.unlinkPhaseAsDenotTransformer(Phases.checkCapturesPhase)
 
       profiler.finished()
     }
diff --git a/compiler/src/dotty/tools/dotc/config/Feature.scala b/compiler/src/dotty/tools/dotc/config/Feature.scala
index d836716c3901..e7117f542384 100644
--- a/compiler/src/dotty/tools/dotc/config/Feature.scala
+++ b/compiler/src/dotty/tools/dotc/config/Feature.scala
@@ -79,19 +79,27 @@ object Feature:
 
   def scala2ExperimentalMacroEnabled(using Context) = enabled(scala2macros)
 
+  /** Is pureFunctions enabled for this compilation unit? */
   def pureFunsEnabled(using Context) =
     enabledBySetting(pureFunctions)
     || ctx.compilationUnit.knowsPureFuns
     || ccEnabled
 
+  /** Is captureChecking enabled for this compilation unit? */
   def ccEnabled(using Context) =
     enabledBySetting(captureChecking)
     || ctx.compilationUnit.needsCaptureChecking
 
+  /** Is pureFunctions enabled for any of the currently compiled compilation units? */
   def pureFunsEnabledSomewhere(using Context) =
     enabledBySetting(pureFunctions)
-    || enabledBySetting(captureChecking)
     || ctx.run != null && ctx.run.nn.pureFunsImportEncountered
+    || ccEnabledSomewhere
+
+  /** Is captureChecking enabled for any of the currently compiled compilation units? */
+  def ccEnabledSomewhere(using Context) =
+    enabledBySetting(captureChecking)
+    || ctx.run != null && ctx.run.nn.ccImportEncountered
 
   def sourceVersionSetting(using Context): SourceVersion =
     SourceVersion.valueOf(ctx.settings.source.value)
@@ -143,6 +151,11 @@ object Feature:
   def isExperimentalEnabled(using Context): Boolean =
     Properties.experimental && !ctx.settings.YnoExperimental.value
 
+  /** Handle language import `import language.<prefix>.<imported>` if it is one
+   *  of the global imports `pureFunctions` or `captureChecking`. In this case
+   *  make the compilation unit's and current run's fields accordingly.
+   *  @return true iff import that was handled
+   */
   def handleGlobalLanguageImport(prefix: TermName, imported: Name)(using Context): Boolean =
     val fullFeatureName = QualifiedName(prefix, imported.asTermName)
     if fullFeatureName == pureFunctions then
@@ -151,7 +164,7 @@ object Feature:
       true
     else if fullFeatureName == captureChecking then
       ctx.compilationUnit.needsCaptureChecking = true
-      if ctx.run != null then ctx.run.nn.pureFunsImportEncountered = true
+      if ctx.run != null then ctx.run.nn.ccImportEncountered = true
       true
     else
       false
diff --git a/compiler/src/dotty/tools/dotc/core/Phases.scala b/compiler/src/dotty/tools/dotc/core/Phases.scala
index b4a2dcac1b85..205554e418ed 100644
--- a/compiler/src/dotty/tools/dotc/core/Phases.scala
+++ b/compiler/src/dotty/tools/dotc/core/Phases.scala
@@ -197,6 +197,14 @@ object Phases {
       config.println(s"nextDenotTransformerId = ${nextDenotTransformerId.toList}")
     }
 
+    /** Unlink `phase` from Denot transformer chain. This means that
+     *  any denotation transformer defined by the phase will not be executed.
+     */
+    def unlinkPhaseAsDenotTransformer(phase: Phase)(using Context) =
+      for i <- 0 until nextDenotTransformerId.length do
+        if nextDenotTransformerId(i) == phase.id then
+          nextDenotTransformerId(i) = nextDenotTransformerId(phase.id + 1)
+
     private var myParserPhase: Phase = _
     private var myTyperPhase: Phase = _
     private var myPostTyperPhase: Phase = _

From 2066efa35fa8b35655718461686fee7c470dfbe6 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:15:27 +0100
Subject: [PATCH 04/37] Enhancement: Revert automatic boxing of universal
 variable initializers

Often, the box point is more interesting than the unbox point. It's when unsafe boxing
a variable's RHS that we have to make usre manually that no capability escapes.
---
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala | 17 +----------------
 tests/pos-custom-args/captures/vars1.scala      | 10 +++-------
 2 files changed, 4 insertions(+), 23 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index a17beca5af78..d19d3d981d35 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -464,25 +464,10 @@ class CheckCaptures extends Recheck, SymTransformer:
         case _ =>
       super.recheckBlock(block, pt)
 
-    /** If `rhsProto` has `*` as its capture set, wrap `rhs` in a `unsafeBox`.
-     *  Used to infer `unsafeBox` for expressions that get assigned to variables
-     *  that have universal capture set.
-     */
-    def maybeBox(rhs: Tree, rhsProto: Type)(using Context): Tree =
-      if rhsProto.captureSet.isUniversal then
-        ref(defn.Caps_unsafeBox).appliedToType(rhsProto).appliedTo(rhs)
-      else rhs
-
-    override def recheckAssign(tree: Assign)(using Context): Type =
-      val rhsProto = recheck(tree.lhs).widen
-      recheck(maybeBox(tree.rhs, rhsProto), rhsProto)
-      defn.UnitType
-
     override def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Unit =
       try
         if !sym.is(Module) then // Modules are checked by checking the module class
-          if sym.is(Mutable) then recheck(maybeBox(tree.rhs, sym.info), sym.info)
-          else super.recheckValDef(tree, sym)
+          super.recheckValDef(tree, sym)
       finally
         if !sym.is(Param) then
           // Parameters with inferred types belong to anonymous methods. We need to wait
diff --git a/tests/pos-custom-args/captures/vars1.scala b/tests/pos-custom-args/captures/vars1.scala
index 8c2f2cb8b5d5..53a770563985 100644
--- a/tests/pos-custom-args/captures/vars1.scala
+++ b/tests/pos-custom-args/captures/vars1.scala
@@ -11,15 +11,11 @@ object Test:
 
   def defaultIncompleteHandler1(): ErrorHandler = ???
   val defaultIncompleteHandler2: ErrorHandler = ???
-  var incompleteHandler1: ErrorHandler = defaultIncompleteHandler1()
-  var incompleteHandler2: ErrorHandler = defaultIncompleteHandler2
-  var incompleteHandler3: ErrorHandler = defaultIncompleteHandler1().unsafeBox
-  var incompleteHandler4: ErrorHandler = defaultIncompleteHandler2.unsafeBox
-  private var incompleteHandler5 = defaultIncompleteHandler1()
-  private var incompleteHandler6 = defaultIncompleteHandler2
+  var incompleteHandler1: ErrorHandler = defaultIncompleteHandler1().unsafeBox
+  var incompleteHandler2: ErrorHandler = defaultIncompleteHandler2.unsafeBox
   private var incompleteHandler7 = defaultIncompleteHandler1().unsafeBox
   private var incompleteHandler8 = defaultIncompleteHandler2.unsafeBox
 
-  incompleteHandler1 = defaultIncompleteHandler2
+  incompleteHandler1 = defaultIncompleteHandler2.unsafeBox
   incompleteHandler1 = defaultIncompleteHandler2.unsafeBox
   val saved = incompleteHandler1.unsafeUnbox

From f17fff9311ff77acf19bd5cfa96f464dbb32ddbc Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:16:59 +0100
Subject: [PATCH 05/37] Enhancement: Special treatment of arguments of
 `asInstanceOf`

Don't subject them to box adaptation.
---
 compiler/src/dotty/tools/dotc/transform/Recheck.scala | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 6d783854ae35..c62b39a9e0c8 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -147,7 +147,10 @@ abstract class Recheck extends Phase, SymTransformer:
 
     def recheckSelect(tree: Select, pt: Type)(using Context): Type =
       val Select(qual, name) = tree
-      recheckSelection(tree, recheck(qual, AnySelectionProto).widenIfUnstable, name, pt)
+      val proto =
+        if tree.symbol == defn.Any_asInstanceOf then WildcardType
+        else AnySelectionProto
+      recheckSelection(tree, recheck(qual, proto).widenIfUnstable, name, pt)
 
     def recheckSelection(tree: Select, qualType: Type, name: Name,
         sharpen: Denotation => Denotation)(using Context): Type =

From feb4c7cb7fdb2b2446923c54ffebbb57ad9a6d05 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:17:33 +0100
Subject: [PATCH 06/37] Enhancement: Assume special capturing types for `eq`
 and `ne`

They take a `{*} Object` instead of an `Object` parameter.
---
 .../src/dotty/tools/dotc/cc/Synthetics.scala     | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Synthetics.scala b/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
index c94b1cd383e2..dacbd27e0f35 100644
--- a/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
@@ -31,10 +31,12 @@ object Synthetics:
    *  The types of these symbols are transformed in a special way without
    *  looking at the definitions's RHS
    */
-  def needsTransform(sym: SymDenotation)(using Context): Boolean =
-    isSyntheticCopyMethod(sym)
-    || isSyntheticCompanionMethod(sym, nme.apply, nme.unapply)
-    || isSyntheticCopyDefaultGetterMethod(sym)
+  def needsTransform(symd: SymDenotation)(using Context): Boolean =
+    isSyntheticCopyMethod(symd)
+    || isSyntheticCompanionMethod(symd, nme.apply, nme.unapply)
+    || isSyntheticCopyDefaultGetterMethod(symd)
+    || (symd.symbol eq defn.Object_eq)
+    || (symd.symbol eq defn.Object_ne)
 
   /** Method is excluded from regular capture checking.
    *  Excluded are synthetic class members
@@ -166,7 +168,9 @@ object Synthetics:
       sym.copySymDenotation(info = addUnapplyCaptures(sym.info))
     case nme.apply | nme.copy =>
       sym.copySymDenotation(info = addCaptureDeps(sym.info))
-
+    case n if n == nme.eq || n == nme.ne =>
+      sym.copySymDenotation(info =
+        MethodType(defn.ObjectType.capturing(CaptureSet.universal) :: Nil, defn.BooleanType))
 
   /** If `sym` refers to a synthetic apply, unapply, copy, or copy default getter method
    *  of a case class, transform it back to what it was before the CC phase.
@@ -179,5 +183,7 @@ object Synthetics:
       sym.copySymDenotation(info = dropUnapplyCaptures(sym.info))
     case nme.apply | nme.copy =>
       sym.copySymDenotation(info = dropCaptureDeps(sym.info))
+    case n if n == nme.eq || n == nme.ne =>
+      sym.copySymDenotation(info = defn.methOfAnyRef(defn.BooleanType))
 
 end Synthetics
\ No newline at end of file

From 96643ef3768f8a76efc208a881676f7e16b64b73 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:18:32 +0100
Subject: [PATCH 07/37] Bugfix: Allow all private definitions to have inferred
 types

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

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index d19d3d981d35..ea444bbe5847 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -871,12 +871,13 @@ class CheckCaptures extends Recheck, SymTransformer:
           val isLocal =
             sym.owner.ownersIterator.exists(_.isTerm)
             || sym.accessBoundary(defn.RootClass).isContainedIn(sym.topLevelClass)
-
-          // The following classes of definitions need explicit capture types ...
-          if !isLocal                            // ... since external capture types are not inferred
-            || sym.owner.is(Trait)               // ... since we do OverridingPairs checking before capture inference
-            || sym.allOverriddenSymbols.nonEmpty // ... since we do override checking before capture inference
-          then
+          def canUseInferred =            // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
+            sym.is(Private)                         // private symbols can always have inferred types
+            ||                                      // non-local symbols cannot have inferred types since external capture types are not inferred
+              isLocal                               // local symbols still need an explicit types if
+              && !sym.owner.is(Trait)               //   - they are defined in a trait, since we do OverridingPairs checking before capture inference
+              && !sym.allOverriddenSymbols.nonEmpty //   - they override some other symbol, since we do override checking before capture inference
+          if !canUseInferred then
             val inferred = t.tpt.knownType
             def checkPure(tp: Type) = tp match
               case CapturingType(_, refs) if !refs.elems.isEmpty =>

From 824580e55985adcc5d1d5e873dea8be5202f333d Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:20:17 +0100
Subject: [PATCH 08/37] Bugfix: Avoid spurious check in RefChecks

---
 .../dotty/tools/dotc/typer/RefChecks.scala    | 22 ++++++++++---------
 .../pos-custom-args/captures/overrides.scala  | 12 ----------
 .../captures/overrides/A.scala                |  4 ++++
 .../captures/overrides/B.scala                |  6 +++++
 4 files changed, 22 insertions(+), 22 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/overrides/A.scala
 create mode 100644 tests/pos-custom-args/captures/overrides/B.scala

diff --git a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
index 1aa53d866b5e..7e65f0c5085b 100644
--- a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
+++ b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
@@ -774,17 +774,19 @@ object RefChecks {
 
         // For each member, check that the type of its symbol, as seen from `self`
         // can override the info of this member
-        for (name <- membersToCheck)
-          for (mbrd <- self.member(name).alternatives) {
-            val mbr = mbrd.symbol
-            val mbrType = mbr.info.asSeenFrom(self, mbr.owner)
-            if (!mbrType.overrides(mbrd.info, relaxedCheck = false, matchLoosely = true))
-              report.errorOrMigrationWarning(
-                em"""${mbr.showLocated} is not a legal implementation of `$name` in $clazz
-                    |  its type             $mbrType
-                    |  does not conform to  ${mbrd.info}""",
-                (if (mbr.owner == clazz) mbr else clazz).srcPos, from = `3.0`)
+        withMode(Mode.IgnoreCaptures) {
+          for (name <- membersToCheck)
+            for (mbrd <- self.member(name).alternatives) {
+              val mbr = mbrd.symbol
+              val mbrType = mbr.info.asSeenFrom(self, mbr.owner)
+              if (!mbrType.overrides(mbrd.info, relaxedCheck = false, matchLoosely = true))
+                report.errorOrMigrationWarning(
+                  em"""${mbr.showLocated} is not a legal implementation of `$name` in $clazz
+                      |  its type             $mbrType
+                      |  does not conform to  ${mbrd.info}""",
+                  (if (mbr.owner == clazz) mbr else clazz).srcPos, from = `3.0`)
           }
+        }
       }
 
       /** Check that inheriting a case class does not constitute a variant refinement
diff --git a/tests/pos-custom-args/captures/overrides.scala b/tests/pos-custom-args/captures/overrides.scala
index 66f19726ffa7..7e70afe7a327 100644
--- a/tests/pos-custom-args/captures/overrides.scala
+++ b/tests/pos-custom-args/captures/overrides.scala
@@ -12,15 +12,3 @@ class Bar extends Foo:
 class Baz extends Bar:
   override def foo = () => println("baz")
   override def bar = "baz"
-  //override def toString = bar
-
-abstract class Message:
-  protected def msg: String
-  override def toString = msg
-
-abstract class SyntaxMsg extends Message
-
-class CyclicInheritance extends SyntaxMsg:
-  def msg = "cyclic"
-
-
diff --git a/tests/pos-custom-args/captures/overrides/A.scala b/tests/pos-custom-args/captures/overrides/A.scala
new file mode 100644
index 000000000000..6a81f8562164
--- /dev/null
+++ b/tests/pos-custom-args/captures/overrides/A.scala
@@ -0,0 +1,4 @@
+abstract class Message:
+  lazy val message: String = ???
+  def rawMessage = message
+
diff --git a/tests/pos-custom-args/captures/overrides/B.scala b/tests/pos-custom-args/captures/overrides/B.scala
new file mode 100644
index 000000000000..ce4a3f20f1d2
--- /dev/null
+++ b/tests/pos-custom-args/captures/overrides/B.scala
@@ -0,0 +1,6 @@
+
+abstract class SyntaxMsg extends Message
+
+class CyclicInheritance extends SyntaxMsg
+
+

From 7740fb7a1e3001ae0ed6a02c825fdb4fa459b2aa Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:22:08 +0100
Subject: [PATCH 09/37] Bugfix: More lenient definition when an inferred type
 is OK for visible definition

We now allow an inferred type of the form `{C.this} T` if `C` is a pure class.
This is OK since such a type is equivalent to `T`.
---
 compiler/src/dotty/tools/dotc/cc/CaptureOps.scala    | 11 +++++++++++
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala |  7 ++++++-
 compiler/test/dotc/pos-test-pickling.blacklist       |  1 -
 tests/pos-custom-args/captures/capt-test.scala       |  3 +++
 tests/pos-custom-args/captures/selftypes.scala       | 10 ++++++++++
 5 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/selftypes.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 3261cb1d90f8..1c3b54bb4b2e 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -168,6 +168,17 @@ extension (tp: Type)
 
 extension (sym: Symbol)
 
+  /** A class is pure if one of its base types has an explicitly declared self type
+   *  with an empty capture set.
+   */
+  def isPureClass(using Context): Boolean = sym match
+    case cls: ClassSymbol =>
+      cls.baseClasses.exists(bc =>
+        val selfType = bc.givenSelfType
+        selfType.exists && selfType.captureSet.isAlwaysEmpty)
+    case _ =>
+      false
+
   /** Does this symbol allow results carrying the universal capability?
    *  Currently this is true only for function type applies (since their
    *  results are unboxed) and `erasedValue` since this function is magic in
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index ea444bbe5847..a80e37d646e8 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -877,10 +877,15 @@ class CheckCaptures extends Recheck, SymTransformer:
               isLocal                               // local symbols still need an explicit types if
               && !sym.owner.is(Trait)               //   - they are defined in a trait, since we do OverridingPairs checking before capture inference
               && !sym.allOverriddenSymbols.nonEmpty //   - they override some other symbol, since we do override checking before capture inference
+          def isNotPureThis(ref: CaptureRef) = ref match {
+            case ref: ThisType => !ref.cls.isPureClass
+            case _ => true
+          }
           if !canUseInferred then
             val inferred = t.tpt.knownType
             def checkPure(tp: Type) = tp match
-              case CapturingType(_, refs) if !refs.elems.isEmpty =>
+              case CapturingType(_, refs)
+              if !refs.elems.filter(isNotPureThis).isEmpty =>
                 val resultStr = if t.isInstanceOf[DefDef] then " result" else ""
                 report.error(
                   em"""Non-local $sym cannot have an inferred$resultStr type
diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist
index a7d8778d4c61..30126f07b49a 100644
--- a/compiler/test/dotc/pos-test-pickling.blacklist
+++ b/compiler/test/dotc/pos-test-pickling.blacklist
@@ -84,7 +84,6 @@ boxmap-paper.scala
 # Function types print differnt after unpickling since test mispredicts Feature.preFundsEnabled
 caps-universal.scala
 
-
 # GADT cast applied to singleton type difference
 i4176-gadt.scala
 
diff --git a/tests/pos-custom-args/captures/capt-test.scala b/tests/pos-custom-args/captures/capt-test.scala
index 6ee0d2a4d9f4..c61577e96eb1 100644
--- a/tests/pos-custom-args/captures/capt-test.scala
+++ b/tests/pos-custom-args/captures/capt-test.scala
@@ -21,6 +21,9 @@ def map[A, B](f: A => B)(xs: LIST[A]): LIST[B] =
 class C
 type Cap = {*} C
 
+class Foo(x: Cap):
+  this: {x} Foo =>
+
 def test(c: Cap, d: Cap) =
   def f(x: Cap): Unit = if c == x then ()
   def g(x: Cap): Unit = if d == x then ()
diff --git a/tests/pos-custom-args/captures/selftypes.scala b/tests/pos-custom-args/captures/selftypes.scala
new file mode 100644
index 000000000000..f5eb1980d060
--- /dev/null
+++ b/tests/pos-custom-args/captures/selftypes.scala
@@ -0,0 +1,10 @@
+  trait A:
+    self: A =>
+    def foo: Int
+
+  abstract class B extends A:
+    def foo: Int
+
+  class C extends B:
+    def foo = 1
+    def derived = this

From 4b981555e3b51e967a51d75a5b70b62cf54502a7 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:22:57 +0100
Subject: [PATCH 10/37] Enhancement: Don't count @constructorOnly parameters
 towards the self type of a class

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

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index a80e37d646e8..b1a11d1e8e1d 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -489,7 +489,8 @@ class CheckCaptures extends Recheck, SymTransformer:
     /** Class-specific capture set relations:
      *   1. The capture set of a class includes the capture sets of its parents.
      *   2. The capture set of the self type of a class includes the capture set of the class.
-     *   3. The capture set of the self type of a class includes the capture set of every class parameter.
+     *   3. The capture set of the self type of a class includes the capture set of every class parameter,
+     *      unless the parameter is marked @constructorOnly.
      */
     override def recheckClassDef(tree: TypeDef, impl: Template, cls: ClassSymbol)(using Context): Type =
       val saved = curEnv
@@ -501,7 +502,8 @@ class CheckCaptures extends Recheck, SymTransformer:
         val thisSet = cls.classInfo.selfType.captureSet.withDescription(i"of the self type of $cls")
         checkSubset(localSet, thisSet, tree.srcPos) // (2)
         for param <- cls.paramGetters do
-          checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3)
+          if !param.hasAnnotation(defn.ConstructorOnlyAnnot) then
+            checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3)
         super.recheckClassDef(tree, impl, cls)
       finally
         curEnv = saved

From b21867f77e38cf826ea421dacf50493c57b0743f Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:25:34 +0100
Subject: [PATCH 11/37] Enhancement: More lenient check for inferred self types

An inferred self type in a non-sealed class is now OK if it is the same
as an explicit self type in a base class.
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 16 ++++++--
 .../dotty/tools/dotc/typer/RefChecks.scala    | 38 +++++++++++++------
 .../pos-custom-args/captures/selftypes.scala  |  5 +++
 3 files changed, 44 insertions(+), 15 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index b1a11d1e8e1d..12b5dbac8a16 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -10,7 +10,7 @@ import config.Printers.{capt, recheckr}
 import config.{Config, Feature}
 import ast.{tpd, untpd, Trees}
 import Trees.*
-import typer.RefChecks.{checkAllOverrides, checkParents}
+import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents}
 import util.{SimpleIdentitySet, EqHashMap, SrcPos}
 import transform.SymUtils.*
 import transform.{Recheck, PreRecheck}
@@ -833,13 +833,21 @@ class CheckCaptures extends Recheck, SymTransformer:
           cls => !parentTrees(cls).exists(ptree => parentTrees.contains(ptree.tpe.classSymbol))
         }
         assert(roots.nonEmpty)
-        for root <- roots do
-          checkParents(root, parentTrees(root))
+        for case root: ClassSymbol <- roots do
+          checkSelfAgainstParents(root, root.baseClasses)
           val selfType = root.asClass.classInfo.selfType
           interpolator(startingVariance = -1).traverse(selfType)
           if !root.isEffectivelySealed  then
+            def matchesExplicitRefsInBaseClass(refs: CaptureSet, cls: ClassSymbol): Boolean =
+              cls.baseClasses.tail.exists { psym =>
+                val selfType = psym.asClass.givenSelfType
+                selfType.exists && selfType.captureSet.elems == refs.elems
+              }
             selfType match
-              case CapturingType(_, refs: CaptureSet.Var) if !refs.isUniversal =>
+              case CapturingType(_, refs: CaptureSet.Var)
+              if !refs.isUniversal && !matchesExplicitRefsInBaseClass(refs, root) =>
+                // Forbid inferred self types unless they are already implied by an explicit
+                // self type in a parent.
                 report.error(
                   i"""$root needs an explicitly declared self type since its
                      |inferred self type $selfType
diff --git a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
index 7e65f0c5085b..5d0a9f55395b 100644
--- a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
+++ b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
@@ -91,24 +91,40 @@ object RefChecks {
       cls.thisType
   }
 
+  /**  - Check that self type of `cls` conforms to self types of all `parents` as seen from
+   *     `cls.thisType`
+   *   - If self type of `cls` is explicit, check that it conforms to the self types
+   *     of all its class symbols.
+   *  @param deep  If true and a self type of a parent is not given explicitly, recurse to
+   *               check against the parents of the parent. This is needed when capture checking,
+   *               since we assume (& check) that the capture set of an inferred self type
+   *               is the intersection of the capture sets of all its parents
+   */
+  def checkSelfAgainstParents(cls: ClassSymbol, parents: List[Symbol])(using Context): Unit =
+    val cinfo = cls.classInfo
+
+    def checkSelfConforms(other: ClassSymbol, category: String, relation: String) =
+      val otherSelf = other.declaredSelfTypeAsSeenFrom(cls.thisType)
+      if otherSelf.exists then
+        if !(cinfo.selfType <:< otherSelf) then
+          report.error(DoesNotConformToSelfType(category, cinfo.selfType, cls, otherSelf, relation, other),
+            cls.srcPos)
+
+    for psym <- parents do
+      checkSelfConforms(psym.asClass, "illegal inheritance", "parent")
+    for reqd <- cls.asClass.givenSelfType.classSymbols do
+      if reqd != cls then
+        checkSelfConforms(reqd, "missing requirement", "required")
+  end checkSelfAgainstParents
+
   /** Check that self type of this class conforms to self types of parents
    *  and required classes. Also check that only `enum` constructs extend
    *  `java.lang.Enum` and no user-written class extends ContextFunctionN.
    */
   def checkParents(cls: Symbol, parentTrees: List[Tree])(using Context): Unit = cls.info match {
     case cinfo: ClassInfo =>
-      def checkSelfConforms(other: ClassSymbol, category: String, relation: String) = {
-        val otherSelf = other.declaredSelfTypeAsSeenFrom(cls.thisType)
-        if otherSelf.exists && !(cinfo.selfType <:< otherSelf) then
-          report.error(DoesNotConformToSelfType(category, cinfo.selfType, cls, otherSelf, relation, other),
-            cls.srcPos)
-      }
       val psyms = cls.asClass.parentSyms
-      for (psym <- psyms)
-        checkSelfConforms(psym.asClass, "illegal inheritance", "parent")
-      for reqd <- cinfo.cls.givenSelfType.classSymbols do
-        if reqd != cls then
-          checkSelfConforms(reqd, "missing requirement", "required")
+      checkSelfAgainstParents(cls.asClass, psyms)
 
       def isClassExtendingJavaEnum =
         !cls.isOneOf(Enum | Trait) && psyms.contains(defn.JavaEnumClass)
diff --git a/tests/pos-custom-args/captures/selftypes.scala b/tests/pos-custom-args/captures/selftypes.scala
index f5eb1980d060..c1b8eefce506 100644
--- a/tests/pos-custom-args/captures/selftypes.scala
+++ b/tests/pos-custom-args/captures/selftypes.scala
@@ -1,3 +1,4 @@
+  import annotation.constructorOnly
   trait A:
     self: A =>
     def foo: Int
@@ -8,3 +9,7 @@
   class C extends B:
     def foo = 1
     def derived = this
+
+  class D(@constructorOnly op: Int => Int) extends C:
+    val x = 1//op(1)
+

From 4b97e1d1a7e74659342130f14b0485eafe024cfc Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:33:37 +0100
Subject: [PATCH 12/37] Enhancement: Add missing case for comparison of
 capturing types.

Add a case for cases like

    x.type <:< {r} (A | x.type)

where `x` captures `r`.

# Conflicts:
#	tests/pos-with-compiler-cc/dotc/core/Types.scala
---
 compiler/src/dotty/tools/dotc/core/TypeComparer.scala |  6 +++++-
 tests/pos-custom-args/captures/cmp-singleton.scala    | 10 ++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 tests/pos-custom-args/captures/cmp-singleton.scala

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 283a7e3a474e..b50d524cd4a0 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -826,7 +826,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             if refs1.isAlwaysEmpty then recur(tp1, parent2)
             else subCaptures(refs1, refs2, frozenConstraint).isOK
               && sameBoxed(tp1, tp2, refs1)
-              && recur(tp1.widen.stripCapturing, parent2)
+              && (recur(tp1.widen.stripCapturing, parent2)
+                 || tp1.isInstanceOf[SingletonType] && recur(tp1, parent2)
+                    // this alternative is needed in case the right hand side is a
+                    // capturing type that contains the lhs as an |-alternative.
+                 )
           catch case ex: AssertionError =>
             println(i"assertion failed while compare captured $tp1 <:< $tp2")
             throw ex
diff --git a/tests/pos-custom-args/captures/cmp-singleton.scala b/tests/pos-custom-args/captures/cmp-singleton.scala
new file mode 100644
index 000000000000..45b4009f5e89
--- /dev/null
+++ b/tests/pos-custom-args/captures/cmp-singleton.scala
@@ -0,0 +1,10 @@
+class Denotation
+abstract class SingleDenotation extends Denotation
+def goRefined: Denotation =
+  val foo: Denotation = ???
+  val joint = foo
+  joint match
+    case joint: SingleDenotation =>
+      joint
+    case _ =>
+      joint
\ No newline at end of file

From 7f0e259d45d125d9b3797480af172ec3dcf28c6f Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:34:22 +0100
Subject: [PATCH 13/37] Enhancement: Force all exception classes to be pure

Impure exceptions can't be thrown anyway since `throw` takes a
pure `Throwable` as operand.

The change avoids having to declare explicit pure self types for
exception classes.
---
 compiler/src/dotty/tools/dotc/cc/CaptureSet.scala   |  5 +++++
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala     |  2 ++
 .../captures/exception-definitions.check            | 13 +++++++++++++
 .../captures/exception-definitions.scala            | 10 ++++++++++
 4 files changed, 30 insertions(+)
 create mode 100644 tests/neg-custom-args/captures/exception-definitions.check
 create mode 100644 tests/neg-custom-args/captures/exception-definitions.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index d3e32ac538a4..694c5140f203 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -326,6 +326,11 @@ object CaptureSet:
   /** Used as a recursion brake */
   @sharable private[dotc] val Pending = Const(SimpleIdentitySet.empty)
 
+  /** The empty capture set with a description that says it's the elf type of an
+   *  exception class.
+   */
+  val emptyOfException: CaptureSet.Const = Const(emptySet, "of an exception class")
+
   def apply(elems: CaptureRef*)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty
     else Const(SimpleIdentitySet(elems.map(_.normalizedRef)*))
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 12b5dbac8a16..67b7bfa30d7c 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -504,6 +504,8 @@ class CheckCaptures extends Recheck, SymTransformer:
         for param <- cls.paramGetters do
           if !param.hasAnnotation(defn.ConstructorOnlyAnnot) then
             checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3)
+        if cls.derivesFrom(defn.ThrowableClass) then
+          checkSubset(thisSet, CaptureSet.emptyOfException, tree.srcPos)
         super.recheckClassDef(tree, impl, cls)
       finally
         curEnv = saved
diff --git a/tests/neg-custom-args/captures/exception-definitions.check b/tests/neg-custom-args/captures/exception-definitions.check
new file mode 100644
index 000000000000..f609580bba4f
--- /dev/null
+++ b/tests/neg-custom-args/captures/exception-definitions.check
@@ -0,0 +1,13 @@
+-- Error: tests/neg-custom-args/captures/exception-definitions.scala:2:6 -----------------------------------------------
+2 |class Err extends Exception: // error
+  |^
+  |reference (scala.caps.* : Any) is not included in allowed capture set {} of an exception class
+3 |  self: {*} Err =>
+-- Error: tests/neg-custom-args/captures/exception-definitions.scala:7:12 ----------------------------------------------
+7 |    val x = c  // error
+  |            ^
+  |   (c : {*} Any) cannot be referenced here; it is not included in the allowed capture set {} of an exception class
+-- Error: tests/neg-custom-args/captures/exception-definitions.scala:8:8 -----------------------------------------------
+8 |  class Err3(c: {*} Any) extends Exception // error
+  |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  |  reference (Err3.this.c : {*} Any) is not included in allowed capture set {} of an exception class
diff --git a/tests/neg-custom-args/captures/exception-definitions.scala b/tests/neg-custom-args/captures/exception-definitions.scala
new file mode 100644
index 000000000000..067f784026e0
--- /dev/null
+++ b/tests/neg-custom-args/captures/exception-definitions.scala
@@ -0,0 +1,10 @@
+
+class Err extends Exception: // error
+  self: {*} Err =>
+
+def test(c: {*} Any) =
+  class Err2 extends Exception:
+    val x = c  // error
+  class Err3(c: {*} Any) extends Exception // error
+
+

From 39645991ad14b4f3ab28436982b80391e48dd4cd Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:35:24 +0100
Subject: [PATCH 14/37] Tweak: Don't refine parameters of Java classes

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

diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 42c80e524a6e..289437b37d59 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -98,7 +98,10 @@ extends tpd.TreeTraverser:
     def addCaptureRefinements(tp: Type): Type = tp match
       case _: TypeRef | _: AppliedType if tp.typeParams.isEmpty =>
         tp.typeSymbol match
-          case cls: ClassSymbol if !defn.isFunctionClass(cls) =>
+          case cls: ClassSymbol
+          if !defn.isFunctionClass(cls) && !cls.is(JavaDefined) =>
+            // We assume that Java classes can refer to capturing Scala types only indirectly,
+            // using type parameters. Hence, no need to refine them.
             cls.paramGetters.foldLeft(tp) { (core, getter) =>
               if getter.termRef.isTracked then
                 val getterType = tp.memberInfo(getter).strippedDealias

From 2ba6289e98fa2d726fd8c91d26ffe88fa7ce6cb0 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:37:14 +0100
Subject: [PATCH 15/37] Tweak: Tweak rechecking of returns

---
 compiler/src/dotty/tools/dotc/transform/Recheck.scala | 11 ++++++++++-
 tests/pos-custom-args/captures/cmp-singleton-2.scala  | 11 +++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/pos-custom-args/captures/cmp-singleton-2.scala

diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index c62b39a9e0c8..3f5f197e4a90 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -300,7 +300,16 @@ abstract class Recheck extends Phase, SymTransformer:
 
       val rawType = recheck(tree.expr)
       val ownType = avoidMap(rawType)
-      checkConforms(ownType, tree.from.symbol.returnProto, tree)
+      // The pattern matching translation, which runs before this phase
+      // sometimes instantiates return types with singleton type alternatives
+      // but the returned expression is widened. We compensate by widening the expected
+      // type as well.
+      def widened(tp: Type): Type = tp match
+        case tp: SingletonType => tp.widen
+        case tp: AndOrType => tp.derivedAndOrType(widened(tp.tp1), widened(tp.tp2))
+        case tp @ AnnotatedType(tp1, ann) => tp.derivedAnnotatedType(widened(tp1), ann)
+        case _ => tp
+      checkConforms(ownType, widened(tree.from.symbol.returnProto), tree)
       defn.NothingType
     end recheckReturn
 
diff --git a/tests/pos-custom-args/captures/cmp-singleton-2.scala b/tests/pos-custom-args/captures/cmp-singleton-2.scala
new file mode 100644
index 000000000000..daaa4add3858
--- /dev/null
+++ b/tests/pos-custom-args/captures/cmp-singleton-2.scala
@@ -0,0 +1,11 @@
+class T
+class A extends T
+class B extends T
+
+def test(tp: T) =
+  val mapping: Map[A, String] = ???
+
+  tp match
+    case a: A => mapping(a) match
+      case s: String => B()
+      case null => a

From d157daa211a93ffede1ca4ceca66d870be0c9f25 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:39:19 +0100
Subject: [PATCH 16/37] Bugfix: Refine canWidenAbstract criterion

When reducing match types, we did not permit to widen an abstract type scrutinee together with
a non-unique type parameter instantiation. But this criterion need not apply if the
widening is in a constraint satisfiabilty check. For instance

    T <: Tuple
    X <: A *: T

    X match
      case x *: (xs <: Tuple) => ...

Here the match does not succeed since X needs to be widened to A *: T and the x parameter
cannot be uniquely instantiated. On the other hand

    A *: T match
      case x *: (xs <: Tuple) => ...

should pass since there is no widening of the scrutinee. But there is a test T <: Tuple to check
whether T can match xs. That second check should not fall under the canWidenAbstract criterion.

Note: I was not able to make a test (without the fix) fail without capture checking, maybe
because the syntax (xs <: Tuple) is actually not allowed. But it is generated after Typer.
---
 .../dotty/tools/dotc/core/ConstraintHandling.scala   | 12 +++++++++++-
 .../src/dotty/tools/dotc/core/TypeComparer.scala     |  2 --
 tests/pos-custom-args/captures/matchtypes.scala      | 10 ++++++++++
 3 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/matchtypes.scala

diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 1dfa04822766..a3d8cabba971 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -58,6 +58,12 @@ trait ConstraintHandling {
    */
   protected var comparedTypeLambdas: Set[TypeLambda] = Set.empty
 
+  /** Used for match type reduction: If false, we don't recognize an abstract type
+   *  to be a subtype type of any of its base classes. This is in place only at the
+   *  toplevel; it is turned on again when we add parts of the scrutinee to the constraint.
+   */
+  protected var canWidenAbstract: Boolean = true
+
   protected var myNecessaryConstraintsOnly = false
   /** When collecting the constraints needed for a particular subtyping
    *  judgment to be true, we sometimes need to approximate the constraint
@@ -839,13 +845,17 @@ trait ConstraintHandling {
     //checkPropagated(s"adding $description")(true) // DEBUG in case following fails
     checkPropagated(s"added $description") {
       addConstraintInvocations += 1
+      val saved = canWidenAbstract
+      canWidenAbstract = true
       try bound match
         case bound: TypeParamRef if constraint contains bound =>
           addParamBound(bound)
         case _ =>
           val pbound = avoidLambdaParams(bound)
           kindCompatible(param, pbound) && addBoundTransitively(param, pbound, !fromBelow)
-      finally addConstraintInvocations -= 1
+      finally
+        canWidenAbstract = saved
+        addConstraintInvocations -= 1
     }
   end addConstraint
 
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index b50d524cd4a0..d19c6cdf5489 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -60,8 +60,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   /** Indicates whether the subtype check used GADT bounds */
   private var GADTused: Boolean = false
 
-  protected var canWidenAbstract: Boolean = true
-
   private var myInstance: TypeComparer = this
   def currentInstance: TypeComparer = myInstance
 
diff --git a/tests/pos-custom-args/captures/matchtypes.scala b/tests/pos-custom-args/captures/matchtypes.scala
new file mode 100644
index 000000000000..b2442277f1f7
--- /dev/null
+++ b/tests/pos-custom-args/captures/matchtypes.scala
@@ -0,0 +1,10 @@
+type HEAD[X <: NonEmptyTuple] = X match {
+  case x *: (_ <: NonEmptyTuple) => x
+}
+
+inline def head[A <: NonEmptyTuple](x: A): HEAD[A] = null.asInstanceOf[HEAD[A]]
+
+def show[A, T <: Tuple](x: A *: T) =
+  show1(head(x))
+  show1(x.head)
+def show1[A](x: A): String = ???
\ No newline at end of file

From 18b8ff4f166e3d60a7f6034bd2dd92a04b4efd9a Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:42:22 +0100
Subject: [PATCH 17/37] Tweak: Widen skolem types before conformity checks

---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  3 +-
 .../dotty/tools/dotc/transform/Recheck.scala  | 39 +++++++++++++++++--
 tests/pending/pos/i16268.scala                | 25 ++++++++++++
 3 files changed, 62 insertions(+), 5 deletions(-)
 create mode 100644 tests/pending/pos/i16268.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 67b7bfa30d7c..8cbd0a40ad85 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -762,7 +762,8 @@ class CheckCaptures extends Recheck, SymTransformer:
               // We can't box/unbox the universal capability. Leave `actual` as it is
               // so we get an error in checkConforms. This tends to give better error
               // messages than disallowing the root capability in `criticalSet`.
-              capt.println(i"cannot box/unbox $actual vs $expected")
+              if ctx.settings.YccDebug.value then
+                println(i"cannot box/unbox $actual vs $expected")
               actual
             else
               // Disallow future addition of `*` to `criticalSet`.
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 3f5f197e4a90..86e0e898235e 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -300,10 +300,14 @@ abstract class Recheck extends Phase, SymTransformer:
 
       val rawType = recheck(tree.expr)
       val ownType = avoidMap(rawType)
+
       // The pattern matching translation, which runs before this phase
       // sometimes instantiates return types with singleton type alternatives
       // but the returned expression is widened. We compensate by widening the expected
-      // type as well.
+      // type as well. See also `widenSkolems` in `checkConformsExpr` which fixes
+      // a more general problem. It turns out that pattern matching returns
+      // are not checked by Ycheck, that's why these problems were allowed to slip
+      // through.
       def widened(tp: Type): Type = tp match
         case tp: SingletonType => tp.widen
         case tp: AndOrType => tp.derivedAndOrType(widened(tp.tp1), widened(tp.tp2))
@@ -435,6 +439,27 @@ abstract class Recheck extends Phase, SymTransformer:
           throw ex
       }
 
+    /** Typing and previous transforms sometiems leaves skolem types in prefixes of
+     *  NamedTypes in `expected` that do not match the `actual` Type. -Ycheck does
+     *  not complain (need to find out why), but a full recheck does. We compensate
+     *  by de-skolemizing everywhere in `expected` except when variance is negative.
+     *  @return If `tp` contains SkolemTypes in covariant or invariant positions,
+     *          the type where these SkolemTypes are mapped to their underlying type.
+     *          Otherwise, `tp` itself
+     */
+    def widenSkolems(tp: Type)(using Context): Type =
+      object widenSkolems extends TypeMap, IdempotentCaptRefMap:
+        var didWiden: Boolean = false
+        def apply(t: Type): Type = t match
+          case t: SkolemType if variance >= 0 =>
+            didWiden = true
+            apply(t.underlying)
+          case t: LazyRef => t
+          case t @ AnnotatedType(t1, ann) => t.derivedAnnotatedType(apply(t1), ann)
+          case _ => mapOver(t)
+      val tp1 = widenSkolems(tp)
+      if widenSkolems.didWiden then tp1 else tp
+
     /** If true, print info for some successful checkConforms operations (failing ones give
      *  an error message in any case).
      */
@@ -450,11 +475,16 @@ abstract class Recheck extends Phase, SymTransformer:
 
     def checkConformsExpr(actual: Type, expected: Type, tree: Tree)(using Context): Unit =
       //println(i"check conforms $actual <:< $expected")
-      val isCompatible =
+
+      def isCompatible(expected: Type): Boolean =
         actual <:< expected
         || expected.isRepeatedParam
-            && actual <:< expected.translateFromRepeated(toArray = tree.tpe.isRef(defn.ArrayClass))
-      if !isCompatible then
+            && isCompatible(expected.translateFromRepeated(toArray = tree.tpe.isRef(defn.ArrayClass)))
+        || {
+          val widened = widenSkolems(expected)
+          (widened ne expected) && isCompatible(widened)
+        }
+      if !isCompatible(expected) then
         recheckr.println(i"conforms failed for ${tree}: $actual vs $expected")
         err.typeMismatch(tree.withType(actual), expected)
       else if debugSuccesses then
@@ -462,6 +492,7 @@ abstract class Recheck extends Phase, SymTransformer:
           case _: Ident =>
             println(i"SUCCESS $tree:\n${TypeComparer.explained(_.isSubType(actual, expected))}")
           case _ =>
+    end checkConformsExpr
 
     def checkUnit(unit: CompilationUnit)(using Context): Unit =
       recheck(unit.tpdTree)
diff --git a/tests/pending/pos/i16268.scala b/tests/pending/pos/i16268.scala
new file mode 100644
index 000000000000..6b44e71a2247
--- /dev/null
+++ b/tests/pending/pos/i16268.scala
@@ -0,0 +1,25 @@
+import language.experimental.captureChecking
+class Tree
+case class Thicket(trees: List[Tree]) extends Tree
+
+def test1(segments: List[{*} Tree]) =
+  val elems = segments flatMap { (t: {*} Tree) => t match // error
+    case ts: Thicket => ts.trees.tail
+    case t => Nil
+  }
+  elems
+
+def test2(segments: List[{*} Tree]) =
+  val f = (t: {*} Tree) => t match
+    case ts: Thicket => ts.trees.tail
+    case t => Nil
+  val elems = segments.flatMap(f) // error
+  elems
+
+def test3(c: {*} Any)(segments: List[{c} Tree]) =
+  val elems = segments flatMap { (t: {c} Tree) => t match
+    case ts: Thicket => ts.trees.tail
+    case t => Nil
+  }
+  elems
+

From 1b15fa67ea809f70d48a60343f3a9c7f953ef2e2 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:43:21 +0100
Subject: [PATCH 18/37] Bugfix: Relax experimental inheritance criterion

We previously required that a class inheriting an @experimental class is itself
@experimental. This is too strict. It should be OK to have the inheriting class
be contained in an experimental scope. I.e.
```
@experimental class A
@experimental object o:
  class B extends A
```
is now OK.
---
 compiler/src/dotty/tools/dotc/typer/CrossVersionChecks.scala | 2 +-
 tests/pos/experimental-inheritance.scala                     | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)
 create mode 100644 tests/pos/experimental-inheritance.scala

diff --git a/compiler/src/dotty/tools/dotc/typer/CrossVersionChecks.scala b/compiler/src/dotty/tools/dotc/typer/CrossVersionChecks.scala
index 044dd7bb8528..00b037a4e259 100644
--- a/compiler/src/dotty/tools/dotc/typer/CrossVersionChecks.scala
+++ b/compiler/src/dotty/tools/dotc/typer/CrossVersionChecks.scala
@@ -117,7 +117,7 @@ class CrossVersionChecks extends MiniPhase:
 
   /** Check that classes extending experimental classes or nested in experimental classes have the @experimental annotation. */
   private def checkExperimentalInheritance(cls: ClassSymbol)(using Context): Unit =
-    if !cls.isAnonymousClass && !cls.hasAnnotation(defn.ExperimentalAnnot) then
+    if !cls.isAnonymousClass && !cls.isInExperimentalScope then
       cls.info.parents.find(_.typeSymbol.isExperimental) match
         case Some(parent) =>
           report.error(em"extension of experimental ${parent.typeSymbol} must have @experimental annotation", cls.srcPos)
diff --git a/tests/pos/experimental-inheritance.scala b/tests/pos/experimental-inheritance.scala
new file mode 100644
index 000000000000..78681caa3929
--- /dev/null
+++ b/tests/pos/experimental-inheritance.scala
@@ -0,0 +1,4 @@
+import annotation.experimental
+@experimental class A
+@experimental object o:
+  class B extends A
\ No newline at end of file

From 055beabb75dc2f43c212fd2db20080c71cea985d Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:45:02 +0100
Subject: [PATCH 19/37] Enhancement: Introduce caps.Pure trait

This can replace the more obscure idiom of declaring a
non-capturing self type.
---
 library/src/scala/caps.scala | 6 ++++++
 project/MiMaFilters.scala    | 1 +
 2 files changed, 7 insertions(+)

diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 21b2f7a4dece..12ab0abd2a21 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -16,3 +16,9 @@ import annotation.experimental
    *  avoids the error that would be raised when unboxing `*`.
    */
   extension [T](x: T) def unsafeUnbox: T = x
+
+  /** Mixing in this trait forces a trait or class to be pure, i.e.
+   *  have no capabilities retained in its self type.
+   */
+  trait Pure:
+    this: Pure =>
diff --git a/project/MiMaFilters.scala b/project/MiMaFilters.scala
index 81510d22d2c2..1221b16e9a44 100644
--- a/project/MiMaFilters.scala
+++ b/project/MiMaFilters.scala
@@ -19,5 +19,6 @@ object MiMaFilters {
     ProblemFilters.exclude[MissingClassProblem]("scala.runtime.stdLibPatches.language$experimental$pureFunctions$"),
     ProblemFilters.exclude[MissingClassProblem]("scala.runtime.stdLibPatches.language$experimental$captureChecking$"),
     ProblemFilters.exclude[MissingClassProblem]("scala.caps"),
+    ProblemFilters.exclude[MissingClassProblem]("scala.caps$Pure"),
   )
 }

From f1940985326b121acdd6e14830a325ba288114c1 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:48:57 +0100
Subject: [PATCH 20/37] Tweak: Make root addition handler take a context

Since root addition handlers are stored in capture sets they should
not close over a context, since otherwise every capture set would
close over a context.

# Conflicts:
#	tests/pos-with-compiler-cc/dotc/cc/CaptureSet.scala
---
 compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 694c5140f203..e57cb53cd12d 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -271,7 +271,7 @@ sealed abstract class CaptureSet extends Showable:
     map(Substituters.SubstParamsMap(tl, to))
 
   /** Invoke handler if this set has (or later aquires) the root capability `*` */
-  def disallowRootCapability(handler: () => Unit)(using Context): this.type =
+  def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
     if isUniversal then handler()
     this
 
@@ -378,7 +378,7 @@ object CaptureSet:
     def isAlwaysEmpty = false
 
     /** A handler to be invoked if the root reference `*` is added to this set */
-    var addRootHandler: () => Unit = () => ()
+    var rootAddedHandler: () => Context ?=> Unit = () => ()
 
     var description: String = ""
 
@@ -409,7 +409,7 @@ object CaptureSet:
     def addNewElems(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
       if !isConst && recordElemsState() then
         elems ++= newElems
-        if isUniversal then addRootHandler()
+        if isUniversal then rootAddedHandler()
         // assert(id != 2 || elems.size != 2, this)
         (CompareResult.OK /: deps) { (r, dep) =>
           r.andAlso(dep.tryInclude(newElems, this))
@@ -426,8 +426,8 @@ object CaptureSet:
       else
         CompareResult.fail(this)
 
-    override def disallowRootCapability(handler: () => Unit)(using Context): this.type =
-      addRootHandler = handler
+    override def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
+      rootAddedHandler = handler
       super.disallowRootCapability(handler)
 
     private var computingApprox = false

From f6e1c0311e35d75137c0fbf1abdfbc61a463b87b Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:52:14 +0100
Subject: [PATCH 21/37] Bugfix: Fix setup of overriding symbols

 - Avoid accidental addition of capture set variables through traverseChildren
   of exact ValDefs and DefDefs.
 - Don't require that overriding symbols need explicit types if their capture set
   is non-empty. This is not needed since an overriding symbol with inferred type
   will get the type of the overridden symbol.
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala    | 11 +++++------
 compiler/src/dotty/tools/dotc/cc/Setup.scala   | 18 ++++++++----------
 tests/neg-custom-args/captures/lazylist.check  | 14 +++++++-------
 tests/neg-custom-args/captures/lazylist.scala  |  2 +-
 4 files changed, 21 insertions(+), 24 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 8cbd0a40ad85..945a303a13b7 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -884,12 +884,11 @@ class CheckCaptures extends Recheck, SymTransformer:
           val isLocal =
             sym.owner.ownersIterator.exists(_.isTerm)
             || sym.accessBoundary(defn.RootClass).isContainedIn(sym.topLevelClass)
-          def canUseInferred =            // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
-            sym.is(Private)                         // private symbols can always have inferred types
-            ||                                      // non-local symbols cannot have inferred types since external capture types are not inferred
-              isLocal                               // local symbols still need an explicit types if
-              && !sym.owner.is(Trait)               //   - they are defined in a trait, since we do OverridingPairs checking before capture inference
-              && !sym.allOverriddenSymbols.nonEmpty //   - they override some other symbol, since we do override checking before capture inference
+          def canUseInferred =        // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
+            sym.is(Private)           // private symbols can always have inferred types
+            ||                        // non-local symbols cannot have inferred types since external capture types are not inferred
+              isLocal                 // local symbols still need explicit types if
+              && !sym.owner.is(Trait) // they are defined in a trait, since we do OverridingPairs checking before capture inference
           def isNotPureThis(ref: CaptureRef) = ref match {
             case ref: ThisType => !ref.cls.isPureClass
             case _ => true
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 289437b37d59..7ae872ac2304 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -385,20 +385,18 @@ extends tpd.TreeTraverser:
           return
         tree.tpt match
           case tpt: TypeTree if tree.symbol.allOverriddenSymbols.hasNext =>
+            tree.paramss.foreach(traverse)
             transformTT(tpt, boxed = false, exact = true)
+            traverse(tree.rhs)
             //println(i"TYPE of ${tree.symbol.showLocated} = ${tpt.knownType}")
           case _ =>
-        traverseChildren(tree)
+            traverseChildren(tree)
       case tree @ ValDef(_, tpt: TypeTree, _) =>
-        val isVar = tree.symbol.is(Mutable)
-        val overrides = tree.symbol.allOverriddenSymbols.hasNext
-        //if overrides then println(i"transforming overriding ${tree.symbol}")
-        if isVar || overrides then
-          transformTT(tpt,
-              boxed = isVar,    // types of mutable variables are boxed
-              exact = overrides // types of symbols that override a parent don't get a capture set
-            )
-        traverseChildren(tree)
+        transformTT(tpt,
+          boxed = tree.symbol.is(Mutable),    // types of mutable variables are boxed
+          exact = tree.symbol.allOverriddenSymbols.hasNext // types of symbols that override a parent don't get a capture set
+        )
+        traverse(tree.rhs)
       case tree @ TypeApply(fn, args) =>
         traverse(fn)
         for case arg: TypeTree <- args do
diff --git a/tests/neg-custom-args/captures/lazylist.check b/tests/neg-custom-args/captures/lazylist.check
index e43538ad97f7..1ad705556b88 100644
--- a/tests/neg-custom-args/captures/lazylist.check
+++ b/tests/neg-custom-args/captures/lazylist.check
@@ -5,6 +5,13 @@
    |        method tail of type -> {*} lazylists.LazyList[Nothing] has incompatible type
    |
    | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:17:15 -------------------------------------
+17 |  def tail = xs() // error
+   |             ^^^^
+   |             Found:    {LazyCons.this.xs} lazylists.LazyList[T]
+   |             Required: lazylists.LazyList[T]
+   |
+   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:35:29 -------------------------------------
 35 |  val ref1c: LazyList[Int] = ref1 // error
    |                             ^^^^
@@ -33,10 +40,3 @@
    |                                             Required: {cap1, ref3, cap3} lazylists.LazyList[Int]
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/lazylist.scala:17:6 -----------------------------------------------------------
-17 |  def tail = xs() // error: cannot have an inferred type
-   |  ^^^^^^^^^^^^^^^
-   |  Non-local method tail cannot have an inferred result type
-   |  {LazyCons.this.xs} lazylists.LazyList[? T]
-   |  with non-empty capture set {LazyCons.this.xs}.
-   |  The type needs to be declared explicitly.
diff --git a/tests/neg-custom-args/captures/lazylist.scala b/tests/neg-custom-args/captures/lazylist.scala
index 56bfc3ea6da2..2674f15a0ee3 100644
--- a/tests/neg-custom-args/captures/lazylist.scala
+++ b/tests/neg-custom-args/captures/lazylist.scala
@@ -14,7 +14,7 @@ abstract class LazyList[+T]:
 class LazyCons[+T](val x: T, val xs: () => {*} LazyList[T]) extends LazyList[T]:
   def isEmpty = false
   def head = x
-  def tail = xs() // error: cannot have an inferred type
+  def tail = xs() // error
 
 object LazyNil extends LazyList[Nothing]:
   def isEmpty = true

From 65477c57eebb36974a69dc4adb6db185c50ac90e Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:53:25 +0100
Subject: [PATCH 22/37] Bugfix: Make another map an IdempotentCaptRefMap

---
 compiler/src/dotty/tools/dotc/core/TypeOps.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index 3e3490b1f01b..4c52a9bd3ef2 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -186,7 +186,7 @@ object TypeOps:
         if (normed.exists) normed else mapOver
       case tp: MethodicType =>
         // See documentation of `Types#simplified`
-        val addTypeVars = new TypeMap:
+        val addTypeVars = new TypeMap with IdempotentCaptRefMap:
           val constraint = ctx.typerState.constraint
           def apply(t: Type): Type = t match
             case t: TypeParamRef => constraint.typeVarOfParam(t).orElse(t)

From 594aa1ab3bd0baf6c93d2cefc8516cb1e2dbd66e Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 18:56:07 +0100
Subject: [PATCH 23/37] Bugfix: Fix handling for call-by-name arguments of
 applied types

We need some special treatment for types such as `(=> A) => B`
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 10 ++++--
 .../dotty/tools/dotc/transform/Recheck.scala  | 36 ++++++++++++++++---
 .../pos-custom-args/captures/bynamefun.scala  | 11 ++++++
 3 files changed, 51 insertions(+), 6 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/bynamefun.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 945a303a13b7..e3e42ee343d4 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -432,7 +432,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       block match
         case closureDef(mdef) =>
           pt.dealias match
-            case defn.FunctionOf(ptformals, _, _, _) if ptformals.forall(_.captureSet.isAlwaysEmpty) =>
+            case defn.FunctionOf(ptformals, _, _, _)
+            if ptformals.nonEmpty && ptformals.forall(_.captureSet.isAlwaysEmpty) =>
               // Redo setup of the anonymous function so that formal parameters don't
               // get capture sets. This is important to avoid false widenings to `*`
               // when taking the base type of the actual closures's dependent function
@@ -442,9 +443,14 @@ class CheckCaptures extends Recheck, SymTransformer:
               // First, undo the previous setup which installed a completer for `meth`.
               atPhase(preRecheckPhase.prev)(meth.denot.copySymDenotation())
                 .installAfter(preRecheckPhase)
+
+              //atPhase(preRecheckPhase.prev)(meth.denot.copySymDenotation())
+              //  .installAfter(thisPhase)
               // Next, update all parameter symbols to match expected formals
               meth.paramSymss.head.lazyZip(ptformals).foreach { (psym, pformal) =>
-                psym.copySymDenotation(info = pformal).installAfter(preRecheckPhase)
+                psym.copySymDenotation(info = pformal.mapExprType).installAfter(preRecheckPhase)
+              //  psym.copySymDenotation(info = pformal).installAfter(thisPhase)
+              //  println(i"UPDATE $psym to ${pformal.mapExprType}, was $pformal")
               }
               // Next, update types of parameter ValDefs
               mdef.paramss.head.lazyZip(ptformals).foreach { (param, pformal) =>
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 86e0e898235e..12d22d99b12a 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -22,6 +22,7 @@ import StdNames.nme
 import reporting.trace
 import annotation.constructorOnly
 import cc.CaptureSet.IdempotentCaptRefMap
+import dotty.tools.dotc.core.Denotations.SingleDenotation
 
 object Recheck:
   import tpd.*
@@ -91,6 +92,18 @@ object Recheck:
 
     def hasRememberedType: Boolean = tree.hasAttachment(RecheckedType)
 
+  extension (tpe: Type)
+
+    /** Map ExprType => T to () ?=> T (and analogously for pure versions).
+     *  Even though this phase runs after ElimByName, ExprTypes can still occur
+     *  as by-name arguments of applied types. See note in doc comment for
+     *  ElimByName phase. Test case is bynamefun.scala.
+     */
+    def mapExprType(using Context): Type = tpe match
+      case ExprType(rt) => defn.ByNameFunction(rt)
+      case _ => tpe
+
+
 /** A base class that runs a simplified typer pass over an already re-typed program. The pass
  *  does not transform trees but returns instead the re-typed type of each tree as it is
  *  traversed. The Recheck phase must be directly preceded by a phase of type PreRecheck.
@@ -152,15 +165,27 @@ abstract class Recheck extends Phase, SymTransformer:
         else AnySelectionProto
       recheckSelection(tree, recheck(qual, proto).widenIfUnstable, name, pt)
 
+    /** When we select the `apply` of a function with type such as `(=> A) => B`,
+     *  we need to convert the parameter type `=> A` to `() ?=> A`. See doc comment
+     *  of `mapExprType`.
+     */
+    def normalizeByName(mbr: SingleDenotation)(using Context): SingleDenotation = mbr.info match
+      case mt: MethodType if mt.paramInfos.exists(_.isInstanceOf[ExprType]) =>
+        mbr.derivedSingleDenotation(mbr.symbol,
+          mt.derivedLambdaType(paramInfos = mt.paramInfos.map(_.mapExprType)))
+      case _ =>
+        mbr
+
     def recheckSelection(tree: Select, qualType: Type, name: Name,
         sharpen: Denotation => Denotation)(using Context): Type =
       if name.is(OuterSelectName) then tree.tpe
       else
         //val pre = ta.maybeSkolemizePrefix(qualType, name)
-        val mbr = sharpen(
+        val mbr = normalizeByName(
+          sharpen(
             qualType.findMember(name, qualType,
               excluded = if tree.symbol.is(Private) then EmptyFlags else Private
-          )).suchThat(tree.symbol == _)
+          )).suchThat(tree.symbol == _))
         constFold(tree, qualType.select(name, mbr))
           //.showing(i"recheck select $qualType . $name : ${mbr.info} = $result")
 
@@ -215,7 +240,8 @@ abstract class Recheck extends Phase, SymTransformer:
       mt.instantiate(argTypes)
 
     def recheckApply(tree: Apply, pt: Type)(using Context): Type =
-      recheck(tree.fun).widen match
+      val funtpe = recheck(tree.fun)
+      funtpe.widen match
         case fntpe: MethodType =>
           assert(fntpe.paramInfos.hasSameLengthAs(tree.args))
           val formals =
@@ -223,7 +249,7 @@ abstract class Recheck extends Phase, SymTransformer:
             else fntpe.paramInfos
           def recheckArgs(args: List[Tree], formals: List[Type], prefs: List[ParamRef]): List[Type] = args match
             case arg :: args1 =>
-              val argType = recheck(arg, formals.head)
+              val argType = recheck(arg, formals.head.mapExprType)
               val formals1 =
                 if fntpe.isParamDependent
                 then formals.tail.map(_.substParam(prefs.head, argType))
@@ -235,6 +261,8 @@ abstract class Recheck extends Phase, SymTransformer:
           val argTypes = recheckArgs(tree.args, formals, fntpe.paramRefs)
           constFold(tree, instantiate(fntpe, argTypes, tree.fun.symbol))
             //.showing(i"typed app $tree : $fntpe with ${tree.args}%, % : $argTypes%, % = $result")
+        case tp =>
+          assert(false, i"unexpected type of ${tree.fun}: $funtpe")
 
     def recheckTypeApply(tree: TypeApply, pt: Type)(using Context): Type =
       recheck(tree.fun).widen match
diff --git a/tests/pos-custom-args/captures/bynamefun.scala b/tests/pos-custom-args/captures/bynamefun.scala
new file mode 100644
index 000000000000..86bad201ffc3
--- /dev/null
+++ b/tests/pos-custom-args/captures/bynamefun.scala
@@ -0,0 +1,11 @@
+object test:
+  class Plan(elem: Plan)
+  object SomePlan extends Plan(???)
+  def f1(expr: (-> Plan) -> Plan): Plan = expr(SomePlan)
+  f1 { onf => Plan(onf) }
+  def f2(expr: (=> Plan) -> Plan): Plan = ???
+  f2 { onf => Plan(onf) }
+  def f3(expr: (-> Plan) => Plan): Plan = ???
+  f1 { onf => Plan(onf) }
+  def f4(expr: (=> Plan) => Plan): Plan = ???
+  f2 { onf => Plan(onf) }

From f8c44824b567a913dc1863861e0cd4ae90b1d78c Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 6 Nov 2022 19:03:25 +0100
Subject: [PATCH 24/37] Bugfix: Make sure to restore anonymous function infos

Make sure to restore info of anonymous functions and their parameters after cc
---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 9 ++-------
 tests/neg-custom-args/captures/selftype.scala        | 4 ++++
 2 files changed, 6 insertions(+), 7 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/selftype.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index e3e42ee343d4..6c4f3fc8eb5f 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -444,13 +444,9 @@ class CheckCaptures extends Recheck, SymTransformer:
               atPhase(preRecheckPhase.prev)(meth.denot.copySymDenotation())
                 .installAfter(preRecheckPhase)
 
-              //atPhase(preRecheckPhase.prev)(meth.denot.copySymDenotation())
-              //  .installAfter(thisPhase)
               // Next, update all parameter symbols to match expected formals
               meth.paramSymss.head.lazyZip(ptformals).foreach { (psym, pformal) =>
-                psym.copySymDenotation(info = pformal.mapExprType).installAfter(preRecheckPhase)
-              //  psym.copySymDenotation(info = pformal).installAfter(thisPhase)
-              //  println(i"UPDATE $psym to ${pformal.mapExprType}, was $pformal")
+                psym.updateInfoBetween(preRecheckPhase, thisPhase, pformal.mapExprType)
               }
               // Next, update types of parameter ValDefs
               mdef.paramss.head.lazyZip(ptformals).foreach { (param, pformal) =>
@@ -464,8 +460,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                   denot.info = mt.companion(ptformals, mdef.tpt.knownType)
                     .showing(i"simplify info of $meth to $result", capt)
                   recheckDef(mdef, meth)
-              meth.copySymDenotation(info = completer, initFlags = meth.flags &~ Touched)
-                .installAfter(preRecheckPhase)
+              meth.updateInfoBetween(preRecheckPhase, thisPhase, completer)
             case _ =>
         case _ =>
       super.recheckBlock(block, pt)
diff --git a/tests/neg-custom-args/captures/selftype.scala b/tests/neg-custom-args/captures/selftype.scala
new file mode 100644
index 000000000000..21148f625a7a
--- /dev/null
+++ b/tests/neg-custom-args/captures/selftype.scala
@@ -0,0 +1,4 @@
+@annotation.experimental class C(x: () => Unit) extends caps.Pure // error
+
+@annotation.experimental class D(@annotation.constructorOnly x: () => Unit) extends caps.Pure // ok
+

From 10c657c8654ee2eea05258c3b85beab66392d106 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 09:41:43 +0100
Subject: [PATCH 25/37] Tweak: Exclude default getters from "must be explicitly
 defined" requirements

Default getters always have an inferred result type. If that type captures capabilities,
we used to get an error that an inferred non pure type needs to be explicitly defined.
But usually, a default getter type does not matter. So we make an exception and allow
it. Note that this could be a hole, for instance in a situation like this:
```scala
  def f[X](x: X = foo): X = ...
```
If `foo`'s inferred type is `{*} T`, and there is a call to `f()` in the same compilation
unit `X` will be instantiated to `{*} T` and this will also be the result for `f`. But if
the call is in a different compilation unit, it will only see `foo: T`, and the result of
`f` is typed `T`.

A better solution would be to demand that default getter's types are pure, but only if the
getter type can leak into the type of the function to which it belongs. The problem is that
currently that's very hard to do because when we see a default getter it's difficult to
discover to which parameter from which function it belongs.

Therefore, for the moment we leave the hole open, hoping for a better solution to default getters
in the future.
---
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala    | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 6c4f3fc8eb5f..7c26f97eac07 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -18,6 +18,7 @@ import Recheck.*
 import scala.collection.mutable
 import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap}
 import StdNames.nme
+import NameKinds.DefaultGetterName
 import reporting.trace
 
 /** The capture checker */
@@ -885,11 +886,14 @@ class CheckCaptures extends Recheck, SymTransformer:
           val isLocal =
             sym.owner.ownersIterator.exists(_.isTerm)
             || sym.accessBoundary(defn.RootClass).isContainedIn(sym.topLevelClass)
-          def canUseInferred =        // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
-            sym.is(Private)           // private symbols can always have inferred types
-            ||                        // non-local symbols cannot have inferred types since external capture types are not inferred
-              isLocal                 // local symbols still need explicit types if
-              && !sym.owner.is(Trait) // they are defined in a trait, since we do OverridingPairs checking before capture inference
+          def canUseInferred =    // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
+            sym.is(Private)                   // private symbols can always have inferred types
+            || sym.name.is(DefaultGetterName) // default getters are exempted since otherwise it would be
+                                              // too annoying. This is a hole since a defualt getter's result type
+                                              // might leak into a type variable.
+            ||                                // non-local symbols cannot have inferred types since external capture types are not inferred
+              isLocal                         // local symbols still need explicit types if
+              && !sym.owner.is(Trait)         // they are defined in a trait, since we do OverridingPairs checking before capture inference
           def isNotPureThis(ref: CaptureRef) = ref match {
             case ref: ThisType => !ref.cls.isPureClass
             case _ => true

From c2086df731669081d33bb0ee9ba9c913214edefc Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 09:42:34 +0100
Subject: [PATCH 26/37] Enhancement: Treat Any as a top type for comparisons.

It was already implied before, but so far an explicit rule that

    cs T <: Any

was missing. Adding that rule is important for bounds checking.
---
 compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index d19c6cdf5489..a37fbdd104cf 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -520,7 +520,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         res
 
       case CapturingType(parent1, refs1) =>
-        if subCaptures(refs1, tp2.captureSet, frozenConstraint).isOK && sameBoxed(tp1, tp2, refs1)
+        if tp2.isAny then true
+        else if subCaptures(refs1, tp2.captureSet, frozenConstraint).isOK && sameBoxed(tp1, tp2, refs1)
         then recur(parent1, tp2)
         else thirdTry
       case tp1: AnnotatedType if !tp1.isRefining =>

From ff5726cf1e6650a233dd1a2f8aab9b1d1c034b1b Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 09:43:10 +0100
Subject: [PATCH 27/37] Enhancement: Implement bounds checking

It turns out that bounds checking was missing so far.
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 22 ++++++++++++++++++-
 .../dotty/tools/dotc/transform/Recheck.scala  |  8 +++++--
 .../src/dotty/tools/dotc/typer/Checking.scala | 11 +++++-----
 .../captures/boundschecks.scala               | 18 +++++++++++++++
 .../captures/boundschecks2.scala              | 13 +++++++++++
 5 files changed, 64 insertions(+), 8 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/boundschecks.scala
 create mode 100644 tests/neg-custom-args/captures/boundschecks2.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 7c26f97eac07..ba35157957d4 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -11,6 +11,7 @@ import config.{Config, Feature}
 import ast.{tpd, untpd, Trees}
 import Trees.*
 import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents}
+import typer.Checking.{checkBounds, checkAppliedTypesIn}
 import util.{SimpleIdentitySet, EqHashMap, SrcPos}
 import transform.SymUtils.*
 import transform.{Recheck, PreRecheck}
@@ -911,8 +912,27 @@ class CheckCaptures extends Recheck, SymTransformer:
                       |The type needs to be declared explicitly.""", t.srcPos)
               case _ =>
             inferred.foreachPart(checkPure, StopAt.Static)
+        case t @ TypeApply(fun, args) =>
+          fun.knownType.widen match
+            case tl: PolyType =>
+              val normArgs = args.lazyZip(tl.paramInfos).map { (arg, bounds) =>
+                arg.withType(arg.knownType.forceBoxStatus(
+                  bounds.hi.isBoxedCapturing | bounds.lo.isBoxedCapturing))
+              }
+              checkBounds(normArgs, tl)
+            case _ =>
         case _ =>
       }
-
+      if !ctx.reporter.errorsReported then
+        // We dont report errors hre if previous errors were reported, because other
+        // errors often result in bad applied types, but flagging these bad types gives
+        // often worse error messages than the original errors.
+        val checkApplied = new TreeTraverser:
+          def traverse(t: Tree)(using Context) = t match
+            case tree: InferredTypeTree =>
+            case tree: New =>
+            case tree: TypeTree => checkAppliedTypesIn(tree.withKnownType)
+            case _ => traverseChildren(t)
+        checkApplied.traverse(unit)
   end CaptureChecker
 end CheckCaptures
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 12d22d99b12a..b28d0a0a048e 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -72,7 +72,7 @@ object Recheck:
       val symd = sym.denot
       symd.validFor.firstPhaseId == phase.id + 1 && (sym.originDenotation ne symd)
 
-  extension (tree: Tree)
+  extension [T <: Tree](tree: T)
 
     /** Remember `tpe` as the type of `tree`, which might be different from the
      *  type stored in the tree itself, unless a type was already remembered for `tree`.
@@ -87,11 +87,15 @@ object Recheck:
       if tpe ne tree.tpe then tree.putAttachment(RecheckedType, tpe)
 
     /** The remembered type of the tree, or if none was installed, the original type */
-    def knownType =
+    def knownType: Type =
       tree.attachmentOrElse(RecheckedType, tree.tpe)
 
     def hasRememberedType: Boolean = tree.hasAttachment(RecheckedType)
 
+    def withKnownType(using Context): T = tree.getAttachment(RecheckedType) match
+      case Some(tpe) => tree.withType(tpe).asInstanceOf[T]
+      case None => tree
+
   extension (tpe: Type)
 
     /** Map ExprType => T to () ?=> T (and analogously for pure versions).
diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala
index c53213d7bd37..16499f6c1f3e 100644
--- a/compiler/src/dotty/tools/dotc/typer/Checking.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala
@@ -67,11 +67,12 @@ object Checking {
    */
   def checkBounds(args: List[tpd.Tree], boundss: List[TypeBounds],
     instantiate: (Type, List[Type]) => Type, app: Type = NoType, tpt: Tree = EmptyTree)(using Context): Unit =
-    args.lazyZip(boundss).foreach { (arg, bound) =>
-      if !bound.isLambdaSub && !arg.tpe.hasSimpleKind then
-        errorTree(arg,
-          showInferred(MissingTypeParameterInTypeApp(arg.tpe), app, tpt))
-    }
+    if ctx.phase != Phases.checkCapturesPhase then
+      args.lazyZip(boundss).foreach { (arg, bound) =>
+        if !bound.isLambdaSub && !arg.tpe.hasSimpleKind then
+          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),
diff --git a/tests/neg-custom-args/captures/boundschecks.scala b/tests/neg-custom-args/captures/boundschecks.scala
new file mode 100644
index 000000000000..cf4eab28f19d
--- /dev/null
+++ b/tests/neg-custom-args/captures/boundschecks.scala
@@ -0,0 +1,18 @@
+object test {
+
+  class Tree
+
+  def f[X <: Tree](x: X): Unit = ()
+
+  class C[X <: Tree](x: X)
+
+  def foo(t: {*} Tree) =
+    f(t) // error
+    f[{*} Tree](t) // error
+    f[Tree](t)  // error
+    val c1 = C(t) // error
+    val c2 = C[{*} Tree](t) // error
+    val c3 = C[Tree](t)  // error
+
+    val foo: C[{*} Tree] = ???
+}
diff --git a/tests/neg-custom-args/captures/boundschecks2.scala b/tests/neg-custom-args/captures/boundschecks2.scala
new file mode 100644
index 000000000000..f6927b04931b
--- /dev/null
+++ b/tests/neg-custom-args/captures/boundschecks2.scala
@@ -0,0 +1,13 @@
+object test {
+
+  class Tree
+
+  def f[X <: Tree](x: X): Unit = ()
+
+  class C[X <: Tree](x: X)
+
+  val foo: C[{*} Tree] = ??? // error
+  type T = C[{*} Tree] // error
+  val bar: T -> T = ???
+  val baz: C[{*} Tree] -> Unit = ??? // error
+}

From 25a42467bcbefe0bd15725e6c8cbf086ab4be320 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 09:43:58 +0100
Subject: [PATCH 28/37] Enhancement: Take purity of classes into account when
 capture checking

Two major changes:

 1. During setup, don't generate a capture set variable for a type T if
   one of the base types of `T` is a pure class.

 2. During subtype checking, admit `cs T <: T` if one of the base types
   of `T` is a pure class. The idea is that in this case we know that the
   capture set will always be empty at runtime.

But don't do (2.) if we are checking self types. In this case the capture set cannot be
stripped. Example:

    class A:
      this: A =>
    class B extends A
      this: {c} B =>

In this case we should not assume `{c} B <: B` since we need to flag an error that the self
type of B does not conform to the self type of A.

   are checking self types. In that cas
---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala  | 35 ++++++++++++++++---
 compiler/src/dotty/tools/dotc/cc/Setup.scala  | 25 +++++++------
 .../tools/dotc/core/CheckRealizable.scala     |  4 +--
 compiler/src/dotty/tools/dotc/core/Mode.scala | 10 ++++--
 .../dotty/tools/dotc/core/TypeComparer.scala  |  3 +-
 .../src/dotty/tools/dotc/core/TypeOps.scala   |  2 +-
 .../src/dotty/tools/dotc/core/Types.scala     |  4 +--
 .../dotty/tools/dotc/typer/RefChecks.scala    | 30 ++++++++--------
 tests/neg-custom-args/captures/try.check      |  2 +-
 .../captures/colltest5/Test_2.scala           |  2 +-
 10 files changed, 77 insertions(+), 40 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 1c3b54bb4b2e..3dfd1324ae1e 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -166,16 +166,43 @@ extension (tp: Type)
       case CapturingType(_, _) => true
       case _ => false
 
+  /** Is type known to be always pure by its class structure,
+   *  so that adding a capture set to it would not make sense?
+   */
+  def isAlwaysPure(using Context): Boolean = tp.dealias match
+    case tp: (TypeRef | AppliedType) =>
+      val sym = tp.typeSymbol
+      if sym.isClass then sym.isPureClass
+      else tp.superType.isAlwaysPure
+    case CapturingType(parent, refs) =>
+      parent.isAlwaysPure || refs.isAlwaysEmpty
+    case tp: TypeProxy =>
+      tp.superType.isAlwaysPure
+    case tp: AndType =>
+      tp.tp1.isAlwaysPure || tp.tp2.isAlwaysPure
+    case tp: OrType =>
+      tp.tp1.isAlwaysPure && tp.tp2.isAlwaysPure
+    case _ =>
+      false
+
 extension (sym: Symbol)
 
-  /** A class is pure if one of its base types has an explicitly declared self type
-   *  with an empty capture set.
+  /** A class is pure if:
+   *   - one its base types has an explicitly declared self type with an empty capture set
+   *   - or it is a value class
+   *   - or it is Nothing or Null
    */
   def isPureClass(using Context): Boolean = sym match
     case cls: ClassSymbol =>
+      val AnyValClass = defn.AnyValClass
       cls.baseClasses.exists(bc =>
-        val selfType = bc.givenSelfType
-        selfType.exists && selfType.captureSet.isAlwaysEmpty)
+        bc == AnyValClass
+        || {
+          val selfType = bc.givenSelfType
+          selfType.exists && selfType.captureSet.isAlwaysEmpty
+        })
+      || cls == defn.NothingClass
+      || cls == defn.NullClass
     case _ =>
       false
 
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 7ae872ac2304..95f2e71437a8 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -120,14 +120,14 @@ extends tpd.TreeTraverser:
         case tp: (TypeRef | AppliedType) =>
           val sym = tp.typeSymbol
           if sym.isClass then
-            tp.typeSymbol == defn.AnyClass
+            sym == defn.AnyClass
               // we assume Any is a shorthand of {*} Any, so if Any is an upper
               // bound, the type is taken to be impure.
           else superTypeIsImpure(tp.superType)
         case tp: (RefinedOrRecType | MatchType) =>
           superTypeIsImpure(tp.underlying)
         case tp: AndType =>
-          superTypeIsImpure(tp.tp1) || canHaveInferredCapture(tp.tp2)
+          superTypeIsImpure(tp.tp1) || needsVariable(tp.tp2)
         case tp: OrType =>
           superTypeIsImpure(tp.tp1) && superTypeIsImpure(tp.tp2)
         case _ =>
@@ -135,23 +135,26 @@ extends tpd.TreeTraverser:
     }.showing(i"super type is impure $tp = $result", capt)
 
     /** Should a capture set variable be added on type `tp`? */
-    def canHaveInferredCapture(tp: Type): Boolean = {
+    def needsVariable(tp: Type): Boolean = {
       tp.typeParams.isEmpty && tp.match
         case tp: (TypeRef | AppliedType) =>
           val tp1 = tp.dealias
-          if tp1 ne tp then canHaveInferredCapture(tp1)
+          if tp1 ne tp then needsVariable(tp1)
           else
             val sym = tp1.typeSymbol
-            if sym.isClass then !sym.isValueClass && sym != defn.AnyClass
+            if sym.isClass then
+              !sym.isPureClass && sym != defn.AnyClass
             else superTypeIsImpure(tp1)
         case tp: (RefinedOrRecType | MatchType) =>
-          canHaveInferredCapture(tp.underlying)
+          needsVariable(tp.underlying)
         case tp: AndType =>
-          canHaveInferredCapture(tp.tp1) && canHaveInferredCapture(tp.tp2)
+          needsVariable(tp.tp1) && needsVariable(tp.tp2)
         case tp: OrType =>
-          canHaveInferredCapture(tp.tp1) || canHaveInferredCapture(tp.tp2)
-        case CapturingType(_, refs) =>
-          refs.isConst && !refs.isUniversal
+          needsVariable(tp.tp1) || needsVariable(tp.tp2)
+        case CapturingType(parent, refs) =>
+          needsVariable(parent)
+          && refs.isConst      // if refs is a variable, no need to add another
+          && !refs.isUniversal // if refs is {*}, an added variable would not change anything
         case _ =>
           false
     }.showing(i"can have inferred capture $tp = $result", capt)
@@ -184,7 +187,7 @@ extends tpd.TreeTraverser:
         CapturingType(OrType(parent1, tp2, tp.isSoft), refs1, tp1.isBoxed)
       case tp @ OrType(tp1, tp2 @ CapturingType(parent2, refs2)) =>
         CapturingType(OrType(tp1, parent2, tp.isSoft), refs2, tp2.isBoxed)
-      case _ if canHaveInferredCapture(tp) =>
+      case _ if needsVariable(tp) =>
         val cs = tp.dealias match
           case CapturingType(_, refs) => CaptureSet.Var(refs.elems)
           case _ => CaptureSet.Var()
diff --git a/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala b/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
index 4b441d512dec..a61701eee2d7 100644
--- a/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
+++ b/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
@@ -149,7 +149,7 @@ class CheckRealizable(using Context) {
    */
   private def boundsRealizability(tp: Type) = {
 
-    val memberProblems = withMode(Mode.CheckBounds) {
+    val memberProblems = withMode(Mode.CheckBoundsOrSelfType) {
       for {
         mbr <- tp.nonClassTypeMembers
         if !(mbr.info.loBound <:< mbr.info.hiBound)
@@ -157,7 +157,7 @@ class CheckRealizable(using Context) {
       yield new HasProblemBounds(mbr.name, mbr.info)
     }
 
-    val refinementProblems = withMode(Mode.CheckBounds) {
+    val refinementProblems = withMode(Mode.CheckBoundsOrSelfType) {
       for {
         name <- refinedNames(tp)
         if (name.isTypeName)
diff --git a/compiler/src/dotty/tools/dotc/core/Mode.scala b/compiler/src/dotty/tools/dotc/core/Mode.scala
index 33ac3de70767..40a45b9f4678 100644
--- a/compiler/src/dotty/tools/dotc/core/Mode.scala
+++ b/compiler/src/dotty/tools/dotc/core/Mode.scala
@@ -70,10 +70,14 @@ object Mode {
   /** We are currently unpickling Scala2 info */
   val Scala2Unpickling: Mode = newMode(13, "Scala2Unpickling")
 
-  /** We are currently checking bounds to be non-empty, so we should not
-   *  do any widening when computing members of refined types.
+  /** Signifies one of two possible situations:
+   *   1. We are currently checking bounds to be non-empty, so we should not
+   *      do any widening when computing members of refined types.
+   *   2. We are currently checking self type conformance, so we should not
+   *      ignore capture sets added to otherwise pure classes (only needed
+   *      for capture checking).
    */
-  val CheckBounds: Mode = newMode(14, "CheckBounds")
+  val CheckBoundsOrSelfType: Mode = newMode(14, "CheckBoundsOrSelfType")
 
   /** Use Scala2 scheme for overloading and implicit resolution */
   val OldOverloadingResolution: Mode = newMode(15, "OldOverloadingResolution")
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index a37fbdd104cf..e823e3c9a72f 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -23,7 +23,7 @@ import typer.ProtoTypes.constrained
 import typer.Applications.productSelectorTypes
 import reporting.trace
 import annotation.constructorOnly
-import cc.{CapturingType, derivedCapturingType, CaptureSet, stripCapturing, isBoxedCapturing, boxed, boxedUnlessFun, boxedIfTypeParam}
+import cc.{CapturingType, derivedCapturingType, CaptureSet, stripCapturing, isBoxedCapturing, boxed, boxedUnlessFun, boxedIfTypeParam, isAlwaysPure}
 
 /** Provides methods to compare types.
  */
@@ -522,6 +522,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       case CapturingType(parent1, refs1) =>
         if tp2.isAny then true
         else if subCaptures(refs1, tp2.captureSet, frozenConstraint).isOK && sameBoxed(tp1, tp2, refs1)
+          || !ctx.mode.is(Mode.CheckBoundsOrSelfType) && tp1.isAlwaysPure
         then recur(parent1, tp2)
         else thirdTry
       case tp1: AnnotatedType if !tp1.isRefining =>
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index 4c52a9bd3ef2..9363b27b4dde 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -615,7 +615,7 @@ object TypeOps:
       boundss: List[TypeBounds],
       instantiate: (Type, List[Type]) => Type,
       app: Type)(
-      using Context): List[BoundsViolation] = withMode(Mode.CheckBounds) {
+      using Context): List[BoundsViolation] = withMode(Mode.CheckBoundsOrSelfType) {
     val argTypes = args.tpes
 
     /** Replace all wildcards in `tps` with `<app>#<tparam>` where `<tparam>` is the
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 4bcd6f0d8de7..732a2fa42fee 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -765,11 +765,11 @@ object Types {
         val rinfo = tp.refinedInfo
         if (name.isTypeName && !pinfo.isInstanceOf[ClassInfo]) { // simplified case that runs more efficiently
           val jointInfo =
-            if rinfo.isInstanceOf[TypeAlias] && !ctx.mode.is(Mode.CheckBounds) then
+            if rinfo.isInstanceOf[TypeAlias] && !ctx.mode.is(Mode.CheckBoundsOrSelfType) then
               // In normal situations, the only way to "improve" on rinfo is to return an empty type bounds
               // So, we do not lose anything essential in "widening" to rinfo.
               // We need to compute the precise info only when checking for empty bounds
-              // which is communicated by the CheckBounds mode.
+              // which is communicated by the CheckBoundsOrSelfType mode.
               rinfo
             else if ctx.base.pendingMemberSearches.contains(name) then
               pinfo safe_& rinfo
diff --git a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
index 5d0a9f55395b..8afcec4dee63 100644
--- a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
+++ b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
@@ -101,20 +101,22 @@ object RefChecks {
    *               is the intersection of the capture sets of all its parents
    */
   def checkSelfAgainstParents(cls: ClassSymbol, parents: List[Symbol])(using Context): Unit =
-    val cinfo = cls.classInfo
-
-    def checkSelfConforms(other: ClassSymbol, category: String, relation: String) =
-      val otherSelf = other.declaredSelfTypeAsSeenFrom(cls.thisType)
-      if otherSelf.exists then
-        if !(cinfo.selfType <:< otherSelf) then
-          report.error(DoesNotConformToSelfType(category, cinfo.selfType, cls, otherSelf, relation, other),
-            cls.srcPos)
-
-    for psym <- parents do
-      checkSelfConforms(psym.asClass, "illegal inheritance", "parent")
-    for reqd <- cls.asClass.givenSelfType.classSymbols do
-      if reqd != cls then
-        checkSelfConforms(reqd, "missing requirement", "required")
+    withMode(Mode.CheckBoundsOrSelfType) {
+      val cinfo = cls.classInfo
+
+      def checkSelfConforms(other: ClassSymbol, category: String, relation: String) =
+        val otherSelf = other.declaredSelfTypeAsSeenFrom(cls.thisType)
+        if otherSelf.exists then
+          if !(cinfo.selfType <:< otherSelf) then
+            report.error(DoesNotConformToSelfType(category, cinfo.selfType, cls, otherSelf, relation, other),
+              cls.srcPos)
+
+      for psym <- parents do
+        checkSelfConforms(psym.asClass, "illegal inheritance", "parent")
+      for reqd <- cls.asClass.givenSelfType.classSymbols do
+        if reqd != cls then
+          checkSelfConforms(reqd, "missing requirement", "required")
+    }
   end checkSelfAgainstParents
 
   /** Check that self type of this class conforms to self types of parents
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index 13aff2661b85..0bd5f1a0ecf2 100644
--- a/tests/neg-custom-args/captures/try.check
+++ b/tests/neg-custom-args/captures/try.check
@@ -10,7 +10,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:43 ------------------------------------------
 29 |  val b = handle[Exception, () -> Nothing] {  // error
    |                                           ^
-   |                                           Found:    ? (x: {*} CT[Exception]) -> {x} () -> ? Nothing
+   |                                           Found:    ? (x: {*} CT[Exception]) -> {x} () -> Nothing
    |                                           Required: CanThrow[Exception] => () -> Nothing
 30 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
 31 |  } {
diff --git a/tests/run-custom-args/captures/colltest5/Test_2.scala b/tests/run-custom-args/captures/colltest5/Test_2.scala
index 934223a9840b..8c070439db80 100644
--- a/tests/run-custom-args/captures/colltest5/Test_2.scala
+++ b/tests/run-custom-args/captures/colltest5/Test_2.scala
@@ -76,7 +76,7 @@ object Test {
     val x4 = xs.head
     val y4: Int = x4
     val x5 = xs.to(List)
-    val y5: {x5} List[Int] = x5
+    val y5: List[Int] = x5
     val (xs6, xs7) = xs.partition(isEven)
     val ys6: {xs6, isEven} View[Int] = xs6
     val ys7: {xs7, isEven} View[Int] = xs7

From f079fe55023b8f1b0e279e11b43c06ffd0665511 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 09:45:03 +0100
Subject: [PATCH 29/37] Enhancement: Add unsafeBoxFunArg operation.

We need an unsafe transform from

    {*} A => B

to

    box {*} A => B

I don't think this is expressible with `unsafeBox/unsafeUnbox` alone.
---
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala   | 15 ++++++++++++---
 .../src/dotty/tools/dotc/core/Definitions.scala   |  1 +
 library/src/scala/caps.scala                      |  5 +++++
 tests/pos-custom-args/captures/foreach.scala      |  4 ++++
 4 files changed, 22 insertions(+), 3 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/foreach.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index ba35157957d4..ffddf1882695 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -337,12 +337,21 @@ class CheckCaptures extends Recheck, SymTransformer:
     override def recheckApply(tree: Apply, pt: Type)(using Context): Type =
       val meth = tree.fun.symbol
       includeCallCaptures(meth, tree.srcPos)
-      if meth == defn.Caps_unsafeBox || meth == defn.Caps_unsafeUnbox then
+      def mapArgUsing(f: Type => Type) =
         val arg :: Nil = tree.args: @unchecked
-        val argType0 = recheckStart(arg, pt)
-          .forceBoxStatus(boxed = meth == defn.Caps_unsafeBox)
+        val argType0 = f(recheckStart(arg, pt))
         val argType = super.recheckFinish(argType0, arg, pt)
         super.recheckFinish(argType, tree, pt)
+
+      if meth == defn.Caps_unsafeBox then
+        mapArgUsing(_.forceBoxStatus(true))
+      else if meth == defn.Caps_unsafeUnbox then
+        mapArgUsing(_.forceBoxStatus(false))
+      else if meth == defn.Caps_unsafeBoxFunArg then
+        mapArgUsing {
+          case defn.FunctionOf(paramtpe :: Nil, restpe, isContectual, isErased) =>
+            defn.FunctionOf(paramtpe.forceBoxStatus(true) :: Nil, restpe, isContectual, isErased)
+        }
       else
         super.recheckApply(tree, pt) match
           case appType @ CapturingType(appType1, refs) =>
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 174244b4a456..e7aea2c89e69 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -963,6 +963,7 @@ class Definitions {
   @tu lazy val CapsModule: Symbol = requiredModule("scala.caps")
     @tu lazy val Caps_unsafeBox: Symbol = CapsModule.requiredMethod("unsafeBox")
     @tu lazy val Caps_unsafeUnbox: Symbol = CapsModule.requiredMethod("unsafeUnbox")
+    @tu lazy val Caps_unsafeBoxFunArg: Symbol = CapsModule.requiredMethod("unsafeBoxFunArg")
     @tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("*")
 
   // Annotation base classes
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 12ab0abd2a21..5f75eeb6a39f 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -17,6 +17,11 @@ import annotation.experimental
    */
   extension [T](x: T) def unsafeUnbox: T = x
 
+  /** If argument is of type `box cs T`, converts to type `cs T`. This
+   *  avoids the error that would be raised when unboxing `*`.
+   */
+  extension [T, U](f: T => U) def unsafeBoxFunArg: T => U = f
+
   /** Mixing in this trait forces a trait or class to be pure, i.e.
    *  have no capabilities retained in its self type.
    */
diff --git a/tests/pos-custom-args/captures/foreach.scala b/tests/pos-custom-args/captures/foreach.scala
new file mode 100644
index 000000000000..ad7c1231b7ca
--- /dev/null
+++ b/tests/pos-custom-args/captures/foreach.scala
@@ -0,0 +1,4 @@
+import caps.*
+def test =
+  val tasks = new collection.mutable.ArrayBuffer[() => Unit]
+  val _: Unit = tasks.foreach(((task: () => Unit) => task()).unsafeBoxFunArg)

From 96bbc1dcec8bb4636c275d19b9f1ad6482de78ff Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 09:46:16 +0100
Subject: [PATCH 30/37] Bugfix: Restore cached denotations of NamedTypes to
 their value before cc

This is needed to make -Ycheck work after capture checking
---
 .../src/dotty/tools/dotc/core/Types.scala     |  5 ++++-
 .../dotty/tools/dotc/transform/Recheck.scala  | 21 +++++++++++++++++--
 .../tools/dotc/transform/TreeChecker.scala    |  2 +-
 .../captures/gadt-ycheck.scala                | 14 +++++++++++++
 4 files changed, 38 insertions(+), 4 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/gadt-ycheck.scala

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 732a2fa42fee..290f9d7b8abf 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -2338,7 +2338,8 @@ object Types {
       lastDenotation match {
         case lastd0: SingleDenotation =>
           val lastd = lastd0.skipRemoved
-          if (lastd.validFor.runId == ctx.runId && (checkedPeriod != Nowhere)) finish(lastd.current)
+          if lastd.validFor.runId == ctx.runId && checkedPeriod != Nowhere then
+            finish(lastd.current)
           else lastd match {
             case lastd: SymDenotation =>
               if (stillValid(lastd) && (checkedPeriod != Nowhere)) finish(lastd.current)
@@ -2443,6 +2444,8 @@ object Types {
     }
 
     private def checkDenot()(using Context) = {}
+      //if name.toString == "getConstructor" then
+      //  println(i"set denot of $this to ${denot.info}, ${denot.getClass}, ${Phases.phaseOf(denot.validFor.lastPhaseId)} at ${ctx.phase}")
 
     private def checkSymAssign(sym: Symbol)(using Context) = {
       def selfTypeOf(sym: Symbol) =
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index b28d0a0a048e..645f83fd28fd 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -133,7 +133,9 @@ abstract class Recheck extends Phase, SymTransformer:
     else sym
 
   def run(using Context): Unit =
-    newRechecker().checkUnit(ctx.compilationUnit)
+    val rechecker = newRechecker()
+    rechecker.checkUnit(ctx.compilationUnit)
+    rechecker.reset()
 
   def newRechecker()(using Context): Rechecker
 
@@ -153,6 +155,12 @@ abstract class Recheck extends Phase, SymTransformer:
      */
     def keepType(tree: Tree): Boolean = keepAllTypes
 
+    private val prevSelDenots = util.HashMap[NamedType, Denotation]()
+
+    def reset()(using Context): Unit =
+      for (ref, mbr) <- prevSelDenots.iterator do
+        ref.withDenot(mbr)
+
     /** Constant-folded rechecked type `tp` of tree `tree` */
     protected def constFold(tree: Tree, tp: Type)(using Context): Type =
       val tree1 = tree.withType(tp)
@@ -190,7 +198,16 @@ abstract class Recheck extends Phase, SymTransformer:
             qualType.findMember(name, qualType,
               excluded = if tree.symbol.is(Private) then EmptyFlags else Private
           )).suchThat(tree.symbol == _))
-        constFold(tree, qualType.select(name, mbr))
+        val newType = tree.tpe match
+          case prevType: NamedType =>
+            val prevDenot = prevType.denot
+            val newType = qualType.select(name, mbr)
+            if (newType eq prevType) && (mbr.info ne prevDenot.info) && !prevSelDenots.contains(prevType) then
+              prevSelDenots(prevType) = prevDenot
+            newType
+          case _ =>
+            qualType.select(name, mbr)
+        constFold(tree, newType)
           //.showing(i"recheck select $qualType . $name : ${mbr.info} = $result")
 
 
diff --git a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
index 6ab0e7fc499f..dc8defa90eef 100644
--- a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
@@ -91,7 +91,7 @@ class TreeChecker extends Phase with SymTransformer {
     if (ctx.phaseId <= erasurePhase.id) {
       val initial = symd.initial
       assert(symd == initial || symd.signature == initial.signature,
-        i"""Signature of ${sym.showLocated} changed at phase ${ctx.phase.prevMega}
+        i"""Signature of ${sym} in ${sym.ownersIterator.toList}%, % changed at phase ${ctx.phase.prevMega}
            |Initial info: ${initial.info}
            |Initial sig : ${initial.signature}
            |Current info: ${symd.info}
diff --git a/tests/pos-custom-args/captures/gadt-ycheck.scala b/tests/pos-custom-args/captures/gadt-ycheck.scala
new file mode 100644
index 000000000000..946763b53e7e
--- /dev/null
+++ b/tests/pos-custom-args/captures/gadt-ycheck.scala
@@ -0,0 +1,14 @@
+package test
+
+import reflect.ClassTag
+import language.experimental.pureFunctions
+
+object Settings:
+  val OptionTag: ClassTag[Option[?]] = ClassTag(classOf[Option[?]])
+
+  class Setting[T: ClassTag](propertyClass: Option[Class[?]]):
+    def tryToSet() =
+      def update(value: Any): String = ???
+      implicitly[ClassTag[T]] match
+        case OptionTag =>
+          update(Some(propertyClass.get.getConstructor().newInstance()))

From 78dc6990b247f6b1248b9655ff05929e1a2722ec Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 09:46:47 +0100
Subject: [PATCH 31/37] Bugfix: Maintain inline context when rechecking

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

diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 645f83fd28fd..0ac9087a08c0 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -314,7 +314,7 @@ abstract class Recheck extends Phase, SymTransformer:
       recheckBlock(tree.stats, tree.expr, pt)
 
     def recheckInlined(tree: Inlined, pt: Type)(using Context): Type =
-      recheckBlock(tree.bindings, tree.expansion, pt)
+      recheckBlock(tree.bindings, tree.expansion, pt)(using inlineContext(tree.call))
 
     def recheckIf(tree: If, pt: Type)(using Context): Type =
       recheck(tree.cond, defn.BooleanType)

From 2d5e9815648e5004b634ef0143a3495512f8bcd0 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 09:47:31 +0100
Subject: [PATCH 32/37] Tweak: Avoid type ascription in uncheckedNN

---
 compiler/src/dotty/tools/package.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/package.scala b/compiler/src/dotty/tools/package.scala
index 57a58151acc7..4ec9ae40c421 100644
--- a/compiler/src/dotty/tools/package.scala
+++ b/compiler/src/dotty/tools/package.scala
@@ -18,7 +18,7 @@ package object tools {
      *  Flow-typing under explicit nulls will automatically insert many necessary
      *  occurrences of uncheckedNN.
      */
-    inline def uncheckedNN: T = x.asInstanceOf[T]
+    transparent inline def uncheckedNN: T = x.asInstanceOf[T]
 
     inline def toOption: Option[T] =
       if x == null then None else Some(x.asInstanceOf[T])

From 0381e2e92e624d201e254320301356d3c63c2e15 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 09:48:47 +0100
Subject: [PATCH 33/37] Enhancement: Move unsafe box/unbox ops into separate
 caps.unsafe module

---
 .../dotty/tools/dotc/core/Definitions.scala   |  7 ++---
 library/src/scala/caps.scala                  | 27 ++++++++++---------
 project/MiMaFilters.scala                     |  1 +
 tests/pos-custom-args/captures/foreach.scala  |  2 +-
 .../captures/unsafe-unbox.scala               |  2 +-
 tests/pos-custom-args/captures/vars1.scala    |  2 +-
 .../no-experimental/dotty-experimental.scala  |  2 +-
 7 files changed, 24 insertions(+), 19 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index e7aea2c89e69..8b7627e969d4 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -961,10 +961,11 @@ class Definitions {
   def RuntimeTupleFunctionsModule(using Context): Symbol = requiredModule("scala.runtime.TupledFunctions")
 
   @tu lazy val CapsModule: Symbol = requiredModule("scala.caps")
-    @tu lazy val Caps_unsafeBox: Symbol = CapsModule.requiredMethod("unsafeBox")
-    @tu lazy val Caps_unsafeUnbox: Symbol = CapsModule.requiredMethod("unsafeUnbox")
-    @tu lazy val Caps_unsafeBoxFunArg: Symbol = CapsModule.requiredMethod("unsafeBoxFunArg")
     @tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("*")
+    @tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe")
+    @tu lazy val Caps_unsafeBox: Symbol = CapsUnsafeModule.requiredMethod("unsafeBox")
+    @tu lazy val Caps_unsafeUnbox: Symbol = CapsUnsafeModule.requiredMethod("unsafeUnbox")
+    @tu lazy val Caps_unsafeBoxFunArg: Symbol = CapsUnsafeModule.requiredMethod("unsafeBoxFunArg")
 
   // Annotation base classes
   @tu lazy val AnnotationClass: ClassSymbol = requiredClass("scala.annotation.Annotation")
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 5f75eeb6a39f..fb1721f98b35 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -7,20 +7,23 @@ import annotation.experimental
   /** The universal capture reference */
   val `*`: Any = ()
 
-  /** If argument is of type `cs T`, converts to type `box cs T`. This
-   *  avoids the error that would be raised when boxing `*`.
-   */
-  extension [T](x: T) def unsafeBox: T = x
+  object unsafe:
 
-  /** If argument is of type `box cs T`, converts to type `cs T`. This
-   *  avoids the error that would be raised when unboxing `*`.
-   */
-  extension [T](x: T) def unsafeUnbox: T = x
+    /** If argument is of type `cs T`, converts to type `box cs T`. This
+     *  avoids the error that would be raised when boxing `*`.
+     */
+    extension [T](x: T) def unsafeBox: T = x
 
-  /** If argument is of type `box cs T`, converts to type `cs T`. This
-   *  avoids the error that would be raised when unboxing `*`.
-   */
-  extension [T, U](f: T => U) def unsafeBoxFunArg: T => U = f
+    /** If argument is of type `box cs T`, converts to type `cs T`. This
+     *  avoids the error that would be raised when unboxing `*`.
+     */
+    extension [T](x: T) def unsafeUnbox: T = x
+
+    /** If argument is of type `box cs T`, converts to type `cs T`. This
+     *  avoids the error that would be raised when unboxing `*`.
+     */
+    extension [T, U](f: T => U) def unsafeBoxFunArg: T => U = f
+  end unsafe
 
   /** Mixing in this trait forces a trait or class to be pure, i.e.
    *  have no capabilities retained in its self type.
diff --git a/project/MiMaFilters.scala b/project/MiMaFilters.scala
index 1221b16e9a44..408930bbeee9 100644
--- a/project/MiMaFilters.scala
+++ b/project/MiMaFilters.scala
@@ -20,5 +20,6 @@ object MiMaFilters {
     ProblemFilters.exclude[MissingClassProblem]("scala.runtime.stdLibPatches.language$experimental$captureChecking$"),
     ProblemFilters.exclude[MissingClassProblem]("scala.caps"),
     ProblemFilters.exclude[MissingClassProblem]("scala.caps$Pure"),
+    ProblemFilters.exclude[MissingClassProblem]("scala.caps$unsafe$"),
   )
 }
diff --git a/tests/pos-custom-args/captures/foreach.scala b/tests/pos-custom-args/captures/foreach.scala
index ad7c1231b7ca..b7dfc49272a9 100644
--- a/tests/pos-custom-args/captures/foreach.scala
+++ b/tests/pos-custom-args/captures/foreach.scala
@@ -1,4 +1,4 @@
-import caps.*
+import caps.unsafe.*
 def test =
   val tasks = new collection.mutable.ArrayBuffer[() => Unit]
   val _: Unit = tasks.foreach(((task: () => Unit) => task()).unsafeBoxFunArg)
diff --git a/tests/pos-custom-args/captures/unsafe-unbox.scala b/tests/pos-custom-args/captures/unsafe-unbox.scala
index e846a7db1b69..b228d8c07925 100644
--- a/tests/pos-custom-args/captures/unsafe-unbox.scala
+++ b/tests/pos-custom-args/captures/unsafe-unbox.scala
@@ -1,4 +1,4 @@
-import caps.*
+import caps.unsafe.*
 def test =
   var finalizeActions = collection.mutable.ListBuffer[() => Unit]()
   val action = finalizeActions.remove(0).unsafeUnbox
diff --git a/tests/pos-custom-args/captures/vars1.scala b/tests/pos-custom-args/captures/vars1.scala
index 53a770563985..c008bac2e72f 100644
--- a/tests/pos-custom-args/captures/vars1.scala
+++ b/tests/pos-custom-args/captures/vars1.scala
@@ -1,4 +1,4 @@
-import caps.*
+import caps.unsafe.*
 
 object Test:
   type ErrorHandler = (Int, String) => Unit
diff --git a/tests/pos-custom-args/no-experimental/dotty-experimental.scala b/tests/pos-custom-args/no-experimental/dotty-experimental.scala
index 74e79c85eaaa..320c68dbea50 100644
--- a/tests/pos-custom-args/no-experimental/dotty-experimental.scala
+++ b/tests/pos-custom-args/no-experimental/dotty-experimental.scala
@@ -1,6 +1,6 @@
 package dotty.tools
 object test {
 
-  val x = caps.unsafeBox
+  val x = caps.unsafe.unsafeBox
 
 }

From 5d7b04355f52018f66553135141d76d96ddbab9e Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 10:08:00 +0100
Subject: [PATCH 34/37] Tweak: Print Ranges like regular types

---
 compiler/src/dotty/tools/dotc/core/Types.scala            | 6 +-----
 compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala | 2 ++
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 290f9d7b8abf..2c59be445010 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -6035,14 +6035,10 @@ object Types {
   /** A range of possible types between lower bound `lo` and upper bound `hi`.
    *  Only used internally in `ApproximatingTypeMap`.
    */
-  case class Range(lo: Type, hi: Type) extends UncachedGroundType {
+  case class Range(lo: Type, hi: Type) extends UncachedGroundType:
     assert(!lo.isInstanceOf[Range])
     assert(!hi.isInstanceOf[Range])
 
-    override def toText(printer: Printer): Text =
-      lo.toText(printer) ~ ".." ~ hi.toText(printer)
-  }
-
   /** Approximate wildcards by their bounds */
   class AvoidWildcardsMap(using Context) extends ApproximatingTypeMap:
     protected def mapWild(t: WildcardType) =
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 60a5c74eedbc..e0c940fd81aa 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -278,6 +278,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
             case ex: Throwable => Str("...")
           }
         "LazyRef(" ~ refTxt ~ ")"
+      case Range(lo, hi) =>
+        toText(lo) ~ ".." ~ toText(hi)
       case _ =>
         tp.fallbackToText(this)
     }

From f07dc95aa198e502b92426450634c2730ee2c416 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 7 Nov 2022 14:55:47 +0100
Subject: [PATCH 35/37] Enhancement: Generalize handling of exceptions to all
 pure base classes

---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala  | 23 +++++++++++--------
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  5 ----
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  6 +++--
 .../dotty/tools/dotc/core/Definitions.scala   |  9 ++++++++
 .../captures/capt-depfun.scala                |  5 ++--
 .../captures/capt-depfun2.scala               |  9 ++++----
 tests/neg-custom-args/captures/cc-this.check  |  9 +++-----
 tests/neg-custom-args/captures/cc-this2.check | 10 ++++----
 .../captures/exception-definitions.check      | 10 +++++---
 .../captures/exception-definitions.scala      |  2 ++
 tests/neg-custom-args/captures/i15116.check   |  4 ++--
 tests/neg-custom-args/captures/try.check      |  2 +-
 tests/neg-custom-args/captures/vars.check     |  4 ++--
 13 files changed, 55 insertions(+), 43 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 3dfd1324ae1e..0ede1825e611 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -185,24 +185,27 @@ extension (tp: Type)
     case _ =>
       false
 
+extension (cls: ClassSymbol)
+
+  def pureBaseClass(using Context): Option[Symbol] =
+    cls.baseClasses.find(bc =>
+      defn.pureBaseClasses.contains(bc)
+      || {
+        val selfType = bc.givenSelfType
+        selfType.exists && selfType.captureSet.isAlwaysEmpty
+      })
+
 extension (sym: Symbol)
 
   /** A class is pure if:
    *   - one its base types has an explicitly declared self type with an empty capture set
    *   - or it is a value class
-   *   - or it is Nothing or Null
+   *   - or it is an exception
+   *   - or it is one of Nothing, Null, or String
    */
   def isPureClass(using Context): Boolean = sym match
     case cls: ClassSymbol =>
-      val AnyValClass = defn.AnyValClass
-      cls.baseClasses.exists(bc =>
-        bc == AnyValClass
-        || {
-          val selfType = bc.givenSelfType
-          selfType.exists && selfType.captureSet.isAlwaysEmpty
-        })
-      || cls == defn.NothingClass
-      || cls == defn.NullClass
+      cls.pureBaseClass.isDefined || defn.pureSimpleClasses.contains(cls)
     case _ =>
       false
 
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index e57cb53cd12d..6bf6d7770d8b 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -326,11 +326,6 @@ object CaptureSet:
   /** Used as a recursion brake */
   @sharable private[dotc] val Pending = Const(SimpleIdentitySet.empty)
 
-  /** The empty capture set with a description that says it's the elf type of an
-   *  exception class.
-   */
-  val emptyOfException: CaptureSet.Const = Const(emptySet, "of an exception class")
-
   def apply(elems: CaptureRef*)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty
     else Const(SimpleIdentitySet(elems.map(_.normalizedRef)*))
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index ffddf1882695..37a16a870f31 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -516,8 +516,10 @@ class CheckCaptures extends Recheck, SymTransformer:
         for param <- cls.paramGetters do
           if !param.hasAnnotation(defn.ConstructorOnlyAnnot) then
             checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3)
-        if cls.derivesFrom(defn.ThrowableClass) then
-          checkSubset(thisSet, CaptureSet.emptyOfException, tree.srcPos)
+        for pureBase <- cls.pureBaseClass do
+          checkSubset(thisSet,
+            CaptureSet.empty.withDescription(i"of pure base class $pureBase"),
+            tree.srcPos)
         super.recheckClassDef(tree, impl, cls)
       finally
         curEnv = saved
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 8b7627e969d4..3373fee9fce6 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -1349,6 +1349,15 @@ class Definitions {
 
   @tu lazy val untestableClasses: Set[Symbol] = Set(NothingClass, NullClass, SingletonClass)
 
+  /** Base classes that are assumed to be pure for the purposes of capture checking.
+   *  Every class inheriting from a pure baseclass is pure.
+   */
+  @tu lazy val pureBaseClasses = Set(defn.AnyValClass, defn.ThrowableClass)
+
+  /** Non-inheritable lasses that are assumed to be pure for the purposes of capture checking,
+   */
+  @tu lazy val pureSimpleClasses = Set(StringClass, NothingClass, NullClass)
+
   @tu lazy val AbstractFunctionType: Array[TypeRef] = mkArityArray("scala.runtime.AbstractFunction", MaxImplementedFunctionArity, 0).asInstanceOf[Array[TypeRef]]
   val AbstractFunctionClassPerRun: PerRun[Array[Symbol]] = new PerRun(AbstractFunctionType.map(_.symbol.asClass))
   def AbstractFunctionClass(n: Int)(using Context): Symbol = AbstractFunctionClassPerRun()(using ctx)(n)
diff --git a/tests/neg-custom-args/captures/capt-depfun.scala b/tests/neg-custom-args/captures/capt-depfun.scala
index a74764f432c7..c01eed7c4b25 100644
--- a/tests/neg-custom-args/captures/capt-depfun.scala
+++ b/tests/neg-custom-args/captures/capt-depfun.scala
@@ -1,8 +1,9 @@
 import annotation.retains
 class C
 type Cap = C @retains(caps.*)
+class Str
 
 def f(y: Cap, z: Cap) =
   def g(): C @retains(y, z) = ???
-  val ac: ((x: Cap) => String @retains(x) => String @retains(x)) = ???
-  val dc: (({y, z} String) => {y, z} String) = ac(g()) // error
+  val ac: ((x: Cap) => Str @retains(x) => Str @retains(x)) = ???
+  val dc: (({y, z} Str) => {y, z} Str) = ac(g()) // error
diff --git a/tests/neg-custom-args/captures/capt-depfun2.scala b/tests/neg-custom-args/captures/capt-depfun2.scala
index 74b9441593c1..52dd74aabf9f 100644
--- a/tests/neg-custom-args/captures/capt-depfun2.scala
+++ b/tests/neg-custom-args/captures/capt-depfun2.scala
@@ -1,11 +1,12 @@
 import annotation.retains
 class C
 type Cap = C @retains(caps.*)
+class Str
 
 def f(y: Cap, z: Cap) =
   def g(): C @retains(y, z) = ???
-  val ac: ((x: Cap) => Array[String @retains(x)]) = ???
-  val dc = ac(g()) // error: Needs explicit type Array[? >: String <: {y, z} String]
+  val ac: ((x: Cap) => Array[Str @retains(x)]) = ???
+  val dc = ac(g()) // error: Needs explicit type Array[? >: Str <: {y, z} Str]
                    // This is a shortcoming of rechecking since the originally inferred
-                   // type is `Array[String]` and the actual type after rechecking
-                   // cannot be expressed as `Array[C String]` for any capture set C
\ No newline at end of file
+                   // type is `Array[Str]` and the actual type after rechecking
+                   // cannot be expressed as `Array[C Str]` for any capture set C
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/cc-this.check b/tests/neg-custom-args/captures/cc-this.check
index c492df15078f..0049f42a5db5 100644
--- a/tests/neg-custom-args/captures/cc-this.check
+++ b/tests/neg-custom-args/captures/cc-this.check
@@ -9,10 +9,7 @@
 10 |  class C2(val x: () => Int): // error
    |               ^
    |        reference (C2.this.x : () => Int) is not included in allowed capture set {} of the self type of class C2
--- [E058] Type Mismatch Error: tests/neg-custom-args/captures/cc-this.scala:17:8 ---------------------------------------
+-- Error: tests/neg-custom-args/captures/cc-this.scala:17:8 ------------------------------------------------------------
 17 |  class C4(val f: () => Int) extends C3 // error
-   |        ^
-   |        illegal inheritance: self type {C4.this.f} C4 of class C4 does not conform to self type C3
-   |        of parent class C3
-   |
-   | longer explanation available when compiling with `-explain`
+   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |  reference (C4.this.f : () => Int) is not included in allowed capture set {} of pure base class class C3
diff --git a/tests/neg-custom-args/captures/cc-this2.check b/tests/neg-custom-args/captures/cc-this2.check
index d10519636ca8..086524d307a2 100644
--- a/tests/neg-custom-args/captures/cc-this2.check
+++ b/tests/neg-custom-args/captures/cc-this2.check
@@ -1,8 +1,6 @@
 
--- [E058] Type Mismatch Error: tests/neg-custom-args/captures/cc-this2/D_2.scala:2:6 -----------------------------------
+-- Error: tests/neg-custom-args/captures/cc-this2/D_2.scala:2:6 --------------------------------------------------------
 2 |class D extends C: // error
-  |      ^
-  |      illegal inheritance: self type {*} D of class D does not conform to self type C
-  |      of parent class C
-  |
-  | longer explanation available when compiling with `-explain`
+  |^
+  |reference (scala.caps.* : Any) is not included in allowed capture set {} of pure base class class C
+3 |  this: {*} D =>
diff --git a/tests/neg-custom-args/captures/exception-definitions.check b/tests/neg-custom-args/captures/exception-definitions.check
index f609580bba4f..aca5d9217d64 100644
--- a/tests/neg-custom-args/captures/exception-definitions.check
+++ b/tests/neg-custom-args/captures/exception-definitions.check
@@ -1,13 +1,17 @@
 -- Error: tests/neg-custom-args/captures/exception-definitions.scala:2:6 -----------------------------------------------
 2 |class Err extends Exception: // error
   |^
-  |reference (scala.caps.* : Any) is not included in allowed capture set {} of an exception class
+  |reference (scala.caps.* : Any) is not included in allowed capture set {} of pure base class class Throwable
 3 |  self: {*} Err =>
+-- Error: tests/neg-custom-args/captures/exception-definitions.scala:10:6 ----------------------------------------------
+10 |class Err4(c: {*} Any) extends AnyVal // error
+   |^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |reference (Err4.this.c : {*} Any) is not included in allowed capture set {} of pure base class class AnyVal
 -- Error: tests/neg-custom-args/captures/exception-definitions.scala:7:12 ----------------------------------------------
 7 |    val x = c  // error
   |            ^
-  |   (c : {*} Any) cannot be referenced here; it is not included in the allowed capture set {} of an exception class
+  |(c : {*} Any) cannot be referenced here; it is not included in the allowed capture set {} of pure base class class Throwable
 -- Error: tests/neg-custom-args/captures/exception-definitions.scala:8:8 -----------------------------------------------
 8 |  class Err3(c: {*} Any) extends Exception // error
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  |  reference (Err3.this.c : {*} Any) is not included in allowed capture set {} of an exception class
+  |  reference (Err3.this.c : {*} Any) is not included in allowed capture set {} of pure base class class Throwable
diff --git a/tests/neg-custom-args/captures/exception-definitions.scala b/tests/neg-custom-args/captures/exception-definitions.scala
index 067f784026e0..9f3539b7febf 100644
--- a/tests/neg-custom-args/captures/exception-definitions.scala
+++ b/tests/neg-custom-args/captures/exception-definitions.scala
@@ -7,4 +7,6 @@ def test(c: {*} Any) =
     val x = c  // error
   class Err3(c: {*} Any) extends Exception // error
 
+class Err4(c: {*} Any) extends AnyVal // error
+
 
diff --git a/tests/neg-custom-args/captures/i15116.check b/tests/neg-custom-args/captures/i15116.check
index 83c552087646..8b8d2d2e091b 100644
--- a/tests/neg-custom-args/captures/i15116.check
+++ b/tests/neg-custom-args/captures/i15116.check
@@ -9,7 +9,7 @@
 5 |  val x = Foo(m)   // error
   |  ^^^^^^^^^^^^^^
   |  Non-local value x cannot have an inferred type
-  |  {Baz.this} Foo{m: {Baz.this} String}
+  |  {Baz.this} Foo{m: {*} String}
   |  with non-empty capture set {Baz.this}.
   |  The type needs to be declared explicitly.
 -- Error: tests/neg-custom-args/captures/i15116.scala:7:6 --------------------------------------------------------------
@@ -23,6 +23,6 @@
 9 |  val x = Foo(m)   // error
   |  ^^^^^^^^^^^^^^
   |  Non-local value x cannot have an inferred type
-  |  {Baz2.this} Foo{m: {Baz2.this} String}
+  |  {Baz2.this} Foo{m: {*} String}
   |  with non-empty capture set {Baz2.this}.
   |  The type needs to be declared explicitly.
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index 0bd5f1a0ecf2..c9cc7f7c1b56 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:23:49 ------------------------------------------
 23 |  val a = handle[Exception, CanThrow[Exception]] { // error
    |                                                 ^
-   |                                                 Found:    ? ({*} CT[Exception]) -> CanThrow[? Exception]
+   |                                                 Found:    ? ({*} CT[Exception]) -> CanThrow[Exception]
    |                                                 Required: CanThrow[Exception] => box {*} CT[Exception]
 24 |    (x: CanThrow[Exception]) => x
 25 |  }{
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
index e4f28fd45e93..8fe72a76493a 100644
--- a/tests/neg-custom-args/captures/vars.check
+++ b/tests/neg-custom-args/captures/vars.check
@@ -9,7 +9,7 @@
 15 |  val u = a  // error
    |          ^
    |          Found:    (a : box {*} String -> String)
-   |          Required: {*} (x$0: ? String) -> ? String
+   |          Required: {*} (x$0: String) -> String
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/vars.scala:16:2 ---------------------------------------------------------------
@@ -25,7 +25,7 @@
 -- Error: tests/neg-custom-args/captures/vars.scala:32:8 ---------------------------------------------------------------
 32 |  local { cap3 => // error
    |  ^
-   |  The expression's type box {*} (x$0: ? String) -> ? String is not allowed to capture the root capability `*`.
+   |  The expression's type box {*} (x$0: String) -> String is not allowed to capture the root capability `*`.
    |  This usually means that a capability persists longer than its allowed lifetime.
 33 |    def g(x: String): String = if cap3 == cap3 then "" else "a"
 34 |    g

From 16b5f4e84fa0cdad9c345ead09226890575e6734 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 10 Nov 2022 12:26:48 +0100
Subject: [PATCH 36/37] Fix typos

---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala  | 2 +-
 compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 37a16a870f31..5a4f1398b165 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -935,7 +935,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         case _ =>
       }
       if !ctx.reporter.errorsReported then
-        // We dont report errors hre if previous errors were reported, because other
+        // We dont report errors here if previous errors were reported, because other
         // errors often result in bad applied types, but flagging these bad types gives
         // often worse error messages than the original errors.
         val checkApplied = new TreeTraverser:
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index e823e3c9a72f..658bf4122aa4 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -829,7 +829,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
               && (recur(tp1.widen.stripCapturing, parent2)
                  || tp1.isInstanceOf[SingletonType] && recur(tp1, parent2)
                     // this alternative is needed in case the right hand side is a
-                    // capturing type that contains the lhs as an |-alternative.
+                    // capturing type that contains the lhs as an alternative of a union type.
                  )
           catch case ex: AssertionError =>
             println(i"assertion failed while compare captured $tp1 <:< $tp2")

From dc4d6c933329182d25250d75ee125aa3a6e28d99 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 10 Nov 2022 13:08:21 +0100
Subject: [PATCH 37/37] Add doc comment to postCheck

---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 1 +
 1 file changed, 1 insertion(+)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 5a4f1398b165..899914e872c8 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -880,6 +880,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      *   - Check that externally visible `val`s or `def`s have empty capture sets. If not,
      *     suggest an explicit type. This is so that separate compilation (where external
      *     symbols have empty capture sets) gives the same results as joint compilation.
+     *   - Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
      */
     def postCheck(unit: tpd.Tree)(using Context): Unit =
       unit.foreachSubTree {