Skip to content

Commit e8e3903

Browse files
LinyxusLinyxus
authored
Allow caps in result types of functions to be mapped to reaches (#23275)
Allow caps in result types of functions to be mapped to reach capabilities Example: If we have `val f: A => C^` then `f` has type `A => C^{f*}`. Before it had that type only if `A` was pure. On the other hand, result caps are not replaced anymore. We used to have for `val f: (x: A) => C^` with `A` pure that `f: (x: A) => C^{f*}`. That's no longer the case. In this case, `f` now has type `f: (x: A) => C^` with the `^` understood to be existentially bound. This aligns the implementation with the Capless paper.
2 parents 2703b6b + ce3d243 commit e8e3903

File tree

16 files changed

+182
-159
lines changed

16 files changed

+182
-159
lines changed

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

Lines changed: 12 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -155,8 +155,7 @@ object Capabilities:
155155

156156
object FreshCap:
157157
def apply(origin: Origin)(using Context): FreshCap | GlobalCap.type =
158-
if ccConfig.useSepChecks then FreshCap(ctx.owner, origin)
159-
else GlobalCap
158+
FreshCap(ctx.owner, origin)
160159

161160
/** A root capability associated with a function type. These are conceptually
162161
* existentially quantified over the function's result type.
@@ -716,14 +715,12 @@ object Capabilities:
716715
* the map being installed for future use.
717716
*/
718717
def capToFresh(tp: Type, origin: Origin)(using Context): Type =
719-
if ccConfig.useSepChecks then
720-
ccState.withoutMappedFutureElems:
721-
CapToFresh(origin)(tp)
722-
else tp
718+
ccState.withoutMappedFutureElems:
719+
CapToFresh(origin)(tp)
723720

724721
/** Maps fresh to cap */
725722
def freshToCap(tp: Type)(using Context): Type =
726-
if ccConfig.useSepChecks then CapToFresh(Origin.Unknown).inverse(tp) else tp
723+
CapToFresh(Origin.Unknown).inverse(tp)
727724

728725
/** Map top-level free existential variables one-to-one to Fresh instances */
729726
def resultToFresh(tp: Type, origin: Origin)(using Context): Type =
@@ -808,17 +805,14 @@ object Capabilities:
808805
case c @ ResultCap(`mt`) =>
809806
// do a reverse getOrElseUpdate on `seen` to produce the
810807
// `Fresh` assosicated with `t`
811-
if !ccConfig.useSepChecks then
812-
FreshCap(Origin.Unknown) // warning: this can cause cycles
813-
else
814-
val primary = c.primaryResultCap
815-
primary.origin match
816-
case GlobalCap =>
817-
val fresh = FreshCap(Origin.Unknown)
818-
primary.setOrigin(fresh)
819-
fresh
820-
case origin: FreshCap =>
821-
origin
808+
val primary = c.primaryResultCap
809+
primary.origin match
810+
case GlobalCap =>
811+
val fresh = FreshCap(Origin.Unknown)
812+
primary.setOrigin(fresh)
813+
fresh
814+
case origin: FreshCap =>
815+
origin
822816
case _ =>
823817
super.mapCapability(c, deep)
824818

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

Lines changed: 5 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -354,22 +354,15 @@ extension (tp: Type)
354354
def apply(t: Type) =
355355
if variance <= 0 then t
356356
else t.dealias match
357-
case t @ CapturingType(p, cs) if cs.containsTerminalCapability =>
357+
case t @ CapturingType(p, cs) if cs.containsCapOrFresh =>
358358
change = true
359359
val reachRef = if cs.isReadOnly then ref.reach.readOnly else ref.reach
360360
t.derivedCapturingType(apply(p), reachRef.singletonCaptureSet)
361361
case t @ AnnotatedType(parent, ann) =>
362362
// Don't map annotations, which includes capture sets
363363
t.derivedAnnotatedType(this(parent), ann)
364364
case t @ FunctionOrMethod(args, res) =>
365-
if args.forall(_.isAlwaysPure) then
366-
// Also map existentials in results to reach capabilities if all
367-
// preceding arguments are known to be always pure
368-
t.derivedFunctionOrMethod(
369-
args,
370-
apply(resultToFresh(res, Origin.ResultInstance(t, NoSymbol))))
371-
else
372-
t
365+
t.derivedFunctionOrMethod(args, apply(res))
373366
case _ =>
374367
mapOver(t)
375368
end narrowCaps
@@ -642,17 +635,15 @@ abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]:
642635
def apply(acc: T, t: Type) =
643636
if variance < 0 then acc
644637
else t.dealias match
645-
case t @ CapturingType(p, cs1) =>
646-
capturingCase(acc, p, cs1)
638+
case t @ CapturingType(parent, cs) =>
639+
capturingCase(acc, parent, cs)
647640
case t: TypeRef if t.symbol.isAbstractOrParamType && !seen.contains(t.symbol) =>
648641
seen += t.symbol
649642
abstractTypeCase(acc, t, t.info.bounds.hi)
650643
case AnnotatedType(parent, _) =>
651644
this(acc, parent)
652645
case t @ FunctionOrMethod(args, res) =>
653-
if args.forall(_.isAlwaysPure) then
654-
this(acc, resultToFresh(res, Origin.ResultInstance(t, NoSymbol)))
655-
else acc
646+
this(acc, res)
656647
case _ =>
657648
foldOver(acc, t)
658649
end DeepTypeAccumulator

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,21 @@ sealed abstract class CaptureSet extends Showable:
103103
final def containsTerminalCapability(using Context) =
104104
elems.exists(_.isTerminalCapability)
105105

106+
/** Does this capture set contain a ResultCap element? */
107+
final def containsResultCapability(using Context) =
108+
elems.exists(_.core.isInstanceOf[ResultCap])
109+
110+
/** Does this capture set contain a GlobalCap or FreshCap, and at the same time
111+
* does not contain a ResultCap?
112+
*/
113+
final def containsCapOrFresh(using Context) =
114+
!containsResultCapability
115+
&& elems.exists: elem =>
116+
elem.core match
117+
case GlobalCap => true
118+
case _: FreshCap => true
119+
case _ => false
120+
106121
final def containsCap(using Context) =
107122
elems.exists(_.core eq GlobalCap)
108123

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -46,14 +46,14 @@ object ccConfig:
4646
*/
4747
inline val postCheckCapturesets = false
4848

49-
/** If true, turn on separation checking */
50-
def useSepChecks(using Context): Boolean =
51-
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.8`)
52-
5349
/** If true, do level checking for FreshCap instances */
5450
def useFreshLevels(using Context): Boolean =
5551
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
5652

53+
/** If true, turn on separation checking */
54+
def useSepChecks(using Context): Boolean =
55+
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.8`)
56+
5757
/** Not used currently. Handy for trying out new features */
5858
def newScheme(using Context): Boolean =
5959
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -222,7 +222,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
222222
boxText
223223
~ toTextLocal(parent)
224224
~ "^"
225-
~ toTextGeneralCaptureSet(refs).provided(!isUniversalCaptureSet(refs))
225+
~ toTextGeneralCaptureSet(refs).provided(!isUniversalCaptureSet(refs) || ccVerbose)
226226

227227
def toText(tp: Type): Text = controlled {
228228
homogenize(tp) match {

‎tests/neg-custom-args/captures/cc-existential-conformance.check‎

Lines changed: 9 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -13,14 +13,13 @@
1313
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:9:29 --------------------
1414
9 | val z: A -> (x: A) -> B^ = y // error
1515
| ^
16-
| Found: (y : A -> A -> B^)
17-
| Required: A -> (x: A) -> B^²
16+
| Found: A -> A -> B^{y*}
17+
| Required: A -> (x: A) -> B^
1818
|
19-
| where: ^ refers to a fresh root capability in the type of value y
20-
| ^² refers to a root capability associated with the result type of (x: A): B^²
19+
| where: ^ refers to a root capability associated with the result type of (x: A): B^
2120
|
22-
| Note that the existential capture root in B^
23-
| cannot subsume the capability cap
21+
| Note that the existential capture root in B^
22+
| cannot subsume the capability y* since that capability is not a SharedCapability
2423
|
2524
| longer explanation available when compiling with `-explain`
2625
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:13:19 -------------------
@@ -38,13 +37,12 @@
3837
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:14:24 -------------------
3938
14 | val z: (x: A) -> B^ = y // error
4039
| ^
41-
| Found: (y : A -> B^)
42-
| Required: (x: A) -> B^²
40+
| Found: A -> B^{y*}
41+
| Required: (x: A) -> B^
4342
|
44-
| where: ^ refers to a fresh root capability in the type of value y
45-
| ^² refers to a root capability associated with the result type of (x: A): B^²
43+
| where: ^ refers to a root capability associated with the result type of (x: A): B^
4644
|
4745
| Note that the existential capture root in B^
48-
| cannot subsume the capability cap
46+
| cannot subsume the capability y* since that capability is not a SharedCapability
4947
|
5048
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/existential-mapping.check‎

Lines changed: 25 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,10 @@
1818
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:12:20 --------------------------
1919
12 | val _: C^ -> C = x2 // error
2020
| ^^
21-
| Found: (x2 : C^ -> C^²)
21+
| Found: C^ -> C^{x2*}
2222
| Required: C^ -> C
2323
|
24-
| where: ^ refers to the universal root capability
25-
| ^² refers to a fresh root capability in the type of value x2
24+
| where: ^ refers to the universal root capability
2625
|
2726
| longer explanation available when compiling with `-explain`
2827
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:15:30 --------------------------
@@ -38,11 +37,10 @@
3837
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:18:25 --------------------------
3938
18 | val _: A^ -> C^ -> C = x4 // error
4039
| ^^
41-
| Found: (x4 : A^ -> C^ -> C^²)
40+
| Found: A^ -> C^ -> C^{x4*}
4241
| Required: A^ -> C^ -> C
4342
|
44-
| where: ^ refers to the universal root capability
45-
| ^² refers to a fresh root capability in the type of value x4
43+
| where: ^ refers to the universal root capability
4644
|
4745
| longer explanation available when compiling with `-explain`
4846
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:21:30 --------------------------
@@ -58,13 +56,12 @@
5856
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:24:30 --------------------------
5957
24 | val _: A^ -> (x: C^) => C = x6 // error
6058
| ^^
61-
| Found: (x6 : A^ -> (x: C^) => C^²)
62-
| Required: A^ -> (x: C^) =>² C
59+
| Found: A^ -> (x: C^) ->{x6*} C^²
60+
| Required: A^ -> (x: C^) => C
6361
|
64-
| where: => refers to a fresh root capability in the type of value x6
65-
| =>² refers to a fresh root capability in the type of value _$6
66-
| ^ refers to the universal root capability
67-
| ^² refers to a root capability associated with the result type of (x: C^): C^²
62+
| where: => refers to a fresh root capability in the type of value _$6
63+
| ^ refers to the universal root capability
64+
| ^² refers to a root capability associated with the result type of (x: C^): C^²
6865
|
6966
| longer explanation available when compiling with `-explain`
7067
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:27:25 --------------------------
@@ -82,41 +79,34 @@
8279
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:30:20 --------------------------
8380
30 | val _: C^ => C = y2 // error
8481
| ^^
85-
| Found: (y2 : C^ => C^²)
86-
| Required: C^ =>² C
82+
| Found: C^ ->{y2} C^{y2*}
83+
| Required: C^ => C
8784
|
88-
| where: => refers to a fresh root capability in the type of value y2
89-
| =>² refers to a fresh root capability in the type of value _$8
90-
| ^ refers to the universal root capability
91-
| ^² refers to a fresh root capability in the type of value y2
85+
| where: => refers to a fresh root capability in the type of value _$8
86+
| ^ refers to the universal root capability
9287
|
9388
| longer explanation available when compiling with `-explain`
9489
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:33:30 --------------------------
9590
33 | val _: A^ => (x: C^) => C = y3 // error
9691
| ^^
97-
| Found: (y3 : A^ => (x: C^) =>² C^²)
98-
| Required: A^ =>³ (x: C^) =>⁴ C
92+
| Found: A^ ->{y3} (x: C^) ->{y3*} C^²
93+
| Required: A^ => (x: C^) =>² C
9994
|
100-
| where: => refers to a fresh root capability in the type of value y3
101-
| =>² refers to a fresh root capability in the type of value y3
102-
| =>³ refers to a fresh root capability in the type of value _$9
103-
| =>⁴ refers to a fresh root capability in the type of value _$9
95+
| where: => refers to a fresh root capability in the type of value _$9
96+
| =>² refers to a fresh root capability in the type of value _$9
10497
| ^ refers to the universal root capability
10598
| ^² refers to a root capability associated with the result type of (x: C^): C^²
10699
|
107100
| longer explanation available when compiling with `-explain`
108101
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:36:25 --------------------------
109102
36 | val _: A^ => C^ => C = y4 // error
110103
| ^^
111-
| Found: (y4 : A^ => C^ =>² C^²)
112-
| Required: A^ =>³ C^ =>⁴ C
104+
| Found: A^ ->{y4} C^ ->{y4*} C^{y4*}
105+
| Required: A^ => C^ =>² C
113106
|
114-
| where: => refers to a fresh root capability in the type of value y4
115-
| =>² refers to a fresh root capability in the type of value y4
116-
| =>³ refers to a fresh root capability in the type of value _$10
117-
| =>⁴ refers to a fresh root capability in the type of value _$10
107+
| where: => refers to a fresh root capability in the type of value _$10
108+
| =>² refers to a fresh root capability in the type of value _$10
118109
| ^ refers to the universal root capability
119-
| ^² refers to a fresh root capability in the type of value y4
120110
|
121111
| longer explanation available when compiling with `-explain`
122112
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:39:30 --------------------------
@@ -134,13 +124,11 @@
134124
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:42:30 --------------------------
135125
42 | val _: A^ => (x: C^) => C = y6 // error
136126
| ^^
137-
| Found: (y6 : A^ => (x: C^) =>² C^²)
138-
| Required: A^ =>³ (x: C^) =>⁴ C
127+
| Found: A^ ->{y6} (x: C^) ->{y6*} C^²
128+
| Required: A^ => (x: C^) =>² C
139129
|
140-
| where: => refers to a fresh root capability in the type of value y6
141-
| =>² refers to a fresh root capability in the type of value y6
142-
| =>³ refers to a fresh root capability in the type of value _$12
143-
| =>⁴ refers to a fresh root capability in the type of value _$12
130+
| where: => refers to a fresh root capability in the type of value _$12
131+
| =>² refers to a fresh root capability in the type of value _$12
144132
| ^ refers to the universal root capability
145133
| ^² refers to a root capability associated with the result type of (x: C^): C^²
146134
|

‎tests/neg-custom-args/captures/reach-in-results.scala‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
import language.experimental.captureChecking
2+
trait File
3+
def usingFile[R](op: File^ => R): R = op(new File {})
4+
def id(x: File^): File^{x} = x
5+
def test1(): Unit =
6+
val op: File^ -> File^ = id // error, this should be disallowed
7+
val g: File^ -> File^{op*} = op // otherwise we can brand arbitrary File as simply capturing op*

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

Lines changed: 2 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -65,18 +65,6 @@
6565
| ^² refers to a fresh root capability in the type of value id
6666
|
6767
| longer explanation available when compiling with `-explain`
68-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:38 --------------------------------------
69-
62 | val leaked = usingFile[File^{id*}]: f => // error // error
70-
| ^
71-
|Found: (f: File^?) ->? box File^?
72-
|Required: (f: File^) => box File^{id*}
73-
|
74-
|where: => refers to a fresh root capability created in value leaked when checking argument to parameter f of method usingFile
75-
| ^ refers to the universal root capability
76-
63 | val f1: File^{id*} = id(f)
77-
64 | f1
78-
|
79-
| longer explanation available when compiling with `-explain`
8068
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:67:32 --------------------------------------
8169
67 | val id: (x: File^) -> File^ = x => x // error
8270
| ^^^^^^
@@ -91,9 +79,9 @@
9179
|
9280
| longer explanation available when compiling with `-explain`
9381
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:70:38 --------------------------------------
94-
70 | val leaked = usingFile[File^{id*}]: f => // error // error
82+
70 | val leaked = usingFile[File^{id*}]: f => // error
9583
| ^
96-
|Found: (f: File^?) ->? box File^?
84+
|Found: (f: File^?) ->? box File^{id*}
9785
|Required: (f: File^) => box File^{id*}
9886
|
9987
|where: => refers to a fresh root capability created in value leaked when checking argument to parameter f of method usingFile
@@ -117,11 +105,3 @@
117105
| ^ refers to the universal root capability
118106
|
119107
| longer explanation available when compiling with `-explain`
120-
-- Error: tests/neg-custom-args/captures/reaches.scala:62:31 -----------------------------------------------------------
121-
62 | val leaked = usingFile[File^{id*}]: f => // error // error
122-
| ^^^
123-
| id* cannot be tracked since its deep capture set is empty
124-
-- Error: tests/neg-custom-args/captures/reaches.scala:70:31 -----------------------------------------------------------
125-
70 | val leaked = usingFile[File^{id*}]: f => // error // error
126-
| ^^^
127-
| id* cannot be tracked since its deep capture set is empty

‎tests/neg-custom-args/captures/reaches.scala‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -59,15 +59,15 @@ def attack2 =
5959
val id: File^ -> File^ = x => x // error
6060
// val id: File^ -> File^{fresh}
6161

62-
val leaked = usingFile[File^{id*}]: f => // error // error
62+
val leaked = usingFile[File^{id*}]: f => // now ok
6363
val f1: File^{id*} = id(f)
6464
f1
6565

6666
def attack3 =
6767
val id: (x: File^) -> File^ = x => x // error
6868
// val id: File^ -> EX C.File^C
6969

70-
val leaked = usingFile[File^{id*}]: f => // error // error
70+
val leaked = usingFile[File^{id*}]: f => // error
7171
val f1: File^{id*} = id(f)
7272
f1
7373

0 commit comments

Comments
 (0)