Refine checking if fields with inferred types

Private fields in publicly accessible classes that contribute fresh caps to their
class still need an explicitly declared type, so that separate compilation can work.

Author: odersky

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

@@ -194,6 +194,11 @@ object CheckCaptures:
     check.traverse(tp)
   end disallowBadRootsIn
 
+  private def contributesFreshToClass(sym: Symbol)(using Context): Boolean =
+    sym.isField
+    && !sym.isOneOf(DeferredOrTermParamOrAccessor)
+    && !sym.hasAnnotation(defn.UntrackedCapturesAnnot)
+
   private def ownerStr(owner: Symbol)(using Context): String =
     if owner.isAnonymousFunction then "enclosing function" else owner.show
 
@@ -918,8 +923,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             val fieldClassifiers =
               for
                 sym <- cls.info.decls.toList
-                if sym.isField && !sym.isOneOf(DeferredOrTermParamOrAccessor)
-                    && !sym.hasAnnotation(defn.UntrackedCapturesAnnot)
+                if contributesFreshToClass(sym)
                 case fresh: FreshCap <- sym.info.spanCaptureSet.elems
                   .filter(_.isTerminalCapability)
                   .map(_.stripReadOnly)
@@ -1160,15 +1164,15 @@ class CheckCaptures extends Recheck, SymTransformer:
     def checkInferredResult(tp: Type, tree: ValOrDefDef)(using Context): Type =
       val sym = tree.symbol
 
-      def canUseInferred =    // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
-        sym.isLocalToCompilationUnit      // Symbols that can't be seen outside the compilation unit can always have inferred types
-        || ctx.owner.enclosingPackageClass.isEmptyPackage
-                                          // We make an exception for symbols in the empty package.
-                                          // these could theoretically be accessed from other files in the empty package, but
-                                          // usually it would be too annoying to require explicit 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.
+      def isExemptFromChecks =
+        ctx.owner.enclosingPackageClass.isEmptyPackage
+          // We make an exception for symbols in the empty package.
+          // these could theoretically be accessed from other files in the empty package, but
+          // usually it would be too annoying to require explicit 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.
 
       def fail(tree: Tree, expected: Type, addenda: Addenda): Unit =
         def maybeResult = if sym.is(Method) then " result" else ""
@@ -1191,14 +1195,28 @@ class CheckCaptures extends Recheck, SymTransformer:
           |must conform to this type."""
 
       tree.tpt match
-        case tpt: InferredTypeTree if !canUseInferred =>
-          val expected = tpt.tpe.dropAllRetains
-          todoAtPostCheck += { () =>
-            withCapAsRoot:
-              testAdapted(tp, expected, tree.rhs, addenda(expected))(fail)
-              // The check that inferred <: expected is done after recheck so that it
-              // does not interfere with normal rechecking by constraining capture set variables.
-          }
+        case tpt: InferredTypeTree if !isExemptFromChecks =>
+          if !sym.isLocalToCompilationUnit
+             // Symbols that can't be seen outside the compilation unit can have inferred types
+             // except for the else clause below.
+          then
+            val expected = tpt.tpe.dropAllRetains
+            todoAtPostCheck += { () =>
+              withCapAsRoot:
+                testAdapted(tp, expected, tree.rhs, addenda(expected))(fail)
+                // The check that inferred <: expected is done after recheck so that it
+                // does not interfere with normal rechecking by constraining capture set variables.
+            }
+          else if sym.is(Private) && !sym.isLocalToCompilationUnitIgnoringPrivate
+              && contributesFreshToClass(sym)
+              // Private symbols capturing a root capability need explicit types
+              // so that we can compute field constributions to class instance
+              // capture sets across compilation units.
+          then
+            report.error(
+              em"""$sym needs an explicit type because it captures a root capability in its type ${tree.tpt.nuType}.
+                  |Fields of publicily accessible classes that capture a root capability need to be given an explicit type.""",
+            tpt.srcPos)
         case _ =>
       tp
     end checkInferredResult

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

@@ -1248,11 +1248,13 @@ object SymDenotations {
       || isClass
         && (!isOneOf(EffectivelyOpenFlags) || isLocalToCompilationUnit)
 
-    final def isLocalToCompilationUnit(using Context): Boolean =
-      is(Private)
-      || owner.ownersIterator.takeWhile(!_.isStaticOwner).exists(_.isTerm)
+    final def isLocalToCompilationUnitIgnoringPrivate(using Context): Boolean =
+      owner.ownersIterator.takeWhile(!_.isStaticOwner).exists(_.isTerm)
       || accessBoundary(defn.RootClass).isProperlyContainedIn(symbol.topLevelClass)
 
+    final def isLocalToCompilationUnit(using Context): Boolean =
+      is(Private) || isLocalToCompilationUnitIgnoringPrivate
+
     final def isTransparentClass(using Context): Boolean =
       is(TransparentType) || defn.isAssumedTransparent(symbol)
 

tests/neg-custom-args/captures/check-inferred.check

@@ -0,0 +1,35 @@
+-- Error: tests/neg-custom-args/captures/check-inferred.scala:12:19 ----------------------------------------------------
+12 |  private val count = Ref() // error
+   |                   ^
+   |        value count needs an explicit type because it captures a root capability in its type test.Ref^.
+   |        Fields of publicily accessible classes that capture a root capability need to be given an explicit type.
+   |
+   |        where:    ^ refers to a fresh root capability classified as Mutable in the type of value count
+-- Error: tests/neg-custom-args/captures/check-inferred.scala:18:13 ----------------------------------------------------
+18 |  val incr = () => // error
+   |             ^
+   |             value incr needs an explicit type because the inferred type does not conform to
+   |             the type that is externally visible in other compilation units.
+   |
+   |              Inferred type          : () ->{Counter.this.count} Unit
+   |              Externally visible type: () -> Unit
+19 |    count.put(count.get + 1)
+-- Error: tests/neg-custom-args/captures/check-inferred.scala:20:13 ----------------------------------------------------
+20 |  val decr = () => // error
+   |             ^
+   |             value decr needs an explicit type because the inferred type does not conform to
+   |             the type that is externally visible in other compilation units.
+   |
+   |              Inferred type          : () ->{Counter.this.count} Unit
+   |              Externally visible type: () -> Unit
+21 |    count.put(count.get - 1)
+-- Error: tests/neg-custom-args/captures/check-inferred.scala:24:14 ----------------------------------------------------
+24 |  val count = Ref(): Object^ // error
+   |              ^^^^^^^^^^^^^^
+   |              value count needs an explicit type because the inferred type does not conform to
+   |              the type that is externally visible in other compilation units.
+   |
+   |               Inferred type          : Object^
+   |               Externally visible type: Object
+   |
+   |              where:    ^ refers to a fresh root capability created in value count

tests/neg-custom-args/captures/check-inferred.scala

@@ -0,0 +1,33 @@
+package test
+import caps.Mutable
+import caps.cap
+import caps.unsafe.untrackedCaptures
+
+class Ref extends Mutable:
+  var x = 0
+  def get: Int = x
+  update def put(y: Int): Unit = x = y
+
+class Counter:
+  private val count = Ref() // error
+  private val altCount: Ref^ = Ref() // ok
+
+  @untrackedCaptures
+  private val altAltCount = Ref() // ok
+
+  val incr = () => // error
+    count.put(count.get + 1)
+  val decr = () => // error
+    count.put(count.get - 1)
+
+trait CounterAPI:
+  val count = Ref(): Object^ // error
+
+def test() =
+  class Counter:
+    private val count = Ref() // ok
+    val incr = () =>
+      count.put(count.get + 1)
+    val decr = () =>
+      count.put(count.get - 1)
+