Implement inheritance condition for Mutable types

odersky · odersky · commit c43976ba047e · 2025-10-25T15:33:46.000+03:00
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -890,7 +890,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         var allCaptures: CaptureSet =
           if core.derivesFromCapability
           then initCs ++ FreshCap(Origin.NewCapability(core)).singletonCaptureSet
-          else initCs ++ impliedByFields(core)
+          else initCs ++ captureSetImpliedByFields(cls, core)
         for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
           val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol
           if !getter.is(Private) && getter.hasTrackedParts then
@@ -914,57 +914,57 @@ class CheckCaptures extends Recheck, SymTransformer:
           val (refined, cs) = addParamArgRefinements(core, initCs)
           refined.capturing(cs)
 
-      /** 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
-       *  capabiltities. Class parameters are not counted.
-       */
-      def impliedByFields(core: Type): CaptureSet =
-        var infos: List[String] = Nil
-        def pushInfo(msg: => String) =
-          if ctx.settings.YccVerbose.value then infos = msg :: infos
-
-        /** The classifiers of the fresh caps in the span capture sets of all fields
-         *  in the given class `cls`.
-         */
-        def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match
-          case cls: ClassSymbol =>
-            val fieldClassifiers =
-              for
-                sym <- 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
-            val parentClassifiers =
-              cls.parentSyms.map(impliedClassifiers).filter(_.nonEmpty)
-            if fieldClassifiers.isEmpty && parentClassifiers.isEmpty
-            then Nil
-            else parentClassifiers.foldLeft(fieldClassifiers.distinct)(dominators)
-          case _ => Nil
-
-        def fresh =
-          FreshCap(Origin.NewInstance(core)).tap: fresh =>
-            if ctx.settings.YccVerbose.value then
-              pushInfo(i"Note: instance of $cls captures a $fresh that comes from a field")
-              report.echo(infos.mkString("\n"), ctx.owner.srcPos)
-
-        knownFresh.getOrElseUpdate(cls, impliedClassifiers(cls)) match
-          case Nil => CaptureSet.empty
-          case cl :: Nil =>
-            val result = fresh
-            result.hiddenSet.adoptClassifier(cl)
-            result.singletonCaptureSet
-          case _ => fresh.singletonCaptureSet
-      end impliedByFields
-
       augmentConstructorType(resType, capturedVars(cls))
         .showing(i"constr type $mt with $argTypes%, % in $constr = $result", capt)
     end refineConstructorInstance
 
+    /** 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
+     *  capabiltities. Class parameters are not counted.
+     */
+    def captureSetImpliedByFields(cls: ClassSymbol, core: Type)(using Context): CaptureSet =
+      var infos: List[String] = Nil
+      def pushInfo(msg: => String) =
+        if ctx.settings.YccVerbose.value then infos = msg :: infos
+
+      /** The classifiers of the fresh caps in the span capture sets of all fields
+       *  in the given class `cls`.
+       */
+      def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match
+        case cls: ClassSymbol =>
+          val fieldClassifiers =
+            for
+              sym <- 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
+          val parentClassifiers =
+            cls.parentSyms.map(impliedClassifiers).filter(_.nonEmpty)
+          if fieldClassifiers.isEmpty && parentClassifiers.isEmpty
+          then Nil
+          else parentClassifiers.foldLeft(fieldClassifiers.distinct)(dominators)
+        case _ => Nil
+
+      def fresh =
+        FreshCap(Origin.NewInstance(core)).tap: fresh =>
+          if ctx.settings.YccVerbose.value then
+            pushInfo(i"Note: instance of $cls captures a $fresh that comes from a field")
+            report.echo(infos.mkString("\n"), ctx.owner.srcPos)
+
+      knownFresh.getOrElseUpdate(cls, impliedClassifiers(cls)) match
+        case Nil => CaptureSet.empty
+        case cl :: Nil =>
+          val result = fresh
+          result.hiddenSet.adoptClassifier(cl)
+          result.singletonCaptureSet
+        case _ => fresh.singletonCaptureSet
+    end captureSetImpliedByFields
+
     /** Recheck type applications:
      *   - Map existential captures in result to `cap`
      *   - include captures of called methods in environment
@@ -2138,10 +2138,40 @@ class CheckCaptures extends Recheck, SymTransformer:
       end for
     end checkEscapingUses
 
-    /** Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
+    /** Check all parent class constructors of classes extending Mutable
+     *  either also extend Mutable or are read-only.
+     *
+     *  A parent class constructor is _read-only_ if the following conditions are met
+     *   1. The class does not retain any exclusive capabilities from its environment.
+     *   2. The constructor does not take arguments that retain exclusive capabilities.
+     *   3. The class does not does not have fields that retain exclusive universal capabilities.
+     */
+    def checkMutableInheritance(cls: ClassSymbol, parents: List[Tree])(using Context): Unit =
+      if cls.derivesFrom(defn.Caps_Mutable) then
+        for parent <- parents do
+          if !parent.tpe.derivesFromMutable then
+            val pcls = parent.nuType.classSymbol
+            val parentIsExclusive =
+              if parent.isType then
+                capturedVars(pcls).isExclusive
+                || captureSetImpliedByFields(cls, parent.nuType).isExclusive
+              else parent.nuType.captureSet.isExclusive
+            if parentIsExclusive then
+              report.error(
+                em"""illegal inheritance: $cls which extends `Mutable` is not allowed to also extend $pcls
+                    |since $pcls retains exclusive capabilities but does not extend `Mutable`.""",
+                parent.srcPos)
+
+    /** Checks to run after the rechecking pass:
+     *   - Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
+     *   - Check that no uses refer to reach capabilities of parameters of enclosing
+     *     methods or classes.
+     *   - Run the separation checker under language.experimental.separationChecking
+     *   - Check that classes extending Mutable do not extend other classes that do
+     *     not extend Mutable yet retain exclusive capabilities
      */
     def postCheck(unit: tpd.Tree)(using Context): Unit =
-      val checker = new TreeTraverser:
+      val check = new TreeTraverser:
         def traverse(tree: Tree)(using Context): Unit =
           val lctx = tree match
             case _: DefTree | _: TypeDef if tree.symbol.exists => ctx.withOwner(tree.symbol)
@@ -2161,30 +2191,35 @@ class CheckCaptures extends Recheck, SymTransformer:
                 if ccConfig.postCheckCapturesets then
                   args.lazyZip(tl.paramNames).foreach(checkTypeParam(_, _, fun.symbol))
               case _ =>
+          case TypeDef(_, impl: Template) =>
+            checkMutableInheritance(tree.symbol.asClass, impl.parents)
           case _ =>
         end check
-      end checker
+      end check
 
-      checker.traverse(unit)(using ctx.withOwner(defn.RootClass))
+      check.traverse(unit)(using ctx.withOwner(defn.RootClass))
       checkEscapingUses()
+      //checkMutableParents()
+
       if sepChecksEnabled then
         for (tree, cs, env) <- useInfos do
           usedSet(tree) = tree.markedFree ++ cs
         ccState.inSepCheck:
           SepCheck(this).traverse(unit)
+
       if !ctx.reporter.errorsReported then
         // We dont report errors here if previous errors were reported, because other
         // errors often result in bad applied types, but flagging these bad types gives
         // often worse error messages than the original errors.
-        val checkApplied = new TreeTraverser:
+        val checkAppliedTypes = new TreeTraverser:
           def traverse(t: Tree)(using Context) = t match
             case tree: InferredTypeTree =>
             case tree: New =>
             case tree: TypeTree =>
               withCollapsedFresh:
                 checkAppliedTypesIn(tree.withType(tree.nuType))
             case _ => traverseChildren(t)
-        checkApplied.traverse(unit)
+        checkAppliedTypes.traverse(unit)
     end postCheck
 
     /** Perform the following kinds of checks:
diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md
@@ -77,11 +77,11 @@ When we create an instance of a mutable type we always add `cap` to its capture
 
 **Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type.
 
-**Definition:** A class is _read_only_ if the following conditions are met:
+**Definition:** A parent class constructor is _read-only_ if the following conditions are met:
 
- 1. It does not extend any exclusive capabilities from its environment.
- 2. It does not take parameters with exclusive capabilities.
- 3. It does not contain mutable fields, or fields that take exclusive capabilities.
+ 1. The class does not retain any exclusive capabilities from its environment.
+ 2. The constructor does not take arguments that retain exclusive capabilities.
+ 3. The class does not does not have fields that retain exclusive universal capabilities.
 
 **Restriction:** If a class or trait extends `Mutable` all its parent classes or traits must either extend `Mutable` or be read-only.
 
@@ -455,4 +455,3 @@ val c = b += 3
 // b cannot be used from here
 ```
 This code is equivalent to functional append with `+`, and is at the same time more efficient since it re-uses the storage of the argument buffer.
-
diff --git a/tests/neg-custom-args/captures/mutable-inheritance.check b/tests/neg-custom-args/captures/mutable-inheritance.check
@@ -0,0 +1,15 @@
+-- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:3:16 ------------------------------------------------
+3 |class A extends E, caps.Mutable // error
+  |                ^
+  |                illegal inheritance: class A which extends `Mutable` is not allowed to also extend class E
+  |                since class E retains exclusive capabilities but does not extend `Mutable`.
+-- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:6:16 ------------------------------------------------
+6 |class C extends B(??? : Int => Int), caps.Mutable // error
+  |                ^^^^^^^^^^^^^^^^^^^
+  |                illegal inheritance: class C which extends `Mutable` is not allowed to also extend class B
+  |                since class B retains exclusive capabilities but does not extend `Mutable`.
+-- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:17:16 -----------------------------------------------
+17 |class H extends G, caps.Mutable // error
+   |                ^
+   |                illegal inheritance: class H which extends `Mutable` is not allowed to also extend class G
+   |                since class G retains exclusive capabilities but does not extend `Mutable`.
diff --git a/tests/neg-custom-args/captures/mutable-inheritance.scala b/tests/neg-custom-args/captures/mutable-inheritance.scala
@@ -0,0 +1,19 @@
+
+class E extends caps.ExclusiveCapability
+class A extends E, caps.Mutable // error
+
+class B(x: Int => Int)
+class C extends B(??? : Int => Int), caps.Mutable // error
+
+class D extends caps.Mutable:
+  var x: Int = 0
+
+class F extends D, caps.Mutable // ok
+
+class Ref extends caps.Mutable
+
+class G:
+  val r: Ref^ = Ref()
+class H extends G, caps.Mutable // error
+
+
