Skip to content

Commit b35fa8a

Browse files
authored
Adapt types according to read-only status (#23332)
Extend type adaptation to read-only status. Two big improvements: - we also adapt if the target type is a mutable type with a read-only capture set. So the following compiles: ```scala class Ref extends Mutable { ... } val x: Ref^{cap.rd} = Ref() ``` - we also adapt deeply inside a type. So the following compiles: ```scala val refs = List(Ref(), Ref()) val rdrs: List[Ref^{cap.rd}] = refs ``` We even try to track arguments through base types, so the following also compiles: ```scala val rdrs2: Seq[Ref^{cap.rd}] = refs ``` But there are some limits, correlating actual and expected type through base types and as-seen-from is hard. In the end I had to abandon the original idea to roll everyhting into subtyping. I got the basics to work, but the problem then was that we use deep capture sets in separation checking, and those were not adapted. To do this, we'd have to somehow figure out what a dcs relative to an expected type is. This looks deeply non-trivial, and would probably in the end come down to techniques similar to the adaptation in this PR. So the benefit of also adding and inferring qualifiers to capture sets are not clear. EDIT: We do need qualifiers for soundness as @Linyxus example below shows. It's now in `ro-mut-conformance.scala`. So the adaptation commit has been rebased on the mutability qualifiers branch.
2 parents 0163e4a + 0c9e224 commit b35fa8a

26 files changed

+560
-94
lines changed

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,14 +70,17 @@ class CCState:
7070

7171
// ------ Iteration count of capture checking run
7272

73-
private var iterCount = 1
73+
private var iterCount = 0
7474

7575
def iterationId = iterCount
7676

7777
def nextIteration[T](op: => T): T =
7878
iterCount += 1
7979
try op finally iterCount -= 1
8080

81+
def start(): Unit =
82+
iterCount = 1
83+
8184
// ------ Global counters -----------------------
8285

8386
/** Next CaptureSet.Var id */

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -330,6 +330,12 @@ object Capabilities:
330330
final def isExclusive(using Context): Boolean =
331331
!isReadOnly && (isTerminalCapability || captureSetOfInfo.isExclusive)
332332

333+
/** Similar to isExlusive, but also includes capabilties with capture
334+
* set variables in their info whose status is still open.
335+
*/
336+
final def maybeExclusive(using Context): Boolean =
337+
!isReadOnly && (isTerminalCapability || captureSetOfInfo.maybeExclusive)
338+
333339
final def isWellformed(using Context): Boolean = this match
334340
case self: CoreCapability => self.isTrackableRef
335341
case _ => true

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

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -22,11 +22,18 @@ private val Captures: Key[CaptureSet] = Key()
2222
def isCaptureChecking(using Context): Boolean =
2323
ctx.phaseId == Phases.checkCapturesPhase.id
2424

25-
/** Are we at checkCaptures or Setup phase? */
25+
/** Are we in the CheckCaptures or Setup phase? */
2626
def isCaptureCheckingOrSetup(using Context): Boolean =
27-
val ccId = Phases.checkCapturesPhase.id
28-
val ctxId = ctx.phaseId
29-
ctxId == ccId || ctxId == ccId - 1
27+
val ccPhase = Phases.checkCapturesPhase
28+
ccPhase.exists
29+
&& {
30+
val ccId = ccPhase.id
31+
val ctxId = ctx.phaseId
32+
ctxId == ccId
33+
|| ctxId == ccId - 1 && ccState.iterationId > 0
34+
// Note: just checking phase id is not enough since Setup would
35+
// also be the phase after pattern matcher.
36+
}
3037

3138
/** A dependent function type with given arguments and result type
3239
* TODO Move somewhere else where we treat all function type related ops together.

0 commit comments

Comments
 (0)