Skip to content

Improve handling of consume in class constructors #24424

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
+80 −3
Open

Improve handling of consume in class constructors #24424

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 16 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Copy link
Contributor

@bracevac bracevac Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm trying to understand what should happen when the if there is one part is not true.
Say, in the below test file, if we let A1 and A2 have no implied fresh (IIUC):

class A1(val b: B^)
class A2(consume val b: B^)

Then it exhibits the expected errors, plus it complains about
val _: A2^{cap, b} = a2 and println(a2) with the same error message:

Separation failure: Illegal access to (a2 : A2{val b: B^{b²}}^{b²}), which was passed to a
   |consume parameter or was used as a prefix to a consume method on line 18
   |and therefore is no longer available.
   |
   |where:    b  is a value in class A2
   |          b² is a value in method Test

Why is accessing a2 forbidden now?

Independently of whether an error is expected or not: The error message itself is confusing, because a2 neither was "passed to a consume parameter" nor "was used as a prefix to a consume method".

//
// 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.
Expand Down
4 changes: 3 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/SepCheck.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -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}")
Expand Down
31 changes: 31 additions & 0 deletions tests/neg-custom-args/captures/consume-in-constructor.check
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
30 changes: 30 additions & 0 deletions tests/neg-custom-args/captures/consume-in-constructor.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Copy link
Contributor

@bracevac bracevac Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
val _: A2^{cap, b} = a2
val _: A2^ = a2

Copy link
Contributor

@bracevac bracevac Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this intentional? It doesn't seem to matter if it's {cap, b} or {cap}. Or is the point to show that mentioning b explicitly as in A1 above doesn't influence the outcome?

println(b) // error
println(a1) // error, since `b` was consumed before
println(a2) // OK since b belongs to a2

Copy link
Contributor

@bracevac bracevac Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Trying println(a2.b) at this point yields a separation failure. But why? The b should be owned by a2 now. If this is as intended, it means that consume on a val constructor parameter makes the field inaccessible.

def Test2 =
val b: B^ = B()
val a1: A1^ = A1(b)
println(b) // error, b is hidden in the type of a1





Loading