Don't automatically add cap when creating instances of capability classes

odersky · odersky · commit c0505d0e1acc · 2025-10-26T18:35:49.000+01:00
To make up for this, refine the scheme to determine an implied fresh cap from
the class fields.
diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -961,7 +961,6 @@ object Capabilities:
     case UnapplyInstance(info: MethodType)
     case LocalInstance(restpe: Type)
     case NewInstance(tp: Type)
-    case NewCapability(tp: Type)
     case LambdaExpected(respt: Type)
     case LambdaActual(restp: Type)
     case OverriddenType(member: Symbol)
@@ -992,9 +991,6 @@ object Capabilities:
         i" when instantiating expected result type $restpe of function literal"
       case NewInstance(tp) =>
         i" when constructing instance $tp"
-      case NewCapability(tp) =>
-        val kind = if tp.derivesFromMutable then "mutable" else "Capability instance"
-        i" when constructing $kind $tp"
       case LambdaExpected(respt) =>
         i" when instantiating expected result type $respt of lambda"
       case LambdaActual(restp: Type) =>
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -881,16 +881,12 @@ class CheckCaptures extends Recheck, SymTransformer:
        *  annotations avoid problematic intersections of capture sets when those
        *  parameters are selected.
        *
-       *  Second half: union of initial capture set and all capture sets of arguments
-       *  to tracked parameters. The initial capture set `initCs` is augmented with
-       *  a fresh cap if `core` extends Capability.
+       *  Second half: union of initial capture set, all capture sets of arguments
+       *  to tracked parameters, and the capture set implied by the fields of the class.
        */
       def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
         var refined: Type = core
-        var allCaptures: CaptureSet =
-          if core.derivesFromCapability
-          then initCs ++ FreshCap(Origin.NewCapability(core)).singletonCaptureSet
-          else initCs ++ impliedByFields(core)
+        var allCaptures: CaptureSet = initCs ++ impliedByFields(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
@@ -917,28 +913,33 @@ class CheckCaptures extends Recheck, SymTransformer:
       /** 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.
+       *  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`.
+         *  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 fieldClassifiers =
+            val fields = cls.info.decls.toList
+            var fieldClassifiers =
               for
-                sym <- cls.info.decls.toList
-                if contributesFreshToClass(sym)
+                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
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -332,7 +332,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
       if !tptToCheck.isEmpty then report.error(msg, tptToCheck.srcPos)
 
     /** If C derives from Capability and we have a C^cs in source, we leave it as is
-     *  instead of expanding it to C^{cap.rd}^cs. We do this by stripping capability-generated
+     *  instead of expanding it to C^{cap}^cs. We do this by stripping capability-generated
      *  universal capture sets from the parent of a CapturingType.
      */
     def stripImpliedCaptureSet(tp: Type): Type = tp match
diff --git a/docs/_docs/reference/experimental/capture-checking/basics.md b/docs/_docs/reference/experimental/capture-checking/basics.md
@@ -219,9 +219,12 @@ This widening is called _avoidance_; it is not specific to capture checking but
 
 ## Capability Classes
 
-Classes like `CanThrow` or `FileSystem` have the property that their values are always intended to be capabilities. We can make this intention explicit and save boilerplate by letting these classes extend the  `SharedCapability` class defined in object `cap`.
+Classes like `CanThrow` or `FileSystem` have the property that their values are always intended to be capabilities. We can make this intention explicit and save boilerplate by letting these classes extend the  `SharedCapability` class defined in object `caps`.
+
+A type extending `SharedCapability` always comes with a capture set. If no capture set is given explicitly, we assume the capture set is `{cap}`.
+
+This means we could equivalently express the `FileSystem` and `Logger` classes as follows:
 
-The capture set of type extending `SharedCapability` is always `{cap}`. This means we could equivalently express the `FileSystem` and `Logger` classes as follows:
 ```scala
 import caps.SharedCapability
 
@@ -234,9 +237,10 @@ def test(using fs: FileSystem) =
   val l: Logger^{fs} = Logger()
   ...
 ```
-In this version, `FileSystem` is a capability class, which means that the `{cap}` capture set is implied on the parameters of `Logger` and `test`.
+In this version, `FileSystem` is a capability class, which means that the occurrences of `FileSystem` in the types of the parameters of `Logger` and `test` are implicitly expanded to `FileSystem^`. On the other hand, types like `FileSystem^{f}` or
+`FileSystem^{}` are kept as written.
 
-Another, unrelated change in the version of the last example here is that the `FileSystem` capability is now passed as an implicit parameter. It is quite natural to model capabilities with implicit parameters since it greatly reduces the wiring overhead once multiple capabilities are in play.
+Another, unrelated change in the last version of the `Logger` example is that the `FileSystem` capability is now passed as an implicit parameter. It is quite natural to model capabilities with implicit parameters since it greatly reduces the wiring overhead once multiple capabilities are in play.
 
 ## Escape Checking
 
diff --git a/tests/neg-custom-args/captures/boundary.check b/tests/neg-custom-args/captures/boundary.check
@@ -2,14 +2,13 @@
  4 |  boundary[AnyRef^]:
  5 |    l1 ?=> // error // error
    |  ^
-   |Found:    scala.util.boundary.Label[Object^'s1]^
-   |Required: scala.util.boundary.Label[Object^²]^³
+   |  Found:    scala.util.boundary.Label[Object^'s1]
+   |  Required: scala.util.boundary.Label[Object^]^²
    |
-   |Note that capability cap cannot be included in outer capture set 's1.
+   |  Note that capability cap cannot be included in outer capture set 's1.
    |
-   |where:    ^          refers to a fresh root capability classified as Control created in value local when constructing Capability instance scala.util.boundary.Label[Object^'s1]
-   |          ^² and cap refer to the universal root capability
-   |          ^³         refers to a fresh root capability classified as Control in the type of value local
+   |  where:    ^ and cap refer to the universal root capability
+   |            ^²        refers to a fresh root capability classified as Control in the type of value local
  6 |      boundary[Unit]: l2 ?=>
  7 |        boundary.break(l2)(using l1) // error
  8 |      ???
diff --git a/tests/neg-custom-args/captures/extending-cap-classes.check b/tests/neg-custom-args/captures/extending-cap-classes.check
@@ -1,27 +1,5 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:7:15 -------------------------
-7 |  val x2: C1 = new C2 // error
-  |               ^^^^^^
-  |Found:    C2^
-  |Required: C1
-  |
-  |Note that capability cap is not included in capture set {}.
-  |
-  |where:    ^ and cap refer to a fresh root capability classified as SharedCapability created in value x2 when constructing Capability instance C2
-  |
-  | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:8:15 -------------------------
-8 |  val x3: C1 = new C3 // error
-  |               ^^^^^^
-  |Found:    C3^
-  |Required: C1
-  |
-  |Note that capability cap is not included in capture set {}.
-  |
-  |where:    ^ and cap refer to a fresh root capability classified as SharedCapability created in value x3 when constructing Capability instance C3
-  |
-  | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:13:15 ------------------------
-13 |  val z2: C1 = y2 // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:14:15 ------------------------
+14 |  val z2: C1 = y2 // error
    |               ^^
    |               Found:    (y2 : C2)
    |               Required: C1
diff --git a/tests/neg-custom-args/captures/extending-cap-classes.scala b/tests/neg-custom-args/captures/extending-cap-classes.scala
@@ -4,11 +4,13 @@ class C3 extends C2
 
 def test =
   val x1: C1 = new C1
-  val x2: C1 = new C2 // error
-  val x3: C1 = new C3 // error
+  val x2: C1 = new C2 // was error, now ok
+  val x3: C1 = new C3 // was error, now ok
 
   val y2: C2 = new C2
   val y3: C3 = new C3
+  val y2ok: C2^{} = new C2
 
   val z2: C1 = y2 // error
+  val z2ok: C1 = y2ok
 
diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check
@@ -13,13 +13,12 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
 15 |  files.map(new Logger(_)) // error, Q: can we improve the error message?
    |            ^^^^^^^^^^^^^
-   |Found:    (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{cap, _$1}
+   |Found:    (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{_$1}
    |Required: File^{C} => Logger{val f: File^'s2}^'s3
    |
    |Note that capability C is not classified as trait SharedCapability, therefore it
    |cannot be included in capture set 's1 of parameter _$1 of SharedCapability elements.
    |
-   |where:    =>  refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map
-   |          cap is a root capability associated with the result type of (_$1: File^'s1): Logger{val f: File^{_$1}}^{cap, _$1}
+   |where:    => refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i23726.check b/tests/neg-custom-args/captures/i23726.check
@@ -1,5 +1,5 @@
--- Error: tests/neg-custom-args/captures/i23726.scala:10:5 -------------------------------------------------------------
-10 |  f1(a)  // error, as expected
+-- Error: tests/neg-custom-args/captures/i23726.scala:11:5 -------------------------------------------------------------
+11 |  f1(a)  // error, as expected
    |     ^
    |Separation failure: argument of type  (a : Ref^)
    |to a function of type (x: Ref^) -> List[() ->{a, x} Unit]
@@ -15,8 +15,8 @@
    |
    |where:    ^  refers to a fresh root capability classified as Mutable in the type of value a
    |          ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
--- Error: tests/neg-custom-args/captures/i23726.scala:15:5 -------------------------------------------------------------
-15 |  f3(b)  // error
+-- Error: tests/neg-custom-args/captures/i23726.scala:16:5 -------------------------------------------------------------
+16 |  f3(b)  // error
    |     ^
    |Separation failure: argument of type  (b : Ref^)
    |to a function of type (x: Ref^) -> (op: () ->{b} Unit) -> List[() ->{op} Unit]
@@ -32,8 +32,8 @@
    |
    |where:    ^  refers to a fresh root capability classified as Mutable in the type of value b
    |          ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
--- Error: tests/neg-custom-args/captures/i23726.scala:23:5 -------------------------------------------------------------
-23 |  f7(a)  // error
+-- Error: tests/neg-custom-args/captures/i23726.scala:24:5 -------------------------------------------------------------
+24 |  f7(a)  // error
    |     ^
    |Separation failure: argument of type  (a : Ref^)
    |to a function of type (x: Ref^) ->{a, b} (y: List[Ref^{a, b}]) ->{a, b} Unit
diff --git a/tests/neg-custom-args/captures/i23726.scala b/tests/neg-custom-args/captures/i23726.scala
@@ -1,7 +1,8 @@
 import language.experimental.captureChecking
 import language.experimental.separationChecking
 import caps.*
-class Ref extends Mutable
+class Ref extends Mutable:
+  update def set = ???
 def swap(a: Ref^, b: Ref^): Unit = ()
 def test1(): Unit =
   val a = Ref()
diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.check b/tests/neg-custom-args/captures/scope-extrude-mut.check
@@ -1,13 +1,13 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scope-extrude-mut.scala:9:8 ------------------------------
-9 |    a = a1  // error
-  |        ^^
-  |        Found:    (a1 : A^)
-  |        Required: A^²
-  |
-  |        Note that capability cap is not included in capture set {cap²}
-  |        because cap in method b is not visible from cap² in variable a.
-  |
-  |        where:    ^ and cap   refer to a fresh root capability classified as Mutable in the type of value a1
-  |                  ^² and cap² refer to a fresh root capability classified as Mutable in the type of variable a
-  |
-  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scope-extrude-mut.scala:10:8 -----------------------------
+10 |    a = a1  // error
+   |        ^^
+   |        Found:    (a1 : A^)
+   |        Required: A^²
+   |
+   |        Note that capability cap is not included in capture set {cap²}
+   |        because cap in method b is not visible from cap² in variable a.
+   |
+   |        where:    ^ and cap   refer to a fresh root capability classified as Mutable in the type of value a1
+   |                  ^² and cap² refer to a fresh root capability classified as Mutable in the type of variable a
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.scala b/tests/neg-custom-args/captures/scope-extrude-mut.scala
@@ -1,6 +1,7 @@
 import language.experimental.captureChecking
 
-class A extends caps.Mutable
+class A extends caps.Mutable:
+  var x = 0
 
 class B:
   private var a: A^ = A()
diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check
@@ -9,4 +9,4 @@
    |where:    ^    refers to a fresh root capability classified as Mutable in the result type of method mkCounter
    |          ^²   refers to a fresh root capability classified as Mutable in the result type of method mkCounter
    |          cap  is a fresh root capability classified as Mutable in the type of value c
-   |          cap² is a fresh root capability classified as Mutable created in value c when constructing mutable Ref
+   |          cap² is a fresh root capability classified as Mutable created in value c when constructing instance Ref
diff --git a/tests/pos-custom-args/captures/strip-implied-cs.scala b/tests/pos-custom-args/captures/strip-implied-cs.scala
@@ -0,0 +1,21 @@
+//> using options -Werror
+import caps.*
+
+trait State[A] extends SharedCapability:
+  def get: A
+  def set(a: A): Unit
+
+def get[A]: State[A] ?-> A          = s ?=> s.get
+def set[A](a: A): State[A] ?-> Unit = s ?=> s.set(a)
+
+trait Rand extends SharedCapability:
+  def range(min: Int, max: Int): Int
+
+object Rand:
+  def fromState: (s: State[Long]) ?-> Rand^{s} =
+    new Rand:
+      override def range(min: Int, max: Int): Int =
+        val seed             = get
+        val (nextSeed, next) = (seed + 1, seed.toInt) // obviously wrong, but not the point...
+        set(nextSeed)
+        next

Original file line number	Diff line number	Diff line change
`@@ -13,13 +13,12 @@`
`13`	`13`	`-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------`
`14`	`14`	`15 \| files.map(new Logger(_)) // error, Q: can we improve the error message?`
`15`	`15`	`\| ^^^^^^^^^^^^^`
`16`		`- \|Found: (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{cap, _$1}`
	`16`	`+ \|Found: (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{_$1}`
`17`	`17`	`\|Required: File^{C} => Logger{val f: File^'s2}^'s3`
`18`	`18`	`\|`
`19`	`19`	`\|Note that capability C is not classified as trait SharedCapability, therefore it`
`20`	`20`	`\|cannot be included in capture set 's1 of parameter _$1 of SharedCapability elements.`
`21`	`21`	`\|`
`22`		`- \|where: => refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map`
`23`		`- \| cap is a root capability associated with the result type of (_$1: File^'s1): Logger{val f: File^{_$1}}^{cap, _$1}`
	`22`	`+ \|where: => refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map`
`24`	`23`	`\|`
`25`	`24`	\| longer explanation available when compiling with `-explain`