Skip to content

Commit 1a56647

Browse files
oderskyodersky
committed
Include capabilities of function results in CaptureSet.ofInfo
Include result capabilities unless they are bound in the result.
1 parent ab77e62 commit 1a56647

File tree

6 files changed

+55
-28
lines changed

6 files changed

+55
-28
lines changed

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

Lines changed: 12 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -439,6 +439,15 @@ sealed abstract class CaptureSet extends Showable:
439439
case fresh: FreshCap => fresh.hiddenSet.adoptClassifier(cls)
440440
case _ =>
441441

442+
/** All capabilities of this set except those Termrefs and FreshCaps that
443+
* are boundby `mt`.
444+
*/
445+
def freeInResult(mt: MethodicType)(using Context): CaptureSet =
446+
filter:
447+
case TermParamRef(binder, _) => binder ne mt
448+
case ResultCap(binder) => binder ne mt
449+
case _ => true
450+
442451
/** A bad root `elem` is inadmissible as a member of this set. What is a bad roots depends
443452
* on the value of `rootLimit`.
444453
* If the limit is null, all capture roots are good.
@@ -1523,14 +1532,10 @@ object CaptureSet:
15231532
// `ref` will not seem subsumed by other capabilities in a `++`.
15241533
universal
15251534
case c: CoreCapability =>
1526-
ofType(c.underlying, followResult = false)
1535+
ofType(c.underlying, followResult = true)
15271536

15281537
/** Capture set of a type
15291538
* @param followResult If true, also include capture sets of function results.
1530-
* This mode is currently not used. It could be interesting
1531-
* when we change the system so that the capture set of a function
1532-
* is the union of the capture sets if its span.
1533-
* In this case we should use `followResult = true` in the call in ofInfo above.
15341539
*/
15351540
def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =
15361541
def recur(tp: Type): CaptureSet = trace(i"ofType $tp, ${tp.getClass} $followResult", show = true):
@@ -1546,13 +1551,9 @@ object CaptureSet:
15461551
recur(parent) ++ refs
15471552
case tp @ AnnotatedType(parent, ann) if ann.symbol.isRetains =>
15481553
recur(parent) ++ ann.tree.toCaptureSet
1549-
case tpd @ defn.RefinedFunctionOf(rinfo: MethodType) if followResult =>
1554+
case tpd @ defn.RefinedFunctionOf(rinfo: MethodOrPoly) if followResult =>
15501555
ofType(tpd.parent, followResult = false) // pick up capture set from parent type
1551-
++ recur(rinfo.resType) // add capture set of result
1552-
.filter:
1553-
case TermParamRef(binder, _) => binder ne rinfo
1554-
case ResultCap(binder) => binder ne rinfo
1555-
case _ => true
1556+
++ recur(rinfo.resType).freeInResult(rinfo) // add capture set of result
15561557
case tpd @ AppliedType(tycon, args) =>
15571558
if followResult && defn.isNonRefinedFunction(tpd) then
15581559
recur(args.last)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -491,7 +491,7 @@ class CheckCaptures extends Recheck, SymTransformer:
491491
case _ => c.core match
492492
case c1: RootCapability => c1.singletonCaptureSet
493493
case c1: CoreCapability =>
494-
CaptureSet.ofType(c1.widen, followResult = false)
494+
CaptureSet.ofType(c1.widen, followResult = true)
495495
capt.println(i"Widen reach $c to $underlying in ${env.owner}")
496496
underlying.disallowRootCapability(NoSymbol): () =>
497497
report.error(em"Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set", tree.srcPos)

‎compiler/src/dotty/tools/dotc/core/Types.scala

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3743,6 +3743,7 @@ object Types extends TypeUtils {
37433743
// is that most poly types are cyclic via poly params,
37443744
// and therefore two different poly types would never be equal.
37453745

3746+
/** Common base trait of MethodType, PolyType and ExprType */
37463747
trait MethodicType extends TermType:
37473748
def resType: Type
37483749

‎tests/neg-custom-args/captures/scoped-caps.check

Lines changed: 32 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,18 @@
3636
| Note that capability <cap of (x: A^): B^> is not included in capture set {cap}.
3737
|
3838
| longer explanation available when compiling with `-explain`
39+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:12:20 ----------------------------------
40+
12 | val _: A^ -> B^ = x => g(x) // error: g is no longer pure, since it contains the ^ of B
41+
| ^^^^^^^^^
42+
| Found: (x: A^) ->{g} B^{g*}
43+
| Required: A^ -> B^²
44+
|
45+
| where: ^ refers to the universal root capability
46+
| ^² refers to a fresh root capability in the type of value _$5
47+
|
48+
| Note that capability (g : A^ -> B^) is not included in capture set {}.
49+
|
50+
| longer explanation available when compiling with `-explain`
3951
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:13:25 ----------------------------------
4052
13 | val _: (x: A^) -> B^ = x => f(x) // error: existential in B cannot subsume `x` since `x` is not shared
4153
| ^^^^^^^^^
@@ -63,35 +75,47 @@
6375
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:17:24 ----------------------------------
6476
17 | val _: (x: S) -> B^ = (x: S) => h(x) // error: eta expansion fails
6577
| ^^^^^^^^^^^^^^
66-
| Found: (x: S^{cap.rd}) ->? B^{h*}
78+
| Found: (x: S^{cap.rd}) ->{h} B^{h*}
6779
| Required: (x: S^{cap.rd}) -> B^
6880
|
6981
| where: ^ refers to a root capability associated with the result type of (x: S^{cap.rd}): B^
7082
| cap is the universal root capability
7183
|
72-
| Note that capability h* is not included in capture set {<cap of (x: S^{cap.rd}): B^{h*}>}.
84+
| Note that capability (h : S -> B^) is not included in capture set {}.
7385
|
7486
| longer explanation available when compiling with `-explain`
75-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:26:19 ----------------------------------
76-
26 | val _: S -> B^ = j // error
87+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:21:23 ----------------------------------
88+
21 | val _: (x: S) -> S = (x: S) => h2(x) // error: eta conversion fails since `h2` is now impure (result type S is a capability)
89+
| ^^^^^^^^^^^^^^^
90+
| Found: (x: S^{cap.rd}) ->{h2} S^{h2*.rd}
91+
| Required: (x: S^{cap.rd}) -> S^{cap².rd}
92+
|
93+
| where: cap is the universal root capability
94+
| cap² is a root capability associated with the result type of (x: S^{cap.rd}): S^{cap².rd}
95+
|
96+
| Note that capability (h2 : S -> S) is not included in capture set {}.
97+
|
98+
| longer explanation available when compiling with `-explain`
99+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:19 ----------------------------------
100+
27 | val _: S -> B^ = j // error
77101
| ^
78102
| Found: (j : (x: S) -> B^)
79103
| Required: S^{cap.rd} -> B^²
80104
|
81105
| where: ^ refers to a root capability associated with the result type of (x: S^{cap.rd}): B^
82-
| ^² refers to a fresh root capability in the type of value _$13
106+
| ^² refers to a fresh root capability in the type of value _$14
83107
| cap is the universal root capability
84108
|
85109
| Note that capability <cap of (x: S^{cap.rd}): B^> is not included in capture set {cap}.
86110
|
87111
| longer explanation available when compiling with `-explain`
88-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:19 ----------------------------------
89-
27 | val _: S -> B^ = x => j(x) // error
112+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:28:19 ----------------------------------
113+
28 | val _: S -> B^ = x => j(x) // error
90114
| ^^^^^^^^^
91115
| Found: (x: S^{cap.rd}) ->? B^{x}
92116
| Required: S^{cap.rd} -> B^
93117
|
94-
| where: ^ refers to a fresh root capability in the type of value _$14
118+
| where: ^ refers to a fresh root capability in the type of value _$15
95119
| cap is the universal root capability
96120
|
97121
| Note that capability x.type is not included in capture set {cap}.

‎tests/neg-custom-args/captures/scoped-caps.scala

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ def test(io: Object^): Unit =
99
val _: (x: A^) -> B^ = g // error
1010
val _: A^ -> B^ = f // error
1111
val _: A^ -> B^ = g
12-
val _: A^ -> B^ = x => g(x) // now ok, was error: since g is pure, g(x): B^{x} , which does not match B^{fresh}
12+
val _: A^ -> B^ = x => g(x) // error: g is no longer pure, since it contains the ^ of B
1313
val _: (x: A^) -> B^ = x => f(x) // error: existential in B cannot subsume `x` since `x` is not shared
1414

1515
val h: S -> B^ = ???
@@ -18,7 +18,8 @@ def test(io: Object^): Unit =
1818

1919
val h2: S -> S = ???
2020
val _: (x: S) -> S = h2 // direct conversion OK for shared S
21-
val _: (x: S) -> S = (x: S) => h2(x) // eta conversion is also OK
21+
val _: (x: S) -> S = (x: S) => h2(x) // error: eta conversion fails since `h2` is now impure (result type S is a capability)
22+
val _: (x: S) ->{h2} S = (x: S) => h2(x) // eta expansion OK
2223

2324
val j: (x: S) -> B^ = ???
2425
val _: (x: S) -> B^ = j

‎tests/neg-custom-args/captures/sep-use2.check

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -47,15 +47,15 @@
4747
24 | { f(c) } // error
4848
| ^
4949
|Separation failure: argument of type (c : Object^)
50-
|to a function of type Object^ ->{f} Object^{f*}
50+
|to a function of type Object^ ->{c} Object^{f*}
5151
|corresponds to capture-polymorphic formal parameter v1 of type Object^²
5252
|and hides capabilities {c}.
5353
|Some of these overlap with the captures of the function prefix.
5454
|
5555
| Hidden set of current argument : {c}
5656
| Hidden footprint of current argument : {c}
57-
| Capture set of function prefix : {f*}
58-
| Footprint set of function prefix : {f*, c}
57+
| Capture set of function prefix : {c, f*}
58+
| Footprint set of function prefix : {c, f*}
5959
| The two sets overlap at : {c}
6060
|
6161
|where: ^ refers to a fresh root capability in the type of parameter c
@@ -69,15 +69,15 @@
6969
28 | { f(c) } // error
7070
| ^
7171
|Separation failure: argument of type (c : Object^)
72-
|to a function of type Object^ ->{f} Object^{f*}
72+
|to a function of type Object^ ->{c} Object^{f*}
7373
|corresponds to capture-polymorphic formal parameter v1 of type Object^²
7474
|and hides capabilities {c}.
7575
|Some of these overlap with the captures of the function prefix.
7676
|
7777
| Hidden set of current argument : {c}
7878
| Hidden footprint of current argument : {c}
79-
| Capture set of function prefix : {f*}
80-
| Footprint set of function prefix : {f*, c}
79+
| Capture set of function prefix : {c, f*}
80+
| Footprint set of function prefix : {c, f*}
8181
| The two sets overlap at : {c}
8282
|
8383
|where: ^ refers to a fresh root capability in the type of parameter c

0 commit comments

Comments
 (0)