Add comments

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

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

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 =

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))

tests/neg/i8861.scala

@@ -1,3 +1,4 @@
+// Compiles under 14026
 object Test {
   sealed trait Container { s =>
     type A

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(???)

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
+

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]