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

@@ -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
+
 }

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

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)
       }

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" +