Create fresh type variables to keep constraints level-correct

This completes the implementation of `LevelAvoidMap` from the previous
commit: we now make sure that the nonParamBounds of a type variable does
not refer to variables of a higher level by creating fresh variables of
the appropriate level if necessary. Each fresh variable will be upper-
or lower-bounded by the existing variable it is substituted for
depending on variance (an idea that I got from [1]), in the invariant
case the existing variable will be instantiated to the fresh one (unlike
[2], we can't simply mutate the nestingLevel of the existing variable
after running avoidance on its bounds because the constraint containing
these bounds might later be retracted).

Additionally:
- When unifying two type variables, keep the one with the lowest level in
the constraint set and make sure the bounds transferred from the other
one are level-correct. This required some changes in
`Constraint#addLess` which previously assumed that `unify` would
always keep the second parameter.
- When instantiating a type variable to its full lower- or upper-bound,
we also need to avoid any type variable of a higher level among its
param bound.

This commit is necessary to avoid leaking local types in i8900a2.scala
and i8900a3.scala, these kind of leaks will become compile-time error in
the next commit.

This commit required making a type parameter explicit both in
SnippetChecker.scala and i13809/Macros_1.scala, in both situations the
problem is that the lambda passed to `map` can only be typed if the type
argument of `map` contains a wildcard, but LevelAvoidMap instead creates
a fresh type variable of a lower level at a point where we don't know
yet that this cannot work. Since this situation seems very rare in
practice, I believe this is an acceptable trade-off for soundness.

[1]: Lionel Parreaux. "The simple essence of algebraic subtyping:
 principal type inference with subtyping made easy (functional pearl)."
 https://dl.acm.org/doi/abs/10.1145/3409006

[2]: Oleg Kiselyov. "How OCaml type checker works -- or what
 polymorphism and garbage collection have in common"
 https://okmij.org/ftp/ML/generalization.html

Author: smarter

compiler/src/dotty/tools/dotc/core/Constraint.scala

@@ -93,13 +93,15 @@ abstract class Constraint extends Showable {
   /** A constraint that includes the relationship `p1 <: p2`.
    *  `<:` relationships between parameters ("edges") are propagated, but
    *  non-parameter bounds are left alone.
+   *
+   *  @param direction  Must be set to `KeepParam1` or `KeepParam2` when
+   *                    `p2 <: p1` is already true depending on which parameter
+   *                    the caller intends to keep. This will avoid propagating
+   *                    bounds that will be redundant after `p1` and `p2` are
+   *                    unified.
    */
-  def addLess(p1: TypeParamRef, p2: TypeParamRef)(using Context): This
-
-  /** A constraint resulting from adding p2 = p1 to this constraint, and at the same
-   *  time transferring all bounds of p2 to p1
-   */
-  def unify(p1: TypeParamRef, p2: TypeParamRef)(using Context): This
+  def addLess(p1: TypeParamRef, p2: TypeParamRef,
+    direction: UnificationDirection = UnificationDirection.NoUnification)(using Context): This
 
   /** A new constraint which is derived from this constraint by removing
    *  the type parameter `param` from the domain and replacing all top-level occurrences
@@ -174,3 +176,15 @@ abstract class Constraint extends Showable {
    */
   def checkConsistentVars()(using Context): Unit
 }
+
+/** When calling `Constraint#addLess(p1, p2, ...)`, the caller might end up
+ *  unifying one parameter with the other, this enum lets `addLess` know which
+ *  direction the unification will take.
+ */
+enum UnificationDirection:
+  /** Neither p1 nor p2 will be instantiated. */
+  case NoUnification
+  /** `p2 := p1`, p1 left uninstantiated. */
+  case KeepParam1
+  /** `p1 := p2`, p2 left uninstantiated. */
+  case KeepParam2

compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala

@@ -10,8 +10,10 @@ import Flags._
 import config.Config
 import config.Printers.typr
 import reporting.trace
-import typer.ProtoTypes.newTypeVar
+import typer.ProtoTypes.{newTypeVar, representedParamRef}
 import StdNames.tpnme
+import UnificationDirection.*
+import NameKinds.AvoidNameKind
 
 /** Methods for adding constraints and solving them.
  *
@@ -85,13 +87,30 @@ trait ConstraintHandling {
     case tv: TypeVar => tv.nestingLevel
     case _ => Int.MaxValue
 
+  /** If `param` is nested deeper than `maxLevel`, try to instantiate it to a
+   *  fresh type variable of level `maxLevel` and return the new variable.
+   *  If this isn't possible, throw a TypeError.
+   */
+  def atLevel(maxLevel: Int, param: TypeParamRef)(using Context): TypeParamRef =
+    if nestingLevel(param) <= maxLevel then return param
+    LevelAvoidMap(0, maxLevel)(param) match
+      case freshVar: TypeVar => freshVar.origin
+      case _ => throw new TypeError(
+        i"Could not decrease the nesting level of ${param} from ${nestingLevel(param)} to $maxLevel in $constraint")
+
   def nonParamBounds(param: TypeParamRef)(using Context): TypeBounds = constraint.nonParamBounds(param)
 
-  def fullLowerBound(param: TypeParamRef)(using Context): Type =
-    constraint.minLower(param).foldLeft(nonParamBounds(param).lo)(_ | _)
+  def fullLowerBound(param: TypeParamRef, maxLevel: Int = Int.MaxValue)(using Context): Type =
+    var loParams = constraint.minLower(param)
+    if maxLevel != Int.MaxValue then
+      loParams = loParams.mapConserve(atLevel(maxLevel, _))
+    loParams.foldLeft(nonParamBounds(param).lo)(_ | _)
 
-  def fullUpperBound(param: TypeParamRef)(using Context): Type =
-    constraint.minUpper(param).foldLeft(nonParamBounds(param).hi)(_ & _)
+  def fullUpperBound(param: TypeParamRef, maxLevel: Int = Int.MaxValue)(using Context): Type =
+    var hiParams = constraint.minUpper(param)
+    if maxLevel != Int.MaxValue then
+      hiParams = hiParams.mapConserve(atLevel(maxLevel, _))
+    hiParams.foldLeft(nonParamBounds(param).hi)(_ & _)
 
   /** Full bounds of `param`, including other lower/upper params.
     *
@@ -116,10 +135,64 @@ trait ConstraintHandling {
     def toAvoid(tp: NamedType): Boolean =
       tp.prefix == NoPrefix && !tp.symbol.isStatic && !levelOK(tp.symbol.nestingLevel)
 
+    /** Return a (possibly fresh) type variable of a level no greater than `maxLevel` which is:
+     *  - lower-bounded by `tp` if variance >= 0
+     *  - upper-bounded by `tp` if variance <= 0
+     *  If this isn't possible, return the empty range.
+     */
+    def legalVar(tp: TypeVar): Type =
+      val oldParam = tp.origin
+      val nameKind =
+        if variance > 0 then AvoidNameKind.UpperBound
+        else if variance < 0 then AvoidNameKind.LowerBound
+        else AvoidNameKind.BothBounds
+
+      /** If it exists, return the first param in the list created in a previous call to `legalVar(tp)`
+       *  with the appropriate level and variance.
+       */
+      def findParam(params: List[TypeParamRef]): Option[TypeParamRef] =
+        params.find(p =>
+          nestingLevel(p) <= maxLevel && representedParamRef(p) == oldParam &&
+          (p.paramName.is(AvoidNameKind.BothBounds) ||
+           variance != 0 && p.paramName.is(nameKind)))
+
+      // First, check if we can reuse an existing parameter, this is more than an optimization
+      // since it avoids an infinite loop in tests/pos/i8900-cycle.scala
+      findParam(constraint.lower(oldParam)).orElse(findParam(constraint.upper(oldParam))) match
+        case Some(param) =>
+          constraint.typeVarOfParam(param)
+        case _ =>
+          // Otherwise, try to return a fresh type variable at `maxLevel` with
+          // the appropriate constraints.
+          val name = nameKind(oldParam.paramName.toTermName).toTypeName
+          val freshVar = newTypeVar(TypeBounds.upper(tp.topType), name,
+            nestingLevel = maxLevel, represents = oldParam)
+          val ok =
+            if variance < 0 then
+              addLess(freshVar.origin, oldParam)
+            else if variance > 0 then
+              addLess(oldParam, freshVar.origin)
+            else
+              unify(freshVar.origin, oldParam)
+          if ok then freshVar else emptyRange
+    end legalVar
+
+    override def apply(tp: Type): Type = tp match
+      case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel) =>
+        legalVar(tp)
+      // TypeParamRef can occur in tl bounds
+      case tp: TypeParamRef =>
+        constraint.typeVarOfParam(tp) match
+          case tvar: TypeVar =>
+            apply(tvar)
+          case _ => super.apply(tp)
+      case _ =>
+        super.apply(tp)
+
     override def mapWild(t: WildcardType) =
       if ctx.mode.is(Mode.TypevarsMissContext) then super.mapWild(t)
       else
-        val tvar = newTypeVar(apply(t.effectiveBounds).toBounds)
+        val tvar = newTypeVar(apply(t.effectiveBounds).toBounds, nestingLevel = maxLevel)
         tvar
   end LevelAvoidMap
 
@@ -151,7 +224,16 @@ trait ConstraintHandling {
           // flip the variance to under-approximate.
           if necessaryConstraintsOnly then variance = -variance
 
-          val approx = LevelAvoidMap(variance, level)
+          val approx = new LevelAvoidMap(variance, nestingLevel(param)):
+            override def legalVar(tp: TypeVar): Type =
+              // `legalVar` will create a type variable whose bounds depend on
+              // `variance`, but whether the variance is positive or negative,
+              // we can still infer necessary constraints since just creating a
+              // type variable doesn't reduce the set of possible solutions.
+              // Therefore, we can safely "unflip" the variance flipped above.
+              // This is necessary for i8900-unflip.scala to typecheck.
+              val v = if necessaryConstraintsOnly then -this.variance else this.variance
+              atVariance(v)(super.legalVar(tp))
           approx(rawBound)
 
       val oldBounds @ TypeBounds(lo, hi) = constraint.nonParamBounds(param)
@@ -248,19 +330,50 @@ trait ConstraintHandling {
 
   def location(using Context) = "" // i"in ${ctx.typerState.stateChainStr}" // use for debugging
 
-  /** Make p2 = p1, transfer all bounds of p2 to p1
-   *  @pre  less(p1)(p2)
+  /** Unify p1 with p2: one parameter will be kept in the constraint, the
+   *  other will be removed and its bounds transferred to the remaining one.
+   *
+   *  If p1 and p2 have different `nestingLevel`, the parameter with the lowest
+   *  level will be kept and the transferred bounds from the other parameter
+   *  will be adjusted for level-correctness.
    */
   private def unify(p1: TypeParamRef, p2: TypeParamRef)(using Context): Boolean = {
     constr.println(s"unifying $p1 $p2")
-    assert(constraint.isLess(p1, p2))
-    constraint = constraint.addLess(p2, p1)
+    if !constraint.isLess(p1, p2) then
+      constraint = constraint.addLess(p1, p2)
+
+    val level1 = nestingLevel(p1)
+    val level2 = nestingLevel(p2)
+    val pKept    = if level1 <= level2 then p1 else p2
+    val pRemoved = if level1 <= level2 then p2 else p1
+
+    constraint = constraint.addLess(p2, p1, direction = if pKept eq p1 then KeepParam2 else KeepParam1)
+
+    val boundKept    = constraint.nonParamBounds(pKept).substParam(pRemoved, pKept)
+    var boundRemoved = constraint.nonParamBounds(pRemoved).substParam(pRemoved, pKept)
+
+    if level1 != level2 then
+      boundRemoved = LevelAvoidMap(-1, math.min(level1, level2))(boundRemoved)
+      val TypeBounds(lo, hi) = boundRemoved
+      // After avoidance, the interval might be empty, e.g. in
+      // tests/pos/i8900-promote.scala:
+      //     >: x.type <: Singleton
+      // becomes:
+      //     >: Int <: Singleton
+      // In that case, we can still get a legal constraint
+      // by replacing the lower-bound to get:
+      //     >: Int & Singleton <: Singleton
+      if !isSub(lo, hi) then
+        boundRemoved = TypeBounds(lo & hi, hi)
+
     val down = constraint.exclusiveLower(p2, p1)
     val up = constraint.exclusiveUpper(p1, p2)
-    constraint = constraint.unify(p1, p2)
-    val bounds = constraint.nonParamBounds(p1)
-    val lo = bounds.lo
-    val hi = bounds.hi
+
+    val newBounds = (boundKept & boundRemoved).bounds
+    constraint = constraint.updateEntry(pKept, newBounds).replace(pRemoved, pKept)
+
+    val lo = newBounds.lo
+    val hi = newBounds.hi
     isSub(lo, hi) &&
     down.forall(addOneBound(_, hi, isUpper = true)) &&
     up.forall(addOneBound(_, lo, isUpper = false))
@@ -313,8 +426,13 @@ trait ConstraintHandling {
   final def approximation(param: TypeParamRef, fromBelow: Boolean)(using Context): Type =
     constraint.entry(param) match
       case entry: TypeBounds =>
+        val maxLevel = nestingLevel(param)
         val useLowerBound = fromBelow || param.occursIn(entry.hi)
-        val inst = if useLowerBound then fullLowerBound(param) else fullUpperBound(param)
+        val inst =
+          if useLowerBound then
+            fullLowerBound(param, maxLevel)
+          else
+            fullUpperBound(param, maxLevel)
         typr.println(s"approx ${param.show}, from below = $fromBelow, inst = ${inst.show}")
         inst
       case inst =>

compiler/src/dotty/tools/dotc/core/GadtConstraint.scala

@@ -11,6 +11,7 @@ import collection.mutable
 import printing._
 
 import scala.annotation.internal.sharable
+import scala.annotation.unused
 
 /** Represents GADT constraints currently in scope */
 sealed abstract class GadtConstraint extends Showable {
@@ -232,12 +233,14 @@ final class ProperGadtConstraint private(
     }
     externalizeMap(constraint.nonParamBounds(param)).bounds
 
-  override def fullLowerBound(param: TypeParamRef)(using Context): Type =
+  override def fullLowerBound(param: TypeParamRef,
+      @unused("no level checking needed in GADT constraints") maxLevel: Int)(using Context): Type =
     constraint.minLower(param).foldLeft(nonParamBounds(param).lo) {
       (t, u) => t | externalize(u)
     }
 
-  override def fullUpperBound(param: TypeParamRef)(using Context): Type =
+  override def fullUpperBound(param: TypeParamRef,
+      @unused("no level checking needed in GADT constraints") maxLevel: Int)(using Context): Type =
     constraint.minUpper(param).foldLeft(nonParamBounds(param).hi) { (t, u) =>
       val eu = externalize(u)
       // Any as the upper bound means "no bound", but if F is higher-kinded,

compiler/src/dotty/tools/dotc/core/NameKinds.scala

@@ -358,6 +358,13 @@ object NameKinds {
   val ProtectedAccessorName: PrefixNameKind = new PrefixNameKind(PROTECTEDACCESSOR, "protected$")
   val InlineAccessorName: PrefixNameKind = new PrefixNameKind(INLINEACCESSOR, "inline$")
 
+  /** See `ConstraintHandling#LevelAvoidMap`. */
+  enum AvoidNameKind(tag: Int, prefix: String) extends PrefixNameKind(tag, prefix):
+    override def definesNewName = true
+    case UpperBound extends AvoidNameKind(AVOIDUPPER, "(upper)")
+    case LowerBound extends AvoidNameKind(AVOIDLOWER, "(lower)")
+    case BothBounds extends AvoidNameKind(AVOIDBOTH, "(avoid)")
+
   val BodyRetainerName: SuffixNameKind = new SuffixNameKind(BODYRETAINER, "$retainedBody")
   val FieldName: SuffixNameKind = new SuffixNameKind(FIELD, "$$local") {
       override def mkString(underlying: TermName, info: ThisInfo) = underlying.toString

compiler/src/dotty/tools/dotc/core/NameTags.scala

@@ -32,6 +32,11 @@ object NameTags extends TastyFormat.NameTags {
 
   inline val SETTER = 34         // A synthesized += suffix.
 
+  // Name of type variables created by `ConstraintHandling#LevelAvoidMap`.
+  final val AVOIDUPPER = 35
+  final val AVOIDLOWER = 36
+  final val AVOIDBOTH = 37
+
   def nameTagToString(tag: Int): String = tag match {
     case UTF8 => "UTF8"
     case QUALIFIED => "QUALIFIED"

compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala

@@ -134,6 +134,8 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
                          private val lowerMap : ParamOrdering,
                          private val upperMap : ParamOrdering) extends Constraint {
 
+  import UnificationDirection.*
+
   type This = OrderingConstraint
 
 // ----------- Basic indices --------------------------------------------------
@@ -350,29 +352,37 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
   /** Add the fact `param1 <: param2` to the constraint `current` and propagate
    *  `<:<` relationships between parameters ("edges") but not bounds.
    */
-  private def order(current: This, param1: TypeParamRef, param2: TypeParamRef)(using Context): This =
+  def order(current: This, param1: TypeParamRef, param2: TypeParamRef, direction: UnificationDirection = NoUnification)(using Context): This =
     if (param1 == param2 || current.isLess(param1, param2)) this
     else {
       assert(contains(param1), i"$param1")
       assert(contains(param2), i"$param2")
-      // Is `order` called during parameter unification?
-      val unifying = isLess(param2, param1)
+      val unifying = direction != NoUnification
       val newUpper = {
         val up = exclusiveUpper(param2, param1)
         if unifying then
           // Since param2 <:< param1 already holds now, filter out param1 to avoid adding
           //   duplicated orderings.
-          param2 :: up.filterNot(_ eq param1)
+          val filtered = up.filterNot(_ eq param1)
+          // Only add bounds for param2 if it will be kept in the constraint after unification.
+          if direction == KeepParam2 then
+            param2 :: filtered
+          else
+            filtered
         else
           param2 :: up
       }
       val newLower = {
         val lower = exclusiveLower(param1, param2)
         if unifying then
-          // Do not add bounds for param1 since it will be unified to param2 soon.
-          // And, similarly filter out param2 from lowerly-ordered parameters
+          // Similarly, filter out param2 from lowerly-ordered parameters
           //   to avoid duplicated orderings.
-          lower.filterNot(_ eq param2)
+          val filtered = lower.filterNot(_ eq param2)
+          // Only add bounds for param1 if it will be kept in the constraint after unification.
+          if direction == KeepParam1 then
+            param1 :: filtered
+          else
+            filtered
         else
           param1 :: lower
       }
@@ -416,14 +426,8 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
   def updateEntry(param: TypeParamRef, tp: Type)(using Context): This =
     updateEntry(this, param, ensureNonCyclic(param, tp)).checkNonCyclic()
 
-  def addLess(param1: TypeParamRef, param2: TypeParamRef)(using Context): This =
-    order(this, param1, param2).checkNonCyclic()
-
-  def unify(p1: TypeParamRef, p2: TypeParamRef)(using Context): This =
-    val bound1 = nonParamBounds(p1).substParam(p2, p1)
-    val bound2 = nonParamBounds(p2).substParam(p2, p1)
-    val p1Bounds = bound1 & bound2
-    updateEntry(p1, p1Bounds).replace(p2, p1)
+  def addLess(param1: TypeParamRef, param2: TypeParamRef, direction: UnificationDirection)(using Context): This =
+    order(this, param1, param2, direction).checkNonCyclic()
 
 // ---------- Replacements and Removals -------------------------------------
 

compiler/src/dotty/tools/dotc/core/TypeApplications.scala

@@ -231,6 +231,16 @@ class TypeApplications(val self: Type) extends AnyVal {
       (alias ne self) && alias.hasSimpleKind
     }
 
+  /** The top type with the same kind as `self`. */
+  def topType(using Context): Type =
+    if self.hasSimpleKind then
+      defn.AnyType
+    else EtaExpand(self.typeParams) match
+      case tp: HKTypeLambda =>
+        tp.derivedLambdaType(resType = tp.resultType.topType)
+      case _ =>
+        defn.AnyKindType
+
   /** If self type is higher-kinded, its result type, otherwise NoType.
    *  Note: The hkResult of an any-kinded type is again AnyKind.
    */