Merge pull request #12773 from dotty-staging/one-instantiation-3

More careful instantiation of type variables

Author: odersky

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

@@ -24,7 +24,10 @@ object Config {
   inline val checkConstraintsNonCyclic = false
 
   /** Check that each constraint resulting from a subtype test
-   *  is satisfiable.
+   *  is satisfiable. Also check that a type variable instantiation
+   *  satisfies its constraints.
+   *  Note that this can fail when bad bounds are in scope, like in
+   *  tests/neg/i4721a.scala.
    */
   inline val checkConstraintsSatisfiable = false
 

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

@@ -300,8 +300,15 @@ trait ConstraintHandling {
         dropped = dropped.tail
         recur(tp)
 
+    val saved = ctx.typerState.snapshot()
     val tpw = recur(tp)
-    if (tpw eq tp) || dropped.forall(_ frozen_<:< tpw) then tp else tpw
+    if (tpw eq tp) || dropped.forall(_ frozen_<:< tpw) then
+      // Rollback any constraint change that would lead to `tp` no longer
+      // being a valid solution.
+      ctx.typerState.resetTo(saved)
+      tp
+    else
+      tpw
   end dropTransparentTraits
 
   /** If `tp` is an applied match type alias which is also an unreducible application

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

@@ -170,6 +170,10 @@ object TypeOps:
         if (normed.exists) normed else mapOver
       case tp: MethodicType =>
         tp // See documentation of `Types#simplified`
+      case tp: SkolemType =>
+        // Mapping over a skolem creates a new skolem which by definition won't
+        // be =:= to the original one.
+        tp
       case _ =>
         mapOver
     }

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

@@ -4479,8 +4479,14 @@ object Types {
 
     /** Instantiate variable with given type */
     def instantiateWith(tp: Type)(using Context): Type = {
-      assert(tp ne this, s"self instantiation of ${tp.show}, constraint = ${ctx.typerState.constraint.show}")
-      typr.println(s"instantiating ${this.show} with ${tp.show}")
+      assert(tp ne this, i"self instantiation of $origin, constraint = ${ctx.typerState.constraint}")
+      assert(!myInst.exists, i"$origin is already instantiated to $myInst but we attempted to instantiate it to $tp")
+      typr.println(i"instantiating $this with $tp")
+
+      if Config.checkConstraintsSatisfiable then
+        assert(currentEntry.bounds.contains(tp),
+          i"$origin is constrained to be $currentEntry but attempted to instantiate it to $tp")
+
       if ((ctx.typerState eq owningState.get) && !TypeComparer.subtypeCheckInProgress)
         setInst(tp)
       ctx.typerState.constraint = ctx.typerState.constraint.replace(origin, tp)
@@ -4495,7 +4501,11 @@ object Types {
      *  is also a singleton type.
      */
     def instantiate(fromBelow: Boolean)(using Context): Type =
-      instantiateWith(avoidCaptures(TypeComparer.instanceType(origin, fromBelow)))
+      val tp = avoidCaptures(TypeComparer.instanceType(origin, fromBelow))
+      if myInst.exists then // The line above might have triggered instantiation of the current type variable
+        myInst
+      else
+        instantiateWith(tp)
 
     /** For uninstantiated type variables: the entry in the constraint (either bounds or
      *  provisional instance value)

compiler/src/dotty/tools/dotc/typer/Inferencing.scala

@@ -403,20 +403,21 @@ object Inferencing {
     val vs = variances(tp)
     val patternBindings = new mutable.ListBuffer[(Symbol, TypeParamRef)]
     vs foreachBinding { (tvar, v) =>
-      if (v == 1) tvar.instantiate(fromBelow = false)
-      else if (v == -1) tvar.instantiate(fromBelow = true)
-      else {
-        val bounds = TypeComparer.fullBounds(tvar.origin)
-        if (bounds.hi <:< bounds.lo || bounds.hi.classSymbol.is(Final) || fromScala2x)
-          tvar.instantiate(fromBelow = false)
+      if !tvar.isInstantiated then
+        if (v == 1) tvar.instantiate(fromBelow = false)
+        else if (v == -1) tvar.instantiate(fromBelow = true)
         else {
-          // We do not add the created symbols to GADT constraint immediately, since they may have inter-dependencies.
-          // Instead, we simultaneously add them later on.
-          val wildCard = newPatternBoundSymbol(UniqueName.fresh(tvar.origin.paramName), bounds, span, addToGadt = false)
-          tvar.instantiateWith(wildCard.typeRef)
-          patternBindings += ((wildCard, tvar.origin))
+          val bounds = TypeComparer.fullBounds(tvar.origin)
+          if (bounds.hi <:< bounds.lo || bounds.hi.classSymbol.is(Final) || fromScala2x)
+            tvar.instantiate(fromBelow = false)
+          else {
+            // We do not add the created symbols to GADT constraint immediately, since they may have inter-dependencies.
+            // Instead, we simultaneously add them later on.
+            val wildCard = newPatternBoundSymbol(UniqueName.fresh(tvar.origin.paramName), bounds, span, addToGadt = false)
+            tvar.instantiateWith(wildCard.typeRef)
+            patternBindings += ((wildCard, tvar.origin))
+          }
         }
-      }
     }
     val res = patternBindings.toList.map { (boundSym, _) =>
       // substitute bounds of pattern bound variables to deal with possible F-bounds
@@ -654,13 +655,16 @@ trait Inferencing { this: Typer =>
             while buf.nonEmpty do
               val first @ (tvar, fromBelow) = buf.head
               buf.dropInPlace(1)
-              val suspend = buf.exists{ (following, _) =>
-                if fromBelow then
-                  constraint.isLess(following.origin, tvar.origin)
-                else
-                  constraint.isLess(tvar.origin, following.origin)
-              }
-              if suspend then suspended += first else tvar.instantiate(fromBelow)
+              if !tvar.isInstantiated then
+                val suspend = buf.exists{ (following, _) =>
+                  if fromBelow then
+                    constraint.isLess(following.origin, tvar.origin)
+                  else
+                    constraint.isLess(tvar.origin, following.origin)
+                }
+                if suspend then suspended += first else tvar.instantiate(fromBelow)
+              end if
+            end while
             doInstantiate(suspended)
         end doInstantiate
         doInstantiate(toInstantiate)

tests/neg/transparent-trait.scala

@@ -0,0 +1,11 @@
+transparent trait A
+transparent trait B
+trait C
+
+object Test:
+  val x = identity(new A with B) // infers A with B (because there's no non-transparent trait in the intersection)
+  val x2: A with B = x // OK
+
+  val y = identity(new A with B with C) // infers C
+  val y2: C = y // OK
+  val y3: A with B = y // error