Don't allow instantiated ResultCaps to subsume anything

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

@@ -148,10 +148,25 @@ object Capabilities:
    *  @param origin  an indication where and why the FreshCap was created, used
    *                 for diagnostics
    */
-  case class FreshCap private (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability:
-    val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked)
+  case class FreshCap(val prefix: Type)
+      (val owner: Symbol, val origin: Origin, origHidden: CaptureSet.HiddenSet | Null)
+      (using @constructorOnly ctx: Context)
+  extends RootCapability:
+    val hiddenSet =
+      if origHidden == null then CaptureSet.HiddenSet(owner, this: @unchecked)
+      else origHidden
       // fails initialization check without the @unchecked
 
+    def derivedFreshCap(newPrefix: Type)(using Context): FreshCap =
+      if newPrefix eq prefix then this
+      else if newPrefix eq hiddenSet.owningCap.prefix then
+        hiddenSet.owningCap
+      else
+        hiddenSet.derivedCaps
+          .getOrElseUpdate(newPrefix, FreshCap(newPrefix)(owner, origin, hiddenSet))
+
+    //assert(rootId != 10, i"fresh $prefix, ${ctx.owner}")
+
     /** Is this fresh cap (definitely) classified? If that's the case, the
      *  classifier cannot be changed anymore.
      *  We need to distinguish `FreshCap`s that can still be classified from
@@ -198,8 +213,10 @@ object Capabilities:
       i"a fresh root capability$classifierStr$originStr"
 
   object FreshCap:
+    def apply(prefix: Type, origin: Origin)(using Context): FreshCap =
+      new FreshCap(prefix)(ctx.owner, origin, null)
     def apply(origin: Origin)(using Context): FreshCap =
-      FreshCap(ctx.owner, origin)
+      apply(ctx.owner.skipWeakOwner.thisType, origin)
 
   /** A root capability associated with a function type. These are conceptually
    *  existentially quantified over the function's result type.
@@ -703,12 +720,24 @@ object Capabilities:
       (this eq y)
       || this.match
         case x: FreshCap =>
+          def classifierOK =
+            if y.tryClassifyAs(x.hiddenSet.classifier) then true
+            else
+              capt.println(i"$y cannot be classified as $x")
+              false
+
+          def prefixAllowsAddHidden: Boolean = x.prefix match
+            case NoPrefix | _: ThisType => true
+            case _ if CCState.collapseFresh => true
+            case pre =>
+              capt.println(i"fresh not open $x, ${x.rootId}, $pre, ${x.ccOwner.skipWeakOwner.thisType}")
+              false
+
           vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y)))
           || x.acceptsLevelOf(y)
-              && ( y.tryClassifyAs(x.hiddenSet.classifier)
-                   || { capt.println(i"$y cannot be classified as $x"); false }
-              )
+              && classifierOK
               && canAddHidden
+              && prefixAllowsAddHidden
               && vs.addHidden(x.hiddenSet, y)
         case x: ResultCap =>
           val result = y match
@@ -1031,7 +1060,13 @@ object Capabilities:
       override def mapCapability(c: Capability, deep: Boolean) = c match
         case c @ ResultCap(binder) =>
           if localBinders.contains(binder) then c // keep bound references
-          else seen.getOrElseUpdate(c, FreshCap(origin)) // map free references to FreshCap
+          else
+            // Create a fresh skolem that does not subsume anything
+            def freshSkolem =
+              val c = FreshCap(origin)
+              c.hiddenSet.markSolved(provisional = false)
+              c
+            seen.getOrElseUpdate(c, freshSkolem) // map free references to FreshCap
         case _ => super.mapCapability(c, deep)
     end subst
 

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

@@ -25,6 +25,30 @@ case class CaptureAnnotation(refs: CaptureSet, boxed: Boolean)(cls: Symbol) exte
   import CaptureAnnotation.*
   import tpd.*
 
+  private var myOrigins: Set[AnnotatedType] | Null = null
+
+  def origins: Set[AnnotatedType] =
+    if myOrigins == null then myOrigins = Set()
+    myOrigins.nn
+
+  def withOrigins(origins: Set[AnnotatedType]): CaptureAnnotation =
+    if myOrigins == null then
+      myOrigins = origins
+      this
+    else if origins.subsetOf(myOrigins.nn) then
+      this
+    else
+      CaptureAnnotation(refs, boxed)(cls).withOrigins(myOrigins.nn ++ origins)
+
+  private var myProvenance: Set[AnnotatedType] | Null = null
+
+  def provenance: Set[AnnotatedType] =
+    if myProvenance == null then
+      myProvenance = origins ++ origins.flatMap:
+        case AnnotatedType(_, ann: CaptureAnnotation) => ann.provenance
+        case _ => Set()
+    myProvenance.nn
+
   /** A cache for the version of this annotation which differs in its boxed status. */
   var boxDual: CaptureAnnotation | Null = null
 

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

@@ -179,14 +179,23 @@ extension (tp: Type)
         && !cs.keepAlways
     then tp
     else tp match
-      case CapturingType(parent, cs1) => parent.capturing(cs1 ++ cs)
+      case tp @ CapturingType(parent, cs1) => parent.capturing(cs1 ++ cs).withOrigin(tp)
       case _ => CapturingType(tp, cs)
 
+  def withOrigins(origins: Set[AnnotatedType])(using Context) = tp match
+    case tp @ AnnotatedType(p, ann: CaptureAnnotation) =>
+      tp.derivedAnnotatedType(p, ann.withOrigins(origins))
+    case _ =>
+      tp
+
+  def withOrigin(origin: AnnotatedType)(using Context) =
+    withOrigins(Set(origin))
+
   /** @pre `tp` is a CapturingType */
   def derivedCapturingType(parent: Type, refs: CaptureSet)(using Context): Type = tp match
     case tp @ CapturingType(p, r) =>
       if (parent eq p) && (refs eq r) then tp
-      else CapturingType(parent, refs, tp.isBoxed)
+      else CapturingType(parent, refs, tp.isBoxed).withOrigin(tp)
 
   /** If this is a unboxed capturing type with nonempty capture set, its boxed version.
    *  Or, if type is a TypeBounds of capturing types, the version where the bounds are boxed.
@@ -196,7 +205,7 @@ extension (tp: Type)
     case tp @ CapturingType(parent, refs) if !tp.isBoxed && !refs.isAlwaysEmpty =>
       tp.annot match
         case ann: CaptureAnnotation if !parent.derivesFrom(defn.Caps_CapSet) =>
-          AnnotatedType(parent, ann.boxedAnnot)
+          AnnotatedType(parent, ann.boxedAnnot).withOrigin(tp)
         case ann => tp
     case tp: RealTypeBounds =>
       tp.derivedTypeBounds(tp.lo.boxed, tp.hi.boxed)
@@ -209,7 +218,7 @@ extension (tp: Type)
    */
   def unboxed(using Context): Type = tp.dealias match
     case tp @ CapturingType(parent, refs) if tp.isBoxed && !refs.isAlwaysEmpty =>
-      CapturingType(parent, refs)
+      CapturingType(parent, refs).withOrigin(tp)
     case tp: RealTypeBounds =>
       tp.derivedTypeBounds(tp.lo.unboxed, tp.hi.unboxed)
     case _ =>
@@ -303,7 +312,7 @@ extension (tp: Type)
         case ref: Capability if ref.isTracked || ref.isInstanceOf[DerivedCapability] =>
           ref.singletonCaptureSet
         case _ => refs
-      CapturingType(parent, refs1, boxed)
+      CapturingType(parent, refs1, boxed).withOrigin(tp)
     case _ =>
       tp
 

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

@@ -12,7 +12,7 @@ import annotation.internal.sharable
 import reporting.trace
 import printing.{Showable, Printer}
 import printing.Texts.*
-import util.{SimpleIdentitySet, Property}
+import util.{SimpleIdentitySet, Property, EqHashMap}
 import typer.ErrorReporting.Addenda
 import scala.collection.{mutable, immutable}
 import TypeComparer.ErrorNote
@@ -559,8 +559,10 @@ object CaptureSet:
   def universal(using Context): Const =
     Const(SimpleIdentitySet(GlobalCap))
 
+  def fresh(prefix: Type, origin: Origin)(using Context): Const =
+    FreshCap(prefix, origin).singletonCaptureSet
   def fresh(origin: Origin)(using Context): Const =
-    FreshCap(origin).singletonCaptureSet
+    fresh(ctx.owner.thisType, origin)
 
   /** The shared capture set `{cap.rd}` */
   def shared(using Context): Const =
@@ -1166,6 +1168,9 @@ object CaptureSet:
 
     override def owner = givenOwner
 
+    /** The FreshCaps generated by derivedFreshCap, indexed by prefix */
+    val derivedCaps = new EqHashMap[Type, FreshCap]()
+
     //assert(id != 3)
 
     description = i"of elements subsumed by a fresh cap in $initialOwner"
@@ -1206,6 +1211,7 @@ object CaptureSet:
       if alias ne this then alias.add(elem)
       else
         def addToElems() =
+          assert(!isConst)
           includeElem(elem)
           deps.foreach: dep =>
             assert(dep != this)
@@ -1378,8 +1384,10 @@ object CaptureSet:
      *  but the special state VarState.Separate overrides this.
      */
     def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean =
-      hidden.add(elem)(using ctx, this)
-      true
+      if hidden.isConst then false
+      else
+        hidden.add(elem)(using ctx, this)
+        true
 
     /** If root1 and root2 belong to the same binder but have different originalBinders
      *  it means that one of the roots was mapped to the binder of the other by a

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

@@ -37,7 +37,7 @@ object CapturingType:
     if refs.isAlwaysEmpty && !refs.keepAlways then parent
     else parent match
       case parent @ CapturingType(parent1, refs1) if boxed || !parent.isBoxed =>
-        apply(parent1, refs ++ refs1, boxed)
+        apply(parent1, refs ++ refs1, boxed).withOrigin(parent)
       case _ =>
         if parent.derivesFromMutable then refs.setMutable()
         refs.adoptClassifier(parent.classifier)

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

@@ -204,25 +204,27 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     /** Pull out an embedded capture set from a part of `tp` */
     def normalizeCaptures(tp: Type)(using Context): Type = tp match
       case tp @ RefinedType(parent @ CapturingType(parent1, refs), rname, rinfo) =>
-        CapturingType(tp.derivedRefinedType(parent1, rname, rinfo), refs, parent.isBoxed)
+        CapturingType(tp.derivedRefinedType(parent1, rname, rinfo), refs, parent.isBoxed).withOrigin(parent)
       case tp: RecType =>
         tp.parent match
           case parent @ CapturingType(parent1, refs) =>
-            CapturingType(tp.derivedRecType(parent1), refs, parent.isBoxed)
+            CapturingType(tp.derivedRecType(parent1), refs, parent.isBoxed).withOrigin(parent)
           case _ =>
             tp // can return `tp` here since unlike RefinedTypes, RecTypes are never created
                 // by `mapInferred`. Hence if the underlying type admits capture variables
                 // a variable was already added, and the first case above would apply.
       case AndType(tp1 @ CapturingType(parent1, refs1), tp2 @ CapturingType(parent2, refs2)) =>
         assert(tp1.isBoxed == tp2.isBoxed)
         CapturingType(AndType(parent1, parent2), refs1 ** refs2, tp1.isBoxed)
+          .withOrigins(Set(tp1, tp2))
       case tp @ OrType(tp1 @ CapturingType(parent1, refs1), tp2 @ CapturingType(parent2, refs2)) =>
         assert(tp1.isBoxed == tp2.isBoxed)
         CapturingType(OrType(parent1, parent2, tp.isSoft), refs1 ++ refs2, tp1.isBoxed)
+          .withOrigins(Set(tp1, tp2))
       case tp @ OrType(tp1 @ CapturingType(parent1, refs1), tp2) =>
-        CapturingType(OrType(parent1, tp2, tp.isSoft), refs1, tp1.isBoxed)
+        CapturingType(OrType(parent1, tp2, tp.isSoft), refs1, tp1.isBoxed).withOrigin(tp1)
       case tp @ OrType(tp1, tp2 @ CapturingType(parent2, refs2)) =>
-        CapturingType(OrType(tp1, parent2, tp.isSoft), refs2, tp2.isBoxed)
+        CapturingType(OrType(tp1, parent2, tp.isSoft), refs2, tp2.isBoxed).withOrigin(tp2)
       case tp @ AppliedType(tycon, args)
       if !defn.isFunctionClass(tp.dealias.typeSymbol) && (tp.dealias eq tp) =>
         tp.derivedAppliedType(tycon, args.mapConserve(_.boxDeeply))
@@ -266,19 +268,18 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           tp.typeSymbol match
             case cls: ClassSymbol
             if !defn.isFunctionClass(cls) && cls.is(CaptureChecked) =>
-              cls.paramGetters.foldLeft(tp) { (core, getter) =>
-                if atPhase(thisPhase.next)(getter.hasTrackedParts)
-                    && getter.isRefiningParamAccessor
-                    && !refiningNames.contains(getter.name) // Don't add a refinement if we have already an explicit one for the same name
-                then
-                  val getterType =
-                    mapInferred(refine = false)(tp.memberInfo(getter)).strippedDealias
-                  RefinedType(core, getter.name,
-                      CapturingType(getterType, new CaptureSet.RefiningVar(ctx.owner)))
-                    .showing(i"add capture refinement $tp --> $result", capt)
-                else
-                  core
-              }
+                cls.paramGetters.foldLeft(tp): (core, getter) =>
+                  if atPhase(thisPhase.next)(getter.hasTrackedParts)
+                      && getter.isRefiningParamAccessor
+                      && !refiningNames.contains(getter.name) // Don't add a refinement if we have already an explicit one for the same name
+                  then
+                    val getterType =
+                      mapInferred(refine = false)(tp.memberInfo(getter)).strippedDealias
+                    RefinedType(core, getter.name,
+                        CapturingType(getterType, new CaptureSet.RefiningVar(ctx.owner)))
+                      .showing(i"add capture refinement $tp --> $result", capt)
+                  else
+                    core
             case _ => tp
         case _ => tp
 
@@ -694,7 +695,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                   if cls.derivesFrom(defn.Caps_Capability) then
                     // If cls is a capability class, we need to add a fresh readonly capability to
                     // ensure we cannot treat the class as pure.
-                    CaptureSet.fresh(Origin.InDecl(cls)).readOnly.subCaptures(cs)
+                    CaptureSet.fresh(cls.thisType, Origin.InDecl(cls)).readOnly.subCaptures(cs)
                   CapturingType(cinfo.selfType, cs)
 
               // Compute new parent types

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

@@ -54,7 +54,7 @@ object ccConfig:
 
   /** Not used currently. Handy for trying out new features */
   def newScheme(using ctx: Context): Boolean =
-    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
+    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.9`)
 
   def allowUse(using Context): Boolean =
     Feature.sourceVersion.stable.isAtMost(SourceVersion.`3.7`)

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

@@ -719,7 +719,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         compareRefined
       case tp2: RecType =>
         def compareRec = tp1.safeDealias match {
-          case tp1: RecType =>
+          case tp1: RecType =>    // TODO this is now also in firstTry, needed here?
             val rthis1 = tp1.recThis
             recur(tp1.parent, tp2.parent.substRecThis(tp2, rthis1))
           case NoType => false

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

@@ -6312,6 +6312,8 @@ object Types extends TypeUtils {
         null
 
     def mapCapability(c: Capability, deep: Boolean = false): Capability | (CaptureSet, Boolean) = c match
+      case c @ FreshCap(prefix) =>
+        c.derivedFreshCap(apply(prefix))
       case c: RootCapability => c
       case Reach(c1) =>
         mapCapability(c1, deep = true)

compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

@@ -39,6 +39,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
   private var elideCapabilityCaps = false
 
   private var openRecs: List[RecType] = Nil
+  private var referredRecs: Set[RecType] = Set.empty
 
   protected def maxToTextRecursions: Int = 100
 
@@ -260,11 +261,15 @@ class PlainPrinter(_ctx: Context) extends Printer {
           refinementChain(tp).reverse: @unchecked
         toTextLocal(parent) ~ "{" ~ Text(refined map toTextRefinement, "; ").close ~ "}"
       case tp: RecType =>
-        try {
+        try
           openRecs = tp :: openRecs
-          "{" ~ selfRecName(openRecs.length) ~ " => " ~ toTextGlobal(tp.parent) ~ "}"
-        }
-        finally openRecs = openRecs.tail
+          val parentTxt = toTextGlobal(tp.parent)
+          if referredRecs.contains(tp) || printDebug
+          then "{" ~ selfRecName(openRecs.length) ~ " => " ~ parentTxt ~ "}"
+          else parentTxt
+        finally
+          referredRecs -= openRecs.head
+          openRecs = openRecs.tail
       case AndType(tp1, tp2) =>
         changePrec(AndTypePrec) { toText(tp1) ~ " & " ~ atPrec(AndTypePrec + 1) { toText(tp2) } }
       case OrType(tp1, tp2) =>
@@ -457,7 +462,9 @@ class PlainPrinter(_ctx: Context) extends Printer {
         ParamRefNameString(pref) ~ hashStr(pref.binder)
       case tp: RecThis =>
         val idx = openRecs.reverse.indexOf(tp.binder)
-        if (idx >= 0) selfRecName(idx + 1)
+        if idx >= 0 then
+          referredRecs += tp.binder
+          selfRecName(idx + 1)
         else "{...}.this" // TODO move underlying type to an addendum, e.g. ... z3 ... where z3: ...
       case tp: SkolemType =>
         def reprStr = toText(tp.repr) ~ hashStr(tp)
@@ -489,8 +496,13 @@ class PlainPrinter(_ctx: Context) extends Printer {
       def classified =
         if c.hiddenSet.classifier == defn.AnyClass then ""
         else s" classified as ${c.hiddenSet.classifier.name.show}"
-      if ccVerbose then s"<fresh$idStr in ${c.ccOwner} hiding " ~ toTextCaptureSet(c.hiddenSet) ~ classified ~ ">"
-      else "cap"
+      def prefixTxt: Text = c.prefix match
+        case NoPrefix | _: ThisType => ""
+        case pre => pre.show ~ "."
+      def core: Text =
+        if ccVerbose then s"<fresh$idStr in ${c.ccOwner} hiding " ~ toTextCaptureSet(c.hiddenSet) ~ classified ~ ">"
+        else "cap"
+      prefixTxt ~ core
     case tp: TypeProxy =>
       homogenize(tp) match
         case tp: SingletonType => toTextRef(tp)

tests/neg-custom-args/captures/frozen-result.scala

@@ -0,0 +1,9 @@
+class B
+
+def Test(consume b1: B^, consume b2: B^) =
+  def f(): B^ = B()
+  var x: B^ = f()
+  x = b1 // error separation but should be OK, see #23889
+  var y = f()
+  y = b2 // error
+