Skip to content

Commit 99a4c20

Browse files
oderskyodersky
committed
Turn level checking on under newScheme (which is on by default)
1 parent d581e54 commit 99a4c20

File tree

10 files changed

+179
-21
lines changed

10 files changed

+179
-21
lines changed

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

+18
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,8 @@ class CCState:
118118

119119
private var capIsRoot: Boolean = false
120120

121+
private var treatFreshAsEqual: Boolean = false
122+
121123
object CCState:
122124

123125
opaque type Level = Int
@@ -162,4 +164,20 @@ object CCState:
162164
/** Is `caps.cap` a root capability that is allowed to subsume other capabilities? */
163165
def capIsRoot(using Context): Boolean = ccState.capIsRoot
164166

167+
/** Run `op` under the assumption that all root.Fresh instances are equal.
168+
* Needed to make override checking of types containing fresh work.
169+
* Asserted in override checking, tested in maxSubsumes.
170+
* Is this sound? Test case is neg-custom-args/captures/leaked-curried.scala.
171+
*/
172+
inline def withTreatFreshAsEqual[T](op: => T)(using Context): T =
173+
if isCaptureCheckingOrSetup then
174+
val ccs = ccState
175+
val saved = ccs.treatFreshAsEqual
176+
ccs.treatFreshAsEqual = true
177+
try op finally ccs.treatFreshAsEqual = saved
178+
else op
179+
180+
/** Should all root.Fresh instances be treated equal? */
181+
def treatFreshAsEqual(using Context): Boolean = ccState.treatFreshAsEqual
182+
165183
end CCState

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

+13-3
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,9 @@ import compiletime.uninitialized
1414
import StdNames.nme
1515
import CaptureSet.VarState
1616
import Annotations.Annotation
17+
import Flags.*
1718
import config.Printers.capt
19+
import CCState.{Level, undefinedLevel}
1820

1921
object CaptureRef:
2022
opaque type Validity = Int
@@ -287,13 +289,21 @@ trait CaptureRef extends TypeProxy, ValueType:
287289
case _ => false
288290
(this eq y)
289291
|| this.match
290-
case root.Fresh(hidden) =>
291-
vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
292-
|| !y.stripReadOnly.isCap
292+
case x @ root.Fresh(hidden) =>
293+
def levelOK =
294+
if ccConfig.newScheme then
295+
val yOwner = y.adjustedOwner
296+
yOwner.isStatic || x.ccOwner.isContainedIn(yOwner)
297+
else
298+
!y.stripReadOnly.isCap
293299
&& !yIsExistential
294300
&& !y.isInstanceOf[ParamRef]
301+
302+
vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
303+
|| levelOK
295304
&& canAddHidden
296305
&& vs.addHidden(hidden, y)
306+
|| ccConfig.newScheme && CCState.treatFreshAsEqual && y.stripReadOnly.isFresh
297307
case x @ root.Result(binder) =>
298308
val result = y match
299309
case y @ root.Result(_) => vs.unify(x, y)

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,6 @@ object ccConfig:
5252

5353
/** Not used currently. Handy for trying out new features */
5454
def newScheme(using Context): Boolean =
55-
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.8`)
55+
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
5656

5757
end ccConfig

‎compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala

+3-1
Original file line numberDiff line numberDiff line change
@@ -225,6 +225,8 @@ object OverridingPairs:
225225
)
226226
else
227227
member.name.is(DefaultGetterName) // default getters are not checked for compatibility
228-
|| memberTp.overrides(otherTp, member.matchNullaryLoosely || other.matchNullaryLoosely || fallBack)
228+
||
229+
CCState.withTreatFreshAsEqual:
230+
memberTp.overrides(otherTp, member.matchNullaryLoosely || other.matchNullaryLoosely || fallBack)
229231

230232
end OverridingPairs

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

+12-2
Original file line numberDiff line numberDiff line change
@@ -31,16 +31,26 @@
3131
|
3232
| where: ^ refers to the universal root capability
3333
-- Error: tests/neg-custom-args/captures/i21401.scala:17:29 ------------------------------------------------------------
34-
17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
34+
17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error
3535
| ^^^^^^^^^^
3636
| Type variable R of value leaked cannot be instantiated to Boxed[box IO^] since
3737
| the part box IO^ of that type captures the root capability `cap`.
3838
|
3939
| where: ^ refers to the universal root capability
4040
-- Error: tests/neg-custom-args/captures/i21401.scala:17:52 ------------------------------------------------------------
41-
17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
41+
17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error
4242
| ^^^^^^^^^^^^^^^^^^^^^^^^
4343
| Type variable X of value leaked cannot be instantiated to Boxed[box IO^] -> Boxed[box IO^] since
4444
| the part box IO^ of that type captures the root capability `cap`.
4545
|
4646
| where: ^ refers to the universal root capability
47+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:17:67 ---------------------------------------
48+
17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error
49+
| ^^^^^^
50+
| Found: (x: Boxed[box IO^]^?) ->? Boxed[box IO^{x*}]^?
51+
| Required: (x: Boxed[box IO^]) -> Boxed[box IO^²]
52+
|
53+
| where: ^ refers to the universal root capability
54+
| ^² refers to a fresh root capability created in value x²
55+
|
56+
| longer explanation available when compiling with `-explain`

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,6 @@ def mkRes(x: IO^): Res =
1414
def test2() =
1515
val a = usingIO[IO^](x => x) // error // error
1616
val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error
17-
val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
17+
val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error
1818
val y: IO^{x*} = x.unbox // was error
1919
y.println("boom")

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

+11-10
Original file line numberDiff line numberDiff line change
@@ -72,16 +72,13 @@
7272
| ^² refers to a fresh root capability in the type of value id
7373
|
7474
| longer explanation available when compiling with `-explain`
75-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:38 --------------------------------------
76-
62 | val leaked = usingFile[File^{id*}]: f => // error // error
77-
| ^
78-
|Found: (f: File^?) ->? box File^?
79-
|Required: (f: File^) => box File^{id*}
75+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:63:27 --------------------------------------
76+
63 | val f1: File^{id*} = id(f) // error // error
77+
| ^^^^^
78+
| Found: File^
79+
| Required: File^{id*}
8080
|
81-
|where: => refers to a fresh root capability created in value leaked when checking argument to parameter f of method usingFile
82-
| ^ refers to the universal root capability
83-
63 | val f1: File^{id*} = id(f)
84-
64 | f1
81+
| where: ^ refers to a fresh root capability in the type of value id
8582
|
8683
| longer explanation available when compiling with `-explain`
8784
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:67:32 --------------------------------------
@@ -126,9 +123,13 @@
126123
|
127124
| longer explanation available when compiling with `-explain`
128125
-- Error: tests/neg-custom-args/captures/reaches.scala:62:31 -----------------------------------------------------------
129-
62 | val leaked = usingFile[File^{id*}]: f => // error // error
126+
62 | val leaked = usingFile[File^{id*}]: f => // error
130127
| ^^^
131128
| id* cannot be tracked since its deep capture set is empty
129+
-- Error: tests/neg-custom-args/captures/reaches.scala:63:18 -----------------------------------------------------------
130+
63 | val f1: File^{id*} = id(f) // error // error
131+
| ^^^
132+
| id* cannot be tracked since its deep capture set is empty
132133
-- Error: tests/neg-custom-args/captures/reaches.scala:70:31 -----------------------------------------------------------
133134
70 | val leaked = usingFile[File^{id*}]: f => // error // error
134135
| ^^^

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -59,8 +59,8 @@ 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
63-
val f1: File^{id*} = id(f)
62+
val leaked = usingFile[File^{id*}]: f => // error
63+
val f1: File^{id*} = id(f) // error // error
6464
f1
6565

6666
def attack3 =

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

+117
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:7:20 -----------------------------------
2+
7 | val g: A^ -> B^ = f // error
3+
| ^
4+
| Found: (f : (x: A^) -> B^²)
5+
| Required: A^ -> B^³
6+
|
7+
| where: ^ refers to the universal root capability
8+
| ^² refers to a root capability associated with the result type of (x: A^): B^²
9+
| ^³ refers to a fresh root capability in the type of value g
10+
|
11+
| longer explanation available when compiling with `-explain`
12+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:9:25 -----------------------------------
13+
9 | val _: (x: A^) -> B^ = g // error
14+
| ^
15+
| Found: (g : A^ -> B^²)
16+
| Required: (x: A^) -> B^³
17+
|
18+
| where: ^ refers to the universal root capability
19+
| ^² refers to a fresh root capability in the type of value g
20+
| ^³ refers to a root capability associated with the result type of (x: A^): B^³
21+
|
22+
|
23+
| Note that the existential capture root in B^
24+
| cannot subsume the capability cap
25+
|
26+
| longer explanation available when compiling with `-explain`
27+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:10:20 ----------------------------------
28+
10 | val _: A^ -> B^ = f // error
29+
| ^
30+
| Found: (f : (x: A^) -> B^²)
31+
| Required: A^ -> B^³
32+
|
33+
| where: ^ refers to the universal root capability
34+
| ^² refers to a root capability associated with the result type of (x: A^): B^²
35+
| ^³ refers to a fresh root capability in the type of value _$3
36+
|
37+
| longer explanation available when compiling with `-explain`
38+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:12:20 ----------------------------------
39+
12 | val _: A^ -> B^ = x => g(x) // error, since g is pure, g(x): B^{x} , which does not match B^{fresh}
40+
| ^^^^^^^^^
41+
| Found: (x: A^) ->? B^{x}
42+
| Required: (x: A^) -> B^²
43+
|
44+
| where: ^ refers to the universal root capability
45+
| ^² refers to a fresh root capability in the type of value _$5
46+
|
47+
| longer explanation available when compiling with `-explain`
48+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:13:25 ----------------------------------
49+
13 | val _: (x: A^) -> B^ = x => f(x) // error: existential in B cannot subsume `x` since `x` is not shared
50+
| ^^^^^^^^^
51+
| Found: (x: A^) ->? B^{x}
52+
| Required: (x: A^) -> B^²
53+
|
54+
| where: ^ refers to the universal root capability
55+
| ^² refers to a root capability associated with the result type of (x: A^): B^²
56+
|
57+
|
58+
| Note that the existential capture root in B^
59+
| cannot subsume the capability x.type since that capability is not a SharedCapability
60+
|
61+
| longer explanation available when compiling with `-explain`
62+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:16:24 ----------------------------------
63+
16 | val _: (x: S) -> B^ = h // error: direct conversion fails
64+
| ^
65+
| Found: (h : S -> B^)
66+
| Required: (x: S) -> B^²
67+
|
68+
| where: ^ refers to a fresh root capability in the type of value h
69+
| ^² refers to a root capability associated with the result type of (x: S): B^²
70+
|
71+
|
72+
| Note that the existential capture root in B^
73+
| cannot subsume the capability cap
74+
|
75+
| longer explanation available when compiling with `-explain`
76+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:22:19 ----------------------------------
77+
22 | val _: S -> B^ = j // error
78+
| ^
79+
| Found: (j : (x: S) -> B^)
80+
| Required: S -> B^²
81+
|
82+
| where: ^ refers to a root capability associated with the result type of (x: S): B^
83+
| ^² refers to a fresh root capability in the type of value _$11
84+
|
85+
| longer explanation available when compiling with `-explain`
86+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:23:19 ----------------------------------
87+
23 | val _: S -> B^ = x => j(x) // error
88+
| ^^^^^^^^^
89+
| Found: (x: S) ->? B^{x}
90+
| Required: (x: S) -> B^
91+
|
92+
| where: ^ refers to a fresh root capability in the type of value _$12
93+
|
94+
| longer explanation available when compiling with `-explain`
95+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:26:20 ----------------------------------
96+
26 | val _: A^ => B^ = x => g2(x) // error: g2(x): B^{g2, x}, and the `x` cannot be subsumed by fresh
97+
| ^^^^^^^^^^
98+
| Found: (x: A^) ->{g2} B^²
99+
| Required: (x: A^) => B^³
100+
|
101+
| where: => refers to a fresh root capability in the type of value _$13
102+
| ^ refers to the universal root capability
103+
| ^² refers to a root capability associated with the result type of (x: A^): B^²
104+
| ^³ refers to a fresh root capability in the type of value _$13
105+
|
106+
| longer explanation available when compiling with `-explain`
107+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:28:24 ----------------------------------
108+
28 | val _: A^{io} => B^ = x => g3(x) // error, fails level checking of fresh instances
109+
| ^^^^^^^^^^
110+
| Found: (x: A^{io}) ->{g3} B^
111+
| Required: (x: A^{io}) => B^²
112+
|
113+
| where: => refers to a fresh root capability in the type of value _$14
114+
| ^ refers to a root capability associated with the result type of (x: A^{io}): B^
115+
| ^² refers to a fresh root capability in the type of value _$14
116+
|
117+
| longer explanation available when compiling with `-explain`

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -25,4 +25,4 @@ def test(io: Object^): Unit =
2525
val g2: A^ => B^ = ???
2626
val _: A^ => B^ = x => g2(x) // error: g2(x): B^{g2, x}, and the `x` cannot be subsumed by fresh
2727
val g3: A^ => B^ = ???
28-
val _: A^{io} => B^ = x => g3(x) // ok, now g3(x): B^{g3, x}, which is widened to B^{g3, io}
28+
val _: A^{io} => B^ = x => g3(x) // error, fails level checking of fresh instances

0 commit comments

Comments
 (0)