Skip to content

Commit a9cb65f

Browse files
oderskyodersky
committed
Introduce property for loose capture root checking
Replaces previous unsound rule where `cap` subsumes everything.
1 parent bec5eda commit a9cb65f

File tree

8 files changed

+55
-40
lines changed

8 files changed

+55
-40
lines changed

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

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -122,15 +122,18 @@ sealed abstract class CaptureSet extends Showable:
122122
* - x is the same as y,
123123
* - x is a this reference and y refers to a field of x
124124
* - x and y are local roots and y is an enclosing root of x
125+
* - the LooseRootChecking property is asserted, and either `x` is `cap`
126+
* or `x` is a local root and y is `cap`.
125127
*/
126128
extension (x: CaptureRef)(using Context)
127129
private def subsumes(y: CaptureRef) =
128130
(x eq y)
129-
|| x.isGenericRootCapability // !!! dubious
130131
|| y.match
131132
case y: TermRef => (y.prefix eq x) || x.isRootIncluding(y)
132133
case y: CaptureRoot.Var => x.isRootIncluding(y)
133134
case _ => false
135+
|| (x.isGenericRootCapability || y.isGenericRootCapability && x.isRootCapability)
136+
&& ctx.property(LooseRootChecking).isDefined
134137

135138
private def isRootIncluding(y: CaptureRoot) =
136139
x.isLocalRootCapability && y.isLocalRootCapability
@@ -367,6 +370,13 @@ object CaptureSet:
367370
def apply(elems: Refs)(using Context): CaptureSet.Const =
368371
if elems.isEmpty then empty else Const(elems)
369372

373+
/** If this context property is asserted, we conflate capture roots in subCapture
374+
* tests. Specifically, `cap` then subsumes everything and all local roots subsume `cap`.
375+
* This generally not sound. We currently use loose root checking only in self type
376+
* conformance tests in CheckCaptures.checkSelfTypes.
377+
*/
378+
val LooseRootChecking: Property.Key[Unit] = Property.Key()
379+
370380
/** The subclass of constant capture sets with given elements `elems` */
371381
class Const private[CaptureSet] (val elems: Refs, val description: String = "") extends CaptureSet:
372382
def isConst = true

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

Lines changed: 25 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ import transform.SymUtils.*
1818
import transform.{Recheck, PreRecheck}
1919
import Recheck.*
2020
import scala.collection.mutable
21-
import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult}
21+
import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult, LooseRootChecking}
2222
import StdNames.nme
2323
import NameKinds.DefaultGetterName
2424
import reporting.trace
@@ -747,23 +747,26 @@ class CheckCaptures extends Recheck, SymTransformer:
747747
super.recheckFinish(tpe, tree, pt)
748748
end recheckFinish
749749

750-
// ------------------ Adaptation -------------------------------------
751-
//
752-
// Adaptations before checking conformance of actual vs expected:
753-
//
754-
// - Convert function to dependent function if expected type is a dependent function type
755-
// (c.f. alignDependentFunction).
756-
// - Relax expected capture set containing `this.type`s by adding references only
757-
// accessible through those types (c.f. addOuterRefs, also #14930 for a discussion).
758-
// - Adapt box status and environment capture sets by simulating box/unbox operations.
759-
760-
override def isCompatible(actual: Type, expected: Type, tree: Tree)(using Context): Boolean =
761-
super.isCompatible(actual, expected, tree)
750+
// ------------------ Adaptation -------------------------------------
751+
//
752+
// Adaptations before checking conformance of actual vs expected:
753+
//
754+
// - Convert function to dependent function if expected type is a dependent function type
755+
// (c.f. alignDependentFunction).
756+
// - Relax expected capture set containing `this.type`s by adding references only
757+
// accessible through those types (c.f. addOuterRefs, also #14930 for a discussion).
758+
// - Adapt box status and environment capture sets by simulating box/unbox operations.
759+
// - Instantiate `cap` in actual as needed to a local root.
760+
761+
override def isCompatible(actual: Type, expected: Type)(using Context): Boolean =
762+
super.isCompatible(actual, expected)
762763
|| {
763-
val mapr = mapRoots(defn.captureRoot.termRef, CaptureRoot.Var(ctx.owner.levelOwner))
764-
val actual1 = mapr(actual)
764+
// When testing whether `A <: B`, it could be that `B` uses a local capture root,
765+
// but a uses `cap`, i.e. is capture polymorphic. In this case, adaptation is allowed
766+
// to instantiate `A` to match the root in `B`.
767+
val actual1 = mapRoots(defn.captureRoot.termRef, CaptureRoot.Var(ctx.owner.levelOwner))(actual)
765768
(actual1 ne actual) && {
766-
val res = super.isCompatible(actual1, expected, tree)
769+
val res = super.isCompatible(actual1, expected)
767770
if !res && ctx.settings.YccDebug.value then
768771
println(i"Failure under mapped roots:")
769772
println(i"${TypeComparer.explained(_.isSubType(actual, expected))}")
@@ -1084,7 +1087,12 @@ class CheckCaptures extends Recheck, SymTransformer:
10841087
}
10851088
assert(roots.nonEmpty)
10861089
for case root: ClassSymbol <- roots do
1087-
inContext(ctx.withOwner(root)):
1090+
inContext(ctx.fresh.setOwner(root).withProperty(LooseRootChecking, Some(()))):
1091+
// Without LooseRootChecking, we get problems with F-bounded parent types.
1092+
// These can make `cap` "pop out" in ways that are hard to prevent. I believe
1093+
// to prevent it we'd have to map `cap` in a whole class graph with all parent
1094+
// classes, which would be very expensive. So for now we approximate by assuming
1095+
// different roots are compatible for self type conformance checking.
10881096
checkSelfAgainstParents(root, root.baseClasses)
10891097
val selfType = root.asClass.classInfo.selfType
10901098
interpolator(startingVariance = -1).traverse(selfType)

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

Lines changed: 6 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,13 @@
1010
| Required: Test2.Cell[() ->{cap[<root>]} Unit]
1111
|
1212
| longer explanation available when compiling with `-explain`
13-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:12:14 ------------------------------------------------------
13+
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:12:6 -------------------------------------------------------
1414
12 | val later = usingLogFile { f => () => f.write(0) } // error
15-
| ^^^^^^^^^^^^
16-
| escaping local reference local.type
15+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
16+
| Non-local value later cannot have an inferred type
17+
| () ->{x$0, 'cap[..<root>](from instantiating usingLogFile)} Unit
18+
| with non-empty capture set {x$0, 'cap[..<root>](from instantiating usingLogFile)}.
19+
| The type needs to be declared explicitly.
1720
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:14 ------------------------------------------------------
1821
23 | val later = usingLogFile { f => () => f.write(0) } // error
1922
| ^^^^^^^^^^^^
@@ -30,17 +33,3 @@
3033
62 | val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
3134
| ^^^^^^^^^
3235
| escaping local reference local.type
33-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:71:16 ------------------------------------------------------
34-
71 | val later = usingFile("logfile", // error
35-
| ^^^^^^^^^
36-
| reference (_$1 : java.io.OutputStream^{local}) is not included in the allowed capture set {x$0, local, local²}
37-
|
38-
| Note that reference (_$1 : java.io.OutputStream^{local}), defined at level 6
39-
| cannot be included in outer capture set {x$0, local, local}, defined at level 1 in method test
40-
|
41-
| where: local is a reference to a value parameter
42-
| local² is a reference to a value parameter
43-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:72:6 -------------------------------------------------------
44-
72 | usingLogger(_, l => () => l.log("test"))) // error ??? but had the comment: ok, since we can widen `l` to `file` instead of to `cap`
45-
| ^^^^^^^^^^^
46-
| escaping local reference local.type

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,6 @@ object Test4:
6868
op(logger)
6969

7070
def test =
71-
val later = usingFile("logfile", // error
72-
usingLogger(_, l => () => l.log("test"))) // error ??? but had the comment: ok, since we can widen `l` to `file` instead of to `cap`
71+
val later = usingFile("logfile",
72+
usingLogger(_, l => () => l.log("test"))) // ok, since we can widen `l` to `file` instead of to `cap`
7373
later()

‎tests/neg/capt-wf.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ def test(c: Cap, other: String): Unit =
1515
val x4: C^{s2} = ??? // OK
1616
val x5: C^{c, c} = ??? // error: redundant
1717
// val x6: C^{c}^{c} = ??? // would be syntax error
18-
val x7: Cap^{c} = ??? // no longer redundant, Cap and c are on different levels
18+
val x7: Cap^{c} = ??? // error: redundant
1919
// val x8: C^{c}^{cap} = ??? // would be syntax error
2020
val x9: C^{c, cap} = ??? // error: redundant
2121
val x10: C^{cap, c} = ??? // error: redundant

‎tests/pos-custom-args/captures/ctest.scala

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
class C
2+
type Cap = C^
3+
4+
class S
5+
6+
def f(y: Cap) =
7+
val a: ((x: Cap) -> S^) = (x: Cap) => S()

‎tests/pos-custom-args/captures/try3.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ def raise[E <: Exception](ex: E)(using CanThrow[E]): Nothing =
1313
throw ex
1414

1515
def test1: Int =
16-
def f(a: Boolean): Boolean -> CanThrow[IOException] ?-> Int =
16+
def f(a: Boolean) =
1717
handle {
1818
if !a then raise(IOException())
1919
(b: Boolean) => (_: CanThrow[IOException]) ?=>
@@ -22,6 +22,7 @@ def test1: Int =
2222
} {
2323
ex => (b: Boolean) => (_: CanThrow[IOException]) ?=> -1
2424
}
25+
def fc(a: Boolean): Boolean -> CanThrow[IOException] ?-> Int = f(a)
2526
handle {
2627
val g = f(true)
2728
g(false) // can raise an exception

‎tests/pos-special/stdlib/collection/Iterator.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1202,7 +1202,7 @@ object Iterator extends IterableFactory[Iterator] {
12021202
} else Iterator.empty.next()
12031203

12041204
override def concat[B >: A](that: => IterableOnce[B]^): Iterator[B]^{this, that} = {
1205-
val c = new ConcatIteratorCell[B](that, null).asInstanceOf[ConcatIteratorCell[A]]
1205+
val c: ConcatIteratorCell[A] = new ConcatIteratorCell[B](that, null).asInstanceOf
12061206
if (tail == null) {
12071207
tail = c
12081208
last = c

0 commit comments

Comments
 (0)