Skip to content

Commit 30971b5

Browse files
oderskyodersky
committed
Open existential scopes only for (x: T) => U functions
Parametric functions `A -> B` or `A => B` do not open an existential scope anymore. Hence, a function of the form ```scala def f(x: A => B^) ``` is capture polymorphic in both the function effect and the function result effect. On the other hand, ```scala def f(x: (y: A) => B^) ``` would be a function that can be passed only arguments that return a fresh result on each call.
1 parent 0f0a5b3 commit 30971b5

25 files changed

+175
-81
lines changed

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

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -540,11 +540,13 @@ extension (tp: Type)
540540
case t @ AnnotatedType(parent, ann) =>
541541
// Don't map annotations, which includes capture sets
542542
t.derivedAnnotatedType(this(parent), ann)
543-
case t @ FunctionOrMethod(args, res)
544-
if args.forall(_.isAlwaysPure) =>
545-
// Also map existentials in results to reach capabilities if all
546-
// preceding arguments are known to be always pure
547-
t.derivedFunctionOrMethod(args, apply(Existential.toCap(res)))
543+
case t @ FunctionOrMethod(args, res) =>
544+
if args.forall(_.isAlwaysPure) then
545+
// Also map existentials in results to reach capabilities if all
546+
// preceding arguments are known to be always pure
547+
t.derivedFunctionOrMethod(args, apply(Existential.toCap(res)))
548+
else
549+
t
548550
case _ =>
549551
mapOver(t)
550552
end narrowCaps

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

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -252,18 +252,23 @@ trait CaptureRef extends TypeProxy, ValueType:
252252
* fail a comparison.
253253
*/
254254
def maxSubsumes(y: CaptureRef, canAddHidden: Boolean)(using ctx: Context, vs: VarState = VarState.Separate): Boolean =
255+
def yIsExistential = y.stripReadOnly match
256+
case Existential.Vble(_) =>
257+
capt.println(i"failed existential $this >: $y")
258+
true
259+
case _ => false
255260
(this eq y)
256261
|| this.match
257262
case Fresh(hidden) =>
258263
vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
259-
|| !y.stripReadOnly.isCap && canAddHidden && vs.addHidden(hidden, y)
264+
|| !y.stripReadOnly.isCap && !yIsExistential && canAddHidden && vs.addHidden(hidden, y)
260265
case Existential.Vble(binder) =>
261266
y.stripReadOnly match
262267
case Existential.Vble(binder1) => binder1.hasSuffix(binder)
263268
.showing(i"cmp existential $binder maxSubsumes $binder1 = $result", capt)
264269
case _ => true
265270
case _ =>
266-
this.isCap && canAddHidden && vs != VarState.HardSeparate
271+
this.isCap /*&& !yIsExistential*/ && canAddHidden && vs != VarState.HardSeparate
267272
|| y.match
268273
case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)
269274
case _ => false

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1260,7 +1260,7 @@ class CheckCaptures extends Recheck, SymTransformer:
12601260
if isCompatible(actualBoxed, expected1) then
12611261
if debugSuccesses then tree match
12621262
case Ident(_) =>
1263-
println(i"SUCCESS $tree:\n${TypeComparer.explained(_.isSubType(actual, expected))}")
1263+
println(i"SUCCESS $tree for $actual <:< $expected:\n${TypeComparer.explained(_.isSubType(actualBoxed, expected1))}")
12641264
case _ =>
12651265
actualBoxed
12661266
else

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -281,7 +281,8 @@ object Existential:
281281
seen.getOrElseUpdate(t, Vble(mt))
282282
else
283283
if variance == 0 then
284-
fail(em"""$tp captures the root capability `cap` in invariant position""")
284+
fail(em"""$tp captures the root capability `cap` in invariant position.
285+
|This capability cannot be converted to an existential in the result type of a function.""")
285286
// we accept variance < 0, and leave the cap as it is
286287
super.mapOver(t)
287288
case defn.FunctionNOf(args, res, contextual) if t.typeSymbol.name.isImpureFunction =>

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -403,7 +403,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
403403
&& (!sym.isConstructor || (t ne tp.finalResultType))
404404
// Don't add ^ to result types of class constructors deriving from Capability
405405
then CapturingType(t, defn.universalCSImpliedByCapability, boxed = false)
406-
else normalizeCaptures(normalizeFunctions(mapFollowingAliases(t), t))
406+
else normalizeCaptures(mapFollowingAliases(t))
407407

408408
def innerApply(t: Type) =
409409
t match
@@ -438,9 +438,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
438438
keptFunAliases = true
439439
mapOver(t)
440440
else
441-
// In the second pass, map the alias and make sure it has the form
442-
// of a dependent function.
443-
normalizeFunctions(apply(t.dealias), t, expandAlways = true)
441+
// In the second pass, map the alias
442+
apply(t.dealias)
444443
case t =>
445444
defaultApply(t)
446445
end toCapturing

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -321,10 +321,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
321321
// This is safe because X$ self-type is X.type
322322
sym1 = sym1.companionModule
323323
if (sym1 ne NoSymbol) && (sym1 eq sym2) then
324-
ctx.erasedTypes ||
325-
sym1.isStaticOwner ||
326-
isSubPrefix(tp1.prefix, tp2.prefix) ||
327-
thirdTryNamed(tp2)
324+
ctx.erasedTypes
325+
|| sym1.isStaticOwner
326+
|| isSubPrefix(tp1.prefix, tp2.prefix)
327+
|| thirdTryNamed(tp2)
328328
else
329329
(tp1.name eq tp2.name)
330330
&& !sym1.is(Private)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1124,7 +1124,7 @@ object Types extends TypeUtils {
11241124
TypeComparer.topLevelSubType(this, that)
11251125
}
11261126

1127-
/** Is this type a subtype of that type? */
1127+
/** Is this type a subtype of that type without adding to the constraint? */
11281128
final def frozen_<:<(that: Type)(using Context): Boolean = {
11291129
record("frozen_<:<")
11301130
TypeComparer.isSubTypeWhenFrozen(this, that)

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
260260
def isUniversal =
261261
refs.elems.size == 1
262262
&& (refs.isUniversal
263-
|| !printDebug && !showUniqueIds && refs.elems.nth(0).match
263+
|| !printDebug && !printFresh && !showUniqueIds && refs.elems.nth(0).match
264264
case Existential.Vble(binder) =>
265265
CCState.openExistentialScopes match
266266
case b :: _ => binder eq b
@@ -459,7 +459,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
459459
val vbleText: Text = CCState.openExistentialScopes.indexOf(binder) match
460460
case -1 =>
461461
"<cap of " ~ toText(binder) ~ ">"
462-
case n => "outer_" * n ++ "cap"
462+
case n => "outer_" * n ++ (if printFresh then "localcap" else "cap")
463463
vbleText ~ hashStr(binder)
464464
case Fresh(hidden) =>
465465
val idStr = if showUniqueIds then s"#${hidden.id}" else ""

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -190,8 +190,8 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
190190
val capturesRoot = refs == rootSetText
191191
if cc.isCaptureCheckingOrSetup
192192
&& tp.allParamNamesSynthetic && !tp.looksDependent
193-
&& !showUniqueIds && !printDebug
194-
then
193+
&& !showUniqueIds && !printDebug && !printFresh
194+
then
195195
// cc.Setup converts all functions to dependent functions. Undo that when printing.
196196
toTextFunction(tp.paramInfos, tp.resType, tp, refs.provided(!capturesRoot), isContextual, isPure && !capturesRoot)
197197
else

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

Lines changed: 24 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,24 @@
1-
-- Error: tests/neg-custom-args/captures/boundschecks3.scala:11:13 -----------------------------------------------------
2-
11 | val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
3-
| ^^^^^^
4-
| test.C[box test.Tree^] captures the root capability `cap` in invariant position
1+
-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:9:11 ---------------------------------
2+
9 | val foo: C[Tree^] = ??? // error
3+
| ^
4+
| Type argument box test.Tree^ does not conform to upper bound test.Tree in inferred type test.C[box test.Tree^]
5+
|
6+
| longer explanation available when compiling with `-explain`
7+
-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:10:11 --------------------------------
8+
10 | type T = C[Tree^] // error
9+
| ^
10+
| Type argument box test.Tree^ does not conform to upper bound test.Tree in inferred type test.C[box test.Tree^]
11+
|
12+
| longer explanation available when compiling with `-explain`
13+
-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:11:11 --------------------------------
14+
11 | val bar: T -> T = ??? // error
15+
| ^
16+
|Type argument box test.Tree^ does not conform to upper bound test.Tree in subpart test.C[box test.Tree^] of inferred type test.C[box test.Tree^] -> test.C[box test.Tree^]
17+
|
18+
| longer explanation available when compiling with `-explain`
19+
-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:12:11 --------------------------------
20+
12 | val baz: C[Tree^] -> Unit = ??? // error
21+
| ^
22+
|Type argument box test.Tree^ does not conform to upper bound test.Tree in subpart test.C[box test.Tree^] of inferred type test.C[box test.Tree^] -> Unit
23+
|
24+
| longer explanation available when compiling with `-explain`

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ object test {
66

77
class C[X <: Tree](x: X)
88

9-
val foo: C[Tree^] = ??? // hidden error
10-
type T = C[Tree^] // hidden error
11-
val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
12-
val baz: C[Tree^] -> Unit = ??? // hidden error
9+
val foo: C[Tree^] = ??? // error
10+
type T = C[Tree^] // error
11+
val bar: T -> T = ??? // error
12+
val baz: C[Tree^] -> Unit = ??? // error
1313
}

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

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,20 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:8:24 --------------------
22
8 | val y: A -> Fun[B^] = x // error
33
| ^
4-
| Found: (x : A -> A -> B^)
5-
| Required: A -> A -> B^{outer_cap}
4+
| Found: (x : A -> (x²: A) -> B^{localcap})
5+
| Required: A -> A -> B^{fresh}
6+
|
7+
| where: x is a value in method test
8+
| x² is a reference to a value parameter
69
|
710
| longer explanation available when compiling with `-explain`
11+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:13:19 -------------------
12+
13 | val y: Fun[B^] = x // error
13+
| ^
14+
| Found: (x : (x²: A) -> B^{localcap})
15+
| Required: A -> B^{fresh}
16+
|
17+
| where: x is a value in method test2
18+
| x² is a reference to a value parameter
19+
|
20+
| longer explanation available when compiling with `-explain`

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,11 @@ class B
44
type Fun[T] = A -> T
55

66
def test() =
7-
val x: A -> A -> B^ = ???
7+
val x: A -> (x: A) -> B^ = ???
88
val y: A -> Fun[B^] = x // error
99
val z: A -> A -> B^ = y // ok
1010

1111
def test2() =
12-
val x: A -> B^ = ???
13-
val y: Fun[B^] = x // should be error
12+
val x: (x: A) -> B^ = ???
13+
val y: Fun[B^] = x // error
1414
val z: A -> B^ = y // ok

‎tests/neg-custom-args/captures/depfun-reach.check

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:19:4 ----------------------------------
22
19 | op // error
33
| ^^
4-
| Found: (xs: List[(X, box () ->{io} Unit)]) ->{op} List[box () ->{xs*} Unit]
4+
| Found: (op : (xs: List[(X, box () ->{io} Unit)]) => List[box () ->{xs*} Unit])
55
| Required: (xs: List[(X, box () ->{io} Unit)]) => List[() -> Unit]
66
|
77
| longer explanation available when compiling with `-explain`
88
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:26:60 ---------------------------------
99
26 | val b: (xs: List[() ->{io} Unit]) => List[() ->{} Unit] = a // error
1010
| ^
11-
| Found: (xs: List[box () ->{io} Unit]) ->{a} List[box () ->{xs*} Unit]
12-
| Required: (xs: List[box () ->{io} Unit]) => List[() -> Unit]
11+
| Found: (a : (xs: List[box () ->{io} Unit]) => List[box () ->{xs*} Unit])
12+
| Required: (xs: List[box () ->{io} Unit]) => List[() -> Unit]
1313
|
1414
| longer explanation available when compiling with `-explain`
1515
-- Error: tests/neg-custom-args/captures/depfun-reach.scala:18:17 ------------------------------------------------------

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

Lines changed: 21 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,88 +1,89 @@
1-
-- Error: tests/neg-custom-args/captures/existential-mapping.scala:44:13 -----------------------------------------------
2-
44 | val z1: A^ => Array[C^] = ??? // error
3-
| ^^^^^^^^^^^^^^^
4-
| Array[box C^] captures the root capability `cap` in invariant position
1+
-- Error: tests/neg-custom-args/captures/existential-mapping.scala:46:10 -----------------------------------------------
2+
46 | val z2: (x: A^) => Array[C^] = ??? // error
3+
| ^^^^^^^^^^^^^^^^^^^^
4+
| Array[box C^] captures the root capability `cap` in invariant position.
5+
| This capability cannot be converted to an existential in the result type of a function.
56
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:9:25 ---------------------------
67
9 | val _: (x: C^) -> C = x1 // error
78
| ^^
8-
| Found: (x1 : (x: C^) -> C^)
9+
| Found: (x1 : (x: C^) -> C^{localcap})
910
| Required: (x: C^) -> C
1011
|
1112
| longer explanation available when compiling with `-explain`
1213
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:12:20 --------------------------
1314
12 | val _: C^ -> C = x2 // error
1415
| ^^
15-
| Found: (x2 : C^ -> C^)
16+
| Found: (x2 : C^ -> C^{fresh})
1617
| Required: C^ -> C
1718
|
1819
| longer explanation available when compiling with `-explain`
1920
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:15:30 --------------------------
2021
15 | val _: A^ -> (x: C^) -> C = x3 // error
2122
| ^^
22-
| Found: (x3 : A^ -> (x: C^) -> C^)
23+
| Found: (x3 : A^ -> (x: C^) -> C^{localcap})
2324
| Required: A^ -> (x: C^) -> C
2425
|
2526
| longer explanation available when compiling with `-explain`
2627
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:18:25 --------------------------
2728
18 | val _: A^ -> C^ -> C = x4 // error
2829
| ^^
29-
| Found: (x4 : A^ -> C^ -> C^)
30+
| Found: (x4 : A^ -> C^ -> C^{fresh})
3031
| Required: A^ -> C^ -> C
3132
|
3233
| longer explanation available when compiling with `-explain`
3334
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:21:30 --------------------------
3435
21 | val _: A^ -> (x: C^) -> C = x5 // error
3536
| ^^
36-
| Found: (x5 : A^ -> (x: C^) -> C^)
37+
| Found: (x5 : A^ -> (x: C^) -> C^{localcap})
3738
| Required: A^ -> (x: C^) -> C
3839
|
3940
| longer explanation available when compiling with `-explain`
4041
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:24:30 --------------------------
4142
24 | val _: A^ -> (x: C^) => C = x6 // error
4243
| ^^
43-
| Found: (x6 : A^ -> (x: C^) => C^)
44-
| Required: A^ -> (x: C^) => C
44+
| Found: (x6 : A^ -> (x: C^) ->{fresh} C^{localcap})
45+
| Required: A^ -> (x: C^) ->{fresh} C
4546
|
4647
| longer explanation available when compiling with `-explain`
4748
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:27:25 --------------------------
4849
27 | val _: (x: C^) => C = y1 // error
4950
| ^^
50-
| Found: (y1 : (x: C^) ->{fresh} C^)
51+
| Found: (y1 : (x: C^) ->{fresh} C^{localcap})
5152
| Required: (x: C^) ->{fresh} C
5253
|
5354
| longer explanation available when compiling with `-explain`
5455
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:30:20 --------------------------
5556
30 | val _: C^ => C = y2 // error
5657
| ^^
57-
| Found: (y2 : C^ ->{fresh} C^)
58+
| Found: (y2 : C^ ->{fresh} C^{fresh})
5859
| Required: C^ ->{fresh} C
5960
|
6061
| longer explanation available when compiling with `-explain`
6162
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:33:30 --------------------------
6263
33 | val _: A^ => (x: C^) => C = y3 // error
6364
| ^^
64-
| Found: (y3 : A^ ->{fresh} (x: C^) => C^)
65-
| Required: A^ ->{fresh} (x: C^) => C
65+
| Found: (y3 : A^ ->{fresh} (x: C^) ->{fresh} C^{localcap})
66+
| Required: A^ ->{fresh} (x: C^) ->{fresh} C
6667
|
6768
| longer explanation available when compiling with `-explain`
6869
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:36:25 --------------------------
6970
36 | val _: A^ => C^ => C = y4 // error
7071
| ^^
71-
| Found: (y4 : A^ ->{fresh} C^ => C^)
72-
| Required: A^ ->{fresh} C^ => C
72+
| Found: (y4 : A^ ->{fresh} C^ ->{fresh} C^{fresh})
73+
| Required: A^ ->{fresh} C^ ->{fresh} C
7374
|
7475
| longer explanation available when compiling with `-explain`
7576
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:39:30 --------------------------
7677
39 | val _: A^ => (x: C^) -> C = y5 // error
7778
| ^^
78-
| Found: (y5 : A^ ->{fresh} (x: C^) -> C^)
79+
| Found: (y5 : A^ ->{fresh} (x: C^) -> C^{localcap})
7980
| Required: A^ ->{fresh} (x: C^) -> C
8081
|
8182
| longer explanation available when compiling with `-explain`
8283
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:42:30 --------------------------
8384
42 | val _: A^ => (x: C^) => C = y6 // error
8485
| ^^
85-
| Found: (y6 : A^ ->{fresh} (x: C^) => C^)
86-
| Required: A^ ->{fresh} (x: C^) => C
86+
| Found: (y6 : A^ ->{fresh} (x: C^) ->{fresh} C^{localcap})
87+
| Required: A^ ->{fresh} (x: C^) ->{fresh} C
8788
|
8889
| longer explanation available when compiling with `-explain`

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@ def Test =
4141
val y6: A^ => IFun[C^] = ???
4242
val _: A^ => (x: C^) => C = y6 // error
4343

44-
val z1: A^ => Array[C^] = ??? // error
44+
val z1: A^ => Array[C^] = ??? // ok
4545

46+
val z2: (x: A^) => Array[C^] = ??? // error
4647

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
99
15 | files.map(new Logger(_)) // error, Q: can we improve the error message?
1010
| ^^^^^^^^^^^^^
11-
| Found: (_$1: box File^{files*}) ->{files*} box Logger{val f: File^{_$1}}^{cap.rd, _$1}
11+
| Found: (_$1: box File^{files*}) ->{files*} box Logger{val f: File^{_$1}}^{localcap.rd, _$1}
1212
| Required: (_$1: box File^{files*}) ->{fresh} box Logger{val f: File^?}^?
1313
|
1414
| Note that reference <cap of (f: box F^{files*.rd}): box Logger{val f: File^?}^?>.rd

0 commit comments

Comments
 (0)