From d38f257603acc27d9cc0e83b1b7fd98dce17aabf Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Fri, 23 May 2025 14:13:14 +0200
Subject: [PATCH 1/4] Add handling for classes deriving from Capability in
capturing type logic
---
compiler/src/dotty/tools/dotc/cc/Setup.scala | 3 +++
1 file changed, 3 insertions(+)
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index c9b4546c8c37..8c622cfe8c8d 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -728,6 +728,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
else if cls.isPureClass then
// is cls is known to be pure, nothing needs to be added to self type
selfInfo
+ else if cls.derivesFrom(defn.Caps_Capability) then
+ CapturingType(cinfo.selfType, CaptureSet.csImpliedByCapability)
+ // CapturingType(cinfo.selfType, CaptureSet.universal)
else if !cls.isEffectivelySealed && !cls.baseClassHasExplicitNonUniversalSelfType then
// assume {cap} for completely unconstrained self types of publicly extensible classes
CapturingType(cinfo.selfType, CaptureSet.universal)
From 5995e3b02ce9b291a13540927e02c3adca10da16 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Fri, 23 May 2025 16:20:12 +0200
Subject: [PATCH 2/4] Make self fresh in capability classes
---
compiler/src/dotty/tools/dotc/cc/Setup.scala | 7 +++++--
tests/neg-custom-args/captures/i23223.scala | 12 ++++++++++++
tests/pos-custom-args/captures/i20237.scala | 4 ++++
3 files changed, 21 insertions(+), 2 deletions(-)
create mode 100644 tests/neg-custom-args/captures/i23223.scala
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 8c622cfe8c8d..d91e235841ec 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -729,8 +729,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
// is cls is known to be pure, nothing needs to be added to self type
selfInfo
else if cls.derivesFrom(defn.Caps_Capability) then
- CapturingType(cinfo.selfType, CaptureSet.csImpliedByCapability)
- // CapturingType(cinfo.selfType, CaptureSet.universal)
+ // If cls is a capability class, we need to add a fresh capability to
+ // ensure we cannot tread itself as pure.
+ CapturingType(cinfo.selfType,
+ CaptureSet.fresh(Origin.InDecl(cls)).readOnly
+ ++ CaptureSet.Var(cls, level = ccState.currentLevel))
else if !cls.isEffectivelySealed && !cls.baseClassHasExplicitNonUniversalSelfType then
// assume {cap} for completely unconstrained self types of publicly extensible classes
CapturingType(cinfo.selfType, CaptureSet.universal)
diff --git a/tests/neg-custom-args/captures/i23223.scala b/tests/neg-custom-args/captures/i23223.scala
new file mode 100644
index 000000000000..e606875b840a
--- /dev/null
+++ b/tests/neg-custom-args/captures/i23223.scala
@@ -0,0 +1,12 @@
+import language.experimental.captureChecking
+import caps.*
+
+class A:
+ def a: A = this
+
+class B extends A, Capability // error
+
+def leak(b: B): A = b.a
+
+class C extends Capability:
+ def c: C^{} = this // error
diff --git a/tests/pos-custom-args/captures/i20237.scala b/tests/pos-custom-args/captures/i20237.scala
index 973f5d2025e3..53efbb2e7583 100644
--- a/tests/pos-custom-args/captures/i20237.scala
+++ b/tests/pos-custom-args/captures/i20237.scala
@@ -1,8 +1,12 @@
import language.experimental.captureChecking
+import caps.*
class Cap extends caps.Capability:
def use[T](body: Cap ?=> T) = body(using this)
+class Cap2 extends caps.Capability:
+ def use[T](body: Cap2 => T) = body(this)
+
class Box[T](body: Cap ?=> T):
inline def open(using cap: Cap) = cap.use(body)
From da5a9025e182beb1bc20595265940c329d7a9227 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Fri, 23 May 2025 16:26:18 +0200
Subject: [PATCH 3/4] Update compiler/src/dotty/tools/dotc/cc/Setup.scala
Fix typo
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
---
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 d91e235841ec..c5125b8eab07 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -730,7 +730,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
selfInfo
else if cls.derivesFrom(defn.Caps_Capability) then
// If cls is a capability class, we need to add a fresh capability to
- // ensure we cannot tread itself as pure.
+ // ensure we cannot treat itself as pure.
CapturingType(cinfo.selfType,
CaptureSet.fresh(Origin.InDecl(cls)).readOnly
++ CaptureSet.Var(cls, level = ccState.currentLevel))
From 8670b999e03c329cc981db3a6119301638c0b36b Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 26 May 2025 19:37:21 +0200
Subject: [PATCH 4/4] Tweak so that we only add one capture set variable to
self types
---
compiler/src/dotty/tools/dotc/cc/Setup.scala | 13 ++++++-------
1 file changed, 6 insertions(+), 7 deletions(-)
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index c5125b8eab07..69bfa96df836 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -728,12 +728,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
else if cls.isPureClass then
// is cls is known to be pure, nothing needs to be added to self type
selfInfo
- else if cls.derivesFrom(defn.Caps_Capability) then
- // If cls is a capability class, we need to add a fresh capability to
- // ensure we cannot treat itself as pure.
- CapturingType(cinfo.selfType,
- CaptureSet.fresh(Origin.InDecl(cls)).readOnly
- ++ CaptureSet.Var(cls, level = ccState.currentLevel))
else if !cls.isEffectivelySealed && !cls.baseClassHasExplicitNonUniversalSelfType then
// assume {cap} for completely unconstrained self types of publicly extensible classes
CapturingType(cinfo.selfType, CaptureSet.universal)
@@ -741,7 +735,12 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
// Infer the self type for the rest, which is all classes without explicit
// self types (to which we also add nested module classes), provided they are
// neither pure, nor are publicily extensible with an unconstrained self type.
- CapturingType(cinfo.selfType, CaptureSet.Var(cls, level = ccState.currentLevel))
+ val cs = CaptureSet.Var(cls, level = ccState.currentLevel)
+ if cls.derivesFrom(defn.Caps_Capability) then
+ // If cls is a capability class, we need to add a fresh readonly capability to
+ // ensure we cannot treat the class as pure.
+ CaptureSet.fresh(Origin.InDecl(cls)).readOnly.subCaptures(cs)
+ CapturingType(cinfo.selfType, cs)
// Compute new parent types
val ps1 = inContext(ctx.withOwner(cls)):