diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 92fa632f5166..c6c442a953d9 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/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. diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index b98f07080181..753cc5e9e375 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/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}") diff --git a/tests/neg-custom-args/captures/consume-in-constructor.check b/tests/neg-custom-args/captures/consume-in-constructor.check new file mode 100644 index 000000000000..1f937098ee94 --- /dev/null +++ b/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 diff --git a/tests/neg-custom-args/captures/consume-in-constructor.scala b/tests/neg-custom-args/captures/consume-in-constructor.scala new file mode 100644 index 000000000000..a469d803f905 --- /dev/null +++ b/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 + + + + +