From 521432fbbb368f75e35c3517ee98afdf7ec8395a Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 3 Oct 2025 22:12:03 +0200 Subject: [PATCH 01/12] Add a prefix to FreshCaps The prefix is mapped as a normal type. It determines whether the hidden set allows to add new elements. ThisType and NoPrefix prefixes allow it, other prefixes forbid it. The pathRoot and ccOwner of a FreshCap now depend on the prefix. --- compiler/src/dotty/tools/dotc/ast/tpd.scala | 2 +- .../src/dotty/tools/dotc/cc/Capability.scala | 65 +++++++++++++++---- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 11 +++- .../dotty/tools/dotc/cc/CheckCaptures.scala | 1 + compiler/src/dotty/tools/dotc/cc/Setup.scala | 2 +- .../src/dotty/tools/dotc/core/Symbols.scala | 4 +- .../src/dotty/tools/dotc/core/Types.scala | 38 +++++++---- .../tools/dotc/printing/PlainPrinter.scala | 9 ++- .../tools/dotc/transform/patmat/Space.scala | 2 +- .../dotty/tools/dotc/typer/Applications.scala | 4 +- tests/neg-custom-args/captures/i19330.check | 15 ----- tests/neg-custom-args/captures/i19330.scala | 2 +- .../captures/cc-poly-varargs.scala | 15 +++++ 13 files changed, 118 insertions(+), 52 deletions(-) create mode 100644 tests/pos-custom-args/captures/cc-poly-varargs.scala diff --git a/compiler/src/dotty/tools/dotc/ast/tpd.scala b/compiler/src/dotty/tools/dotc/ast/tpd.scala index eddc0c675e9a..909387bbb809 100644 --- a/compiler/src/dotty/tools/dotc/ast/tpd.scala +++ b/compiler/src/dotty/tools/dotc/ast/tpd.scala @@ -517,7 +517,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo { def singleton(tp: Type, needLoad: Boolean = true)(using Context): Tree = tp.dealias match { case tp: TermRef => ref(tp, needLoad) case tp: ThisType => This(tp.cls) - case tp: SkolemType => singleton(tp.narrow, needLoad) + case tp: SkolemType => singleton(tp.narrow(), needLoad) case SuperType(qual, _) => singleton(qual, needLoad) case ConstantType(value) => Literal(value) } diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index d665e8d4bd3c..98fd5e7dda9e 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -23,6 +23,7 @@ import printing.Texts.Text import reporting.{Message, trace} import NameOps.isImpureFunction import annotation.internal.sharable +import collection.immutable /** Capabilities are members of capture sets. They partially overlap with types * as shown in the trait hierarchy below. @@ -147,10 +148,30 @@ object Capabilities: * @param origin an indication where and why the FreshCap was created, used * for diagnostics */ - case class FreshCap (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability: - val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked) + case class FreshCap(val prefix: Type) + (val owner: Symbol, val origin: Origin, origHidden: CaptureSet.HiddenSet | Null) + (using @constructorOnly ctx: Context) + extends RootCapability: + val hiddenSet = + if origHidden == null then CaptureSet.HiddenSet(owner, this: @unchecked) + else origHidden // fails initialization check without the @unchecked + def derivedFreshCap(newPrefix: Type)(using Context): FreshCap = + if newPrefix eq prefix then this + else if newPrefix eq hiddenSet.owningCap.prefix then + hiddenSet.owningCap + else + hiddenSet.derivedCaps + .getOrElseUpdate(newPrefix, FreshCap(newPrefix)(owner, origin, hiddenSet)) + + /** A map from context owners to skolem TermRefs that were created by ensurePath + * TypeMap's mapCapability. + */ + var skolems: immutable.Map[Symbol, TermRef] = immutable.HashMap.empty + + //assert(rootId != 10, i"fresh $prefix, ${ctx.owner}") + /** Is this fresh cap (definitely) classified? If that's the case, the * classifier cannot be changed anymore. * We need to distinguish `FreshCap`s that can still be classified from @@ -167,12 +188,6 @@ object Capabilities: case _ => false /** Is this fresh cap at the right level to be able to subsume `ref`? - * Only outer freshes can be subsumed. - * TODO Can we merge this with levelOK? Right now we use two different schemes: - * - For level checking capsets with levelOK: Check that the visibility of the element - * os not properly contained in the captset owner. - * - For level checking elements subsumed by FreshCaps: Check that the widened scope - * (using levelOwner) of the elements contains the owner of the FreshCap. */ def acceptsLevelOf(ref: Capability)(using Context): Boolean = if ccConfig.useFreshLevels && !CCState.collapseFresh then @@ -203,8 +218,12 @@ object Capabilities: i"a fresh root capability$classifierStr$originStr" object FreshCap: + def apply(owner: Symbol, prefix: Type, origin: Origin)(using Context): FreshCap = + new FreshCap(prefix)(owner, origin, null) + def apply(owner: Symbol, origin: Origin)(using Context): FreshCap = + apply(owner, owner.skipWeakOwner.thisType, origin) def apply(origin: Origin)(using Context): FreshCap = - FreshCap(ctx.owner, origin) + apply(ctx.owner, origin) /** A root capability associated with a function type. These are conceptually * existentially quantified over the function's result type. @@ -441,6 +460,7 @@ object Capabilities: * the form this.C but their pathroot is still this.C, not this. */ final def pathRoot(using Context): Capability = this match + case FreshCap(pre: Capability) => pre.pathRoot case _: RootCapability => this case self: DerivedCapability => self.underlying.pathRoot case self: CoreCapability => self.dealias match @@ -485,7 +505,13 @@ object Capabilities: case TermRef(prefix: Capability, _) => prefix.ccOwner case self: NamedType => self.symbol case self: DerivedCapability => self.underlying.ccOwner - case self: FreshCap => self.hiddenSet.owner + case self: FreshCap => + val setOwner = self.hiddenSet.owner + self.prefix match + case prefix: ThisType if setOwner.isTerm && setOwner.owner == prefix.cls => + setOwner + case prefix: Capability => prefix.ccOwner + case _ => setOwner case _ /* : GlobalCap | ResultCap | ParamRef */ => NoSymbol final def visibility(using Context): Symbol = this match @@ -732,12 +758,25 @@ object Capabilities: (this eq y) || this.match case x: FreshCap => + def classifierOK = + if y.tryClassifyAs(x.hiddenSet.classifier) then true + else + capt.println(i"$y cannot be classified as $x") + false + + def prefixAllowsAddHidden: Boolean = + CCState.collapseFresh || x.prefix.match + case NoPrefix => true + case pre: ThisType => x.ccOwner.isContainedIn(pre.cls) + case pre => + capt.println(i"fresh not open $x, ${x.rootId}, $pre, ${x.ccOwner.skipWeakOwner.thisType}") + false + vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y))) || x.acceptsLevelOf(y) - && ( y.tryClassifyAs(x.hiddenSet.classifier) - || { capt.println(i"$y cannot be classified as $x"); false } - ) + && classifierOK && canAddHidden + && prefixAllowsAddHidden && vs.addHidden(x.hiddenSet, y) case x: ResultCap => val result = y match diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 86c502b489f8..d4f058de2c38 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -12,7 +12,7 @@ import annotation.internal.sharable import reporting.trace import printing.{Showable, Printer} import printing.Texts.* -import util.{SimpleIdentitySet, Property} +import util.{SimpleIdentitySet, Property, EqHashMap} import typer.ErrorReporting.Addenda import scala.collection.{mutable, immutable} import TypeComparer.ErrorNote @@ -560,8 +560,10 @@ object CaptureSet: def universal(using Context): Const = Const(SimpleIdentitySet(GlobalCap)) + def fresh(owner: Symbol, prefix: Type, origin: Origin)(using Context): Const = + FreshCap(owner, prefix, origin).singletonCaptureSet def fresh(origin: Origin)(using Context): Const = - FreshCap(origin).singletonCaptureSet + fresh(ctx.owner, ctx.owner.thisType, origin) /** The shared capture set `{cap.rd}` */ def shared(using Context): Const = @@ -990,7 +992,7 @@ object CaptureSet: case _ => isSubsumed if !isSubsumed then if elem.origin != Origin.InDecl(owner) || elem.hiddenSet.isConst then - val fc = new FreshCap(owner, Origin.InDecl(owner)) + val fc = FreshCap(owner, Origin.InDecl(owner)) assert(fc.tryClassifyAs(elem.hiddenSet.classifier), fail) hideIn(fc) super.includeElem(fc) @@ -1225,6 +1227,9 @@ object CaptureSet: override def owner = givenOwner + /** The FreshCaps generated by derivedFreshCap, indexed by prefix */ + val derivedCaps = new EqHashMap[Type, FreshCap]() + //assert(id != 3) description = i"of elements subsumed by a fresh cap in $initialOwner" diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index d5cc2811f264..ab4bbb9875d6 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1939,6 +1939,7 @@ class CheckCaptures extends Recheck, SymTransformer: private val setup: SetupAPI = thisPhase.prev.asInstanceOf[Setup] override def checkUnit(unit: CompilationUnit)(using Context): Unit = + capt.println(i"cc check ${unit.source}") ccState.start() setup.setupUnit(unit.tpdTree, this) collectCapturedMutVars.traverse(unit.tpdTree) diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index d1b0f0c5cc72..1d098d3905ec 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -690,7 +690,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: if cls.derivesFrom(defn.Caps_Capability) then // If cls is a capability class, we need to add a fresh readonly capability to // ensure we cannot treat the class as pure. - CaptureSet.fresh(Origin.InDecl(cls)).readOnly.subCaptures(cs) + CaptureSet.fresh(cls, cls.thisType, Origin.InDecl(cls)).readOnly.subCaptures(cs) CapturingType(cinfo.selfType, cs) // Compute new parent types diff --git a/compiler/src/dotty/tools/dotc/core/Symbols.scala b/compiler/src/dotty/tools/dotc/core/Symbols.scala index d86c50cbe2e3..f3496a8636dd 100644 --- a/compiler/src/dotty/tools/dotc/core/Symbols.scala +++ b/compiler/src/dotty/tools/dotc/core/Symbols.scala @@ -900,8 +900,8 @@ object Symbols extends SymUtils { /** Create a new skolem symbol. This is not the same as SkolemType, even though the * motivation (create a singleton referencing to a type) is similar. */ - def newSkolem(tp: Type)(using Context): TermSymbol = - newSymbol(defn.RootClass, nme.SKOLEM, SyntheticArtifact | NonMember | Permanent, tp) + def newSkolem(owner: Symbol, tp: Type)(using Context): TermSymbol = + newSymbol(owner, nme.SKOLEM, SyntheticArtifact | NonMember | Permanent, tp) def newErrorSymbol(owner: Symbol, name: Name, msg: Message)(using Context): Symbol = { val errType = ErrorType(msg) diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index 97a172966701..ec6d10c1712d 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -1706,11 +1706,10 @@ object Types extends TypeUtils { if hasNext then current = f(current.asInstanceOf[TypeProxy]) res - /** A prefix-less refined this or a termRef to a new skolem symbol - * that has the given type as info. + /** A prefix-less TermRef to a new skolem symbol that has this type as info. */ - def narrow(using Context): TermRef = - TermRef(NoPrefix, newSkolem(this)) + def narrow(using Context)(owner: Symbol = defn.RootClass): TermRef = + TermRef(NoPrefix, newSkolem(owner, this)) /** Useful for diagnostics: The underlying type if this type is a type proxy, * otherwise NoType @@ -2319,14 +2318,14 @@ object Types extends TypeUtils { override def dropIfProto = WildcardType } - /** Implementations of this trait cache the results of `narrow`. */ - trait NarrowCached extends Type { + /** Implementations of this trait cache the results of `narrow` if the owner is RootClass. */ + trait NarrowCached extends Type: private var myNarrow: TermRef | Null = null - override def narrow(using Context): TermRef = { - if (myNarrow == null) myNarrow = super.narrow - myNarrow.nn - } - } + override def narrow(using Context)(owner: Symbol): TermRef = + if owner == defn.RootClass then + if myNarrow == null then myNarrow = super.narrow(owner) + myNarrow.nn + else super.narrow(owner) // --- NamedTypes ------------------------------------------------------------------ @@ -6330,6 +6329,23 @@ object Types extends TypeUtils { null def mapCapability(c: Capability, deep: Boolean = false): Capability | (CaptureSet, Boolean) = c match + case c @ FreshCap(prefix) => + // If `pre` is not a path, transform it to a path starting with a skolem TermRef. + // We create at most one such skolem per FreshCap/context owner pair. + // This approximates towards creating fewer skolems than otherwise needed, + // which means we might get more separation conflicts than otherwise. But + // it's not clear we will get such conflicts anyway. + def ensurePath(pre: Type)(using Context): Type = pre match + case pre @ TermRef(pre1, _) => pre.withPrefix(ensurePath(pre1)) + case NoPrefix | _: SingletonType => pre + case pre => + c.skolems.get(ctx.owner) match + case Some(skolem) => skolem + case None => + val skolem = pre.narrow(ctx.owner) + c.skolems = c.skolems.updated(ctx.owner, skolem) + skolem + c.derivedFreshCap(ensurePath(apply(prefix))) case c: RootCapability => c case Reach(c1) => mapCapability(c1, deep = true) diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala index 3a0611e74ec1..bdf527dfbebd 100644 --- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -491,8 +491,13 @@ class PlainPrinter(_ctx: Context) extends Printer { def classified = if c.hiddenSet.classifier == defn.AnyClass then "" else s" classified as ${c.hiddenSet.classifier.name.show}" - if ccVerbose then s"" - else "cap" + def prefixTxt: Text = c.prefix match + case NoPrefix | _: ThisType => "" + case pre => pre.show ~ "." + def core: Text = + if ccVerbose then s"" + else "cap" + prefixTxt ~ core case tp: TypeProxy => homogenize(tp) match case tp: SingletonType => toTextRef(tp) diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala index 7857f8c86189..5ff098e0dc35 100644 --- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala +++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala @@ -395,7 +395,7 @@ object SpaceEngine { case _ => // Pattern is an arbitrary expression; assume a skolem (i.e. an unknown value) of the pattern type - Typ(pat.tpe.narrow, decomposed = false) + Typ(pat.tpe.narrow(), decomposed = false) }) private def project(tp: Type)(using Context): Space = tp match { diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala index 5ecf1601db8a..b2b36e438597 100644 --- a/compiler/src/dotty/tools/dotc/typer/Applications.scala +++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala @@ -337,7 +337,7 @@ object Applications { case pre: SingletonType => singleton(pre, needLoad = !testOnly) case pre if testOnly => // In this case it is safe to skolemize now; we will produce a stable prefix for the actual call. - ref(pre.narrow) + ref(pre.narrow()) case _ => EmptyTree if fn.symbol.hasDefaultParams then @@ -1845,7 +1845,7 @@ trait Applications extends Compatibility { case methRef: TermRef if methRef.widenSingleton.isInstanceOf[MethodicType] => p(methRef) case mt: MethodicType => - p(mt.narrow) + p(mt.narrow()) case _ => followApply && tp.member(nme.apply).hasAltWith(d => p(TermRef(tp, nme.apply, d))) } diff --git a/tests/neg-custom-args/captures/i19330.check b/tests/neg-custom-args/captures/i19330.check index 72947fb1bcf6..abdeeb1eded3 100644 --- a/tests/neg-custom-args/captures/i19330.check +++ b/tests/neg-custom-args/captures/i19330.check @@ -12,21 +12,6 @@ | Note that capability t is not included in capture set {}. | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i19330.scala:22:22 --------------------------------------- -22 | val bad: bar.T = foo(bar) // error - | ^^^^^^^^ - | Found: bar.T - | Required: () => Logger^ - | - | Note that capability cap is not included in capture set {cap²} - | because cap in class Bar is not visible from cap² in value bad. - | - | where: => refers to a fresh root capability in the type of value bad - | ^ refers to a fresh root capability in the type of value bad - | cap is a fresh root capability in the type of type T - | cap² is a fresh root capability in the type of value bad - | - | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/i19330.scala:16:14 ------------------------------------------------------------ 16 | val t: () => Logger^ = () => l // error | ^^^^^^^^^^^^^ diff --git a/tests/neg-custom-args/captures/i19330.scala b/tests/neg-custom-args/captures/i19330.scala index cdc0367bc7d3..57a54ef81a20 100644 --- a/tests/neg-custom-args/captures/i19330.scala +++ b/tests/neg-custom-args/captures/i19330.scala @@ -19,5 +19,5 @@ def foo(x: Foo): x.T = def test(): Unit = val bar = new Bar - val bad: bar.T = foo(bar) // error + val bad: bar.T = foo(bar) val leaked: Logger^ = bad() // leaked scoped capability! diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs.scala new file mode 100644 index 000000000000..b6c270d35cc7 --- /dev/null +++ b/tests/pos-custom-args/captures/cc-poly-varargs.scala @@ -0,0 +1,15 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +abstract class Source[+T] + +extension[T](src: Source[T]^) + def transformValuesWith[U](f: (T -> U)^{src, caps.cap}): Source[U]^{src, f} = ??? + +def race[T, D^](sources: Source[T]^{D}*): Source[T]^{D} = ??? + +def either[T1, T2]( + src1: Source[T1]^, + src2: Source[T2]^): Source[Either[T1, T2]]^{src1, src2} = + val left = src1.transformValuesWith(Left(_)) // ok + val right = src2.transformValuesWith(Right(_)) // ok + race(left, right) \ No newline at end of file From a04c0981cbed6f8cbe1f28c7af93ce0e6c795298 Mon Sep 17 00:00:00 2001 From: odersky Date: Sat, 4 Oct 2025 19:17:28 +0200 Subject: [PATCH 02/12] Add a test from left over previous PR Also: add another test that demonstrates some behavior relating to default parameters. Also: Rename a test so that we don't accidentally get the test file. In general, it's a bad idea to use a source file name in the compiler code for a test since we often get the wrong file when loading it into the editor. --- tests/pos-macros/i22584/Main.scala | 2 +- tests/pos-macros/i22584/Types.scala | 2 +- tests/run/curried-using-threading.scala | 10 ++++++++++ 3 files changed, 12 insertions(+), 2 deletions(-) create mode 100644 tests/run/curried-using-threading.scala diff --git a/tests/pos-macros/i22584/Main.scala b/tests/pos-macros/i22584/Main.scala index 4b6442078f96..0de80bbf4e07 100644 --- a/tests/pos-macros/i22584/Main.scala +++ b/tests/pos-macros/i22584/Main.scala @@ -1,4 +1,4 @@ -import Types.* +import types.* @main def main() = Macros.myMacro[MyClass1] diff --git a/tests/pos-macros/i22584/Types.scala b/tests/pos-macros/i22584/Types.scala index 01560035ca60..a8c29430ad82 100644 --- a/tests/pos-macros/i22584/Types.scala +++ b/tests/pos-macros/i22584/Types.scala @@ -1,4 +1,4 @@ -object Types { +object types { final case class MyClass1( int: Int, string: String, diff --git a/tests/run/curried-using-threading.scala b/tests/run/curried-using-threading.scala new file mode 100644 index 000000000000..329e4698fe39 --- /dev/null +++ b/tests/run/curried-using-threading.scala @@ -0,0 +1,10 @@ +case class Context(str: String) + +def root(using Context): String = summon[Context].str + +def narrow(using Context)(owner: String = root) = owner + +given Context("alpha") + +@main def Test = assert(narrow() == "alpha") + From 97927acbbc5c0f5dff40dd90f7221e0c7803fabb Mon Sep 17 00:00:00 2001 From: odersky Date: Sun, 5 Oct 2025 12:53:38 +0200 Subject: [PATCH 03/12] Add cap when creating an object of a Capability class Was cap.rd before, which was a left-over of the old model. --- .../src/dotty/tools/dotc/cc/Capability.scala | 5 ++-- .../dotty/tools/dotc/cc/CheckCaptures.scala | 24 ++++++++++++++----- tests/neg-custom-args/captures/boundary.check | 14 +++++------ .../captures/extending-cap-classes.check | 14 ++++++----- tests/neg-custom-args/captures/i21614.check | 19 ++++----------- tests/neg-custom-args/captures/i21614.scala | 2 +- 6 files changed, 41 insertions(+), 37 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 98fd5e7dda9e..c7f2e03589b3 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -950,10 +950,9 @@ object Capabilities: i" when instantiating argument of unapply with type $info" case LocalInstance(restpe) => i" when instantiating expected result type $restpe of function literal" - case NewMutable(tp) => - i" when constructing mutable $tp" case NewCapability(tp) => - i" when constructing Capability instance $tp" + val kind = if tp.derivesFromMutable then "mutable" else "Capability instance" + i" when constructing $kind $tp" case LambdaExpected(respt) => i" when instantiating expected result type $respt of lambda" case LambdaActual(restp: Type) => diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index ab4bbb9875d6..67df5146af17 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -863,16 +863,13 @@ class CheckCaptures extends Recheck, SymTransformer: * * Second half: union of initial capture set and all capture sets of arguments * to tracked parameters. The initial capture set `initCs` is augmented with - * - FreshCap(...) if `core` extends Mutable - * - FreshCap(...).rd if `core` extends Capability + * a fresh cap if `core` extends Capability. */ def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) = var refined: Type = core var allCaptures: CaptureSet = - if core.derivesFromMutable then - initCs ++ FreshCap(Origin.NewMutable(core)).singletonCaptureSet - else if core.derivesFromCapability then - initCs ++ FreshCap(Origin.NewCapability(core)).readOnly.singletonCaptureSet + if core.derivesFromCapability + then initCs ++ FreshCap(Origin.NewCapability(core)).singletonCaptureSet else initCs for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol @@ -897,6 +894,21 @@ class CheckCaptures extends Recheck, SymTransformer: val (refined, cs) = addParamArgRefinements(core, initCs) refined.capturing(cs) + /* + def impliedFresh: CaptureSet = + cls.info.fields.foldLeft(CaptureSet.empty: CaptureSet): (cs, field) => + if !cs.isAlwaysEmpty || field.symbol.is(ParamAccessor) then + cs + else + val fieldFreshCaps = field.info.spanCaptureSet.elems.filter(_.isTerminalCapability) + if fieldFreshCaps.isEmpty then cs + else + val classFresh = FreshCap(ctx.owner, NoPrefix, ) + if fieldFreshCaps.forall(_.isReadOnly) + then cs + classFresh.readOnly + else cs + classFresh + */ + augmentConstructorType(resType, capturedVars(cls)) .showing(i"constr type $mt with $argTypes%, % in $constr = $result", capt) end refineConstructorInstance diff --git a/tests/neg-custom-args/captures/boundary.check b/tests/neg-custom-args/captures/boundary.check index 0cac2ec2f60d..3d14805014e7 100644 --- a/tests/neg-custom-args/captures/boundary.check +++ b/tests/neg-custom-args/captures/boundary.check @@ -2,15 +2,15 @@ 4 | boundary[AnyRef^]: 5 | l1 ?=> // error // error | ^ - |Found: scala.util.boundary.Label[Object^'s1]^{cap.rd} - |Required: scala.util.boundary.Label[Object^]^² + |Found: scala.util.boundary.Label[Object^'s1]^ + |Required: scala.util.boundary.Label[Object^²]^³ | - |Note that capability cap² cannot be included in outer capture set 's1. + |Note that capability cap cannot be included in outer capture set 's1. | - |where: ^ refers to the universal root capability - | ^² refers to a fresh root capability classified as Control in the type of value local - | cap is a fresh root capability classified as Control created in value local when constructing Capability instance scala.util.boundary.Label[Object^'s1] - | cap² is the universal root capability + |where: ^ refers to a fresh root capability classified as Control created in value local when constructing Capability instance scala.util.boundary.Label[Object^'s1] + | ^² refers to the universal root capability + | ^³ refers to a fresh root capability classified as Control in the type of value local + | cap is the universal root capability 6 | boundary[Unit]: l2 ?=> 7 | boundary.break(l2)(using l1) // error 8 | ??? diff --git a/tests/neg-custom-args/captures/extending-cap-classes.check b/tests/neg-custom-args/captures/extending-cap-classes.check index be0e94316f71..5fd80f8e2fba 100644 --- a/tests/neg-custom-args/captures/extending-cap-classes.check +++ b/tests/neg-custom-args/captures/extending-cap-classes.check @@ -1,23 +1,25 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:7:15 ------------------------- 7 | val x2: C1 = new C2 // error | ^^^^^^ - |Found: C2^{cap.rd} + |Found: C2^ |Required: C1 | - |Note that capability cap.rd is not included in capture set {}. + |Note that capability cap is not included in capture set {}. | - |where: cap is a fresh root capability classified as SharedCapability created in value x2 when constructing Capability instance C2 + |where: ^ refers to a fresh root capability classified as SharedCapability created in value x2 when constructing Capability instance C2 + | cap is a fresh root capability classified as SharedCapability created in value x2 when constructing Capability instance C2 | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:8:15 ------------------------- 8 | val x3: C1 = new C3 // error | ^^^^^^ - |Found: C3^{cap.rd} + |Found: C3^ |Required: C1 | - |Note that capability cap.rd is not included in capture set {}. + |Note that capability cap is not included in capture set {}. | - |where: cap is a fresh root capability classified as SharedCapability created in value x3 when constructing Capability instance C3 + |where: ^ refers to a fresh root capability classified as SharedCapability created in value x3 when constructing Capability instance C3 + | cap is a fresh root capability classified as SharedCapability created in value x3 when constructing Capability instance C3 | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:13:15 ------------------------ diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check index 89b9a4b216c1..2f4de5702c62 100644 --- a/tests/neg-custom-args/captures/i21614.check +++ b/tests/neg-custom-args/captures/i21614.check @@ -1,5 +1,5 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:33 --------------------------------------- -12 | files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)? +12 | files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)? | ^ |Found: (f : F) |Required: File^ @@ -11,25 +11,16 @@ | cap² is a fresh root capability classified as SharedCapability created in anonymous function of type (f²: F): Logger when checking argument to parameter f of constructor Logger | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/i21614.scala:12:8 ------------------------------------------------------------- -12 | files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)? - | ^^^^^^^^^ - |Type variable U of method map cannot be instantiated to Logger{val f: File^'s1}^{cap.rd} since - |that type captures the root capability `cap`. - |This is often caused by a local capability in an argument of method map - |leaking as part of its result. - | - |where: cap is a root capability associated with the result type of (f²: F^{files*}): Logger{val f: File^'s1}^'s2 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 --------------------------------------- 15 | files.map(new Logger(_)) // error, Q: can we improve the error message? | ^^^^^^^^^^^^^ - |Found: (_$1: File^'s3) ->{C} Logger{val f: File^{_$1}}^{cap.rd, _$1} - |Required: File^{C} => Logger{val f: File^'s4}^'s5 + |Found: (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{cap, _$1} + |Required: File^{C} => Logger{val f: File^'s2}^'s3 | |Note that capability C is not classified as trait SharedCapability, therefore it - |cannot be included in capture set 's3 of parameter _$1 of SharedCapability elements. + |cannot be included in capture set 's1 of parameter _$1 of SharedCapability elements. | |where: => refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map - | cap is a root capability associated with the result type of (_$1: File^'s3): Logger{val f: File^{_$1}}^{cap.rd, _$1} + | cap is a root capability associated with the result type of (_$1: File^'s1): Logger{val f: File^{_$1}}^{cap, _$1} | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21614.scala b/tests/neg-custom-args/captures/i21614.scala index 54e3ea863677..11929f2414db 100644 --- a/tests/neg-custom-args/captures/i21614.scala +++ b/tests/neg-custom-args/captures/i21614.scala @@ -9,7 +9,7 @@ trait File extends SharedCapability class Logger(f: File^) extends SharedCapability // <- will work if we remove the extends clause def mkLoggers1[F <: File^](files: List[F]): List[Logger^] = - files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)? + files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)? def mkLoggers2[C^](files: List[File^{C}]): List[Logger^] = files.map(new Logger(_)) // error, Q: can we improve the error message? From ecc8ba32988e0739b5843e9590545cedfbd9eda5 Mon Sep 17 00:00:00 2001 From: odersky Date: Sun, 5 Oct 2025 19:34:40 +0200 Subject: [PATCH 04/12] Refine isField test Refine the isField test in SymUtils to exclude non-members and phantom symbols --- compiler/src/dotty/tools/dotc/core/SymUtils.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/core/SymUtils.scala b/compiler/src/dotty/tools/dotc/core/SymUtils.scala index c7733acbfdec..435320fec568 100644 --- a/compiler/src/dotty/tools/dotc/core/SymUtils.scala +++ b/compiler/src/dotty/tools/dotc/core/SymUtils.scala @@ -313,7 +313,7 @@ class SymUtils: } def isField(using Context): Boolean = - self.isTerm && !self.is(Method) + self.isTerm && !self.isOneOf(Method | PhantomSymbol | NonMember) def isEnumCase(using Context): Boolean = self.isAllOf(EnumCase, butNot = JavaDefined) From d2abdfef0a2ff3fc511bfe0ea909cb0931f0cac4 Mon Sep 17 00:00:00 2001 From: odersky Date: Sun, 5 Oct 2025 19:39:05 +0200 Subject: [PATCH 05/12] Let FreshCaps in field types contribute to class captures A fresh in the capture set of a class field now causes a fresh to be added to the capture set of every instance of that class. --- .../src/dotty/tools/dotc/cc/Capability.scala | 20 +++-- .../dotty/tools/dotc/cc/CheckCaptures.scala | 73 ++++++++++++++----- library/src/scala/caps/package.scala | 21 +++++- library/src/scala/collection/Iterator.scala | 8 +- .../scala/collection/generic/IsIterable.scala | 2 + .../collection/generic/IsIterableOnce.scala | 2 + .../src/scala/collection/generic/IsSeq.scala | 2 + .../immutable/LazyListIterable.scala | 3 +- tests/neg-custom-args/captures/cc-this.check | 2 +- .../captures/fresh-fields.check | 60 +++++++++++++++ .../captures/fresh-fields.scala | 33 +++++++++ tests/neg-custom-args/captures/i24137.check | 22 ++++++ tests/neg-custom-args/captures/i24137.scala | 18 +++++ tests/neg-custom-args/captures/lazyref.check | 9 ++- tests/neg-custom-args/captures/lazyref.scala | 2 +- tests/pos-custom-args/captures/i21507.scala | 3 +- 16 files changed, 246 insertions(+), 34 deletions(-) create mode 100644 tests/neg-custom-args/captures/fresh-fields.check create mode 100644 tests/neg-custom-args/captures/fresh-fields.scala create mode 100644 tests/neg-custom-args/captures/i24137.check create mode 100644 tests/neg-custom-args/captures/i24137.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index c7f2e03589b3..93f0ec38e411 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -896,18 +896,26 @@ object Capabilities: else if cls2.isSubClass(cls1) then cls2 else defn.NothingClass - def joinClassifiers(cs1: Classifiers, cs2: Classifiers)(using Context): Classifiers = + /** The smallest list D of class symbols in cs1 and cs2 such that + * every class symbol in cs1 and cs2 is a subclass of a class symbol in D + */ + def dominators(cs1: List[ClassSymbol], cs2: List[ClassSymbol])(using Context): List[ClassSymbol] = // Drop classes that subclass classes of the other set // @param proper If true, only drop proper subclasses of a class of the other set def filterSub(cs1: List[ClassSymbol], cs2: List[ClassSymbol], proper: Boolean) = cs1.filter: cls1 => !cs2.exists: cls2 => cls1.isSubClass(cls2) && (!proper || cls1 != cls2) + filterSub(cs1, cs2, proper = true) ++ filterSub(cs2, cs1, proper = false) + + def joinClassifiers(cs1: Classifiers, cs2: Classifiers)(using Context): Classifiers = (cs1, cs2) match - case (Unclassified, _) | (_, Unclassified) => Unclassified - case (UnknownClassifier, _) | (_, UnknownClassifier) => UnknownClassifier + case (Unclassified, _) | (_, Unclassified) => + Unclassified + case (UnknownClassifier, _) | (_, UnknownClassifier) => + UnknownClassifier case (ClassifiedAs(cs1), ClassifiedAs(cs2)) => - ClassifiedAs(filterSub(cs1, cs2, proper = true) ++ filterSub(cs2, cs1, proper = false)) + ClassifiedAs(dominators(cs1, cs2)) /** The place of - and cause for - creating a fresh capability. Used for * error diagnostics @@ -920,7 +928,7 @@ object Capabilities: case ResultInstance(methType: Type, meth: Symbol) case UnapplyInstance(info: MethodType) case LocalInstance(restpe: Type) - case NewMutable(tp: Type) + case NewInstance(tp: Type) case NewCapability(tp: Type) case LambdaExpected(respt: Type) case LambdaActual(restp: Type) @@ -950,6 +958,8 @@ object Capabilities: i" when instantiating argument of unapply with type $info" case LocalInstance(restpe) => i" when instantiating expected result type $restpe of function literal" + case NewInstance(tp) => + i" when constructing instance $tp" case NewCapability(tp) => val kind = if tp.derivesFromMutable then "mutable" else "Capability instance" i" when constructing $kind $tp" diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 67df5146af17..a284bce7ab94 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -17,6 +17,7 @@ import typer.Checking.{checkBounds, checkAppliedTypesIn} import typer.ErrorReporting.{Addenda, NothingToAdd, err} import typer.ProtoTypes.{LhsProto, WildcardSelectionProto, SelectionProto} import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property} +import util.chaining.tap import transform.{Recheck, PreRecheck, CapturedVars} import Recheck.* import scala.collection.mutable @@ -247,6 +248,11 @@ class CheckCaptures extends Recheck, SymTransformer: val ccState1 = new CCState // Dotty problem: Rename to ccState ==> Crash in ExplicitOuter + /** A cache that stores for each class the classifiers of all fresh instances + * in the types of its fields. + */ + val knownFresh = new util.EqHashMap[Symbol, List[ClassSymbol]] + class CaptureChecker(ictx: Context) extends Rechecker(ictx), CheckerAPI: // println(i"checking ${ictx.source}"(using ictx)) @@ -620,9 +626,7 @@ class CheckCaptures extends Recheck, SymTransformer: fn.tpe.widenDealias match case tl: TypeLambda => tl.paramNames case ref: AppliedType if ref.typeSymbol.isClass => ref.typeSymbol.typeParams.map(_.name) - case t => - println(i"parent type: $t") - args.map(_ => EmptyTypeName) + case t => args.map(_ => EmptyTypeName) for case (arg: TypeTree, pname) <- args.lazyZip(paramNames) do def where = if sym.exists then i" in an argument of $sym" else "" @@ -870,7 +874,7 @@ class CheckCaptures extends Recheck, SymTransformer: var allCaptures: CaptureSet = if core.derivesFromCapability then initCs ++ FreshCap(Origin.NewCapability(core)).singletonCaptureSet - else initCs + else initCs ++ impliedByFields(core) for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol if !getter.is(Private) && getter.hasTrackedParts then @@ -894,20 +898,53 @@ class CheckCaptures extends Recheck, SymTransformer: val (refined, cs) = addParamArgRefinements(core, initCs) refined.capturing(cs) - /* - def impliedFresh: CaptureSet = - cls.info.fields.foldLeft(CaptureSet.empty: CaptureSet): (cs, field) => - if !cs.isAlwaysEmpty || field.symbol.is(ParamAccessor) then - cs - else - val fieldFreshCaps = field.info.spanCaptureSet.elems.filter(_.isTerminalCapability) - if fieldFreshCaps.isEmpty then cs - else - val classFresh = FreshCap(ctx.owner, NoPrefix, ) - if fieldFreshCaps.forall(_.isReadOnly) - then cs + classFresh.readOnly - else cs + classFresh - */ + /** The additional capture set implied by the capture sets of its fields. This + * is either empty or, if some fields have a terminal capability in their span + * capture sets, it consists of a single fresh cap that subsumes all these terminal + * capabiltities. Class parameters are not counted. + */ + def impliedByFields(core: Type): CaptureSet = + var infos: List[String] = Nil + def pushInfo(msg: => String) = + if ctx.settings.YccVerbose.value then infos = msg :: infos + + /** The classifiers of the fresh caps in the span capture sets of all fields + * in the given class `cls`. + */ + def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match + case cls: ClassSymbol => + val fieldClassifiers = + for + sym <- cls.info.decls.toList + if sym.isField && !sym.isOneOf(DeferredOrTermParamOrAccessor) + && !sym.hasAnnotation(defn.UntrackedCapturesAnnot) + case fresh: FreshCap <- sym.info.spanCaptureSet.elems + .filter(_.isTerminalCapability) + .map(_.stripReadOnly) + .toList + _ = pushInfo(i"Note: ${sym.showLocated} captures a $fresh") + yield fresh.hiddenSet.classifier + val parentClassifiers = + cls.parentSyms.map(impliedClassifiers).filter(_.nonEmpty) + if fieldClassifiers.isEmpty && parentClassifiers.isEmpty + then Nil + else parentClassifiers.foldLeft(fieldClassifiers.distinct)(dominators) + case _ => Nil + + def fresh = + FreshCap(Origin.NewInstance(core)).tap: fresh => + if ctx.settings.YccVerbose.value then + pushInfo(i"Note: instance of $cls captures a $fresh that comes from a field") + report.echo(infos.mkString("\n"), ctx.owner.srcPos) + + knownFresh.getOrElseUpdate(cls, impliedClassifiers(cls)) match + case Nil => CaptureSet.empty + case cl :: Nil => + val result = fresh + result.hiddenSet.adoptClassifier(cl) + result.singletonCaptureSet + case _ => fresh.singletonCaptureSet + end impliedByFields augmentConstructorType(resType, capturedVars(cls)) .showing(i"constr type $mt with $argTypes%, % in $constr = $result", capt) diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index 2cd75efdf197..e6edcebdf9b2 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -173,10 +173,23 @@ end internal @experimental object unsafe: - /** - * Marks the constructor parameter as untracked. - * The capture set of this parameter will not be included in - * the capture set of the constructed object. + /** Two usages: + * + * 1. Marks the constructor parameter as untracked. + * The capture set of this parameter will not be included in + * the capture set of the constructed object. + * + * 2. Marks a class field that has a cap in its capture set, so that + * the cap is not contributed to the class instance. + * Exampple: + * + * class A { val b B^ = ... }; new A() + * + * has type A^ since b contributes a cap. But + * + * class A { @untrackedCaptures val b: B^ = ... }; new A() + * + * has type A. The `b` field does not contribute its cap. * * @note This should go into annotations. For now it is here, so that we * can experiment with it quickly between minor releases diff --git a/library/src/scala/collection/Iterator.scala b/library/src/scala/collection/Iterator.scala index 4ddef7dcb18f..bb90b859944f 100644 --- a/library/src/scala/collection/Iterator.scala +++ b/library/src/scala/collection/Iterator.scala @@ -18,6 +18,7 @@ import scala.collection.mutable.{ArrayBuffer, ArrayBuilder, Builder, ImmutableBu import scala.annotation.tailrec import scala.annotation.unchecked.uncheckedVariance import scala.runtime.Statics +import caps.unsafe.untrackedCaptures /** Iterators are data structures that allow to iterate over a sequence * of elements. They have a `hasNext` method for checking @@ -917,7 +918,12 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite */ def patch[B >: A](from: Int, patchElems: Iterator[B]^, replaced: Int): Iterator[B]^{this, patchElems} = new AbstractIterator[B] { - private[this] var origElems: Iterator[B]^ = self + // TODO We should be able to prove that origElems is safe even though it is + // declared as Iterator[B]^. We could show that origElems is never assigned a + // freh cap. Maybe we can invent another annotation that is checked and that + // shows that the `^` is just used as an upper bound for concete non-fresh + // capabilities. + @untrackedCaptures private[this] var origElems: Iterator[B]^ = self // > 0 => that many more elems from `origElems` before switching to `patchElems` // 0 => need to drop elems from `origElems` and start using `patchElems` // -1 => have dropped elems from `origElems`, will be using `patchElems` until it's empty diff --git a/library/src/scala/collection/generic/IsIterable.scala b/library/src/scala/collection/generic/IsIterable.scala index 0b80203037fc..4ba72ff3fe08 100644 --- a/library/src/scala/collection/generic/IsIterable.scala +++ b/library/src/scala/collection/generic/IsIterable.scala @@ -15,6 +15,7 @@ package generic import scala.language.`2.13` import language.experimental.captureChecking +import caps.unsafe.untrackedCaptures /** A trait which can be used to avoid code duplication when defining extension * methods that should be applicable both to existing Scala collections (i.e., @@ -123,6 +124,7 @@ transparent trait IsIterable[Repr] extends IsIterableOnce[Repr] { type C @deprecated("'conversion' is now a method named 'apply'", "2.13.0") + @untrackedCaptures override val conversion: Repr => IterableOps[A, Iterable, C] = apply(_) /** A conversion from the type `Repr` to `IterableOps[A, Iterable, C]` */ diff --git a/library/src/scala/collection/generic/IsIterableOnce.scala b/library/src/scala/collection/generic/IsIterableOnce.scala index bced6e190206..6bdad3287ede 100644 --- a/library/src/scala/collection/generic/IsIterableOnce.scala +++ b/library/src/scala/collection/generic/IsIterableOnce.scala @@ -16,6 +16,7 @@ package generic import scala.language.`2.13` import language.experimental.captureChecking +import caps.unsafe.untrackedCaptures /** Type class witnessing that a collection representation type `Repr` has * elements of type `A` and has a conversion to `IterableOnce[A]`. @@ -46,6 +47,7 @@ transparent trait IsIterableOnce[Repr] { type A @deprecated("'conversion' is now a method named 'apply'", "2.13.0") + @untrackedCaptures val conversion: Repr => IterableOnce[A] = apply(_) /** A conversion from the representation type `Repr` to a `IterableOnce[A]`. */ diff --git a/library/src/scala/collection/generic/IsSeq.scala b/library/src/scala/collection/generic/IsSeq.scala index 04a94c5e5da0..3e5b644a7ea1 100644 --- a/library/src/scala/collection/generic/IsSeq.scala +++ b/library/src/scala/collection/generic/IsSeq.scala @@ -15,6 +15,7 @@ package generic import scala.language.`2.13` import language.experimental.captureChecking +import caps.unsafe.untrackedCaptures import scala.reflect.ClassTag @@ -31,6 +32,7 @@ import scala.reflect.ClassTag transparent trait IsSeq[Repr] extends IsIterable[Repr] { @deprecated("'conversion' is now a method named 'apply'", "2.13.0") + @untrackedCaptures override val conversion: Repr => SeqOps[A, Iterable, C] = apply(_) /** A conversion from the type `Repr` to `SeqOps[A, Iterable, C]` diff --git a/library/src/scala/collection/immutable/LazyListIterable.scala b/library/src/scala/collection/immutable/LazyListIterable.scala index f1d14bbb1fad..790b640fb7f6 100644 --- a/library/src/scala/collection/immutable/LazyListIterable.scala +++ b/library/src/scala/collection/immutable/LazyListIterable.scala @@ -25,6 +25,7 @@ import scala.collection.generic.SerializeEnd import scala.collection.mutable.{Builder, ReusableBuilder, StringBuilder} import scala.language.implicitConversions import scala.runtime.Statics +import caps.unsafe.untrackedCaptures /** This class implements an immutable linked list. We call it "lazy" * because it computes its elements only when they are needed. @@ -1374,7 +1375,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] { private final class WithFilter[A] private[LazyListIterable](lazyList: LazyListIterable[A]^, p: A => Boolean) extends collection.WithFilter[A, LazyListIterable] { - private[this] val filtered = lazyList.filter(p) + @untrackedCaptures private[this] val filtered = lazyList.filter(p) def map[B](f: A => B): LazyListIterable[B]^{this, f} = filtered.map(f) def flatMap[B](f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f} = filtered.flatMap(f) def foreach[U](f: A => U): Unit = filtered.foreach(f) diff --git a/tests/neg-custom-args/captures/cc-this.check b/tests/neg-custom-args/captures/cc-this.check index a66e210461ee..77c32e211013 100644 --- a/tests/neg-custom-args/captures/cc-this.check +++ b/tests/neg-custom-args/captures/cc-this.check @@ -18,4 +18,4 @@ -- Error: tests/neg-custom-args/captures/cc-this.scala:33:8 ------------------------------------------------------------ 33 | def c3 = c2.y // error | ^ - | Separation failure: method c3's inferred result type C{val x: () => Int}^{cc} hides non-local parameter cc + | Separation failure: method c3's inferred result type C{val x: () => Int}^ hides non-local parameter cc diff --git a/tests/neg-custom-args/captures/fresh-fields.check b/tests/neg-custom-args/captures/fresh-fields.check new file mode 100644 index 000000000000..b49da1ef381f --- /dev/null +++ b/tests/neg-custom-args/captures/fresh-fields.check @@ -0,0 +1,60 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:25:13 --------------------------------- +25 | val _: B = b // error + | ^ + | Found: (b : B^) + | Required: B + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ refers to a fresh root capability in the type of value b + | cap is a fresh root capability in the type of value b + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:27:13 --------------------------------- +27 | val _: C = c // error + | ^ + | Found: (c : C^) + | Required: C + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ refers to a fresh root capability in the type of value c + | cap is a fresh root capability in the type of value c + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:29:13 --------------------------------- +29 | val _: D = d // error + | ^ + | Found: (d : D^) + | Required: D + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ refers to a fresh root capability in the type of value d + | cap is a fresh root capability in the type of value d + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:31:13 --------------------------------- +31 | val _: E = e // error + | ^ + | Found: (e : E^) + | Required: E + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ refers to a fresh root capability classified as SharedCapability in the type of value e + | cap is a fresh root capability classified as SharedCapability in the type of value e + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:33:13 --------------------------------- +33 | val _: F = f // error + | ^ + | Found: (f : F^) + | Required: F + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ refers to a fresh root capability in the type of value f + | cap is a fresh root capability in the type of value f + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/fresh-fields.scala b/tests/neg-custom-args/captures/fresh-fields.scala new file mode 100644 index 000000000000..cbfa32cb201a --- /dev/null +++ b/tests/neg-custom-args/captures/fresh-fields.scala @@ -0,0 +1,33 @@ +open class A: + def a: A^ = A() // no fresh contribution since `a` is a method + val as: List[A^] = List(A()) // no fresh contribution since A^ is boxed + +class B: + private val b: A^ = A() // contributes fresh + +class C extends B // contributes fresh via B + +class D: + private val f: () -> A = () => new A() + private val b: () -> A^ = f // contributes fresh + +class Shared extends caps.SharedCapability + +trait E: + private val e: Shared = Shared() + +class F extends B, E + +def test() = + val a = A() + val _: A = a // ok + val b = B() + val _: B = b // error + val c = C() + val _: C = c // error + val d = D() + val _: D = d // error + val e = new E() {} + val _: E = e // error + val f = F() + val _: F = f // error diff --git a/tests/neg-custom-args/captures/i24137.check b/tests/neg-custom-args/captures/i24137.check new file mode 100644 index 000000000000..3f7d14144c32 --- /dev/null +++ b/tests/neg-custom-args/captures/i24137.check @@ -0,0 +1,22 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i24137.scala:16:21 --------------------------------------- +16 | val _: B^{async} = b // error, but could be OK if we have a way to mark + | ^ + | Found: (b : B{val elem1: A^{a}; val elem2: A^{a}}^{cap, a}) + | Required: B^{async} + | + | Note that capability cap is not included in capture set {async}. + | + | where: cap is a fresh root capability in the type of value b + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i24137.scala:18:23 --------------------------------------- +18 | val b1: B^{async} = B(a, a) // error but could also be OK + | ^^^^^^^ + | Found: B{val elem1: (a : A^{async}); val elem2: (a : A^{async})}^{cap, a} + | Required: B^{async} + | + | Note that capability cap is not included in capture set {async}. + | + | where: cap is a fresh root capability created in value b1 when constructing instance B + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i24137.scala b/tests/neg-custom-args/captures/i24137.scala new file mode 100644 index 000000000000..033fa1b7d2f2 --- /dev/null +++ b/tests/neg-custom-args/captures/i24137.scala @@ -0,0 +1,18 @@ +//< using options -Ycc-verbose +import caps.{cap, Shared, SharedCapability} + +open class A + +class B(elem1: A^{cap.only[Shared]}, elem2: A^{cap.only[Shared]}): + private var curElem: A^ = elem1 // problem is curElem contibutes cap to B(). + def next() = + curElem = elem2 + +class Async extends caps.SharedCapability + +def test(async: Async) = + val a: A^{async} = A() + val b = B(a, a) + val _: B^{async} = b // error, but could be OK if we have a way to mark + // curElem above as not contributing anything + val b1: B^{async} = B(a, a) // error but could also be OK diff --git a/tests/neg-custom-args/captures/lazyref.check b/tests/neg-custom-args/captures/lazyref.check index 52e787f66553..56d0c8a2d329 100644 --- a/tests/neg-custom-args/captures/lazyref.check +++ b/tests/neg-custom-args/captures/lazyref.check @@ -34,14 +34,19 @@ | Note that capability ref4 is not included in capture set {cap1}. | | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/lazyref.scala:6:14 ------------------------------------------------------------ +6 | def get: () => T = elem // error: separation failure + | ^^^^^^^ + | Separation failure: method get's result type () => T hides non-local this of class class LazyRef. + | The access must be in a consume method to allow this. -- Error: tests/neg-custom-args/captures/lazyref.scala:8:24 ------------------------------------------------------------ 8 | new LazyRef(() => f(elem())) // error: separation failure | ^^^^ | Separation failure: Illegal access to {LazyRef.this.elem} which is hidden by the previous definition - | of value get with type () => T. + | of method get with result type () => T. | This type hides capabilities {LazyRef.this.elem} | - | where: => refers to a fresh root capability in the type of value get + | where: => refers to a fresh root capability in the result type of method get -- Error: tests/neg-custom-args/captures/lazyref.scala:29:9 ------------------------------------------------------------ 29 | .map(g) // error: separation failure | ^ diff --git a/tests/neg-custom-args/captures/lazyref.scala b/tests/neg-custom-args/captures/lazyref.scala index ea3897484857..28149c6d10a3 100644 --- a/tests/neg-custom-args/captures/lazyref.scala +++ b/tests/neg-custom-args/captures/lazyref.scala @@ -3,7 +3,7 @@ class CC type Cap = CC^ class LazyRef[T](val elem: () => T): - val get: () => T = elem + def get: () => T = elem // error: separation failure def map[U](f: T => U): LazyRef[U]^{f, this} = new LazyRef(() => f(elem())) // error: separation failure diff --git a/tests/pos-custom-args/captures/i21507.scala b/tests/pos-custom-args/captures/i21507.scala index 455aa3940fb6..953c8a0b0dca 100644 --- a/tests/pos-custom-args/captures/i21507.scala +++ b/tests/pos-custom-args/captures/i21507.scala @@ -4,7 +4,8 @@ trait Box[Cap^]: def store(f: (() -> Unit)^{Cap}): Unit def run[Cap^](f: Box[{Cap}]^{Cap} => Unit): Box[{Cap}]^{Cap} = - new Box[{Cap}]: + new Box[{Cap}] { private var item: () ->{Cap} Unit = () => () def store(f: () ->{Cap} Unit): Unit = item = f // was error, now ok + } From 93cb35c32765e1d6f825183c8922d77568fc5e14 Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 6 Oct 2025 16:02:25 +0200 Subject: [PATCH 06/12] Don't store elements in hidden sets under CCState.collapseFresh --- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 2 +- .../src/dotty/tools/dotc/core/Types.scala | 3 ++ .../captures/cc-poly-varargs.check | 34 ------------------- tests/neg-custom-args/captures/cc-this.check | 4 --- tests/neg-custom-args/captures/cc-this.scala | 2 +- .../captures/cc-poly-varargs-original.scala} | 4 +-- 6 files changed, 7 insertions(+), 42 deletions(-) delete mode 100644 tests/neg-custom-args/captures/cc-poly-varargs.check rename tests/{neg-custom-args/captures/cc-poly-varargs.scala => pos-custom-args/captures/cc-poly-varargs-original.scala} (73%) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index d4f058de2c38..1055c668232a 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -1392,7 +1392,7 @@ object CaptureSet: def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean = if hidden.isConst then false else - hidden.add(elem)(using ctx, this) + if !CCState.collapseFresh then hidden.add(elem)(using ctx, this) true /** If root1 and root2 belong to the same binder but have different originalBinders diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index ec6d10c1712d..993775fcb7f0 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -923,6 +923,9 @@ object Types extends TypeUtils { else val isRefinedMethod = rinfo.isInstanceOf[MethodOrPoly] val joint = CCState.withCollapsedFresh: + // We have to do a collapseFresh here since `pdenot` will see the class + // view and a fresh in the class will not be able to subsume a + // refinement from outside since level checking would fail. pdenot.meet( new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod), pre, diff --git a/tests/neg-custom-args/captures/cc-poly-varargs.check b/tests/neg-custom-args/captures/cc-poly-varargs.check deleted file mode 100644 index 764274813faf..000000000000 --- a/tests/neg-custom-args/captures/cc-poly-varargs.check +++ /dev/null @@ -1,34 +0,0 @@ --- Error: tests/neg-custom-args/captures/cc-poly-varargs.scala:11:13 --------------------------------------------------- -11 | val left = src1.transformValuesWith(Left(_)) // error - | ^^^^ - |Separation failure: argument of type (src1 : Source[T1, scala.caps.CapSet^{Cap}]^{Cap}) - |to method transformValuesWith: [T, Cap >: scala.caps.CapSet <: scala.caps.CapSet^] - | (src: Source[T, scala.caps.CapSet^{Cap}]^)[U](f: T ->{Cap} U): Source[U, scala.caps.CapSet^{Cap}]^{src, f} - |corresponds to capture-polymorphic formal parameter src of type Source[T1^'s3, scala.caps.CapSet^{Cap}]^ - |and hides capabilities {src1}. - |Some of these overlap with the captures of the function result with type Source[Left[T1^'s1, Nothing]^'s2, scala.caps.CapSet^{Cap}]^{src1}. - | - | Hidden set of current argument : {src1} - | Hidden footprint of current argument : {src1, Cap} - | Capture set of function result : {src1, Cap} - | Footprint set of function result : {src1, Cap} - | The two sets overlap at : {src1, Cap} - | - |where: ^ refers to a fresh root capability created in value left when checking argument to parameter src of method transformValuesWith --- Error: tests/neg-custom-args/captures/cc-poly-varargs.scala:12:14 --------------------------------------------------- -12 | val right = src2.transformValuesWith(Right(_)) // error - | ^^^^ - |Separation failure: argument of type (src2 : Source[T2, scala.caps.CapSet^{Cap}]^{Cap}) - |to method transformValuesWith: [T, Cap >: scala.caps.CapSet <: scala.caps.CapSet^] - | (src: Source[T, scala.caps.CapSet^{Cap}]^)[U](f: T ->{Cap} U): Source[U, scala.caps.CapSet^{Cap}]^{src, f} - |corresponds to capture-polymorphic formal parameter src of type Source[T2^'s6, scala.caps.CapSet^{Cap}]^ - |and hides capabilities {src2}. - |Some of these overlap with the captures of the function result with type Source[Right[Nothing, T2^'s4]^'s5, scala.caps.CapSet^{Cap}]^{src2}. - | - | Hidden set of current argument : {src2} - | Hidden footprint of current argument : {src2, Cap} - | Capture set of function result : {src2, Cap} - | Footprint set of function result : {src2, Cap} - | The two sets overlap at : {src2, Cap} - | - |where: ^ refers to a fresh root capability created in value right when checking argument to parameter src of method transformValuesWith diff --git a/tests/neg-custom-args/captures/cc-this.check b/tests/neg-custom-args/captures/cc-this.check index 77c32e211013..d7bd06246218 100644 --- a/tests/neg-custom-args/captures/cc-this.check +++ b/tests/neg-custom-args/captures/cc-this.check @@ -15,7 +15,3 @@ 19 | class C4(val f: () => Int) extends C3 // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |reference (C4.this.f : () => Int) captured by this self type is not included in the allowed capture set {} of pure base class class C3 --- Error: tests/neg-custom-args/captures/cc-this.scala:33:8 ------------------------------------------------------------ -33 | def c3 = c2.y // error - | ^ - | Separation failure: method c3's inferred result type C{val x: () => Int}^ hides non-local parameter cc diff --git a/tests/neg-custom-args/captures/cc-this.scala b/tests/neg-custom-args/captures/cc-this.scala index 3d9f8ca5cf53..6182e840edef 100644 --- a/tests/neg-custom-args/captures/cc-this.scala +++ b/tests/neg-custom-args/captures/cc-this.scala @@ -30,6 +30,6 @@ def test2(using consume cc: Cap) = def c1 = new C(f) def c2 = c1 - def c3 = c2.y // error + def c3 = c2.y // was error, now OK val c4: C^ = c3 val _ = c3: C^ diff --git a/tests/neg-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs-original.scala similarity index 73% rename from tests/neg-custom-args/captures/cc-poly-varargs.scala rename to tests/pos-custom-args/captures/cc-poly-varargs-original.scala index 6907bc7f91fa..9b2bba06e2d1 100644 --- a/tests/neg-custom-args/captures/cc-poly-varargs.scala +++ b/tests/pos-custom-args/captures/cc-poly-varargs-original.scala @@ -8,6 +8,6 @@ def race[T, Cap^](sources: Source[T, {Cap}]^{Cap}*): Source[T, {Cap}]^{Cap} = ?? def either[T1, T2, Cap^]( src1: Source[T1, {Cap}]^{Cap}, src2: Source[T2, {Cap}]^{Cap}): Source[Either[T1, T2], {Cap}]^{Cap} = - val left = src1.transformValuesWith(Left(_)) // error - val right = src2.transformValuesWith(Right(_)) // error + val left = src1.transformValuesWith(Left(_)) // was error, now OK + val right = src2.transformValuesWith(Right(_)) // was error, now OK race(left, right) From ba1ef96aef1c0246ae79bb900fb91bf7441591ad Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 6 Oct 2025 18:21:21 +0200 Subject: [PATCH 07/12] Avoid assertion violation due to empty footprint overlap - Drop the assertion and handle the case of empty overlap - At the same time, avoid the empty overlap by taking complete instead of direct footprints. Also: Improve printing of FreshCap prefixes --- compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 11 ++++++----- .../src/dotty/tools/dotc/printing/PlainPrinter.scala | 3 ++- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 65aa2fdce124..46812ecc0d91 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -272,7 +272,6 @@ object SepCheck: * 3. the set itself if it consists only of hidden terminal capabilities. */ def reduced(using Context): Refs = - assert(!refs.isEmpty) val concrete = refs.nonPeaks if !concrete.isEmpty then concrete else @@ -356,9 +355,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val hiddenFootprint = hiddenSet.directFootprint val clashFootprint = clashSet.directFootprint val shared = hiddenFootprint.overlapWith(clashFootprint).reduced - shared.nth(0) match + if shared.isEmpty then i"${CaptureSet(shared)}" + else shared.nth(0) match case fresh: FreshCap => - if fresh.hiddenSet.owner.exists then i"$fresh of ${fresh.hiddenSet.owner}" else i"$fresh" + if fresh.hiddenSet.owner.exists then i"{$fresh of ${fresh.hiddenSet.owner}}" else i"$fresh" case _ => i"${CaptureSet(shared)}" @@ -402,8 +402,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: else i" with type ${clashing.nuType}" val hiddenSet = formalCaptures(polyArg).transHiddenSet val clashSet = if clashIdx == -1 then deepCaptures(clashing) else spanCaptures(clashing) - val hiddenFootprint = hiddenSet.directFootprint - val clashFootprint = clashSet.directFootprint + val hiddenFootprint = hiddenSet.completeFootprint + val clashFootprint = clashSet.completeFootprint + report.error( em"""Separation failure: argument of type ${polyArg.nuType} |to $funStr diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala index bdf527dfbebd..c84ac611f363 100644 --- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -493,7 +493,8 @@ class PlainPrinter(_ctx: Context) extends Printer { else s" classified as ${c.hiddenSet.classifier.name.show}" def prefixTxt: Text = c.prefix match case NoPrefix | _: ThisType => "" - case pre => pre.show ~ "." + case pre: SingletonType => toTextRef(pre) ~ "." + case pre => toText(pre) ~ "." def core: Text = if ccVerbose then s"" else "cap" From 339581e5ed84b19dad94e7d004b44effca747af1 Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 6 Oct 2025 18:23:55 +0200 Subject: [PATCH 08/12] Establish a "covers" relation between a fresh for an object and a fresh for one of its fields. --- .../src/dotty/tools/dotc/cc/Capability.scala | 33 ++++++- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 1 + .../src/dotty/tools/dotc/cc/SepCheck.scala | 2 +- .../captures/sep-pairs-unboxed.check | 86 +++++++++++++++++++ .../captures/sep-pairs-unboxed.scala | 60 +++++++++++++ .../neg-custom-args/captures/sep-pairs.check | 2 +- 6 files changed, 179 insertions(+), 5 deletions(-) create mode 100644 tests/neg-custom-args/captures/sep-pairs-unboxed.check create mode 100644 tests/neg-custom-args/captures/sep-pairs-unboxed.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 93f0ec38e411..15cb64b4100d 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -691,6 +691,8 @@ object Capabilities: try (this eq y) || maxSubsumes(y, canAddHidden = !vs.isOpen) + // if vs is open, we should add new elements to the set containing `this` + // instead of adding them to the hidden set of of `this`. || y.match case y: TermRef => y.prefix.match @@ -773,6 +775,7 @@ object Capabilities: false vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y))) + || x.coversFresh(y) || x.acceptsLevelOf(y) && classifierOK && canAddHidden @@ -839,15 +842,39 @@ object Capabilities: case _ => false || x.match - case x: FreshCap if !seen.contains(x) => - seen.add(x) - x.hiddenSet.exists(recur(_, y)) + case x: FreshCap => + if x.coversFresh(y) then true + else if !seen.contains(x) then + seen.add(x) + x.hiddenSet.exists(recur(_, y)) + else false case Restricted(x1, _) => recur(x1, y) case _ => false recur(this, y) end covers + /** `x eq y` or `x` is a fresh cap, `y` is a fresh cap with prefix + * `p`, and there is a prefix of `p` that contains `x` in its + * capture set. + */ + final def coversFresh(y: Capability)(using Context): Boolean = + (this eq y) || this.match + case x: FreshCap => y match + case y: FreshCap => + x.origin match + case Origin.InDecl(sym) => + def occursInPrefix(pre: Type): Boolean = pre match + case pre @ TermRef(pre1, _) => + pre.symbol == sym + && pre.info.captureSet.elems.contains(x) + || occursInPrefix(pre1) + case _ => false + occursInPrefix(y.prefix) + case _ => false + case _ => false + case _ => false + def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[Capability] = CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 1055c668232a..a91989ac03dd 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -1236,6 +1236,7 @@ object CaptureSet: /** Add element to hidden set. */ def add(elem: Capability)(using ctx: Context, vs: VarState): Unit = + assert(elem ne owningCap) includeElem(elem) /** Apply function `f` to `elems` while setting `elems` to empty for the diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 46812ecc0d91..abd5981cd208 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -221,7 +221,7 @@ object SepCheck: refs1.foreach: ref => if !ref.isReadOnly then val coreRef = ref.stripRestricted - if refs2.exists(_.stripRestricted.stripReadOnly eq coreRef) then + if refs2.exists(_.stripRestricted.stripReadOnly.coversFresh(coreRef)) then acc += coreRef acc assert(refs.forall(_.isTerminalCapability)) diff --git a/tests/neg-custom-args/captures/sep-pairs-unboxed.check b/tests/neg-custom-args/captures/sep-pairs-unboxed.check new file mode 100644 index 000000000000..6ad2cf889fe6 --- /dev/null +++ b/tests/neg-custom-args/captures/sep-pairs-unboxed.check @@ -0,0 +1,86 @@ +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:11:27 ------------------------------------------------- +11 |def mkPair(x: Ref^) = Pair(x, x) // error: separation failure + | ^ + |Separation failure: argument of type (x : Ref^) + |to constructor Pair: (fst: Ref^, snd: Ref^): Pair + |corresponds to capture-polymorphic formal parameter fst of type Ref^² + |and hides capabilities {x}. + |Some of these overlap with the captures of the second argument with type (x : Ref^). + | + | Hidden set of current argument : {x} + | Hidden footprint of current argument : {x} + | Capture set of second argument : {x} + | Footprint set of second argument : {x} + | The two sets overlap at : {x} + | + |where: ^ refers to a fresh root capability classified as Mutable in the type of parameter x + | ^² refers to a fresh root capability classified as Mutable created in method mkPair when checking argument to parameter fst of constructor Pair +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:35:25 ------------------------------------------------- +35 | val twoCopy = Pair(two.fst, two.fst) // error + | ^^^^^^^ + |Separation failure: argument of type (two.fst : Ref^) + |to constructor Pair: (fst: Ref^, snd: Ref^): Pair + |corresponds to capture-polymorphic formal parameter fst of type Ref^² + |and hides capabilities {two.fst}. + |Some of these overlap with the captures of the second argument with type (two.fst : Ref^). + | + | Hidden set of current argument : {two.fst} + | Hidden footprint of current argument : {two.fst} + | Capture set of second argument : {two.fst} + | Footprint set of second argument : {two.fst} + | The two sets overlap at : {two.fst} + | + |where: ^ refers to a fresh root capability classified as Mutable in the type of value fst + | ^² refers to a fresh root capability classified as Mutable created in value twoCopy when checking argument to parameter fst of constructor Pair +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:41:29 ------------------------------------------------- +41 | val twisted = PairPair(two.fst, two) // error + | ^^^^^^^ + |Separation failure: argument of type (two.fst : Ref^) + |to constructor PairPair: (fst: Ref^, snd: Pair^): PairPair + |corresponds to capture-polymorphic formal parameter fst of type Ref^² + |and hides capabilities {two.fst}. + |Some of these overlap with the captures of the second argument with type (two : Pair{val fst: Ref^; val snd: Ref^}^). + | + | Hidden set of current argument : {two.fst} + | Hidden footprint of current argument : {two.fst} + | Capture set of second argument : {two*} + | Footprint set of second argument : {two*} + | The two sets overlap at : {two.cap of class Pair} + | + |where: ^ refers to a fresh root capability classified as Mutable in the type of value fst + | ^² refers to a fresh root capability classified as Mutable created in value twisted when checking argument to parameter fst of constructor PairPair +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:47:24 ------------------------------------------------- +47 | val twisted = swapped(two, two.snd) // error + | ^^^ + |Separation failure: argument of type (two : Pair{val fst: Ref^; val snd: Ref^²}^³) + |to method swapped: (@consume x: Pair^, @consume y: Ref^): PairPair^ + |corresponds to capture-polymorphic formal parameter x of type Pair^⁴ + |and hides capabilities {two}. + |Some of these overlap with the captures of the second argument with type (two.snd : Ref^). + | + | Hidden set of current argument : {two} + | Hidden footprint of current argument : {two} + | Capture set of second argument : {two.snd} + | Footprint set of second argument : {two.snd} + | The two sets overlap at : {two.snd} + | + |where: ^ refers to a fresh root capability classified as Mutable in the type of value fst + | ^² refers to a fresh root capability classified as Mutable in the type of value snd + | ^³ refers to a fresh root capability in the type of value two + | ^⁴ refers to a fresh root capability created in value twisted when checking argument to parameter x of method swapped +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:22 ------------------------------------------------- +58 | val twoOther = Pair(two.fst, two.snd) // error // error + | ^^^ + | Separation failure: Illegal access to {two.fst} which is hidden by the previous definition + | of value twoCopy with type Pair^. + | This type hides capabilities {two.fst, two.snd} + | + | where: ^ refers to a fresh root capability in the type of value twoCopy +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:31 ------------------------------------------------- +58 | val twoOther = Pair(two.fst, two.snd) // error // error + | ^^^ + | Separation failure: Illegal access to {two.snd} which is hidden by the previous definition + | of value twoCopy with type Pair^. + | This type hides capabilities {two.fst, two.snd} + | + | where: ^ refers to a fresh root capability in the type of value twoCopy diff --git a/tests/neg-custom-args/captures/sep-pairs-unboxed.scala b/tests/neg-custom-args/captures/sep-pairs-unboxed.scala new file mode 100644 index 000000000000..22b8bf9e1d19 --- /dev/null +++ b/tests/neg-custom-args/captures/sep-pairs-unboxed.scala @@ -0,0 +1,60 @@ +import caps.Mutable +import caps.cap + +class Ref extends Mutable: + var x = 0 + def get: Int = x + update def put(y: Int): Unit = x = y + +class Pair(val fst: Ref^, val snd: Ref^) + +def mkPair(x: Ref^) = Pair(x, x) // error: separation failure + +def bad: Pair^ = + val r0 = Ref() + val r1 = mkPair(r0) + r1 + +def twoRefs(): Pair^ = + val r1 = Ref() + val r2 = Ref() + Pair(r1, r2) + +def good1(): Unit = + val two = twoRefs() + val fst = two.fst + val snd = two.snd + val twoCopy = Pair(fst, snd) // ok + +def good2(): Unit = + val two = twoRefs() + val twoCopy = Pair(two.fst, two.snd) // ok + +def bad2(): Unit = + val two = twoRefs() + val twoCopy = Pair(two.fst, two.fst) // error + +class PairPair(val fst: Ref^, val snd: Pair^) + +def bad3(): Unit = + val two = twoRefs() + val twisted = PairPair(two.fst, two) // error + +def swapped(consume x: Pair^, consume y: Ref^): PairPair^ = PairPair(y, x) + +def bad4(): Unit = + val two = twoRefs() + val twisted = swapped(two, two.snd) // error + +def good3(): Unit = + val two = twoRefs() + val twoCopy = Pair(two.fst, two.snd) + val _: Pair^{two.fst, two.snd} = twoCopy + val twoOther = Pair(two.fst, two.snd) + +def bad5(): Unit = + val two = twoRefs() + val twoCopy: Pair^ = Pair(two.fst, two.snd) + val twoOther = Pair(two.fst, two.snd) // error // error + + diff --git a/tests/neg-custom-args/captures/sep-pairs.check b/tests/neg-custom-args/captures/sep-pairs.check index 69909cf4f648..d51870f3eedf 100644 --- a/tests/neg-custom-args/captures/sep-pairs.check +++ b/tests/neg-custom-args/captures/sep-pairs.check @@ -26,7 +26,7 @@ | Separation failure in value sameToPair's type Pair[Ref^, Ref^²]. | One part, Ref^, hides capabilities {fstSame}. | Another part, Ref^², captures capabilities {sndSame, same.snd*}. - | The two sets overlap at cap of value same. + | The two sets overlap at {cap of value same}. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value sameToPair | ^² refers to a fresh root capability classified as Mutable in the type of value sameToPair From 8aeec6ab1488a4b17d09ac5b435df3d1d9cd4119 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 7 Oct 2025 16:22:59 +0200 Subject: [PATCH 09/12] Use the whole selection tree for markFree Needed for use checking, since if we just take the leftmost prefix we sometimes end up with a `this`. --- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 3 +- .../dotty/tools/dotc/cc/CheckCaptures.scala | 38 +++++++++++++++---- .../src/dotty/tools/dotc/cc/SepCheck.scala | 17 +++++++-- .../captures/fresh-counter.check | 16 ++++++++ .../captures/fresh-counter.scala | 23 +++++++++++ .../captures/sep-pairs-unboxed.check | 8 ++-- 6 files changed, 88 insertions(+), 17 deletions(-) create mode 100644 tests/neg-custom-args/captures/fresh-counter.check create mode 100644 tests/neg-custom-args/captures/fresh-counter.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index a91989ac03dd..313db27c3e28 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -966,8 +966,7 @@ object CaptureSet: case elem: FreshCap if !nestedOK && !elems.contains(elem) - && !owner.isAnonymousFunction - && ccConfig.newScheme => + && !owner.isAnonymousFunction => def fail = i"attempting to add $elem to $this" def hideIn(fc: FreshCap): Unit = assert(elem.tryClassifyAs(fc.hiddenSet.classifier), fail) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index a284bce7ab94..9fe647d4ed35 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -102,7 +102,7 @@ object CheckCaptures: end SubstParamsMap /** A prototype that indicates selection with an immutable value */ - class PathSelectionProto(val sym: Symbol, val pt: Type)(using Context) extends WildcardSelectionProto + class PathSelectionProto(val select: Select, val pt: Type)(using Context) extends WildcardSelectionProto /** Check that a @retains annotation only mentions references that can be tracked. * This check is performed at Typer. @@ -653,11 +653,15 @@ class CheckCaptures extends Recheck, SymTransformer: // If ident refers to a parameterless method, charge its cv to the environment includeCallCaptures(sym, sym.info, tree) else if !sym.isStatic then - markFree(sym, pathRef(sym.termRef, pt), tree) + if ccConfig.newScheme && sym.exists + then markPathFree(sym.termRef, pt, tree) + else markFree(sym, pathRef(sym.termRef, pt), tree) mapResultRoots(super.recheckIdent(tree, pt), tree.symbol) override def recheckThis(tree: This, pt: Type)(using Context): Type = - markFree(pathRef(tree.tpe.asInstanceOf[ThisType], pt), tree) + if ccConfig.newScheme + then markPathFree(tree.tpe.asInstanceOf[ThisType], pt, tree) + else markFree(pathRef(tree.tpe.asInstanceOf[ThisType], pt), tree) super.recheckThis(tree, pt) /** Add all selections and also any `.rd modifier implied by the expected @@ -668,18 +672,38 @@ class CheckCaptures extends Recheck, SymTransformer: private def pathRef(base: TermRef | ThisType, pt: Type)(using Context): Capability = def addSelects(ref: TermRef | ThisType, pt: Type): Capability = pt match case pt: PathSelectionProto if ref.isTracked => - if pt.sym.isReadOnlyMethod then + if pt.select.symbol.isReadOnlyMethod then ref.readOnly else // if `ref` is not tracked then the selection could not give anything new // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters. - addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt) + addSelects(ref.select(pt.select.symbol).asInstanceOf[TermRef], pt.pt) case _ => ref val ref: Capability = addSelects(base, pt) if ref.derivesFromMutable && pt.isValueType && !pt.isMutableType then ref.readOnly else ref + /** Add all selections and also any `.rd modifier implied by the expected + * type `pt` to `base`. Example: + * If we have `x` and the expected type says we select that with `.a.b` + * where `b` is a read-only method, we charge `x.a.b.rd` instead of `x`. + */ + private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit = + pt match + case pt: PathSelectionProto if ref.isTracked => + // if `ref` is not tracked then the selection could not give anything new + // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters. + if pt.select.symbol.isReadOnlyMethod then + markFree(ref.readOnly, tree) + else + markPathFree(ref.select(pt.select.symbol).asInstanceOf[TermRef], pt.pt, pt.select) + case _ => + if ref.derivesFromMutable && pt.isValueType && !pt.isMutableType then + markFree(ref.readOnly, tree) + else + markFree(ref, tree) + /** The expected type for the qualifier of a selection. If the selection * could be part of a capability path or is a a read-only method, we return * a PathSelectionProto. @@ -688,7 +712,7 @@ class CheckCaptures extends Recheck, SymTransformer: val sym = tree.symbol if !sym.isOneOf(UnstableValueFlags) && !sym.isStatic || sym.isReadOnlyMethod - then PathSelectionProto(sym, pt) + then PathSelectionProto(tree, pt) else super.selectionProto(tree, pt) /** A specialized implementation of the selection rule. @@ -1820,7 +1844,7 @@ class CheckCaptures extends Recheck, SymTransformer: private def noWiden(actual: Type, expected: Type)(using Context): Boolean = actual.isSingleton && expected.match - case expected: PathSelectionProto => !expected.sym.isOneOf(UnstableValueFlags) + case expected: PathSelectionProto => !expected.select.symbol.isOneOf(UnstableValueFlags) case _ => expected.stripCapturing.isSingleton || expected == LhsProto /** Adapt `actual` type to `expected` type. This involves: diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index abd5981cd208..56e4c399982f 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -431,6 +431,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def sepUseError(tree: Tree, clashingDef: ValOrDefDef | Null, used: Refs, hidden: Refs)(using Context): Unit = if clashingDef != null then def resultStr = if clashingDef.isInstanceOf[DefDef] then " result" else "" + //println(i"sep use error: previous ${clashingDef.tpt.nuType}, ref = $used") report.error( em"""Separation failure: Illegal access to ${overlapStr(hidden, used)} which is hidden by the previous definition |of ${clashingDef.symbol} with$resultStr type ${clashingDef.tpt.nuType}. @@ -568,11 +569,17 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val usedPeaks = used.allPeaks val overlap = defsShadow.allPeaks.sharedPeaks(usedPeaks) if !defsShadow.allPeaks.sharedPeaks(usedPeaks).isEmpty then - val sym = tree.symbol - + // Drop all Selects unless they select from a `this` + def pathRoot(tree: Tree): Tree = tree match + case Select(This(_), _) => tree + case Select(prefix, _) => pathRoot(prefix) + case _ => tree + + val rootSym = pathRoot(tree).symbol + def findClashing(prevDefs: List[DefInfo]): Option[DefInfo] = prevDefs match case prevDef :: prevDefs1 => - if prevDef.symbol == sym then Some(prevDef) + if prevDef.symbol == rootSym then Some(prevDef) else if !prevDef.hiddenPeaks.sharedPeaks(usedPeaks).isEmpty then Some(prevDef) else findClashing(prevDefs1) case Nil => @@ -580,10 +587,12 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: findClashing(previousDefs) match case Some(clashing) => - if clashing.symbol != sym then + //println(i"check use $tree, $used, $rootSym, ${clashing.symbol}") + if clashing.symbol != rootSym then sepUseError(tree, clashing.tree, used, clashing.hidden) case None => sepUseError(tree, null, used, defsShadow) + end if for ref <- used do val pos = consumed.clashing(ref) diff --git a/tests/neg-custom-args/captures/fresh-counter.check b/tests/neg-custom-args/captures/fresh-counter.check new file mode 100644 index 000000000000..4818515a41d6 --- /dev/null +++ b/tests/neg-custom-args/captures/fresh-counter.check @@ -0,0 +1,16 @@ +-- Error: tests/neg-custom-args/captures/fresh-counter.scala:22:6 ------------------------------------------------------ +22 | par(i, d) // error: separation failure + | ^ + |Separation failure: argument of type (i : () ->{c.incr} Unit) + |to method par: (p1: () => Unit, p2: () => Unit): Unit + |corresponds to capture-polymorphic formal parameter p1 of type () => Unit + |and hides capabilities {i}. + |Some of these overlap with the captures of the second argument with type (d : () ->{c.decr} Unit). + | + | Hidden set of current argument : {i} + | Hidden footprint of current argument : {i, c.incr, c.count} + | Capture set of second argument : {d} + | Footprint set of second argument : {d, c.decr, c.count} + | The two sets overlap at : {c.count} + | + |where: => refers to a fresh root capability created in method test when checking argument to parameter p1 of method par diff --git a/tests/neg-custom-args/captures/fresh-counter.scala b/tests/neg-custom-args/captures/fresh-counter.scala new file mode 100644 index 000000000000..94da57727633 --- /dev/null +++ b/tests/neg-custom-args/captures/fresh-counter.scala @@ -0,0 +1,23 @@ +import caps.Mutable +import caps.cap + +class Ref extends Mutable: + var x = 0 + def get: Int = x + update def put(y: Int): Unit = x = y + +class Counter: + private val count: Ref^ = Ref() + val incr = () => + count.put(count.get + 1) + val decr = () => + count.put(count.get - 1) + +def par(p1: () => Unit, p2: () => Unit) = () + +def test() = + val c = Counter() + val i = c.incr + val d = c.decr + par(i, d) // error: separation failure + diff --git a/tests/neg-custom-args/captures/sep-pairs-unboxed.check b/tests/neg-custom-args/captures/sep-pairs-unboxed.check index 6ad2cf889fe6..c1c4a95bb4fd 100644 --- a/tests/neg-custom-args/captures/sep-pairs-unboxed.check +++ b/tests/neg-custom-args/captures/sep-pairs-unboxed.check @@ -68,17 +68,17 @@ | ^² refers to a fresh root capability classified as Mutable in the type of value snd | ^³ refers to a fresh root capability in the type of value two | ^⁴ refers to a fresh root capability created in value twisted when checking argument to parameter x of method swapped --- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:22 ------------------------------------------------- +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:26 ------------------------------------------------- 58 | val twoOther = Pair(two.fst, two.snd) // error // error - | ^^^ + | ^^^^^^^ | Separation failure: Illegal access to {two.fst} which is hidden by the previous definition | of value twoCopy with type Pair^. | This type hides capabilities {two.fst, two.snd} | | where: ^ refers to a fresh root capability in the type of value twoCopy --- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:31 ------------------------------------------------- +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:35 ------------------------------------------------- 58 | val twoOther = Pair(two.fst, two.snd) // error // error - | ^^^ + | ^^^^^^^ | Separation failure: Illegal access to {two.snd} which is hidden by the previous definition | of value twoCopy with type Pair^. | This type hides capabilities {two.fst, two.snd} From c8f51e74cab21bb7931a3c4e31e446412ce369dd Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 7 Oct 2025 16:27:46 +0200 Subject: [PATCH 10/12] Drop switch on newScheme, drop code that's no longer used. --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 36 ++++--------------- 1 file changed, 7 insertions(+), 29 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 9fe647d4ed35..f3a586f2ddca 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -652,42 +652,20 @@ class CheckCaptures extends Recheck, SymTransformer: if sym.is(Method) then // If ident refers to a parameterless method, charge its cv to the environment includeCallCaptures(sym, sym.info, tree) - else if !sym.isStatic then - if ccConfig.newScheme && sym.exists - then markPathFree(sym.termRef, pt, tree) - else markFree(sym, pathRef(sym.termRef, pt), tree) + else if sym.exists && !sym.isStatic then + markPathFree(sym.termRef, pt, tree) mapResultRoots(super.recheckIdent(tree, pt), tree.symbol) override def recheckThis(tree: This, pt: Type)(using Context): Type = - if ccConfig.newScheme - then markPathFree(tree.tpe.asInstanceOf[ThisType], pt, tree) - else markFree(pathRef(tree.tpe.asInstanceOf[ThisType], pt), tree) + markPathFree(tree.tpe.asInstanceOf[ThisType], pt, tree) super.recheckThis(tree, pt) /** Add all selections and also any `.rd modifier implied by the expected - * type `pt` to `base`. Example: + * type `pt` to `ref`. Expand the marked tree accordingly to take account of + * the added path. Example: * If we have `x` and the expected type says we select that with `.a.b` - * where `b` is a read-only method, we charge `x.a.b.rd` instead of `x`. - */ - private def pathRef(base: TermRef | ThisType, pt: Type)(using Context): Capability = - def addSelects(ref: TermRef | ThisType, pt: Type): Capability = pt match - case pt: PathSelectionProto if ref.isTracked => - if pt.select.symbol.isReadOnlyMethod then - ref.readOnly - else - // if `ref` is not tracked then the selection could not give anything new - // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters. - addSelects(ref.select(pt.select.symbol).asInstanceOf[TermRef], pt.pt) - case _ => ref - val ref: Capability = addSelects(base, pt) - if ref.derivesFromMutable && pt.isValueType && !pt.isMutableType - then ref.readOnly - else ref - - /** Add all selections and also any `.rd modifier implied by the expected - * type `pt` to `base`. Example: - * If we have `x` and the expected type says we select that with `.a.b` - * where `b` is a read-only method, we charge `x.a.b.rd` instead of `x`. + * where `b` is a read-only method, we charge `x.a.b.rd` for tree `x.a.b` + * instead of just charging `x`. */ private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit = pt match From a0f16137f3c9c763642d953d7e5f0324d8abbfaf Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 7 Oct 2025 16:54:07 +0200 Subject: [PATCH 11/12] New test cases --- .../captures/fresh-counter.check | 24 ++++++-- .../captures/fresh-counter.scala | 14 ++++- .../captures/sep-curried-par.check | 59 +++++++++++++++++++ .../captures/sep-curried-par.scala | 29 +++++++++ 4 files changed, 121 insertions(+), 5 deletions(-) create mode 100644 tests/neg-custom-args/captures/sep-curried-par.check create mode 100644 tests/neg-custom-args/captures/sep-curried-par.scala diff --git a/tests/neg-custom-args/captures/fresh-counter.check b/tests/neg-custom-args/captures/fresh-counter.check index 4818515a41d6..84d3137b63bb 100644 --- a/tests/neg-custom-args/captures/fresh-counter.check +++ b/tests/neg-custom-args/captures/fresh-counter.check @@ -1,5 +1,5 @@ --- Error: tests/neg-custom-args/captures/fresh-counter.scala:22:6 ------------------------------------------------------ -22 | par(i, d) // error: separation failure +-- Error: tests/neg-custom-args/captures/fresh-counter.scala:23:6 ------------------------------------------------------ +23 | par(i, d) // error: separation failure | ^ |Separation failure: argument of type (i : () ->{c.incr} Unit) |to method par: (p1: () => Unit, p2: () => Unit): Unit @@ -10,7 +10,23 @@ | Hidden set of current argument : {i} | Hidden footprint of current argument : {i, c.incr, c.count} | Capture set of second argument : {d} - | Footprint set of second argument : {d, c.decr, c.count} - | The two sets overlap at : {c.count} + | Footprint set of second argument : {d, c.decr, c} + | The two sets overlap at : {c.incr, c.count} | |where: => refers to a fresh root capability created in method test when checking argument to parameter p1 of method par +-- Error: tests/neg-custom-args/captures/fresh-counter.scala:33:4 ------------------------------------------------------ +33 | () => count.put(count.get + 1), // error: separation failure + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + |Separation failure: argument of type () ->{count} Unit + |to constructor Pair: (a: () => Unit, b: () => Unit): Pair + |corresponds to capture-polymorphic formal parameter a of type () => Unit + |and hides capabilities {count}. + |Some of these overlap with the captures of the second argument with type () ->{count} Unit. + | + | Hidden set of current argument : {count} + | Hidden footprint of current argument : {count} + | Capture set of second argument : {count} + | Footprint set of second argument : {count} + | The two sets overlap at : {count} + | + |where: => refers to a fresh root capability created in method mkCounter when checking argument to parameter a of constructor Pair diff --git a/tests/neg-custom-args/captures/fresh-counter.scala b/tests/neg-custom-args/captures/fresh-counter.scala index 94da57727633..233b0e3c91e2 100644 --- a/tests/neg-custom-args/captures/fresh-counter.scala +++ b/tests/neg-custom-args/captures/fresh-counter.scala @@ -10,14 +10,26 @@ class Counter: private val count: Ref^ = Ref() val incr = () => count.put(count.get + 1) - val decr = () => + val decr: () ->{this} Unit = () => count.put(count.get - 1) def par(p1: () => Unit, p2: () => Unit) = () +def seq(p1: () => Unit, p2: () ->{cap, p1} Unit) = () def test() = val c = Counter() val i = c.incr val d = c.decr par(i, d) // error: separation failure + seq(i, d) + +type Proc = () => Unit + +class Pair(val a: Proc, val b: Proc) + +def mkCounter(): Pair^ = + val count = Ref() + Pair( + () => count.put(count.get + 1), // error: separation failure + () => count.put(count.get - 1)) diff --git a/tests/neg-custom-args/captures/sep-curried-par.check b/tests/neg-custom-args/captures/sep-curried-par.check new file mode 100644 index 000000000000..04c052f9c7cc --- /dev/null +++ b/tests/neg-custom-args/captures/sep-curried-par.check @@ -0,0 +1,59 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/sep-curried-par.scala:23:32 ------------------------------ +23 | val bar = (p1: () => Unit) => (p2: () ->{p1, cap} Unit) => par(p1, p2) // error, but error message could be better + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | Found: (p2: () ->{p1, cap} Unit) ->{p1} Unit + | Required: (() ->'s1 Unit) ->'s2 Unit + | + | Note that capability p1, defined in method $anonfun + | cannot be included in outer capture set 's2. + | + | where: cap is the universal root capability + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:6:48 ---------------------------------------------------- +6 |def parCurriedBad(p1: () => Unit): (() => Unit) => Unit = // error: consume failure + | ^^^^^^^^^^^^^^^^^^^^ + | Separation failure: method parCurriedBad's result type (() => Unit) => Unit hides parameter p1. + | The parameter needs to be annotated with consume to allow this. +-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:15:6 ---------------------------------------------------- +15 | par(p, p) // error: separation + | ^ + |Separation failure: argument of type (p : () => Unit) + |to method par: (p1: () => Unit, p2: () => Unit): Unit + |corresponds to capture-polymorphic formal parameter p1 of type () =>² Unit + |and hides capabilities {p}. + |Some of these overlap with the captures of the second argument with type (p : () => Unit). + | + | Hidden set of current argument : {p} + | Hidden footprint of current argument : {p} + | Capture set of second argument : {p} + | Footprint set of second argument : {p} + | The two sets overlap at : {p} + | + |where: => refers to a fresh root capability in the type of value p + | =>² refers to a fresh root capability created in method test when checking argument to parameter p1 of method par +-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:18:16 --------------------------------------------------- +18 | parCurried(p)(p) // error: consume failure + | ^ + | Separation failure: Illegal access to (p : () => Unit), 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: => refers to a fresh root capability in the type of value p +-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:21:9 ---------------------------------------------------- +21 | foo(c)(c) // error: separation + | ^ + |Separation failure: argument of type (c : () => Unit) + |to a function of type (() => Unit) ->{c} Unit + |corresponds to capture-polymorphic formal parameter v1 of type () =>² Unit + |and hides capabilities {c}. + |Some of these overlap with the captures of the function prefix. + | + | Hidden set of current argument : {c} + | Hidden footprint of current argument : {c} + | Capture set of function prefix : {c} + | Footprint set of function prefix : {c} + | The two sets overlap at : {c} + | + |where: => refers to a fresh root capability in the type of parameter c + | =>² refers to a fresh root capability created in method test when checking argument to parameter v1 of method apply diff --git a/tests/neg-custom-args/captures/sep-curried-par.scala b/tests/neg-custom-args/captures/sep-curried-par.scala new file mode 100644 index 000000000000..a1f4e54ac1a0 --- /dev/null +++ b/tests/neg-custom-args/captures/sep-curried-par.scala @@ -0,0 +1,29 @@ +import caps.cap + +def par(p1: () => Unit, p2: () => Unit) = () +def seq(p1: () => Unit, p2: () ->{cap, p1} Unit) = () + +def parCurriedBad(p1: () => Unit): (() => Unit) => Unit = // error: consume failure + (p2: () => Unit) => par(p1, p2) +def parCurried(consume p1: () => Unit): (() => Unit) => Unit = + (p2: () => Unit) => par(p1, p2) + +type Proc = () => Unit + +def test(c: () => Unit) = + val p: Proc = ??? + par(p, p) // error: separation + seq(p, p) + parCurriedBad(p)(p) // ok, but parCurriedBad ill-typed + parCurried(p)(p) // error: consume failure + + val foo = (p1: () => Unit) => (p2: () ->{c, cap} Unit) => par(p1, p2) + foo(c)(c) // error: separation + + val bar = (p1: () => Unit) => (p2: () ->{p1, cap} Unit) => par(p1, p2) // error, but error message could be better + bar(c)(c) + + + + + From 6689785a62be62d03e24c94b700fe7b2c4f802d6 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 8 Oct 2025 11:21:07 +0200 Subject: [PATCH 12/12] Refine checking if fields with inferred types Private fields in publicly accessible classes that contribute fresh caps to their class still need an explicitly declared type, so that separate compilation can work. --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 58 +++++++++++++------ .../tools/dotc/core/SymDenotations.scala | 8 ++- .../captures/check-inferred.check | 35 +++++++++++ .../captures/check-inferred.scala | 34 +++++++++++ 4 files changed, 113 insertions(+), 22 deletions(-) create mode 100644 tests/neg-custom-args/captures/check-inferred.check create mode 100644 tests/neg-custom-args/captures/check-inferred.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index f3a586f2ddca..5f52fa5b10cc 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -194,6 +194,11 @@ object CheckCaptures: check.traverse(tp) end disallowBadRootsIn + private def contributesFreshToClass(sym: Symbol)(using Context): Boolean = + sym.isField + && !sym.isOneOf(DeferredOrTermParamOrAccessor) + && !sym.hasAnnotation(defn.UntrackedCapturesAnnot) + private def ownerStr(owner: Symbol)(using Context): String = if owner.isAnonymousFunction then "enclosing function" else owner.show @@ -918,8 +923,7 @@ class CheckCaptures extends Recheck, SymTransformer: val fieldClassifiers = for sym <- cls.info.decls.toList - if sym.isField && !sym.isOneOf(DeferredOrTermParamOrAccessor) - && !sym.hasAnnotation(defn.UntrackedCapturesAnnot) + if contributesFreshToClass(sym) case fresh: FreshCap <- sym.info.spanCaptureSet.elems .filter(_.isTerminalCapability) .map(_.stripReadOnly) @@ -1160,15 +1164,15 @@ class CheckCaptures extends Recheck, SymTransformer: def checkInferredResult(tp: Type, tree: ValOrDefDef)(using Context): Type = val sym = tree.symbol - def canUseInferred = // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly - sym.isLocalToCompilationUnit // Symbols that can't be seen outside the compilation unit can always have inferred types - || ctx.owner.enclosingPackageClass.isEmptyPackage - // We make an exception for symbols in the empty package. - // these could theoretically be accessed from other files in the empty package, but - // usually it would be too annoying to require explicit types. - || sym.name.is(DefaultGetterName) // Default getters are exempted since otherwise it would be - // too annoying. This is a hole since a defualt getter's result type - // might leak into a type variable. + def isExemptFromChecks = + ctx.owner.enclosingPackageClass.isEmptyPackage + // We make an exception for symbols in the empty package. + // these could theoretically be accessed from other files in the empty package, but + // usually it would be too annoying to require explicit types. + || sym.name.is(DefaultGetterName) + // Default getters are exempted since otherwise it would be + // too annoying. This is a hole since a defualt getter's result type + // might leak into a type variable. def fail(tree: Tree, expected: Type, addenda: Addenda): Unit = def maybeResult = if sym.is(Method) then " result" else "" @@ -1191,14 +1195,30 @@ class CheckCaptures extends Recheck, SymTransformer: |must conform to this type.""" tree.tpt match - case tpt: InferredTypeTree if !canUseInferred => - val expected = tpt.tpe.dropAllRetains - todoAtPostCheck += { () => - withCapAsRoot: - testAdapted(tp, expected, tree.rhs, addenda(expected))(fail) - // The check that inferred <: expected is done after recheck so that it - // does not interfere with normal rechecking by constraining capture set variables. - } + case tpt: InferredTypeTree if !isExemptFromChecks => + if !sym.isLocalToCompilationUnit + // Symbols that can't be seen outside the compilation unit can have inferred types + // except for the else clause below. + then + val expected = tpt.tpe.dropAllRetains + todoAtPostCheck += { () => + withCapAsRoot: + testAdapted(tp, expected, tree.rhs, addenda(expected))(fail) + // The check that inferred <: expected is done after recheck so that it + // does not interfere with normal rechecking by constraining capture set variables. + } + else if sym.is(Private) + && !sym.isLocalToCompilationUnitIgnoringPrivate + && tree.tpt.nuType.spanCaptureSet.containsTerminalCapability + && contributesFreshToClass(sym) + // Private symbols capturing a root capability need explicit types + // so that we can compute field constributions to class instance + // capture sets across compilation units. + then + report.error( + em"""$sym needs an explicit type because it captures a root capability in its type ${tree.tpt.nuType}. + |Fields of publicily accessible classes that capture a root capability need to be given an explicit type.""", + tpt.srcPos) case _ => tp end checkInferredResult diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala index 6dcf2a83ba5c..53a96931c83e 100644 --- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala +++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala @@ -1248,11 +1248,13 @@ object SymDenotations { || isClass && (!isOneOf(EffectivelyOpenFlags) || isLocalToCompilationUnit) - final def isLocalToCompilationUnit(using Context): Boolean = - is(Private) - || owner.ownersIterator.takeWhile(!_.isStaticOwner).exists(_.isTerm) + final def isLocalToCompilationUnitIgnoringPrivate(using Context): Boolean = + owner.ownersIterator.takeWhile(!_.isStaticOwner).exists(_.isTerm) || accessBoundary(defn.RootClass).isProperlyContainedIn(symbol.topLevelClass) + final def isLocalToCompilationUnit(using Context): Boolean = + is(Private) || isLocalToCompilationUnitIgnoringPrivate + final def isTransparentClass(using Context): Boolean = is(TransparentType) || defn.isAssumedTransparent(symbol) diff --git a/tests/neg-custom-args/captures/check-inferred.check b/tests/neg-custom-args/captures/check-inferred.check new file mode 100644 index 000000000000..7e3f9022f5a5 --- /dev/null +++ b/tests/neg-custom-args/captures/check-inferred.check @@ -0,0 +1,35 @@ +-- Error: tests/neg-custom-args/captures/check-inferred.scala:12:19 ---------------------------------------------------- +12 | private val count = Ref() // error + | ^ + | value count needs an explicit type because it captures a root capability in its type test.Ref^. + | Fields of publicily accessible classes that capture a root capability need to be given an explicit type. + | + | where: ^ refers to a fresh root capability classified as Mutable in the type of value count +-- Error: tests/neg-custom-args/captures/check-inferred.scala:18:13 ---------------------------------------------------- +18 | val incr = () => // error + | ^ + | value incr needs an explicit type because the inferred type does not conform to + | the type that is externally visible in other compilation units. + | + | Inferred type : () ->{Counter.this.count} Unit + | Externally visible type: () -> Unit +19 | count.put(count.get + 1) +-- Error: tests/neg-custom-args/captures/check-inferred.scala:20:13 ---------------------------------------------------- +20 | val decr = () => // error + | ^ + | value decr needs an explicit type because the inferred type does not conform to + | the type that is externally visible in other compilation units. + | + | Inferred type : () ->{Counter.this.count} Unit + | Externally visible type: () -> Unit +21 | count.put(count.get - 1) +-- Error: tests/neg-custom-args/captures/check-inferred.scala:24:14 ---------------------------------------------------- +24 | val count = Ref(): Object^ // error + | ^^^^^^^^^^^^^^ + | value count needs an explicit type because the inferred type does not conform to + | the type that is externally visible in other compilation units. + | + | Inferred type : Object^ + | Externally visible type: Object + | + | where: ^ refers to a fresh root capability created in value count diff --git a/tests/neg-custom-args/captures/check-inferred.scala b/tests/neg-custom-args/captures/check-inferred.scala new file mode 100644 index 000000000000..2462e4cb2e82 --- /dev/null +++ b/tests/neg-custom-args/captures/check-inferred.scala @@ -0,0 +1,34 @@ +package test +import caps.Mutable +import caps.cap +import caps.unsafe.untrackedCaptures + +class Ref extends Mutable: + var x = 0 + def get: Int = x + update def put(y: Int): Unit = x = y + +class Counter: + private val count = Ref() // error + private val altCount: Ref^ = Ref() // ok + + @untrackedCaptures + private val altAltCount = Ref() // ok + + val incr = () => // error + count.put(count.get + 1) + val decr = () => // error + count.put(count.get - 1) + +trait CounterAPI: + val count = Ref(): Object^ // error + private def count2 = Ref() // ok + +def test() = + class Counter: + private val count = Ref() // ok + val incr = () => + count.put(count.get + 1) + val decr = () => + count.put(count.get - 1) +