Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 0827546

Browse files
oderskyodersky
authoredJun 18, 2025··
Standardize on log-based undo (#23357)
Drop the snapshot scheme in VarState. The previous scheme did leak instantiations from failed subtype comparisons, since a subtype comparison might have several subCaptures tests. If a first subCaptures test succeeds then anything it instantiated is made permanent, even if a subsequent test and the whole subType comparison fails. The change needed updates in several neg test files where we find that fewer things are instantiated in error messages.
2 parents 1b5138d + 2dea57d commit 0827546

21 files changed

+118
-206
lines changed
 

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

Lines changed: 46 additions & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -178,12 +178,7 @@ sealed abstract class CaptureSet extends Showable:
178178

179179
/** Try to include all element in `refs` to this capture set. */
180180
protected final def tryInclude(newElems: Refs, origin: CaptureSet)(using Context, VarState): Boolean =
181-
TypeComparer.inNestedLevel:
182-
// Run in nested level so that a error notes for a failure here can be
183-
// cancelled in case the whole comparison succeeds.
184-
// We do this here because all nested tryInclude and subCaptures calls go
185-
// through this method.
186-
newElems.forall(tryInclude(_, origin))
181+
newElems.forall(tryInclude(_, origin))
187182

188183
protected def mutableToReader(origin: CaptureSet)(using Context): Boolean =
189184
if mutability == Mutable then toReader() else true
@@ -284,16 +279,14 @@ sealed abstract class CaptureSet extends Showable:
284279

285280
/** The subcapturing test, using a given VarState */
286281
final def subCaptures(that: CaptureSet)(using ctx: Context, vs: VarState = VarState()): Boolean =
287-
val this1 = this.adaptMutability(that)
288-
if this1 == null then false
289-
else if this1 ne this then
290-
capt.println(i"WIDEN ro $this with ${this.mutability} <:< $that with ${that.mutability} to $this1")
291-
this1.subCaptures(that, vs)
292-
else if that.tryInclude(elems, this) then
293-
addDependent(that)
294-
else
295-
varState.rollBack()
296-
false
282+
TypeComparer.inNestedLevel:
283+
val this1 = this.adaptMutability(that)
284+
if this1 == null then false
285+
else if this1 ne this then
286+
capt.println(i"WIDEN ro $this with ${this.mutability} <:< $that with ${that.mutability} to $this1")
287+
this1.subCaptures(that, vs)
288+
else
289+
that.tryInclude(elems, this) && addDependent(that)
297290

298291
/** Two capture sets are considered =:= equal if they mutually subcapture each other
299292
* in a frozen state.
@@ -662,30 +655,6 @@ object CaptureSet:
662655

663656
var description: String = ""
664657

665-
/** Record current elements in given VarState provided it does not yet
666-
* contain an entry for this variable.
667-
*/
668-
private def recordElemsState()(using VarState): Boolean =
669-
varState.getElems(this) match
670-
case None => varState.putElems(this, elems)
671-
case _ => true
672-
673-
/** Record current dependent sets in given VarState provided it does not yet
674-
* contain an entry for this variable.
675-
*/
676-
private[CaptureSet] def recordDepsState()(using VarState): Boolean =
677-
varState.getDeps(this) match
678-
case None => varState.putDeps(this, deps)
679-
case _ => true
680-
681-
/** Reset elements to what was recorded in `state` */
682-
def resetElems()(using state: VarState): Unit =
683-
elems = state.elems(this)
684-
685-
/** Reset dependent sets to what was recorded in `state` */
686-
def resetDeps()(using state: VarState): Unit =
687-
deps = state.deps(this)
688-
689658
/** Check that all maps recorded in skippedMaps map `elem` to itself
690659
* or something subsumed by it.
691660
*/
@@ -695,16 +664,28 @@ object CaptureSet:
695664
assert(elem.subsumes(elem1),
696665
i"Skipped map ${tm.getClass} maps newly added $elem to $elem1 in $this")
697666

667+
protected def includeElem(elem: Capability)(using Context): Unit =
668+
if !elems.contains(elem) then
669+
elems += elem
670+
TypeComparer.logUndoAction: () =>
671+
elems -= elem
672+
673+
def includeDep(cs: CaptureSet)(using Context): Unit =
674+
if !deps.contains(cs) then
675+
deps += cs
676+
TypeComparer.logUndoAction: () =>
677+
deps -= cs
678+
698679
final def addThisElem(elem: Capability)(using Context, VarState): Boolean =
699-
if isConst || !recordElemsState() then // Fail if variable is solved or given VarState is frozen
680+
if isConst || !varState.canRecord then // Fail if variable is solved or given VarState is frozen
700681
addIfHiddenOrFail(elem)
701682
else if !levelOK(elem) then
702683
failWith(IncludeFailure(this, elem, levelError = true)) // or `elem` is not visible at the level of the set.
703684
else
704685
// id == 108 then assert(false, i"trying to add $elem to $this")
705686
assert(elem.isWellformed, elem)
706687
assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState])
707-
elems += elem
688+
includeElem(elem)
708689
if isBadRoot(rootLimit, elem) then
709690
rootAddedHandler()
710691
newElemAddedHandler(elem)
@@ -772,7 +753,7 @@ object CaptureSet:
772753
(cs eq this)
773754
|| cs.isUniversal
774755
|| isConst
775-
|| recordDepsState() && { deps += cs; true }
756+
|| varState.canRecord && { includeDep(cs); true }
776757

777758
override def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
778759
rootLimit = upto
@@ -1126,7 +1107,7 @@ object CaptureSet:
11261107
if alias ne this then alias.add(elem)
11271108
else
11281109
def addToElems() =
1129-
elems += elem
1110+
includeElem(elem)
11301111
deps.foreach: dep =>
11311112
assert(dep != this)
11321113
vs.addHidden(dep.asInstanceOf[HiddenSet], elem)
@@ -1142,7 +1123,7 @@ object CaptureSet:
11421123
deps = SimpleIdentitySet(elem.hiddenSet)
11431124
else
11441125
addToElems()
1145-
elem.hiddenSet.deps += this
1126+
elem.hiddenSet.includeDep(this)
11461127
case _ =>
11471128
addToElems()
11481129

@@ -1238,41 +1219,15 @@ object CaptureSet:
12381219
*/
12391220
class VarState:
12401221

1241-
/** A map from captureset variables to their elements at the time of the snapshot. */
1242-
private val elemsMap: util.EqHashMap[Var, Refs] = new util.EqHashMap
1243-
1244-
/** A map from captureset variables to their dependent sets at the time of the snapshot. */
1245-
private val depsMap: util.EqHashMap[Var, Deps] = new util.EqHashMap
1246-
12471222
/** A map from ResultCap values to other ResultCap values. If two result values
12481223
* `a` and `b` are unified, then `eqResultMap(a) = b` and `eqResultMap(b) = a`.
12491224
*/
12501225
private var eqResultMap: util.SimpleIdentityMap[ResultCap, ResultCap] = util.SimpleIdentityMap.empty
12511226

1252-
/** A snapshot of the `eqResultMap` value at the start of a VarState transaction */
1253-
private var eqResultSnapshot: util.SimpleIdentityMap[ResultCap, ResultCap] | Null = null
1254-
1255-
/** The recorded elements of `v` (it's required that a recording was made) */
1256-
def elems(v: Var): Refs = elemsMap(v)
1257-
1258-
/** Optionally the recorded elements of `v`, None if nothing was recorded for `v` */
1259-
def getElems(v: Var): Option[Refs] = elemsMap.get(v)
1260-
12611227
/** Record elements, return whether this was allowed.
12621228
* By default, recording is allowed in regular but not in frozen states.
12631229
*/
1264-
def putElems(v: Var, elems: Refs): Boolean = { elemsMap(v) = elems; true }
1265-
1266-
/** The recorded dependent sets of `v` (it's required that a recording was made) */
1267-
def deps(v: Var): Deps = depsMap(v)
1268-
1269-
/** Optionally the recorded dependent sets of `v`, None if nothing was recorded for `v` */
1270-
def getDeps(v: Var): Option[Deps] = depsMap.get(v)
1271-
1272-
/** Record dependent sets, return whether this was allowed.
1273-
* By default, recording is allowed in regular but not in frozen states.
1274-
*/
1275-
def putDeps(v: Var, deps: Deps): Boolean = { depsMap(v) = deps; true }
1230+
def canRecord: Boolean = true
12761231

12771232
/** Does this state allow additions of elements to capture set variables? */
12781233
def isOpen = true
@@ -1283,11 +1238,6 @@ object CaptureSet:
12831238
* but the special state VarState.Separate overrides this.
12841239
*/
12851240
def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean =
1286-
elemsMap.get(hidden) match
1287-
case None =>
1288-
elemsMap(hidden) = hidden.elems
1289-
depsMap(hidden) = hidden.deps
1290-
case _ =>
12911241
hidden.add(elem)(using ctx, this)
12921242
true
12931243

@@ -1311,17 +1261,13 @@ object CaptureSet:
13111261
&& eqResultMap(c1) == null
13121262
&& eqResultMap(c2) == null
13131263
&& {
1314-
if eqResultSnapshot == null then eqResultSnapshot = eqResultMap
13151264
eqResultMap = eqResultMap.updated(c1, c2).updated(c2, c1)
1265+
TypeComparer.logUndoAction: () =>
1266+
eqResultMap.remove(c1)
1267+
eqResultMap.remove(c2)
13161268
true
13171269
}
13181270

1319-
/** Roll back global state to what was recorded in this VarState */
1320-
def rollBack(): Unit =
1321-
elemsMap.keysIterator.foreach(_.resetElems()(using this))
1322-
depsMap.keysIterator.foreach(_.resetDeps()(using this))
1323-
if eqResultSnapshot != null then eqResultMap = eqResultSnapshot.nn
1324-
13251271
private var seen: util.EqHashSet[Capability] = new util.EqHashSet
13261272

13271273
/** Run test `pred` unless `ref` was seen in an enclosing `ifNotSeen` operation */
@@ -1341,8 +1287,7 @@ object CaptureSet:
13411287
* subsume arbitary types, which are then recorded in their hidden sets.
13421288
*/
13431289
class Closed extends VarState:
1344-
override def putElems(v: Var, refs: Refs) = false
1345-
override def putDeps(v: Var, deps: Deps) = false
1290+
override def canRecord = false
13461291
override def isOpen = false
13471292
override def toString = "closed varState"
13481293

@@ -1366,23 +1311,29 @@ object CaptureSet:
13661311
*/
13671312
def HardSeparate(using Context): Separating = ccState.HardSeparate
13681313

1369-
/** A special state that turns off recording of elements. Used only
1370-
* in `addSub` to prevent cycles in recordings. Instantiated in ccState.Unrecorded.
1371-
*/
1372-
class Unrecorded extends VarState:
1373-
override def putElems(v: Var, refs: Refs) = true
1374-
override def putDeps(v: Var, deps: Deps) = true
1375-
override def rollBack(): Unit = ()
1314+
/** A mixin trait that overrides the addHidden and unify operations to
1315+
* not depend in state. */
1316+
trait Stateless extends VarState:
1317+
1318+
/** Allow adding hidden elements, but don't store them */
13761319
override def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean = true
1320+
1321+
/** Don't allow to unify result caps */
1322+
override def unify(c1: ResultCap, c2: ResultCap)(using Context): Boolean = false
1323+
end Stateless
1324+
1325+
/** An open state that turns off recording of hidden elements (but allows
1326+
* adding them). Used in `addAsDependentTo`. Instantiated in ccState.Unrecorded.
1327+
*/
1328+
class Unrecorded extends VarState, Stateless:
13771329
override def toString = "unrecorded varState"
13781330

13791331
def Unrecorded(using Context): Unrecorded = ccState.Unrecorded
13801332

13811333
/** A closed state that turns off recording of hidden elements (but allows
13821334
* adding them). Used in `mightAccountFor`. Instantiated in ccState.ClosedUnrecorded.
13831335
*/
1384-
class ClosedUnrecorded extends Closed:
1385-
override def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean = true
1336+
class ClosedUnrecorded extends Closed, Stateless:
13861337
override def toString = "closed unrecorded varState"
13871338

13881339
def ClosedUnrecorded(using Context): ClosedUnrecorded = ccState.ClosedUnrecorded

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

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
5353
needsGc = false
5454
maxErrorLevel = -1
5555
errorNotes = Nil
56-
logSize = 0
56+
undoLog.clear()
5757
if Config.checkTypeComparerReset then checkReset()
5858

5959
private var pendingSubTypes: util.MutableSet[(Type, Type)] | Null = null
@@ -63,8 +63,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
6363
private var maxErrorLevel: Int = -1
6464
protected var errorNotes: List[(Int, ErrorNote)] = Nil
6565

66-
private val undoLog = mutable.ArrayBuffer[() => Unit]()
67-
private var logSize = 0
66+
val undoLog = mutable.ArrayBuffer[() => Unit]()
6867

6968
private var needsGc = false
7069

@@ -1588,18 +1587,20 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
15881587
undoLog(i)()
15891588
i += 1
15901589
undoLog.takeInPlace(prevSize)
1590+
assert(undoLog.size == prevSize)
15911591

15921592
// begin recur
15931593
if tp2 eq NoType then false
15941594
else if tp1 eq tp2 then true
15951595
else
15961596
val savedCstr = constraint
15971597
val savedGadt = ctx.gadt
1598-
val savedLogSize = logSize
1598+
val savedLogSize = undoLog.size
15991599
inline def restore() =
16001600
state.constraint = savedCstr
16011601
ctx.gadtState.restore(savedGadt)
16021602
if undoLog.size != savedLogSize then
1603+
//println(i"ROLLBACK $tp1 <:< $tp2")
16031604
rollBack(savedLogSize)
16041605
val savedSuccessCount = successCount
16051606
try

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

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,9 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:11:43 ----------------------------------
2-
11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon
2+
11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error
33
| ^^^^^^^
44
| Found: Str^{} ->{ac, y, z} Str^{y, z}
55
| Required: Str^{y, z} => Str^{y, z}
66
|
77
| where: => refers to a fresh root capability in the type of value dc
88
|
99
| longer explanation available when compiling with `-explain`
10-
-- Error: tests/neg-custom-args/captures/capt-depfun.scala:11:24 -------------------------------------------------------
11-
11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon
12-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
13-
| Separation failure: value dc's type Str^{y, z} => Str^{y, z} hides parameters y and z.
14-
| The parameters need to be annotated with @consume to allow this.

‎tests/neg-custom-args/captures/capt-depfun.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,4 +8,4 @@ class Str
88
def f(y: Cap, z: Cap) =
99
def g(): C @retains[y.type | z.type] = ???
1010
val ac: ((x: Cap) => Str @retains[x.type] => Str @retains[x.type]) = ???
11-
val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon
11+
val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error

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

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,3 @@
2727
| =>² refers to a fresh root capability in the type of value b
2828
|
2929
| longer explanation available when compiling with `-explain`
30-
-- Error: tests/neg-custom-args/captures/depfun-reach.scala:18:17 ------------------------------------------------------
31-
18 | : (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] = // error
32-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
33-
|Separation failure: method foo's result type (xs: List[(X, () ->{io} Unit)]) => List[() -> Unit] hides parameter op.
34-
|The parameter needs to be annotated with @consume to allow this.

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ def test(io: Object^, async: Object^) =
1515
compose(op)
1616

1717
def foo[X](op: (xs: List[(X, () ->{io} Unit)]) => List[() ->{xs*} Unit])
18-
: (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] = // error
18+
: (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] =
1919
op // error
2020

2121
def boom(op: List[(() ->{async} Unit, () ->{io} Unit)]): List[() ->{} Unit] =

‎tests/neg-custom-args/captures/effect-swaps-explicit.check

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,21 +17,21 @@
1717
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:69:10 ------------------------
1818
69 | Future: fut ?=> // error, type mismatch
1919
| ^
20-
|Found: (contextual$9: boundary.Label[Result[Future[T^?]^?, E^?]^?]^) ?->{fr, async} Future[T^?]^{fr, contextual$9}
21-
|Required: (boundary.Label[Result[Future[T^?]^{fr, async}, E^?]]^) ?=> Future[T^?]^{fr, async}
20+
|Found: (contextual$9: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, contextual$9}
21+
|Required: (boundary.Label[Result[Future[T^?]^?, E^?]]^) ?=> Future[T^?]^?
2222
|
2323
|where: ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make
2424
| ^ refers to the universal root capability
2525
|
2626
|Note that reference contextual$9.type
27-
|cannot be included in outer capture set {fr, async}
27+
|cannot be included in outer capture set ?
2828
70 | fr.await.ok
2929
|
3030
| longer explanation available when compiling with `-explain`
3131
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:73:35 ------------------------
3232
73 | Result.make[Future[T], E]: lbl ?=> // error: type mismatch
3333
| ^
34-
|Found: (lbl: boundary.Label[Result[Future[T^?]^?, E^?]^?]^) ?->{fr, async} Future[T^?]^{fr, lbl}
34+
|Found: (lbl: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, lbl}
3535
|Required: (boundary.Label[Result[Future[T], E]]^) ?=> Future[T]
3636
|
3737
|where: ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make

‎tests/neg-custom-args/captures/effect-swaps.check

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,21 +17,21 @@
1717
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:69:10 ---------------------------------
1818
69 | Future: fut ?=> // error, type mismatch
1919
| ^
20-
|Found: (contextual$9: boundary.Label[Result[Future[T^?]^?, E^?]^?]^{cap.rd}) ?->{fr, async} Future[T^?]^{fr, contextual$9}
21-
|Required: (boundary.Label[Result[Future[T^?]^{fr, async}, E^?]]^{cap.rd}) ?=> Future[T^?]^{fr, async}
20+
|Found: (contextual$9: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, contextual$9}
21+
|Required: (boundary.Label[Result[Future[T^?]^?, E^?]]^{cap.rd}) ?=> Future[T^?]^?
2222
|
2323
|where: ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make
2424
| cap is the universal root capability
2525
|
2626
|Note that reference contextual$9.type
27-
|cannot be included in outer capture set {fr, async}
27+
|cannot be included in outer capture set ?
2828
70 | fr.await.ok
2929
|
3030
| longer explanation available when compiling with `-explain`
3131
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:73:35 ---------------------------------
3232
73 | Result.make[Future[T], E]: lbl ?=> // error: type mismatch
3333
| ^
34-
|Found: (lbl: boundary.Label[Result[Future[T^?]^?, E^?]^?]^{cap.rd}) ?->{fr, async} Future[T^?]^{fr, lbl}
34+
|Found: (lbl: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, lbl}
3535
|Required: (boundary.Label[Result[Future[T], E]]^{cap.rd}) ?=> Future[T]
3636
|
3737
|where: ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make

‎tests/neg-custom-args/captures/heal-tparam-cs.check

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:10:23 -------------------------------
22
10 | val test1 = localCap { c => // error
33
| ^
4-
|Found: (c: Capp^) ->? () ->{c} Unit
4+
|Found: (c: Capp^?) ->? () ->{c} Unit
55
|Required: (c: Capp^) => () ->? Unit
66
|
77
|where: => refers to a fresh root capability created in value test1 when checking argument to parameter op of method localCap
@@ -16,7 +16,7 @@
1616
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:15:13 -------------------------------
1717
15 | localCap { c => // error
1818
| ^
19-
| Found: (x$0: Capp^) ->? () ->{x$0} Unit
19+
| Found: (x$0: Capp^?) ->? () ->{x$0} Unit
2020
| Required: (c: Capp^) -> () => Unit
2121
|
2222
| where: => refers to a root capability associated with the result type of (c: Capp^): () => Unit
@@ -31,7 +31,7 @@
3131
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:25:13 -------------------------------
3232
25 | localCap { c => // error
3333
| ^
34-
| Found: (x$0: Capp^{io}) ->? () ->{x$0} Unit
34+
| Found: (x$0: Capp^?) ->? () ->{x$0} Unit
3535
| Required: (c: Capp^{io}) -> () ->{net} Unit
3636
26 | (c1: Capp^{io}) => () => { c1.use() }
3737
27 | }

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,13 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923.scala:12:21 ---------------------------------------
22
12 | val leak = withCap(cap => mkId(cap)) // error
33
| ^^^^^^^^^^^^^^^^
4-
|Found: (lcap: scala.caps.Capability^{cap.rd}) ?->? Cap^{lcap} ->? Id[Cap^{cap².rd}]^?
4+
|Found: (lcap: scala.caps.Capability^{cap.rd}) ?->? Cap^? ->? Id[Cap^?]^?
55
|Required: (lcap: scala.caps.Capability^{cap.rd}) ?-> Cap^{lcap} => Id[Cap^?]^?
66
|
7-
|where: => refers to a root capability associated with the result type of (using lcap: scala.caps.Capability^{cap.rd}): Cap^{lcap} => Id[Cap^?]^?
8-
| cap is the universal root capability
9-
| cap² is a root capability associated with the result type of (x$0: Cap^{lcap}): Id[Cap^{cap².rd}]^?
7+
|where: => refers to a root capability associated with the result type of (using lcap: scala.caps.Capability^{cap.rd}): Cap^{lcap} => Id[Cap^?]^?
8+
| cap is the universal root capability
109
|
11-
|Note that reference <cap of (x$0: Cap^{lcap}): Id[Cap^{cap.rd}]^?>.rd
10+
|Note that reference <cap of (x$0: Cap^?): Id[Cap^?]^?>.rd
1211
|cannot be included in outer capture set ?
1312
|
1413
| longer explanation available when compiling with `-explain`

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

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,14 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923a.scala:7:21 ---------------------------------------
22
7 | val leak = withCap(lcap => () => mkId(lcap)) // error
33
| ^^^^^^^^^^^^^^^^^^^^^^^^
4-
|Found: (lcap: Cap^) ->? () ->? Id[Cap^²]^?
4+
|Found: (lcap: Cap^?) ->? () ->? Id[Cap^?]^?
55
|Required: (lcap: Cap^) => () =>² Id[Cap^?]^?
66
|
77
|where: => refers to a fresh root capability created in value leak when checking argument to parameter op of method withCap
88
| =>² refers to a root capability associated with the result type of (lcap: Cap^): () =>² Id[Cap^?]^?
99
| ^ refers to the universal root capability
10-
| ^² refers to a root capability associated with the result type of (): Id[Cap^²]^?
1110
|
12-
|Note that reference <cap of (): Id[Cap^]^?>
11+
|Note that reference <cap of (): Id[Cap^?]^?>
1312
|cannot be included in outer capture set ?
1413
|
1514
| longer explanation available when compiling with `-explain`

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,25 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:13:4 ----------------------------------------
22
13 | (ref1, f1) => map[A, B](ref1, f1) // error
33
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
4-
|Found: (ref1: LazyRef[A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?) ->? LazyRef[B^?]{val elem: () =>² B^?}^{f1, ref1}
5-
|Required: (LazyRef[A]^{io}, A => B) =>³ LazyRef[B]^
4+
|Found: (ref1: LazyRef[A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?) ->? LazyRef[B^?]{val elem: () => B^?}^{f1, ref1}
5+
|Required: (LazyRef[A]^{io}, A =>² B) =>³ LazyRef[B]^
66
|
7-
|where: => refers to the universal root capability
8-
| =>² refers to a root capability associated with the result type of (ref1: LazyRef[A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?): LazyRef[B^?]{val elem: () =>² B^?}^{f1, ref1}
7+
|where: => refers to a root capability associated with the result type of (ref1: LazyRef[A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?): LazyRef[B^?]{val elem: () => B^?}^{f1, ref1}
8+
| =>² refers to the universal root capability
99
| =>³ refers to a fresh root capability in the result type of method mapc
1010
| ^ refers to a fresh root capability in the result type of method mapc
1111
|
1212
| longer explanation available when compiling with `-explain`
1313
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:15:4 ----------------------------------------
1414
15 | (ref1, f1) => map[A, B](ref1, f1) // error
1515
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
16-
|Found: (ref1: LazyRef[A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?) ->? LazyRef[B^?]{val elem: () =>² B^?}^{f1, ref1}
17-
|Required: (ref: LazyRef[A]^{io}, f: A => B) =>³ LazyRef[B]^
16+
|Found: (ref1: LazyRef[A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?) ->? LazyRef[B^?]{val elem: () => B^?}^{f1, ref1}
17+
|Required: (ref: LazyRef[A]^{io}, f: A =>² B) =>³ LazyRef[B]^
1818
|
19-
|where: => refers to the universal root capability
20-
| =>² refers to a root capability associated with the result type of (ref1: LazyRef[A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?): LazyRef[B^?]{val elem: () =>² B^?}^{f1, ref1}
19+
|where: => refers to a root capability associated with the result type of (ref1: LazyRef[A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?): LazyRef[B^?]{val elem: () => B^?}^{f1, ref1}
20+
| =>² refers to the universal root capability
2121
| =>³ refers to a fresh root capability in the result type of method mapd
22-
| ^ refers to a root capability associated with the result type of (ref: LazyRef[A]^{io}, f: A => B): LazyRef[B]^
22+
| ^ refers to a root capability associated with the result type of (ref: LazyRef[A]^{io}, f: A =>² B): LazyRef[B]^
2323
|
2424
|Note that the existential capture root in LazyRef[B]^
2525
|cannot subsume the capability f1.type since that capability is not a SharedCapability

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:15:23 ---------------------------------------
1616
15 | val a = usingIO[IO^](x => x) // error // error
1717
| ^^^^^^
18-
|Found: (x: IO^) ->? IO^{x}
18+
|Found: (x: IO^?) ->? IO^{x}
1919
|Required: IO^ => IO^²
2020
|
2121
|where: => refers to a fresh root capability created in value a when checking argument to parameter op of method usingIO

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,11 @@
1010
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
1111
15 | files.map(new Logger(_)) // error, Q: can we improve the error message?
1212
| ^^^^^^^^^^^^^
13-
|Found: (_$1: File^{files*}) ->{files*} Logger{val f: File^{_$1}}^{cap.rd, _$1}
13+
|Found: (_$1: File^?) ->{files*} Logger{val f: File^{_$1}}^{cap.rd, _$1}
1414
|Required: File^{files*} => Logger{val f: File^?}^?
1515
|
1616
|where: => refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map
17-
| cap is a root capability associated with the result type of (_$1: File^{files*}): Logger{val f: File^{_$1}}^{cap.rd, _$1}
17+
| cap is a root capability associated with the result type of (_$1: File^?): Logger{val f: File^{_$1}}^{cap.rd, _$1}
1818
|
1919
|Note that reference <cap of (_$1: File^{files*}): Logger{val f: File^?}^?>.rd
2020
|cannot be included in outer capture set ?

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

Lines changed: 13 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -34,51 +34,19 @@
3434
| This type hides capabilities {LazyRef.this.elem}
3535
|
3636
| where: => refers to a fresh root capability in the type of value get
37-
-- Error: tests/neg-custom-args/captures/lazyref.scala:23:13 -----------------------------------------------------------
38-
23 | val ref3 = ref1.map(g) // error: separation failure
39-
| ^^^^
40-
| Separation failure: Illegal access to {cap1} which is hidden by the previous definition
41-
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
42-
| This type hides capabilities {LazyRef.this.elem, cap1}
43-
|
44-
| where: => refers to a fresh root capability in the type of value elem
45-
-- Error: tests/neg-custom-args/captures/lazyref.scala:26:9 ------------------------------------------------------------
46-
26 | if cap1 == cap2 // error: separation failure // error: separation failure
47-
| ^^^^
48-
| Separation failure: Illegal access to {cap1} which is hidden by the previous definition
49-
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
50-
| This type hides capabilities {LazyRef.this.elem, ref2*, cap1}
51-
|
52-
| where: => refers to a fresh root capability in the type of value elem
53-
-- Error: tests/neg-custom-args/captures/lazyref.scala:26:17 -----------------------------------------------------------
54-
26 | if cap1 == cap2 // error: separation failure // error: separation failure
55-
| ^^^^
56-
| Separation failure: Illegal access to {cap2} which is hidden by the previous definition
57-
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
58-
| This type hides capabilities {LazyRef.this.elem, ref2*, cap1}
59-
|
60-
| where: => refers to a fresh root capability in the type of value elem
61-
-- Error: tests/neg-custom-args/captures/lazyref.scala:27:11 -----------------------------------------------------------
62-
27 | then ref1 // error: separation failure
63-
| ^^^^
64-
| Separation failure: Illegal access to {cap1, ref1} which is hidden by the previous definition
65-
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
66-
| This type hides capabilities {LazyRef.this.elem, ref2*, cap1}
67-
|
68-
| where: => refers to a fresh root capability in the type of value elem
69-
-- Error: tests/neg-custom-args/captures/lazyref.scala:28:11 -----------------------------------------------------------
70-
28 | else ref2) // error: separation failure
71-
| ^^^^
72-
| Separation failure: Illegal access to {cap1, cap2, ref1} which is hidden by the previous definition
73-
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
74-
| This type hides capabilities {LazyRef.this.elem, ref2*, cap1}
75-
|
76-
| where: => refers to a fresh root capability in the type of value elem
7737
-- Error: tests/neg-custom-args/captures/lazyref.scala:29:9 ------------------------------------------------------------
7838
29 | .map(g) // error: separation failure
7939
| ^
80-
| Separation failure: Illegal access to {cap2} which is hidden by the previous definition
81-
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
82-
| This type hides capabilities {LazyRef.this.elem, ref2*, cap1}
83-
|
84-
| where: => refers to a fresh root capability in the type of value elem
40+
|Separation failure: argument of type (x: Int) ->{cap2} Int
41+
|to method map: [U](f: T => U): LazyRef[U]^{f, LazyRef.this}
42+
|corresponds to capture-polymorphic formal parameter f of type Int => Int
43+
|and hides capabilities {cap2}.
44+
|Some of these overlap with the captures of the function prefix with type (LazyRef[Int]{val elem: () ->{ref2*} Int} | (ref1 : LazyRef[Int]{val elem: () ->{cap1} Int}^{cap1}))^{ref2}.
45+
|
46+
| Hidden set of current argument : {cap2}
47+
| Hidden footprint of current argument : {cap2}
48+
| Capture set of function prefix : {ref1, ref2, ref2*}
49+
| Footprint set of function prefix : {ref1, ref2, ref2*, cap1, cap2}
50+
| The two sets overlap at : {cap2}
51+
|
52+
|where: => refers to a fresh root capability created in value ref4 when checking argument to parameter f of method map

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,11 @@ def test(cap1: Cap, cap2: Cap) =
2020
val ref1c: LazyRef[Int] = ref1 // error
2121
val ref2 = map(ref1, g)
2222
val ref2c: LazyRef[Int]^{cap2} = ref2 // error
23-
val ref3 = ref1.map(g) // error: separation failure
23+
val ref3 = ref1.map(g)
2424
val ref3c: LazyRef[Int]^{ref1} = ref3 // error
2525
val ref4 = (
26-
if cap1 == cap2 // error: separation failure // error: separation failure
27-
then ref1 // error: separation failure
28-
else ref2) // error: separation failure
26+
if cap1 == cap2
27+
then ref1
28+
else ref2)
2929
.map(g) // error: separation failure
3030
val ref4c: LazyRef[Int]^{cap1} = ref4 // error

‎tests/neg-custom-args/captures/leaking-iterators.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaking-iterators.scala:56:16 ----------------------------
22
56 | usingLogFile: log => // error
33
| ^
4-
|Found: (log: java.io.FileOutputStream^) ->? cctest.Iterator[Int]^{log}
4+
|Found: (log: java.io.FileOutputStream^?) ->? cctest.Iterator[Int]^{log}
55
|Required: java.io.FileOutputStream^ => cctest.Iterator[Int]^?
66
|
77
|where: => refers to a fresh root capability created in method test when checking argument to parameter op of method usingLogFile

‎tests/neg-custom-args/captures/ro-mut-conformance.check

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
-- Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:8:4 --------------------------------------------------
2-
8 | a.set(42) // error
3-
| ^^^^^
4-
| cannot call update method set from (a : Ref),
5-
| since its capture set {a} is read-only
6-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:10:21 ---------------------------
7-
10 | val t: Ref^{cap} = a // error
1+
-- Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:10:4 -------------------------------------------------
2+
10 | a.set(42) // error
3+
| ^^^^^
4+
| cannot call update method set from (a : Ref),
5+
| since its capture set {a} is read-only
6+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:12:21 ---------------------------
7+
12 | val t: Ref^{cap} = a // error
88
| ^
99
| Found: (a : Ref)
1010
| Required: Ref^

‎tests/neg-custom-args/captures/ro-mut-conformance.scala

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
11
import language.experimental.captureChecking
22
import caps.*
3-
class Ref extends Mutable:
3+
trait IRef:
4+
def get: Int
5+
class Ref extends IRef, Mutable:
46
private var _data: Int = 0
57
def get: Int = _data
68
update def set(x: Int): Unit = _data = x
79
def test1(a: Ref^{cap.rd}): Unit =
810
a.set(42) // error
911
def test2(a: Ref^{cap.rd}): Unit =
1012
val t: Ref^{cap} = a // error
13+
def b: Ref^{cap.rd} = ???
14+
val i: IRef^{cap} = b // ok, no added privilege from `cap` on an IRef
1115
t.set(42)

‎tests/neg-custom-args/captures/simple-using.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/simple-using.scala:8:15 ----------------------------------
22
8 | usingLogFile { f => () => f.write(2) } // error
33
| ^^^^^^^^^^^^^^^^^^^^^^^^^
4-
|Found: (f: java.io.FileOutputStream^) ->? () ->{f} Unit
4+
|Found: (f: java.io.FileOutputStream^?) ->? () ->{f} Unit
55
|Required: java.io.FileOutputStream^ => () ->? Unit
66
|
77
|where: => refers to a fresh root capability created in method test when checking argument to parameter op of method usingLogFile

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:22:27 ---------------------------------
22
22 | val later = usingLogFile { f => () => f.write(0) } // error
33
| ^^^^^^^^^^^^^^^^^^^^^^^^^
4-
|Found: (f: java.io.FileOutputStream^) ->? () ->{f} Unit
4+
|Found: (f: java.io.FileOutputStream^?) ->? () ->{f} Unit
55
|Required: java.io.FileOutputStream^ => () ->? Unit
66
|
77
|where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingLogFile
@@ -14,7 +14,7 @@
1414
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:27:36 ---------------------------------
1515
27 | private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error
1616
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
17-
|Found: (f: java.io.FileOutputStream^) ->? Test2.Cell[() ->{f} Unit]^?
17+
|Found: (f: java.io.FileOutputStream^?) ->? Test2.Cell[() ->{f} Unit]^?
1818
|Required: java.io.FileOutputStream^ => Test2.Cell[() ->? Unit]^?
1919
|
2020
|where: => refers to a fresh root capability created in value later2 when checking argument to parameter op of method usingLogFile
@@ -27,7 +27,7 @@
2727
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:43:33 ---------------------------------
2828
43 | val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
2929
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
30-
|Found: (f: java.io.OutputStream^) ->? Int ->{f} Unit
30+
|Found: (f: java.io.OutputStream^?) ->? Int ->{f} Unit
3131
|Required: java.io.OutputStream^ => Int ->? Unit
3232
|
3333
|where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingFile
@@ -40,7 +40,7 @@
4040
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:52:6 ----------------------------------
4141
52 | usingLogger(_, l => () => l.log("test"))) // error after checking mapping scheme
4242
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
43-
|Found: (_$1: java.io.OutputStream^) ->? () ->{_$1} Unit
43+
|Found: (_$1: java.io.OutputStream^?) ->? () ->{_$1} Unit
4444
|Required: java.io.OutputStream^ => () ->? Unit
4545
|
4646
|where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingFile

0 commit comments

Comments
 (0)
Please sign in to comment.