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.

Author: odersky

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,16 +664,28 @@ 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.
       else
         // 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,23 +1311,29 @@ 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
 
     /** 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

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,18 +1587,20 @@ 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
     else if tp1 eq tp2 then true
     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

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

@@ -1,14 +1,9 @@
 -- [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}
    |
    |                                         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.

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

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, () ->{io} Unit)]) => List[() -> Unit] hides parameter op.
-   |The parameter needs to be annotated with @consume to allow this.

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] =

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

@@ -17,21 +17,21 @@
 -- [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[Result[Future[T^?]^?, E^?]^?]^) ?->{fr, async} Future[T^?]^{fr, contextual$9}
-   |Required: (boundary.Label[Result[Future[T^?]^{fr, async}, E^?]]^) ?=> Future[T^?]^{fr, async}
+   |Found:    (contextual$9: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, contextual$9}
+   |Required: (boundary.Label[Result[Future[T^?]^?, E^?]]^) ?=> Future[T^?]^?
    |
    |where:    ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make
    |          ^   refers to the universal root capability
    |
    |Note that reference contextual$9.type
-   |cannot be included in outer capture set {fr, async}
+   |cannot be included in outer capture set ?
 70 |            fr.await.ok
    |
    | longer explanation available when compiling with `-explain`
 -- [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[Result[Future[T^?]^?, E^?]^?]^) ?->{fr, async} Future[T^?]^{fr, lbl}
+   |Found:    (lbl: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, lbl}
    |Required: (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

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

@@ -17,21 +17,21 @@
 -- [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[Result[Future[T^?]^?, E^?]^?]^{cap.rd}) ?->{fr, async} Future[T^?]^{fr, contextual$9}
-   |Required: (boundary.Label[Result[Future[T^?]^{fr, async}, E^?]]^{cap.rd}) ?=> Future[T^?]^{fr, async}
+   |Found:    (contextual$9: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, contextual$9}
+   |Required: (boundary.Label[Result[Future[T^?]^?, E^?]]^{cap.rd}) ?=> Future[T^?]^?
    |
    |where:    ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make
    |          cap is the universal root capability
    |
    |Note that reference contextual$9.type
-   |cannot be included in outer capture set {fr, async}
+   |cannot be included in outer capture set ?
 70 |            fr.await.ok
    |
    | longer explanation available when compiling with `-explain`
 -- [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[Result[Future[T^?]^?, E^?]^?]^{cap.rd}) ?->{fr, async} Future[T^?]^{fr, lbl}
+   |Found:    (lbl: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, lbl}
    |Required: (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