Relax avoidance checks more for match type reduction

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

@@ -81,16 +81,28 @@ trait ConstraintHandling {
     assert(homogenizeArgs == false)
     assert(comparedTypeLambdas == Set.empty)
 
-  def nestingLevel(param: TypeParamRef) = constraint.typeVarOfParam(param) match
+  def nestingLevel(param: TypeParamRef)(using Context) = constraint.typeVarOfParam(param) match
     case tv: TypeVar => tv.nestingLevel
-    case _ => Int.MaxValue
+    case _ =>
+      // This should only happen when reducing match types (in
+      // TrackingTypeComparer#matchCases) or in uncommitable TyperStates (as
+      // asserted in ProtoTypes.constrained) and is special-cased in `levelOK`
+      // below.
+      Int.MaxValue
+
+  /** Is `level` <= `maxLevel` or legal in the current context? */
+  def levelOK(level: Int, maxLevel: Int)(using Context): Boolean =
+    level <= maxLevel ||
+    ctx.isAfterTyper || !ctx.typerState.isCommittable || // Leaks in these cases shouldn't break soundness
+    level == Int.MaxValue // See `nestingLevel` above.
 
   /** 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
+    if levelOK(nestingLevel(param), maxLevel) then
+      return param
     LevelAvoidMap(0, maxLevel)(param) match
       case freshVar: TypeVar => freshVar.origin
       case _ => throw new TypeError(
@@ -129,18 +141,12 @@ trait ConstraintHandling {
 
   /** An approximating map that prevents types nested deeper than maxLevel as
    *  well as WildcardTypes from leaking into the constraint.
-   *  Note that level-checking is turned off after typer and in uncommitable
-   *  TyperState since these leaks should be safe.
    */
   class LevelAvoidMap(topLevelVariance: Int, maxLevel: Int)(using Context) extends TypeOps.AvoidMap:
     variance = topLevelVariance
 
-    /** Are we allowed to refer to types of the given `level`? */
-    private def levelOK(level: Int): Boolean =
-      level <= maxLevel || ctx.isAfterTyper || !ctx.typerState.isCommittable
-
     def toAvoid(tp: NamedType): Boolean =
-      tp.prefix == NoPrefix && !tp.symbol.isStatic && !levelOK(tp.symbol.nestingLevel)
+      tp.prefix == NoPrefix && !tp.symbol.isStatic && !levelOK(tp.symbol.nestingLevel, maxLevel)
 
     /** Return a (possibly fresh) type variable of a level no greater than `maxLevel` which is:
      *  - lower-bounded by `tp` if variance >= 0
@@ -185,7 +191,7 @@ trait ConstraintHandling {
     end legalVar
 
     override def apply(tp: Type): Type = tp match
-      case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel) =>
+      case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel, maxLevel) =>
         legalVar(tp)
       // TypeParamRef can occur in tl bounds
       case tp: TypeParamRef =>
@@ -431,7 +437,6 @@ 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)
         typr.println(s"approx ${param.show}, from below = $fromBelow, inst = ${inst.show}")

compiler/src/dotty/tools/dotc/typer/Inferencing.scala

@@ -637,13 +637,15 @@ trait Inferencing { this: Typer =>
             else if v.intValue != 0 then
               typr.println(i"interpolate $tvar in $state in $tree: $tp, fromBelow = ${v.intValue == 1}, $constraint")
               toInstantiate += ((tvar, v.intValue == 1))
-            else if tvar.nestingLevel > ctx.nestingLevel then
-              // Invariant: a type variable of level N can only appear
-              // in the type of a tree whose enclosing scope is level <= N.
-              typr.println(i"instantiate nonvariant $tvar of level ${tvar.nestingLevel} to a type variable of level <= ${ctx.nestingLevel}, $constraint")
-              comparing(_.atLevel(ctx.nestingLevel, tvar.origin))
-            else
-              typr.println(i"no interpolation for nonvariant $tvar in $state")
+            else comparing(cmp =>
+              if !cmp.levelOK(tvar.nestingLevel, ctx.nestingLevel) then
+                // Invariant: The type of a tree whose enclosing scope is level
+                // N only contains type variables of level <= N.
+                typr.println(i"instantiate nonvariant $tvar of level ${tvar.nestingLevel} to a type variable of level <= ${ctx.nestingLevel}, $constraint")
+                cmp.atLevel(ctx.nestingLevel, tvar.origin)
+              else
+                typr.println(i"no interpolation for nonvariant $tvar in $state")
+            )
 
         /** Instantiate all type variables in `buf` in the indicated directions.
          *  If a type variable A is instantiated from below, and there is another

tests/pos/i14921/A_1.scala

@@ -0,0 +1,28 @@
+import scala.compiletime.ops.int.*
+
+final class Label (val getLabel: String)
+
+trait ShapelessPolyfill {
+
+  type Represented[R] = R match {
+    case IndexedSeq[a] => a
+  }
+
+  type TupleSized[R, A, N <: Int] <: Tuple = N match {
+    case 0 => EmptyTuple
+    case S[n] => A *: TupleSized[R, A, n]
+  }
+
+  extension [R, A, N <: Int] (s: TupleSized[R, A, N]) {
+    def unsized: IndexedSeq[A] = s.productIterator.toIndexedSeq.asInstanceOf[IndexedSeq[A]]
+  }
+
+  type Nat = Int
+
+  type Sized[Repr, L <: Nat] = TupleSized[Repr, Represented[Repr], L]
+
+  object Sized {
+    def apply[A](a1: A): Sized[IndexedSeq[A], 1] = Tuple1(a1)
+  }
+}
+object poly extends ShapelessPolyfill

tests/pos/i14921/B_2.scala

@@ -0,0 +1,3 @@
+import poly.*
+
+def failing: Tuple1[Label] = Sized(new Label("foo"))