Improve handling of consume in class constructors

Author: odersky

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

@@ -917,12 +917,26 @@ class CheckCaptures extends Recheck, SymTransformer:
        */
       def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
         var refined: Type = core
-        var allCaptures: CaptureSet = initCs ++ captureSetImpliedByFields(cls, core)
+        val implied = captureSetImpliedByFields(cls, core)
+        var allCaptures: CaptureSet = initCs ++ implied
         for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
           val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol
           if !getter.is(Private) && getter.hasTrackedParts then
             refined = refined.refinedOverride(getterName, argType.unboxed) // Yichen you might want to check this
-            allCaptures ++= argType.captureSet
+            if getter.hasAnnotation(defn.ConsumeAnnot)
+                && !implied.isAlwaysEmpty
+                && argType.captureSet.subCaptures(allCaptures)
+                // A consume parameter of a constructor will be hidden in the implied fresh of the
+                // class if there is one. Example:
+                //
+                //    class A(consume val x: B^) { val c: C^ = ... }
+                //    val a = A(b)  // a: A{...}^{cap hiding b}
+                // But
+                //    class A1(val x: B^) { val c: C^ = ... }
+                //    val a1 = A1(b)  // a1: A{...}^{cap, b}
+                // See consume-in-constructor.scala.
+            then () // force the fresh in implied to hide argType.captureSet
+            else allCaptures ++= argType.captureSet
         (refined, allCaptures)
 
       /** Augment result type of constructor with refinements and captures.

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

@@ -7,6 +7,7 @@ import collection.mutable
 import core.*
 import Symbols.*, Types.*, Flags.*, Contexts.*, Names.*, Decorators.*
 import CaptureSet.{Refs, emptyRefs, HiddenSet}
+import NameKinds.WildcardParamName
 import config.Printers.capt
 import StdNames.nme
 import util.{SimpleIdentitySet, EqHashMap, SrcPos}
@@ -986,7 +987,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           traverseSection(tree)
         case tree: ValDef =>
           traverseChildren(tree)
-          checkValOrDefDef(tree)
+          if !tree.name.is(WildcardParamName) then
+            checkValOrDefDef(tree)
         case tree: DefDef =>
           if skippable(tree.symbol) then
             capt.println(i"skipping sep check of ${tree.symbol}")

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

@@ -0,0 +1,31 @@
+-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:18:10 --------------------------------------------
+18 |  println(b) // error
+   |          ^
+   |          Separation failure: Illegal access to {b} which is hidden by the previous definition
+   |          of value a2 with type A2{val b: B^{b²}}^.
+   |          This type hides capabilities  {cap, b²}
+   |
+   |          where:    ^   refers to a fresh root capability in the type of value a2
+   |                    b   is a value in class A2
+   |                    b²  is a value in method Test
+   |                    cap is a fresh root capability created in value a2 when constructing instance A2
+-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:19:10 --------------------------------------------
+19 |  println(a1) // error, since `b` was consumed before
+   |          ^^
+   |          Separation failure: Illegal access to {b} which is hidden by the previous definition
+   |          of value a2 with type A2{val b: B^{b²}}^.
+   |          This type hides capabilities  {cap, b²}
+   |
+   |          where:    ^   refers to a fresh root capability in the type of value a2
+   |                    b   is a value in class A2
+   |                    b²  is a value in method Test
+   |                    cap is a fresh root capability created in value a2 when constructing instance A2
+-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:25:10 --------------------------------------------
+25 |  println(b) // error, b is hidden in the type of a1
+   |          ^
+   |          Separation failure: Illegal access to {b} which is hidden by the previous definition
+   |          of value a1 with type A1^.
+   |          This type hides capabilities  {cap, b}
+   |
+   |          where:    ^   refers to a fresh root capability in the type of value a1
+   |                    cap is a fresh root capability created in value a1 when constructing instance A1

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

@@ -0,0 +1,30 @@
+import caps.cap
+
+class B
+
+class A1(val b: B^):
+  val bb: B^ = B()
+
+class A2(consume val b: B^):
+  val bb: B^ = B()
+
+def Test =
+  val b: B^ = B()
+  val a1 = A1(b)
+  val _: A1^{cap, b} = a1
+  println(b)  // OK   since a1's type mentions `b` explicitly
+  val a2 = A2(b)
+  val _: A2^{cap, b} = a2
+  println(b) // error
+  println(a1) // error, since `b` was consumed before
+  println(a2) // OK since b belongs to a2
+
+def Test2 =
+  val b: B^ = B()
+  val a1: A1^ = A1(b)
+  println(b) // error, b is hidden in the type of a1
+
+
+
+
+