From 74b6bf610e32370b70ee9d5383e304961129990b Mon Sep 17 00:00:00 2001 From: noti0na1 Date: Wed, 18 Sep 2024 15:33:16 +0200 Subject: [PATCH 01/13] Add path support for cc --- compiler/src/dotty/tools/dotc/ast/untpd.scala | 4 +- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 3 +- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 84 +++++++++----- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 8 +- .../dotty/tools/dotc/cc/CheckCaptures.scala | 106 ++++++++++-------- .../dotty/tools/dotc/parsing/Parsers.scala | 28 ++--- .../captures/class-contra.check | 13 +-- .../captures/class-contra.scala | 3 +- .../captures/explain-under-approx.check | 14 +-- .../captures/filevar-multi-ios.scala | 41 +++++++ tests/neg-custom-args/captures/i15116.check | 16 ++- tests/neg-custom-args/captures/path-box.scala | 20 ++++ .../captures/path-connection.scala | 46 ++++++++ .../captures/path-illigal.scala | 7 ++ .../captures/path-simple.scala | 27 +++++ .../neg-custom-args/captures/singletons.scala | 8 +- .../captures/filevar-expanded.scala | 3 +- tests/pos-custom-args/captures/filevar.scala | 3 +- 18 files changed, 314 insertions(+), 120 deletions(-) create mode 100644 tests/neg-custom-args/captures/filevar-multi-ios.scala create mode 100644 tests/neg-custom-args/captures/path-box.scala create mode 100644 tests/neg-custom-args/captures/path-connection.scala create mode 100644 tests/neg-custom-args/captures/path-illigal.scala create mode 100644 tests/neg-custom-args/captures/path-simple.scala diff --git a/compiler/src/dotty/tools/dotc/ast/untpd.scala b/compiler/src/dotty/tools/dotc/ast/untpd.scala index 60309d4d83bd..b86734afcc0a 100644 --- a/compiler/src/dotty/tools/dotc/ast/untpd.scala +++ b/compiler/src/dotty/tools/dotc/ast/untpd.scala @@ -525,8 +525,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo { def makeRetaining(parent: Tree, refs: List[Tree], annotName: TypeName)(using Context): Annotated = Annotated(parent, New(scalaAnnotationDot(annotName), List(refs))) - def makeCapsOf(id: Ident)(using Context): Tree = - TypeApply(Select(scalaDot(nme.caps), nme.capsOf), id :: Nil) + def makeCapsOf(tp: Tree)(using Context): Tree = + TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil) def makeCapsBound()(using Context): Tree = makeRetaining( diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 29c6528e36de..79cc7d136e45 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -194,7 +194,8 @@ extension (tp: Type) true case tp: TermRef => ((tp.prefix eq NoPrefix) - || tp.symbol.is(ParamAccessor) && tp.prefix.isThisTypeOf(tp.symbol.owner) + || tp.symbol.isField && !tp.symbol.isStatic && ( + tp.prefix.isThisTypeOf(tp.symbol.owner) || tp.prefix.isTrackableRef) || tp.isRootCapability ) && !tp.symbol.isOneOf(UnstableValueFlags) case tp: TypeRef => diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index f00c6869cd80..05162907b608 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -61,18 +61,19 @@ trait CaptureRef extends TypeProxy, ValueType: case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists) case _ => false - /** Normalize reference so that it can be compared with `eq` for equality */ - final def normalizedRef(using Context): CaptureRef = this match - case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef => - tp.derivedAnnotatedType(parent.normalizedRef, annot) - case tp: TermRef if tp.isTrackableRef => - tp.symbol.termRef - case _ => this + // With the support of pathes, we don't need to normalize the `TermRef`s anymore. + // /** Normalize reference so that it can be compared with `eq` for equality */ + // final def normalizedRef(using Context): CaptureRef = this match + // case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef => + // tp.derivedAnnotatedType(parent.normalizedRef, annot) + // case tp: TermRef if tp.isTrackableRef => + // tp.symbol.termRef + // case _ => this /** The capture set consisting of exactly this reference */ final def singletonCaptureSet(using Context): CaptureSet.Const = if mySingletonCaptureSet == null then - mySingletonCaptureSet = CaptureSet(this.normalizedRef) + mySingletonCaptureSet = CaptureSet(this) mySingletonCaptureSet.uncheckedNN /** The capture set of the type underlying this reference */ @@ -99,25 +100,56 @@ trait CaptureRef extends TypeProxy, ValueType: * x: x1.type /\ x1 subsumes y ==> x subsumes y */ final def subsumes(y: CaptureRef)(using Context): Boolean = - (this eq y) - || this.isRootCapability - || y.match - case y: TermRef => - (y.prefix eq this) - || y.info.match - case y1: SingletonCaptureRef => this.subsumes(y1) - case _ => false - case MaybeCapability(y1) => this.stripMaybe.subsumes(y1) - case _ => false - || this.match - case ReachCapability(x1) => x1.subsumes(y.stripReach) - case x: TermRef => - x.info match - case x1: SingletonCaptureRef => x1.subsumes(y) + def compareCaptureRefs(x: Type, y: Type): Boolean = + (x eq y) + || y.match + case y: CaptureRef => x.match + case x: CaptureRef => x.subsumes(y) case _ => false - case x: TermParamRef => subsumesExistentially(x, y) - case x: TypeRef => assumedContainsOf(x).contains(y) - case _ => false + case _ => false + + def compareUndelying(x: Type): Boolean = x match + case x: SingletonCaptureRef => x.subsumes(y) + case x: AndType => compareUndelying(x.tp1) || compareUndelying(x.tp2) + case x: OrType => compareUndelying(x.tp1) && compareUndelying(x.tp2) + case _ => false + + if (this eq y) || this.isRootCapability then return true + + // similar to compareNamed in TypeComparer + y match + case y: TermRef => + this match + case x: TermRef => + val xSym = x.symbol + val ySym = y.symbol + + // check x.f and y.f + if (xSym ne NoSymbol) + && (xSym eq ySym) + && compareCaptureRefs(x.prefix, y.prefix) + || (x.name eq y.name) + && x.isPrefixDependentMemberRef + && compareCaptureRefs(x.prefix, y.prefix) + && x.signature == y.signature + && !(xSym.isClass && ySym.isClass) + then return true + case _ => + + // shorten + if compareCaptureRefs(this, y.prefix) then return true + // underlying + if compareCaptureRefs(this, y.info) then return true + case MaybeCapability(y1) => return this.stripMaybe.subsumes(y1) + case _ => + + return this.match + case ReachCapability(x1) => x1.subsumes(y.stripReach) + case x: TermRef => compareUndelying(x.info) + case CapturingType(x1, _) => compareUndelying(x1) + case x: TermParamRef => subsumesExistentially(x, y) + case x: TypeRef => assumedContainsOf(x).contains(y) + case _ => false def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] = 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 44d5e2cf4b88..81b4287961ba 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -374,7 +374,7 @@ object CaptureSet: def apply(elems: CaptureRef*)(using Context): CaptureSet.Const = if elems.isEmpty then empty - else Const(SimpleIdentitySet(elems.map(_.normalizedRef.ensuring(_.isTrackableRef))*)) + else Const(SimpleIdentitySet(elems.map(_.ensuring(_.isTrackableRef))*)) def apply(elems: Refs)(using Context): CaptureSet.Const = if elems.isEmpty then empty else Const(elems) @@ -508,7 +508,11 @@ object CaptureSet: !noUniversal else elem match case elem: TermRef if level.isDefined => - elem.symbol.ccLevel <= level + elem.prefix match + case prefix: CaptureRef => + levelOK(prefix) + case _ => + elem.symbol.ccLevel <= level case elem: ThisType if level.isDefined => elem.cls.ccLevel.nextInner <= level case ReachCapability(elem1) => diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index b05ab8542137..ec1e63137311 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -122,10 +122,6 @@ object CheckCaptures: * This check is performed at Typer. */ def checkWellformed(parent: Tree, ann: Tree)(using Context): Unit = - parent.tpe match - case _: SingletonType => - report.error(em"Singleton type $parent cannot have capture set", parent.srcPos) - case _ => def check(elem: Tree, pos: SrcPos): Unit = elem.tpe match case ref: CaptureRef => if !ref.isTrackableRef then @@ -373,45 +369,54 @@ class CheckCaptures extends Recheck, SymTransformer: * the environment's owner */ def markFree(cs: CaptureSet, pos: SrcPos)(using Context): Unit = + // A captured reference with the symbol `sym` is visible from the environment + // if `sym` is not defined inside the owner of the environment. + inline def isVisibleFromEnv(sym: Symbol, env: Env) = + if env.kind == EnvKind.NestedInOwner then + !sym.isProperlyContainedIn(env.owner) + else + !sym.isContainedIn(env.owner) + + def checkSubsetEnv(cs: CaptureSet, env: Env)(using Context): Unit = + // Only captured references that are visible from the environment + // should be included. + val included = cs.filter: c => + c.stripReach match + case ref: NamedType => + val refSym = ref.symbol + val refOwner = refSym.owner + val isVisible = isVisibleFromEnv(refOwner, env) + if isVisible && !ref.isRootCapability then + ref match + case ref: TermRef if ref.prefix `ne` NoPrefix => + // If c is a path of a class defined outside the environment, + // we check the capture set of its info. + checkSubsetEnv(ref.captureSetOfInfo, env) + case _ => + if !isVisible + && (c.isReach || ref.isType) + && (!ccConfig.useSealed || refSym.is(Param)) + && refOwner == env.owner + then + if refSym.hasAnnotation(defn.UnboxAnnot) then + capt.println(i"exempt: $ref in $refOwner") + else + // Reach capabilities that go out of scope have to be approximated + // by their underlying capture set, which cannot be universal. + // Reach capabilities of @unboxed parameters are exempted. + val cs = CaptureSet.ofInfo(c) + cs.disallowRootCapability: () => + report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos) + checkSubset(cs, env.captured, pos, provenance(env)) + isVisible + case ref: ThisType => isVisibleFromEnv(ref.cls, env) + case _ => false + checkSubset(included, env.captured, pos, provenance(env)) + capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}") + if !cs.isAlwaysEmpty then forallOuterEnvsUpTo(ctx.owner.topLevelClass): env => - // Whether a symbol is defined inside the owner of the environment? - inline def isContainedInEnv(sym: Symbol) = - if env.kind == EnvKind.NestedInOwner then - sym.isProperlyContainedIn(env.owner) - else - sym.isContainedIn(env.owner) - // A captured reference with the symbol `sym` is visible from the environment - // if `sym` is not defined inside the owner of the environment - inline def isVisibleFromEnv(sym: Symbol) = !isContainedInEnv(sym) - // Only captured references that are visible from the environment - // should be included. - val included = cs.filter: c => - c.stripReach match - case ref: NamedType => - val refSym = ref.symbol - val refOwner = refSym.owner - val isVisible = isVisibleFromEnv(refOwner) - if !isVisible - && (c.isReach || ref.isType) - && (!ccConfig.useSealed || refSym.is(Param)) - && refOwner == env.owner - then - if refSym.hasAnnotation(defn.UnboxAnnot) then - capt.println(i"exempt: $ref in $refOwner") - else - // Reach capabilities that go out of scope have to be approximated - // by their underlying capture set, which cannot be universal. - // Reach capabilities of @unboxed parameters are exempted. - val cs = CaptureSet.ofInfo(c) - cs.disallowRootCapability: () => - report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos) - checkSubset(cs, env.captured, pos, provenance(env)) - isVisible - case ref: ThisType => isVisibleFromEnv(ref.cls) - case _ => false - checkSubset(included, env.captured, pos, provenance(env)) - capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}") + checkSubsetEnv(cs, env) end markFree /** Include references captured by the called method in the current environment stack */ @@ -488,21 +493,28 @@ class CheckCaptures extends Recheck, SymTransformer: case _ => denot val selType = recheckSelection(tree, qualType, name, disambiguate) - val selCs = selType.widen.captureSet - if selCs.isAlwaysEmpty - || selType.widen.isBoxedCapturing + val selWiden = selType.widen + def isStableSel = selType match + case selType: NamedType => selType.symbol.isStableMember + case _ => false + + if pt == LhsProto || qualType.isBoxedCapturing - || pt == LhsProto + || selType.isTrackableRef + || selWiden.isBoxedCapturing + || selWiden.captureSet.isAlwaysEmpty then selType else val qualCs = qualType.captureSet - capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs in $tree") + val selCs = selType.captureSet + capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs ${selWiden.captureSet} in $tree") + if qualCs.mightSubcapture(selCs) && !selCs.mightSubcapture(qualCs) && !pt.stripCapturing.isInstanceOf[SingletonType] then - selType.widen.stripCapturing.capturing(qualCs) + selWiden.stripCapturing.capturing(qualCs) .showing(i"alternate type for select $tree: $selType --> $result, $qualCs / $selCs", capt) else selType diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala index 8a173faa3cec..96f09a0d6214 100644 --- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala +++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala @@ -1548,21 +1548,23 @@ object Parsers { case _ => None } - /** CaptureRef ::= ident [`*` | `^`] | `this` + /** CaptureRef ::= (ident | `this`) [`*` | `^`] */ def captureRef(): Tree = - if in.token == THIS then simpleRef() - else - val id = termIdent() - if isIdent(nme.raw.STAR) then - in.nextToken() - atSpan(startOffset(id)): - PostfixOp(id, Ident(nme.CC_REACH)) - else if isIdent(nme.UPARROW) then - in.nextToken() - atSpan(startOffset(id)): - makeCapsOf(cpy.Ident(id)(id.name.toTypeName)) - else id + val ref = singleton() + if isIdent(nme.raw.STAR) then + in.nextToken() + atSpan(startOffset(ref)): + PostfixOp(ref, Ident(nme.CC_REACH)) + else if isIdent(nme.UPARROW) then + in.nextToken() + def toTypeSel(r: Tree): Tree = r match + case id: Ident => cpy.Ident(id)(id.name.toTypeName) + case Select(qual, id) => Select(qual, id.toTypeName) + case _ => r + atSpan(startOffset(ref)): + makeCapsOf(toTypeSel(ref)) + else ref /** CaptureSet ::= `{` CaptureRef {`,` CaptureRef} `}` -- under captureChecking */ diff --git a/tests/neg-custom-args/captures/class-contra.check b/tests/neg-custom-args/captures/class-contra.check index 9fc009ac3d48..808118bd1795 100644 --- a/tests/neg-custom-args/captures/class-contra.check +++ b/tests/neg-custom-args/captures/class-contra.check @@ -1,10 +1,7 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:39 --------------------------------- -12 | def fun(x: K{val f: T^{a}}) = x.setf(a) // error - | ^ - | Found: (a : T^{x, y}) - | Required: T^{} - | - | Note that a capability (K.this.f : T^) in a capture set appearing in contravariant position - | was mapped to (x.f : T^{a}) which is not a capability. Therefore, it was under-approximated to the empty set. +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:40 --------------------------------- +12 | def fun1(k: K{val f: T^{a}}) = k.setf(a) // error + | ^ + | Found: (a : T^{x, y}) + | Required: T^{k.f} | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/class-contra.scala b/tests/neg-custom-args/captures/class-contra.scala index 210fd4e331f1..8ef8e7485a18 100644 --- a/tests/neg-custom-args/captures/class-contra.scala +++ b/tests/neg-custom-args/captures/class-contra.scala @@ -9,5 +9,6 @@ class T def test(x: Cap, y: Cap) = val a: T^{x, y} = ??? - def fun(x: K{val f: T^{a}}) = x.setf(a) // error + def fun1(k: K{val f: T^{a}}) = k.setf(a) // error + def fun2(k: K{val f: a.type}) = k.setf(a) () \ No newline at end of file diff --git a/tests/neg-custom-args/captures/explain-under-approx.check b/tests/neg-custom-args/captures/explain-under-approx.check index 2d2b05b4b95a..c186fc6adb11 100644 --- a/tests/neg-custom-args/captures/explain-under-approx.check +++ b/tests/neg-custom-args/captures/explain-under-approx.check @@ -1,20 +1,14 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:12:10 ------------------------- 12 | col.add(Future(() => 25)) // error | ^^^^^^^^^^^^^^^^ - | Found: Future[Int]{val a: (async : Async^)}^{async} - | Required: Future[Int]^{} - | - | Note that a capability Collector.this.futs* in a capture set appearing in contravariant position - | was mapped to col.futs* which is not a capability. Therefore, it was under-approximated to the empty set. + | Found: Future[Int]{val a: (async : Async^)}^{async} + | Required: Future[Int]^{col.futs*} | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:15:11 ------------------------- 15 | col1.add(Future(() => 25)) // error | ^^^^^^^^^^^^^^^^ - | Found: Future[Int]{val a: (async : Async^)}^{async} - | Required: Future[Int]^{} - | - | Note that a capability Collector.this.futs* in a capture set appearing in contravariant position - | was mapped to col1.futs* which is not a capability. Therefore, it was under-approximated to the empty set. + | Found: Future[Int]{val a: (async : Async^)}^{async} + | Required: Future[Int]^{col1.futs*} | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/filevar-multi-ios.scala b/tests/neg-custom-args/captures/filevar-multi-ios.scala new file mode 100644 index 000000000000..8ffc8d8e299c --- /dev/null +++ b/tests/neg-custom-args/captures/filevar-multi-ios.scala @@ -0,0 +1,41 @@ +import language.experimental.modularity +import compiletime.uninitialized + +class IO extends caps.Capability + +class File: + def write(x: String): Unit = ??? + +object test1: + + class Service(val io: IO, val io2: IO): + var file: File^{io} = uninitialized + var file2: File^{io2} = uninitialized + def log = file.write("log") + + def withFile[T](io: IO)(op: File^{io} => T): T = + op(new File) + + def test(io3: IO, io4: IO) = + withFile(io3): f => + val o = Service(io3, io4) + o.file = f // error + o.file2 = f // error + o.log + +object test2: + + class Service(tracked val io: IO, tracked val io2: IO): + var file: File^{io} = uninitialized + var file2: File^{io2} = uninitialized + def log = file.write("log") + + def withFile[T](io: IO)(op: File^{io} => T): T = + op(new File) + + def test(io3: IO, io4: IO) = + withFile(io3): f => + val o = Service(io3, io4) + o.file = f + o.file2 = f // error + o.log diff --git a/tests/neg-custom-args/captures/i15116.check b/tests/neg-custom-args/captures/i15116.check index df05324866e1..0a16af9f6704 100644 --- a/tests/neg-custom-args/captures/i15116.check +++ b/tests/neg-custom-args/captures/i15116.check @@ -18,13 +18,17 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:5:13 ---------------------------------------- 5 | val x = Foo(m) // error | ^^^^^^ - | Found: Foo{val m: String^{Baz.this}}^{Baz.this} + | Found: Foo{val m²: (Baz.this.m : String^)}^{Baz.this.m} | Required: Foo | + | where: m is a value in trait Baz + | m² is a value in class Foo + | + | | Note that the expected type Foo | is the previously inferred type of value x | which is also the type seen in separately compiled sources. - | The new inferred type Foo{val m: String^{Baz.this}}^{Baz.this} + | The new inferred type Foo{val m: (Baz.this.m : String^)}^{Baz.this.m} | must conform to this type. | | longer explanation available when compiling with `-explain` @@ -48,13 +52,17 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:9:13 ---------------------------------------- 9 | val x = Foo(m) // error | ^^^^^^ - | Found: Foo{val m: String^{Baz2.this}}^{Baz2.this} + | Found: Foo{val m²: (Baz2.this.m : String^)}^{Baz2.this.m} | Required: Foo | + | where: m is a value in trait Baz2 + | m² is a value in class Foo + | + | | Note that the expected type Foo | is the previously inferred type of value x | which is also the type seen in separately compiled sources. - | The new inferred type Foo{val m: String^{Baz2.this}}^{Baz2.this} + | The new inferred type Foo{val m: (Baz2.this.m : String^)}^{Baz2.this.m} | must conform to this type. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/path-box.scala b/tests/neg-custom-args/captures/path-box.scala new file mode 100644 index 000000000000..3213c236aaf5 --- /dev/null +++ b/tests/neg-custom-args/captures/path-box.scala @@ -0,0 +1,20 @@ +class A: + val m: A^ = ??? + val self: this.type = this + +case class Box[+T](value: T) + +def testBox1(a: A^): Box[A^{a}] = + Box(a.m) + +def testBox2(a: A^): Box[A^{a.m}] = + Box(a.m) + +def testBox3(a: A^): Box[A^{a.m}] = + Box(a) // error + +def testBox4(a: A^): Box[A^{a.m}] = + Box(a.m.m.m) + +def testBox5(a: A^): Box[A^{a.m}] = + Box(a.m.m.self) \ No newline at end of file diff --git a/tests/neg-custom-args/captures/path-connection.scala b/tests/neg-custom-args/captures/path-connection.scala new file mode 100644 index 000000000000..3b3820488c8d --- /dev/null +++ b/tests/neg-custom-args/captures/path-connection.scala @@ -0,0 +1,46 @@ +import language.experimental.modularity + +trait Reader: + def read(): String + +trait Sender: + def send(msg: String): Unit + +class Connection extends Reader, Sender: + def read() = "hello" + def send(msg: String) = () + + val readOnly: Reader^ = new Reader: + def read() = Connection.this.read() + +class ReaderProxy(tracked val r: Reader^) extends Reader: + def read() = "(Proxy)" + r.read() + +class SenderProxy(tracked val s: Sender^) extends Sender: + def send(msg: String) = s.send("(Proxy) " + msg) + +def testConnection(c: Connection^)( + handle1: Reader^{c.readOnly} => String, + handle2: Sender^{c} => Unit, + handle3: Reader^{c} => String, + ) = + val m1 = c.read() + c.send("hello") + + val m2 = c.readOnly.read() + + val m3a = handle1(c.readOnly) + val m3b = handle3(c.readOnly) + + val m4a = handle1(c) // error + val m4b = handle3(c) + + val m5a = handle1(new ReaderProxy(c.readOnly)) + val m5b = handle3(new ReaderProxy(c.readOnly)) + + val m6a = handle1(new ReaderProxy(c)) // error + val m6b = handle3(new ReaderProxy(c)) + + handle2(c) + + handle2(new SenderProxy(c)) \ No newline at end of file diff --git a/tests/neg-custom-args/captures/path-illigal.scala b/tests/neg-custom-args/captures/path-illigal.scala new file mode 100644 index 000000000000..f09db0087ef7 --- /dev/null +++ b/tests/neg-custom-args/captures/path-illigal.scala @@ -0,0 +1,7 @@ +class A: + val m: A^ = ??? + var n: A^ = ??? + +def test1(a: A^) = + val c1: A^{a.m} = a.m + val f1: A^{a.n} = a.n // error \ No newline at end of file diff --git a/tests/neg-custom-args/captures/path-simple.scala b/tests/neg-custom-args/captures/path-simple.scala new file mode 100644 index 000000000000..93b6dacebe74 --- /dev/null +++ b/tests/neg-custom-args/captures/path-simple.scala @@ -0,0 +1,27 @@ + +class A: + val m: A^ = ??? + val self: this.type = this + +case class C(ca: A^) + +def test1(a: A^, b: A^) = + val c1: A^{a} = a.m + val c2: A^{a.m} = a.m + val c3: A^{b} = a.m // error + + val d1: A^{a} = a.self + val d2: A^{a.self} = a.self + val d3: A^{a.self} = a + + val e1: A^{a.m} = a.self.m + val e2: A^{a.self.m} = a.self.m + val e3: A^{a.self.m} = a.m + +def test2(a: A^) = + val b: a.type = a + val c1: C^{a} = new C(a) + val c2: C^{a} = new C(a.m) + val c3: C^{a.m} = new C(a.m) + val c4: C^{b} = new C(a) + val c5: C^{a} = new C(b) \ No newline at end of file diff --git a/tests/neg-custom-args/captures/singletons.scala b/tests/neg-custom-args/captures/singletons.scala index 194e6e850dcd..be0ee67ab1bc 100644 --- a/tests/neg-custom-args/captures/singletons.scala +++ b/tests/neg-custom-args/captures/singletons.scala @@ -1,6 +1,6 @@ val x = () => () -val y1: x.type = x // ok -val y2: x.type^{} = x // error: singleton type cannot have capture set -val y3: x.type^{x} = x // error: singleton type cannot have capture set // error -val y4: x.type^ = x // error: singleton type cannot have capture set +val y1: x.type = x +val y2: x.type^{} = x +val y3: x.type^{x} = x // error +val y4: x.type^ = x diff --git a/tests/pos-custom-args/captures/filevar-expanded.scala b/tests/pos-custom-args/captures/filevar-expanded.scala index a883471e8d2e..58e7a0e67e0a 100644 --- a/tests/pos-custom-args/captures/filevar-expanded.scala +++ b/tests/pos-custom-args/captures/filevar-expanded.scala @@ -1,4 +1,5 @@ import language.experimental.captureChecking +import language.experimental.modularity import compiletime.uninitialized object test1: @@ -22,7 +23,7 @@ object test2: class File: def write(x: String): Unit = ??? - class Service(io: IO^): + class Service(tracked val io: IO^): var file: File^{io} = uninitialized def log = file.write("log") diff --git a/tests/pos-custom-args/captures/filevar.scala b/tests/pos-custom-args/captures/filevar.scala index 9ab34fe617b5..dc8d0b18908b 100644 --- a/tests/pos-custom-args/captures/filevar.scala +++ b/tests/pos-custom-args/captures/filevar.scala @@ -1,4 +1,5 @@ import language.experimental.captureChecking +import language.experimental.modularity import compiletime.uninitialized object test1: @@ -22,7 +23,7 @@ object test2: class File: def write(x: String): Unit = ??? - class Service(io: IO): + class Service(tracked val io: IO): var file: File^{io} = uninitialized def log = file.write("log") From ddba6082ba08487d528f773232ad3094e055a874 Mon Sep 17 00:00:00 2001 From: noti0na1 Date: Thu, 19 Sep 2024 15:30:57 +0200 Subject: [PATCH 02/13] Add comment for path-dependent limitation --- compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 5 +---- compiler/src/dotty/tools/dotc/cc/Setup.scala | 5 +++++ tests/neg-custom-args/captures/path-connection.scala | 2 ++ 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index ec1e63137311..b3a1ab44d6cd 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -494,10 +494,7 @@ class CheckCaptures extends Recheck, SymTransformer: val selType = recheckSelection(tree, qualType, name, disambiguate) val selWiden = selType.widen - def isStableSel = selType match - case selType: NamedType => selType.symbol.isStableMember - case _ => false - + if pt == LhsProto || qualType.isBoxedCapturing || selType.isTrackableRef diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 22e7899eeea1..76ae41649517 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -518,6 +518,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: info match case mt: MethodOrPoly => val psyms = psymss.head + // TODO: the substitution does not work for param-dependent method types. + // For example, `(x: T, y: x.f.type) => Unit`. In this case, when we + // substitute `x.f.type`, `x` becomes a `TermParamRef`. But the new method + // type is still under initialization and `paramInfos` is still `null`, + // so the new `NamedType` will not have a denoation. mt.companion(mt.paramNames)( mt1 => if !paramSignatureChanges && !mt.isParamDependent && prevLambdas.isEmpty then diff --git a/tests/neg-custom-args/captures/path-connection.scala b/tests/neg-custom-args/captures/path-connection.scala index 3b3820488c8d..c65aa75b1ed2 100644 --- a/tests/neg-custom-args/captures/path-connection.scala +++ b/tests/neg-custom-args/captures/path-connection.scala @@ -19,6 +19,8 @@ class ReaderProxy(tracked val r: Reader^) extends Reader: class SenderProxy(tracked val s: Sender^) extends Sender: def send(msg: String) = s.send("(Proxy) " + msg) +// TODO: We have to put `c` in the different argument list to make it work. +// See the comments in `integrateRT`. def testConnection(c: Connection^)( handle1: Reader^{c.readOnly} => String, handle2: Sender^{c} => Unit, From 440c053213ae75f6fb68581cf9a3ecb4e30785e7 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 24 Sep 2024 18:05:57 +0200 Subject: [PATCH 03/13] Add alternative subsumes implementations This is done for comparing old with new --- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 46 +++++++++++++++++-- 1 file changed, 41 insertions(+), 5 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index 05162907b608..107b1a178069 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -93,23 +93,59 @@ trait CaptureRef extends TypeProxy, ValueType: final def invalidateCaches() = myCaptureSetRunId = NoRunId + final def subsumes(y: CaptureRef)(using Context): Boolean = + val was = subsumesOld(y) + val now = subsumesNew(y) + if was != now then + println(i"diff for $this subsumes $y, now: $now, ${this.getClass}, ${y.getClass}") + was + + final def subsumesOld(y: CaptureRef)(using Context): Boolean = + (this eq y) + || this.isRootCapability + || y.match + case y: TermRef => + y.prefix.match + case ypre: CaptureRef => + this.subsumesOld(ypre) + || this.match + case x @ TermRef(xpre: CaptureRef, _) => + x.symbol == y.symbol && xpre =:= ypre + case _ => + false + case _ => false + || y.info.match + case y1: SingletonCaptureRef => this.subsumesOld(y1) + case _ => false + case MaybeCapability(y1) => this.stripMaybe.subsumesOld(y1) + case _ => false + || this.match + case ReachCapability(x1) => x1.subsumesOld(y.stripReach) + case x: TermRef => + x.info match + case x1: SingletonCaptureRef => x1.subsumesOld(y) + case _ => false + case x: TermParamRef => subsumesExistentially(x, y) + case x: TypeRef => assumedContainsOf(x).contains(y) + case _ => false + /** x subsumes x * this subsumes this.f * x subsumes y ==> x* subsumes y, x subsumes y? * x subsumes y ==> x* subsumes y*, x? subsumes y? * x: x1.type /\ x1 subsumes y ==> x subsumes y */ - final def subsumes(y: CaptureRef)(using Context): Boolean = + final def subsumesNew(y: CaptureRef)(using Context): Boolean = def compareCaptureRefs(x: Type, y: Type): Boolean = (x eq y) || y.match case y: CaptureRef => x.match - case x: CaptureRef => x.subsumes(y) + case x: CaptureRef => x.subsumesNew(y) case _ => false case _ => false def compareUndelying(x: Type): Boolean = x match - case x: SingletonCaptureRef => x.subsumes(y) + case x: SingletonCaptureRef => x.subsumesNew(y) case x: AndType => compareUndelying(x.tp1) || compareUndelying(x.tp2) case x: OrType => compareUndelying(x.tp1) && compareUndelying(x.tp2) case _ => false @@ -140,11 +176,11 @@ trait CaptureRef extends TypeProxy, ValueType: if compareCaptureRefs(this, y.prefix) then return true // underlying if compareCaptureRefs(this, y.info) then return true - case MaybeCapability(y1) => return this.stripMaybe.subsumes(y1) + case MaybeCapability(y1) => return this.stripMaybe.subsumesNew(y1) case _ => return this.match - case ReachCapability(x1) => x1.subsumes(y.stripReach) + case ReachCapability(x1) => x1.subsumesNew(y.stripReach) case x: TermRef => compareUndelying(x.info) case CapturingType(x1, _) => compareUndelying(x1) case x: TermParamRef => subsumesExistentially(x, y) From 45df15269d9c237e78a4f4322a7b8e52bfec02e0 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 24 Sep 2024 18:07:50 +0200 Subject: [PATCH 04/13] Revert to previous subsumes scheme Add the path cases without changing the whole logic --- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 82 +++---------------- 1 file changed, 12 insertions(+), 70 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index 107b1a178069..195f07f778eb 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -93,21 +93,21 @@ trait CaptureRef extends TypeProxy, ValueType: final def invalidateCaches() = myCaptureSetRunId = NoRunId + /** x subsumes x + * this subsumes this.f + * x subsumes y ==> x* subsumes y, x subsumes y? + * x subsumes y ==> x* subsumes y*, x? subsumes y? + * x: x1.type /\ x1 subsumes y ==> x subsumes y + * TODO: Document path cases + */ final def subsumes(y: CaptureRef)(using Context): Boolean = - val was = subsumesOld(y) - val now = subsumesNew(y) - if was != now then - println(i"diff for $this subsumes $y, now: $now, ${this.getClass}, ${y.getClass}") - was - - final def subsumesOld(y: CaptureRef)(using Context): Boolean = (this eq y) || this.isRootCapability || y.match case y: TermRef => y.prefix.match case ypre: CaptureRef => - this.subsumesOld(ypre) + this.subsumes(ypre) || this.match case x @ TermRef(xpre: CaptureRef, _) => x.symbol == y.symbol && xpre =:= ypre @@ -115,78 +115,20 @@ trait CaptureRef extends TypeProxy, ValueType: false case _ => false || y.info.match - case y1: SingletonCaptureRef => this.subsumesOld(y1) + case y1: SingletonCaptureRef => this.subsumes(y1) case _ => false - case MaybeCapability(y1) => this.stripMaybe.subsumesOld(y1) + case MaybeCapability(y1) => this.stripMaybe.subsumes(y1) case _ => false || this.match - case ReachCapability(x1) => x1.subsumesOld(y.stripReach) + case ReachCapability(x1) => x1.subsumes(y.stripReach) case x: TermRef => x.info match - case x1: SingletonCaptureRef => x1.subsumesOld(y) + case x1: SingletonCaptureRef => x1.subsumes(y) case _ => false case x: TermParamRef => subsumesExistentially(x, y) case x: TypeRef => assumedContainsOf(x).contains(y) case _ => false - /** x subsumes x - * this subsumes this.f - * x subsumes y ==> x* subsumes y, x subsumes y? - * x subsumes y ==> x* subsumes y*, x? subsumes y? - * x: x1.type /\ x1 subsumes y ==> x subsumes y - */ - final def subsumesNew(y: CaptureRef)(using Context): Boolean = - def compareCaptureRefs(x: Type, y: Type): Boolean = - (x eq y) - || y.match - case y: CaptureRef => x.match - case x: CaptureRef => x.subsumesNew(y) - case _ => false - case _ => false - - def compareUndelying(x: Type): Boolean = x match - case x: SingletonCaptureRef => x.subsumesNew(y) - case x: AndType => compareUndelying(x.tp1) || compareUndelying(x.tp2) - case x: OrType => compareUndelying(x.tp1) && compareUndelying(x.tp2) - case _ => false - - if (this eq y) || this.isRootCapability then return true - - // similar to compareNamed in TypeComparer - y match - case y: TermRef => - this match - case x: TermRef => - val xSym = x.symbol - val ySym = y.symbol - - // check x.f and y.f - if (xSym ne NoSymbol) - && (xSym eq ySym) - && compareCaptureRefs(x.prefix, y.prefix) - || (x.name eq y.name) - && x.isPrefixDependentMemberRef - && compareCaptureRefs(x.prefix, y.prefix) - && x.signature == y.signature - && !(xSym.isClass && ySym.isClass) - then return true - case _ => - - // shorten - if compareCaptureRefs(this, y.prefix) then return true - // underlying - if compareCaptureRefs(this, y.info) then return true - case MaybeCapability(y1) => return this.stripMaybe.subsumesNew(y1) - case _ => - - return this.match - case ReachCapability(x1) => x1.subsumesNew(y.stripReach) - case x: TermRef => compareUndelying(x.info) - case CapturingType(x1, _) => compareUndelying(x1) - case x: TermParamRef => subsumesExistentially(x, y) - case x: TypeRef => assumedContainsOf(x).contains(y) - case _ => false - def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] = CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty) From 263d6eb9337f6849ee8aa77941a017d500af68ff Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 25 Sep 2024 11:57:39 +0200 Subject: [PATCH 05/13] Add logic to mark paths as used If we refer to a path `a.b`, we should mark `a.b` as used, which is better than marking `a`. --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 27 +++++++++++++------ .../dotty/tools/dotc/transform/Recheck.scala | 15 +++++------ .../dotty/tools/dotc/typer/ProtoTypes.scala | 6 +++-- tests/pos-custom-args/captures/path-use.scala | 19 +++++++++++++ 4 files changed, 49 insertions(+), 18 deletions(-) create mode 100644 tests/pos-custom-args/captures/path-use.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index b3a1ab44d6cd..05bcecf86067 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -13,7 +13,7 @@ import Trees.* import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents, OverridingPairsChecker} import typer.Checking.{checkBounds, checkAppliedTypesIn} import typer.ErrorReporting.{Addenda, NothingToAdd, err} -import typer.ProtoTypes.{AnySelectionProto, LhsProto} +import typer.ProtoTypes.{LhsProto, WildcardSelectionProto} import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property} import transform.{Recheck, PreRecheck, CapturedVars} import Recheck.* @@ -183,6 +183,9 @@ object CheckCaptures: /** Attachment key for bodies of closures, provided they are values */ val ClosureBodyValue = Property.Key[Unit] + /** A prototype that indicates selection with an immutable value */ + class PathSelectionProto(val sym: Symbol, val pt: Type)(using Context) extends WildcardSelectionProto + class CheckCaptures extends Recheck, SymTransformer: thisPhase => @@ -357,12 +360,13 @@ class CheckCaptures extends Recheck, SymTransformer: * the environment in which `sym` is defined. */ def markFree(sym: Symbol, pos: SrcPos)(using Context): Unit = - if sym.exists then - val ref = sym.termRef - if ref.isTracked then - forallOuterEnvsUpTo(sym.enclosure): env => - capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}") - checkElem(ref, env.captured, pos, provenance(env)) + markFree(sym, sym.termRef, pos) + + def markFree(sym: Symbol, ref: TermRef, pos: SrcPos)(using Context): Unit = + if sym.exists && ref.isTracked then + forallOuterEnvsUpTo(sym.enclosure): env => + capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}") + checkElem(ref, env.captured, pos, provenance(env)) /** Make sure (projected) `cs` is a subset of the capture sets of all enclosing * environments. At each stage, only include references from `cs` that are outside @@ -464,9 +468,16 @@ class CheckCaptures extends Recheck, SymTransformer: includeCallCaptures(tree.symbol, tree.srcPos) else //debugShowEnvs() - markFree(tree.symbol, tree.srcPos) + def addSelects(ref: TermRef, pt: Type): TermRef = pt match + case pt: PathSelectionProto => addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt) + case _ => ref + markFree(tree.symbol, addSelects(tree.symbol.termRef, pt), tree.srcPos) super.recheckIdent(tree, pt) + override def selectionProto(tree: Select, pt: Type)(using Context): Type = + if !tree.symbol.isOneOf(UnstableValueFlags) then PathSelectionProto(tree.symbol, pt) + else super.selectionProto(tree, pt) + /** A specialized implementation of the selection rule. * * E |- f: T{ m: R^Cr }^{f} diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala index 03f0001110d3..26a75215bab1 100644 --- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala +++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala @@ -12,7 +12,7 @@ import DenotTransformers.{DenotTransformer, IdentityDenotTransformer, SymTransfo import NamerOps.linkConstructorParams import NullOpsDecorator.stripNull import typer.ErrorReporting.err -import typer.ProtoTypes.* +import typer.ProtoTypes.{AnySelectionProto, LhsProto} import typer.TypeAssigner.seqLitType import typer.ConstFold import typer.ErrorReporting.{Addenda, NothingToAdd} @@ -203,13 +203,12 @@ abstract class Recheck extends Phase, SymTransformer: tree.tpe def recheckSelect(tree: Select, pt: Type)(using Context): Type = - recheckSelection(tree, recheckSelectQualifier(tree), tree.name, pt) + recheckSelection(tree, + recheck(tree.qualifier, selectionProto(tree, pt)).widenIfUnstable, + tree.name, pt) - def recheckSelectQualifier(tree: Select)(using Context): Type = - val proto = - if tree.symbol == defn.Any_asInstanceOf then WildcardType - else AnySelectionProto - recheck(tree.qualifier, proto).widenIfUnstable + def selectionProto(tree: Select, pt: Type)(using Context): Type = + if tree.symbol == defn.Any_asInstanceOf then WildcardType else AnySelectionProto def recheckSelection(tree: Select, qualType: Type, name: Name, sharpen: Denotation => Denotation)(using Context): Type = @@ -308,7 +307,7 @@ abstract class Recheck extends Phase, SymTransformer: def recheckApply(tree: Apply, pt: Type)(using Context): Type = val (funtpe0, qualType) = tree.fun match case fun: Select => - val qualType = recheckSelectQualifier(fun) + val qualType = recheck(fun.qualifier, selectionProto(fun, WildcardType)).widenIfUnstable (recheckSelection(fun, qualType, fun.name, WildcardType), qualType) case _ => (recheck(tree.fun), NoType) diff --git a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala index a69a63d1ceef..53e0b456ed9a 100644 --- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala +++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala @@ -324,6 +324,8 @@ object ProtoTypes { case tp: UnapplyFunProto => new UnapplySelectionProto(name, nameSpan) case tp => SelectionProto(name, IgnoredProto(tp), typer, privateOK = true, nameSpan) + class WildcardSelectionProto extends SelectionProto(nme.WILDCARD, WildcardType, NoViewsAllowed, true, NoSpan) + /** A prototype for expressions [] that are in some unspecified selection operation * * [].?: ? @@ -332,9 +334,9 @@ object ProtoTypes { * operation is further selection. In this case, the expression need not be a value. * @see checkValue */ - @sharable object AnySelectionProto extends SelectionProto(nme.WILDCARD, WildcardType, NoViewsAllowed, true, NoSpan) + @sharable object AnySelectionProto extends WildcardSelectionProto - @sharable object SingletonTypeProto extends SelectionProto(nme.WILDCARD, WildcardType, NoViewsAllowed, true, NoSpan) + @sharable object SingletonTypeProto extends WildcardSelectionProto /** A prototype for selections in pattern constructors */ class UnapplySelectionProto(name: Name, nameSpan: Span) extends SelectionProto(name, WildcardType, NoViewsAllowed, true, nameSpan) diff --git a/tests/pos-custom-args/captures/path-use.scala b/tests/pos-custom-args/captures/path-use.scala new file mode 100644 index 000000000000..5eb2b60fd218 --- /dev/null +++ b/tests/pos-custom-args/captures/path-use.scala @@ -0,0 +1,19 @@ +import language.experimental.namedTuples + +class IO + +class C(val f: IO^): + val procs: List[Proc] = ??? + +type Proc = () => Unit + +def test(io: IO^) = + val c = C(io) + val f = () => println(c.f) + val _: () ->{c.f} Unit = f + + val x = c.procs + val _: List[() ->{c.procs*} Unit] = x + + val g = () => println(c.procs.head) + val _: () ->{c.procs*} Unit = g From 152710b04a7f14a5aba57a3d828865b58bbb5855 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 25 Sep 2024 21:01:05 +0200 Subject: [PATCH 06/13] Tweaks to path checking and massage tests Needed to make stdlib2-cc go through. There were two errors. One in LayListIterable required a type annotation and a tweak to markFree. The other in Vieew.scala required a cast, but this could be fixed with better handling of pattern matching. path-patmat-should-be-pos.scala is a minimization. --- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 27 ++++++++++++------- .../dotty/tools/dotc/cc/CheckCaptures.scala | 25 ++++++++++++----- .../src/scala/collection/View.scala | 5 +++- .../immutable/LazyListIterable.scala | 4 ++- .../captures/path-patmat-should-be-pos.scala | 26 ++++++++++++++++++ 5 files changed, 69 insertions(+), 18 deletions(-) create mode 100644 tests/neg-custom-args/captures/path-patmat-should-be-pos.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index 195f07f778eb..bbaf0c7d2fa0 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -101,6 +101,19 @@ trait CaptureRef extends TypeProxy, ValueType: * TODO: Document path cases */ final def subsumes(y: CaptureRef)(using Context): Boolean = + + def subsumingRefs(x: Type, y: Type): Boolean = x match + case x: CaptureRef => y match + case y: CaptureRef => x.subsumes(y) + case _ => false + case _ => false + + def viaInfo(info: Type)(test: Type => Boolean): Boolean = info.match + case info: SingletonCaptureRef => test(info) + case info: AndType => test(info.tp1) || test(info.tp2) + case info: OrType => test(info.tp1) && test(info.tp2) + case _ => false + (this eq y) || this.isRootCapability || y.match @@ -109,25 +122,21 @@ trait CaptureRef extends TypeProxy, ValueType: case ypre: CaptureRef => this.subsumes(ypre) || this.match - case x @ TermRef(xpre: CaptureRef, _) => - x.symbol == y.symbol && xpre =:= ypre + case x @ TermRef(xpre: CaptureRef, _) if x.symbol == y.symbol => + subsumingRefs(xpre, ypre) && subsumingRefs(ypre, xpre) case _ => false case _ => false - || y.info.match - case y1: SingletonCaptureRef => this.subsumes(y1) - case _ => false + || viaInfo(y.info)(subsumingRefs(this, _)) case MaybeCapability(y1) => this.stripMaybe.subsumes(y1) case _ => false || this.match case ReachCapability(x1) => x1.subsumes(y.stripReach) - case x: TermRef => - x.info match - case x1: SingletonCaptureRef => x1.subsumes(y) - case _ => false + case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y)) case x: TermParamRef => subsumesExistentially(x, y) case x: TypeRef => assumedContainsOf(x).contains(y) case _ => false + end subsumes def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] = CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 05bcecf86067..19acebde8651 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -466,16 +466,24 @@ class CheckCaptures extends Recheck, SymTransformer: if tree.symbol.info.isParameterless then // there won't be an apply; need to include call captures now includeCallCaptures(tree.symbol, tree.srcPos) - else + else if !tree.symbol.isStatic then //debugShowEnvs() def addSelects(ref: TermRef, pt: Type): TermRef = pt match - case pt: PathSelectionProto => addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt) + 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. + addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt) case _ => ref - markFree(tree.symbol, addSelects(tree.symbol.termRef, pt), tree.srcPos) + val ref = tree.symbol.termRef + val pathRef = addSelects(ref, pt) + //if pathRef ne ref then + // println(i"add selects $ref --> $pathRef") + markFree(tree.symbol, if false then ref else pathRef, tree.srcPos) super.recheckIdent(tree, pt) override def selectionProto(tree: Select, pt: Type)(using Context): Type = - if !tree.symbol.isOneOf(UnstableValueFlags) then PathSelectionProto(tree.symbol, pt) + val sym = tree.symbol + if !sym.isOneOf(UnstableValueFlags) && !sym.isStatic then PathSelectionProto(sym, pt) else super.selectionProto(tree, pt) /** A specialized implementation of the selection rule. @@ -1141,11 +1149,14 @@ class CheckCaptures extends Recheck, SymTransformer: (erefs /: erefs.elems): (erefs, eref) => eref match case eref: ThisType if isPureContext(ctx.owner, eref.cls) => - erefs ++ arefs.filter { - case aref: TermRef => eref.cls.isProperlyContainedIn(aref.symbol.owner) + def isOuterRef(aref: Type): Boolean = aref match + case aref: TermRef => + val owner = aref.symbol.owner + if owner.isClass then isOuterRef(aref.prefix) + else eref.cls.isProperlyContainedIn(owner) case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls) case _ => false - } + erefs ++ arefs.filter(isOuterRef) case _ => erefs diff --git a/scala2-library-cc/src/scala/collection/View.scala b/scala2-library-cc/src/scala/collection/View.scala index 31c544a46beb..132934dbe3bd 100644 --- a/scala2-library-cc/src/scala/collection/View.scala +++ b/scala2-library-cc/src/scala/collection/View.scala @@ -150,7 +150,10 @@ object View extends IterableFactory[View] { object Filter { def apply[A](underlying: Iterable[A]^, p: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, p} = underlying match { - case filter: Filter[A] if filter.isFlipped == isFlipped => new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped) + case filter: Filter[A] if filter.isFlipped == isFlipped => + new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped) + .asInstanceOf[Filter[A]^{underlying, p}] + // !!! asInstanceOf needed once paths were added, see path-patmat-should-be-pos.scala for minimization case _ => new Filter(underlying, p, isFlipped) } } diff --git a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala index 2f7b017a6729..28ce8da104aa 100644 --- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala +++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala @@ -1366,7 +1366,9 @@ object LazyListIterable extends IterableFactory[LazyListIterable] { case SerializeEnd => initRead = true case a => init += a.asInstanceOf[A] } - val tail = in.readObject().asInstanceOf[LazyListIterable[A]] + val tail: LazyListIterable[A] = in.readObject().asInstanceOf[LazyListIterable[A]] + // Explicit type annotation needed so that tail.state below is dropped from capture set. + // Before paths were added, it was tail that was added, and the `asSeenFrom` to a pure type made it work. // scala/scala#10118: caution that no code path can evaluate `tail.state` // before the resulting LazyListIterable is returned val it = init.toList.iterator diff --git a/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala b/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala new file mode 100644 index 000000000000..aca6102204a3 --- /dev/null +++ b/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala @@ -0,0 +1,26 @@ +class It[A] + +class Filter[A](val underlying: It[A]^, val p: A => Boolean) extends It[A] +object Filter: + def apply[A](underlying: It[A]^, p: A => Boolean): Filter[A]^{underlying, p} = + underlying match + case filter: Filter[A]^ => + val x = new Filter(filter.underlying, a => filter.p(a) && p(a)) + x: Filter[A]^{underlying, p} // error + // !!! should work, it seems to be the case that the system does not recognize that + // underlying and filter are aliases. + + // On the other hand, the following works: + locally: + val filter: underlying.type & Filter[A] = ??? + val a: It[A]^{filter.underlying} = ??? + val b: It[A]^{underlying} = a + val x = new Filter(filter.underlying, a => filter.p(a) && p(a)) + x: Filter[A]^{underlying, p} + + locally: + val filter: underlying.type & Filter[A]^ = ??? + val a: It[A]^{filter.underlying} = ??? + val b: It[A]^{underlying} = a + val x = new Filter(filter.underlying, a => filter.p(a) && p(a)) + x: Filter[A]^{underlying, p} From 215b67af405fc0b20e4af73884a2fbe0e7e352e9 Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 27 Sep 2024 19:04:45 +0200 Subject: [PATCH 07/13] Account for added outer refs in the capture sets of classes --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 45 ++++++++++++++----- .../captures/outerRefsUses.scala | 10 +++++ 2 files changed, 45 insertions(+), 10 deletions(-) create mode 100644 tests/neg-custom-args/captures/outerRefsUses.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 19acebde8651..4d905a5df4ab 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1089,7 +1089,7 @@ class CheckCaptures extends Recheck, SymTransformer: if actualBoxed eq actual then // Only `addOuterRefs` when there is no box adaptation - expected1 = addOuterRefs(expected1, actual) + expected1 = addOuterRefs(expected1, actual, tree.srcPos) if isCompatible(actualBoxed, expected1) then if debugSuccesses then tree match case Ident(_) => @@ -1130,8 +1130,12 @@ class CheckCaptures extends Recheck, SymTransformer: * that are outside `Cls`. These are all accessed through `Cls.this`, * so we can assume they are already accounted for by `Ce` and adding * them explicitly to `Ce` changes nothing. + * - To make up for this, we also add these variables to the capture set of `Cls`, + * so that all instances of `Cls` will capture these outer references. + * So in a sense we use `{Cls.this}` as a placeholder for certain outer captures. + * that we needed to be subsumed by `Cls.this`. */ - private def addOuterRefs(expected: Type, actual: Type)(using Context): Type = + private def addOuterRefs(expected: Type, actual: Type, pos: SrcPos)(using Context): Type = def isPure(info: Type): Boolean = info match case info: PolyType => isPure(info.resType) @@ -1144,19 +1148,40 @@ class CheckCaptures extends Recheck, SymTransformer: else isPure(owner.info) && isPureContext(owner.owner, limit) // Augment expeced capture set `erefs` by all references in actual capture - // set `arefs` that are outside some `this.type` reference in `erefs` + // set `arefs` that are outside some `C.this.type` reference in `erefs` for an enclosing + // class `C`. If an added reference is not a ThisType itself, add it to the capture set + // (i.e. use set) of the `C`. This makes sure that any outer reference implicitly subsumed + // by `C.this` becomes a capture reference of every instance of `C`. def augment(erefs: CaptureSet, arefs: CaptureSet): CaptureSet = (erefs /: erefs.elems): (erefs, eref) => eref match case eref: ThisType if isPureContext(ctx.owner, eref.cls) => - def isOuterRef(aref: Type): Boolean = aref match - case aref: TermRef => - val owner = aref.symbol.owner - if owner.isClass then isOuterRef(aref.prefix) - else eref.cls.isProperlyContainedIn(owner) + + def pathRoot(aref: Type): Type = aref match + case aref: NamedType if aref.symbol.owner.isClass => pathRoot(aref.prefix) + case _ => aref + + def isOuterRef(aref: Type): Boolean = pathRoot(aref) match + case aref: NamedType => eref.cls.isProperlyContainedIn(aref.symbol.owner) case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls) case _ => false - erefs ++ arefs.filter(isOuterRef) + + val outerRefs = arefs.filter(isOuterRef) + + // Include implicitly added outer references in the capture set of the class of `eref`. + for outerRef <- outerRefs.elems do + if !erefs.elems.contains(outerRef) + && !pathRoot(outerRef).isInstanceOf[ThisType] + // we don't need to add outer ThisTypes as these are anyway added as path + // prefixes at the use site. And this exemption is required since capture sets + // of non-local classes are always empty, so we can't add an outer this to them. + then + def provenance = + i""" of the enclosing class ${eref.cls}. + |The reference was included since we tried to establish that $arefs <: $erefs""" + checkElem(outerRef, capturedVars(eref.cls), pos, provenance) + + erefs ++ outerRefs case _ => erefs @@ -1341,7 +1366,7 @@ class CheckCaptures extends Recheck, SymTransformer: * @param sym symbol of the field definition that is being checked */ override def checkSubType(actual: Type, expected: Type)(using Context): Boolean = - val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing) + val expected1 = alignDependentFunction(addOuterRefs(expected, actual, srcPos), actual.stripCapturing) val actual1 = val saved = curEnv try diff --git a/tests/neg-custom-args/captures/outerRefsUses.scala b/tests/neg-custom-args/captures/outerRefsUses.scala new file mode 100644 index 000000000000..cd03c8c41efd --- /dev/null +++ b/tests/neg-custom-args/captures/outerRefsUses.scala @@ -0,0 +1,10 @@ +class IO +def test(io: IO^) = + class C: + def foo() = () => + val x: IO^{this} = io + () + val c = new C + val _: C^{io} = c // ok + val _: C = c // error + () From dc8b8a0fe5c03d8eb2f9cb6f9cba66bed8cc636b Mon Sep 17 00:00:00 2001 From: odersky Date: Sat, 5 Oct 2024 17:52:19 +0200 Subject: [PATCH 08/13] Recognize double annotated capabilities such as x*? x*? is x.type @reach @maybe. This was not recognized before. --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 4 ++-- tests/neg-custom-args/captures/i21646.scala | 13 ++++++++++++ tests/neg-custom-args/captures/uses.scala | 20 +++++++++++++++++++ 3 files changed, 35 insertions(+), 2 deletions(-) create mode 100644 tests/neg-custom-args/captures/i21646.scala create mode 100644 tests/neg-custom-args/captures/uses.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 79cc7d136e45..db17022efe92 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -640,8 +640,8 @@ object CapsOfApply: class AnnotatedCapability(annot: Context ?=> ClassSymbol): def apply(tp: Type)(using Context) = AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan)) - def unapply(tree: AnnotatedType)(using Context): Option[SingletonCaptureRef] = tree match - case AnnotatedType(parent: SingletonCaptureRef, ann) if ann.symbol == annot => Some(parent) + def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match + case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent) case _ => None /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express diff --git a/tests/neg-custom-args/captures/i21646.scala b/tests/neg-custom-args/captures/i21646.scala new file mode 100644 index 000000000000..42c493a9ea80 --- /dev/null +++ b/tests/neg-custom-args/captures/i21646.scala @@ -0,0 +1,13 @@ +import language.experimental.captureChecking +import caps.Capability + +trait File extends Capability + +class Resource[T <: Capability](gen: T): + def use[U](f: T => U): U = + f(gen) // error + +@main def run = + val myFile: File = ??? + val r = Resource(myFile) // error + () diff --git a/tests/neg-custom-args/captures/uses.scala b/tests/neg-custom-args/captures/uses.scala new file mode 100644 index 000000000000..b872c7b03ec7 --- /dev/null +++ b/tests/neg-custom-args/captures/uses.scala @@ -0,0 +1,20 @@ +class C +def test(x: C^, y: C^) = + class D { + println(x) + def foo() = println(y) + } + val d = D() + val _: D^{y} = d // error, should be ok + val _: D = d // error + + val f = () => println(D()) + val _: () ->{x} Unit = f // ok + val _: () -> Unit = f // should be error + + def g = () => + println(x) + () => println(y) + val _: () ->{x} () ->{y} Unit = g // error, should be ok + val _: () -> () -> Unit = g // error + From 5215945e0da3cf2470170053638a861d20f175b9 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 9 Oct 2024 10:46:46 +0200 Subject: [PATCH 09/13] Allow annotations after `^` and `^{xs}` We extend the grammar to allow e.g. `Iterator[T]^ @use`. --- compiler/src/dotty/tools/dotc/parsing/Parsers.scala | 11 ++++++----- compiler/src/dotty/tools/dotc/parsing/Tokens.scala | 2 +- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala index 96f09a0d6214..cd481dba14ef 100644 --- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala +++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala @@ -1827,7 +1827,7 @@ object Parsers { if in.token == LPAREN then funParamClause() :: funParamClauses() else Nil /** InfixType ::= RefinedType {id [nl] RefinedType} - * | RefinedType `^` // under capture checking + * | RefinedType `^` {Annotation} // under capture checking */ def infixType(): Tree = infixTypeRest(refinedType()) @@ -1838,7 +1838,7 @@ object Parsers { && !(isIdent(nme.as) && in.featureEnabled(Feature.modularity)) && nextCanFollowOperator(canStartInfixTypeTokens)) - /** RefinedType ::= WithType {[nl] Refinement} [`^` CaptureSet] + /** RefinedType ::= WithType {[nl] Refinement} [`^` CaptureSet {Annotation}] */ val refinedTypeFn: Location => Tree = _ => refinedType() @@ -1867,9 +1867,10 @@ object Parsers { else if Feature.ccEnabled && in.isIdent(nme.UPARROW) && isCaptureUpArrow then atSpan(t.span.start): in.nextToken() - if in.token == LBRACE - then makeRetaining(t, captureSet(), tpnme.retains) - else makeRetaining(t, Nil, tpnme.retainsCap) + annotTypeRest: + if in.token == LBRACE + then makeRetaining(t, captureSet(), tpnme.retains) + else makeRetaining(t, Nil, tpnme.retainsCap) else t } diff --git a/compiler/src/dotty/tools/dotc/parsing/Tokens.scala b/compiler/src/dotty/tools/dotc/parsing/Tokens.scala index b0a533b2f1df..a7f44fc8370e 100644 --- a/compiler/src/dotty/tools/dotc/parsing/Tokens.scala +++ b/compiler/src/dotty/tools/dotc/parsing/Tokens.scala @@ -232,7 +232,7 @@ object Tokens extends TokensCommon { final val canStartExprTokens2: TokenSet = canStartExprTokens3 | BitSet(DO) final val canStartInfixTypeTokens: TokenSet = literalTokens | identifierTokens | BitSet( - THIS, SUPER, USCORE, LPAREN, LBRACE, AT) + THIS, SUPER, USCORE, LPAREN, LBRACE) final val canStartTypeTokens: TokenSet = canStartInfixTypeTokens | BitSet(LBRACE) From 17460918d302e59eaba5b2445a52f2919cf58147 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 9 Oct 2024 11:30:25 +0200 Subject: [PATCH 10/13] First version of @use checking --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 62 ++++++++++++++----- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 15 ++++- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 8 ++- .../dotty/tools/dotc/cc/CheckCaptures.scala | 45 ++++++++++++-- compiler/src/dotty/tools/dotc/cc/Setup.scala | 4 +- .../dotty/tools/dotc/core/Definitions.scala | 24 ++++++- .../src/dotty/tools/dotc/core/StdNames.scala | 1 + .../dotty/tools/dotc/core/TypeComparer.scala | 41 ++++++++---- .../tools/dotc/printing/PlainPrinter.scala | 3 +- .../tools/dotc/printing/RefinedPrinter.scala | 4 +- .../internal/reachUnderUseCapability.scala | 9 +++ library/src/scala/caps.scala | 1 + tests/neg-custom-args/captures/i15749a.scala | 4 +- tests/neg-custom-args/captures/i21347.check | 2 +- tests/neg-custom-args/captures/i21614.check | 2 +- tests/neg-custom-args/captures/i21614.scala | 6 +- .../captures/leak-problem-2.scala | 2 +- tests/neg-custom-args/captures/reaches.scala | 8 +-- .../captures/unbox-overrides.check | 35 ++++++----- .../captures/unbox-overrides.scala | 22 +++++-- tests/neg-custom-args/captures/useAnnot.check | 4 ++ tests/neg-custom-args/captures/useAnnot.scala | 16 +++++ tests/neg/i20503.scala | 4 +- tests/neg/leak-problem-unboxed.scala | 11 ++-- .../captures/curried-uses.scala | 9 +++ 25 files changed, 262 insertions(+), 80 deletions(-) create mode 100644 library/src/scala/annotation/internal/reachUnderUseCapability.scala create mode 100644 tests/neg-custom-args/captures/useAnnot.check create mode 100644 tests/neg-custom-args/captures/useAnnot.scala create mode 100644 tests/pos-custom-args/captures/curried-uses.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index db17022efe92..74a10bd723ff 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -92,6 +92,16 @@ class CCState: */ val approxWarnings: mutable.ListBuffer[Message] = mutable.ListBuffer() + /** The operation to perform `recordUse` is called. This is typically the case + * when a subtype check is performed between a part of a function argument + * and a corresponding part of a formal parameter that was labelled @use. + * Such annotations are mapped to `[T]` applications, which are handled + * as compiletime ops. + * The parameter to the handler is typically the deep capture set of the argument. + * The result of the handler is the result to be returned from the subtype check. + */ + private var useHandler: CaptureSet => Boolean = Function.const(true) + private var curLevel: Level = outermostLevel private val symLevel: mutable.Map[Symbol, Int] = mutable.Map() @@ -108,6 +118,17 @@ object CCState: */ def currentLevel(using Context): Level = ccState.curLevel + /** Perform operation `op` with a given useHandler */ + inline def withUseHandler[T](handler: CaptureSet => Boolean)(inline op: T)(using Context): T = + val ccs = ccState + val saved = ccs.useHandler + ccs.useHandler = handler + try op finally ccs.useHandler = saved + + /** Record a deep capture set in the current `useSet` */ + def recordUse(cs: CaptureSet)(using Context): Boolean = + ccState.useHandler(cs) + inline def inNestedLevel[T](inline op: T)(using Context): T = val ccs = ccState val saved = ccs.curLevel @@ -146,7 +167,7 @@ extension (tree: Tree) */ def toCaptureRefs(using Context): List[CaptureRef] = tree match case ReachCapabilityApply(arg) => - arg.toCaptureRefs.map(_.reach) + arg.toCaptureRefs.map(_.reach()) case CapsOfApply(arg) => arg.toCaptureRefs case _ => tree.tpe.dealiasKeepAnnots match @@ -204,6 +225,7 @@ extension (tp: Type) tp.derivesFrom(defn.Caps_CapSet) case AnnotatedType(parent, annot) => (annot.symbol == defn.ReachCapabilityAnnot + || annot.symbol == defn.ReachUnderUseCapabilityAnnot || annot.symbol == defn.MaybeCapabilityAnnot ) && parent.isTrackableRef case _ => @@ -233,7 +255,8 @@ extension (tp: Type) if dcs.isAlwaysEmpty then dcs else tp match case tp @ ReachCapability(_) => tp.singletonCaptureSet - case tp: SingletonCaptureRef => tp.reach.singletonCaptureSet + case tp @ ReachUnderUseCapability(_) => tp.singletonCaptureSet + case tp: SingletonCaptureRef => tp.reach().singletonCaptureSet case _ => dcs /** A type capturing `ref` */ @@ -396,9 +419,11 @@ extension (tp: Type) * type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}` * are unrelated. */ - def reach(using Context): CaptureRef = tp match + def reach(underUse: Boolean = false)(using Context): CaptureRef = tp match case tp: CaptureRef if tp.isTrackableRef => - if tp.isReach then tp else ReachCapability(tp) + if tp.isReach then tp + else if underUse then ReachUnderUseCapability(tp) + else ReachCapability(tp) /** If `x` is a capture ref, its maybe capability `x?`, represented internally * as `x @maybeCapability`. `x?` stands for a capability `x` that might or might @@ -471,26 +496,32 @@ extension (tp: Type) object narrowCaps extends TypeMap: /** Has the variance been flipped at this point? */ private var isFlipped: Boolean = false + private var underUse = false def apply(t: Type) = val saved = isFlipped try if variance <= 0 then isFlipped = true - t.dealias match - case t1 @ CapturingType(p, cs) if cs.isUniversal && !isFlipped => - t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet) - case t1 @ FunctionOrMethod(args, res @ Existential(_, _)) + t.dealiasKeepAnnots match + case t @ CapturingType(p, cs) if cs.isUniversal && !isFlipped => + t.derivedCapturingType(apply(p), ref.reach(underUse).singletonCaptureSet) + case t @ AnnotatedType(parent, ann) => + if ann.symbol == defn.UseAnnot then + val saved = underUse + underUse = true + try mapOver(t) + finally underUse = saved + else + t.derivedAnnotatedType(this(parent), ann) + case t @ FunctionOrMethod(args, res @ Existential(_, _)) if args.forall(_.isAlwaysPure) => // Also map existentials in results to reach capabilities if all // preceding arguments are known to be always pure - apply(t1.derivedFunctionOrMethod(args, Existential.toCap(res))) + this(t.derivedFunctionOrMethod(args, Existential.toCap(res))) case Existential(_, _) => t - case _ => t match - case t @ CapturingType(p, cs) => - t.derivedCapturingType(apply(p), cs) // don't map capture set variables - case t => - mapOver(t) + case _ => + mapOver(t) finally isFlipped = saved end narrowCaps @@ -640,7 +671,7 @@ object CapsOfApply: class AnnotatedCapability(annot: Context ?=> ClassSymbol): def apply(tp: Type)(using Context) = AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan)) - def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match + def unapply(tp: AnnotatedType)(using Context): Option[CaptureRef] = tp match case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent) case _ => None @@ -648,6 +679,7 @@ class AnnotatedCapability(annot: Context ?=> ClassSymbol): * the reach capability `ref*` as a type. */ object ReachCapability extends AnnotatedCapability(defn.ReachCapabilityAnnot) +object ReachUnderUseCapability extends AnnotatedCapability(defn.ReachUnderUseCapabilityAnnot) /** An extractor for `ref @maybeCapability`, which is used to express * the maybe capability `ref?` as a type. diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index bbaf0c7d2fa0..0f43280d582a 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -30,9 +30,21 @@ trait CaptureRef extends TypeProxy, ValueType: /** Is this a reach reference of the form `x*`? */ final def isReach(using Context): Boolean = this match - case AnnotatedType(_, annot) => annot.symbol == defn.ReachCapabilityAnnot + case AnnotatedType(_, annot) => + annot.symbol == defn.ReachCapabilityAnnot || annot.symbol == defn.ReachUnderUseCapabilityAnnot case _ => false + final def isUnderUse(using Context): Boolean = this match + case AnnotatedType(_, annot) => annot.symbol == defn.ReachUnderUseCapabilityAnnot + case _ => false + + def toUnderUse(using Context): CaptureRef = + if isUnderUse then + this match + case _: AnnotatedType => stripReach.reach(underUse = true) + // TODO: Handle capture set variables here + else this + /** Is this a maybe reference of the form `x?`? */ final def isMaybe(using Context): Boolean = this match case AnnotatedType(_, annot) => annot.symbol == defn.MaybeCapabilityAnnot @@ -132,6 +144,7 @@ trait CaptureRef extends TypeProxy, ValueType: case _ => false || this.match case ReachCapability(x1) => x1.subsumes(y.stripReach) + case ReachUnderUseCapability(x1) => x1.subsumes(y.stripReach) case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y)) case x: TermParamRef => subsumesExistentially(x, y) case x: TypeRef => assumedContainsOf(x).contains(y) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 81b4287961ba..5e31b8c8aa11 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -517,6 +517,8 @@ object CaptureSet: elem.cls.ccLevel.nextInner <= level case ReachCapability(elem1) => levelOK(elem1) + case ReachUnderUseCapability(elem1) => + levelOK(elem1) case MaybeCapability(elem1) => levelOK(elem1) case _ => @@ -1066,6 +1068,8 @@ object CaptureSet: else CaptureSet.universal case ReachCapability(ref1) => deepCaptureSet(ref1.widen) .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt) + case ReachUnderUseCapability(ref1) => deepCaptureSet(ref1.widen) + .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt) case _ => ofType(ref.underlying, followResult = true) /** Capture set of a type */ @@ -1082,7 +1086,9 @@ object CaptureSet: empty case CapturingType(parent, refs) => recur(parent) ++ refs - case tp @ AnnotatedType(parent, ann) if ann.hasSymbol(defn.ReachCapabilityAnnot) => + case tp @ AnnotatedType(parent, ann) + if ann.hasSymbol(defn.ReachCapabilityAnnot) + || ann.hasSymbol(defn.ReachUnderUseCapabilityAnnot) => parent match case parent: SingletonCaptureRef if parent.isTrackableRef => tp.singletonCaptureSet diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 4d905a5df4ab..84ed67b9a8a2 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -402,7 +402,10 @@ class CheckCaptures extends Recheck, SymTransformer: && (!ccConfig.useSealed || refSym.is(Param)) && refOwner == env.owner then - if refSym.hasAnnotation(defn.UnboxAnnot) then + if refSym.hasAnnotation(defn.UnboxAnnot) + || ref.info.hasAnnotation(defn.UseAnnot) + || c.isUnderUse + then capt.println(i"exempt: $ref in $refOwner") else // Reach capabilities that go out of scope have to be approximated @@ -410,7 +413,8 @@ class CheckCaptures extends Recheck, SymTransformer: // Reach capabilities of @unboxed parameters are exempted. val cs = CaptureSet.ofInfo(c) cs.disallowRootCapability: () => - report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos) + def kind = if c.isReach then "reach capability" else "capture set variable" + report.error(em"Local $kind $c leaks into capture scope of ${env.ownerString}", pos) checkSubset(cs, env.captured, pos, provenance(env)) isVisible case ref: ThisType => isVisibleFromEnv(ref.cls, env) @@ -576,11 +580,38 @@ class CheckCaptures extends Recheck, SymTransformer: protected override def recheckArg(arg: Tree, formal: Type)(using Context): Type = val argType = recheck(arg, formal) + accountForUses(arg, argType, formal) if unboxedArgs.contains(arg) then capt.println(i"charging deep capture set of $arg: ${argType} = ${argType.deepCaptureSet}") markFree(argType.deepCaptureSet, arg.srcPos) argType + class MapUses(deep: Boolean)(using Context) extends TypeMap: + var usesFound = false + def apply(t: Type) = t match + case t @ AnnotatedType(parent, ann) => + if ann.symbol == defn.UseAnnot then + usesFound = true + defn.UseType.typeRef.appliedTo(apply(parent)) + else + t.derivedAnnotatedType(this(parent), ann) + case Existential(_, _) if !deep => + t + case _ => + mapOver(t) + + def accountForUses(arg: Tree, argType: Type, formal: Type)(using Context): Unit = + val mapper = MapUses(deep = false) + val formal1 = mapper(formal) + if mapper.usesFound then + def markUsesAsFree(cs: CaptureSet): Boolean = + capt.println(i"actual uses for $arg: $argType vs $formal = $cs") + markFree(cs, arg.srcPos) + true + CCState.withUseHandler(markUsesAsFree): + checkConformsExpr(argType, formal1, arg, NothingToAdd) + end accountForUses + /** A specialized implementation of the apply rule. * * E |- q: Tq^Cq @@ -1366,13 +1397,15 @@ class CheckCaptures extends Recheck, SymTransformer: * @param sym symbol of the field definition that is being checked */ override def checkSubType(actual: Type, expected: Type)(using Context): Boolean = - val expected1 = alignDependentFunction(addOuterRefs(expected, actual, srcPos), actual.stripCapturing) + val mapUses = MapUses(deep = true) + val expected1 = alignDependentFunction( + addOuterRefs(mapUses(expected), actual, srcPos), actual.stripCapturing) val actual1 = val saved = curEnv try curEnv = Env(clazz, EnvKind.NestedInOwner, capturedVars(clazz), outer0 = curEnv) val adapted = - adaptBoxed(actual, expected1, srcPos, covariant = true, alwaysConst = true, null) + adaptBoxed(mapUses(actual), expected1, srcPos, covariant = true, alwaysConst = true, null) actual match case _: MethodType => // We remove the capture set resulted from box adaptation for method types, @@ -1382,7 +1415,9 @@ class CheckCaptures extends Recheck, SymTransformer: adapted.stripCapturing case _ => adapted finally curEnv = saved - actual1 frozen_<:< expected1 + CCState.withUseHandler(Function.const(false)): + TypeComparer.usingContravarianceForMethods: + actual1 frozen_<:< expected1 override def needsCheck(overriding: Symbol, overridden: Symbol)(using Context): Boolean = !setup.isPreCC(overriding) && !setup.isPreCC(overridden) diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 76ae41649517..967ff9e827d9 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -212,8 +212,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: def apply(tp: Type) = val tp1 = tp match - case AnnotatedType(parent, annot) if annot.symbol.isRetains => - // Drop explicit retains annotations + case AnnotatedType(parent, annot) if annot.symbol.isRetains || annot.symbol == defn.UseAnnot => + // Drop inferred retains and @use annotations apply(parent) case tp @ AppliedType(tycon, args) => val tycon1 = this(tycon) diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index f95bb3cea351..dac51e5e8b1c 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -551,6 +551,17 @@ class Definitions { completeClass(enterCompleteClassSymbol( ScalaPackageClass, tpnme.maybeCapability, Final, List(StaticAnnotationClass.typeRef))) + /** A type `type [+T] <: T` used locally in capture checking. At certain points + * `T @use` types are converted to `[T]` types. These types are handled as + * compile-time applied types by TypeComparer. + */ + @tu lazy val UseType: TypeSymbol = + enterPermanentSymbol( + tpnme.USE, + TypeBounds.upper( + HKTypeLambda(HKTypeLambda.syntheticParamNames(1), Covariant :: Nil) + (_ => TypeBounds.empty :: Nil, _.paramRefs.head))).asType + @tu lazy val CollectionSeqType: TypeRef = requiredClassRef("scala.collection.Seq") @tu lazy val SeqType: TypeRef = requiredClassRef("scala.collection.immutable.Seq") @tu lazy val SeqModule: Symbol = requiredModule("scala.collection.immutable.Seq") @@ -1057,12 +1068,13 @@ class Definitions { @tu lazy val ExperimentalAnnot: ClassSymbol = requiredClass("scala.annotation.experimental") @tu lazy val ThrowsAnnot: ClassSymbol = requiredClass("scala.throws") @tu lazy val TransientAnnot: ClassSymbol = requiredClass("scala.transient") - @tu lazy val UnboxAnnot: ClassSymbol = requiredClass("scala.caps.unbox") + @tu lazy val UnboxAnnot: ClassSymbol = requiredClass("scala.caps.unbox") @tu lazy val UncheckedAnnot: ClassSymbol = requiredClass("scala.unchecked") @tu lazy val UncheckedStableAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedStable") @tu lazy val UncheckedVarianceAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedVariance") @tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures") @tu lazy val UntrackedCapturesAnnot: ClassSymbol = requiredClass("scala.caps.untrackedCaptures") + @tu lazy val UseAnnot: ClassSymbol = requiredClass("scala.caps.use") @tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile") @tu lazy val BeanGetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanGetter") @tu lazy val BeanSetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanSetter") @@ -1077,6 +1089,7 @@ class Definitions { @tu lazy val TargetNameAnnot: ClassSymbol = requiredClass("scala.annotation.targetName") @tu lazy val VarargsAnnot: ClassSymbol = requiredClass("scala.annotation.varargs") @tu lazy val ReachCapabilityAnnot = requiredClass("scala.annotation.internal.reachCapability") + @tu lazy val ReachUnderUseCapabilityAnnot = requiredClass("scala.annotation.internal.reachUnderUseCapability") @tu lazy val RequiresCapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.internal.requiresCapability") @tu lazy val RetainsAnnot: ClassSymbol = requiredClass("scala.annotation.retains") @tu lazy val RetainsCapAnnot: ClassSymbol = requiredClass("scala.annotation.retainsCap") @@ -1352,6 +1365,9 @@ class Definitions { final def isNamedTuple_From(sym: Symbol)(using Context): Boolean = sym.name == tpnme.From && sym.owner == NamedTupleModule.moduleClass + final def isUse(sym: Symbol)(using Context): Boolean = + sym.name == tpnme.USE && sym.owner == ScalaPackageClass + private val compiletimePackageAnyTypes: Set[Name] = Set( tpnme.Equals, tpnme.NotEquals, tpnme.IsConst, tpnme.ToString ) @@ -1380,7 +1396,7 @@ class Definitions { tpnme.Plus, tpnme.Length, tpnme.Substring, tpnme.Matches, tpnme.CharAt ) private val compiletimePackageOpTypes: Set[Name] = - Set(tpnme.S, tpnme.From) + Set(tpnme.S, tpnme.From, tpnme.USE) ++ compiletimePackageAnyTypes ++ compiletimePackageIntTypes ++ compiletimePackageLongTypes @@ -1394,6 +1410,7 @@ class Definitions { && ( isCompiletime_S(sym) || isNamedTuple_From(sym) + || isUse(sym) || sym.owner == CompiletimeOpsAnyModuleClass && compiletimePackageAnyTypes.contains(sym.name) || sym.owner == CompiletimeOpsIntModuleClass && compiletimePackageIntTypes.contains(sym.name) || sym.owner == CompiletimeOpsLongModuleClass && compiletimePackageLongTypes.contains(sym.name) @@ -2195,7 +2212,8 @@ class Definitions { NothingClass, SingletonClass, CBCompanion, - MaybeCapabilityAnnot) + MaybeCapabilityAnnot, + UseType) @tu lazy val syntheticCoreClasses: List[Symbol] = syntheticScalaClasses ++ List( EmptyPackageVal, diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala index d3e198a7e7a7..5bf75e95c4e9 100644 --- a/compiler/src/dotty/tools/dotc/core/StdNames.scala +++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala @@ -194,6 +194,7 @@ object StdNames { final val WILDCARD_STAR: N = "_*" final val REIFY_TREECREATOR_PREFIX: N = "$treecreator" final val REIFY_TYPECREATOR_PREFIX: N = "$typecreator" + final val USE: N = "" final val Any: N = "Any" final val AnyKind: N = "AnyKind" diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 8fc6307c426c..43e9c081af8b 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -51,6 +51,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling assocExistentials = Nil recCount = 0 needsGc = false + useContravariance = false if Config.checkTypeComparerReset then checkReset() private var pendingSubTypes: util.MutableSet[(Type, Type)] | Null = null @@ -79,6 +80,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling */ private var assocExistentials: ExAssoc = Nil + /** Whether method type parameters should be compared contra-variantly. + * This is usually false, but set to true for comparisons of methods in + * refinements and for override checks in capture checking. + */ + private var useContravariance = false + private var myInstance: TypeComparer = this def currentInstance: TypeComparer = myInstance @@ -667,7 +674,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling info1.paramNames.hasSameLengthAs(info2.paramNames) && isSubInfo(info1.resultType, info2.resultType.subst(info2, info1)) case (info1: MethodType, info2: MethodType) => - matchingMethodParams(info1, info2, precise = false) + usingContravarianceForMethods(matchingMethodParams(info1, info2)) && isSubInfo(info1.resultType, info2.resultType.subst(info2, info1)) case (info1 @ CapturingType(parent1, refs1), info2: Type) if info2.stripCapturing.isInstanceOf[MethodOrPoly] => @@ -1527,13 +1534,15 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling * with `other` via ">:>" if fromBelow is true, "<:<" otherwise. * Delegates to compareS if `tycon` is scala.compiletime.S. Otherwise, constant folds if possible. */ - def compareCompiletimeAppliedType(tp: AppliedType, other: Type, fromBelow: Boolean): Boolean = { - if (defn.isCompiletime_S(tp.tycon.typeSymbol)) compareS(tp, other, fromBelow) - else { + def compareCompiletimeAppliedType(tp: AppliedType, other: Type, fromBelow: Boolean): Boolean = + val tycon = tp.tycon.typeSymbol + if defn.isCompiletime_S(tycon) then + compareS(tp, other, fromBelow) + else if defn.isUse(tycon) && fromBelow then + CCState.recordUse(other.deepCaptureSet) && recur(other, tp.args.head) + else val folded = tp.tryCompiletimeConstantFold if (fromBelow) recur(other, folded) else recur(folded, other) - } - } /** Like tp1 <:< tp2, but returns false immediately if we know that * the case was covered previously during subtyping. @@ -2154,7 +2163,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling info1 match case info1: MethodType => val symInfo1 = symInfo.stripPoly - matchingMethodParams(info1, info2, precise = false) + usingContravarianceForMethods(matchingMethodParams(info1, info2)) && isSubInfo(info1.resultType, info2.resultType.subst(info2, info1), symInfo1.resultType) && sigsOK(symInfo1, info2) case _ => inFrozenGadtIf(tp1IsSingleton) { isSubType(info1, info2) } @@ -2277,18 +2286,18 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling } /** Do the parameter types of `tp1` and `tp2` match in a way that allows `tp1` - * to override `tp2` ? Two modes: precise or not. - * If `precise` is set (which is the default) this is the case if they're pairwise `=:=`. - * Otherwise parameters in `tp2` must be subtypes of corresponding parameters in `tp1`. + * to override `tp2` ? Two modes, dependenging on `useContravariance`. + * If `useContravariance` is off (which is the default) this is the case if they're pairwise `=:=`. + * If `useContravariance` is on, parameters in `tp2` must be subtypes of corresponding parameters in `tp1`. */ - def matchingMethodParams(tp1: MethodType, tp2: MethodType, precise: Boolean = true): Boolean = { + def matchingMethodParams(tp1: MethodType, tp2: MethodType): Boolean = { def loop(formals1: List[Type], formals2: List[Type]): Boolean = formals1 match { case formal1 :: rest1 => formals2 match { case formal2 :: rest2 => val formal2a = if (tp2.isParamDependent) formal2.subst(tp2, tp1) else formal2 val paramsMatch = - if precise then + if !useContravariance then isSameTypeWhenFrozen(formal1, formal2a) else if isCaptureCheckingOrSetup then // allow to constrain capture set variables @@ -2907,6 +2916,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling (tp1.isBoxedCapturing == tp2.isBoxedCapturing) || refs1.subCaptures(CaptureSet.empty, frozenConstraint).isOK + protected def usingContravarianceForMethods[T](op: => T)(using Context) = + val saved = useContravariance + useContravariance = true + try op finally useContravariance = saved + // ----------- Diagnostics -------------------------------------------------- /** A hook for showing subtype traces. Overridden in ExplainingTypeComparer */ @@ -3452,6 +3466,9 @@ object TypeComparer { def subsumesExistentially(tp1: TermParamRef, tp2: CaptureRef)(using Context) = comparing(_.subsumesExistentially(tp1, tp2)) + + def usingContravarianceForMethods[T](op: => T)(using Context) = + comparing(_.usingContravarianceForMethods(op)) } object MatchReducer: diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala index b5ed3bdb4fa7..a3913c699a3d 100644 --- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -15,7 +15,7 @@ import util.SourcePosition import scala.util.control.NonFatal import scala.annotation.switch import config.{Config, Feature} -import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, MaybeCapability, isBoxed, retainedElems, isRetainsLike} +import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, ReachUnderUseCapability, MaybeCapability, isBoxed, retainedElems, isRetainsLike} class PlainPrinter(_ctx: Context) extends Printer { @@ -418,6 +418,7 @@ class PlainPrinter(_ctx: Context) extends Printer { case tp: SingletonType => toTextRef(tp) case tp: (TypeRef | TypeParamRef) => toText(tp) ~ "^" case ReachCapability(tp1) => toTextCaptureRef(tp1) ~ "*" + case ReachUnderUseCapability(tp1) => toTextCaptureRef(tp1) ~ "*@use" case MaybeCapability(tp1) => toTextCaptureRef(tp1) ~ "?" case tp => toText(tp) diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala index ea729e9549d5..6f499656396e 100644 --- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala @@ -27,7 +27,7 @@ import config.{Config, Feature} import dotty.tools.dotc.util.SourcePosition import dotty.tools.dotc.ast.untpd.{MemberDef, Modifiers, PackageDef, RefTree, Template, TypeDef, ValOrDefDef} -import cc.{CaptureSet, CapturingType, toCaptureSet, IllegalCaptureRef, isRetains, ReachCapability, MaybeCapability} +import cc.* import dotty.tools.dotc.parsing.JavaParsers class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { @@ -330,7 +330,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { "?" ~ (("(ignored: " ~ toText(ignored) ~ ")") provided printDebug) case tp @ PolyProto(targs, resType) => "[applied to [" ~ toTextGlobal(targs, ", ") ~ "] returning " ~ toText(resType) - case ReachCapability(_) | MaybeCapability(_) => + case ReachCapability(_) | ReachUnderUseCapability(_) | MaybeCapability(_) => toTextCaptureRef(tp) case _ => super.toText(tp) diff --git a/library/src/scala/annotation/internal/reachUnderUseCapability.scala b/library/src/scala/annotation/internal/reachUnderUseCapability.scala new file mode 100644 index 000000000000..6c07be66adc5 --- /dev/null +++ b/library/src/scala/annotation/internal/reachUnderUseCapability.scala @@ -0,0 +1,9 @@ +package scala.annotation +package internal + +/** An annotation that marks a capture ref as a reach capability occurring + * under a @use part of a parameter type. + * Example: When it occurs in `C[x* @use]`, `x*` is encoded as + * `x.type @reachUnderuseCapability` + */ +class reachUnderUseCapability extends StaticAnnotation diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala index 9911ef920116..c8ea94160ea9 100644 --- a/library/src/scala/caps.scala +++ b/library/src/scala/caps.scala @@ -56,6 +56,7 @@ import annotation.{experimental, compileTimeOnly, retainsCap} * can experiment with it quickly between minor releases */ final class unbox extends annotation.StaticAnnotation + final class use extends annotation.StaticAnnotation object unsafe: diff --git a/tests/neg-custom-args/captures/i15749a.scala b/tests/neg-custom-args/captures/i15749a.scala index 57fca27fae66..a620bd1d7c0c 100644 --- a/tests/neg-custom-args/captures/i15749a.scala +++ b/tests/neg-custom-args/captures/i15749a.scala @@ -1,5 +1,5 @@ import caps.cap -import caps.unbox +import caps.use class Unit object u extends Unit @@ -18,7 +18,7 @@ def test = def force[A](thunk: Unit ->{cap} A): A = thunk(u) - def forceWrapper[A](@unbox mx: Wrapper[Unit ->{cap} A]): Wrapper[A] = + def forceWrapper[A](mx: Wrapper[Unit ->{cap} A] @use): Wrapper[A] = // Γ ⊢ mx: Wrapper[□ {cap} Unit => A] // `force` should be typed as ∀(□ {cap} Unit -> A) A, but it can not strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // error // should work diff --git a/tests/neg-custom-args/captures/i21347.check b/tests/neg-custom-args/captures/i21347.check index c680a54d3efc..0d9ed6993d3e 100644 --- a/tests/neg-custom-args/captures/i21347.check +++ b/tests/neg-custom-args/captures/i21347.check @@ -1,7 +1,7 @@ -- Error: tests/neg-custom-args/captures/i21347.scala:4:15 ------------------------------------------------------------- 4 | ops.foreach: op => // error | ^ - | Local reach capability C leaks into capture scope of method runOps + | Local capture set variable C leaks into capture scope of method runOps 5 | op() -- Error: tests/neg-custom-args/captures/i21347.scala:8:14 ------------------------------------------------------------- 8 | () => runOps(f :: Nil) // error diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check index 14b468db4c8e..af6ddee624b6 100644 --- a/tests/neg-custom-args/captures/i21614.check +++ b/tests/neg-custom-args/captures/i21614.check @@ -8,7 +8,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:12 --------------------------------------- 12 | files.map(new Logger(_)) // error, Q: can we improve the error message? | ^^^^^^^^^^^^^ - | Found: Logger{val f: (_$1 : File^{files*})}^ + | Found: Logger{val f: (_$1 : File^{files*@use})}^ | Required: Logger{val f: File^?}^? | | Note that the universal capability `cap` diff --git a/tests/neg-custom-args/captures/i21614.scala b/tests/neg-custom-args/captures/i21614.scala index a5ed25d818a5..333c9368629e 100644 --- a/tests/neg-custom-args/captures/i21614.scala +++ b/tests/neg-custom-args/captures/i21614.scala @@ -1,12 +1,12 @@ import language.experimental.captureChecking import caps.Capability -import caps.unbox +import caps.use trait File extends Capability class Logger(f: File^) extends Capability // <- will work if we remove the extends clause -def mkLoggers1[F <: File^](@unbox files: List[F]): List[Logger^] = +def mkLoggers1[F <: File^](files: List[F @use]): List[Logger^] = files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)? -def mkLoggers2(@unbox files: List[File^]): List[Logger^] = +def mkLoggers2(files: List[File^ @use]): List[Logger^] = files.map(new Logger(_)) // error, Q: can we improve the error message? diff --git a/tests/neg-custom-args/captures/leak-problem-2.scala b/tests/neg-custom-args/captures/leak-problem-2.scala index 08a3a6c2d9ca..7c1b6e31d60c 100644 --- a/tests/neg-custom-args/captures/leak-problem-2.scala +++ b/tests/neg-custom-args/captures/leak-problem-2.scala @@ -2,7 +2,7 @@ import language.experimental.captureChecking trait Source[+T] -def race[T](@caps.unbox sources: Seq[Source[T]^]): Source[T]^{sources*} = ??? +def race[T](sources: Seq[Source[T]^ @caps.use]): Source[T]^{sources*} = ??? def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{} = race(Seq(src1, src2)) // error diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala index c33ba80a668b..3ddddcc35e9b 100644 --- a/tests/neg-custom-args/captures/reaches.scala +++ b/tests/neg-custom-args/captures/reaches.scala @@ -1,4 +1,4 @@ -import caps.unbox +import caps.use class File: def write(): Unit = ??? @@ -11,7 +11,7 @@ class Ref[T](init: T): def get: T = x def set(y: T) = { x = y } -def runAll0(@unbox xs: List[Proc]): Unit = +def runAll0(xs: List[Proc] @use): Unit = var cur: List[() ->{xs*} Unit] = xs while cur.nonEmpty do val next: () ->{xs*} Unit = cur.head @@ -21,7 +21,7 @@ def runAll0(@unbox xs: List[Proc]): Unit = usingFile: f => cur = (() => f.write()) :: Nil // error -def runAll1(@unbox xs: List[Proc]): Unit = +def runAll1(xs: List[Proc] @use): Unit = val cur = Ref[List[() ->{xs*} Unit]](xs) // OK, by revised VAR while cur.get.nonEmpty do val next: () ->{xs*} Unit = cur.get.head @@ -78,5 +78,5 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C = def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] = ps.map((x, y) => compose1(x, y)) // error // error -def mapCompose2[A](@unbox ps: List[(A => A, A => A)]): List[A ->{ps*} A] = +def mapCompose2[A](ps: List[(A => A, A => A)] @use): List[A ->{ps*} A] = ps.map((x, y) => compose1(x, y)) diff --git a/tests/neg-custom-args/captures/unbox-overrides.check b/tests/neg-custom-args/captures/unbox-overrides.check index b9a3be7bffbc..404475fae2a8 100644 --- a/tests/neg-custom-args/captures/unbox-overrides.check +++ b/tests/neg-custom-args/captures/unbox-overrides.check @@ -1,21 +1,28 @@ --- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:8:6 ---------------------------------- -8 | def foo(x: C): C // error - | ^ - |error overriding method foo in trait A of type (x: C): C; - | method foo of type (x: C): C has a parameter x with different @unbox status than the corresponding parameter in the overridden definition - | - | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:9:6 ---------------------------------- -9 | def bar(@unbox x: C): C // error +9 | def bar(x: C @use): C // error | ^ - |error overriding method bar in trait A of type (x: C): C; - | method bar of type (x: C): C has a parameter x with different @unbox status than the corresponding parameter in the overridden definition + | error overriding method bar in trait A of type (x: C): C; + | method bar of type (x: C @use): C has incompatible type | | longer explanation available when compiling with `-explain` --- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:15:15 -------------------------------- -15 |abstract class C extends A[C], B2 // error +-- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:16:6 --------------------------------- +16 | def foo(x: C @use): C // error + | ^ + | error overriding method foo in trait B2 of type (x: C): C; + | method foo of type (x: C @use): C has incompatible type + | + | longer explanation available when compiling with `-explain` +-- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:19:15 -------------------------------- +19 |abstract class C extends A[C], B2 // error | ^ - |error overriding method foo in trait A of type (x: C): C; - | method foo in trait B2 of type (x: C): C has a parameter x with different @unbox status than the corresponding parameter in the overridden definition + | error overriding method bar in trait A of type (x: C): C; + | method bar in trait B2 of type (x: C @use): C has incompatible type + | + | longer explanation available when compiling with `-explain` +-- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:26:6 --------------------------------- +26 | def foo[T](a: Int)(x: C @use): C // error + | ^ + | error overriding method foo in trait Poly of type [T](a: Int)(x: C): C; + | method foo of type [T](a: Int)(x: C @use): C has incompatible type | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/unbox-overrides.scala b/tests/neg-custom-args/captures/unbox-overrides.scala index 5abb5013bfbe..757133f8b115 100644 --- a/tests/neg-custom-args/captures/unbox-overrides.scala +++ b/tests/neg-custom-args/captures/unbox-overrides.scala @@ -1,15 +1,27 @@ -import caps.unbox +import caps.use trait A[X]: - def foo(@unbox x: X): X + def foo(x: X @use): X def bar(x: X): X trait B extends A[C]: - def foo(x: C): C // error - def bar(@unbox x: C): C // error + def foo(x: C): C // ok + def bar(x: C @use): C // error trait B2: def foo(x: C): C - def bar(@unbox x: C): C + def bar(x: C @use): C + +trait B3 extends B2: + def foo(x: C @use): C // error + def bar(x: C): C // ok abstract class C extends A[C], B2 // error + +trait Poly: + def foo[T](a: Int)(x: C): C + def bar[T](a: Int)(x: C @use): C + +trait Poly1 extends Poly: + def foo[T](a: Int)(x: C @use): C // error + def bar[T](a: Int)(x: C): C // ok diff --git a/tests/neg-custom-args/captures/useAnnot.check b/tests/neg-custom-args/captures/useAnnot.check new file mode 100644 index 000000000000..271a776e091a --- /dev/null +++ b/tests/neg-custom-args/captures/useAnnot.check @@ -0,0 +1,4 @@ +-- Error: tests/neg-custom-args/captures/useAnnot.scala:13:26 ---------------------------------------------------------- +13 | val _ = () => println(f(ioProcs)) // error + | ^^^^^^^ + | Local reach capability ioProcs* leaks into capture scope of method Test2 diff --git a/tests/neg-custom-args/captures/useAnnot.scala b/tests/neg-custom-args/captures/useAnnot.scala new file mode 100644 index 000000000000..deb0839bdbd3 --- /dev/null +++ b/tests/neg-custom-args/captures/useAnnot.scala @@ -0,0 +1,16 @@ +import caps.use + +type Proc = () => Unit + +def f(xs: List[Proc] @use) = ??? +def g(xs: List[Proc]) = ??? + +def Test(ioProcs: List[Proc @use]) = + val ff = () => println(f(ioProcs)) // ok + () + +def Test2(ioProcs: List[Proc]) = + val _ = () => println(f(ioProcs)) // error + val gg = () => println(g(ioProcs)) // ok + () + diff --git a/tests/neg/i20503.scala b/tests/neg/i20503.scala index 3fb0573f6c2f..562aea94e0f6 100644 --- a/tests/neg/i20503.scala +++ b/tests/neg/i20503.scala @@ -1,5 +1,5 @@ import language.experimental.captureChecking -import caps.unbox +import caps.use class List[+A]: def head: A = ??? @@ -8,7 +8,7 @@ class List[+A]: def foreach[U](f: A => U): Unit = ??? def nonEmpty: Boolean = ??? -def runOps(@unbox ops: List[() => Unit]): Unit = +def runOps(ops: List[(() => Unit) @use]): Unit = // See i20156, due to limitation in expressiveness of current system, // we could map over the list of impure elements. OK with existentials. ops.foreach(op => op()) diff --git a/tests/neg/leak-problem-unboxed.scala b/tests/neg/leak-problem-unboxed.scala index 7de3d84bfcca..f03a6b16ab10 100644 --- a/tests/neg/leak-problem-unboxed.scala +++ b/tests/neg/leak-problem-unboxed.scala @@ -1,5 +1,5 @@ import language.experimental.captureChecking -import caps.unbox +import caps.use // Some capabilities that should be used locally trait Async: @@ -9,20 +9,21 @@ def usingAsync[X](op: Async^ => X): X = ??? case class Box[+T](get: T) -def useBoxedAsync(@unbox x: Box[Async^]): Unit = +def useBoxedAsync(x: Box[Async^ @use]): Unit = val t0 = x val t1 = t0.get // ok t1.read() -def useBoxedAsync1(@unbox x: Box[Async^]): Unit = x.get.read() // ok +def useBoxedAsync1(x: Box[Async^ @use]): Unit = x.get.read() // ok def test(): Unit = val f: Box[Async^] => Unit = (x: Box[Async^]) => useBoxedAsync(x) // error val _: Box[Async^] => Unit = useBoxedAsync(_) // error val _: Box[Async^] => Unit = useBoxedAsync // error - val _ = useBoxedAsync(_) // error - val _ = useBoxedAsync // error + val _ = (x: Box[Async^]) => useBoxedAsync(x) // error + val _ = useBoxedAsync(_) // was error, now OK since @use is inferred + val _ = useBoxedAsync // was error, now OK since @use is inferred def boom(x: Async^): () ->{f} Unit = () => f(Box(x)) diff --git a/tests/pos-custom-args/captures/curried-uses.scala b/tests/pos-custom-args/captures/curried-uses.scala new file mode 100644 index 000000000000..3e2b5378f845 --- /dev/null +++ b/tests/pos-custom-args/captures/curried-uses.scala @@ -0,0 +1,9 @@ + +def test() = + val f: () => () => Unit = ??? + val x = () => + val z1: () => Unit = f() + val z2 = z1() + z2 + val _: () ->{f} Unit = x + () From 1391da7b9859d12eea255ed11d6598d39d24889e Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 9 Oct 2024 11:53:03 +0200 Subject: [PATCH 11/13] Drop @unbox Convert remaining occurrences in tests to @use --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 102 ++++-------------- .../dotty/tools/dotc/core/Definitions.scala | 3 +- .../src/dotty/tools/dotc/core/Types.scala | 2 +- library/src/scala/caps.scala | 1 - .../captures/spread-problem.scala | 2 +- tests/pos-custom-args/captures/Buffer.scala | 4 +- .../pos-custom-args/captures/dep-reach.scala | 6 +- tests/pos-custom-args/captures/reaches.scala | 4 +- tests/pos/Buffer.scala | 22 ---- tests/pos/cc-poly-source-capability.scala | 4 +- tests/pos/cc-poly-source.scala | 4 +- tests/pos/gears-probem-1.scala | 4 +- tests/pos/i18699.scala | 4 +- tests/pos/reach-capability.scala | 4 +- tests/pos/reach-problem.scala | 4 +- 15 files changed, 44 insertions(+), 126 deletions(-) delete mode 100644 tests/pos/Buffer.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 84ed67b9a8a2..4bbcd9f31dce 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -402,15 +402,16 @@ class CheckCaptures extends Recheck, SymTransformer: && (!ccConfig.useSealed || refSym.is(Param)) && refOwner == env.owner then - if refSym.hasAnnotation(defn.UnboxAnnot) - || ref.info.hasAnnotation(defn.UseAnnot) - || c.isUnderUse - then + if ref.info.hasAnnotation(defn.UseAnnot)|| c.isUnderUse then capt.println(i"exempt: $ref in $refOwner") else // Reach capabilities that go out of scope have to be approximated // by their underlying capture set, which cannot be universal. - // Reach capabilities of @unboxed parameters are exempted. + // Reach capabilities are exempted if + // - they are under-use capabilties that were generated from a cap + // appearing under a @use, or + // - their reference has a type thar carries a @use annotation. In that + // case callers will charge the deep capture set of the argument. val cs = CaptureSet.ofInfo(c) cs.disallowRootCapability: () => def kind = if c.isReach then "reach capability" else "capture set variable" @@ -428,48 +429,14 @@ class CheckCaptures extends Recheck, SymTransformer: end markFree /** Include references captured by the called method in the current environment stack */ - def includeCallCaptures(sym: Symbol, pos: SrcPos)(using Context): Unit = - if sym.exists && curEnv.isOpen then markFree(capturedVars(sym), pos) - - private val prefixCalls = util.EqHashSet[GenericApply]() - private val unboxedArgs = util.EqHashSet[Tree]() - - def handleCall(meth: Symbol, call: GenericApply, eval: () => Type)(using Context): Type = - if prefixCalls.remove(call) then return eval() - - val unboxedParamNames = - meth.rawParamss.flatMap: params => - params.collect: - case param if param.hasAnnotation(defn.UnboxAnnot) => - param.name - .toSet - - def markUnboxedArgs(call: GenericApply): Unit = call.fun.tpe.widen match - case MethodType(pnames) => - for (pname, arg) <- pnames.lazyZip(call.args) do - if unboxedParamNames.contains(pname) then - unboxedArgs.add(arg) - case _ => - - def markPrefixCalls(tree: Tree): Unit = tree match - case tree: GenericApply => - prefixCalls.add(tree) - markUnboxedArgs(tree) - markPrefixCalls(tree.fun) - case _ => - - markUnboxedArgs(call) - markPrefixCalls(call.fun) - val res = eval() - includeCallCaptures(meth, call.srcPos) - res - end handleCall + def includeCallCaptures(sym: Symbol, resType: Type, pos: SrcPos)(using Context): Unit = resType match + case _: MethodOrPoly => // wait until method is fully applied + case _ => + if sym.exists && curEnv.isOpen then markFree(capturedVars(sym), pos) override def recheckIdent(tree: Ident, pt: Type)(using Context): Type = if tree.symbol.is(Method) then - if tree.symbol.info.isParameterless then - // there won't be an apply; need to include call captures now - includeCallCaptures(tree.symbol, tree.srcPos) + includeCallCaptures(tree.symbol, tree.symbol.info, tree.srcPos) else if !tree.symbol.isStatic then //debugShowEnvs() def addSelects(ref: TermRef, pt: Type): TermRef = pt match @@ -574,16 +541,15 @@ class CheckCaptures extends Recheck, SymTransformer: tp.derivedCapturingType(forceBox(parent), refs) mapArgUsing(forceBox) else - handleCall(meth, tree, () => super.recheckApply(tree, pt)) + val res = super.recheckApply(tree, pt) + includeCallCaptures(meth, res, tree.srcPos) + res end recheckApply protected override def recheckArg(arg: Tree, formal: Type)(using Context): Type = val argType = recheck(arg, formal) accountForUses(arg, argType, formal) - if unboxedArgs.contains(arg) then - capt.println(i"charging deep capture set of $arg: ${argType} = ${argType.deepCaptureSet}") - markFree(argType.deepCaptureSet, arg.srcPos) argType class MapUses(deep: Boolean)(using Context) extends TypeMap: @@ -620,15 +586,10 @@ class CheckCaptures extends Recheck, SymTransformer: * --------------------- * E |- f(a): Tr^C * - * If the function `f` does not have an `@unboxed` parameter, then - * any unboxing it does would be charged to the environment of the function - * so they have to appear in Cq. Since any capabilities of the result of the - * application must already be present in the application, an upper - * approximation of the result capture set is Cq \union Ca, where `Ca` - * is the capture set of the argument. - * If the function `f` does have an `@unboxed` parameter, then it could in addition - * unbox reach capabilities over its formal parameter. Therefore, the approximation - * would be `Cq \union dcs(Ca)` instead. + * If the type of the function `f` does not mention any formal parameters + * any capabilities of the result of the application must already be present in + * the application. So an upper approximation of the result capture set is Cq \union Ca, + * where `Ca` is the capture set of the argument. * If the approximation is known to subcapture the declared result Cr, we pick it for C * otherwise we pick Cr. */ @@ -636,11 +597,7 @@ class CheckCaptures extends Recheck, SymTransformer: def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type = val appType = Existential.toCap(super.recheckApplication(tree, qualType, funType, argTypes)) val qualCaptures = qualType.captureSet - val argCaptures = - for (arg, argType) <- tree.args.lazyZip(argTypes) yield - if unboxedArgs.remove(arg) // need to ensure the remove happens, that's why argCaptures is computed even if not needed. - then argType.deepCaptureSet - else argType.captureSet + val argCaptures = argTypes.map(_.captureSet) appType match case appType @ CapturingType(appType1, refs) if qualType.exists @@ -735,8 +692,10 @@ class CheckCaptures extends Recheck, SymTransformer: i"Sealed type variable $pname", "be instantiated to", i"This is often caused by a local capability$where\nleaking as part of its result.", tree.srcPos) - try handleCall(meth, tree, () => Existential.toCap(super.recheckTypeApply(tree, pt))) - finally checkContains(tree) + val res = Existential.toCap(super.recheckTypeApply(tree, pt)) + includeCallCaptures(meth, res, tree.srcPos) + checkContains(tree) + res end recheckTypeApply /** Faced with a tree of form `caps.contansImpl[CS, r.type]`, check that `R` is a tracked @@ -1423,21 +1382,6 @@ class CheckCaptures extends Recheck, SymTransformer: !setup.isPreCC(overriding) && !setup.isPreCC(overridden) override def checkInheritedTraitParameters: Boolean = false - - /** Check that overrides don't change the @unbox status of their parameters */ - override def additionalChecks(member: Symbol, other: Symbol)(using Context): Unit = - for - (params1, params2) <- member.rawParamss.lazyZip(other.rawParamss) - (param1, param2) <- params1.lazyZip(params2) - do - if param1.hasAnnotation(defn.UnboxAnnot) != param2.hasAnnotation(defn.UnboxAnnot) then - report.error( - OverrideError( - i"has a parameter ${param1.name} with different @unbox status than the corresponding parameter in the overridden definition", - self, member, other, self.memberInfo(member), self.memberInfo(other) - ), - if member.owner == clazz then member.srcPos else clazz.srcPos - ) end OverridingPairsCheckerCC def traverse(t: Tree)(using Context) = diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index dac51e5e8b1c..15f067db1df2 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -552,7 +552,7 @@ class Definitions { ScalaPackageClass, tpnme.maybeCapability, Final, List(StaticAnnotationClass.typeRef))) /** A type `type [+T] <: T` used locally in capture checking. At certain points - * `T @use` types are converted to `[T]` types. These types are handled as + * `T @use` types are converted to `[T]` types. These types are handled as * compile-time applied types by TypeComparer. */ @tu lazy val UseType: TypeSymbol = @@ -1068,7 +1068,6 @@ class Definitions { @tu lazy val ExperimentalAnnot: ClassSymbol = requiredClass("scala.annotation.experimental") @tu lazy val ThrowsAnnot: ClassSymbol = requiredClass("scala.throws") @tu lazy val TransientAnnot: ClassSymbol = requiredClass("scala.transient") - @tu lazy val UnboxAnnot: ClassSymbol = requiredClass("scala.caps.unbox") @tu lazy val UncheckedAnnot: ClassSymbol = requiredClass("scala.unchecked") @tu lazy val UncheckedStableAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedStable") @tu lazy val UncheckedVarianceAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedVariance") diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index aba8c3bb31fd..60bac8221e1d 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -1796,7 +1796,7 @@ object Types extends TypeUtils { /** Is this either not a method at all, or a parameterless method? */ final def isParameterless(using Context): Boolean = stripPoly match { - case mt: MethodType => false + case mt: MethodOrPoly => false case _ => true } diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala index c8ea94160ea9..6c7610e410c0 100644 --- a/library/src/scala/caps.scala +++ b/library/src/scala/caps.scala @@ -55,7 +55,6 @@ import annotation.{experimental, compileTimeOnly, retainsCap} /** This should go into annotations. For now it is here, so that we * can experiment with it quickly between minor releases */ - final class unbox extends annotation.StaticAnnotation final class use extends annotation.StaticAnnotation object unsafe: diff --git a/tests/neg-custom-args/captures/spread-problem.scala b/tests/neg-custom-args/captures/spread-problem.scala index 579c7817b9c1..92b1cb86c99d 100644 --- a/tests/neg-custom-args/captures/spread-problem.scala +++ b/tests/neg-custom-args/captures/spread-problem.scala @@ -2,7 +2,7 @@ import language.experimental.captureChecking trait Source[+T] -def race[T](@caps.unbox sources: (Source[T]^)*): Source[T]^{sources*} = ??? +def race[T](sources: (Source[T]^ @caps.use)*): Source[T]^{sources*} = ??? def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{} = race(Seq(src1, src2)*) // error diff --git a/tests/pos-custom-args/captures/Buffer.scala b/tests/pos-custom-args/captures/Buffer.scala index 2412e5b388ca..a5f4bd6657e3 100644 --- a/tests/pos-custom-args/captures/Buffer.scala +++ b/tests/pos-custom-args/captures/Buffer.scala @@ -8,10 +8,8 @@ trait Buffer[A]: def flatMapInPlace(f: A => IterableOnce[A]^): this.type = { val g = f val s = 10 - // capture checking: we need the copy since we box/unbox on g* on the next line + // capture checking: we need the copy since we box/unbox on g* on the next line // TODO: This looks fishy, need to investigate - // Alternative would be to mark `f` as @unbox. It's not inferred - // since `^ appears in a function result, not under a box. val newElems = new Array[(IterableOnce[A]^{f})](s) var i = 0 while i < s do diff --git a/tests/pos-custom-args/captures/dep-reach.scala b/tests/pos-custom-args/captures/dep-reach.scala index c81197aa738d..b84ed2113b26 100644 --- a/tests/pos-custom-args/captures/dep-reach.scala +++ b/tests/pos-custom-args/captures/dep-reach.scala @@ -1,10 +1,10 @@ -import caps.unbox +import caps.use object Test: class C type Proc = () => Unit def f(c: C^, d: C^): () ->{c, d} Unit = - def foo(@unbox xs: Proc*): () ->{xs*} Unit = + def foo(xs: Proc @use *): () ->{xs*} Unit = xs.head val a: () ->{c} Unit = () => () val b: () ->{d} Unit = () => () @@ -13,7 +13,7 @@ object Test: def g(c: C^, d: C^): () ->{c, d} Unit = - def foo(@unbox xs: Seq[() => Unit]): () ->{xs*} Unit = + def foo(xs: Seq[(() => Unit) @use]): () ->{xs*} Unit = xs.head val a: () ->{c} Unit = () => () diff --git a/tests/pos-custom-args/captures/reaches.scala b/tests/pos-custom-args/captures/reaches.scala index ab0da9b67d18..8e21a1f2edd6 100644 --- a/tests/pos-custom-args/captures/reaches.scala +++ b/tests/pos-custom-args/captures/reaches.scala @@ -1,4 +1,4 @@ -import caps.unbox +import caps.use class C def f(xs: List[C^]) = @@ -22,7 +22,7 @@ extension [A](x: A) def :: (xs: List[A]): List[A] = ??? object Nil extends List[Nothing] -def runAll(@unbox xs: List[Proc]): Unit = +def runAll(xs: List[Proc] @use): Unit = var cur: List[() ->{xs*} Unit] = xs // OK, by revised VAR while cur.nonEmpty do val next: () ->{xs*} Unit = cur.head diff --git a/tests/pos/Buffer.scala b/tests/pos/Buffer.scala deleted file mode 100644 index 2412e5b388ca..000000000000 --- a/tests/pos/Buffer.scala +++ /dev/null @@ -1,22 +0,0 @@ -import language.experimental.captureChecking - -// Extract of the problem in collection.mutable.Buffers -trait Buffer[A]: - - def apply(i: Int): A = ??? - - def flatMapInPlace(f: A => IterableOnce[A]^): this.type = { - val g = f - val s = 10 - // capture checking: we need the copy since we box/unbox on g* on the next line - // TODO: This looks fishy, need to investigate - // Alternative would be to mark `f` as @unbox. It's not inferred - // since `^ appears in a function result, not under a box. - val newElems = new Array[(IterableOnce[A]^{f})](s) - var i = 0 - while i < s do - val x = g(this(i)) - newElems(i) = x - i += 1 - this - } \ No newline at end of file diff --git a/tests/pos/cc-poly-source-capability.scala b/tests/pos/cc-poly-source-capability.scala index 3b6c0bde1398..0ecea7a7932f 100644 --- a/tests/pos/cc-poly-source-capability.scala +++ b/tests/pos/cc-poly-source-capability.scala @@ -1,7 +1,7 @@ import language.experimental.captureChecking import annotation.experimental import caps.{CapSet, Capability} -import caps.unbox +import caps.use @experimental object Test: @@ -18,7 +18,7 @@ import caps.unbox def allListeners: Set[Listener^{X^}] = listeners - def test1(async1: Async, @unbox others: List[Async]) = + def test1(async1: Async, others: List[Async @use]) = val src = Source[CapSet^{async1, others*}] val lst1 = listener(async1) val lsts = others.map(listener) diff --git a/tests/pos/cc-poly-source.scala b/tests/pos/cc-poly-source.scala index 4cfbbaa06936..aa516afea910 100644 --- a/tests/pos/cc-poly-source.scala +++ b/tests/pos/cc-poly-source.scala @@ -1,7 +1,7 @@ import language.experimental.captureChecking import annotation.experimental import caps.{CapSet, Capability} -import caps.unbox +import caps.use @experimental object Test: @@ -25,7 +25,7 @@ import caps.unbox val ls = src.allListeners val _: Set[Listener^{lbl1, lbl2}] = ls - def test2(@unbox lbls: List[Label^]) = + def test2(lbls: List[Label^ @use]) = def makeListener(lbl: Label^): Listener^{lbl} = ??? val listeners = lbls.map(makeListener) val src = Source[CapSet^{lbls*}] diff --git a/tests/pos/gears-probem-1.scala b/tests/pos/gears-probem-1.scala index ab71616b72fc..45a6a8234737 100644 --- a/tests/pos/gears-probem-1.scala +++ b/tests/pos/gears-probem-1.scala @@ -1,5 +1,5 @@ import language.experimental.captureChecking -import caps.unbox +import caps.use trait Future[+T]: def await: T @@ -17,7 +17,7 @@ class Result[+T, +E]: case class Err[+E](e: E) extends Result[Nothing, E] case class Ok[+T](x: T) extends Result[T, Nothing] -extension [T](@unbox fs: Seq[Future[T]^]) +extension [T](fs: Seq[Future[T]^ @use]) def awaitAll = val collector//: Collector[T]{val futures: Seq[Future[T]^{fs*}]} = Collector(fs) diff --git a/tests/pos/i18699.scala b/tests/pos/i18699.scala index 1937d7dca8c5..2cf9368a3176 100644 --- a/tests/pos/i18699.scala +++ b/tests/pos/i18699.scala @@ -1,9 +1,9 @@ import language.experimental.captureChecking -import caps.unbox +import caps.use trait Cap: def use: Int = 42 -def test2(@unbox cs: List[Cap^]): Unit = +def test2(cs: List[Cap^] @use): Unit = val t0: Cap^{cs*} = cs.head // error var t1: Cap^{cs*} = cs.head // error diff --git a/tests/pos/reach-capability.scala b/tests/pos/reach-capability.scala index 50ea479ec3c1..19e3165efbf9 100644 --- a/tests/pos/reach-capability.scala +++ b/tests/pos/reach-capability.scala @@ -1,7 +1,7 @@ import language.experimental.captureChecking import annotation.experimental import caps.Capability -import caps.unbox +import caps.use @experimental object Test2: @@ -12,7 +12,7 @@ import caps.unbox class Listener - def test2(@unbox lbls: List[Label]) = + def test2(lbls: List[Label] @use) = def makeListener(lbl: Label): Listener^{lbl} = ??? val listeners = lbls.map(makeListener) // should work diff --git a/tests/pos/reach-problem.scala b/tests/pos/reach-problem.scala index d6b7b79011a6..a2388837d923 100644 --- a/tests/pos/reach-problem.scala +++ b/tests/pos/reach-problem.scala @@ -1,11 +1,11 @@ import language.experimental.captureChecking -import caps.unbox +import caps.use class Box[T](items: Seq[T^]): def getOne: T^{items*} = ??? object Box: - def getOne[T](@unbox items: Seq[T^]): T^{items*} = + def getOne[T](items: Seq[T^ @use]): T^{items*} = val bx = Box(items) bx.getOne /* From 549deb82e14504e28d19fe90e52ea9f315a3f350 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 10 Oct 2024 10:02:40 +0200 Subject: [PATCH 12/13] Fix override checking for @use annotations --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 25 ++++++--- .../dotty/tools/dotc/cc/CheckCaptures.scala | 51 +++++++++++++------ .../dotty/tools/dotc/core/Definitions.scala | 17 ++----- .../src/dotty/tools/dotc/core/StdNames.scala | 2 +- .../dotty/tools/dotc/core/TypeComparer.scala | 15 +++--- library/src/scala/caps.scala | 2 + .../captures/unbox-overrides.check | 14 +++++ .../captures/unbox-overrides.scala | 21 ++++++++ 8 files changed, 102 insertions(+), 45 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 74a10bd723ff..119c70614064 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -79,6 +79,15 @@ def depFun(args: List[Type], resultType: Type, isContextual: Boolean, paramNames /** An exception thrown if a @retains argument is not syntactically a CaptureRef */ class IllegalCaptureRef(tpe: Type)(using Context) extends Exception(tpe.show) +/** The type of a function to be called when a `caps.$use[T]` is encountered in a subtype + * comparison. + * @param tpUnderUse the type under the caps.$use[...] + * @param other the type it is compared with + * @param fromBelow If true it's `other <: tpUnderUse` otherwise it's `tpUnderUse <: other` + * @param op The subtype test to possibly perform as a continuation + */ +type UseHandler = (toUnderUse: Type, other: Type, fromBelow: Boolean) => (op: () => Boolean) => Boolean + /** Capture checking state, which is known to other capture checking components */ class CCState: @@ -95,12 +104,12 @@ class CCState: /** The operation to perform `recordUse` is called. This is typically the case * when a subtype check is performed between a part of a function argument * and a corresponding part of a formal parameter that was labelled @use. - * Such annotations are mapped to `[T]` applications, which are handled + * Such annotations are mapped to `caps.$use[T]` applications, which are handled * as compiletime ops. * The parameter to the handler is typically the deep capture set of the argument. * The result of the handler is the result to be returned from the subtype check. */ - private var useHandler: CaptureSet => Boolean = Function.const(true) + private var useHandler: UseHandler = (tpUnderUse, other, fromBelow) => op => op() private var curLevel: Level = outermostLevel private val symLevel: mutable.Map[Symbol, Int] = mutable.Map() @@ -118,16 +127,18 @@ object CCState: */ def currentLevel(using Context): Level = ccState.curLevel - /** Perform operation `op` with a given useHandler */ - inline def withUseHandler[T](handler: CaptureSet => Boolean)(inline op: T)(using Context): T = + /** Perform operation `op` with a given useHandler to be called when `caps.$use[T]` types + * are encountered. + */ + inline def withUseHandler[T](handler: UseHandler)(inline op: T)(using Context): T = val ccs = ccState val saved = ccs.useHandler ccs.useHandler = handler try op finally ccs.useHandler = saved - /** Record a deep capture set in the current `useSet` */ - def recordUse(cs: CaptureSet)(using Context): Boolean = - ccState.useHandler(cs) + /** Call the current use handler with given arguments. This might then call `op`. */ + def underUse[T](tpUnderUse: Type, other: Type, fromBelow: Boolean)(op: => Boolean)(using Context): Boolean = + ccState.useHandler(tpUnderUse, other, fromBelow)(() => op) inline def inNestedLevel[T](inline op: T)(using Context): T = val ccs = ccState diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 4bbcd9f31dce..98c22a5c86d3 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -552,13 +552,16 @@ class CheckCaptures extends Recheck, SymTransformer: accountForUses(arg, argType, formal) argType - class MapUses(deep: Boolean)(using Context) extends TypeMap: + /** At given variance, map occurrences of `T @use` to `caps.$use[T]`. + * @param deep If true also map result types of functions + */ + class MapUses(deep: Boolean, atVariance: Int)(using Context) extends TypeMap: var usesFound = false def apply(t: Type) = t match case t @ AnnotatedType(parent, ann) => - if ann.symbol == defn.UseAnnot then + if ann.symbol == defn.UseAnnot && variance == atVariance then usesFound = true - defn.UseType.typeRef.appliedTo(apply(parent)) + defn.Caps_Use.typeRef.appliedTo(apply(parent)) else t.derivedAnnotatedType(this(parent), ann) case Existential(_, _) if !deep => @@ -566,15 +569,20 @@ class CheckCaptures extends Recheck, SymTransformer: case _ => mapOver(t) + /** If `formal` contains `@use` occurrences charge the deep capture set + * of the corresponding `argType` parts to the enclosing environments. + */ def accountForUses(arg: Tree, argType: Type, formal: Type)(using Context): Unit = - val mapper = MapUses(deep = false) + val mapper = MapUses(deep = false, atVariance = 1) val formal1 = mapper(formal) if mapper.usesFound then - def markUsesAsFree(cs: CaptureSet): Boolean = - capt.println(i"actual uses for $arg: $argType vs $formal = $cs") - markFree(cs, arg.srcPos) - true - CCState.withUseHandler(markUsesAsFree): + def useHandler(tpUnderUse: Type, other: Type, fromBelow: Boolean)(cmp: () => Boolean): Boolean = + if fromBelow then + val dcs = other.deepCaptureSet + capt.println(i"actual uses for $arg: $argType vs $formal = $dcs") + markFree(dcs, arg.srcPos) + cmp() + CCState.withUseHandler(useHandler): checkConformsExpr(argType, formal1, arg, NothingToAdd) end accountForUses @@ -1351,12 +1359,15 @@ class CheckCaptures extends Recheck, SymTransformer: */ def checkOverrides = new TreeTraverser: class OverridingPairsCheckerCC(clazz: ClassSymbol, self: Type, srcPos: SrcPos)(using Context) extends OverridingPairsChecker(clazz, self): - /** Check subtype with box adaptation. - * This function is passed to RefChecks to check the compatibility of overriding pairs. - * @param sym symbol of the field definition that is being checked - */ + /** Check subtype with box adaptation and @use checking. + * This function is passed to RefChecks to check the compatibility of overriding pairs. + * @param sym symbol of the field definition that is being checked + * @use checking: Overrides must have fewer @uses than overridden members. + * I.e. every @use in an parameter of an overriding method must correspond + * to an enclosing @use in the parameter of the overridden method. + */ override def checkSubType(actual: Type, expected: Type)(using Context): Boolean = - val mapUses = MapUses(deep = true) + val mapUses = MapUses(deep = true, atVariance = -1) val expected1 = alignDependentFunction( addOuterRefs(mapUses(expected), actual, srcPos), actual.stripCapturing) val actual1 = @@ -1374,10 +1385,18 @@ class CheckCaptures extends Recheck, SymTransformer: adapted.stripCapturing case _ => adapted finally curEnv = saved - CCState.withUseHandler(Function.const(false)): + + def lowerUseSeen: UseHandler = (tpUnderUse, other, fromBelow) => cmp => + cmp() + def noLowerUseSeen: UseHandler = (tpUnderUse, other, fromBelow) => cmp => + if fromBelow + then false // found a @use in overriding that is not covered by an enclosing @use in overridden + else CCState.withUseHandler(lowerUseSeen)(cmp()) + CCState.withUseHandler(noLowerUseSeen): TypeComparer.usingContravarianceForMethods: actual1 frozen_<:< expected1 - + end checkSubtype + override def needsCheck(overriding: Symbol, overridden: Symbol)(using Context): Boolean = !setup.isPreCC(overriding) && !setup.isPreCC(overridden) diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index 15f067db1df2..fb1094fe87c3 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -551,17 +551,6 @@ class Definitions { completeClass(enterCompleteClassSymbol( ScalaPackageClass, tpnme.maybeCapability, Final, List(StaticAnnotationClass.typeRef))) - /** A type `type [+T] <: T` used locally in capture checking. At certain points - * `T @use` types are converted to `[T]` types. These types are handled as - * compile-time applied types by TypeComparer. - */ - @tu lazy val UseType: TypeSymbol = - enterPermanentSymbol( - tpnme.USE, - TypeBounds.upper( - HKTypeLambda(HKTypeLambda.syntheticParamNames(1), Covariant :: Nil) - (_ => TypeBounds.empty :: Nil, _.paramRefs.head))).asType - @tu lazy val CollectionSeqType: TypeRef = requiredClassRef("scala.collection.Seq") @tu lazy val SeqType: TypeRef = requiredClassRef("scala.collection.immutable.Seq") @tu lazy val SeqModule: Symbol = requiredModule("scala.collection.immutable.Seq") @@ -1015,6 +1004,7 @@ class Definitions { @tu lazy val Caps_unsafeBoxFunArg: Symbol = CapsUnsafeModule.requiredMethod("unsafeBoxFunArg") @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains") @tu lazy val Caps_containsImpl: TermSymbol = CapsModule.requiredMethod("containsImpl") + @tu lazy val Caps_Use: TypeSymbol = CapsModule.requiredType("$use") /** The same as CaptureSet.universal but generated implicitly for references of Capability subtypes */ @tu lazy val universalCSImpliedByCapability = CaptureSet(captureRoot.termRef) @@ -1365,7 +1355,7 @@ class Definitions { sym.name == tpnme.From && sym.owner == NamedTupleModule.moduleClass final def isUse(sym: Symbol)(using Context): Boolean = - sym.name == tpnme.USE && sym.owner == ScalaPackageClass + sym.name == tpnme.USE && sym.owner == CapsModule.moduleClass private val compiletimePackageAnyTypes: Set[Name] = Set( tpnme.Equals, tpnme.NotEquals, tpnme.IsConst, tpnme.ToString @@ -2211,8 +2201,7 @@ class Definitions { NothingClass, SingletonClass, CBCompanion, - MaybeCapabilityAnnot, - UseType) + MaybeCapabilityAnnot) @tu lazy val syntheticCoreClasses: List[Symbol] = syntheticScalaClasses ++ List( EmptyPackageVal, diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala index 5bf75e95c4e9..e30cabcc9f4b 100644 --- a/compiler/src/dotty/tools/dotc/core/StdNames.scala +++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala @@ -194,7 +194,7 @@ object StdNames { final val WILDCARD_STAR: N = "_*" final val REIFY_TREECREATOR_PREFIX: N = "$treecreator" final val REIFY_TYPECREATOR_PREFIX: N = "$typecreator" - final val USE: N = "" + final val USE: N = "$use" final val Any: N = "Any" final val AnyKind: N = "AnyKind" diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 43e9c081af8b..9b161b2be661 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -819,10 +819,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling case tp2: MethodType => def compareMethod = tp1 match { case tp1: MethodType => - (tp1.signature consistentParams tp2.signature) && - matchingMethodParams(tp1, tp2) && - (!tp2.isImplicitMethod || tp1.isImplicitMethod) && - isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1)) + (useContravariance || tp1.signature.consistentParams(tp2.signature)) + && matchingMethodParams(tp1, tp2) + && (!tp2.isImplicitMethod || tp1.isImplicitMethod) + && isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1)) case _ => false } compareMethod @@ -830,7 +830,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling def comparePoly = tp1 match { case tp1: PolyType => comparingTypeLambdas(tp1, tp2) { - (tp1.signature consistentParams tp2.signature) + (useContravariance || (tp1.signature consistentParams tp2.signature)) && matchingPolyParams(tp1, tp2) && isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1)) } @@ -1538,8 +1538,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling val tycon = tp.tycon.typeSymbol if defn.isCompiletime_S(tycon) then compareS(tp, other, fromBelow) - else if defn.isUse(tycon) && fromBelow then - CCState.recordUse(other.deepCaptureSet) && recur(other, tp.args.head) + else if defn.isUse(tycon) then + CCState.underUse(tp.args.head, other, fromBelow): + if fromBelow then recur(other, tp.args.head) else recur(tp.args.head, other) else val folded = tp.tryCompiletimeConstantFold if (fromBelow) recur(other, folded) else recur(folded, other) diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala index 6c7610e410c0..83dc3ae16423 100644 --- a/library/src/scala/caps.scala +++ b/library/src/scala/caps.scala @@ -57,6 +57,8 @@ import annotation.{experimental, compileTimeOnly, retainsCap} */ final class use extends annotation.StaticAnnotation + type $use[+T] + object unsafe: extension [T](x: T) diff --git a/tests/neg-custom-args/captures/unbox-overrides.check b/tests/neg-custom-args/captures/unbox-overrides.check index 404475fae2a8..20b3a05e25d0 100644 --- a/tests/neg-custom-args/captures/unbox-overrides.check +++ b/tests/neg-custom-args/captures/unbox-overrides.check @@ -26,3 +26,17 @@ | method foo of type [T](a: Int)(x: C @use): C has incompatible type | | longer explanation available when compiling with `-explain` +-- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:35:6 --------------------------------- +35 | def foo(x: (List[C], List[C]) @use): Unit // error + | ^ + | error overriding method foo in trait D1 of type (x: (List[C @use], List[C])): Unit; + | method foo of type (x: (List[C], List[C]) @use): Unit has incompatible type + | + | longer explanation available when compiling with `-explain` +-- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:36:6 --------------------------------- +36 | def bar(x: (List[C], List[C]) @use): Unit // error + | ^ + | error overriding method bar in trait D1 of type (x: (List[C @use], List[C @use])): Unit; + | method bar of type (x: (List[C], List[C]) @use): Unit has incompatible type + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/unbox-overrides.scala b/tests/neg-custom-args/captures/unbox-overrides.scala index 757133f8b115..f18d71c24722 100644 --- a/tests/neg-custom-args/captures/unbox-overrides.scala +++ b/tests/neg-custom-args/captures/unbox-overrides.scala @@ -25,3 +25,24 @@ trait Poly: trait Poly1 extends Poly: def foo[T](a: Int)(x: C @use): C // error def bar[T](a: Int)(x: C): C // ok + +trait D1: + def foo(x: (List[C @use], List[C])): Unit + def bar(x: (List[C @use], List[C @use])): Unit + def baz(x: (List[C], List[C]) @use): Unit + +trait D2 extends D1: + def foo(x: (List[C], List[C]) @use): Unit // error + def bar(x: (List[C], List[C]) @use): Unit // error + def baz(x: (List[C] @use, List[C] @use)): Unit // ok + +trait E2: + def foo(x: (List[C], List[C]) @use): Unit + def bar(x: (List[C], List[C]) @use): Unit + def baz(x: (List[C] @use, List[C] @use)): Unit + +trait E3 extends E2: + def foo(x: (List[C] @use, List[C])): Unit // ok + def bar(x: (List[C], List[C])): Unit // ok + def baz(x: (List[C] @use, List[C] @use)): Unit // ok + From 7f63f8432d6597d69724f92d7b4c33a6d6952415 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 10 Oct 2024 16:34:35 +0200 Subject: [PATCH 13/13] Change encoding of reach capabilities under @use The new encoding wraps such capabilities with @use instead of relying on a @ReachUnderUse annotation. Advantage: This can generalize to capture set variables under @use. --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 30 +++++++++++-------- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 23 ++++++-------- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 7 +---- .../dotty/tools/dotc/cc/CheckCaptures.scala | 8 ++--- .../dotty/tools/dotc/core/Definitions.scala | 1 - .../tools/dotc/printing/PlainPrinter.scala | 6 ++-- .../tools/dotc/printing/RefinedPrinter.scala | 2 +- .../internal/reachUnderUseCapability.scala | 9 ------ 8 files changed, 36 insertions(+), 50 deletions(-) delete mode 100644 library/src/scala/annotation/internal/reachUnderUseCapability.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 119c70614064..0bc9297b55bd 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -178,7 +178,7 @@ extension (tree: Tree) */ def toCaptureRefs(using Context): List[CaptureRef] = tree match case ReachCapabilityApply(arg) => - arg.toCaptureRefs.map(_.reach()) + arg.toCaptureRefs.map(_.reach) case CapsOfApply(arg) => arg.toCaptureRefs case _ => tree.tpe.dealiasKeepAnnots match @@ -236,8 +236,8 @@ extension (tp: Type) tp.derivesFrom(defn.Caps_CapSet) case AnnotatedType(parent, annot) => (annot.symbol == defn.ReachCapabilityAnnot - || annot.symbol == defn.ReachUnderUseCapabilityAnnot || annot.symbol == defn.MaybeCapabilityAnnot + || annot.symbol == defn.UseAnnot ) && parent.isTrackableRef case _ => false @@ -264,10 +264,9 @@ extension (tp: Type) def deepCaptureSet(using Context): CaptureSet = val dcs = CaptureSet.ofTypeDeeply(tp) if dcs.isAlwaysEmpty then dcs - else tp match + else tp.stripUse match case tp @ ReachCapability(_) => tp.singletonCaptureSet - case tp @ ReachUnderUseCapability(_) => tp.singletonCaptureSet - case tp: SingletonCaptureRef => tp.reach().singletonCaptureSet + case tp: SingletonCaptureRef => tp.reach.singletonCaptureSet case _ => dcs /** A type capturing `ref` */ @@ -430,11 +429,9 @@ extension (tp: Type) * type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}` * are unrelated. */ - def reach(underUse: Boolean = false)(using Context): CaptureRef = tp match + def reach(using Context): CaptureRef = tp match case tp: CaptureRef if tp.isTrackableRef => - if tp.isReach then tp - else if underUse then ReachUnderUseCapability(tp) - else ReachCapability(tp) + if tp.isReach then tp else ReachCapability(tp) /** If `x` is a capture ref, its maybe capability `x?`, represented internally * as `x @maybeCapability`. `x?` stands for a capability `x` that might or might @@ -458,6 +455,14 @@ extension (tp: Type) case tp: CaptureRef if tp.isTrackableRef => if tp.isMaybe then tp else MaybeCapability(tp) + def isUnderUse(using Context): Boolean = tp match + case AnnotatedType(_: CaptureRef, annot) => annot.symbol == defn.UseAnnot + case _ => false + + def stripUse(using Context): Type = tp match + case AnnotatedType(tp1: CaptureRef, annot) if annot.symbol == defn.UseAnnot => tp1 + case _ => tp + /** If `ref` is a trackable capture ref, and `tp` has only covariant occurrences of a * universal capture set, replace all these occurrences by `{ref*}`. This implements * the new aspect of the (Var) rule, which can now be stated as follows: @@ -515,7 +520,9 @@ extension (tp: Type) if variance <= 0 then isFlipped = true t.dealiasKeepAnnots match case t @ CapturingType(p, cs) if cs.isUniversal && !isFlipped => - t.derivedCapturingType(apply(p), ref.reach(underUse).singletonCaptureSet) + var reach = ref.reach + if underUse then reach = reach.underUse + t.derivedCapturingType(apply(p), reach.singletonCaptureSet) case t @ AnnotatedType(parent, ann) => if ann.symbol == defn.UseAnnot then val saved = underUse @@ -682,7 +689,7 @@ object CapsOfApply: class AnnotatedCapability(annot: Context ?=> ClassSymbol): def apply(tp: Type)(using Context) = AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan)) - def unapply(tp: AnnotatedType)(using Context): Option[CaptureRef] = tp match + def unapply(tp: AnnotatedType)(using Context): Option[CaptureRef] = tp.stripUse match case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent) case _ => None @@ -690,7 +697,6 @@ class AnnotatedCapability(annot: Context ?=> ClassSymbol): * the reach capability `ref*` as a type. */ object ReachCapability extends AnnotatedCapability(defn.ReachCapabilityAnnot) -object ReachUnderUseCapability extends AnnotatedCapability(defn.ReachUnderUseCapabilityAnnot) /** An extractor for `ref @maybeCapability`, which is used to express * the maybe capability `ref?` as a type. diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index 0f43280d582a..8097eee2fe7a 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -13,6 +13,7 @@ import CCState.* import Periods.NoRunId import compiletime.uninitialized import StdNames.nme +import Annotations.Annotation /** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs, * as well as two kinds of AnnotatedTypes representing reach and maybe capabilities. @@ -29,36 +30,31 @@ trait CaptureRef extends TypeProxy, ValueType: this.isTrackableRef && (isMaxCapability || !captureSetOfInfo.isAlwaysEmpty) /** Is this a reach reference of the form `x*`? */ - final def isReach(using Context): Boolean = this match - case AnnotatedType(_, annot) => - annot.symbol == defn.ReachCapabilityAnnot || annot.symbol == defn.ReachUnderUseCapabilityAnnot + final def isReach(using Context): Boolean = this.stripUse match + case AnnotatedType(_, annot) => annot.symbol == defn.ReachCapabilityAnnot case _ => false final def isUnderUse(using Context): Boolean = this match - case AnnotatedType(_, annot) => annot.symbol == defn.ReachUnderUseCapabilityAnnot + case AnnotatedType(_, annot) => annot.symbol == defn.UseAnnot case _ => false - def toUnderUse(using Context): CaptureRef = - if isUnderUse then - this match - case _: AnnotatedType => stripReach.reach(underUse = true) - // TODO: Handle capture set variables here - else this + def underUse(using Context): CaptureRef = + AnnotatedType(this, Annotation(defn.UseAnnot, util.Spans.NoSpan)) /** Is this a maybe reference of the form `x?`? */ - final def isMaybe(using Context): Boolean = this match + final def isMaybe(using Context): Boolean = this.stripUse match case AnnotatedType(_, annot) => annot.symbol == defn.MaybeCapabilityAnnot case _ => false final def stripReach(using Context): CaptureRef = if isReach then - val AnnotatedType(parent: CaptureRef, _) = this: @unchecked + val AnnotatedType(parent: CaptureRef, _) = this.stripUse: @unchecked parent else this final def stripMaybe(using Context): CaptureRef = if isMaybe then - val AnnotatedType(parent: CaptureRef, _) = this: @unchecked + val AnnotatedType(parent: CaptureRef, _) = this.stripUse: @unchecked parent else this @@ -144,7 +140,6 @@ trait CaptureRef extends TypeProxy, ValueType: case _ => false || this.match case ReachCapability(x1) => x1.subsumes(y.stripReach) - case ReachUnderUseCapability(x1) => x1.subsumes(y.stripReach) case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y)) case x: TermParamRef => subsumesExistentially(x, y) case x: TypeRef => assumedContainsOf(x).contains(y) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 5e31b8c8aa11..2b5df937484a 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -517,8 +517,6 @@ object CaptureSet: elem.cls.ccLevel.nextInner <= level case ReachCapability(elem1) => levelOK(elem1) - case ReachUnderUseCapability(elem1) => - levelOK(elem1) case MaybeCapability(elem1) => levelOK(elem1) case _ => @@ -1068,8 +1066,6 @@ object CaptureSet: else CaptureSet.universal case ReachCapability(ref1) => deepCaptureSet(ref1.widen) .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt) - case ReachUnderUseCapability(ref1) => deepCaptureSet(ref1.widen) - .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt) case _ => ofType(ref.underlying, followResult = true) /** Capture set of a type */ @@ -1087,8 +1083,7 @@ object CaptureSet: case CapturingType(parent, refs) => recur(parent) ++ refs case tp @ AnnotatedType(parent, ann) - if ann.hasSymbol(defn.ReachCapabilityAnnot) - || ann.hasSymbol(defn.ReachUnderUseCapabilityAnnot) => + if ann.hasSymbol(defn.ReachCapabilityAnnot) => parent match case parent: SingletonCaptureRef if parent.isTrackableRef => tp.singletonCaptureSet diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 98c22a5c86d3..dd128848532d 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1359,7 +1359,7 @@ class CheckCaptures extends Recheck, SymTransformer: */ def checkOverrides = new TreeTraverser: class OverridingPairsCheckerCC(clazz: ClassSymbol, self: Type, srcPos: SrcPos)(using Context) extends OverridingPairsChecker(clazz, self): - /** Check subtype with box adaptation and @use checking. + /** Check subtype with box adaptation and @use checking. * This function is passed to RefChecks to check the compatibility of overriding pairs. * @param sym symbol of the field definition that is being checked * @use checking: Overrides must have fewer @uses than overridden members. @@ -1385,7 +1385,7 @@ class CheckCaptures extends Recheck, SymTransformer: adapted.stripCapturing case _ => adapted finally curEnv = saved - + def lowerUseSeen: UseHandler = (tpUnderUse, other, fromBelow) => cmp => cmp() def noLowerUseSeen: UseHandler = (tpUnderUse, other, fromBelow) => cmp => @@ -1395,8 +1395,8 @@ class CheckCaptures extends Recheck, SymTransformer: CCState.withUseHandler(noLowerUseSeen): TypeComparer.usingContravarianceForMethods: actual1 frozen_<:< expected1 - end checkSubtype - + end checkSubType + override def needsCheck(overriding: Symbol, overridden: Symbol)(using Context): Boolean = !setup.isPreCC(overriding) && !setup.isPreCC(overridden) diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index fb1094fe87c3..af91e2296304 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -1078,7 +1078,6 @@ class Definitions { @tu lazy val TargetNameAnnot: ClassSymbol = requiredClass("scala.annotation.targetName") @tu lazy val VarargsAnnot: ClassSymbol = requiredClass("scala.annotation.varargs") @tu lazy val ReachCapabilityAnnot = requiredClass("scala.annotation.internal.reachCapability") - @tu lazy val ReachUnderUseCapabilityAnnot = requiredClass("scala.annotation.internal.reachUnderUseCapability") @tu lazy val RequiresCapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.internal.requiresCapability") @tu lazy val RetainsAnnot: ClassSymbol = requiredClass("scala.annotation.retains") @tu lazy val RetainsCapAnnot: ClassSymbol = requiredClass("scala.annotation.retainsCap") diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala index a3913c699a3d..0c8358e07cfa 100644 --- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -15,7 +15,7 @@ import util.SourcePosition import scala.util.control.NonFatal import scala.annotation.switch import config.{Config, Feature} -import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, ReachUnderUseCapability, MaybeCapability, isBoxed, retainedElems, isRetainsLike} +import cc.* class PlainPrinter(_ctx: Context) extends Printer { @@ -417,8 +417,8 @@ class PlainPrinter(_ctx: Context) extends Printer { case tp: TermRef if tp.symbol == defn.captureRoot => Str("cap") case tp: SingletonType => toTextRef(tp) case tp: (TypeRef | TypeParamRef) => toText(tp) ~ "^" - case ReachCapability(tp1) => toTextCaptureRef(tp1) ~ "*" - case ReachUnderUseCapability(tp1) => toTextCaptureRef(tp1) ~ "*@use" + case ReachCapability(tp1) => + toTextCaptureRef(tp1) ~ "*" ~ Str("@use").provided(tp.isUnderUse) case MaybeCapability(tp1) => toTextCaptureRef(tp1) ~ "?" case tp => toText(tp) diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala index 6f499656396e..f753088d67b0 100644 --- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala @@ -330,7 +330,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { "?" ~ (("(ignored: " ~ toText(ignored) ~ ")") provided printDebug) case tp @ PolyProto(targs, resType) => "[applied to [" ~ toTextGlobal(targs, ", ") ~ "] returning " ~ toText(resType) - case ReachCapability(_) | ReachUnderUseCapability(_) | MaybeCapability(_) => + case ReachCapability(_) | MaybeCapability(_) => toTextCaptureRef(tp) case _ => super.toText(tp) diff --git a/library/src/scala/annotation/internal/reachUnderUseCapability.scala b/library/src/scala/annotation/internal/reachUnderUseCapability.scala deleted file mode 100644 index 6c07be66adc5..000000000000 --- a/library/src/scala/annotation/internal/reachUnderUseCapability.scala +++ /dev/null @@ -1,9 +0,0 @@ -package scala.annotation -package internal - -/** An annotation that marks a capture ref as a reach capability occurring - * under a @use part of a parameter type. - * Example: When it occurs in `C[x* @use]`, `x*` is encoded as - * `x.type @reachUnderuseCapability` - */ -class reachUnderUseCapability extends StaticAnnotation