Put level checking under a config flag

Off by default

Author: odersky

compiler/src/dotty/tools/dotc/config/Config.scala

@@ -226,4 +226,10 @@ object Config {
    *  reduces the number of allocated denotations by ~50%.
    */
   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.
+   */
+  inline val checkLevels = false
 }

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

@@ -92,9 +92,10 @@ trait ConstraintHandling {
 
   /** 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.
+    level <= maxLevel
+    || ctx.isAfterTyper || !ctx.typerState.isCommittable // Leaks in these cases shouldn't break soundness
+    || level == Int.MaxValue // See `nestingLevel` above.
+    || !Config.checkLevels
 
   /** If `param` is nested deeper than `maxLevel`, try to instantiate it to a
    *  fresh type variable of level `maxLevel` and return the new variable.

tests/pos/i14494.scala

@@ -0,0 +1,6 @@
+object ImplNotFound:
+  def main(args: Array[String]): Unit =
+    val res: Seq[String | Int] = (??? : Seq[Int]).collect {
+      case 1 => Seq("")
+      case 2 => Seq(1)
+    }.flatten

tests/pos/i15178.scala

@@ -0,0 +1,17 @@
+// This should be a neg test once level checking is re-enabled.
+
+trait E[F[_]] {
+  type T
+  val value: F[T]
+}
+
+object E {
+  def apply[F[_], T1](value1: F[T1]) = new E[F] {
+    type T = T1
+    val value = value1
+  }
+}
+
+val a: Option[E[Ordering]] = Option(E(Ordering[Int]))
+val _ = a.map(it => E(it.value)) // there should be an error here
+

tests/pos/i15184.scala

@@ -0,0 +1,14 @@
+def test() = {
+  func(_ => Box(Seq.empty[String]) )
+}
+
+def func[R0](to0: Unit => R0): Unit = ???
+
+trait JsonFormat[T]
+object JsonFormat{
+  implicit def immSeqFormat: JsonFormat[Seq[String]]  = ???
+
+  implicit def iterableFormat: JsonFormat[Iterable[String]]   = ???
+}
+
+case class Box[A1: JsonFormat](elem: A1)

tests/pos/i15216.scala

@@ -0,0 +1,25 @@
+sealed abstract class Free[S[_], A] {
+  final def map[B](f: A => B): Free[S, B] = ???
+  final def flatMap[B](f: A => Free[S, B]): Free[S, B] = new Free[S, B] {}
+}
+
+trait Parameter[T]
+def namedDouble(name: String): Free[Parameter, Double] = ???
+
+type Double2 = (Double, Double)
+type Double3 = (Double, Double, Double)
+val spec: Free[Parameter, Either[Double3, Double2]] = for {
+  result <-
+    if (???) {
+      for {
+        x <- namedDouble("X")
+        y <- namedDouble("Y")
+        z <- namedDouble("Z")
+      } yield Left((x, y, z))
+    } else {
+      for {
+        x <- namedDouble("X")
+        y <- namedDouble("Y")
+      } yield Right((x, y))
+    }
+} yield result