Normalize fresh caps in result types

odersky · odersky · commit 7a7f7477a60f · 2025-10-01T20:22:23.000+02:00
Ensure that capset variables in types of vals and result types of
non-anonymous functions contain only a single FreshCap, and furthermore
that that FreshCap has as origin InDecl(owner), where owner is the val
or def for which the type is defined.
diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -147,7 +147,7 @@ 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:
+  case class FreshCap (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability:
     val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked)
       // fails initialization check without the @unchecked
 
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -777,7 +777,7 @@ object CaptureSet:
           assert(elem.subsumes(elem1),
             i"Skipped map ${tm.getClass} maps newly added $elem to $elem1 in $this")
 
-    protected def includeElem(elem: Capability)(using Context): Unit =
+    protected def includeElem(elem: Capability)(using Context, VarState): Unit =
       if !elems.contains(elem) then
         if debugVars && id == debugTarget then
           println(i"###INCLUDE $elem in $this")
@@ -803,7 +803,10 @@ object CaptureSet:
         // id == 108 then assert(false, i"trying to add $elem to $this")
         assert(elem.isWellformed, elem)
         assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState])
-        includeElem(elem)
+        try includeElem(elem)
+        catch case ex: AssertionError =>
+          println(i"error for incl $elem in $this, ${summon[VarState].toString}")
+          throw ex
         if isBadRoot(elem) then
           rootAddedHandler()
         val normElem = if isMaybeSet then elem else elem.stripMaybe
@@ -947,16 +950,66 @@ object CaptureSet:
     override def toString = s"Var$id$elems"
   end Var
 
-  /** Variables that represent refinements of class parameters can have the universal
-   *  capture set, since they represent only what is the result of the constructor.
-   *  Test case: Without that tweak, logger.scala would not compile.
-   */
-  class RefiningVar(owner: Symbol)(using Context) extends Var(owner):
-    override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) = this
+  inline val strictFreshLevels = true
 
   /** Variables created in types of inferred type trees */
-  class ProperVar(override val owner: Symbol, initialElems: Refs, nestedOK: Boolean)(using /*@constructorOnly*/ ictx: Context)
-  extends Var(owner, initialElems, nestedOK)
+  class ProperVar(override val owner: Symbol, initialElems: Refs = emptyRefs, nestedOK: Boolean = true, isRefining: Boolean)(using /*@constructorOnly*/ ictx: Context)
+  extends Var(owner, initialElems, nestedOK):
+
+    /** Make sure that capset variables in types of vals and result types of
+     *  non-anonymous functions contain only a single FreshCap, and furthermore
+     *  that that FreshCap has as origin InDecl(owner), where owner is the val
+     *  or def for which the type is defined.
+     *  Note: This currently does not apply to classified or read-only fresh caps.
+     */
+    override def includeElem(elem: Capability)(using ctx: Context, vs: VarState): Unit = elem match
+      case elem: FreshCap
+      if !nestedOK
+          && !elems.contains(elem)
+          && !owner.isAnonymousFunction
+          && ccConfig.newScheme =>
+        def fail = i"attempting to add $elem to $this"
+        def hideIn(fc: FreshCap): Unit =
+          assert(elem.tryClassifyAs(fc.hiddenSet.classifier), fail)
+          if strictFreshLevels && !isRefining then
+            // If a variable is added by addCaptureRefinements in a synthetic
+            // refinement of a class type, don't do level checking. The problem is
+            // that the variable might be matched against a type that does not have
+            // a refinement, in which case FreshCaps of the class definition would
+            // leak out in the corresponding places. This will fail level checking.
+            // The disallowBadRoots override below has a similar reason.
+            // TODO: We should instead mark the variable as impossible to instantiate
+            // and drop the refinement later in the inferred type.
+            // Test case is drop-refinement.scala.
+            assert(fc.acceptsLevelOf(elem),
+              i"level failure, cannot add $elem with ${elem.levelOwner} to $owner / $getClass / $fail")
+          fc.hiddenSet.add(elem)
+        val isSubsumed = (false /: elems): (isSubsumed, prev) =>
+          prev match
+            case prev: FreshCap =>
+              hideIn(prev)
+              true
+            case _ => isSubsumed
+        if !isSubsumed then
+          if elem.origin != Origin.InDecl(owner) || elem.hiddenSet.isConst then
+            val fc = new FreshCap(owner, Origin.InDecl(owner))
+            assert(fc.tryClassifyAs(elem.hiddenSet.classifier), fail)
+            hideIn(fc)
+            super.includeElem(fc)
+          else
+            super.includeElem(elem)
+      case _ =>
+        super.includeElem(elem)
+
+    /** Variables that represent refinements of class parameters can have the universal
+     *  capture set, since they represent only what is the result of the constructor.
+     *  Test case: Without that tweak, logger.scala would not compile.
+     */
+    override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) =
+      if isRefining then this
+      else super.disallowBadRoots(upto)(handler)
+
+  end ProperVar
 
   /** A variable that is derived from some other variable via a map or filter. */
   abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1376,7 +1376,10 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  where local capture roots are instantiated to root variables.
      */
     override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type =
-      testAdapted(actual, expected, tree, addenda)(err.typeMismatch)
+      try testAdapted(actual, expected, tree, addenda)(err.typeMismatch)
+      catch case ex: AssertionError =>
+        println(i"error while checking $tree: $actual against $expected")
+        throw ex
 
     @annotation.tailrec
     private def findImpureUpperBound(tp: Type)(using Context): Type = tp match
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -252,7 +252,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     *  Polytype bounds are only cleaned using step 1, but not otherwise transformed.
     */
   private def transformInferredType(tp: Type)(using Context): Type =
-    def mapInferred(refine: Boolean): TypeMap = new TypeMap with SetupTypeMap:
+    def mapInferred(inCaptureRefinement: Boolean): TypeMap = new TypeMap with SetupTypeMap:
       override def toString = "map inferred"
 
       var refiningNames: Set[Name] = Set()
@@ -262,23 +262,23 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
        *  where CV_1, ..., CV_n are fresh capture set variables.
        */
       def addCaptureRefinements(tp: Type): Type = tp match
-        case _: TypeRef | _: AppliedType if refine && tp.typeParams.isEmpty =>
+        case _: TypeRef | _: AppliedType if !inCaptureRefinement && tp.typeParams.isEmpty =>
           tp.typeSymbol match
             case cls: ClassSymbol
             if !defn.isFunctionClass(cls) && cls.is(CaptureChecked) =>
-              cls.paramGetters.foldLeft(tp) { (core, getter) =>
+              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
+                    mapInferred(inCaptureRefinement = true)(tp.memberInfo(getter)).strippedDealias
                   RefinedType(core, getter.name,
-                      CapturingType(getterType, new CaptureSet.RefiningVar(ctx.owner)))
+                      CapturingType(getterType,
+                        CaptureSet.ProperVar(ctx.owner, isRefining = true)))
                     .showing(i"add capture refinement $tp --> $result", capt)
                 else
                   core
-              }
             case _ => tp
         case _ => tp
 
@@ -302,11 +302,12 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
             mapFollowingAliases(tp)
         addVar(
           addCaptureRefinements(normalizeCaptures(normalizeFunctions(tp1, tp))),
-          ctx.owner)
+          ctx.owner,
+          isRefining = inCaptureRefinement)
     end mapInferred
 
     try
-      val tp1 = mapInferred(refine = true)(tp)
+      val tp1 = mapInferred(inCaptureRefinement = false)(tp)
       val tp2 = toResultInResults(NoSymbol, _ => assert(false))(tp1)
       if tp2 ne tp then capt.println(i"expanded inferred in ${ctx.owner}: $tp  -->  $tp1  -->  $tp2")
       tp2
@@ -685,7 +686,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                 // Infer the self type for the rest, which is all classes without explicit
                 // self types (to which we also add nested module classes), provided they are
                 // neither pure, nor are publicily extensible with an unconstrained self type.
-                val cs = CaptureSet.ProperVar(cls, CaptureSet.emptyRefs, nestedOK = false)
+                val cs = CaptureSet.ProperVar(cls, CaptureSet.emptyRefs, nestedOK = false, isRefining = false)
                 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.
@@ -851,8 +852,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
       else maybeAdd(tp, tp)
 
   /** Add a capture set variable to `tp` if necessary. */
-  private def addVar(tp: Type, owner: Symbol)(using Context): Type =
-    decorate(tp, CaptureSet.ProperVar(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner)))
+  private def addVar(tp: Type, owner: Symbol, isRefining: Boolean)(using Context): Type =
+    decorate(tp, CaptureSet.ProperVar(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner), isRefining))
 
   /** A map that adds <fluid> capture sets at all contra- and invariant positions
    *  in a type where a capture set would be needed. This is used to make types
diff --git a/tests/neg-custom-args/captures/cc-this5.check b/tests/neg-custom-args/captures/cc-this5.check
@@ -1,8 +1,3 @@
--- Error: tests/neg-custom-args/captures/cc-this5.scala:16:20 ----------------------------------------------------------
-16 |    def f = println(c)  // error
-   |                    ^
-   |                    reference (c : Cap) is not included in the allowed capture set {}
-   |                    of the enclosing class A
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-this5.scala:21:15 -------------------------------------
 21 |    val x: A = this // error
    |               ^^^^
diff --git a/tests/neg-custom-args/captures/cc-this5.scala b/tests/neg-custom-args/captures/cc-this5.scala
@@ -13,7 +13,7 @@ def foo(c: Cap) =
 def test(c: Cap) =
   class A:
     val x: A = this
-    def f = println(c)  // error
+    def f = println(c)
 
 def test2(c: Cap) =
   class A:
diff --git a/tests/neg-custom-args/captures/i23726.check b/tests/neg-custom-args/captures/i23726.check
@@ -13,7 +13,7 @@
    |  Footprint set of function result      : {a}
    |  The two sets overlap at               : {a}
    |
-   |where:    ^  refers to a fresh root capability classified as Mutable created in value a when constructing mutable Ref
+   |where:    ^  refers to a fresh root capability classified as Mutable in the type of value a
    |          ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
 -- Error: tests/neg-custom-args/captures/i23726.scala:15:5 -------------------------------------------------------------
 15 |  f3(b)  // error
@@ -30,7 +30,7 @@
    |  Footprint set of function result      : {op, b}
    |  The two sets overlap at               : {b}
    |
-   |where:    ^  refers to a fresh root capability classified as Mutable created in value b when constructing mutable Ref
+   |where:    ^  refers to a fresh root capability classified as Mutable in the type of value b
    |          ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
 -- Error: tests/neg-custom-args/captures/i23726.scala:23:5 -------------------------------------------------------------
 23 |  f7(a)  // error
@@ -47,5 +47,5 @@
    |  Footprint set of function prefix      : {f7*, a, b}
    |  The two sets overlap at               : {a}
    |
-   |where:    ^  refers to a fresh root capability classified as Mutable created in value a when constructing mutable Ref
+   |where:    ^  refers to a fresh root capability classified as Mutable in the type of value a
    |          ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
diff --git a/tests/neg-custom-args/captures/reference-cc.check b/tests/neg-custom-args/captures/reference-cc.check
@@ -1,8 +1,3 @@
--- Error: tests/neg-custom-args/captures/reference-cc.scala:42:20 ------------------------------------------------------
-42 |    def f = println(c)  // error
-   |                    ^
-   |                    reference (c : Cap) is not included in the allowed capture set {}
-   |                    of the enclosing class A
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:44:29 ---------------------------------
 44 |  val later = usingLogFile { file => () => file.write(0) } // error
    |                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/neg-custom-args/captures/reference-cc.scala b/tests/neg-custom-args/captures/reference-cc.scala
@@ -39,7 +39,7 @@ class Cap extends caps.SharedCapability
 def test(c: Cap) =
   class A:
     val x: A = this
-    def f = println(c)  // error
+    def f = println(c)
 
   val later = usingLogFile { file => () => file.write(0) } // error
   later() // crash
diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.check b/tests/neg-custom-args/captures/scope-extrude-mut.check
@@ -1,15 +1,15 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scope-extrude-mut.scala:9:8 ------------------------------
 9 |    a = a1  // error
   |        ^^
-  |Found:    (a1 : A^)
-  |Required: A^²
+  |        Found:    (a1 : A^)
+  |        Required: A^²
   |
-  |Note that capability cap is not included in capture set {cap²}
-  |because cap in method b is not visible from cap² in variable a.
+  |        Note that capability cap is not included in capture set {cap²}
+  |        because cap in method b is not visible from cap² in variable a.
   |
-  |where:    ^    refers to a fresh root capability classified as Mutable created in value a1 when constructing mutable A
-  |          ^²   refers to a fresh root capability classified as Mutable in the type of variable a
-  |          cap  is a fresh root capability classified as Mutable created in value a1 when constructing mutable A
-  |          cap² is a fresh root capability classified as Mutable in the type of variable a
+  |        where:    ^    refers to a fresh root capability classified as Mutable in the type of value a1
+  |                  ^²   refers to a fresh root capability classified as Mutable in the type of variable a
+  |                  cap  is a fresh root capability classified as Mutable in the type of value a1
+  |                  cap² is a fresh root capability classified as Mutable in the type of variable a
   |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check
@@ -1,11 +1,12 @@
 -- Error: tests/neg-custom-args/captures/sep-counter.scala:12:19 -------------------------------------------------------
 12 |  def mkCounter(): Pair[Ref^, Ref^] =  // error
    |                   ^^^^^^^^^^^^^^^^
-   | Separation failure in method mkCounter's result type Pair[Ref^, Ref^²].
-   | One part,  Ref^, hides capabilities  {c, cap}.
-   | Another part,  Ref^²,  captures capabilities  {c, cap}.
-   | The two sets overlap at  {c}.
+   |Separation failure in method mkCounter's result type Pair[Ref^, Ref^²].
+   |One part,  Ref^, hides capabilities  {c, cap, cap²}.
+   |Another part,  Ref^²,  captures capabilities  {c, cap, cap²}.
+   |The two sets overlap at  {c}.
    |
-   | where:    ^   refers to a fresh root capability classified as Mutable in the result type of method mkCounter
-   |           ^²  refers to a fresh root capability classified as Mutable in the result type of method mkCounter
-   |           cap is a fresh root capability classified as Mutable created in value c when constructing mutable Ref
+   |where:    ^    refers to a fresh root capability classified as Mutable in the result type of method mkCounter
+   |          ^²   refers to a fresh root capability classified as Mutable in the result type of method mkCounter
+   |          cap  is a fresh root capability classified as Mutable in the type of value c
+   |          cap² is a fresh root capability classified as Mutable created in value c when constructing mutable Ref
diff --git a/tests/new/test.scala b/tests/new/test.scala
@@ -1,9 +1 @@
-object e:
-  def foldRL(f: Int => Int)(g: String => Int) = ???
-
-
-val xs = e.foldRL
-  : i => i + 1
-  : s => s.length
-
-
+object Test
diff --git a/tests/pos-custom-args/captures/drop-refinement.scala b/tests/pos-custom-args/captures/drop-refinement.scala
@@ -0,0 +1,18 @@
+import scala.annotation.unchecked.uncheckedVariance
+
+private final class ConcatIterator[+A](val from: Iterator[A @uncheckedVariance]^) {
+  self: ConcatIterator[A]^ =>
+  def hasNext: Boolean = ???
+  def next(): A = ???
+
+  def concat[B >: A](that: => IterableOnce[B]^): ConcatIterator[B]^{this, that} = {
+    val c = new ConcatIteratorCell[B](that, null).asInstanceOf[ConcatIteratorCell[A]]
+      // crashes without special exemption for isRefining in CaptureSet.ProperVar$includeElem.
+    this
+  }
+}
+
+private final class ConcatIteratorCell[A](head: => IterableOnce[A]^, var tail: ConcatIteratorCell[A]^) {
+  def headIterator: Iterator[A]^{this} = head.iterator
+}
+
