Tighten level checking

odersky · odersky · commit 9f0527dda1c2 · 2025-05-12T21:35:21.000+02:00
We had the wrong condition in maxSubsumes before. We need to test for isStaticOwner instead
of isStatic. The previous test made all fresh capabilities in global classes slip through the net.
diff --git a/compiler/src/dotty/tools/dotc/cc/CCState.scala b/compiler/src/dotty/tools/dotc/cc/CCState.scala
@@ -118,7 +118,7 @@ class CCState:
 
   private var capIsRoot: Boolean = false
 
-  private var treatFreshAsEqual: Boolean = false
+  private var ignoreFreshLevels: Boolean = false
 
 object CCState:
 
@@ -169,15 +169,15 @@ object CCState:
    *  Asserted in override checking, tested in maxSubsumes.
    *  Is this sound? Test case is neg-custom-args/captures/leaked-curried.scala.
    */
-  inline def withTreatFreshAsEqual[T](op: => T)(using Context): T =
+  inline def ignoringFreshLevels[T](op: => T)(using Context): T =
     if isCaptureCheckingOrSetup then
       val ccs = ccState
-      val saved = ccs.treatFreshAsEqual
-      ccs.treatFreshAsEqual = true
-      try op finally ccs.treatFreshAsEqual = saved
+      val saved = ccs.ignoreFreshLevels
+      ccs.ignoreFreshLevels = true
+      try op finally ccs.ignoreFreshLevels = saved
     else op
 
   /** Should all root.Fresh instances be treated equal? */
-  def treatFreshAsEqual(using Context): Boolean = ccState.treatFreshAsEqual
+  def ignoreFreshLevels(using Context): Boolean = ccState.ignoreFreshLevels
 
 end CCState
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -4,12 +4,13 @@ package cc
 
 import core.*
 import Types.*, Symbols.*, Contexts.*, Annotations.*, Flags.*
-import Names.TermName
+import Names.{Name, TermName}
 import ast.{tpd, untpd}
 import Decorators.*, NameOps.*
 import config.Printers.capt
 import util.Property.Key
 import tpd.*
+import Annotations.Annotation
 import CaptureSet.VarState
 
 /** Attachment key for capturing type trees */
@@ -504,6 +505,10 @@ extension (tp: Type)
     case tp: ThisType => ccState.symLevel(tp.cls).nextInner
     case _ => CCState.undefinedLevel
 
+  def refinedOverride(name: Name, rinfo: Type)(using Context): Type =
+    RefinedType(tp, name,
+      AnnotatedType(rinfo, Annotation(defn.RefineOverrideAnnot, util.Spans.NoSpan)))
+
 extension (tp: MethodType)
   /** A method marks an existential scope unless it is the prefix of a curried method */
   def marksExistentialScope(using Context): Boolean =
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -131,7 +131,7 @@ trait CaptureRef extends TypeProxy, ValueType:
   final def ccOwner(using Context): Symbol = this match
     case root.Fresh(hidden) =>
       hidden.owner
-    case ref: TermRef =>
+    case ref: NamedType =>
       if ref.isCap then NoSymbol
       else ref.prefix match
         case prefix: CaptureRef => prefix.ccOwner
@@ -295,9 +295,9 @@ trait CaptureRef extends TypeProxy, ValueType:
     || this.match
       case x @ root.Fresh(hidden) =>
         def levelOK =
-          if ccConfig.useFreshLevels then
+          if ccConfig.useFreshLevels && !CCState.ignoreFreshLevels then
             val yOwner = y.adjustedOwner
-            yOwner.isStatic || x.ccOwner.isContainedIn(yOwner)
+            yOwner.isStaticOwner || x.ccOwner.isContainedIn(yOwner)
           else
             !y.stripReadOnly.isCap
             && !yIsExistential
@@ -307,7 +307,6 @@ trait CaptureRef extends TypeProxy, ValueType:
         || levelOK
             && canAddHidden
             && vs.addHidden(hidden, y)
-        || ccConfig.useFreshLevels && CCState.treatFreshAsEqual && y.stripReadOnly.isFresh
       case x @ root.Result(binder) =>
         val result = y match
           case y @ root.Result(_) => vs.unify(x, y)
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -209,8 +209,9 @@ sealed abstract class CaptureSet extends Showable:
    */
   def mightAccountFor(x: CaptureRef)(using Context): Boolean =
     reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true):
-      CCState.withCapAsRoot: // OK here since we opportunistically choose an alternative which gets checked later
-        elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded))
+      CCState.withCapAsRoot:
+        CCState.ignoringFreshLevels: // OK here since we opportunistically choose an alternative which gets checked later
+          elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded))
       || !x.isRootCapability
         && {
           val elems = x.captureSetOfInfo.elems
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -843,8 +843,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
           val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol
           if !getter.is(Private) && getter.hasTrackedParts then
-            refined = RefinedType(refined, getterName,
-              AnnotatedType(argType.unboxed, Annotation(defn.RefineOverrideAnnot, util.Spans.NoSpan))) // Yichen you might want to check this
+            refined = refined.refinedOverride(getterName, argType.unboxed) // Yichen you might want to check this
             allCaptures ++= argType.captureSet
         (refined, allCaptures)
 
@@ -1507,9 +1506,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           val cs = actual.captureSet
           if covariant then cs ++ leaked
           else
-            if // CCState.withCapAsRoot: // Not sure withCapAsRoot is OK here, actually
-              !leaked.subCaptures(cs).isOK
-            then
+            if !leaked.subCaptures(cs).isOK then
               report.error(
                 em"""$expected cannot be box-converted to ${actual.capturing(leaked)}
                     |since the additional capture set $leaked resulting from box conversion is not allowed in $actual""", tree.srcPos)
@@ -1708,7 +1705,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       def traverse(t: Tree)(using Context) =
         t match
           case t: Template =>
-            checkAllOverrides(ctx.owner.asClass, OverridingPairsCheckerCC(_, _, t))
+            ignoringFreshLevels:
+              checkAllOverrides(ctx.owner.asClass, OverridingPairsCheckerCC(_, _, t))
           case _ =>
         traverseChildren(t)
     end checkOverrides
@@ -1912,7 +1910,8 @@ class CheckCaptures extends Recheck, SymTransformer:
                   arg.withType(arg.nuType.forceBoxStatus(
                     bounds.hi.isBoxedCapturing | bounds.lo.isBoxedCapturing))
                 CCState.withCapAsRoot: // OK? We need this since bounds use `cap` instead of `fresh`
-                  checkBounds(normArgs, tl)
+                  CCState.ignoringFreshLevels:
+                    checkBounds(normArgs, tl)
                 if ccConfig.postCheckCapturesets then
                   args.lazyZip(tl.paramNames).foreach(checkTypeParam(_, _, fun.symbol))
               case _ =>
@@ -1932,7 +1931,8 @@ class CheckCaptures extends Recheck, SymTransformer:
             case tree: New =>
             case tree: TypeTree =>
               CCState.withCapAsRoot:
-                checkAppliedTypesIn(tree.withType(tree.nuType))
+                CCState.ignoringFreshLevels:
+                  checkAppliedTypesIn(tree.withType(tree.nuType))
             case _ => traverseChildren(t)
         checkApplied.traverse(unit)
     end postCheck
diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -915,7 +915,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           traverseChildren(tree)
           checkValOrDefDef(tree)
         case tree: DefDef =>
-          inSection:
+          if tree.symbol.isInlineMethod then
+            // We currently skip inline method since these seem to generate
+            // spurious recheck completions. Test case is i20237.scala
+            capt.println(i"skipping sep check of inline def ${tree.symbol}")
+          else inSection:
             consumed.segment:
               for params <- tree.paramss; case param: ValDef <- params do
                 pushDef(param, emptyRefs)
diff --git a/compiler/src/dotty/tools/dotc/cc/Synthetics.scala b/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
@@ -77,12 +77,11 @@ object Synthetics:
           case tp: MethodOrPoly =>
             tp.derivedLambdaType(resType = augmentResult(tp.resType))
           case _ =>
-            val refined = trackedParams.foldLeft(tp) { (parent, pref) =>
-              RefinedType(parent, pref.paramName,
+            val refined = trackedParams.foldLeft(tp): (parent, pref) =>
+              parent.refinedOverride(pref.paramName,
                 CapturingType(
                   atPhase(ctx.phase.next)(pref.underlying.stripCapturing),
                   CaptureSet(pref)))
-            }
             CapturingType(refined, CaptureSet(trackedParams*))
         if trackedParams.isEmpty then info
         else augmentResult(info).showing(i"augment apply/copy type $info to $result", capt)
@@ -116,8 +115,7 @@ object Synthetics:
     def transformUnapplyCaptures(info: Type)(using Context): Type = info match
       case info: MethodType =>
         val paramInfo :: Nil = info.paramInfos: @unchecked
-        val newParamInfo = CapturingType(paramInfo,
-          CaptureSet.fresh(root.Origin.UnapplyInstance(info)))
+        val newParamInfo = CapturingType(paramInfo, CaptureSet.universal)
         val trackedParam = info.paramRefs.head
         def newResult(tp: Type): Type = tp match
           case tp: MethodOrPoly =>
diff --git a/compiler/src/dotty/tools/dotc/cc/root.scala b/compiler/src/dotty/tools/dotc/cc/root.scala
@@ -155,7 +155,7 @@ object root:
       case Annot(kind) => this.kind eq kind
       case _ => false
 
-    /** Special treatment of `SubstBindingMaps` which can change the binder of a
+    /** Special treatment of `SubstBindingMaps` which can change the binder of
      *  Result instances
      */
     override def mapWith(tm: TypeMap)(using Context) = kind match
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -868,10 +868,19 @@ object Types extends TypeUtils {
             pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, overridingRefinement)
           else
             val isRefinedMethod = rinfo.isInstanceOf[MethodOrPoly]
-            val joint = pdenot.meet(
-              new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),
-              pre,
-              safeIntersection = ctx.base.pendingMemberSearches.contains(name))
+            val joint = try
+              CCState.ignoringFreshLevels:
+                pdenot.meet(
+                  new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),
+                  pre,
+                  safeIntersection = ctx.base.pendingMemberSearches.contains(name))
+              pdenot.meet(
+                new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),
+                pre,
+                safeIntersection = ctx.base.pendingMemberSearches.contains(name))
+            catch case ex: AssertionError =>
+              println(i"error while do refined $tp . $name, ${pdenot.info} / $rinfo")
+              throw ex
             joint match
               case joint: SingleDenotation
               if isRefinedMethod
diff --git a/compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala b/compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala
@@ -226,7 +226,6 @@ object OverridingPairs:
     else
       member.name.is(DefaultGetterName) // default getters are not checked for compatibility
       ||
-      CCState.withTreatFreshAsEqual:
-        memberTp.overrides(otherTp, member.matchNullaryLoosely || other.matchNullaryLoosely || fallBack)
+      memberTp.overrides(otherTp, member.matchNullaryLoosely || other.matchNullaryLoosely || fallBack)
 
 end OverridingPairs
diff --git a/tests/neg-custom-args/captures/filevar.check b/tests/neg-custom-args/captures/filevar.check
@@ -1,10 +1,27 @@
 -- Error: tests/neg-custom-args/captures/filevar.scala:8:6 -------------------------------------------------------------
-8 |  var file: File^ = uninitialized  // error, was OK under unsealed
+8 |  var file: File^ = uninitialized  // error, under sealed
   |      ^
   |      Mutable variable file cannot have type File^ since
   |      that type captures the root capability `cap`.
   |
   |      where:    ^ refers to a fresh root capability in the type of variable file
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/filevar.scala:15:12 --------------------------------------
+15 |  withFile: f =>       // error with level checking, was OK under both schemes before
+   |            ^
+   |Found:    (l: scala.caps.Capability^{cap.rd}) ?->? File^? ->? Unit
+   |Required: (l: scala.caps.Capability^{cap.rd}) ?-> (f: File^{l}) => Unit
+   |
+   |where:    =>  refers to a root capability associated with the result type of (using l: scala.caps.Capability^{cap.rd}): (f: File^{l}) => Unit
+   |          cap is the universal root capability
+   |
+   |
+   |Note that reference l.type
+   |cannot be included in outer capture set ? of parameter f
+16 |    val o = Service()
+17 |    o.file = f
+18 |    o.log
+   |
+   | longer explanation available when compiling with `-explain`
 -- Warning: tests/neg-custom-args/captures/filevar.scala:11:55 ---------------------------------------------------------
 11 |def withFile[T](op: (l: caps.Capability) ?-> (f: File^{l}) => T): T =
    |                                                       ^
diff --git a/tests/neg-custom-args/captures/filevar.scala b/tests/neg-custom-args/captures/filevar.scala
@@ -5,14 +5,14 @@ class File:
   def write(x: String): Unit = ???
 
 class Service:
-  var file: File^ = uninitialized  // error, was OK under unsealed
+  var file: File^ = uninitialized  // error, under sealed
   def log = file.write("log") // OK, was error under unsealed
 
 def withFile[T](op: (l: caps.Capability) ?-> (f: File^{l}) => T): T =
   op(using caps.cap)(new File)
 
 def test =
-  withFile: f =>
+  withFile: f =>       // error with level checking, was OK under both schemes before
     val o = Service()
     o.file = f
     o.log
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
@@ -72,13 +72,16 @@
    |                                     ^² refers to a fresh root capability in the type of value id
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:63:27 --------------------------------------
-63 |    val f1: File^{id*} = id(f) // error // error
-   |                         ^^^^^
-   |                         Found:    File^
-   |                         Required: File^{id*}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:38 --------------------------------------
+62 |  val leaked = usingFile[File^{id*}]: f => // error // error
+   |                                      ^
+   |Found:    (f: File^?) ->? box File^?
+   |Required: (f: File^) => box File^{id*}
    |
-   |                         where:    ^ refers to a fresh root capability in the type of value id
+   |where:    => refers to a fresh root capability created in value leaked when checking argument to parameter f of method usingFile
+   |          ^  refers to the universal root capability
+63 |    val f1: File^{id*} = id(f)
+64 |    f1
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:67:32 --------------------------------------
@@ -123,13 +126,9 @@
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/reaches.scala:62:31 -----------------------------------------------------------
-62 |  val leaked = usingFile[File^{id*}]: f => // error
+62 |  val leaked = usingFile[File^{id*}]: f => // error // error
    |                               ^^^
    |                               id* cannot be tracked since its deep capture set is empty
--- Error: tests/neg-custom-args/captures/reaches.scala:63:18 -----------------------------------------------------------
-63 |    val f1: File^{id*} = id(f) // error // error
-   |                  ^^^
-   |                  id* cannot be tracked since its deep capture set is empty
 -- Error: tests/neg-custom-args/captures/reaches.scala:70:31 -----------------------------------------------------------
 70 |  val leaked = usingFile[File^{id*}]: f => // error // error
    |                               ^^^
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
@@ -59,8 +59,8 @@ def attack2 =
   val id: File^ -> File^ = x => x // error
     // val id: File^ -> File^{fresh}
 
-  val leaked = usingFile[File^{id*}]: f => // error
-    val f1: File^{id*} = id(f) // error // error
+  val leaked = usingFile[File^{id*}]: f => // error // error
+    val f1: File^{id*} = id(f)
     f1
 
 def attack3 =
diff --git a/tests/neg-custom-args/captures/scoped-caps.check b/tests/neg-custom-args/captures/scoped-caps.check
@@ -98,23 +98,11 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:26:20 ----------------------------------
 26 |  val _: A^ => B^ = x => g2(x)  // error: g2(x): B^{g2, x}, and the `x` cannot be subsumed by fresh
    |                    ^^^^^^^^^^
-   |                    Found:    (x: A^) ->{g2} B^²
-   |                    Required: (x: A^) => B^³
+   |                    Found:    (x: A^) ->{g2} B^{g2, x}
+   |                    Required: (x: A^) => B^²
    |
    |                    where:    => refers to a fresh root capability in the type of value _$13
    |                              ^  refers to the universal root capability
-   |                              ^² refers to a root capability associated with the result type of (x: A^): B^²
-   |                              ^³ refers to a fresh root capability in the type of value _$13
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:28:24 ----------------------------------
-28 |  val _: A^{io} => B^ = x => g3(x)  // error, fails level checking of fresh instances
-   |                        ^^^^^^^^^^
-   |                     Found:    (x: A^{io}) ->{g3} B^
-   |                     Required: (x: A^{io}) => B^²
-   |
-   |                     where:    => refers to a fresh root capability in the type of value _$14
-   |                               ^  refers to a root capability associated with the result type of (x: A^{io}): B^
-   |                               ^² refers to a fresh root capability in the type of value _$14
+   |                              ^² refers to a fresh root capability in the type of value _$13
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/scoped-caps.scala b/tests/neg-custom-args/captures/scoped-caps.scala
@@ -25,4 +25,4 @@ def test(io: Object^): Unit =
   val g2: A^ => B^ = ???
   val _: A^ => B^ = x => g2(x)  // error: g2(x): B^{g2, x}, and the `x` cannot be subsumed by fresh
   val g3: A^ => B^ = ???
-  val _: A^{io} => B^ = x => g3(x)  // error, fails level checking of fresh instances
+  val _: A^{io} => B^ = x => g3(x)  // ok, now g3(x): B^{g3, x}, which is widened to B^{g3, io}
