From bdbb0ba8b08c3e68cbc9139acc5226bbbdc354b3 Mon Sep 17 00:00:00 2001 From: noti0na1 Date: Fri, 1 Nov 2024 13:22:47 +0100 Subject: [PATCH 1/5] Handle CapsOf in more places --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 2 +- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 2 ++ .../dotty/tools/dotc/cc/CheckCaptures.scala | 2 +- .../src/dotty/tools/dotc/core/Types.scala | 4 ++- .../captures/capture-poly.scala | 25 +++++++++++++++++++ 5 files changed, 32 insertions(+), 3 deletions(-) create mode 100644 tests/neg-custom-args/captures/capture-poly.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index aad6ca8ddeac..a9272b73e605 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -198,7 +198,7 @@ extension (tp: Type) || tp.isRootCapability ) && !tp.symbol.isOneOf(UnstableValueFlags) case tp: TypeRef => - tp.symbol.isAbstractOrParamType && tp.derivesFrom(defn.Caps_CapSet) + tp.symbol.isType && tp.derivesFrom(defn.Caps_CapSet) case tp: TypeParamRef => tp.derivesFrom(defn.Caps_CapSet) case AnnotatedType(parent, annot) => diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index 590beda42903..199114880c2b 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -140,6 +140,8 @@ trait CaptureRef extends TypeProxy, ValueType: case ReachCapability(x1) => x1.subsumes(y.stripReach) case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y)) case x: TermParamRef => subsumesExistentially(x, y) + case x: TypeRef if x.symbol.info.derivesFrom(defn.Caps_CapSet) => + x.captureSetOfInfo.elems.exists(_.subsumes(y)) case x: TypeRef => assumedContainsOf(x).contains(y) case _ => false end subsumes diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 77d893ad49b9..2a3cd50d0e0c 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -135,7 +135,7 @@ object CheckCaptures: elem match case CapsOfApply(arg) => def isLegalCapsOfArg = - arg.symbol.isAbstractOrParamType && arg.symbol.info.derivesFrom(defn.Caps_CapSet) + arg.symbol.isType && arg.symbol.info.derivesFrom(defn.Caps_CapSet) if !isLegalCapsOfArg then report.error( em"""$arg is not a legal prefix for `^` here, diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index 31e11487ae38..821363c74a25 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -4007,7 +4007,7 @@ object Types extends TypeUtils { (compute(status, parent, theAcc) /: refs.elems) { (s, ref) => ref.stripReach match case tp: TermParamRef if tp.binder eq thisLambdaType => combine(s, CaptureDeps) - case _ => s + case tp => combine(s, compute(status, tp, theAcc)) } case _ => if tp.annot.refersToParamOf(thisLambdaType) then TrueDeps @@ -6078,6 +6078,8 @@ object Types extends TypeUtils { case tp: CaptureRef => if tp.isTrackableRef then tp else ensureTrackable(tp.underlying) + case tp: TypeAlias => + ensureTrackable(tp.alias) case _ => assert(false, i"not a trackable captureRef ref: $result, ${result.underlyingIterator.toList}") ensureTrackable(result) diff --git a/tests/neg-custom-args/captures/capture-poly.scala b/tests/neg-custom-args/captures/capture-poly.scala new file mode 100644 index 000000000000..a3a7a4c2a3d7 --- /dev/null +++ b/tests/neg-custom-args/captures/capture-poly.scala @@ -0,0 +1,25 @@ +import caps.* + +trait Foo extends Capability + +trait CaptureSet: + type C <: CapSet^ + +def capturePoly[C^](a: Foo^{C^}): Foo^{C^} = a +def capturePoly2(c: CaptureSet)(a: Foo^{c.C^}): Foo^{c.C^} = a + +def test = + val x: Foo^ = ??? + val y: Foo^ = ??? + + object X extends CaptureSet: + type C = CapSet^{x} + + val z1: Foo^{X.C^} = x + val z2: Foo^{X.C^} = y // error + + val z3: Foo^{x} = capturePoly(x) + val z4: Foo^{x} = capturePoly(y) // error + + val z5: Foo^{x} = capturePoly2(X)(x) + val z6: Foo^{x} = capturePoly2(X)(y) // error \ No newline at end of file From 13e443954a871da85f043b5c9649a31a892a1ff7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Mon, 18 Nov 2024 17:49:03 +0100 Subject: [PATCH 2/5] Report error in Setup for illegal capture refs --- compiler/src/dotty/tools/dotc/cc/Setup.scala | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 3147a0f7bd47..cc456567ce8a 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -18,6 +18,7 @@ import reporting.Message import printing.{Printer, Texts}, Texts.{Text, Str} import collection.mutable import CCState.* +import dotty.tools.dotc.util.NoSourcePosition /** Operations accessed from CheckCaptures */ trait SetupAPI: @@ -323,7 +324,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: val parent2 = stripImpliedCaptureSet(parent1) for tpt <- tptToCheck do checkWellformedLater(parent2, ann.tree, tpt) - CapturingType(parent2, ann.tree.toCaptureSet) + try + CapturingType(parent2, ann.tree.toCaptureSet) + catch case ex: IllegalCaptureRef => + report.error(em"Illegal capture reference: ${ex.getMessage.nn}", tptToCheck.fold(NoSourcePosition)(_.srcPos)) + t else t.derivedAnnotatedType(parent1, ann) case throwsAlias(res, exc) => From 20917c7a95f004ac5caad5097d5d06eb5120da77 Mon Sep 17 00:00:00 2001 From: noti0na1 Date: Tue, 19 Nov 2024 18:04:51 +0100 Subject: [PATCH 3/5] Add some tests --- .../captures/capset-bound.scala | 18 ++++++++++++++++++ tests/neg-custom-args/captures/i21868.scala | 14 ++++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 tests/neg-custom-args/captures/capset-bound.scala create mode 100644 tests/neg-custom-args/captures/i21868.scala diff --git a/tests/neg-custom-args/captures/capset-bound.scala b/tests/neg-custom-args/captures/capset-bound.scala new file mode 100644 index 000000000000..c00f61240dea --- /dev/null +++ b/tests/neg-custom-args/captures/capset-bound.scala @@ -0,0 +1,18 @@ +import caps.* + +class IO + +case class File(io: IO^) + +def test(io1: IO^, io2: IO^) = + def f[C >: CapSet^{io1} <: CapSet^](file: File^{C^}) = ??? + val f1: File^{io1} = ??? + val f2: File^{io2} = ??? + val f3: File^{io1, io2} = ??? + f[CapSet^{io1}](f1) + f[CapSet^{io1}](f2) // error + f[CapSet^{io1}](f3) // error + f[CapSet^{io2}](f2) // error + f[CapSet^{io1, io2}](f1) + f[CapSet^{io1, io2}](f2) + f[CapSet^{io1, io2}](f3) \ No newline at end of file diff --git a/tests/neg-custom-args/captures/i21868.scala b/tests/neg-custom-args/captures/i21868.scala new file mode 100644 index 000000000000..349750a2ee4b --- /dev/null +++ b/tests/neg-custom-args/captures/i21868.scala @@ -0,0 +1,14 @@ +import caps. + +trait AbstractWrong: + type C <: CapSet + def boom(): Unit^{C^} // error + +trait Abstract: + type C <: CapSet^ + def boom(): Unit^{C^} + +class Concrete extends Abstract: + type C = Nothing + def boom() = () // error + From cf66d1840e1fcbc9a59e627ac970d866df29036e Mon Sep 17 00:00:00 2001 From: noti0na1 Date: Wed, 20 Nov 2024 13:20:22 +0100 Subject: [PATCH 4/5] Fix the test --- tests/neg-custom-args/captures/i21868.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/neg-custom-args/captures/i21868.scala b/tests/neg-custom-args/captures/i21868.scala index 349750a2ee4b..929e770a21c6 100644 --- a/tests/neg-custom-args/captures/i21868.scala +++ b/tests/neg-custom-args/captures/i21868.scala @@ -1,4 +1,4 @@ -import caps. +import caps.* trait AbstractWrong: type C <: CapSet From a163f0c9257e0165f723b016f20e0b30c7b0a342 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Thu, 21 Nov 2024 15:17:45 +0100 Subject: [PATCH 5/5] Report illegal capture reference only once If we do not strip the capture set at this point, then the type will be transformed twice and we'll get the same error message twice. --- compiler/src/dotty/tools/dotc/cc/Setup.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index cc456567ce8a..7cd12b999618 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -328,7 +328,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: CapturingType(parent2, ann.tree.toCaptureSet) catch case ex: IllegalCaptureRef => report.error(em"Illegal capture reference: ${ex.getMessage.nn}", tptToCheck.fold(NoSourcePosition)(_.srcPos)) - t + parent2 else t.derivedAnnotatedType(parent1, ann) case throwsAlias(res, exc) =>