From 2317859414eaff4c992eb18012d9514bfc0f1d44 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 31 May 2022 18:19:26 +0200
Subject: [PATCH] Put level checking under a config flag

Off by default
---
 .../src/dotty/tools/dotc/config/Config.scala  |  6 +++++
 .../tools/dotc/core/ConstraintHandling.scala  |  7 +++---
 tests/pos/i14494.scala                        |  6 +++++
 tests/pos/i15178.scala                        | 17 +++++++++++++
 tests/pos/i15184.scala                        | 14 +++++++++++
 tests/pos/i15216.scala                        | 25 +++++++++++++++++++
 6 files changed, 72 insertions(+), 3 deletions(-)
 create mode 100644 tests/pos/i14494.scala
 create mode 100644 tests/pos/i15178.scala
 create mode 100644 tests/pos/i15184.scala
 create mode 100644 tests/pos/i15216.scala

diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala
index b9a8c96f49d9..0ea5089ed13c 100644
--- a/compiler/src/dotty/tools/dotc/config/Config.scala
+++ b/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
 }
diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 0fdaec68e826..6c9bd1bb6577 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/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.
diff --git a/tests/pos/i14494.scala b/tests/pos/i14494.scala
new file mode 100644
index 000000000000..33170dea035b
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/tests/pos/i15178.scala b/tests/pos/i15178.scala
new file mode 100644
index 000000000000..45dd90e6654b
--- /dev/null
+++ b/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
+
diff --git a/tests/pos/i15184.scala b/tests/pos/i15184.scala
new file mode 100644
index 000000000000..4a81eb9a6aeb
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/tests/pos/i15216.scala b/tests/pos/i15216.scala
new file mode 100644
index 000000000000..6150d3d93098
--- /dev/null
+++ b/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
\ No newline at end of file