From 68b711c5db392464b043c27f1b0460327babe013 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 5 May 2021 10:26:47 +0200
Subject: [PATCH 1/7] Maintain TyperState invariants after mergeConstraints

---
 .../dotty/tools/dotc/core/TyperState.scala    | 22 ++++++++++++++-----
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TyperState.scala b/compiler/src/dotty/tools/dotc/core/TyperState.scala
index 8b4b6a476d1b..4ddf1bbeedb1 100644
--- a/compiler/src/dotty/tools/dotc/core/TyperState.scala
+++ b/compiler/src/dotty/tools/dotc/core/TyperState.scala
@@ -120,12 +120,11 @@ class TyperState() {
     if constraint ne targetState.constraint then
       Stats.record("typerState.commit.new constraint")
       constr.println(i"committing $this to $targetState, fromConstr = $constraint, toConstr = ${targetState.constraint}")
-      if targetState.constraint eq previousConstraint then targetState.constraint = constraint
-      else targetState.mergeConstraintWith(this)
-    if !ownedVars.isEmpty then
-      for tvar <- ownedVars do
-        tvar.owningState = new WeakReference(targetState)
-      targetState.ownedVars ++= ownedVars
+      if targetState.constraint eq previousConstraint then
+        targetState.constraint = constraint
+        if !ownedVars.isEmpty then ownedVars.foreach(targetState.includeVar)
+      else
+        targetState.mergeConstraintWith(this)
     targetState.gc()
     reporter.flush()
     isCommitted = true
@@ -133,6 +132,17 @@ class TyperState() {
 
   def mergeConstraintWith(that: TyperState)(using Context): Unit =
     constraint = constraint & (that.constraint, otherHasErrors = that.reporter.errorsReported)
+    for tvar <- constraint.uninstVars do
+      if !isOwnedAnywhere(this, tvar) then ownedVars += tvar
+    for tl <- constraint.domainLambdas do
+      if constraint.isRemovable(tl) then constraint = constraint.remove(tl)
+
+  private def includeVar(tvar: TypeVar)(using Context): Unit =
+    tvar.owningState = new WeakReference(this)
+    ownedVars += tvar
+
+  private def isOwnedAnywhere(ts: TyperState, tvar: TypeVar): Boolean =
+    ts.ownedVars.contains(tvar) || ts.previous != null && isOwnedAnywhere(ts.previous, tvar)
 
   /** Make type variable instances permanent by assigning to `inst` field if
    *  type variable instantiation cannot be retracted anymore. Then, remove

From ce60b142b5cf3c47db76fde172298bb15bcb7e93 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 5 May 2021 14:21:42 +0200
Subject: [PATCH 2/7] Handle weak reference that can be reset by the GC

owningState weak reference can be reset to null. This was observed
when compiling scalatest.
---
 compiler/src/dotty/tools/dotc/core/Types.scala | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index e9f5f48eb24b..8b6d750901a9 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4396,13 +4396,13 @@ object Types {
     private var myInst: Type = NoType
 
     private[core] def inst: Type = myInst
-    private[core] def inst_=(tp: Type): Unit = {
+    private[core] def inst_=(tp: Type): Unit =
       myInst = tp
-      if (tp.exists && (owningState ne null)) {
-        owningState.get.ownedVars -= this
-        owningState = null // no longer needed; null out to avoid a memory leak
-      }
-    }
+      if tp.exists && owningState != null then
+        val owningState1 = owningState.get
+        if owningState1 != null then
+          owningState1.ownedVars -= this
+          owningState = null // no longer needed; null out to avoid a memory leak
 
     /** The state owning the variable. This is at first `creatorState`, but it can
      *  be changed to an enclosing state on a commit.

From 73abb32ea8afa6928a8147ca1af65b9eb3cafd7a Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 5 May 2021 16:34:00 +0200
Subject: [PATCH 3/7] Fix renaming of constraints

When we replace a type lambda in a constraint by another,
the type variables associated with the old lambda changed their origin
to point to the new lambda. But that means that the same type
variables in predecessor typestates do not point to their associated
lambda anymore. To fix this, we have to do the same renaming
of type lambdas also in predecessor typestates.
---
 .../dotty/tools/dotc/core/Constraint.scala    |  9 ++++--
 .../tools/dotc/core/OrderingConstraint.scala  | 32 +++----------------
 .../dotty/tools/dotc/core/TyperState.scala    | 21 ++++++++++++
 3 files changed, 32 insertions(+), 30 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Constraint.scala b/compiler/src/dotty/tools/dotc/core/Constraint.scala
index 81c108bc1241..3349e52a35d0 100644
--- a/compiler/src/dotty/tools/dotc/core/Constraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/Constraint.scala
@@ -118,8 +118,11 @@ abstract class Constraint extends Showable {
   /** A new constraint with all entries coming from `tl` removed. */
   def remove(tl: TypeLambda)(using Context): This
 
-  /** A new constraint with entry `tl` renamed to a fresh type lambda */
-  def rename(tl: TypeLambda)(using Context): This
+  /** A new constraint with entry `from` replaced with `to`
+   *  Rerences to `from` from within other constraint bounds are updated to `to`.
+   *  Type variables are left alone.
+   */
+  def subst(from: TypeLambda, to: TypeLambda)(using Context): This
 
   /** Gives for each instantiated type var that does not yet have its `inst` field
    *  set, the instance value stored in the constraint. Storing instances in constraints
@@ -150,6 +153,8 @@ abstract class Constraint extends Showable {
   def uninstVars: collection.Seq[TypeVar]
 
   /** The weakest constraint that subsumes both this constraint and `other`.
+   *  The constraints should be _compatible_, meaning that a type lambda
+   *  occurring in both constraints is associated with the same typevars in each.
    *
    *  @param otherHasErrors    If true, handle incompatible constraints by
    *                           returning an approximate constraint, instead of
diff --git a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
index 9b1fbecc517d..343fa2dfcf23 100644
--- a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
@@ -485,24 +485,7 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
             throw new AssertionError(i"cannot merge $this with $other, mergeEntries($e1, $e2) failed")
       }
 
-    /** Ensure that constraint `c` does not associate different TypeVars for the
-     *  same type lambda than this constraint. Do this by renaming type lambdas
-     *  in `c` where necessary.
-     */
-    def ensureNotConflicting(c: OrderingConstraint): OrderingConstraint = {
-      def hasConflictingTypeVarsFor(tl: TypeLambda) =
-        this.typeVarOfParam(tl.paramRefs(0)) ne c.typeVarOfParam(tl.paramRefs(0))
-          // Note: Since TypeVars are allocated in bulk for each type lambda, we only
-          // have to check the first one to find out if some of them are different.
-      val conflicting = c.domainLambdas.find(tl =>
-        this.contains(tl) && hasConflictingTypeVarsFor(tl))
-      conflicting match {
-        case Some(tl) => ensureNotConflicting(c.rename(tl))
-        case None => c
-      }
-    }
-
-    val that = ensureNotConflicting(other.asInstanceOf[OrderingConstraint])
+    val that = other.asInstanceOf[OrderingConstraint]
 
     new OrderingConstraint(
         merge(this.boundsMap, that.boundsMap, mergeEntries),
@@ -510,24 +493,17 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
         merge(this.upperMap, that.upperMap, mergeParams))
   }.showing(i"constraint merge $this with $other = $result", constr)
 
-  def rename(tl: TypeLambda)(using Context): OrderingConstraint = {
-    assert(contains(tl))
-    val tl1 = ensureFresh(tl)
-    def swapKey[T](m: ArrayValuedMap[T]) = m.remove(tl).updated(tl1, m(tl))
+  def subst(from: TypeLambda, to: TypeLambda)(using Context): OrderingConstraint =
+    def swapKey[T](m: ArrayValuedMap[T]) = m.remove(from).updated(to, m(from))
     var current = newConstraint(swapKey(boundsMap), swapKey(lowerMap), swapKey(upperMap))
-    def subst[T <: Type](x: T): T = x.subst(tl, tl1).asInstanceOf[T]
+    def subst[T <: Type](x: T): T = x.subst(from, to).asInstanceOf[T]
     current.foreachParam {(p, i) =>
       current = boundsLens.map(this, current, p, i, subst)
       current = lowerLens.map(this, current, p, i, _.map(subst))
       current = upperLens.map(this, current, p, i, _.map(subst))
     }
-    current.foreachTypeVar { tvar =>
-      val TypeParamRef(binder, n) = tvar.origin
-      if (binder eq tl) tvar.setOrigin(tl1.paramRefs(n))
-    }
     constr.println(i"renamed $this to $current")
     current.checkNonCyclic()
-  }
 
   def instType(tvar: TypeVar): Type = entry(tvar.origin) match
     case _: TypeBounds => NoType
diff --git a/compiler/src/dotty/tools/dotc/core/TyperState.scala b/compiler/src/dotty/tools/dotc/core/TyperState.scala
index 4ddf1bbeedb1..ce4261f5b875 100644
--- a/compiler/src/dotty/tools/dotc/core/TyperState.scala
+++ b/compiler/src/dotty/tools/dotc/core/TyperState.scala
@@ -130,7 +130,28 @@ class TyperState() {
     isCommitted = true
   }
 
+  /** Ensure that this constraint does not associate different TypeVars for the
+   *  same type lambda than the `other` constraint. Do this by renaming type lambdas
+   *  in this constraint and its predecessors where necessary.
+   */
+  def ensureNotConflicting(other: Constraint)(using Context): Unit =
+    def hasConflictingTypeVarsFor(tl: TypeLambda) =
+      constraint.typeVarOfParam(tl.paramRefs(0)) ne other.typeVarOfParam(tl.paramRefs(0))
+        // Note: Since TypeVars are allocated in bulk for each type lambda, we only
+        // have to check the first one to find out if some of them are different.
+    val conflicting = constraint.domainLambdas.find(tl =>
+      other.contains(tl) && hasConflictingTypeVarsFor(tl))
+    for tl <- conflicting do
+      val tl1 = constraint.ensureFresh(tl)
+      for case (tvar: TypeVar, pref1) <- tl.paramRefs.map(constraint.typeVarOfParam).lazyZip(tl1.paramRefs) do
+        tvar.setOrigin(pref1)
+      var ts = this
+      while ts.constraint.domainLambdas.contains(tl) do
+        ts.constraint = ts.constraint.subst(tl, tl1)
+        ts = ts.previous
+
   def mergeConstraintWith(that: TyperState)(using Context): Unit =
+    that.ensureNotConflicting(constraint)
     constraint = constraint & (that.constraint, otherHasErrors = that.reporter.errorsReported)
     for tvar <- constraint.uninstVars do
       if !isOwnedAnywhere(this, tvar) then ownedVars += tvar

From 4c9198824ac29be624bfa11b96e6dcaf4182ad14 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 5 May 2021 17:05:40 +0200
Subject: [PATCH 4/7] Add optional check that type variables in constraints are
 consistent

I verified that with the previous commit all compilation tests except two neg
tests pass this check.
---
 compiler/src/dotty/tools/dotc/config/Config.scala    |  6 ++++++
 compiler/src/dotty/tools/dotc/core/Constraint.scala  |  5 +++++
 .../dotty/tools/dotc/core/OrderingConstraint.scala   |  7 +++++++
 compiler/src/dotty/tools/dotc/core/TyperState.scala  | 12 +++++++-----
 compiler/src/dotty/tools/dotc/core/Types.scala       |  4 ++--
 5 files changed, 27 insertions(+), 7 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala
index c009372f19d3..32470a026084 100644
--- a/compiler/src/dotty/tools/dotc/config/Config.scala
+++ b/compiler/src/dotty/tools/dotc/config/Config.scala
@@ -34,6 +34,12 @@ object Config {
    */
   inline val checkConstraintsPropagated = false
 
+  /** If a constraint is over a type lambda `tl` and `tvar` is one of
+   *  the type variables associated with `tl` in the constraint, check
+   *  that the origin of `tvar` is a parameter of `tl`.
+   */
+  inline val checkConsistentVars = false
+
   /** Check that constraints of globally committable typer states are closed.
    *  NOTE: When enabled, the check can cause CyclicReference errors because
    *  it traverses all elements of a type. Such failures were observed when
diff --git a/compiler/src/dotty/tools/dotc/core/Constraint.scala b/compiler/src/dotty/tools/dotc/core/Constraint.scala
index 3349e52a35d0..097397375c87 100644
--- a/compiler/src/dotty/tools/dotc/core/Constraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/Constraint.scala
@@ -174,6 +174,11 @@ abstract class Constraint extends Showable {
   /** Check that constraint only refers to TypeParamRefs bound by itself */
   def checkClosed()(using Context): Unit
 
+  /** Check that every typevar om this constraint has as origin a type parameter
+   *  of athe type lambda that is associated with the typevar itself.
+   */
+  def checkConsistentVars()(using Context): Unit
+
   /** A string describing the constraint's contents without a header or trailer */
   def contentsToString(using Context): String
 }
diff --git a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
index 343fa2dfcf23..0faadac35e36 100644
--- a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
@@ -523,6 +523,13 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
     }
     else tl
 
+  def checkConsistentVars()(using Context): Unit =
+    for param <- domainParams do
+      typeVarOfParam(param) match
+        case tvar: TypeVar =>
+          assert(tvar.origin == param, i"mismatch $tvar, $param")
+        case _ =>
+
 // ---------- Exploration --------------------------------------------------------
 
   def domainLambdas: List[TypeLambda] = boundsMap.keys
diff --git a/compiler/src/dotty/tools/dotc/core/TyperState.scala b/compiler/src/dotty/tools/dotc/core/TyperState.scala
index ce4261f5b875..a4d92ac53e4a 100644
--- a/compiler/src/dotty/tools/dotc/core/TyperState.scala
+++ b/compiler/src/dotty/tools/dotc/core/TyperState.scala
@@ -44,6 +44,8 @@ class TyperState() {
   def constraint_=(c: Constraint)(using Context): Unit = {
     if (Config.debugCheckConstraintsClosed && isGlobalCommittable) c.checkClosed()
     myConstraint = c
+    if Config.checkConsistentVars && !ctx.reporter.errorsReported then
+      c.checkConsistentVars()
   }
 
   private var previousConstraint: Constraint = _
@@ -177,11 +179,11 @@ class TyperState() {
         if !tvar.inst.exists then
           val inst = constraint.instType(tvar)
           if inst.exists then
-            tvar.inst = inst
-            val lam = tvar.origin.binder
-            if constraint.isRemovable(lam) then toCollect += lam
-      for poly <- toCollect do
-        constraint = constraint.remove(poly)
+            tvar.setInst(inst)
+            val tl = tvar.origin.binder
+            if constraint.isRemovable(tl) then toCollect += tl
+      for tl <- toCollect do
+        constraint = constraint.remove(tl)
 
   override def toString: String = {
     def ids(state: TyperState): List[String] =
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 8b6d750901a9..e42988483333 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4396,7 +4396,7 @@ object Types {
     private var myInst: Type = NoType
 
     private[core] def inst: Type = myInst
-    private[core] def inst_=(tp: Type): Unit =
+    private[core] def setInst(tp: Type): Unit =
       myInst = tp
       if tp.exists && owningState != null then
         val owningState1 = owningState.get
@@ -4454,7 +4454,7 @@ object Types {
       assert(tp ne this, s"self instantiation of ${tp.show}, constraint = ${ctx.typerState.constraint.show}")
       typr.println(s"instantiating ${this.show} with ${tp.show}")
       if ((ctx.typerState eq owningState.get) && !TypeComparer.subtypeCheckInProgress)
-        inst = tp
+        setInst(tp)
       ctx.typerState.constraint = ctx.typerState.constraint.replace(origin, tp)
       tp
     }

From d5eb457226090be4e936070c6112af6c706f1e26 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Thu, 6 May 2021 09:55:22 +0200
Subject: [PATCH 5/7] Fix hole when resetting a typerstate

Besides the constraint, we also need to reset any instantiated type variables.
This is necessary for correctness and also to avoid uncollected garbage in constraints
when an entry is never dropped since the associated type variables are no longer
owned by the constraint.
---
 compiler/src/dotty/tools/dotc/core/TyperState.scala | 11 +++++++++++
 compiler/src/dotty/tools/dotc/core/Types.scala      |  4 ++++
 compiler/src/dotty/tools/dotc/typer/Typer.scala     |  7 ++++---
 tests/neg/i9568.check                               |  4 ++--
 4 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TyperState.scala b/compiler/src/dotty/tools/dotc/core/TyperState.scala
index a4d92ac53e4a..c3997552f2d8 100644
--- a/compiler/src/dotty/tools/dotc/core/TyperState.scala
+++ b/compiler/src/dotty/tools/dotc/core/TyperState.scala
@@ -22,6 +22,17 @@ object TyperState {
       .init(null, OrderingConstraint.empty)
       .setReporter(new ConsoleReporter())
       .setCommittable(true)
+
+  opaque type Snapshot = (Constraint, TypeVars)
+
+  extension (ts: TyperState)
+    def snapshot(): Snapshot = (ts.constraint, ts.ownedVars)
+
+    def resetTo(state: Snapshot)(using Context): Unit =
+      val (c, tvs) = state
+      for tv <- tvs do if tv.isInstantiated then tv.resetInst(ts)
+      ts.ownedVars = tvs
+      ts.constraint = c
 }
 
 class TyperState() {
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index e42988483333..6f211889116f 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4404,6 +4404,10 @@ object Types {
           owningState1.ownedVars -= this
           owningState = null // no longer needed; null out to avoid a memory leak
 
+    private[core] def resetInst(ts: TyperState): Unit =
+      myInst = NoType
+      owningState = new WeakReference(ts)
+
     /** The state owning the variable. This is at first `creatorState`, but it can
      *  be changed to an enclosing state on a commit.
      */
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 214872788942..9df0c8409fad 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -3247,7 +3247,7 @@ class Typer extends Namer
         replaceSingletons(tp)
       }
       wtp.paramInfos.foreach(instantiate)
-      val constr = ctx.typerState.constraint
+      val saved = ctx.typerState.snapshot()
 
       def dummyArg(tp: Type) = untpd.Ident(nme.???).withTypeUnchecked(tp)
 
@@ -3347,8 +3347,9 @@ class Typer extends Namer
         if (propFail.exists) {
           // If there are several arguments, some arguments might already
           // have influenced the context, binding variables, but later ones
-          // might fail. In that case the constraint needs to be reset.
-          ctx.typerState.constraint = constr
+          // might fail. In that case the constraint and instantiated variables
+          // need to be reset.
+          ctx.typerState.resetTo(saved)
 
           // If method has default params, fall back to regular application
           // where all inferred implicits are passed as named args.
diff --git a/tests/neg/i9568.check b/tests/neg/i9568.check
index 11aab7e9ec56..1173d483ed02 100644
--- a/tests/neg/i9568.check
+++ b/tests/neg/i9568.check
@@ -7,6 +7,6 @@
    |          .
    |          I found:
    |
-   |              Test.blaMonad[Nothing, S](Test.blaMonad[F, S])
+   |              Test.blaMonad[F, S](Test.blaMonad[F, S])
    |
-   |          But method blaMonad in object Test does not match type => Monad[Nothing].
+   |          But method blaMonad in object Test does not match type => Monad[F].

From 3efcebed7f362e51a12f82821144cfe029e2e60b Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Thu, 6 May 2021 12:20:13 +0200
Subject: [PATCH 6/7] Refine snapshot logic to take spurious nulls in weak
 references into account

---
 .../dotty/tools/dotc/core/TyperState.scala    | 21 +++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TyperState.scala b/compiler/src/dotty/tools/dotc/core/TyperState.scala
index c3997552f2d8..170d0dc92d99 100644
--- a/compiler/src/dotty/tools/dotc/core/TyperState.scala
+++ b/compiler/src/dotty/tools/dotc/core/TyperState.scala
@@ -23,14 +23,19 @@ object TyperState {
       .setReporter(new ConsoleReporter())
       .setCommittable(true)
 
-  opaque type Snapshot = (Constraint, TypeVars)
+  opaque type Snapshot = (Constraint, TypeVars, TypeVars)
 
   extension (ts: TyperState)
-    def snapshot(): Snapshot = (ts.constraint, ts.ownedVars)
+    def snapshot()(using Context): Snapshot =
+      var previouslyInstantiated: TypeVars = SimpleIdentitySet.empty
+      for tv <- ts.ownedVars do if tv.inst.exists then previouslyInstantiated += tv
+      (ts.constraint, ts.ownedVars, previouslyInstantiated)
 
     def resetTo(state: Snapshot)(using Context): Unit =
-      val (c, tvs) = state
-      for tv <- tvs do if tv.isInstantiated then tv.resetInst(ts)
+      val (c, tvs, previouslyInstantiated) = state
+      for tv <- tvs do
+        if tv.inst.exists && !previouslyInstantiated.contains(tv) then
+          tv.resetInst(ts)
       ts.ownedVars = tvs
       ts.constraint = c
 }
@@ -74,7 +79,11 @@ class TyperState() {
 
   private var isCommitted: Boolean = _
 
-  /** The set of uninstantiated type variables which have this state as their owning state */
+  /** The set of uninstantiated type variables which have this state as their owning state
+   *  NOTE: It could be that a variable in `ownedVars` is already instantiated. This is because
+   *  the link between ownedVars and variable instantiation in TypeVar#setInst is made up
+   *  from a weak reference and weak references can have spurious nulls.
+   */
   private var myOwnedVars: TypeVars = _
   def ownedVars: TypeVars = myOwnedVars
   def ownedVars_=(vs: TypeVars): Unit = myOwnedVars = vs
@@ -187,7 +196,7 @@ class TyperState() {
       Stats.record("typerState.gc")
       val toCollect = new mutable.ListBuffer[TypeLambda]
       for tvar <- ownedVars do
-        if !tvar.inst.exists then
+        if !tvar.inst.exists then // See comment of `ownedVars` for why this test is necessary
           val inst = constraint.instType(tvar)
           if inst.exists then
             tvar.setInst(inst)

From 8dc0cb5565f589e2bd90c9ab48a6dceae6c69031 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Thu, 6 May 2021 13:49:41 +0200
Subject: [PATCH 7/7] Reset typerState when reducing a match type

It is not enough to reset the constraint only, since type variables might have
gotten instantiated during matchtype reduction.

With that change we now test in -Ycheck that constraints are empty after each phase.
---
 compiler/src/dotty/tools/dotc/Run.scala                   | 1 +
 compiler/src/dotty/tools/dotc/core/TypeComparer.scala     | 8 ++------
 compiler/src/dotty/tools/dotc/core/Types.scala            | 8 +++++++-
 compiler/src/dotty/tools/dotc/transform/TreeChecker.scala | 2 ++
 4 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/Run.scala b/compiler/src/dotty/tools/dotc/Run.scala
index 6b51908c37d7..0afea7988958 100644
--- a/compiler/src/dotty/tools/dotc/Run.scala
+++ b/compiler/src/dotty/tools/dotc/Run.scala
@@ -212,6 +212,7 @@ class Run(comp: Compiler, ictx: Context) extends ImplicitRunInfo with Constraint
             Stats.record(s"total trees at end of $phase", ast.Trees.ntrees)
             for (unit <- units)
               Stats.record(s"retained typed trees at end of $phase", unit.tpdTree.treeSize)
+            ctx.typerState.gc()
           }
 
       profiler.finished()
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 36967e049b86..08f4feadeb04 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -2876,12 +2876,8 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
       // obviously sound, but quite restrictive. With the current formulation,
       // we need to be careful that `provablyEmpty` covers all the conditions
       // used to conclude disjointness in `provablyDisjoint`.
-      if (provablyEmpty(scrut))
-        NoType
-      else
-        val savedConstraint = constraint
-        try recur(cases)
-        finally constraint = savedConstraint // caseLambda additions are dropped
+      if (provablyEmpty(scrut)) NoType
+      else recur(cases)
     }
   }
 }
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 6f211889116f..04ded20d7c90 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4597,10 +4597,16 @@ object Types {
         myReduced =
           trace(i"reduce match type $this $hashCode", matchTypes, show = true) {
             def matchCases(cmp: TrackingTypeComparer): Type =
+              val saved = ctx.typerState.snapshot()
               try cmp.matchCases(scrutinee.normalized, cases)
               catch case ex: Throwable =>
                 handleRecursive("reduce type ", i"$scrutinee match ...", ex)
-              finally updateReductionContext(cmp.footprint)
+              finally
+                updateReductionContext(cmp.footprint)
+                ctx.typerState.resetTo(saved)
+                  // this drops caseLambdas in constraint and undoes any typevar
+                  // instantiations during matchtype reduction
+
             TypeComparer.tracked(matchCases)
           }
       myReduced
diff --git a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
index e3a0489cf0fa..831d8f395025 100644
--- a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
@@ -128,6 +128,8 @@ class TreeChecker extends Phase with SymTransformer {
     report.echo(s"checking ${ctx.compilationUnit} after phase ${fusedPhase}")(using ctx)
 
     inContext(ctx) {
+      assert(ctx.typerState.constraint.domainLambdas.isEmpty,
+        i"non-empty constraint at end of $fusedPhase: ${ctx.typerState.constraint}, ownedVars = ${ctx.typerState.ownedVars.toList}%, %")
       assertSelectWrapsNew(ctx.compilationUnit.tpdTree)
     }