From d03e62600f1a7772c5b9c265d1a2ad797b47351c Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 26 Jul 2022 11:37:56 +0200
Subject: [PATCH] Change Config flags

Introduce separate Config flags that enable level checking on constraints
or level checking on instantiation.
---
 compiler/src/dotty/tools/dotc/config/Config.scala | 11 +++++++----
 .../tools/dotc/core/ConstraintHandling.scala      | 15 +++++++++------
 .../dotty/tools/dotc/core/tasty/TreePickler.scala |  2 +-
 compiler/src/dotty/tools/dotc/typer/Namer.scala   |  2 +-
 4 files changed, 18 insertions(+), 12 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala
index 0ea5089ed13c..67545233136d 100644
--- a/compiler/src/dotty/tools/dotc/config/Config.scala
+++ b/compiler/src/dotty/tools/dotc/config/Config.scala
@@ -227,9 +227,12 @@ object Config {
    */
   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.
+  /** If `checkLevelsOnConstraints` is true, check levels of type variables
+   *  and create fresh ones as needed when bounds are first entered intot he constraint.
+   *  If `checkLevelsOnInstantiation` is true, allow level-incorrect constraints but
+   *  fix levels on type variable instantiation.
    */
-  inline val checkLevels = false
+  inline val checkLevelsOnConstraints = false
+  inline val checkLevelsOnInstantiation = true
+
 }
diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index d91d4f8fda8d..fa14348017b8 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -103,12 +103,15 @@ trait ConstraintHandling {
    *  of `1`. So the lower bound is `1 | x.M` and when we level-avoid that we
    *  get `1 | Int & String`, which simplifies to `Int`.
    */
-  protected var trustBounds = true
+  private var myTrustBounds = true
 
   inline def withUntrustedBounds(op: => Type): Type =
-    val saved = trustBounds
-    trustBounds = false
-    try op finally trustBounds = saved
+    val saved = myTrustBounds
+    myTrustBounds = false
+    try op finally myTrustBounds = saved
+
+  def trustBounds: Boolean =
+    !Config.checkLevelsOnInstantiation || myTrustBounds
 
   def checkReset() =
     assert(addConstraintInvocations == 0)
@@ -131,7 +134,7 @@ trait ConstraintHandling {
     level <= maxLevel
     || ctx.isAfterTyper || !ctx.typerState.isCommittable // Leaks in these cases shouldn't break soundness
     || level == Int.MaxValue // See `nestingLevel` above.
-    || !Config.checkLevels
+    || !Config.checkLevelsOnConstraints
 
   /** If `param` is nested deeper than `maxLevel`, try to instantiate it to a
    *  fresh type variable of level `maxLevel` and return the new variable.
@@ -518,7 +521,7 @@ trait ConstraintHandling {
       if !fromBelow then variance = -1
       def toAvoid(tp: NamedType) = needsFix(tp)
 
-    if ctx.isAfterTyper then tp
+    if !Config.checkLevelsOnInstantiation || ctx.isAfterTyper then tp
     else
       val needsLeveling = NeedsLeveling()
       if needsLeveling(false, tp) then
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index 8d80d69fdfa9..475a258e8330 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -206,7 +206,7 @@ class TreePickler(pickler: TastyPickler) {
       }
       else if (tpe.prefix == NoPrefix) {
         writeByte(if (tpe.isType) TYPEREFdirect else TERMREFdirect)
-        if Config.checkLevels && !symRefs.contains(sym) && !sym.isPatternBound && !sym.hasAnnotation(defn.QuotedRuntimePatterns_patternTypeAnnot) then
+        if Config.checkLevelsOnConstraints && !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 d3cf8308bf83..e6426cc54cd5 100644
--- a/compiler/src/dotty/tools/dotc/typer/Namer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala
@@ -1687,7 +1687,7 @@ class Namer { typer: Typer =>
             // Examples that fail otherwise are pos/scalaz-redux.scala and pos/java-futures.scala.
             // So fixing levels at instantiation avoids the soundness problem but apparently leads
             // to type inference problems since it comes too late.
-            if !Config.checkLevels then
+            if !Config.checkLevelsOnConstraints 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" +