diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 6684c6615bc8..47c96e604784 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -178,12 +178,7 @@ sealed abstract class CaptureSet extends Showable: /** Try to include all element in `refs` to this capture set. */ protected final def tryInclude(newElems: Refs, origin: CaptureSet)(using Context, VarState): Boolean = - TypeComparer.inNestedLevel: - // Run in nested level so that a error notes for a failure here can be - // cancelled in case the whole comparison succeeds. - // We do this here because all nested tryInclude and subCaptures calls go - // through this method. - newElems.forall(tryInclude(_, origin)) + newElems.forall(tryInclude(_, origin)) protected def mutableToReader(origin: CaptureSet)(using Context): Boolean = if mutability == Mutable then toReader() else true @@ -284,16 +279,14 @@ sealed abstract class CaptureSet extends Showable: /** The subcapturing test, using a given VarState */ final def subCaptures(that: CaptureSet)(using ctx: Context, vs: VarState = VarState()): Boolean = - val this1 = this.adaptMutability(that) - if this1 == null then false - else if this1 ne this then - capt.println(i"WIDEN ro $this with ${this.mutability} <:< $that with ${that.mutability} to $this1") - this1.subCaptures(that, vs) - else if that.tryInclude(elems, this) then - addDependent(that) - else - varState.rollBack() - false + TypeComparer.inNestedLevel: + val this1 = this.adaptMutability(that) + if this1 == null then false + else if this1 ne this then + capt.println(i"WIDEN ro $this with ${this.mutability} <:< $that with ${that.mutability} to $this1") + this1.subCaptures(that, vs) + else + that.tryInclude(elems, this) && addDependent(that) /** Two capture sets are considered =:= equal if they mutually subcapture each other * in a frozen state. @@ -662,30 +655,6 @@ object CaptureSet: var description: String = "" - /** Record current elements in given VarState provided it does not yet - * contain an entry for this variable. - */ - private def recordElemsState()(using VarState): Boolean = - varState.getElems(this) match - case None => varState.putElems(this, elems) - case _ => true - - /** Record current dependent sets in given VarState provided it does not yet - * contain an entry for this variable. - */ - private[CaptureSet] def recordDepsState()(using VarState): Boolean = - varState.getDeps(this) match - case None => varState.putDeps(this, deps) - case _ => true - - /** Reset elements to what was recorded in `state` */ - def resetElems()(using state: VarState): Unit = - elems = state.elems(this) - - /** Reset dependent sets to what was recorded in `state` */ - def resetDeps()(using state: VarState): Unit = - deps = state.deps(this) - /** Check that all maps recorded in skippedMaps map `elem` to itself * or something subsumed by it. */ @@ -695,8 +664,20 @@ object CaptureSet: assert(elem.subsumes(elem1), i"Skipped map ${tm.getClass} maps newly added $elem to $elem1 in $this") + protected def includeElem(elem: Capability)(using Context): Unit = + if !elems.contains(elem) then + elems += elem + TypeComparer.logUndoAction: () => + elems -= elem + + def includeDep(cs: CaptureSet)(using Context): Unit = + if !deps.contains(cs) then + deps += cs + TypeComparer.logUndoAction: () => + deps -= cs + final def addThisElem(elem: Capability)(using Context, VarState): Boolean = - if isConst || !recordElemsState() then // Fail if variable is solved or given VarState is frozen + if isConst || !varState.canRecord then // Fail if variable is solved or given VarState is frozen addIfHiddenOrFail(elem) else if !levelOK(elem) then failWith(IncludeFailure(this, elem, levelError = true)) // or `elem` is not visible at the level of the set. @@ -704,7 +685,7 @@ object CaptureSet: // id == 108 then assert(false, i"trying to add $elem to $this") assert(elem.isWellformed, elem) assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState]) - elems += elem + includeElem(elem) if isBadRoot(rootLimit, elem) then rootAddedHandler() newElemAddedHandler(elem) @@ -772,7 +753,7 @@ object CaptureSet: (cs eq this) || cs.isUniversal || isConst - || recordDepsState() && { deps += cs; true } + || varState.canRecord && { includeDep(cs); true } override def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type = rootLimit = upto @@ -1126,7 +1107,7 @@ object CaptureSet: if alias ne this then alias.add(elem) else def addToElems() = - elems += elem + includeElem(elem) deps.foreach: dep => assert(dep != this) vs.addHidden(dep.asInstanceOf[HiddenSet], elem) @@ -1142,7 +1123,7 @@ object CaptureSet: deps = SimpleIdentitySet(elem.hiddenSet) else addToElems() - elem.hiddenSet.deps += this + elem.hiddenSet.includeDep(this) case _ => addToElems() @@ -1238,41 +1219,15 @@ object CaptureSet: */ class VarState: - /** A map from captureset variables to their elements at the time of the snapshot. */ - private val elemsMap: util.EqHashMap[Var, Refs] = new util.EqHashMap - - /** A map from captureset variables to their dependent sets at the time of the snapshot. */ - private val depsMap: util.EqHashMap[Var, Deps] = new util.EqHashMap - /** A map from ResultCap values to other ResultCap values. If two result values * `a` and `b` are unified, then `eqResultMap(a) = b` and `eqResultMap(b) = a`. */ private var eqResultMap: util.SimpleIdentityMap[ResultCap, ResultCap] = util.SimpleIdentityMap.empty - /** A snapshot of the `eqResultMap` value at the start of a VarState transaction */ - private var eqResultSnapshot: util.SimpleIdentityMap[ResultCap, ResultCap] | Null = null - - /** The recorded elements of `v` (it's required that a recording was made) */ - def elems(v: Var): Refs = elemsMap(v) - - /** Optionally the recorded elements of `v`, None if nothing was recorded for `v` */ - def getElems(v: Var): Option[Refs] = elemsMap.get(v) - /** Record elements, return whether this was allowed. * By default, recording is allowed in regular but not in frozen states. */ - def putElems(v: Var, elems: Refs): Boolean = { elemsMap(v) = elems; true } - - /** The recorded dependent sets of `v` (it's required that a recording was made) */ - def deps(v: Var): Deps = depsMap(v) - - /** Optionally the recorded dependent sets of `v`, None if nothing was recorded for `v` */ - def getDeps(v: Var): Option[Deps] = depsMap.get(v) - - /** Record dependent sets, return whether this was allowed. - * By default, recording is allowed in regular but not in frozen states. - */ - def putDeps(v: Var, deps: Deps): Boolean = { depsMap(v) = deps; true } + def canRecord: Boolean = true /** Does this state allow additions of elements to capture set variables? */ def isOpen = true @@ -1283,11 +1238,6 @@ object CaptureSet: * but the special state VarState.Separate overrides this. */ def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean = - elemsMap.get(hidden) match - case None => - elemsMap(hidden) = hidden.elems - depsMap(hidden) = hidden.deps - case _ => hidden.add(elem)(using ctx, this) true @@ -1311,17 +1261,13 @@ object CaptureSet: && eqResultMap(c1) == null && eqResultMap(c2) == null && { - if eqResultSnapshot == null then eqResultSnapshot = eqResultMap eqResultMap = eqResultMap.updated(c1, c2).updated(c2, c1) + TypeComparer.logUndoAction: () => + eqResultMap.remove(c1) + eqResultMap.remove(c2) true } - /** Roll back global state to what was recorded in this VarState */ - def rollBack(): Unit = - elemsMap.keysIterator.foreach(_.resetElems()(using this)) - depsMap.keysIterator.foreach(_.resetDeps()(using this)) - if eqResultSnapshot != null then eqResultMap = eqResultSnapshot.nn - private var seen: util.EqHashSet[Capability] = new util.EqHashSet /** Run test `pred` unless `ref` was seen in an enclosing `ifNotSeen` operation */ @@ -1341,8 +1287,7 @@ object CaptureSet: * subsume arbitary types, which are then recorded in their hidden sets. */ class Closed extends VarState: - override def putElems(v: Var, refs: Refs) = false - override def putDeps(v: Var, deps: Deps) = false + override def canRecord = false override def isOpen = false override def toString = "closed varState" @@ -1366,14 +1311,21 @@ object CaptureSet: */ def HardSeparate(using Context): Separating = ccState.HardSeparate - /** A special state that turns off recording of elements. Used only - * in `addSub` to prevent cycles in recordings. Instantiated in ccState.Unrecorded. - */ - class Unrecorded extends VarState: - override def putElems(v: Var, refs: Refs) = true - override def putDeps(v: Var, deps: Deps) = true - override def rollBack(): Unit = () + /** A mixin trait that overrides the addHidden and unify operations to + * not depend in state. */ + trait Stateless extends VarState: + + /** Allow adding hidden elements, but don't store them */ override def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean = true + + /** Don't allow to unify result caps */ + override def unify(c1: ResultCap, c2: ResultCap)(using Context): Boolean = false + end Stateless + + /** An open state that turns off recording of hidden elements (but allows + * adding them). Used in `addAsDependentTo`. Instantiated in ccState.Unrecorded. + */ + class Unrecorded extends VarState, Stateless: override def toString = "unrecorded varState" def Unrecorded(using Context): Unrecorded = ccState.Unrecorded @@ -1381,8 +1333,7 @@ object CaptureSet: /** A closed state that turns off recording of hidden elements (but allows * adding them). Used in `mightAccountFor`. Instantiated in ccState.ClosedUnrecorded. */ - class ClosedUnrecorded extends Closed: - override def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean = true + class ClosedUnrecorded extends Closed, Stateless: override def toString = "closed unrecorded varState" def ClosedUnrecorded(using Context): ClosedUnrecorded = ccState.ClosedUnrecorded diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 97a32e66f30e..eb03a2b1c05d 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -53,7 +53,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling needsGc = false maxErrorLevel = -1 errorNotes = Nil - logSize = 0 + undoLog.clear() if Config.checkTypeComparerReset then checkReset() private var pendingSubTypes: util.MutableSet[(Type, Type)] | Null = null @@ -63,8 +63,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling private var maxErrorLevel: Int = -1 protected var errorNotes: List[(Int, ErrorNote)] = Nil - private val undoLog = mutable.ArrayBuffer[() => Unit]() - private var logSize = 0 + val undoLog = mutable.ArrayBuffer[() => Unit]() private var needsGc = false @@ -1588,6 +1587,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling undoLog(i)() i += 1 undoLog.takeInPlace(prevSize) + assert(undoLog.size == prevSize) // begin recur if tp2 eq NoType then false @@ -1595,11 +1595,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling else val savedCstr = constraint val savedGadt = ctx.gadt - val savedLogSize = logSize + val savedLogSize = undoLog.size inline def restore() = state.constraint = savedCstr ctx.gadtState.restore(savedGadt) if undoLog.size != savedLogSize then + //println(i"ROLLBACK $tp1 <:< $tp2") rollBack(savedLogSize) val savedSuccessCount = successCount try diff --git a/tests/neg-custom-args/captures/capt-depfun.check b/tests/neg-custom-args/captures/capt-depfun.check index a5db4da7a319..369c9915bbe0 100644 --- a/tests/neg-custom-args/captures/capt-depfun.check +++ b/tests/neg-custom-args/captures/capt-depfun.check @@ -1,5 +1,5 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:11:43 ---------------------------------- -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 | ^^^^^^^ | Found: Str^{} ->{ac, y, z} Str^{y, z} | Required: Str^{y, z} => Str^{y, z} @@ -7,8 +7,3 @@ | where: => refers to a fresh root capability in the type of value dc | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/capt-depfun.scala:11:24 ------------------------------------------------------- -11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon - | ^^^^^^^^^^^^^^^^^^^^^^^^^^ - | Separation failure: value dc's type Str^{y, z} => Str^{y, z} hides parameters y and z. - | The parameters need to be annotated with @consume to allow this. diff --git a/tests/neg-custom-args/captures/capt-depfun.scala b/tests/neg-custom-args/captures/capt-depfun.scala index d9033c9e5264..e973bc0486ff 100644 --- a/tests/neg-custom-args/captures/capt-depfun.scala +++ b/tests/neg-custom-args/captures/capt-depfun.scala @@ -8,4 +8,4 @@ class Str def f(y: Cap, z: Cap) = def g(): C @retains[y.type | z.type] = ??? val ac: ((x: Cap) => Str @retains[x.type] => Str @retains[x.type]) = ??? - val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon + val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error diff --git a/tests/neg-custom-args/captures/depfun-reach.check b/tests/neg-custom-args/captures/depfun-reach.check index 9f47722078aa..9aaac1132218 100644 --- a/tests/neg-custom-args/captures/depfun-reach.check +++ b/tests/neg-custom-args/captures/depfun-reach.check @@ -27,8 +27,3 @@ | =>² refers to a fresh root capability in the type of value b | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/depfun-reach.scala:18:17 ------------------------------------------------------ -18 | : (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] = // error - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Separation failure: method foo's result type (xs: List[(X, box () ->{io} Unit)]) => List[() -> Unit] hides parameter op. - |The parameter needs to be annotated with @consume to allow this. diff --git a/tests/neg-custom-args/captures/depfun-reach.scala b/tests/neg-custom-args/captures/depfun-reach.scala index 074a9429bec4..f9a4589ab5c4 100644 --- a/tests/neg-custom-args/captures/depfun-reach.scala +++ b/tests/neg-custom-args/captures/depfun-reach.scala @@ -15,7 +15,7 @@ def test(io: Object^, async: Object^) = compose(op) def foo[X](op: (xs: List[(X, () ->{io} Unit)]) => List[() ->{xs*} Unit]) - : (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] = // error + : (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] = op // error def boom(op: List[(() ->{async} Unit, () ->{io} Unit)]): List[() ->{} Unit] = diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.check b/tests/neg-custom-args/captures/effect-swaps-explicit.check index 469a0c6f14a4..5355f80a22a9 100644 --- a/tests/neg-custom-args/captures/effect-swaps-explicit.check +++ b/tests/neg-custom-args/captures/effect-swaps-explicit.check @@ -17,7 +17,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:69:10 ------------------------ 69 | Future: fut ?=> // error, type mismatch | ^ - |Found: (contextual$9: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^) ?->{fr, async} + |Found: (contextual$9: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^?) ?->{fr, async} | box Future[box T^?]^{fr, contextual$9} |Required: (contextual$9: boundary.Label[Result[box Future[box T^?]^?, box E^?]]^) ?=> box Future[box T^?]^? | @@ -32,7 +32,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:73:35 ------------------------ 73 | Result.make[Future[T], E]: lbl ?=> // error: type mismatch | ^ - |Found: (lbl: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^) ?->{fr, async} Future[box T^?]^{fr, lbl} + |Found: (lbl: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^?) ?->{fr, async} Future[box T^?]^{fr, lbl} |Required: (lbl: boundary.Label[Result[Future[T], E]]^) ?=> Future[T] | |where: ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make diff --git a/tests/neg-custom-args/captures/effect-swaps.check b/tests/neg-custom-args/captures/effect-swaps.check index 69cedcde2f75..13147b3e976e 100644 --- a/tests/neg-custom-args/captures/effect-swaps.check +++ b/tests/neg-custom-args/captures/effect-swaps.check @@ -17,7 +17,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:69:10 --------------------------------- 69 | Future: fut ?=> // error, type mismatch | ^ - |Found: (contextual$9: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^{cap.rd}) ?->{fr, async} + |Found: (contextual$9: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^?) ?->{fr, async} | box Future[box T^?]^{fr, contextual$9} |Required: (contextual$9: boundary.Label[Result[box Future[box T^?]^?, box E^?]]^{cap.rd}) ?=> box Future[box T^?]^? | @@ -32,7 +32,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:73:35 --------------------------------- 73 | Result.make[Future[T], E]: lbl ?=> // error: type mismatch | ^ - |Found: (lbl: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^{cap.rd}) ?->{fr, async} Future[box T^?]^{fr, lbl} + |Found: (lbl: boundary.Label[box Result[box Future[box T^?]^?, box E^?]^?]^?) ?->{fr, async} Future[box T^?]^{fr, lbl} |Required: (lbl: boundary.Label[Result[Future[T], E]]^{cap.rd}) ?=> Future[T] | |where: ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make diff --git a/tests/neg-custom-args/captures/heal-tparam-cs.check b/tests/neg-custom-args/captures/heal-tparam-cs.check index 0a7c333c9e95..042c5723bf8a 100644 --- a/tests/neg-custom-args/captures/heal-tparam-cs.check +++ b/tests/neg-custom-args/captures/heal-tparam-cs.check @@ -1,7 +1,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:10:23 ------------------------------- 10 | val test1 = localCap { c => // error | ^ - |Found: (c: Capp^) ->? box () ->{c} Unit + |Found: (c: Capp^?) ->? box () ->{c} Unit |Required: (c: Capp^) => box () ->? Unit | |where: => refers to a fresh root capability created in value test1 when checking argument to parameter op of method localCap @@ -16,7 +16,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:15:13 ------------------------------- 15 | localCap { c => // error | ^ - | Found: (x$0: Capp^) ->? () ->{x$0} Unit + | Found: (x$0: Capp^?) ->? () ->{x$0} Unit | Required: (c: Capp^) -> () => Unit | | where: => refers to a root capability associated with the result type of (c: Capp^): () => Unit @@ -31,7 +31,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:25:13 ------------------------------- 25 | localCap { c => // error | ^ - | Found: (x$0: Capp^{io}) ->? () ->{x$0} Unit + | Found: (x$0: Capp^?) ->? () ->{x$0} Unit | Required: (c: Capp^{io}) -> () ->{net} Unit 26 | (c1: Capp^{io}) => () => { c1.use() } 27 | } diff --git a/tests/neg-custom-args/captures/i15923.check b/tests/neg-custom-args/captures/i15923.check index 4d3019f92d7a..09a82e27de03 100644 --- a/tests/neg-custom-args/captures/i15923.check +++ b/tests/neg-custom-args/captures/i15923.check @@ -1,14 +1,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923.scala:12:21 --------------------------------------- 12 | val leak = withCap(cap => mkId(cap)) // error | ^^^^^^^^^^^^^^^^ - |Found: (lcap: scala.caps.Capability^{cap.rd}) ?->? Cap^{lcap} ->? box Id[box Cap^{cap².rd}]^? + |Found: (lcap: scala.caps.Capability^{cap.rd}) ?->? Cap^? ->? box Id[box Cap^?]^? |Required: (lcap: scala.caps.Capability^{cap.rd}) ?-> Cap^{lcap} => box Id[box Cap^?]^? | - |where: => refers to a root capability associated with the result type of (using lcap: scala.caps.Capability^{cap.rd}): Cap^{lcap} => box Id[box Cap^?]^? - | cap is the universal root capability - | cap² is a root capability associated with the result type of (x$0: Cap^{lcap}): box Id[box Cap^{cap².rd}]^? + |where: => refers to a root capability associated with the result type of (using lcap: scala.caps.Capability^{cap.rd}): Cap^{lcap} => box Id[box Cap^?]^? + | cap is the universal root capability | - |Note that reference .rd + |Note that reference .rd |cannot be included in outer capture set ? | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i15923a.check b/tests/neg-custom-args/captures/i15923a.check index 1b4ef98aff20..e395eb22b0a4 100644 --- a/tests/neg-custom-args/captures/i15923a.check +++ b/tests/neg-custom-args/captures/i15923a.check @@ -1,15 +1,14 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923a.scala:7:21 --------------------------------------- 7 | val leak = withCap(lcap => () => mkId(lcap)) // error | ^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (lcap: Cap^) ->? () ->? box Id[box Cap^²]^? + |Found: (lcap: Cap^?) ->? () ->? box Id[box Cap^?]^? |Required: (lcap: Cap^) => () =>² box Id[box Cap^?]^? | |where: => refers to a fresh root capability created in value leak when checking argument to parameter op of method withCap | =>² refers to a root capability associated with the result type of (lcap: Cap^): () =>² box Id[box Cap^?]^? | ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (): box Id[box Cap^²]^? | - |Note that reference + |Note that reference |cannot be included in outer capture set ? | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i16226.check b/tests/neg-custom-args/captures/i16226.check index 4fb4119fdbef..f179871ab3c2 100644 --- a/tests/neg-custom-args/captures/i16226.check +++ b/tests/neg-custom-args/captures/i16226.check @@ -1,11 +1,11 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:13:4 ---------------------------------------- 13 | (ref1, f1) => map[A, B](ref1, f1) // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (ref1: LazyRef[box A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?) ->? LazyRef[box B^?]{val elem: () =>² B^?}^{f1, ref1} - |Required: (ref1: LazyRef[A]^{io}, f1: A => B) =>³ LazyRef[B]^ + |Found: (ref1: LazyRef[box A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?) ->? LazyRef[box B^?]{val elem: () => B^?}^{f1, ref1} + |Required: (ref1: LazyRef[A]^{io}, f1: A =>² B) =>³ LazyRef[B]^ | - |where: => refers to the universal root capability - | =>² refers to a root capability associated with the result type of (ref1: LazyRef[box A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?): LazyRef[box B^?]{val elem: () =>² B^?}^{f1, ref1} + |where: => refers to a root capability associated with the result type of (ref1: LazyRef[box A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?): LazyRef[box B^?]{val elem: () => B^?}^{f1, ref1} + | =>² refers to the universal root capability | =>³ refers to a fresh root capability in the result type of method mapc | ^ refers to a fresh root capability in the result type of method mapc | @@ -13,13 +13,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:15:4 ---------------------------------------- 15 | (ref1, f1) => map[A, B](ref1, f1) // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (ref1: LazyRef[box A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?) ->? LazyRef[box B^?]{val elem: () =>² B^?}^{f1, ref1} - |Required: (ref: LazyRef[A]^{io}, f: A => B) =>³ LazyRef[B]^ + |Found: (ref1: LazyRef[box A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?) ->? LazyRef[box B^?]{val elem: () => B^?}^{f1, ref1} + |Required: (ref: LazyRef[A]^{io}, f: A =>² B) =>³ LazyRef[B]^ | - |where: => refers to the universal root capability - | =>² refers to a root capability associated with the result type of (ref1: LazyRef[box A^?]{val elem: () => A^?}^{io}, f1: A^? => B^?): LazyRef[box B^?]{val elem: () =>² B^?}^{f1, ref1} + |where: => refers to a root capability associated with the result type of (ref1: LazyRef[box A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?): LazyRef[box B^?]{val elem: () => B^?}^{f1, ref1} + | =>² refers to the universal root capability | =>³ refers to a fresh root capability in the result type of method mapd - | ^ refers to a root capability associated with the result type of (ref: LazyRef[A]^{io}, f: A => B): LazyRef[B]^ + | ^ refers to a root capability associated with the result type of (ref: LazyRef[A]^{io}, f: A =>² B): LazyRef[B]^ | |Note that the existential capture root in LazyRef[B]^ |cannot subsume the capability f1.type since that capability is not a SharedCapability diff --git a/tests/neg-custom-args/captures/i21401.check b/tests/neg-custom-args/captures/i21401.check index 2f0443e90ed9..eb6a5cca35d7 100644 --- a/tests/neg-custom-args/captures/i21401.check +++ b/tests/neg-custom-args/captures/i21401.check @@ -15,7 +15,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:15:23 --------------------------------------- 15 | val a = usingIO[IO^](x => x) // error // error | ^^^^^^ - |Found: (x: IO^) ->? box IO^{x} + |Found: (x: IO^?) ->? box IO^{x} |Required: (x: IO^) => box IO^² | |where: => refers to a fresh root capability created in value a when checking argument to parameter op of method usingIO diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check index 5bc01afa4dd0..d1c9fc270745 100644 --- a/tests/neg-custom-args/captures/i21614.check +++ b/tests/neg-custom-args/captures/i21614.check @@ -10,11 +10,11 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 --------------------------------------- 15 | files.map(new Logger(_)) // error, Q: can we improve the error message? | ^^^^^^^^^^^^^ - |Found: (_$1: box File^{files*}) ->{files*} box Logger{val f: File^{_$1}}^{cap.rd, _$1} + |Found: (_$1: box File^?) ->{files*} box Logger{val f: File^{_$1}}^{cap.rd, _$1} |Required: (_$1: box File^{files*}) => box Logger{val f: File^?}^? | |where: => refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map - | cap is a root capability associated with the result type of (_$1: box File^{files*}): box Logger{val f: File^{_$1}}^{cap.rd, _$1} + | cap is a root capability associated with the result type of (_$1: box File^?): box Logger{val f: File^{_$1}}^{cap.rd, _$1} | |Note that reference .rd |cannot be included in outer capture set ? diff --git a/tests/neg-custom-args/captures/lazyref.check b/tests/neg-custom-args/captures/lazyref.check index dde9e6fd2bac..a8419cb30b12 100644 --- a/tests/neg-custom-args/captures/lazyref.check +++ b/tests/neg-custom-args/captures/lazyref.check @@ -34,51 +34,19 @@ | This type hides capabilities {LazyRef.this.elem} | | where: => refers to a fresh root capability in the type of value get --- Error: tests/neg-custom-args/captures/lazyref.scala:23:13 ----------------------------------------------------------- -23 | val ref3 = ref1.map(g) // error: separation failure - | ^^^^ - | Separation failure: Illegal access to {cap1} which is hidden by the previous definition - | of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}. - | This type hides capabilities {LazyRef.this.elem, cap1} - | - | where: => refers to a fresh root capability in the type of value elem --- Error: tests/neg-custom-args/captures/lazyref.scala:26:9 ------------------------------------------------------------ -26 | if cap1 == cap2 // error: separation failure // error: separation failure - | ^^^^ - | Separation failure: Illegal access to {cap1} which is hidden by the previous definition - | of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}. - | This type hides capabilities {LazyRef.this.elem, ref2*, cap1} - | - | where: => refers to a fresh root capability in the type of value elem --- Error: tests/neg-custom-args/captures/lazyref.scala:26:17 ----------------------------------------------------------- -26 | if cap1 == cap2 // error: separation failure // error: separation failure - | ^^^^ - | Separation failure: Illegal access to {cap2} which is hidden by the previous definition - | of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}. - | This type hides capabilities {LazyRef.this.elem, ref2*, cap1} - | - | where: => refers to a fresh root capability in the type of value elem --- Error: tests/neg-custom-args/captures/lazyref.scala:27:11 ----------------------------------------------------------- -27 | then ref1 // error: separation failure - | ^^^^ - | Separation failure: Illegal access to {cap1, ref1} which is hidden by the previous definition - | of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}. - | This type hides capabilities {LazyRef.this.elem, ref2*, cap1} - | - | where: => refers to a fresh root capability in the type of value elem --- Error: tests/neg-custom-args/captures/lazyref.scala:28:11 ----------------------------------------------------------- -28 | else ref2) // error: separation failure - | ^^^^ - | Separation failure: Illegal access to {cap1, cap2, ref1} which is hidden by the previous definition - | of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}. - | This type hides capabilities {LazyRef.this.elem, ref2*, cap1} - | - | where: => refers to a fresh root capability in the type of value elem -- Error: tests/neg-custom-args/captures/lazyref.scala:29:9 ------------------------------------------------------------ 29 | .map(g) // error: separation failure | ^ - | Separation failure: Illegal access to {cap2} which is hidden by the previous definition - | of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}. - | This type hides capabilities {LazyRef.this.elem, ref2*, cap1} - | - | where: => refers to a fresh root capability in the type of value elem + |Separation failure: argument of type (x: Int) ->{cap2} Int + |to method map: [U](f: T => U): LazyRef[U]^{f, LazyRef.this} + |corresponds to capture-polymorphic formal parameter f of type Int => Int + |and hides capabilities {cap2}. + |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}. + | + | Hidden set of current argument : {cap2} + | Hidden footprint of current argument : {cap2} + | Capture set of function prefix : {ref1, ref2, ref2*} + | Footprint set of function prefix : {ref1, ref2, ref2*, cap1, cap2} + | The two sets overlap at : {cap2} + | + |where: => refers to a fresh root capability created in value ref4 when checking argument to parameter f of method map diff --git a/tests/neg-custom-args/captures/lazyref.scala b/tests/neg-custom-args/captures/lazyref.scala index 396d9470ea17..ea3897484857 100644 --- a/tests/neg-custom-args/captures/lazyref.scala +++ b/tests/neg-custom-args/captures/lazyref.scala @@ -20,11 +20,11 @@ def test(cap1: Cap, cap2: Cap) = val ref1c: LazyRef[Int] = ref1 // error val ref2 = map(ref1, g) val ref2c: LazyRef[Int]^{cap2} = ref2 // error - val ref3 = ref1.map(g) // error: separation failure + val ref3 = ref1.map(g) val ref3c: LazyRef[Int]^{ref1} = ref3 // error val ref4 = ( - if cap1 == cap2 // error: separation failure // error: separation failure - then ref1 // error: separation failure - else ref2) // error: separation failure + if cap1 == cap2 + then ref1 + else ref2) .map(g) // error: separation failure val ref4c: LazyRef[Int]^{cap1} = ref4 // error diff --git a/tests/neg-custom-args/captures/leaking-iterators.check b/tests/neg-custom-args/captures/leaking-iterators.check index a64934c41360..380fdc86fe15 100644 --- a/tests/neg-custom-args/captures/leaking-iterators.check +++ b/tests/neg-custom-args/captures/leaking-iterators.check @@ -1,7 +1,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaking-iterators.scala:56:16 ---------------------------- 56 | usingLogFile: log => // error | ^ - |Found: (log: java.io.FileOutputStream^) ->? box cctest.Iterator[Int]^{log} + |Found: (log: java.io.FileOutputStream^?) ->? box cctest.Iterator[Int]^{log} |Required: (log: java.io.FileOutputStream^) => box cctest.Iterator[Int]^? | |where: => refers to a fresh root capability created in method test when checking argument to parameter op of method usingLogFile diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check index 0a3fe9f0318b..416671d96668 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.check +++ b/tests/neg-custom-args/captures/ro-mut-conformance.check @@ -1,10 +1,10 @@ --- Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:8:4 -------------------------------------------------- -8 | a.set(42) // error - | ^^^^^ - | cannot call update method set from (a : Ref), - | since its capture set {a} is read-only --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:10:21 --------------------------- -10 | val t: Ref^{cap} = a // error +-- Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:10:4 ------------------------------------------------- +10 | a.set(42) // error + | ^^^^^ + | cannot call update method set from (a : Ref), + | since its capture set {a} is read-only +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:12:21 --------------------------- +12 | val t: Ref^{cap} = a // error | ^ | Found: (a : Ref) | Required: Ref^ diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.scala b/tests/neg-custom-args/captures/ro-mut-conformance.scala index 0aecbb2b972e..4b3f34af47f3 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.scala +++ b/tests/neg-custom-args/captures/ro-mut-conformance.scala @@ -1,6 +1,8 @@ import language.experimental.captureChecking import caps.* -class Ref extends Mutable: +trait IRef: + def get: Int +class Ref extends IRef, Mutable: private var _data: Int = 0 def get: Int = _data update def set(x: Int): Unit = _data = x @@ -8,4 +10,6 @@ def test1(a: Ref^{cap.rd}): Unit = a.set(42) // error def test2(a: Ref^{cap.rd}): Unit = val t: Ref^{cap} = a // error + def b: Ref^{cap.rd} = ??? + val i: IRef^{cap} = b // ok, no added privilege from `cap` on an IRef t.set(42) \ No newline at end of file diff --git a/tests/neg-custom-args/captures/simple-using.check b/tests/neg-custom-args/captures/simple-using.check index 3f31f6e41dd2..ecf17a8e8c57 100644 --- a/tests/neg-custom-args/captures/simple-using.check +++ b/tests/neg-custom-args/captures/simple-using.check @@ -1,7 +1,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/simple-using.scala:8:15 ---------------------------------- 8 | usingLogFile { f => () => f.write(2) } // error | ^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (f: java.io.FileOutputStream^) ->? box () ->{f} Unit + |Found: (f: java.io.FileOutputStream^?) ->? box () ->{f} Unit |Required: (f: java.io.FileOutputStream^) => box () ->? Unit | |where: => refers to a fresh root capability created in method test when checking argument to parameter op of method usingLogFile diff --git a/tests/neg-custom-args/captures/usingLogFile.check b/tests/neg-custom-args/captures/usingLogFile.check index 04df1e7aeca6..42ba670a0bf3 100644 --- a/tests/neg-custom-args/captures/usingLogFile.check +++ b/tests/neg-custom-args/captures/usingLogFile.check @@ -1,7 +1,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:22:27 --------------------------------- 22 | val later = usingLogFile { f => () => f.write(0) } // error | ^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (f: java.io.FileOutputStream^) ->? box () ->{f} Unit + |Found: (f: java.io.FileOutputStream^?) ->? box () ->{f} Unit |Required: (f: java.io.FileOutputStream^) => box () ->? Unit | |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingLogFile @@ -14,7 +14,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:27:36 --------------------------------- 27 | private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (f: java.io.FileOutputStream^) ->? box Test2.Cell[box () ->{f} Unit]^? + |Found: (f: java.io.FileOutputStream^?) ->? box Test2.Cell[box () ->{f} Unit]^? |Required: (f: java.io.FileOutputStream^) => box Test2.Cell[box () ->? Unit]^? | |where: => refers to a fresh root capability created in value later2 when checking argument to parameter op of method usingLogFile @@ -27,7 +27,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:43:33 --------------------------------- 43 | val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (f: java.io.OutputStream^) ->? box Int ->{f} Unit + |Found: (f: java.io.OutputStream^?) ->? box Int ->{f} Unit |Required: (f: java.io.OutputStream^) => box Int ->? Unit | |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingFile @@ -40,7 +40,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:52:6 ---------------------------------- 52 | usingLogger(_, l => () => l.log("test"))) // error after checking mapping scheme | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (_$1: java.io.OutputStream^) ->? box () ->{_$1} Unit + |Found: (_$1: java.io.OutputStream^?) ->? box () ->{_$1} Unit |Required: (_$1: java.io.OutputStream^) => box () ->? Unit | |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingFile