Fix Paths Referencing Consumed Parameters

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}
@@ -558,6 +559,69 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           sepApplyError(fn, parts, arg, app)
   end checkApply
 
+  /** Compute the set of capabilities that are consumed along a selection path.
+   *  For example, if we have the path `a.b` where `b` is a consume field with type `B^{x}`,
+   *  this returns the actual consumed capabilities `{x}` from the type's capture set.
+   *
+   *  This walks the path and for each consume field encountered, collects the capabilities
+   *  from that field's widened type's capture set.
+   *
+   *  @param cap  The capability to analyze (e.g., `a.b`)
+   *  @return     The set of actual consumed capabilities from all consume fields along the path
+   */
+  def consumedByPath(cap: Capability)(using Context): Refs = cap match
+    case Reach(underlying) => consumedByPath(underlying)
+    case ref: TermRef =>
+      def recur(tp: Type, acc: Refs): Refs = tp match
+        case ref: TermRef =>
+          // This is a selection like a.b, or just a reference like a
+          val fieldSym = ref.symbol
+          val accWithCurrent =
+            if fieldSym.exists && fieldSym.isConsumeParam then
+              // This field is a consume parameter. Collect capabilities from its type's capture set.
+              acc ++ ref.widen.captureSet.elems
+            else
+              acc
+          // Also check if the current reference's type has consume fields
+          val accWithConsumeFields = accWithCurrent ++ capsFromConsumeFields(ref)
+          // Recurse on the prefix if it's a selection
+          if ref.prefix ne NoPrefix then
+            recur(ref.prefix, accWithConsumeFields)
+          else
+            accWithConsumeFields
+        case _ =>
+          acc
+
+      def capsFromConsumeFields(ref: TermRef): Refs =
+        // For types with consume fields, use the capture set of the reference itself
+        // and recursively check what those capabilities consume
+        val tpe = ref.widen.dealias
+        val cls = tpe.classSymbol
+        if cls.exists then
+          // Check if this class has any consume fields
+          val hasConsumeFields = cls.info.decls.exists(m => m.isConsumeParam && m.isTerm)
+          if hasConsumeFields then
+            // Use the capture set of the widened type
+            val captureSet = ref.widen.captureSet.elems
+            // Use the capture set of the reference itself (e.g., {a} for holder.a : A^{a})
+            // Return both the capabilities in the capture set AND what they transitively consume
+            var result = emptyRefs
+            for cap <- captureSet do
+              cap match
+                case _: RootCapability => // Skip
+                case _ =>
+                  result = result + cap
+                  result = result ++ consumedByPath(cap)
+            result
+          else
+            emptyRefs
+        else
+          emptyRefs
+
+      recur(ref, emptyRefs)
+    case _ =>
+      emptyRefs
+
   /** 1. Check that the capabilities used at `tree` don't overlap with
    *     capabilities hidden by a previous definition.
    *  2. Also check that none of the used capabilities was consumed before.
@@ -597,8 +661,18 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       for ref <- used do
         val pos = consumed.clashing(ref)
         if pos != null then
-          // println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.directPeaks.toList}, used = $used, exposed = ${ref.directPeaks }")
-          consumeError(ref, pos, tree.srcPos)
+          // Check if this reference should be exempted because consume fields along
+          // the path own the consumed capabilities.
+          val pathConsumed = consumedByPath(ref)
+
+          // Check if any capability consumed by the path was consumed at position `pos`.
+          // We need to check both the capability and its reach, since consumed might store the reach version.
+          val shouldExempt = pathConsumed.exists:
+            case _: RootCapability => false
+            case cap => consumed.get(cap) == pos || consumed.get(cap.reach) == pos
+
+          if !shouldExempt then
+            consumeError(ref, pos, tree.srcPos)
   end checkUse
 
   /** If `tp` denotes some version of a singleton capability `x.type` the set `{x, x*}`
@@ -986,7 +1060,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:20:10 --------------------------------------------
+20 |  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:21:10 --------------------------------------------
+21 |  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:28:10 --------------------------------------------
+28 |  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,33 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+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
+  println(a2.b) // 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
+
+
+
+
+

tests/pos-custom-args/captures/paths-complex-consume.scala

@@ -0,0 +1,80 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+import caps.cap
+
+// Create a deeper nesting structure
+class D()
+class C(val d: D^)
+class B(val c: C^)
+class A(consume val b: B^)
+
+// Test 1: Accessing nested fields through a consumed path
+def testNestedFieldsAfterConsume =
+  val d: D^ = D()
+  val c: C^ = C(d)
+  val b: B^ = B(c)
+  val a = A(b)
+
+  // After a consumed b, we should be able to access:
+  println(a.b)       // OK - a owns b
+  println(a.b.c)     // OK - accessing field of consumed b through a
+  println(a.b.c.d)   // OK - deeper nesting through consumed path
+
+// Test 2: Non-trivial prefix accessing a consumed field
+class Container(consume val a: A^):
+  val other: A^ = A(B(C(D())))
+
+class Outer(consume val container: Container^)
+
+def testComplexPrefix =
+  val d1: D^ = D()
+  val c1: C^ = C(d1)
+  val b1: B^ = B(c1)
+  val a1 = A(b1)
+  val container1 = Container(a1)
+  val outer = Outer(container1)
+
+  // Non-trivial prefix: outer.container.a (where 'a' was consumed by container)
+  println(outer.container)            // OK - outer consumed container
+  println(outer.container.a)          // OK - accessing consumed field through prefix
+  println(outer.container.a.b)        // OK - and then its nested fields
+  println(outer.container.a.b.c)      // OK - even deeper
+  println(outer.container.a.b.c.d)    // OK - deepest level
+
+// Test 3: Multiple consume parameters with nested access
+class Multi(consume val b1: B^, consume val b2: B^):
+  val b3: B^ = B(C(D()))
+
+def testMultipleConsume =
+  val b1: B^ = B(C(D()))
+  val b2: B^ = B(C(D()))
+  val multi = Multi(b1, b2)
+
+  // All of these should work:
+  println(multi.b1)           // OK
+  println(multi.b1.c)         // OK - nested field of consumed b1
+  println(multi.b1.c.d)       // OK - deeper nesting
+  println(multi.b2)           // OK
+  println(multi.b2.c)         // OK - nested field of consumed b2
+  println(multi.b2.c.d)       // OK - deeper nesting
+  println(multi.b3.c.d)       // OK - non-consumed field
+
+// Test 4: Consume at multiple levels with complex paths
+class Top(consume val outer: Outer^)
+
+def testMultiLevelConsume =
+  val d2: D^ = D()
+  val c2: C^ = C(d2)
+  val b2: B^ = B(c2)
+  val a2 = A(b2)
+  val container2 = Container(a2)
+  val outer2 = Outer(container2)
+  val top = Top(outer2)
+
+  // Very deep path through multiple consume levels:
+  println(top.outer)                      // OK - top consumed outer
+  println(top.outer.container)            // OK - continue through path
+  println(top.outer.container.a)          // OK - container consumed a
+  println(top.outer.container.a.b)        // OK - a consumed b
+  println(top.outer.container.a.b.c)      // OK - nested field
+  println(top.outer.container.a.b.c.d)    // OK - deepest field

tests/pos-custom-args/captures/paths-deep-consume.scala

@@ -0,0 +1,24 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+import caps.cap
+
+class B
+
+class A(consume val b: B^):
+  val bb: B^ = B()
+
+class C(consume val a: A^):
+  val aa: A^ = A(B())
+
+// Test deep nested access paths
+def testDeepPaths =
+  val b: B^ = B()
+  val a = A(b)
+  val c = C(a)
+
+  // All these should work - accessing through ownership chain
+  println(c.a)       // c owns a
+  println(c.a.b)     // c owns a, a owns b
+  println(c.a.bb)    // c owns a, accessing other field
+  println(c.aa)      // accessing other field of c
+  println(c.aa.b)    // accessing nested field through c.aa

tests/pos-custom-args/captures/paths-nested-consume.scala

@@ -0,0 +1,33 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+import caps.cap
+
+class B
+
+class A(consume val b: B^):
+  val bb: B^ = B()
+
+class C(consume val a: A^):
+  val aa: A^ = A(B())
+
+// Test: After consuming b into a, then consuming a into c,
+// we should be able to access c.a.b (nested field selection)
+def testNestedAccess =
+  val b: B^ = B()
+  val a = A(b)
+  println(a.b)    // OK - a consumed b, accessing through a
+  val c = C(a)
+  println(c.a)    // Should be OK - c consumed a, accessing through c
+  println(c.a.b)  // Should be OK - accessing b through c.a, where c owns a and a owns b
+
+// Test: The deeper path c.a.b should work even though a was consumed
+def testDeepPath =
+  val b: B^ = B()
+  val a = A(b)
+  val c = C(a)
+  // At this point:
+  // - b was consumed by a (so we can't use b directly)
+  // - a was consumed by c (so we can't use a directly)
+  // But we should be able to access:
+  println(c.a.b)  // OK - full path through ownership chain
+  println(c.a.bb) // OK - other field of c.a

tests/pos-custom-args/captures/paths-simple-suffix-consume.scala

@@ -0,0 +1,37 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+import caps.cap
+
+// Create a deep nesting structure for testing suffix paths
+class D
+class C(val d: D^)
+class B(val c: C^)
+class A(consume val b: B^)
+
+// Test 1: Simple suffix paths after consume
+def test1 =
+  val d: D^ = D()
+  val c: C^ = C(d)
+  val b: B^ = B(c)
+  val a = A(b)
+
+  // After 'a' consumes 'b', access nested fields:
+  println(a.b)       // OK - consumed field
+  println(a.b.c)     // OK - suffix: .c after consumed field
+  println(a.b.c.d)   // OK - suffix: .c.d after consumed field
+
+// Test 2: Non-consume wrapper with consumed inner field
+class Holder(val a: A^)  // Note: NOT consume
+
+def test2 =
+  val d: D^ = D()
+  val c: C^ = C(d)
+  val b: B^ = B(c)
+  val a = A(b)
+  val holder = Holder(a)
+
+  // Access through holder.a.b where b was consumed by a:
+  println(holder.a)         // OK - not consumed
+  println(holder.a.b)       // OK - accessing consumed field through prefix
+  println(holder.a.b.c)     // OK - suffix .c
+  println(holder.a.b.c.d)   // OK - suffix .c.d