Always add cap to results of constructors with consume parameters

Author: odersky

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

@@ -531,7 +531,11 @@ extension (cls: ClassSymbol)
     else defn.AnyClass
 
   def isSeparate(using Context): Boolean =
-    cls.typeRef.isStatefulType || cls.derivesFrom(defn.Caps_Separate)
+    cls.derivesFrom(defn.Caps_Separate)
+    || cls.typeRef.isStatefulType
+    || cls.paramGetters.exists: getter =>
+          !getter.is(Private) // Setup makes sure that getters with capture sets are not private
+          && getter.hasAnnotation(defn.ConsumeAnnot)
 
 extension (sym: Symbol)
 

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

@@ -1384,14 +1384,6 @@ class CheckCaptures extends Recheck, SymTransformer:
      *      type arguments. Charge deep capture sets of type arguments to non-reserved typevars
      *      to the environment. Other generic parents are represented as TypeApplys, where the
      *      same check is already done in the TypeApply.
-     *   6. Consume parameters are only allowed for classes producing a fresh cap
-     *      for their constructor, and they don't contribute to the capture set. Example:
-     *
-     *        class A(consume val x: B^) extends caps.Separate
-     *        val a = A(b)
-     *
-     *      Here, `a` is of type A{val x: B^}^, and the outer `^` does not hide `b`.
-     *      That's necessary since we would otherwise get consume/use conflicts on `b`.
      */
     override def recheckClassDef(tree: TypeDef, impl: Template, cls: ClassSymbol)(using Context): Type =
       if Feature.enabled(Feature.separationChecking) then sepChecksEnabled = true
@@ -1436,28 +1428,6 @@ class CheckCaptures extends Recheck, SymTransformer:
               markFreeTypeArgs(tpt, fn.typeSymbol, args.map(TypeTree(_)))
             case _ =>
 
-        // (6) Check that consume parameters are covered by an implied FreshCap
-        for getter <- cls.paramGetters do
-          if !getter.is(Private) // Setup makes sure that getters with capture sets are not private
-            && getter.hasAnnotation(defn.ConsumeAnnot)
-          then
-            val implied = captureSetImpliedByFields(cls, cls.appliedRef)
-            val getterCS = getter.info.captureSet
-
-            val hasCoveringFresh = implied.elems.exists:
-              case fresh: FreshCap =>
-                getterCS.elems.forall: elem =>
-                  given VarState = VarState.Unrecorded // make sure we don't add to fresh's hidden set
-                  fresh.maxSubsumes(elem, canAddHidden = true)
-              case _ =>
-                false
-
-            if !hasCoveringFresh then
-              report.error(
-                  em"""A consume parameter is only allowed for classes producing a `cap` in their constructor.
-                      |This can be achieved by having the class extend caps.Separate.""",
-                  getter.srcPos)
-
         super.recheckClassDef(tree, impl, cls)
       finally
         completed += cls

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

@@ -56,7 +56,7 @@ class Counter extends Stateful:
 
 In class `Counter`, the `incr` method should be declared as an update method since it accesses `this` as an exclusive write capability by writing to the variable `this.count` in its environment.
 
-`update` can also be used on an inner class of a class or object extending `Stateful`. It gives all code in the class the right to  access exclusive capabilities in the class environment. Normal classes
+`update` can also be used on an inner class of a class or object extending `Stateful`. It gives all code in the inner class the right to  access exclusive capabilities in the outer class environment. Normal classes
 can only access exclusive capabilities defined in the class or passed to it in parameters.
 
 For instance, we can also define counter objects that update a shared variable that is external to the object:

tests/neg-custom-args/captures/consume-in-constructor.check

@@ -1,8 +1,3 @@
--- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:11:21 --------------------------------------------
-11 |class A3(consume val b: B^) // error
-   |                     ^
-   |                     A consume parameter is only allowed for classes producing a `cap` in their constructor.
-   |                     This can be achieved by having the class extend caps.Separate.
 -- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:20:10 --------------------------------------------
 20 |  println(b) // error
    |          ^

tests/neg-custom-args/captures/consume-in-constructor.scala

@@ -8,7 +8,7 @@ class A1(val b: B^):
 class A2(consume val b: B^):
   val bb: B^ = B()
 
-class A3(consume val b: B^) // error
+class A3(consume val b: B^) // was error now ok
 class A4(consume val b: B^) extends Stateful { var x: Int = 1 } // ok
 def Test =
   val b: B^ = B()