Expand Capability types T to T^ only if no explicit capture set is given

compiler/src/dotty/tools/dotc/cc/CaptureOps.scala

@@ -528,9 +528,11 @@ extension (cls: ClassSymbol)
                                  // and err on the side of impure.
               && selfType.exists && selfType.captureSet.isAlwaysEmpty
 
-  def baseClassHasExplicitSelfType(using Context): Boolean =
+  def baseClassHasExplicitNonUniversalSelfType(using Context): Boolean =
     cls.baseClasses.exists: bc =>
-      bc.is(CaptureChecked) && bc.givenSelfType.exists
+      bc.is(CaptureChecked)
+      && bc.givenSelfType.exists
+      && !bc.givenSelfType.captureSet.isUniversal
 
   def matchesExplicitRefsInBaseClass(refs: CaptureSet)(using Context): Boolean =
     cls.baseClasses.tail.exists: bc =>

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -632,7 +632,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
           var refined: Type = core
           var allCaptures: CaptureSet =
-            if core.derivesFromCapability then CaptureSet.universal else initCs
+            if core.derivesFromCapability then defn.universalCSImpliedByCapability else initCs
           for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
             val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol
             if !getter.is(Private) && getter.hasTrackedParts then
@@ -809,7 +809,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         val localSet = capturedVars(sym)
         if !localSet.isAlwaysEmpty then
           curEnv = Env(sym, EnvKind.Regular, localSet, curEnv)
-          
+
         // ctx with AssumedContains entries for each Contains parameter
         val bodyCtx =
           var ac = CaptureSet.assumedContains
@@ -828,7 +828,7 @@ class CheckCaptures extends Recheck, SymTransformer:
               interpolateVarsIn(tree.tpt)
             curEnv = saved
     end recheckDefDef
-    
+
     /** If val or def definition with inferred (result) type is visible
      *  in other compilation units, check that the actual inferred type
      *  conforms to the expected type where all inferred capture sets are dropped.

compiler/src/dotty/tools/dotc/cc/Setup.scala

@@ -299,24 +299,32 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           CapturingType(fntpe, cs, boxed = false)
         else fntpe
 
+      def stripImpliedCaptureSet(tp: Type): Type = tp match
+        case tp @ CapturingType(parent, refs)
+        if (refs eq defn.universalCSImpliedByCapability) && !tp.isBoxedCapturing =>
+          parent
+        case tp @ CapturingType(parent, refs) => tp
+        case _ => tp
+
       def apply(t: Type) =
         t match
           case t @ CapturingType(parent, refs) =>
-            t.derivedCapturingType(this(parent), refs)
+            t.derivedCapturingType(stripImpliedCaptureSet(this(parent)), refs)
           case t @ AnnotatedType(parent, ann) =>
             val parent1 = this(parent)
             if ann.symbol.isRetains then
+              val parent2 = stripImpliedCaptureSet(parent1)
               for tpt <- tptToCheck do
-                checkWellformedLater(parent1, ann.tree, tpt)
-              CapturingType(parent1, ann.tree.toCaptureSet)
+                checkWellformedLater(parent2, ann.tree, tpt)
+              CapturingType(parent2, ann.tree.toCaptureSet)
             else
               t.derivedAnnotatedType(parent1, ann)
           case throwsAlias(res, exc) =>
             this(expandThrowsAlias(res, exc, Nil))
           case t =>
             // Map references to capability classes C to C^
             if t.derivesFromCapability && !t.isSingleton && t.typeSymbol != defn.Caps_Exists
-            then CapturingType(t, CaptureSet.universal, boxed = false)
+            then CapturingType(t, defn.universalCSImpliedByCapability, boxed = false)
             else normalizeCaptures(mapOver(t))
     end toCapturing
 
@@ -570,7 +578,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                 else if cls.isPureClass then
                   // is cls is known to be pure, nothing needs to be added to self type
                   selfInfo
-                else if !cls.isEffectivelySealed && !cls.baseClassHasExplicitSelfType then
+                else if !cls.isEffectivelySealed && !cls.baseClassHasExplicitNonUniversalSelfType then
                   // assume {cap} for completely unconstrained self types of publicly extensible classes
                   CapturingType(cinfo.selfType, CaptureSet.universal)
                 else

compiler/src/dotty/tools/dotc/core/Definitions.scala

@@ -1005,6 +1005,9 @@ class Definitions {
     @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains")
     @tu lazy val Caps_containsImpl: TermSymbol = CapsModule.requiredMethod("containsImpl")
 
+  /** The same as CaptureSet.universal but generated implicitly for references of Capability subtypes */
+  @tu lazy val universalCSImpliedByCapability = CaptureSet(captureRoot.termRef)
+
   @tu lazy val PureClass: Symbol = requiredClass("scala.Pure")
 
   // Annotation base classes

scala2-library-cc/src/scala/collection/IndexedSeqView.scala

@@ -16,13 +16,10 @@ package collection
 import scala.annotation.nowarn
 import language.experimental.captureChecking
 
-trait IndexedSeqViewOps[+A, +CC[_], +C] extends Any with SeqViewOps[A, CC, C] {
-  self: IndexedSeqViewOps[A, CC, C]^ =>
-}
+trait IndexedSeqViewOps[+A, +CC[_], +C] extends Any with SeqViewOps[A, CC, C]
 
 /** View defined in terms of indexing a range */
 trait IndexedSeqView[+A] extends IndexedSeqViewOps[A, View, View[A]] with SeqView[A] {
-  self: IndexedSeqView[A]^ =>
 
   override def view: IndexedSeqView[A]^{this} = this
 

scala2-library-cc/src/scala/collection/SeqView.scala

@@ -25,7 +25,6 @@ import scala.annotation.unchecked.uncheckedCaptures
  *  mapping a SeqView with an impure function gives an impure view).
  */
 trait SeqViewOps[+A, +CC[_], +C] extends Any with IterableOps[A, CC, C] {
-  self: SeqViewOps[A, CC, C]^ =>
 
   def length: Int
   def apply(x: Int): A
@@ -75,7 +74,6 @@ trait SeqViewOps[+A, +CC[_], +C] extends Any with IterableOps[A, CC, C] {
 }
 
 trait SeqView[+A] extends SeqViewOps[A, View, View[A]] with View[A] {
-  self: SeqView[A]^ =>
 
   override def view: SeqView[A]^{this} = this
 

tests/pos-custom-args/captures/cap-refine.scala

@@ -0,0 +1,12 @@
+//> using options -Werror
+import caps.Capability
+
+trait Buffer[T] extends Capability:
+  def append(x: T): this.type
+
+def f(buf: Buffer[Int]) =
+  val buf1 = buf.append(1).append(2)
+  val buf2: Buffer[Int]^{buf1} = buf1
+
+
+