Skip to content

Commit f41a94a

Browse files
committed
Revise path handling
- Don't widen prefix type if followed by a path selection - When applying VAR with a prefix path p on a boxed capture set, replace cap with p* instead of p. This makes it clear that we need to charge deep capture sets on parameters and avoids paradoxes like this one: case class Box[+T](get: T) val b: Box[C^] Here, b.get <:< b, but b.get's underlying capture set is {cap} whereas b's underlying capture set is {}. By using b.get* instead of b.get, we make sure that we compare against the dcs of `b`, which is also {cap}.
1 parent af223d7 commit f41a94a

File tree

7 files changed

+48
-21
lines changed

7 files changed

+48
-21
lines changed

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,10 @@ object ccConfig:
5656
def useSepChecks(using Context): Boolean =
5757
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
5858

59+
/** Not used currently. Handy for trying out new features */
60+
def newScheme(using Context): Boolean =
61+
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
62+
5963
end ccConfig
6064

6165
/** Are we at checkCaptures phase? */

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

Lines changed: 24 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -643,7 +643,7 @@ class CheckCaptures extends Recheck, SymTransformer:
643643
// - on the LHS of assignments, or
644644
// - if the qualifier or selection type is boxed, or
645645
// - the selection is either a trackable capture ref or a pure type
646-
if pt == LhsProto
646+
if noWiden(selType, pt)
647647
|| qualType.isBoxedCapturing
648648
|| selWiden.isBoxedCapturing
649649
|| selType.isTrackableRef
@@ -1496,11 +1496,14 @@ class CheckCaptures extends Recheck, SymTransformer:
14961496
* Then
14971497
* foo: Foo { def a: C^{foo}; def b: C^{foo} }^{foo}
14981498
*/
1499-
private def improveCaptures(widened: Type, actual: Type)(using Context): Type = actual match
1499+
private def improveCaptures(widened: Type, prefix: Type)(using Context): Type = prefix match
15001500
case ref: CaptureRef if ref.isTracked =>
15011501
widened match
1502-
case CapturingType(p, refs) if ref.singletonCaptureSet.mightSubcapture(refs) =>
1503-
widened.derivedCapturingType(p, ref.singletonCaptureSet)
1502+
case widened @ CapturingType(p, refs) if ref.singletonCaptureSet.mightSubcapture(refs) =>
1503+
val improvedCs =
1504+
if widened.isBoxed then ref.reach.singletonCaptureSet
1505+
else ref.singletonCaptureSet
1506+
widened.derivedCapturingType(p, improvedCs)
15041507
.showing(i"improve $widened to $result", capt)
15051508
case _ => widened
15061509
case _ => widened
@@ -1524,13 +1527,29 @@ class CheckCaptures extends Recheck, SymTransformer:
15241527
case _ =>
15251528
actual
15261529

1530+
/* Currently not needed since it forms part of `adapt`
1531+
private def improve(actual: Type, prefix: Type)(using Context): Type =
1532+
val widened = actual.widen.dealiasKeepAnnots
1533+
val improved = improveCaptures(widened, prefix).withReachCaptures(prefix)
1534+
if improved eq widened then actual else improved
1535+
*/
1536+
1537+
/** An actual singleton type should not be widened if the expected type is a
1538+
* LhsProto, or a singleton type, or a path selection with a stable value
1539+
*/
1540+
private def noWiden(actual: Type, expected: Type)(using Context): Boolean =
1541+
actual.isSingleton
1542+
&& expected.match
1543+
case expected: PathSelectionProto => !expected.sym.isOneOf(UnstableValueFlags)
1544+
case _ => expected.isSingleton || expected == LhsProto
1545+
15271546
/** Adapt `actual` type to `expected` type. This involves:
15281547
* - narrow toplevel captures of `x`'s underlying type to `{x}` according to CC's VAR rule
15291548
* - narrow nested captures of `x`'s underlying type to `{x*}`
15301549
* - do box adaptation
15311550
*/
15321551
def adapt(actual: Type, expected: Type, tree: Tree, boxErrors: BoxErrors)(using Context): Type =
1533-
if expected == LhsProto || expected.isSingleton && actual.isSingleton then
1552+
if noWiden(actual, expected) then
15341553
actual
15351554
else
15361555
val improvedVAR = improveCaptures(actual.widen.dealiasKeepAnnots, actual)

scala2-library-cc/src/scala/collection/View.scala

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -151,12 +151,16 @@ object View extends IterableFactory[View] {
151151
object Filter {
152152
def apply[A](underlying: Iterable[A]^, p: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, p} =
153153
underlying match {
154-
case filter: Filter[A]^{underlying} if filter.isFlipped == isFlipped =>
155-
unsafeAssumeSeparate:
154+
case filter: Filter[A] if filter.isFlipped == isFlipped =>
155+
new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped)
156+
.asInstanceOf[Filter[A]^{underlying, p}]
157+
// !!! asInstanceOf needed once paths were added, see path-patmat-should-be-pos.scala for minimization
158+
//case filter: Filter[A]^{underlying} if filter.isFlipped == isFlipped =>
159+
// unsafeAssumeSeparate:
156160
// See filter-iterable.scala for a test where a variant of Filter
157161
// works without the unsafeAssumeSeparate. But it requires significant
158162
// changes compared to the version here. See also Filter in colltest5.CollectionStrawManCC5_1.
159-
new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped)
163+
// new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped)
160164
case _ => new Filter(underlying, p, isFlipped)
161165
}
162166
}

tests/neg-custom-args/captures/i21442.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
-- Error: tests/neg-custom-args/captures/i21442.scala:10:13 ------------------------------------------------------------
22
10 | val io = x.unbox // error: local reach capability {x*} leaks
33
| ^^^^^^^
4-
| Local reach capability x* leaks into capture scope of method foo.
4+
| Local reach capability x.unbox* leaks into capture scope of method foo.
55
| To allow this, the parameter x should be declared with a @use annotation
66
-- Error: tests/neg-custom-args/captures/i21442.scala:17:10 ------------------------------------------------------------
77
17 | val x1: Boxed[IO^] = x // error

tests/pos-custom-args/captures/i15749.scala

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
1-
//> using options -source 3.4
2-
// (to make sure we use the sealed policy)
1+
import caps.use
32
class Unit
43
object unit extends Unit
54

@@ -12,6 +11,6 @@ class Foo[T](val x: T)
1211
// Foo[□ Unit => T]
1312
type BoxedLazyVal[T] = Foo[LazyVal[T]]
1413

15-
def force[A](v: BoxedLazyVal[A]): A =
14+
def force[A](@use v: BoxedLazyVal[A]): A =
1615
// Γ ⊢ v.x : □ {cap} Unit -> A
1716
v.x(unit) // should be error: (unbox v.x)(unit), where (unbox v.x) should be untypable, now ok

tests/pending/pos-custom-args/captures/sep-pairs.scala renamed to tests/pos-custom-args/captures/sep-pairs.scala

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -13,16 +13,15 @@ def twoRefs(): Pair[Ref^, Ref^] =
1313
val r2 = Ref()
1414
Pair(r1, r2)
1515

16+
/*
1617
def twoRefsBad(): Pair[Ref^, Ref^] =
1718
Pair(Ref(), Ref()) // error: universal capability cannot be included in capture set
1819
// even though this is morally equivalent to `twoRefs`
19-
20+
*/
2021

2122
def test(io: Object^): Unit =
2223
val two = twoRefs()
23-
val fst = two.fst // error: local reach capability two* leaks into test
24-
// first, the leakage makes no sense
25-
// second, the capture should be two.fst, not two*
24+
val fst = two.fst
2625
val snd = two.snd
27-
val three: Pair[Ref^{io}, Ref^{io}] = ???
28-
val bad = three.fst
26+
27+
val p: Pair[Ref^, Ref^] = Pair(fst, snd)

tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -455,12 +455,14 @@ object CollectionStrawMan5 {
455455
object Filter:
456456
def apply[A](underlying: Iterable[A]^, pp: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, pp} =
457457
underlying match
458-
case filter: Filter[A]^{underlying} =>
459-
unsafeAssumeSeparate:
458+
case filter: Filter[A] =>
459+
new Filter(filter.underlying, a => filter.p(a) && pp(a))
460+
.asInstanceOf[Filter[A]^{underlying, pp}]
461+
//unsafeAssumeSeparate:
460462
// See filter-iterable.scala for a test where a variant of Filter
461463
// works without the unsafeAssumeSeparate. But it requires significant
462464
// changes compared to the version here.
463-
new Filter(filter.underlying, a => filter.p(a) && pp(a))
465+
//new Filter(filter.underlying, a => filter.p(a) && pp(a))
464466
case _ => new Filter(underlying, pp)
465467

466468
case class Partition[A](val underlying: Iterable[A]^, p: A => Boolean) {

0 commit comments

Comments
 (0)