From 824496b805f31a9c8c2b20a8d375429b8f02ab75 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 16 Jul 2022 18:50:13 +0200
Subject: [PATCH 1/8] Avoid instantiating variables to types with deeper
 nesting levels

---
 .../tools/dotc/core/ConstraintHandling.scala  | 107 +++++++++++++++---
 .../src/dotty/tools/dotc/core/Contexts.scala  |   2 +-
 .../tools/dotc/core/GadtConstraint.scala      |   8 +-
 .../dotty/tools/dotc/core/TypeComparer.scala  |  10 +-
 .../src/dotty/tools/dotc/core/Types.scala     |   4 +-
 .../tools/dotc/inlines/InlineReducer.scala    |   2 +-
 .../tools/dotc/transform/TypeTestsCasts.scala |   2 +-
 .../test/dotc/pos-test-pickling.blacklist     |   3 -
 tests/{pending/run => neg}/i8861.scala        |   2 +-
 tests/{pos => neg}/i8900-promote.scala        |   5 +-
 tests/{pending => }/neg/i8900.scala           |   0
 tests/pos/i15595.scala                        |  14 +++
 12 files changed, 125 insertions(+), 34 deletions(-)
 rename tests/{pending/run => neg}/i8861.scala (96%)
 rename tests/{pos => neg}/i8900-promote.scala (84%)
 rename tests/{pending => }/neg/i8900.scala (100%)
 create mode 100644 tests/pos/i15595.scala

diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 7b96062dda95..4a9e4bda22fc 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -12,6 +12,7 @@ import config.Printers.typr
 import typer.ProtoTypes.{newTypeVar, representedParamRef}
 import UnificationDirection.*
 import NameKinds.AvoidNameKind
+import util.SimpleIdentitySet
 
 /** Methods for adding constraints and solving them.
  *
@@ -74,8 +75,41 @@ trait ConstraintHandling {
   protected def necessaryConstraintsOnly(using Context): Boolean =
     ctx.mode.is(Mode.GadtConstraintInference) || myNecessaryConstraintsOnly
 
+  /** If `trustBounds = false` we perform comparisons in a pessimistic way as follows:
+   *  Given an abstract type `A >: L <: H`, a subtype comparison of any type
+   *  with `A` will compare against both `L` and `H`. E.g.
+   *
+   *     T <:< A   if T <:< L and T <:< H
+   *     A <:< T   if L <:< T and H <:< T
+   *
+   *  This restricted form makes sure we don't "forget"  types when forming
+   *  unions and intersections with abstract types that have bad bounds. E.g.
+   *  the following example from neg/i8900.scala that @smarter came up with:
+   *  We have a type variable X with constraints
+   *
+   *     X >: 1, X >: x.M
+   *
+   *  where `x` is a locally nested variable and `x.M` has bad bounds
+   *
+   *     x.M >: Int | String <: Int & String
+   *
+   *  If we trust bounds, then the lower bound of `X` is `x.M` since `x.M >: 1`.
+   *  Then even if we correct levels on instantiation to eliminate the local `x`,
+   *  it is alreay too late, we'd get `Int & String` as instance, which does not
+   *  satisfy the original constraint `X >: 1`.
+   *
+   *  But if `trustBounds` is false, we do not conclude the `x.M >: 1` since
+   *  we compare both bounds and the upper bound `Int & String` is not a supertype
+   *  of `1`. So the lower bound is `1 | x.M` and when we level-avoid that we
+   *  get `1 | Int & String`, which simplifies to `Int`.
+   */
   protected var trustBounds = true
 
+  inline def withUntrustedBounds(op: => Type): Type =
+    val saved = trustBounds
+    trustBounds = false
+    try op finally trustBounds = saved
+
   def checkReset() =
     assert(addConstraintInvocations == 0)
     assert(frozenConstraint == false)
@@ -262,16 +296,14 @@ trait ConstraintHandling {
         // If `isUpper` is true, ensure that `param <: `bound`, otherwise ensure
         // that `param >: bound`.
         val narrowedBounds =
-          val savedHomogenizeArgs = homogenizeArgs
-          val savedTrustBounds = trustBounds
+          val saved = homogenizeArgs
           homogenizeArgs = Config.alignArgsInAnd
           try
-            trustBounds = false
-            if isUpper then oldBounds.derivedTypeBounds(lo, hi & bound)
-            else oldBounds.derivedTypeBounds(lo | bound, hi)
+            withUntrustedBounds(
+              if isUpper then oldBounds.derivedTypeBounds(lo, hi & bound)
+              else oldBounds.derivedTypeBounds(lo | bound, hi))
           finally
-            homogenizeArgs = savedHomogenizeArgs
-            trustBounds = savedTrustBounds
+            homogenizeArgs = saved
         //println(i"narrow bounds for $param from $oldBounds to $narrowedBounds")
         val c1 = constraint.updateEntry(param, narrowedBounds)
         (c1 eq constraint)
@@ -431,6 +463,49 @@ trait ConstraintHandling {
       }
     }
 
+  private def fixLevels(tp: Type, fromBelow: Boolean, maxLevel: Int, param: TypeParamRef)(using Context) =
+
+    def needsFix(tp: NamedType) =
+      (tp.prefix eq NoPrefix) && tp.symbol.nestingLevel > maxLevel
+
+    class NeedsLeveling extends TypeAccumulator[Boolean]:
+      if !fromBelow then variance = -1
+      var nestedVarsLo, nestedVarsHi: SimpleIdentitySet[TypeVar] = SimpleIdentitySet.empty
+      def apply(need: Boolean, tp: Type) =
+        need || tp.match
+          case tp: NamedType =>
+            needsFix(tp)
+            || !stopBecauseStaticOrLocal(tp) && apply(need, tp.prefix)
+          case tp: TypeVar =>
+            val inst = tp.instanceOpt
+            if inst.exists then apply(need, inst)
+            else if tp.nestingLevel > maxLevel then
+              if variance > 0 then nestedVarsLo += tp
+              else if variance < 0 then nestedVarsHi += tp
+              else tp.nestingLevel = maxLevel
+              true
+            else false
+          case _ =>
+            foldOver(need, tp)
+
+    class LevelAvoidMap extends TypeOps.AvoidMap:
+      if !fromBelow then variance = -1
+      def toAvoid(tp: NamedType) = needsFix(tp)
+      //override def apply(tp: Type): Type = tp match
+      //  case tp: LazyRef => tp
+      //  case _ => super.apply(tp)
+
+    if ctx.isAfterTyper then tp
+    else
+      val needsLeveling = NeedsLeveling()
+      if needsLeveling(false, tp) then
+        typr.println(i"instance $tp for $param needs leveling to $maxLevel, nested = ${needsLeveling.nestedVarsLo.toList} | ${needsLeveling.nestedVarsHi.toList}")
+        needsLeveling.nestedVarsLo.foreach(_.instantiate(fromBelow = true))
+        needsLeveling.nestedVarsHi.foreach(_.instantiate(fromBelow = false))
+        LevelAvoidMap()(tp)
+      else tp
+  end fixLevels
+
   /** Solve constraint set for given type parameter `param`.
    *  If `fromBelow` is true the parameter is approximated by its lower bound,
    *  otherwise it is approximated by its upper bound, unless the upper bound
@@ -442,13 +517,17 @@ trait ConstraintHandling {
    *  @return the instantiating type
    *  @pre `param` is in the constraint's domain.
    */
-  final def approximation(param: TypeParamRef, fromBelow: Boolean)(using Context): Type =
+  final def approximation(param: TypeParamRef, fromBelow: Boolean, maxLevel: Int)(using Context): Type =
     constraint.entry(param) match
       case entry: TypeBounds =>
         val useLowerBound = fromBelow || param.occursIn(entry.hi)
-        val inst = if useLowerBound then fullLowerBound(param) else fullUpperBound(param)
-        typr.println(s"approx ${param.show}, from below = $fromBelow, inst = ${inst.show}")
-        inst
+        val rawInst = withUntrustedBounds(
+          if useLowerBound then fullLowerBound(param) else fullUpperBound(param))
+        val levelInst = fixLevels(rawInst, fromBelow, maxLevel, param)
+        if levelInst ne rawInst then
+          typr.println(i"level avoid for $maxLevel: $rawInst --> $levelInst")
+        typr.println(i"approx $param, from below = $fromBelow, inst = $levelInst")
+        levelInst
       case inst =>
         assert(inst.exists, i"param = $param\nconstraint = $constraint")
         inst
@@ -561,8 +640,8 @@ trait ConstraintHandling {
    *  a lower bound instantiation can be a singleton type only if the upper bound
    *  is also a singleton type.
    */
-  def instanceType(param: TypeParamRef, fromBelow: Boolean)(using Context): Type = {
-    val approx = approximation(param, fromBelow).simplified
+  def instanceType(param: TypeParamRef, fromBelow: Boolean, maxLevel: Int)(using Context): Type = {
+    val approx = approximation(param, fromBelow, maxLevel).simplified
     if fromBelow then
       val widened = widenInferred(approx, param)
       // Widening can add extra constraints, in particular the widened type might
@@ -572,7 +651,7 @@ trait ConstraintHandling {
       // (we do not check for non-toplevel occurences: those should never occur
       // since `addOneBound` disallows recursive lower bounds).
       if constraint.occursAtToplevel(param, widened) then
-        instanceType(param, fromBelow)
+        instanceType(param, fromBelow, maxLevel)
       else
         widened
     else
diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala
index 3dfafe6837d0..919598c41d6e 100644
--- a/compiler/src/dotty/tools/dotc/core/Contexts.scala
+++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala
@@ -165,7 +165,7 @@ object Contexts {
     protected def scope_=(scope: Scope): Unit = _scope = scope
     final def scope: Scope = _scope
 
-    /** The current type comparer */
+    /** The current typerstate */
     private var _typerState: TyperState = _
     protected def typerState_=(typerState: TyperState): Unit = _typerState = typerState
     final def typerState: TyperState = _typerState
diff --git a/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala b/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
index ae87dd662d56..a8b5eee4902d 100644
--- a/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
@@ -47,7 +47,7 @@ sealed abstract class GadtConstraint extends Showable {
   def isNarrowing: Boolean
 
   /** See [[ConstraintHandling.approximation]] */
-  def approximation(sym: Symbol, fromBelow: Boolean)(using Context): Type
+  def approximation(sym: Symbol, fromBelow: Boolean, maxLevel: Int = Int.MaxValue)(using Context): Type
 
   def symbols: List[Symbol]
 
@@ -205,9 +205,9 @@ final class ProperGadtConstraint private(
 
   def isNarrowing: Boolean = wasConstrained
 
-  override def approximation(sym: Symbol, fromBelow: Boolean)(using Context): Type = {
+  override def approximation(sym: Symbol, fromBelow: Boolean, maxLevel: Int)(using Context): Type = {
     val res =
-      approximation(tvarOrError(sym).origin, fromBelow = fromBelow) match
+      approximation(tvarOrError(sym).origin, fromBelow, maxLevel) match
         case tpr: TypeParamRef =>
           // Here we do externalization when the returned type is a TypeParamRef,
           //  b/c ConstraintHandling.approximation may return internal types when
@@ -317,7 +317,7 @@ final class ProperGadtConstraint private(
   override def addToConstraint(params: List[Symbol])(using Context): Boolean = unsupported("EmptyGadtConstraint.addToConstraint")
   override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(using Context): Boolean = unsupported("EmptyGadtConstraint.addBound")
 
-  override def approximation(sym: Symbol, fromBelow: Boolean)(using Context): Type = unsupported("EmptyGadtConstraint.approximation")
+  override def approximation(sym: Symbol, fromBelow: Boolean, maxLevel: Int)(using Context): Type = unsupported("EmptyGadtConstraint.approximation")
 
   override def symbols: List[Symbol] = Nil
 
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index b330a6178d68..80e9ff4f8865 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -2863,11 +2863,11 @@ object TypeComparer {
   def subtypeCheckInProgress(using Context): Boolean =
     comparing(_.subtypeCheckInProgress)
 
-  def instanceType(param: TypeParamRef, fromBelow: Boolean)(using Context): Type =
-    comparing(_.instanceType(param, fromBelow))
+  def instanceType(param: TypeParamRef, fromBelow: Boolean, maxLevel: Int = Int.MaxValue)(using Context): Type =
+    comparing(_.instanceType(param, fromBelow, maxLevel))
 
-  def approximation(param: TypeParamRef, fromBelow: Boolean)(using Context): Type =
-    comparing(_.approximation(param, fromBelow))
+  def approximation(param: TypeParamRef, fromBelow: Boolean, maxLevel: Int = Int.MaxValue)(using Context): Type =
+    comparing(_.approximation(param, fromBelow, maxLevel))
 
   def bounds(param: TypeParamRef)(using Context): TypeBounds =
     comparing(_.bounds(param))
@@ -2953,7 +2953,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
         case param @ TypeParamRef(b, n) if b eq caseLambda =>
           insts(n) =
             if canApprox then
-              approximation(param, fromBelow = variance >= 0).simplified
+              approximation(param, fromBelow = variance >= 0, Int.MaxValue).simplified
             else constraint.entry(param) match
               case entry: TypeBounds =>
                 val lo = fullLowerBound(param)
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index fd355abf982a..27cc18bad0d6 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4509,7 +4509,7 @@ object Types {
    *                        - On instantiation, replacing any param in the param bound
    *                          with a level greater than nestingLevel (see `fullLowerBound`).
    */
-  final class TypeVar private(initOrigin: TypeParamRef, creatorState: TyperState | Null, val nestingLevel: Int) extends CachedProxyType with ValueType {
+  final class TypeVar private(initOrigin: TypeParamRef, creatorState: TyperState | Null, var nestingLevel: Int) extends CachedProxyType with ValueType {
     private var currentOrigin = initOrigin
 
     def origin: TypeParamRef = currentOrigin
@@ -4574,7 +4574,7 @@ object Types {
      *  is also a singleton type.
      */
     def instantiate(fromBelow: Boolean)(using Context): Type =
-      val tp = TypeComparer.instanceType(origin, fromBelow)
+      val tp = TypeComparer.instanceType(origin, fromBelow, nestingLevel)
       if myInst.exists then // The line above might have triggered instantiation of the current type variable
         myInst
       else
diff --git a/compiler/src/dotty/tools/dotc/inlines/InlineReducer.scala b/compiler/src/dotty/tools/dotc/inlines/InlineReducer.scala
index b5e2e7d475ad..717e7f42dabe 100644
--- a/compiler/src/dotty/tools/dotc/inlines/InlineReducer.scala
+++ b/compiler/src/dotty/tools/dotc/inlines/InlineReducer.scala
@@ -302,7 +302,7 @@ class InlineReducer(inliner: Inliner)(using Context):
 
       def addTypeBindings(typeBinds: TypeBindsMap)(using Context): Unit =
         typeBinds.foreachBinding { case (sym, shouldBeMinimized) =>
-          newTypeBinding(sym, ctx.gadt.approximation(sym, fromBelow = shouldBeMinimized))
+          newTypeBinding(sym, ctx.gadt.approximation(sym, fromBelow = shouldBeMinimized, Int.MaxValue))
         }
 
       def registerAsGadtSyms(typeBinds: TypeBindsMap)(using Context): Unit =
diff --git a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
index 88f06122310e..ca977a6799f8 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
@@ -376,7 +376,7 @@ object TypeTestsCasts {
   private[transform] def foundClasses(tp: Type)(using Context): List[Symbol] =
     def go(tp: Type, acc: List[Type])(using Context): List[Type] = tp.dealias match
       case  OrType(tp1, tp2) => go(tp2, go(tp1, acc))
-      case AndType(tp1, tp2) => (for t1 <- go(tp1, Nil); t2 <- go(tp2, Nil); yield AndType(t1, t2)) ::: acc
+      case AndType(tp1, tp2) => (for t1 <- go(tp1, Nil); t2 <- go(tp2, Nil) yield AndType(t1, t2)) ::: acc
       case _                 => tp :: acc
     go(tp, Nil).map(effectiveClass)
 }
diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist
index 8adbb38df743..71292f4590b1 100644
--- a/compiler/test/dotc/pos-test-pickling.blacklist
+++ b/compiler/test/dotc/pos-test-pickling.blacklist
@@ -85,6 +85,3 @@ i4176-gadt.scala
 i13974a.scala
 
 java-inherited-type1
-
-# avoidance bug
-i15174.scala
\ No newline at end of file
diff --git a/tests/pending/run/i8861.scala b/tests/neg/i8861.scala
similarity index 96%
rename from tests/pending/run/i8861.scala
rename to tests/neg/i8861.scala
index e1e802a5c72b..ca337cd17095 100644
--- a/tests/pending/run/i8861.scala
+++ b/tests/neg/i8861.scala
@@ -22,7 +22,7 @@ object Test {
   // now infers `c.visit[(Int & M | String & M)]`
   def minimalFail[M](c: Container { type A = M }): M = c.visit(
     int = vi => vi.i : vi.A,
-    str = vs => vs.t : vs.A
+    str = vs => vs.t : vs.A // error
   )
 
   def main(args: Array[String]): Unit = {
diff --git a/tests/pos/i8900-promote.scala b/tests/neg/i8900-promote.scala
similarity index 84%
rename from tests/pos/i8900-promote.scala
rename to tests/neg/i8900-promote.scala
index 7d3a2ff96bed..fac6f021edae 100644
--- a/tests/pos/i8900-promote.scala
+++ b/tests/neg/i8900-promote.scala
@@ -12,7 +12,8 @@ object Test {
   def inv(cond: Boolean) = // used to leak: Inv[x.type]
     if (cond)
       val x: Int = 1
-      new Inv(x)
+      new Inv(x) // error
     else
-      Inv.empty
+      Inv.empty // error
+
 }
diff --git a/tests/pending/neg/i8900.scala b/tests/neg/i8900.scala
similarity index 100%
rename from tests/pending/neg/i8900.scala
rename to tests/neg/i8900.scala
diff --git a/tests/pos/i15595.scala b/tests/pos/i15595.scala
new file mode 100644
index 000000000000..b5d6cf402ed3
--- /dev/null
+++ b/tests/pos/i15595.scala
@@ -0,0 +1,14 @@
+trait MatchResult[+T]
+
+@main def Test() = {
+  def convert[T <: Seq[_], U <: MatchResult[_]](fn: T => U)(implicit x: Seq[_] = Seq.empty): U = ???
+  def resultOf[T](v: T): MatchResult[T] = ???
+
+  convert { _ =>
+    type R = String
+    resultOf[R](???)
+    // this would not lead to crash:
+    // val x = resultOf[R](???)
+    // x
+  }
+}
\ No newline at end of file

From 01b972af9d177fd2624c5ee07b4c0a43cff307aa Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 25 Jul 2022 17:02:46 +0200
Subject: [PATCH 2/8] Add comments

---
 .../tools/dotc/core/ConstraintHandling.scala  | 33 +++++++++++++++++--
 .../src/dotty/tools/dotc/core/Types.scala     | 10 ++----
 .../tools/dotc/inlines/InlineReducer.scala    |  3 +-
 .../src/dotty/tools/dotc/typer/Namer.scala    |  4 +++
 tests/neg/i8861.scala                         |  1 +
 tests/neg/i8900-promote.scala                 |  1 +
 tests/pos/java-futures.scala                  | 26 +++++++++++++++
 tests/pos/scalaz-redux.scala                  | 20 +++++++++++
 8 files changed, 87 insertions(+), 11 deletions(-)
 create mode 100644 tests/pos/java-futures.scala
 create mode 100644 tests/pos/scalaz-redux.scala

diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 4a9e4bda22fc..d91d4f8fda8d 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -463,14 +463,30 @@ trait ConstraintHandling {
       }
     }
 
+  /** Fix instance type `tp` by avoidance  so that it does not contain references
+   *  to types at level > `maxLevel`.
+   *  @param tp         the type to be fixed
+   *  @param fromBelow  whether type was obtained from lower bound
+   *  @param maxLevel   the maximum level of references allowed
+   *  @param param      the parameter that was instantiated
+   */
   private def fixLevels(tp: Type, fromBelow: Boolean, maxLevel: Int, param: TypeParamRef)(using Context) =
 
     def needsFix(tp: NamedType) =
       (tp.prefix eq NoPrefix) && tp.symbol.nestingLevel > maxLevel
 
+    /** An accumulator that determines whether levels need to be fixed
+     *  and computes on the side sets of nested type variables that need
+     *  to be instantiated.
+     */
     class NeedsLeveling extends TypeAccumulator[Boolean]:
       if !fromBelow then variance = -1
+
+      /** Nested type variables that should be instiated to theor lower (respoctively
+       *  upper) bounds.
+       */
       var nestedVarsLo, nestedVarsHi: SimpleIdentitySet[TypeVar] = SimpleIdentitySet.empty
+
       def apply(need: Boolean, tp: Type) =
         need || tp.match
           case tp: NamedType =>
@@ -483,17 +499,24 @@ trait ConstraintHandling {
               if variance > 0 then nestedVarsLo += tp
               else if variance < 0 then nestedVarsHi += tp
               else tp.nestingLevel = maxLevel
+                // For invariant type variables, we use a different strategy.
+                // Rather than instantiating to a bound and then propagating in an
+                // AvoidMap, change the nesting level of an invariant type
+                // variable to `maxLevel`. This means that the type variable will be
+                // instantiated later to a less nested type. If there are other references
+                // to the same type variable that do not come from the type undergoing
+                // `fixLevels`, this could lead to coarser types. But it has the potential
+                // to give a better approximation for the current type, since it avoids forming
+                // a Range in invariant position, which can lead to very coarse types further out.
               true
             else false
           case _ =>
             foldOver(need, tp)
+    end NeedsLeveling
 
     class LevelAvoidMap extends TypeOps.AvoidMap:
       if !fromBelow then variance = -1
       def toAvoid(tp: NamedType) = needsFix(tp)
-      //override def apply(tp: Type): Type = tp match
-      //  case tp: LazyRef => tp
-      //  case _ => super.apply(tp)
 
     if ctx.isAfterTyper then tp
     else
@@ -512,6 +535,8 @@ trait ConstraintHandling {
    *  contains a reference to the parameter itself (such occurrences can arise
    *  for F-bounded types, `addOneBound` ensures that they never occur in the
    *  lower bound).
+   *  The solved type is not allowed to contain references to types nested deeper
+   *  than `maxLevel`.
    *  Wildcard types in bounds are approximated by their upper or lower bounds.
    *  The constraint is left unchanged.
    *  @return the instantiating type
@@ -639,6 +664,8 @@ trait ConstraintHandling {
    *  lower bounds; otherwise it is the glb of its upper bounds. However,
    *  a lower bound instantiation can be a singleton type only if the upper bound
    *  is also a singleton type.
+   *  The instance type is not allowed to contain references to types nested deeper
+   *  than `maxLevel`.
    */
   def instanceType(param: TypeParamRef, fromBelow: Boolean, maxLevel: Int)(using Context): Type = {
     val approx = approximation(param, fromBelow, maxLevel).simplified
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 27cc18bad0d6..3d77ada0c90b 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4501,13 +4501,9 @@ object Types {
    *  @param  creatorState  The typer state in which the variable was created.
    *  @param  nestingLevel  Symbols with a nestingLevel strictly greater than this
    *                        will not appear in the instantiation of this type variable.
-   *                        This is enforced in `ConstraintHandling` by:
-   *                        - Maintaining the invariant that the `nonParamBounds`
-   *                          of a type variable never refer to a type with a
-   *                          greater `nestingLevel` (see `legalBound` for the reason
-   *                          why this cannot be delayed until instantiation).
-   *                        - On instantiation, replacing any param in the param bound
-   *                          with a level greater than nestingLevel (see `fullLowerBound`).
+   *                        This is enforced in `ConstraintHandling#fixLevels`.
+   *                        The `nestingLevel` of a type variable can be made smaller when
+   *                        fixing the levels for some other type variable instance.
    */
   final class TypeVar private(initOrigin: TypeParamRef, creatorState: TyperState | Null, var nestingLevel: Int) extends CachedProxyType with ValueType {
     private var currentOrigin = initOrigin
diff --git a/compiler/src/dotty/tools/dotc/inlines/InlineReducer.scala b/compiler/src/dotty/tools/dotc/inlines/InlineReducer.scala
index 717e7f42dabe..debf51872d5a 100644
--- a/compiler/src/dotty/tools/dotc/inlines/InlineReducer.scala
+++ b/compiler/src/dotty/tools/dotc/inlines/InlineReducer.scala
@@ -302,7 +302,8 @@ class InlineReducer(inliner: Inliner)(using Context):
 
       def addTypeBindings(typeBinds: TypeBindsMap)(using Context): Unit =
         typeBinds.foreachBinding { case (sym, shouldBeMinimized) =>
-          newTypeBinding(sym, ctx.gadt.approximation(sym, fromBelow = shouldBeMinimized, Int.MaxValue))
+          newTypeBinding(sym,
+            ctx.gadt.approximation(sym, fromBelow = shouldBeMinimized, maxLevel = Int.MaxValue))
         }
 
       def registerAsGadtSyms(typeBinds: TypeBindsMap)(using Context): Unit =
diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala
index 40f9906038f6..d3cf8308bf83 100644
--- a/compiler/src/dotty/tools/dotc/typer/Namer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala
@@ -1683,6 +1683,10 @@ class Namer { typer: Typer =>
             // are better ways to achieve this. It would be good if we could get rid of this code.
             // It seems at least partially redundant with the nesting level checking on TypeVar
             // instantiation.
+            // It turns out if we fix levels on instantiation we still need this code.
+            // Examples that fail otherwise are pos/scalaz-redux.scala and pos/java-futures.scala.
+            // So fixing levels at instantiation avoids the soundness problem but apparently leads
+            // to type inference problems since it comes too late.
             if !Config.checkLevels then
               val hygienicType = TypeOps.avoid(rhsType, termParamss.flatten)
               if (!hygienicType.isValueType || !(hygienicType <:< tpt.tpe))
diff --git a/tests/neg/i8861.scala b/tests/neg/i8861.scala
index ca337cd17095..7599848efe94 100644
--- a/tests/neg/i8861.scala
+++ b/tests/neg/i8861.scala
@@ -1,3 +1,4 @@
+// Compiles under 14026
 object Test {
   sealed trait Container { s =>
     type A
diff --git a/tests/neg/i8900-promote.scala b/tests/neg/i8900-promote.scala
index fac6f021edae..8be0029214b4 100644
--- a/tests/neg/i8900-promote.scala
+++ b/tests/neg/i8900-promote.scala
@@ -1,3 +1,4 @@
+// Compiles under #14026
 class Inv[A <: Singleton](x: A)
 object Inv {
   def empty[A <: Singleton]: Inv[A] = new Inv(???)
diff --git a/tests/pos/java-futures.scala b/tests/pos/java-futures.scala
new file mode 100644
index 000000000000..f6c841675c92
--- /dev/null
+++ b/tests/pos/java-futures.scala
@@ -0,0 +1,26 @@
+import java.util.concurrent.{TimeUnit, TimeoutException, Future, Executors => JExecutors}
+
+class TestSource
+trait LoggedRunnable extends Runnable
+
+
+
+object Test:
+
+  val filteredSources: List[TestSource] = ???
+
+  def encapsulatedCompilation(testSource: TestSource): LoggedRunnable = ???
+
+  def testSuite(): this.type =
+    val pool = JExecutors.newWorkStealingPool(Runtime.getRuntime.availableProcessors())
+    val eventualResults = for target <- filteredSources yield
+      pool.submit(encapsulatedCompilation(target))
+
+    for fut <- eventualResults do
+      try fut.get()
+      catch case ex: Exception =>
+        System.err.println(ex.getMessage)
+        ex.printStackTrace()
+
+    this
+
diff --git a/tests/pos/scalaz-redux.scala b/tests/pos/scalaz-redux.scala
new file mode 100644
index 000000000000..49a442966487
--- /dev/null
+++ b/tests/pos/scalaz-redux.scala
@@ -0,0 +1,20 @@
+
+sealed abstract class LazyEither[A, B] {
+
+  def fold[X](left: (=> A) => X, right: (=> B) => X): X =
+    this match {
+      case LazyLeft(a)  => left(a())
+      case LazyRight(b) => right(b())
+    }
+}
+
+object LazyEither {
+
+  final case class LeftProjection[A, B](e: LazyEither[A, B]) extends AnyVal {
+
+    def getOrElse[AA >: A](default: => AA): AA =
+      e.fold(z => z, _ => default)
+  }
+}
+private case class LazyLeft[A, B](a: () => A) extends LazyEither[A, B]
+private case class LazyRight[A, B](b: () => B) extends LazyEither[A, B]

From d44cbab0c1b853576a6d5616950894e99c53b903 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 26 Jul 2022 11:37:56 +0200
Subject: [PATCH 3/8] Change Config flags

Introduce separate Config flags that enable level checking on constraints
or level checking on instantiation.
---
 compiler/src/dotty/tools/dotc/config/Config.scala | 11 +++++++----
 .../tools/dotc/core/ConstraintHandling.scala      | 15 +++++++++------
 .../dotty/tools/dotc/core/tasty/TreePickler.scala |  2 +-
 compiler/src/dotty/tools/dotc/typer/Namer.scala   |  2 +-
 4 files changed, 18 insertions(+), 12 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala
index 0ea5089ed13c..67545233136d 100644
--- a/compiler/src/dotty/tools/dotc/config/Config.scala
+++ b/compiler/src/dotty/tools/dotc/config/Config.scala
@@ -227,9 +227,12 @@ object Config {
    */
   inline val reuseSymDenotations = true
 
-  /** If true, check levels of type variables and create fresh ones as needed.
-   *  This is necessary for soundness (see 3ab18a9), but also causes several
-   *  regressions that should be fixed before turning this on.
+  /** If `checkLevelsOnConstraints` is true, check levels of type variables
+   *  and create fresh ones as needed when bounds are first entered intot he constraint.
+   *  If `checkLevelsOnInstantiation` is true, allow level-incorrect constraints but
+   *  fix levels on type variable instantiation.
    */
-  inline val checkLevels = false
+  inline val checkLevelsOnConstraints = false
+  inline val checkLevelsOnInstantiation = true
+
 }
diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index d91d4f8fda8d..fa14348017b8 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -103,12 +103,15 @@ trait ConstraintHandling {
    *  of `1`. So the lower bound is `1 | x.M` and when we level-avoid that we
    *  get `1 | Int & String`, which simplifies to `Int`.
    */
-  protected var trustBounds = true
+  private var myTrustBounds = true
 
   inline def withUntrustedBounds(op: => Type): Type =
-    val saved = trustBounds
-    trustBounds = false
-    try op finally trustBounds = saved
+    val saved = myTrustBounds
+    myTrustBounds = false
+    try op finally myTrustBounds = saved
+
+  def trustBounds: Boolean =
+    !Config.checkLevelsOnInstantiation || myTrustBounds
 
   def checkReset() =
     assert(addConstraintInvocations == 0)
@@ -131,7 +134,7 @@ trait ConstraintHandling {
     level <= maxLevel
     || ctx.isAfterTyper || !ctx.typerState.isCommittable // Leaks in these cases shouldn't break soundness
     || level == Int.MaxValue // See `nestingLevel` above.
-    || !Config.checkLevels
+    || !Config.checkLevelsOnConstraints
 
   /** If `param` is nested deeper than `maxLevel`, try to instantiate it to a
    *  fresh type variable of level `maxLevel` and return the new variable.
@@ -518,7 +521,7 @@ trait ConstraintHandling {
       if !fromBelow then variance = -1
       def toAvoid(tp: NamedType) = needsFix(tp)
 
-    if ctx.isAfterTyper then tp
+    if !Config.checkLevelsOnInstantiation || ctx.isAfterTyper then tp
     else
       val needsLeveling = NeedsLeveling()
       if needsLeveling(false, tp) then
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index 8d80d69fdfa9..475a258e8330 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -206,7 +206,7 @@ class TreePickler(pickler: TastyPickler) {
       }
       else if (tpe.prefix == NoPrefix) {
         writeByte(if (tpe.isType) TYPEREFdirect else TERMREFdirect)
-        if Config.checkLevels && !symRefs.contains(sym) && !sym.isPatternBound && !sym.hasAnnotation(defn.QuotedRuntimePatterns_patternTypeAnnot) then
+        if Config.checkLevelsOnConstraints && !symRefs.contains(sym) && !sym.isPatternBound && !sym.hasAnnotation(defn.QuotedRuntimePatterns_patternTypeAnnot) then
           report.error(i"pickling reference to as yet undefined $tpe with symbol ${sym}", sym.srcPos)
         pickleSymRef(sym)
       }
diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala
index d3cf8308bf83..e6426cc54cd5 100644
--- a/compiler/src/dotty/tools/dotc/typer/Namer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala
@@ -1687,7 +1687,7 @@ class Namer { typer: Typer =>
             // Examples that fail otherwise are pos/scalaz-redux.scala and pos/java-futures.scala.
             // So fixing levels at instantiation avoids the soundness problem but apparently leads
             // to type inference problems since it comes too late.
-            if !Config.checkLevels then
+            if !Config.checkLevelsOnConstraints then
               val hygienicType = TypeOps.avoid(rhsType, termParamss.flatten)
               if (!hygienicType.isValueType || !(hygienicType <:< tpt.tpe))
                 report.error(i"return type ${tpt.tpe} of lambda cannot be made hygienic;\n" +

From 4649fd9b4dde52b786f6ebd9c05c2a2e5ee7b3e9 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 26 Jul 2022 11:48:37 +0200
Subject: [PATCH 4/8] Explain both level avoidance schemes in the TypeVar doc
 comment

---
 compiler/src/dotty/tools/dotc/core/Types.scala | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 3d77ada0c90b..83ff371e1a0e 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4501,9 +4501,21 @@ object Types {
    *  @param  creatorState  The typer state in which the variable was created.
    *  @param  nestingLevel  Symbols with a nestingLevel strictly greater than this
    *                        will not appear in the instantiation of this type variable.
-   *                        This is enforced in `ConstraintHandling#fixLevels`.
-   *                        The `nestingLevel` of a type variable can be made smaller when
-   *                        fixing the levels for some other type variable instance.
+   *                        This is enforced in `ConstraintHandling`, dependig on the
+   *                        Config flags setting `checkLevelsOnConstraints` and
+   *                        `checkLevelsOnInstantiation`.
+   *
+   *                        Under `checkLevelsOnConstraints` we maintain the invariant that
+   *                        the `nonParamBounds` of a type variable never refer to a type with a
+   *                        greater `nestingLevel` (see `legalBound` for the reason why this
+   *                        cannot be delayed until instantiation). Then, on instantiation,
+   *                        we replace any param in the param bound with a level greater than
+   *                        nestingLevel (see `fullLowerBound`).
+   *
+   *                        Under `checkLevelsOnInstantiation`, we avoid incorrect levels only
+   *                        when a type variable is instantiated, see `ConstraintHandling$fixLevels`.
+   *                        Under this mode, the `nestingLevel` of a type variable can be made
+   *                        smaller when fixing the levels for some other type variable instance.
    */
   final class TypeVar private(initOrigin: TypeParamRef, creatorState: TyperState | Null, var nestingLevel: Int) extends CachedProxyType with ValueType {
     private var currentOrigin = initOrigin

From 06336a2d5a676a200d5d5f715cf818dc92489efe Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 19 Aug 2022 19:59:57 +0200
Subject: [PATCH 5/8] Comment and diagnostic printing when lowering
 nestingLevel

---
 .../src/dotty/tools/dotc/core/ConstraintHandling.scala | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index fa14348017b8..d6f21a4344d1 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -501,7 +501,7 @@ trait ConstraintHandling {
             else if tp.nestingLevel > maxLevel then
               if variance > 0 then nestedVarsLo += tp
               else if variance < 0 then nestedVarsHi += tp
-              else tp.nestingLevel = maxLevel
+              else
                 // For invariant type variables, we use a different strategy.
                 // Rather than instantiating to a bound and then propagating in an
                 // AvoidMap, change the nesting level of an invariant type
@@ -511,6 +511,14 @@ trait ConstraintHandling {
                 // `fixLevels`, this could lead to coarser types. But it has the potential
                 // to give a better approximation for the current type, since it avoids forming
                 // a Range in invariant position, which can lead to very coarse types further out.
+                // TODO: This widening is a side effect that is not undone if a typer state is aborted
+                // I don't think it's a soundness problem, since all that could happen is that
+                // the type variable causes earlier instantiations of other type variables
+                // down the line. But it could produce a hard-to-debug side effect that leads
+                // to worse types than expected. We should find a more robust way to do this.
+                // Maybe instantiating `tp` to another freshly created type at nesting level?
+                constr.println(i"widening nesting level of type variable $tp from ${tp.nestingLevel} to $maxLevel")
+                tp.nestingLevel = maxLevel
               true
             else false
           case _ =>

From ec2b5d683ed95474d8092b0da444a0ab4dde5a8c Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 20 Aug 2022 15:13:36 +0200
Subject: [PATCH 6/8] Update nesting level in typer state

---
 .../tools/dotc/core/ConstraintHandling.scala  |  8 +---
 .../dotty/tools/dotc/core/TyperState.scala    | 37 +++++++++++++---
 .../src/dotty/tools/dotc/core/Types.scala     | 44 ++++++++++---------
 3 files changed, 57 insertions(+), 32 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index d6f21a4344d1..747500465c0a 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -511,14 +511,8 @@ trait ConstraintHandling {
                 // `fixLevels`, this could lead to coarser types. But it has the potential
                 // to give a better approximation for the current type, since it avoids forming
                 // a Range in invariant position, which can lead to very coarse types further out.
-                // TODO: This widening is a side effect that is not undone if a typer state is aborted
-                // I don't think it's a soundness problem, since all that could happen is that
-                // the type variable causes earlier instantiations of other type variables
-                // down the line. But it could produce a hard-to-debug side effect that leads
-                // to worse types than expected. We should find a more robust way to do this.
-                // Maybe instantiating `tp` to another freshly created type at nesting level?
                 constr.println(i"widening nesting level of type variable $tp from ${tp.nestingLevel} to $maxLevel")
-                tp.nestingLevel = maxLevel
+                ctx.typerState.setNestingLevel(tp, maxLevel)
               true
             else false
           case _ =>
diff --git a/compiler/src/dotty/tools/dotc/core/TyperState.scala b/compiler/src/dotty/tools/dotc/core/TyperState.scala
index 34f9a0139142..cea96e29fab6 100644
--- a/compiler/src/dotty/tools/dotc/core/TyperState.scala
+++ b/compiler/src/dotty/tools/dotc/core/TyperState.scala
@@ -10,7 +10,7 @@ import config.Config
 import config.Printers.constr
 import collection.mutable
 import java.lang.ref.WeakReference
-import util.Stats
+import util.{Stats, SimpleIdentityMap}
 import Decorators._
 
 import scala.annotation.internal.sharable
@@ -23,24 +23,28 @@ object TyperState {
       .setReporter(new ConsoleReporter())
       .setCommittable(true)
 
-  opaque type Snapshot = (Constraint, TypeVars, TypeVars)
+  type LevelMap = SimpleIdentityMap[TypeVar, Integer]
+
+  opaque type Snapshot = (Constraint, TypeVars, TypeVars, LevelMap)
 
   extension (ts: TyperState)
     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)
+      (ts.constraint, ts.ownedVars, previouslyInstantiated, ts.upLevels)
 
     def resetTo(state: Snapshot)(using Context): Unit =
-      val (c, tvs, previouslyInstantiated) = state
+      val (c, tvs, previouslyInstantiated, upLevels) = state
       for tv <- tvs do
         if tv.inst.exists && !previouslyInstantiated.contains(tv) then
           tv.resetInst(ts)
       ts.ownedVars = tvs
       ts.constraint = c
+      ts.upLevels = upLevels
 }
 
 class TyperState() {
+  import TyperState.LevelMap
 
   private var myId: Int = _
   def id: Int = myId
@@ -89,6 +93,8 @@ class TyperState() {
   def ownedVars: TypeVars = myOwnedVars
   def ownedVars_=(vs: TypeVars): Unit = myOwnedVars = vs
 
+  private var upLevels: LevelMap = _
+
   /** Initializes all fields except reporter, isCommittable, which need to be
    *  set separately.
    */
@@ -99,6 +105,7 @@ class TyperState() {
     this.myConstraint = constraint
     this.previousConstraint = constraint
     this.myOwnedVars = SimpleIdentitySet.empty
+    this.upLevels = SimpleIdentityMap.empty
     this.isCommitted = false
     this
 
@@ -106,13 +113,27 @@ class TyperState() {
   def fresh(reporter: Reporter = StoreReporter(this.reporter, fromTyperState = true),
       committable: Boolean = this.isCommittable): TyperState =
     util.Stats.record("TyperState.fresh")
-    TyperState().init(this, this.constraint)
+    val ts = TyperState().init(this, this.constraint)
       .setReporter(reporter)
       .setCommittable(committable)
+    ts.upLevels = upLevels
+    ts
 
   /** The uninstantiated variables */
   def uninstVars: collection.Seq[TypeVar] = constraint.uninstVars
 
+  /** The nestingLevel of `tv` in this typer state */
+  def nestingLevel(tv: TypeVar): Int =
+    val own = upLevels(tv)
+    if own == null then tv.initNestingLevel else own.intValue()
+
+  /** Set the nestingLevel of `tv` in this typer state
+   *  @pre this level must be smaller than `tv.initNestingLevel`
+  */
+  def setNestingLevel(tv: TypeVar, level: Int) =
+    assert(level < tv.initNestingLevel)
+    upLevels = upLevels.updated(tv, level)
+
   /** The closest ancestor of this typer state (including possibly this typer state itself)
    *  which is not yet committed, or which does not have a parent.
    */
@@ -164,6 +185,12 @@ class TyperState() {
         if !ownedVars.isEmpty then ownedVars.foreach(targetState.includeVar)
       else
         targetState.mergeConstraintWith(this)
+
+    upLevels.foreachBinding { (tv, level) =>
+      if level < targetState.nestingLevel(tv) then
+        targetState.setNestingLevel(tv, level)
+    }
+    
     targetState.gc()
     isCommitted = true
     ownedVars = SimpleIdentitySet.empty
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 83ff371e1a0e..e906313510a7 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4497,27 +4497,11 @@ object Types {
    *  is different from the variable's creation state (meaning unrolls are possible)
    *  in the current typer state.
    *
-   *  @param  origin        The parameter that's tracked by the type variable.
-   *  @param  creatorState  The typer state in which the variable was created.
-   *  @param  nestingLevel  Symbols with a nestingLevel strictly greater than this
-   *                        will not appear in the instantiation of this type variable.
-   *                        This is enforced in `ConstraintHandling`, dependig on the
-   *                        Config flags setting `checkLevelsOnConstraints` and
-   *                        `checkLevelsOnInstantiation`.
-   *
-   *                        Under `checkLevelsOnConstraints` we maintain the invariant that
-   *                        the `nonParamBounds` of a type variable never refer to a type with a
-   *                        greater `nestingLevel` (see `legalBound` for the reason why this
-   *                        cannot be delayed until instantiation). Then, on instantiation,
-   *                        we replace any param in the param bound with a level greater than
-   *                        nestingLevel (see `fullLowerBound`).
-   *
-   *                        Under `checkLevelsOnInstantiation`, we avoid incorrect levels only
-   *                        when a type variable is instantiated, see `ConstraintHandling$fixLevels`.
-   *                        Under this mode, the `nestingLevel` of a type variable can be made
-   *                        smaller when fixing the levels for some other type variable instance.
+   *  @param  origin           the parameter that's tracked by the type variable.
+   *  @param  creatorState     the typer state in which the variable was created.
+   *  @param  initNestingLevel the initial nesting level of the type variable. (c.f. nestingLevel)
    */
-  final class TypeVar private(initOrigin: TypeParamRef, creatorState: TyperState | Null, var nestingLevel: Int) extends CachedProxyType with ValueType {
+  final class TypeVar private(initOrigin: TypeParamRef, creatorState: TyperState | Null, val initNestingLevel: Int) extends CachedProxyType with ValueType {
     private var currentOrigin = initOrigin
 
     def origin: TypeParamRef = currentOrigin
@@ -4549,6 +4533,26 @@ object Types {
     private[core] var owningState: WeakReference[TyperState] | Null =
       if (creatorState == null) null else new WeakReference(creatorState)
 
+    /** The nesting level of this type variable in the current typer state. This is usually
+     *  the same as `initNestingLevel`, but can be decremented by calling `TyperState#setNestingLevel`.
+     *  Symbols with a nestingLevel strictly greater than this level will not appear in the
+     *  instantiation of this type variable. This is enforced in `ConstraintHandling`,
+     *  dependig on the Config flags setting `checkLevelsOnConstraints` and `checkLevelsOnInstantiation`.
+     *
+     *  Under `checkLevelsOnConstraints` we maintain the invariant that
+     *  the `nonParamBounds` of a type variable never refer to a type with a
+     *  greater `nestingLevel` (see `legalBound` for the reason why this
+     *  cannot be delayed until instantiation). Then, on instantiation,
+     *  we replace any param in the param bound with a level greater than
+     *  nestingLevel (see `fullLowerBound`).
+     *
+     *  Under `checkLevelsOnInstantiation`, we avoid incorrect levels only
+     *  when a type variable is instantiated, see `ConstraintHandling$fixLevels`.
+     *  Under this mode, the `nestingLevel` of a type variable can be made
+     *  smaller when fixing the levels for some other type variable instance.
+     */
+    def nestingLevel(using Context): Int = ctx.typerState.nestingLevel(this)
+
     /** The instance type of this variable, or NoType if the variable is currently
      *  uninstantiated
      */

From 86f249c50a6e5ad360de6cc65a12092ee2694dad Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 21 Aug 2022 12:32:30 +0200
Subject: [PATCH 7/8] Fix resetInst logic

The previous way never reset any type variable since it traversed `ownedVars`, and
instantiated TypeVars are no longer in the ownedVars of their owning TyperState.
---
 .../src/dotty/tools/dotc/core/TyperState.scala | 18 ++++++++----------
 compiler/src/dotty/tools/dotc/core/Types.scala |  1 +
 2 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TyperState.scala b/compiler/src/dotty/tools/dotc/core/TyperState.scala
index cea96e29fab6..81b60c608e28 100644
--- a/compiler/src/dotty/tools/dotc/core/TyperState.scala
+++ b/compiler/src/dotty/tools/dotc/core/TyperState.scala
@@ -25,21 +25,19 @@ object TyperState {
 
   type LevelMap = SimpleIdentityMap[TypeVar, Integer]
 
-  opaque type Snapshot = (Constraint, TypeVars, TypeVars, LevelMap)
+  opaque type Snapshot = (Constraint, TypeVars, LevelMap)
 
   extension (ts: TyperState)
     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, ts.upLevels)
+      (ts.constraint, ts.ownedVars, ts.upLevels)
 
     def resetTo(state: Snapshot)(using Context): Unit =
-      val (c, tvs, previouslyInstantiated, upLevels) = state
-      for tv <- tvs do
-        if tv.inst.exists && !previouslyInstantiated.contains(tv) then
+      val (constraint, ownedVars, upLevels) = state
+      for tv <- ownedVars do
+        if !ts.ownedVars.contains(tv) then // tv has been instantiated
           tv.resetInst(ts)
-      ts.ownedVars = tvs
-      ts.constraint = c
+      ts.constraint = constraint
+      ts.ownedVars = ownedVars
       ts.upLevels = upLevels
 }
 
@@ -190,7 +188,7 @@ class TyperState() {
       if level < targetState.nestingLevel(tv) then
         targetState.setNestingLevel(tv, level)
     }
-    
+
     targetState.gc()
     isCommitted = true
     ownedVars = SimpleIdentitySet.empty
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index e906313510a7..65352aaae219 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4524,6 +4524,7 @@ object Types {
           owningState = null // no longer needed; null out to avoid a memory leak
 
     private[core] def resetInst(ts: TyperState): Unit =
+      assert(myInst.exists)
       myInst = NoType
       owningState = new WeakReference(ts)
 

From f01abfba6840d8e91e1a8936cd7c112007667a23 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 21 Aug 2022 12:48:51 +0200
Subject: [PATCH 8/8] Update comment for harmonize

---
 compiler/src/dotty/tools/dotc/typer/Applications.scala | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index f650304c3f0e..c662d6f00045 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -2216,7 +2216,13 @@ trait Applications extends Compatibility {
    *  have added constraints to type parameters which are no longer
    *  implied after harmonization. No essential constraints are lost by this because
    *  the result of harmonization will be compared again with the expected type.
-   *  Test cases where this matters are in pos/harmomize.scala.
+   *  Test cases where this matters are in neg/harmomize.scala and run/weak-conformance.scala.
+   *
+   *  Note: this assumes that the internal typing of the arguments using `op` does
+   *  not leave any constraints, so the only info that is reset is the relationship
+   *  between the argument's types and the expected type. I am not sure this will
+   *  always be the case. If that property does not hold, we risk forgetting constraints
+   *  which could lead to unsoundness.
    */
   def harmonic[T](harmonize: List[T] => List[T], pt: Type)(op: => List[T])(using Context): List[T] =
     if (!isFullyDefined(pt, ForceDegree.none)) {