Implement inheritance condition for Mutable types

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

@@ -886,7 +886,7 @@ class CheckCaptures extends Recheck, SymTransformer:
        */
       def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
         var refined: Type = core
-        var allCaptures: CaptureSet = initCs ++ impliedByFields(core)
+        var allCaptures: CaptureSet = 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
@@ -910,62 +910,61 @@ 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. If the type is a mutable type,
-       *  we add a fresh cap in any case -- this is because we can currently hide
-       *  mutability in array vals, an example is neg-customargs/captures/matrix.scala.
-       */
-      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`. Mutable types get at least a fresh classified
-         *  as mutable.
-         */
-        def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match
-          case cls: ClassSymbol =>
-            val fields = cls.info.decls.toList
-            var fieldClassifiers =
-              for
-                sym <- fields 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
-            if cls.typeRef.isMutableType then
-              fieldClassifiers = defn.Caps_Mutable :: fieldClassifiers
-            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. If the type is a mutable type,
+     *  we add a fresh cap in any case -- this is because we can currently hide
+     *  mutability in array vals, an example is neg-customargs/captures/matrix.scala.
+     */
+    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 =>
+          var 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
+          if cls.typeRef.isMutableType then
+            fieldClassifiers = defn.Caps_Mutable :: fieldClassifiers
+          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
@@ -2139,7 +2138,38 @@ 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(pcls.asClass, 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:
@@ -2150,6 +2180,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           trace(i"post check $tree"):
             traverseChildren(tree)(using lctx)
             check(tree)
+
         def check(tree: Tree)(using Context) = tree match
           case TypeApply(fun, args) =>
             fun.nuType.widen match
@@ -2162,8 +2193,9 @@ 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
 
       checker.traverse(unit)(using ctx.withOwner(defn.RootClass))
@@ -2173,19 +2205,20 @@ class CheckCaptures extends Recheck, SymTransformer:
           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:

docs/_docs/reference/experimental/capture-checking/mutability.md

@@ -75,13 +75,13 @@ an update method or an update class as non-private member or constructor.
 
 When we create an instance of a mutable type we always add `cap` to its capture set. For instance, if class `Ref` is declared as shown previously then `new Ref(1)` has type `Ref[Int]^`.
 
-**Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type.
+**Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type. (Note: This is currently not enforced)
 
-**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.
 
@@ -293,166 +293,3 @@ The subcapturing theory for sets is then as before, with the following additiona
  - `{x, ...}.RD = {x.rd, ...}.RD`
  - `{x.rd, ...} <: {x, ...}`
 
-## Separation Checking
-
-The idea behind separation checking is simple: We now interpret each occurrence of `cap` as a separate top capability. This includes derived syntaxes like `A^` and `B => C`. We further keep track during capture checking which capabilities are subsumed by each `cap`. If capture checking widens a capability `x` to a top capability `capᵢ`, we say `x` is _hidden_ by `capᵢ`. The rule then is that any capability hidden by a top capability `capᵢ` cannot be referenced independently or hidden in another `capⱼ` in code that can see `capᵢ`.
-
-Here's an example:
-```scala
-val x: C^ = y
-  ... x ...  // ok
-  ... y ...  // error
-```
-This principle ensures that capabilities such as `x` that have `cap` as underlying capture set are un-aliased or "fresh". Any previously existing aliases such as `y` in the code above are inaccessible as long as `x` is also visible.
-
-Separation checking applies only to exclusive capabilities and their read-only versions. Any capability extending `SharedCapability` in its type is exempted; the following definitions and rules do not apply to them.
-
-**Definitions:**
-
- - The _transitive capture set_ `tcs(c)` of a capability `c` with underlying capture set `C` is `c` itself, plus the transitive capture set of `C`.
-
- - The _transitive capture set_ `tcs(C)` of a capture set C is the union
-   of `tcs(c)` for all elements `c` of `C`.
-
- - Two capture sets _interfere_ if one contains an exclusive capability `x` and the other also contains `x` or contains the read-only capability `x.rd`. Conversely, two capture sets are _separated_ if their transitive capture sets don't interfere.
-
-Separation checks are applied in the following scenarios:
-
-### Checking Applications
-
-When checking a function application `f(e_1, ..., e_n)`, we instantiate each `cap` in a formal parameter of `f` to a fresh top capability and compare the argument types with these instantiated parameter types. We then check that the hidden set of each instantiated top capability for an argument `eᵢ` is separated from the capture sets of all the other arguments as well as from the capture sets of the function prefix and the function result. For instance a
-call to
-```scala
-multiply(a, b, a)
-```
-would be rejected since `a` appears in the hidden set of the last parameter of multiply, which has type `Matrix^` and also appears in the capture set of the
-first parameter.
-
-We do not report a separation error between two sets if a formal parameter's capture set explicitly names a conflicting parameter. For instance, consider a method `seq` to apply two effectful function arguments in sequence. It can be declared as follows:
-```scala
-def seq(f: () => Unit; g: () ->{cap, f} Unit): Unit =
-  f(); g()
-```
-Here, the `g` parameter explicitly mentions `f` in its potential capture set. This means that the `cap` in the same capture set would not need to hide the  first argument, since it already appears explicitly in the same set. Consequently, we can pass the same function twice to `compose` without violating the separation criteria:
-```scala
-val r = Ref(1)
-val plusOne = r.set(r.get + 1)
-seq(plusOne, plusOne)
-```
-Without the explicit mention of parameter `f` in the capture set of parameter `g` of `seq` we'd get a separation error, since the transitive capture sets of both arguments contain `r` and are therefore not separated.
-
-### Checking Statement Sequences
-
-When a capability `x` is used at some point in a statement sequence, we check that `{x}` is separated from the hidden sets of all previous definitions.
-
-Example:
-```scala
-val a: Ref^ = Ref(1)
-val b: Ref^ = a
-val x = a.get // error
-```
-Here, the last line violates the separation criterion since it uses in `a.get` the capability `a`, which is hidden by the definition of `b`.
-Note that this check only applies when there are explicit top capabilities in play. One could very well write
-```scala
-val a: Ref^ = Ref(1)
-val b: Ref^{a} = a
-val x = a.get // ok
-```
-One can also drop the explicit type of `b` and leave it to be inferred. That would
-not cause a separation error either.
-```scala
-val a: Ref^ = Ref(0
-val b = a
-val x = a.get // ok
-```
-
-### Checking Types
-
-When a type contains top capabilities we check that their hidden sets don't interfere with other parts of the same type.
-
-Example:
-```scala
-val b: (Ref^, Ref^) = (a, a)       // error
-val c: (Ref^, Ref^{a}) = (a, a)    // error
-val d: (Ref^{a}, Ref^{a}) = (a, a) // ok
-```
-Here, the definition of `b` is in error since the hidden sets of the two `^`s in its type both contain `a`. Likewise, the definition of `c` is in error since the hidden set of the `^` in its type contains `a`, which is also part of a capture set somewhere else in the type. On the other hand, the definition of `d` is legal since there are no hidden sets to check.
-
-### Checking Return Types
-
-When a `cap` appears in the return type of a function it means a "fresh" top capability, different from what is known at the call site. Separation checking makes sure this is the case. For instance, the following is OK:
-```scala
-def newRef(): Ref^ = Ref(1)
-```
-And so is this:
-```scala
-def newRef(): Ref^ =
-  val a = Ref(1)
-  a
-```
-But the next definitions would cause a separation error:
-```scala
-val a = Ref(1)
-def newRef(): Ref^ = a // error
-```
-The rule is that the hidden set of a fresh cap in a return type cannot reference exclusive or read-only capabilities defined outside of the function. What about parameters? Here's another illegal version:
-```scala
-def incr(a: Ref^): Ref^ =
-  a.set(a.get + 1)
-  a
-```
-These needs to be rejected because otherwise we could have set up the following bad example:
-```scala
-val a = Ref(1)
-val b: Ref^ = incr(a)
-```
-Here, `b` aliases `a` but does not hide it. If we referred to `a` afterwards we would be surprised to see that the reference has now a value of 2.
-Therefore, parameters cannot appear in the hidden sets of fresh result caps either, at least not in general. An exception to this rule is described in the next section.
-
-### Consume Parameters
-
-Returning parameters in fresh result caps is safe if the actual argument to the parameter is not used afterwards. We can signal and enforce this pattern by adding a `consume` modifier to a parameter. With that new soft modifier, the following variant of `incr` is legal:
-```scala
-def incr(consume a: Ref^): Ref^ =
-  a.set(a.get + 1)
-  a
-```
-Here, we increment the value of a reference and then return the same reference while enforcing the condition that the original reference cannot be used afterwards. Then the following is legal:
-```scala
-val a1 = Ref(1)
-val a2 = incr(a1)
-val a3 = incr(a2)
-println(a3)
-```
-Each reference `aᵢ` is unused after it is passed to `incr`. But the following continuation of that sequence would be in error:
-```scala
-val a4 = println(a2) // error
-val a5 = incr(a1)    // error
-```
-In both of these assignments we use a capability that was consumed in an argument
-of a previous application.
-
-Consume parameters enforce linear access to resources. This can be very useful. As an example, consider Scala's  buffers such as `ListBuffer` or `ArrayBuffer`. We can treat these buffers as if they were purely functional, if we can enforce linear access.
-
-For instance, we can define a function `linearAdd` that adds elements to buffers in-place without violating referential transparency:
-```scala
-def linearAdd[T](consume buf: Buffer[T]^, elem: T): Buffer[T]^ =
-  buf += elem
-```
-`linearAdd` returns a fresh buffer resulting from appending `elem` to `buf`. It overwrites `buf`, but that's OK since the `consume` modifier on `buf` ensures that the argument is not used after the call.
-
-### Consume Methods
-
-Buffers in Scala's standard library use a single-argument method `+=` instead of a two argument global function like `linearAdd`. We can enforce linearity in this case by adding the `consume` modifier to the method itself.
-```scala
-class Buffer[T] extends Mutable:
-  consume def +=(x: T): Buffer[T]^ = this // ok
-```
-`consume` on a method implies `update`, so there's no need to label `+=` separately as an update method. Then we can write
-```scala
-val b = Buffer[Int]() += 1 += 2
-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.
-