Better level-checking in constraints to handle bad bounds

Previously, we enforced level-correctness only when instantiating type
variables, but this is not good enough as demonstrated by
tests/neg/i8900.scala. The problem is that if we allow level-incorrect
bounds, then we might end up reasoning with bad bounds outside of the
scope where they are defined. This can lead to level-correct but unsound
instantiations.

To prevent this, we now enforce level-correctness in constraints at all
times, we also introduce `AvoidMap` to share more logic between level-avoidance
and symbol-avoidance (see also the added TODO on `TypeOps#avoid`).

Note that this implementation is still incomplete: we only check the
nestingLevel of NamedTypes, but we also need to check for TypeVars, this
will be handled in the next commit.

Author: smarter

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

@@ -81,6 +81,10 @@ trait ConstraintHandling {
     assert(homogenizeArgs == false)
     assert(comparedTypeLambdas == Set.empty)
 
+  def nestingLevel(param: TypeParamRef) = constraint.typeVarOfParam(param) match
+    case tv: TypeVar => tv.nestingLevel
+    case _ => Int.MaxValue
+
   def nonParamBounds(param: TypeParamRef)(using Context): TypeBounds = constraint.nonParamBounds(param)
 
   def fullLowerBound(param: TypeParamRef)(using Context): Type =
@@ -97,23 +101,57 @@ trait ConstraintHandling {
   def fullBounds(param: TypeParamRef)(using Context): TypeBounds =
     nonParamBounds(param).derivedTypeBounds(fullLowerBound(param), fullUpperBound(param))
 
+  /** 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)
+
+    override def mapWild(t: WildcardType) =
+      if ctx.mode.is(Mode.TypevarsMissContext) then super.mapWild(t)
+      else
+        val tvar = newTypeVar(apply(t.effectiveBounds).toBounds)
+        tvar
+  end LevelAvoidMap
+
+  /** Approximate `rawBound` if needed to make it a legal bound of `param` by
+   *  avoiding wildcards and types with a level strictly greater than its
+   *  `nestingLevel`.
+   *
+   *  Note that level-checking must be performed here and cannot be delayed
+   *  until instantiation because if we allow level-incorrect bounds, then we
+   *  might end up reasoning with bad bounds outside of the scope where they are
+   *  defined. This can lead to level-correct but unsound instantiations as
+   *  demonstrated by tests/neg/i8900.scala.
+   */
+  protected def legalBound(param: TypeParamRef, rawBound: Type, isUpper: Boolean)(using Context): Type =
+    // Over-approximate for soundness.
+    var variance = if isUpper then -1 else 1
+    // ...unless we can only infer necessary constraints, in which case we
+    // flip the variance to under-approximate.
+    if necessaryConstraintsOnly then variance = -variance
+
+    val approx = LevelAvoidMap(variance, nestingLevel(param))
+    approx(rawBound)
+  end legalBound
+
   protected def addOneBound(param: TypeParamRef, rawBound: Type, isUpper: Boolean)(using Context): Boolean =
     if !constraint.contains(param) then true
     else if !isUpper && param.occursIn(rawBound) then
       // We don't allow recursive lower bounds when defining a type,
       // so we shouldn't allow them as constraints either.
       false
     else
-      val dropWildcards = new AvoidWildcardsMap:
-        // Approximate the upper-bound from below and vice-versa
-        if isUpper then variance = -1
-        // ...unless we can only infer necessary constraints, in which case we
-        // flip the variance to under-approximate.
-        if necessaryConstraintsOnly then variance = -variance
-        override def mapWild(t: WildcardType) =
-          if ctx.mode.is(Mode.TypevarsMissContext) then super.mapWild(t)
-          else newTypeVar(apply(t.effectiveBounds).toBounds)
-      val bound = dropWildcards(rawBound)
+      val bound = legalBound(param, rawBound, isUpper)
       val oldBounds @ TypeBounds(lo, hi) = constraint.nonParamBounds(param)
       val equalBounds = (if isUpper then lo else hi) eq bound
       if equalBounds && !bound.existsPart(_ eq param, StopAt.Static) then

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

@@ -79,6 +79,11 @@ final class ProperGadtConstraint private(
     subsumes(extractConstraint(left), extractConstraint(right), extractConstraint(pre))
   }
 
+  override protected def legalBound(param: TypeParamRef, rawBound: Type, isUpper: Boolean)(using Context): Type =
+    // GADT constraints never involve wildcards and are not propagated outside
+    // the case where they're valid, so no approximating is needed.
+    rawBound
+
   override def addToConstraint(params: List[Symbol])(using Context): Boolean = {
     import NameKinds.DepParamName
 

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

@@ -410,91 +410,109 @@ object TypeOps:
     }
   }
 
-  /** An upper approximation of the given type `tp` that does not refer to any symbol in `symsToAvoid`.
+  /** An approximating map that drops NamedTypes matching `toAvoid` and wildcard types. */
+  abstract class AvoidMap(using Context) extends AvoidWildcardsMap:
+    @threadUnsafe lazy val localParamRefs = util.HashSet[Type]()
+
+    def toAvoid(tp: NamedType): Boolean
+
+    /** True iff all NamedTypes on this prefix are static */
+    override def isStaticPrefix(pre: Type)(using Context): Boolean = pre match
+      case pre: NamedType =>
+        val sym = pre.currentSymbol
+        sym.is(Package) || sym.isStatic && isStaticPrefix(pre.prefix)
+      case _ => true
+
+    override def apply(tp: Type): Type = tp match
+      case tp: TermRef
+      if toAvoid(tp) =>
+        tp.info.widenExpr.dealias match {
+          case info: SingletonType => apply(info)
+          case info => range(defn.NothingType, apply(info))
+        }
+      case tp: TypeRef if toAvoid(tp) =>
+        tp.info match {
+          case info: AliasingBounds =>
+            apply(info.alias)
+          case TypeBounds(lo, hi) =>
+            range(atVariance(-variance)(apply(lo)), apply(hi))
+          case info: ClassInfo =>
+            range(defn.NothingType, apply(classBound(info)))
+          case _ =>
+            emptyRange // should happen only in error cases
+        }
+      case tp: ThisType =>
+        // ThisType is only used inside a class.
+        // Therefore, either they don't appear in the type to be avoided, or
+        // it must be a class that encloses the block whose type is to be avoided.
+        tp
+      case tp: LazyRef =>
+        if localParamRefs.contains(tp.ref) then tp
+        else if isExpandingBounds then emptyRange
+        else mapOver(tp)
+      case tl: HKTypeLambda =>
+        localParamRefs ++= tl.paramRefs
+        mapOver(tl)
+      case _ =>
+        super.apply(tp)
+    end apply
+
+    /** Three deviations from standard derivedSelect:
+     *   1. We first try a widening conversion to the type's info with
+     *      the original prefix. Since the original prefix is known to
+     *      be a subtype of the returned prefix, this can improve results.
+     *   2. Then, if the approximation result is a singleton reference C#x.type, we
+     *      replace by the widened type, which is usually more natural.
+     *   3. Finally, we need to handle the case where the prefix type does not have a member
+     *      named `tp.name` anymmore. In that case, we need to fall back to Bot..Top.
+     */
+    override def derivedSelect(tp: NamedType, pre: Type) =
+      if (pre eq tp.prefix)
+        tp
+      else tryWiden(tp, tp.prefix).orElse {
+        if (tp.isTerm && variance > 0 && !pre.isSingleton)
+          apply(tp.info.widenExpr)
+        else if (upper(pre).member(tp.name).exists)
+          super.derivedSelect(tp, pre)
+        else
+          range(defn.NothingType, defn.AnyType)
+      }
+  end AvoidMap
+
+  /** An upper approximation of the given type `tp` that does not refer to any symbol in `symsToAvoid`
+   *  and does not contain any WildcardType.
    *  We need to approximate with ranges:
    *
    *    term references to symbols in `symsToAvoid`,
    *    term references that have a widened type of which some part refers
    *    to a symbol in `symsToAvoid`,
    *    type references to symbols in `symsToAvoid`,
-   *    this types of classes in `symsToAvoid`.
    *
    *  Type variables that would be interpolated to a type that
    *  needs to be widened are replaced by the widened interpolation instance.
+   *
+   *  TODO: Could we replace some or all usages of this method by
+   *  `LevelAvoidMap` instead? It would be good to investigate this in details
+   *  but when I tried it, avoidance for inlined trees broke because `TreeMap`
+   *  does not update `ctx.nestingLevel` when entering a block so I'm leaving
+   *  this as Future Work™.
    */
   def avoid(tp: Type, symsToAvoid: => List[Symbol])(using Context): Type = {
-    val widenMap = new ApproximatingTypeMap {
+    val widenMap = new AvoidMap {
       @threadUnsafe lazy val forbidden = symsToAvoid.toSet
-      @threadUnsafe lazy val localParamRefs = util.HashSet[Type]()
-      def toAvoid(sym: Symbol) = !sym.isStatic && forbidden.contains(sym)
-      def partsToAvoid = new NamedPartsAccumulator(tp => toAvoid(tp.symbol))
-
-      /** True iff all NamedTypes on this prefix are static */
-      override def isStaticPrefix(pre: Type)(using Context): Boolean = pre match
-        case pre: NamedType =>
-          val sym = pre.currentSymbol
-          sym.is(Package) || sym.isStatic && isStaticPrefix(pre.prefix)
-        case _ => true
-
-      def apply(tp: Type): Type = tp match
-        case tp: TermRef
-        if toAvoid(tp.symbol) || partsToAvoid(Nil, tp.info).nonEmpty =>
-          tp.info.widenExpr.dealias match {
-            case info: SingletonType => apply(info)
-            case info => range(defn.NothingType, apply(info))
-          }
-        case tp: TypeRef if toAvoid(tp.symbol) =>
-          tp.info match {
-            case info: AliasingBounds =>
-              apply(info.alias)
-            case TypeBounds(lo, hi) =>
-              range(atVariance(-variance)(apply(lo)), apply(hi))
-            case info: ClassInfo =>
-              range(defn.NothingType, apply(classBound(info)))
-            case _ =>
-              emptyRange // should happen only in error cases
-          }
-        case tp: ThisType =>
-          // ThisType is only used inside a class.
-          // Therefore, either they don't appear in the type to be avoided, or
-          // it must be a class that encloses the block whose type is to be avoided.
-          tp
+      def toAvoid(tp: NamedType) =
+        val sym = tp.symbol
+        !sym.isStatic && forbidden.contains(sym)
+
+      override def apply(tp: Type): Type = tp match
         case tp: TypeVar if mapCtx.typerState.constraint.contains(tp) =>
           val lo = TypeComparer.instanceType(
             tp.origin, fromBelow = variance > 0 || variance == 0 && tp.hasLowerBound)(using mapCtx)
           val lo1 = apply(lo)
           if (lo1 ne lo) lo1 else tp
-        case tp: LazyRef =>
-          if localParamRefs.contains(tp.ref) then tp
-          else if isExpandingBounds then emptyRange
-          else mapOver(tp)
-        case tl: HKTypeLambda =>
-          localParamRefs ++= tl.paramRefs
-          mapOver(tl)
         case _ =>
-          mapOver(tp)
+          super.apply(tp)
       end apply
-
-      /** Three deviations from standard derivedSelect:
-       *   1. We first try a widening conversion to the type's info with
-       *      the original prefix. Since the original prefix is known to
-       *      be a subtype of the returned prefix, this can improve results.
-       *   2. Then, if the approximation result is a singleton reference C#x.type, we
-       *      replace by the widened type, which is usually more natural.
-       *   3. Finally, we need to handle the case where the prefix type does not have a member
-       *      named `tp.name` anymmore. In that case, we need to fall back to Bot..Top.
-       */
-      override def derivedSelect(tp: NamedType, pre: Type) =
-        if (pre eq tp.prefix)
-          tp
-        else tryWiden(tp, tp.prefix).orElse {
-          if (tp.isTerm && variance > 0 && !pre.isSingleton)
-            apply(tp.info.widenExpr)
-          else if (upper(pre).member(tp.name).exists)
-            super.derivedSelect(tp, pre)
-          else
-            range(defn.NothingType, defn.AnyType)
-        }
     }
 
     widenMap(tp)

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

@@ -4668,7 +4668,6 @@ object Types {
    *  @param  creatorState  The typer state in which the variable was created.
    */
   final class TypeVar private(initOrigin: TypeParamRef, creatorState: TyperState, val nestingLevel: Int) extends CachedProxyType with ValueType {
-
     private var currentOrigin = initOrigin
 
     def origin: TypeParamRef = currentOrigin
@@ -4709,38 +4708,6 @@ object Types {
     /** Is the variable already instantiated? */
     def isInstantiated(using Context): Boolean = instanceOpt.exists
 
-    /** Avoid term references in `tp` to parameters or local variables that
-     *  are nested more deeply than the type variable itself.
-     */
-    private def avoidCaptures(tp: Type)(using Context): Type =
-      if ctx.isAfterTyper then
-        return tp
-      val problemSyms = new TypeAccumulator[Set[Symbol]]:
-        def apply(syms: Set[Symbol], t: Type): Set[Symbol] = t match
-          case ref: NamedType
-          // AVOIDANCE TODO: Are there other problematic kinds of references?
-          // Our current tests only give us these, but we might need to generalize this.
-          if (ref.prefix eq NoPrefix) && ref.symbol.maybeOwner.nestingLevel > nestingLevel =>
-            syms + ref.symbol
-          case _ =>
-            foldOver(syms, t)
-      val problems = problemSyms(Set.empty, tp)
-      if problems.isEmpty then tp
-      else
-        val atp = TypeOps.avoid(tp, problems.toList)
-        def msg = i"Inaccessible variables captured in instantation of type variable $this.\n$tp was fixed to $atp"
-        typr.println(msg)
-        val bound = TypeComparer.fullUpperBound(origin)
-        if !(atp <:< bound) then
-          throw new TypeError(i"$msg,\nbut the latter type does not conform to the upper bound $bound")
-        atp
-      // AVOIDANCE TODO: This really works well only if variables are instantiated from below
-      // If we hit a problematic symbol while instantiating from above, then avoidance
-      // will widen the instance type further. This could yield an alias, which would be OK.
-      // But it also could yield a true super type which would then fail the bounds check
-      // and throw a TypeError. The right thing to do instead would be to avoid "downwards".
-      // To do this, we need first test cases for that situation.
-
     /** Instantiate variable with given type */
     def instantiateWith(tp: Type)(using Context): Type = {
       assert(tp ne this, i"self instantiation of $origin, constraint = ${ctx.typerState.constraint}")
@@ -4765,7 +4732,7 @@ object Types {
      *  is also a singleton type.
      */
     def instantiate(fromBelow: Boolean)(using Context): Type =
-      val tp = avoidCaptures(TypeComparer.instanceType(origin, fromBelow))
+      val tp = TypeComparer.instanceType(origin, fromBelow)
       if myInst.exists then // The line above might have triggered instantiation of the current type variable
         myInst
       else

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

@@ -447,7 +447,7 @@ object Inferencing {
    *  We need to take the occurences in `pt` into account because a type
    *  variable created when typing the current tree might only appear in the
    *  bounds of a type variable in the expected type, for example when
-   *  `ConstraintHandling#addOneBound` creates type variables when approximating
+   *  `ConstraintHandling#legalBound` creates type variables when approximating
    *  a bound.
    *
    *  Note: We intentionally use a relaxed version of variance here,

tests/neg/i8900.scala

@@ -0,0 +1,28 @@
+trait Base {
+  type M
+}
+trait A {
+  type M >: Int | String
+}
+trait B {
+  type M <: Int & String
+}
+object Test {
+  def foo[T](z: T, x: A & B => T): T = z
+  def foo2[T](z: T, x: T): T = z
+
+  def main(args: Array[String]): Unit = {
+    val x = foo(1, x => (??? : x.M))
+    val x1: String = x // error (was: ClassCastException)
+
+    val a = foo2(1,
+      if false then
+        val x: A & B = ???
+        ??? : x.M
+      else 1
+    )
+
+    val b: String = a // error (was: ClassCastException)
+  }
+}
+

tests/neg/i8861.scala renamed to tests/run/i8861.scala

@@ -18,14 +18,16 @@ object Test {
     int = vi => vi.i : vi.A,
     str = vs => vs.t : vs.A
   )
+  // Used to infer `c.visit[Int & M)]` and error out in the second lambda,
+  // 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  // error // error
+    str = vs => vs.t : vs.A
   )
 
   def main(args: Array[String]): Unit = {
     val e: Container { type A = String } = new StrV
     println(minimalOk(e)) // this one prints "hello"
-    println(minimalFail(e)) // this one fails with ClassCastException: class java.lang.String cannot be cast to class java.lang.Integer
+    println(minimalFail(e)) // used to fail with ClassCastException, now prints "hello"
   }
-}
+}