Skip to content

Commit d4e0d2e

Browse files
oderskyodersky
committed
Imply cap.rd only for exclusive capabilities
For capabilities classified as Shared, assume `cap` instead.
1 parent 5404f7a commit d4e0d2e

File tree

12 files changed

+66
-61
lines changed

12 files changed

+66
-61
lines changed

‎compiler/src/dotty/tools/dotc/cc/CaptureOps.scala

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -379,6 +379,7 @@ extension (tp: Type)
379379
def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability)
380380
def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable)
381381
def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)
382+
def derivesFromExclusive(using Context): Boolean = derivesFromCapTrait(defn.Caps_ExclusiveCapability)
382383

383384
/** Drop @retains annotations everywhere */
384385
def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling

‎compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -626,9 +626,13 @@ object CaptureSet:
626626
then i" under-approximating the result of mapping $ref to $mapped"
627627
else ""
628628

629+
private def capImpliedByCapability(parent: Type)(using Context): Capability =
630+
if parent.derivesFromExclusive then GlobalCap.readOnly else GlobalCap
631+
629632
/* The same as {cap.rd} but generated implicitly for references of Capability subtypes.
630633
*/
631-
case class CSImpliedByCapability() extends Const(SimpleIdentitySet(GlobalCap.readOnly))
634+
class CSImpliedByCapability(parent: Type)(using @constructorOnly ctx: Context)
635+
extends Const(SimpleIdentitySet(capImpliedByCapability(parent)))
632636

633637
/** A special capture set that gets added to the types of symbols that were not
634638
* themselves capture checked, in order to admit arbitrary corresponding capture

‎compiler/src/dotty/tools/dotc/cc/Setup.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -400,7 +400,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
400400
then
401401
normalizeCaptures(mapOver(t)) match
402402
case t1 @ CapturingType(_, _) => t1
403-
case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(), boxed = false)
403+
case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(t1), boxed = false)
404404
else normalizeCaptures(mapFollowingAliases(t))
405405

406406
def innerApply(t: Type) =

‎compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -284,9 +284,9 @@ class PlainPrinter(_ctx: Context) extends Printer {
284284
case tp @ CapturingType(parent, refs) =>
285285
val boxText: Text = Str("box ") provided tp.isBoxed && ccVerbose
286286
if elideCapabilityCaps
287-
&& parent.derivesFrom(defn.Caps_Capability)
287+
&& parent.derivesFromCapability
288288
&& refs.containsTerminalCapability
289-
&& refs.isReadOnly
289+
&& (!parent.derivesFromExclusive || refs.isReadOnly)
290290
then toText(parent)
291291
else toTextCapturing(parent, refs, boxText)
292292
case tp @ RetainingType(parent, refSet) =>

‎tests/neg-custom-args/captures/effect-swaps.check

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -19,10 +19,10 @@
1919
69 | Future: fut ?=> // error, type mismatch
2020
| ^
2121
|Found: (contextual$9: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, contextual$9}
22-
|Required: (boundary.Label[Result[Future[T^?]^?, E^?]]^{cap.rd}) ?=> Future[T^?]^?
22+
|Required: (boundary.Label[Result[Future[T^?]^?, E^?]]^) ?=> Future[T^?]^?
2323
|
2424
|where: ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make
25-
| cap is the universal root capability
25+
| ^ refers to the universal root capability
2626
|
2727
|Note that capability contextual$9.type
2828
|cannot be included in outer capture set ?.
@@ -33,10 +33,10 @@
3333
73 | Result.make[Future[T], E]: lbl ?=> // error: type mismatch
3434
| ^
3535
|Found: (lbl: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, lbl}
36-
|Required: (boundary.Label[Result[Future[T], E]]^{cap.rd}) ?=> Future[T]
36+
|Required: (boundary.Label[Result[Future[T], E]]^) ?=> Future[T]
3737
|
3838
|where: ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make
39-
| cap is the universal root capability
39+
| ^ refers to the universal root capability
4040
|
4141
|Note that capability (fr : Future[Result[T, E]]^) is not included in capture set {}.
4242
74 | Future: fut ?=>

‎tests/neg-custom-args/captures/extending-cap-classes.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,6 @@
2525
| ^^
2626
| Found: (y2 : C2)
2727
| Required: C1
28-
| Note that capability cap.rd is not included in capture set {}.
28+
| Note that capability cap is not included in capture set {}.
2929
|
3030
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/filevar.check

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/filevar.scala:15:12 --------------------------------------
22
15 | withFile: f => // error with level checking, was OK under both schemes before
33
| ^
4-
|Found: (l: scala.caps.Capability^{cap.rd}) ?->? File^? ->? Unit
5-
|Required: (l: scala.caps.Capability^{cap.rd}) ?-> (f: File^{l}) => Unit
4+
|Found: (l: scala.caps.Capability^) ?->? File^? ->? Unit
5+
|Required: (l: scala.caps.Capability^) ?-> (f: File^{l}) => Unit
66
|
7-
|where: => refers to a root capability associated with the result type of (using l: scala.caps.Capability^{cap.rd}): (f: File^{l}) => Unit
8-
| cap is the universal root capability
7+
|where: => refers to a root capability associated with the result type of (using l: scala.caps.Capability^): (f: File^{l}) => Unit
8+
| ^ refers to the universal root capability
99
|
1010
|Note that capability l.type
1111
|cannot be included in outer capture set ? of parameter f.

‎tests/neg-custom-args/captures/i15923.check

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923.scala:12:21 ---------------------------------------
22
12 | val leak = withCap(cap => mkId(cap)) // error
33
| ^^^^^^^^^^^^^^^^
4-
|Found: (lcap: scala.caps.Capability^{cap.rd}) ?->? Cap^? ->? Id[Cap^?]^?
5-
|Required: (lcap: scala.caps.Capability^{cap.rd}) ?-> Cap^{lcap} => Id[Cap^?]^?
4+
|Found: (lcap: scala.caps.Capability^) ?->? Cap^? ->? Id[Cap^?]^?
5+
|Required: (lcap: scala.caps.Capability^) ?-> Cap^{lcap} => Id[Cap^?]^?
66
|
7-
|where: => refers to a root capability associated with the result type of (using lcap: scala.caps.Capability^{cap.rd}): Cap^{lcap} => Id[Cap^?]^?
8-
| cap is the universal root capability
7+
|where: => refers to a root capability associated with the result type of (using lcap: scala.caps.Capability^): Cap^{lcap} => Id[Cap^?]^?
8+
| ^ refers to the universal root capability
99
|
10-
|Note that capability <cap of (x$0: Cap^?): Id[Cap^?]^?>.rd
10+
|Note that capability <cap of (x$0: Cap^?): Id[Cap^?]^?>
1111
|cannot be included in outer capture set ?.
1212
|
1313
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/i21614.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
|
77
|where: ^ refers to a fresh root capability classified as SharedCapability created in anonymous function of type (f²: F): Logger when checking argument to parameter f of constructor Logger
88
|
9-
|Note that capability cap.rd is not included in capture set {cap}.
9+
|Note that capability cap is not included in capture set {cap}.
1010
|
1111
| longer explanation available when compiling with `-explain`
1212
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------

‎tests/neg-custom-args/captures/lazylists-exceptions.check

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
-- Error: tests/neg-custom-args/captures/lazylists-exceptions.scala:36:2 -----------------------------------------------
22
36 | try // error
33
| ^
4-
| The result of `try` cannot have type LazyList[Int]^{cap.rd} since
4+
| The result of `try` cannot have type LazyList[Int]^ since
55
| that type captures the root capability `cap`.
66
| This is often caused by a locally generated exception capability leaking as part of its result.
77
|
8-
| where: cap is a fresh root capability classified as Control in the type of given instance canThrow$1
8+
| where: ^ refers to a fresh root capability classified as Control in the type of given instance canThrow$1
99
37 | tabulate(10) { i =>
1010
38 | if i > 9 then throw Ex1()
1111
39 | i * i

0 commit comments

Comments
 (0)