Generalize inferred types check

We now need to also check that fields with inferred types would not contribute
a fresh capability to the implied capture set of the class.

Author: odersky

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

@@ -378,10 +378,15 @@ object Capabilities:
       case tp: SetCapability => tp.captureSetOfInfo.isReadOnly
       case _ => this ne stripReadOnly
 
-    final def restriction(using Context): Symbol = this match
+    /** The classifier, either given in an explicit `.only` or assumed for a
+     *  FreshCap. AnyRef for unclassified FreshCaps. Otherwise NoSymbol if no
+     *  classifier is given.
+     */
+    final def classifier(using Context): Symbol = this match
       case Restricted(_, cls) => cls
-      case ReadOnly(ref1) => ref1.restriction
-      case Maybe(ref1) => ref1.restriction
+      case ReadOnly(ref1) => ref1.classifier
+      case Maybe(ref1) => ref1.classifier
+      case self: FreshCap => self.hiddenSet.classifier
       case _ => NoSymbol
 
     /** Is this a reach reference of the form `x*` or a readOnly or maybe variant
@@ -617,7 +622,7 @@ object Capabilities:
           case Reach(_) =>
             captureSetOfInfo.transClassifiers
           case self: CoreCapability =>
-            if self.derivesFromCapability then toClassifiers(self.classifier)
+            if self.derivesFromCapability then toClassifiers(self.inheritedClassifier)
             else captureSetOfInfo.transClassifiers
         if myClassifiers != UnknownClassifier then
           classifiersValid == currentId

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

@@ -487,7 +487,7 @@ extension (tp: Type)
     case _ =>
       tp
 
-  def classifier(using Context): ClassSymbol =
+  def inheritedClassifier(using Context): ClassSymbol =
     tp.classSymbols.map(_.classifier).foldLeft(defn.AnyClass)(leastClassifier)
 
 extension (tp: MethodType)

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

@@ -40,7 +40,7 @@ object CapturingType:
         apply(parent1, refs ++ refs1, boxed)
       case _ =>
         if parent.derivesFromMutable then refs.associateWithMutable()
-        refs.adoptClassifier(parent.classifier)
+        refs.adoptClassifier(parent.inheritedClassifier)
         AnnotatedType(parent, CaptureAnnotation(refs, boxed)(defn.RetainsAnnot))
 
   /** An extractor for CapturingTypes. Capturing types are recognized if

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

@@ -929,6 +929,17 @@ class CheckCaptures extends Recheck, SymTransformer:
         .showing(i"constr type $mt with $argTypes%, % in $constr = $result", capt)
     end refineConstructorInstance
 
+    /** If `mbr` is a field that has (possibly restricted) FreshCaps in its span capture set,
+     *  their classifiers, otherwise the empty list.
+     */
+    private def classifiersOfFreshInType(mbr: Symbol)(using Context): List[ClassSymbol] =
+      if contributesFreshToClass(mbr) then
+        mbr.info.spanCaptureSet.elems
+          .filter(_.isTerminalCapability)
+          .toList
+          .map(_.classifier.asClass)
+      else Nil
+
     /** The additional capture set implied by the capture sets of its fields. This
      *  is either empty or, if some fields have a terminal capability in their span
      *  capture sets, it consists of a single fresh cap that subsumes all these terminal
@@ -946,16 +957,9 @@ class CheckCaptures extends Recheck, SymTransformer:
        */
       def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match
         case cls: ClassSymbol =>
-          var fieldClassifiers =
-            for
-              sym <- setup.fieldsWithExplicitTypes.getOrElse(cls, cls.info.decls.toList)
-              if contributesFreshToClass(sym)
-              case fresh: FreshCap <- sym.info.spanCaptureSet.elems
-                .filter(_.isTerminalCapability)
-                .map(_.stripReadOnly)
-                .toList
-              _ = pushInfo(i"Note: ${sym.showLocated} captures a $fresh")
-            yield fresh.hiddenSet.classifier
+          var fieldClassifiers = setup.fieldsWithExplicitTypes // pick fields with explicit types for classes in this compilation unit
+              .getOrElse(cls, cls.info.decls.toList)           // pick all symbols in class scope for other classes
+              .flatMap(classifiersOfFreshInType)
           if cls.typeRef.isMutableType then
             fieldClassifiers = defn.Caps_Mutable :: fieldClassifiers
           val parentClassifiers =
@@ -1199,11 +1203,20 @@ class CheckCaptures extends Recheck, SymTransformer:
           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.
-     *  This ensures that if files compile separately, they will also compile
-     *  in a joint compilation.
+    /** Two tests for member definitions with inferred types:
+     *
+     *   1. 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.
+     *      This ensures that if files compile separately, they will also compile
+     *      in a joint compilation.
+     *   2. If a val has an inferred type with a terminal capability in its span capset,
+     *      check that it this capability is subsumed by the capset that was inferred
+     *      for the class from its other fields via `captureSetImpliedByFields`.
+     *      That capset is defined to take into account all fields but is computed
+     *      only from fields with explicitly given types in order to avoid cycles.
+     *      See comment on Setup.fieldsWithExplicitTypes. So we have to make sure
+     *      that fields with inferred types would not change that capset.
      */
     def checkInferredResult(tp: Type, tree: ValOrDefDef)(using Context): Type =
       val sym = tree.symbol
@@ -1238,8 +1251,15 @@ class CheckCaptures extends Recheck, SymTransformer:
           |The new inferred type $tp
           |must conform to this type."""
 
+      def covers(classCapset: CaptureSet, fieldClassifiers: List[ClassSymbol]): Boolean =
+        fieldClassifiers.forall: cls =>
+          classCapset.elems.exists:
+            case fresh: FreshCap => cls.isSubClass(fresh.hiddenSet.classifier)
+            case _ => false
+
       tree.tpt match
         case tpt: InferredTypeTree =>
+          // Test point (1) of doc comment above
           if !sym.isLocalToCompilationUnit && !isExemptFromChecks
             // Symbols that can't be seen outside the compilation unit can have inferred types
           then
@@ -1250,17 +1270,19 @@ class CheckCaptures extends Recheck, SymTransformer:
                 // The check that inferred <: expected is done after recheck so that it
                 // does not interfere with normal rechecking by constraining capture set variables.
             }
-          if !sym.isLocalToCompilationUnitIgnoringPrivate
+          // Test point (2) of doc comment above
+          if sym.owner.isClass && !sym.owner.isStaticOwner
               && 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
             todoAtPostCheck += { () =>
-              if sym.info.spanCaptureSet.containsTerminalCapability then
+              val cls = sym.owner.asClass
+              val fieldClassifiers = classifiersOfFreshInType(sym)
+              val classCapset = captureSetImpliedByFields(cls, cls.appliedRef)
+              if !covers(classCapset, fieldClassifiers) 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.""",
+                      |Fields capturing a root capability need to be given an explicit type unless the capability is already
+                      |subsumed by the computed capability of the enclosing class.""",
                 tpt.srcPos)
             }
         case _ =>

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

@@ -1,10 +1,3 @@
--- 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
    |             ^
@@ -24,7 +17,7 @@
    |              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
+24 |  val count = Ref(): Object^ // error // 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.
@@ -33,3 +26,36 @@
    |               Externally visible type: Object
    |
    |              where:    ^ refers to a fresh root capability created in value count
+-- Error: tests/neg-custom-args/captures/check-inferred.scala:24:11 ----------------------------------------------------
+24 |  val count = Ref(): Object^ // error // error
+   |           ^
+   |           value count needs an explicit type because it captures a root capability in its type Object^.
+   |           Fields capturing a root capability need to be given an explicit type unless the capability is already
+   |           subsumed by the computed capability of the enclosing class.
+   |
+   |           where:    ^ refers to a fresh root capability in the type of value count
+-- Error: tests/neg-custom-args/captures/check-inferred.scala:45:15 ----------------------------------------------------
+45 |  private val y = ??? : A^    // error
+   |               ^
+   |           value y needs an explicit type because it captures a root capability in its type test.A^.
+   |           Fields capturing a root capability need to be given an explicit type unless the capability is already
+   |           subsumed by the computed capability of the enclosing class.
+   |
+   |           where:    ^ refers to a fresh root capability in the type of value y
+-- Error: tests/neg-custom-args/captures/check-inferred.scala:49:15 ----------------------------------------------------
+49 |  private val y = ??? : (() => A^{cap.only[caps.Read]})  // error
+   |               ^
+   | value y needs an explicit type because it captures a root capability in its type () => test.A^{cap.only[Read]}.
+   | Fields capturing a root capability need to be given an explicit type unless the capability is already
+   | subsumed by the computed capability of the enclosing class.
+   |
+   | where:    =>  refers to a fresh root capability in the type of value y
+   |           cap is a fresh root capability created in value y
+-- Error: tests/neg-custom-args/captures/check-inferred.scala:29:21 ----------------------------------------------------
+29 |    private val count = Ref() // error
+   |                     ^
+   |           value count needs an explicit type because it captures a root capability in its type test.Ref^.
+   |           Fields capturing a root capability need to be given an explicit type unless the capability is already
+   |           subsumed by the computed capability of the enclosing class.
+   |
+   |           where:    ^ refers to a fresh root capability classified as Mutable in the type of value count

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

@@ -9,7 +9,7 @@ class Ref extends Mutable:
   update def put(y: Int): Unit = x = y
 
 class Counter:
-  private val count = Ref() // error
+  private val count = Ref()
   private val altCount: Ref^ = Ref() // ok
 
   @untrackedCaptures
@@ -21,14 +21,30 @@ class Counter:
     count.put(count.get - 1)
 
 trait CounterAPI:
-  val count = Ref(): Object^ // error
+  val count = Ref(): Object^ // error // error
   private def count2 = Ref() // ok
 
 def test() =
   class Counter:
-    private val count = Ref() // ok
+    private val count = Ref() // error
     val incr = () =>
       count.put(count.get + 1)
     val decr = () =>
       count.put(count.get - 1)
 
+class A:
+  val x: A^{cap.only[caps.Control]} = ???
+  private val y = ??? : A^{cap.only[caps.Control]}  // ok
+
+class B:
+  val x: A^ = ???
+  private val y = ??? : A^{cap.only[caps.Control]}  // ok
+
+class C:
+  val x: A^{cap.only[caps.Control]} = ???
+  private val y = ??? : A^    // error
+
+class D:
+  val x: A^{cap.only[caps.Control]} = ???
+  private val y = ??? : (() => A^{cap.only[caps.Read]})  // error
+

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

@@ -7,3 +7,11 @@
   |                      Note that capability C.this.c.io is not included in capture set {}.
   |
   | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/i24335.scala:13:7 -------------------------------------------------------------
+13 |  val r = Ref() // error
+   |       ^
+   |       value r needs an explicit type because it captures a root capability in its type Ref^.
+   |       Fields capturing a root capability need to be given an explicit type unless the capability is already
+   |       subsumed by the computed capability of the enclosing class.
+   |
+   |       where:    ^ refers to a fresh root capability classified as Mutable in the type of value r