Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 64b4e78

Browse files
oderskyodersky
committedFeb 13, 2025
Use peaks-based checking for types
1 parent 3c2a206 commit 64b4e78

File tree

6 files changed

+242
-173
lines changed

6 files changed

+242
-173
lines changed
 

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

+158-146
Large diffs are not rendered by default.

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

+26-16
Original file line numberDiff line numberDiff line change
@@ -19,24 +19,34 @@
1919
| Required: LazyRef[Int]^{ref1}
2020
|
2121
| longer explanation available when compiling with `-explain`
22-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:26:35 --------------------------------------
23-
26 | val ref4c: LazyRef[Int]^{cap1} = ref4 // error
22+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:30:35 --------------------------------------
23+
30 | val ref4c: LazyRef[Int]^{cap1} = ref4 // error
2424
| ^^^^
2525
| Found: LazyRef[Int]{val elem: () ->{ref4*} Int}^{ref4}
2626
| Required: LazyRef[Int]^{cap1}
2727
|
2828
| longer explanation available when compiling with `-explain`
29-
-- Error: tests/neg-custom-args/captures/lazyref.scala:25:55 -----------------------------------------------------------
30-
25 | val ref4 = (if cap1 == cap2 then ref1 else ref2).map(g) // error: separation failure
31-
| ^
32-
|Separation failure: argument of type (x: Int) ->{cap2} Int
33-
|to method map: [U](f: T => U): LazyRef[U]^{f, LazyRef.this}
34-
|corresponds to capture-polymorphic formal parameter f of type Int => Int
35-
|and hides capabilities {cap2}.
36-
|Some of these overlap with the captures of the function prefix with type (LazyRef[Int]{val elem: () ->{ref2*} Int} | (ref1 : LazyRef[Int]{val elem: () ->{cap1} Int}^{cap1}))^{ref2}.
37-
|
38-
| Hidden set of current argument : {cap2}
39-
| Hidden footprint of current argument : {cap2}
40-
| Capture set of function prefix : {ref1, ref2, ref2*}
41-
| Footprint set of function prefix : {ref1, ref2, ref2*, cap1, cap2}
42-
| The two sets overlap at : {cap2}
29+
-- Error: tests/neg-custom-args/captures/lazyref.scala:26:9 ------------------------------------------------------------
30+
26 | if cap1 == cap2 // error: separation failure // error: separation failure
31+
| ^^^^
32+
| Separation failure: Illegal access to {cap1} which is hidden by the previous definition
33+
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
34+
| This type hides capabilities {ref2*, cap1, cap2, ref1}
35+
-- Error: tests/neg-custom-args/captures/lazyref.scala:26:17 -----------------------------------------------------------
36+
26 | if cap1 == cap2 // error: separation failure // error: separation failure
37+
| ^^^^
38+
| Separation failure: Illegal access to {cap2} which is hidden by the previous definition
39+
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
40+
| This type hides capabilities {ref2*, cap1, cap2, ref1}
41+
-- Error: tests/neg-custom-args/captures/lazyref.scala:27:11 -----------------------------------------------------------
42+
27 | then ref1 // error: separation failure
43+
| ^^^^
44+
| Separation failure: Illegal access to {ref1} which is hidden by the previous definition
45+
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
46+
| This type hides capabilities {ref2*, cap1, cap2, ref1}
47+
-- Error: tests/neg-custom-args/captures/lazyref.scala:29:9 ------------------------------------------------------------
48+
29 | .map(g) // error: separation failure
49+
| ^
50+
| Separation failure: Illegal access to {cap2} which is hidden by the previous definition
51+
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
52+
| This type hides capabilities {ref2*, cap1, cap2, ref1}

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

+5-1
Original file line numberDiff line numberDiff line change
@@ -22,5 +22,9 @@ def test(cap1: Cap, cap2: Cap) =
2222
val ref2c: LazyRef[Int]^{cap2} = ref2 // error
2323
val ref3 = ref1.map(g)
2424
val ref3c: LazyRef[Int]^{ref1} = ref3 // error
25-
val ref4 = (if cap1 == cap2 then ref1 else ref2).map(g) // error: separation failure
25+
val ref4 = (
26+
if cap1 == cap2 // error: separation failure // error: separation failure
27+
then ref1 // error: separation failure
28+
else ref2)
29+
.map(g) // error: separation failure
2630
val ref4c: LazyRef[Int]^{cap1} = ref4 // error

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

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/sep-pairs.scala:32:10 ------------------------------------
2+
32 | Pair(Ref(), Ref()) // error // error: universal capability cannot be included in capture set
3+
| ^^^^^
4+
| Found: box Ref^{cap.rd, cap}
5+
| Required: box Ref^?
6+
|
7+
| Note that the universal capability `cap.rd`
8+
| cannot be included in capture set ?
9+
|
10+
| longer explanation available when compiling with `-explain`
11+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/sep-pairs.scala:32:17 ------------------------------------
12+
32 | Pair(Ref(), Ref()) // error // error: universal capability cannot be included in capture set
13+
| ^^^^^
14+
| Found: box Ref^{cap.rd, cap}
15+
| Required: box Ref^?
16+
|
17+
| Note that the universal capability `cap.rd`
18+
| cannot be included in capture set ?
19+
|
20+
| longer explanation available when compiling with `-explain`
21+
-- Error: tests/neg-custom-args/captures/sep-pairs.scala:15:10 ---------------------------------------------------------
22+
15 | val r1: Pair[Ref^, Ref^] = mkPair(r0) // error: overlap at r0
23+
| ^^^^^^^^^^^^^^^^
24+
| Separation failure in value r1's type Pair[box Ref^, box Ref^].
25+
| One part, box Ref^, hides capabilities {r0}.
26+
| Another part, box Ref^, captures capabilities {r0}.
27+
| The two sets overlap at {r0}.
28+
-- Error: tests/neg-custom-args/captures/sep-pairs.scala:13:9 ----------------------------------------------------------
29+
13 |def bad: Pair[Ref^, Ref^] = // error: overlap at r1*, r0
30+
| ^^^^^^^^^^^^^^^^
31+
| Separation failure in method bad's result type Pair[box Ref^, box Ref^].
32+
| One part, box Ref^, hides capabilities {cap, cap}.
33+
| Another part, box Ref^, captures capabilities {cap, cap}.
34+
| The two sets overlap at cap of method bad.
35+
-- Error: tests/neg-custom-args/captures/sep-pairs.scala:44:18 ---------------------------------------------------------
36+
44 | val sameToPair: Pair[Ref^, Ref^] = Pair(fstSame, sndSame) // error
37+
| ^^^^^^^^^^^^^^^^
38+
| Separation failure in value sameToPair's type Pair[box Ref^, box Ref^].
39+
| One part, box Ref^, hides capabilities {fstSame}.
40+
| Another part, box Ref^, captures capabilities {sndSame}.
41+
| The two sets overlap at cap of value same.

‎tests/neg-custom-args/captures/sep-pairs.scala

+6-4
Original file line numberDiff line numberDiff line change
@@ -36,10 +36,12 @@ def test(io: Object^): Unit =
3636
val two = twoRefs()
3737
val fst: Ref^{two.fst*} = two.fst
3838
val snd: Ref^{two.snd*} = two.snd
39+
val twoCopy: Pair[Ref^, Ref^] = Pair(fst, snd) // ok
40+
41+
val same = twoRefs2()
42+
val fstSame = same.fst
43+
val sndSame = same.snd
44+
val sameToPair: Pair[Ref^, Ref^] = Pair(fstSame, sndSame) // error
3945

40-
val two2 = twoRefs2()
41-
val fst2 = two.fst
42-
val snd2 = two.snd
4346

44-
val p2: Pair[Ref^, Ref^] = Pair(fst, snd) // should be error
4547

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

+6-6
Original file line numberDiff line numberDiff line change
@@ -22,22 +22,22 @@
2222
14 | val x1: (Object^, Object^) = (c, c) // error
2323
| ^^^^^^^^^^^^^^^^^^
2424
| Separation failure in value x1's type (box Object^, box Object^).
25-
| One part, box Object^ , hides {c}.
26-
| A previous part, box Object^ , also hides {c}.
25+
| One part, box Object^, hides capabilities {c}.
26+
| Another part, box Object^, captures capabilities {c}.
2727
| The two sets overlap at {c}.
2828
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:15:10 --------------------------------------------------------
2929
15 | val x2: (Object^, Object^{d}) = (d, d) // error
3030
| ^^^^^^^^^^^^^^^^^^^^^
3131
| Separation failure in value x2's type (box Object^, box Object^{d}).
32-
| One part, box Object^{d} , references {d}.
33-
| A previous part, box Object^ , hides {d}.
32+
| One part, box Object^, hides capabilities {d}.
33+
| Another part, box Object^{d}, captures capabilities {d}.
3434
| The two sets overlap at {d}.
3535
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:27:6 ---------------------------------------------------------
3636
27 | bar((c, c)) // error
3737
| ^^^^^^
3838
| Separation failure in the argument's adapted type (box Object^, box Object^).
39-
| One part, box Object^ , hides {c}.
40-
| A previous part, box Object^ , also hides {c}.
39+
| One part, box Object^, hides capabilities {c}.
40+
| Another part, box Object^, captures capabilities {c}.
4141
| The two sets overlap at {c}.
4242
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:30:9 ---------------------------------------------------------
4343
30 | val x: (Object^, Object^{c}) = (d, c) // error

0 commit comments

Comments
 (0)
Please sign in to comment.