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 93364f0bccb5..75c728a5bb29 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/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index dd2cc46c406d..0c06c3ecaf04 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -15,6 +15,7 @@ import Comments.{Comment, CommentsContext}
 import NameKinds._
 import StdNames.nme
 import transform.SymUtils._
+import config.Config
 import collection.mutable
 import dotty.tools.tasty.TastyFormat.ASTsSection
 
@@ -85,6 +86,11 @@ class TreePickler(pickler: TastyPickler) {
     case Some(label) =>
       if (label != NoAddr) writeRef(label) else pickleForwardSymRef(sym)
     case None =>
+      // See pos/t1957.scala for an example where this can happen.
+      // I believe it's a bug in typer: the type of an implicit argument refers
+      // to a closure parameter outside the closure itself. TODO: track this down, so that we
+      // can eliminate this case.
+      report.log(i"pickling reference to as yet undefined $sym in ${sym.owner}", sym.srcPos)
       pickleForwardSymRef(sym)
   }
 
@@ -197,7 +203,7 @@ class TreePickler(pickler: TastyPickler) {
       }
       else if (tpe.prefix == NoPrefix) {
         writeByte(if (tpe.isType) TYPEREFdirect else TERMREFdirect)
-        if !symRefs.contains(sym) && !sym.isPatternBound && !sym.hasAnnotation(defn.QuotedRuntimePatterns_patternTypeAnnot) then
+        if Config.checkLevels && !symRefs.contains(sym) && !sym.isPatternBound && !sym.hasAnnotation(defn.QuotedRuntimePatterns_patternTypeAnnot) then
           report.error(i"pickling reference to as yet undefined $tpe with symbol ${sym}", sym.srcPos)
         pickleSymRef(sym)
       }
diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala
index a442f2b23999..c47ed9e7d6f8 100644
--- a/compiler/src/dotty/tools/dotc/typer/Namer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala
@@ -1534,7 +1534,23 @@ class Namer { typer: Typer =>
             // This case applies if the closure result type contains uninstantiated
             // type variables. In this case, constrain the closure result from below
             // by the parameter-capture-avoiding type of the body.
-            typedAheadExpr(mdef.rhs, tpt.tpe).tpe
+            val rhsType = typedAheadExpr(mdef.rhs, tpt.tpe).tpe
+
+            // The following part is important since otherwise we might instantiate
+            // the closure result type with a plain functon type that refers
+            // to local parameters. An example where this happens in `dependent-closures.scala`
+            // If the code after `val rhsType` is commented out, this file fails pickling tests.
+            // AVOIDANCE TODO: Follow up why this happens, and whether there
+            // are better ways to achieve this. It would be good if we could get rid of this code.
+            // It seems at least partially redundant with the nesting level checking on TypeVar
+            // instantiation.
+            if !Config.checkLevels then
+              val hygienicType = TypeOps.avoid(rhsType, termParamss.flatten)
+              if (!hygienicType.isValueType || !(hygienicType <:< tpt.tpe))
+                report.error(i"return type ${tpt.tpe} of lambda cannot be made hygienic;\n" +
+                  i"it is not a supertype of the hygienic type $hygienicType", mdef.srcPos)
+            //println(i"lifting $rhsType over $termParamss -> $hygienicType = ${tpt.tpe}")
+            //println(TypeComparer.explained { implicit ctx => hygienicType <:< tpt.tpe })
           case _ =>
         }
         WildcardType
diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist
index b099805a139f..a42b3c59fd99 100644
--- a/compiler/test/dotc/pos-test-pickling.blacklist
+++ b/compiler/test/dotc/pos-test-pickling.blacklist
@@ -81,3 +81,6 @@ i4176-gadt.scala
 i13974a.scala
 
 java-inherited-type1
+
+# avoidance bug
+i15174.scala
\ No newline at end of file
diff --git a/tests/neg/i8900.scala b/tests/pending/neg/i8900.scala
similarity index 100%
rename from tests/neg/i8900.scala
rename to tests/pending/neg/i8900.scala
diff --git a/tests/run-macros/i7519c/Macro_1.scala b/tests/pending/run-macros/i7519c/Macro_1.scala
similarity index 100%
rename from tests/run-macros/i7519c/Macro_1.scala
rename to tests/pending/run-macros/i7519c/Macro_1.scala
diff --git a/tests/run-macros/i7519c/Test_2.scala b/tests/pending/run-macros/i7519c/Test_2.scala
similarity index 100%
rename from tests/run-macros/i7519c/Test_2.scala
rename to tests/pending/run-macros/i7519c/Test_2.scala
diff --git a/tests/run/i8861.scala b/tests/pending/run/i8861.scala
similarity index 100%
rename from tests/run/i8861.scala
rename to tests/pending/run/i8861.scala
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