Fix ApproximateGadtAccumulator

Explanations are in the relevant doc.

Provisionally restored GADT-approximating version of `recover` in
`adaptToSubType`, as it turns out to be necessary to typecheck i7044.scala.

Moved boundspropagation.scala to pending.
Originally, ApproximateGadtAccumulator allowed it to typecheck, so it
was added as a test. Since `recover` was provisionally restored, the
test succeeds again. However, as GADT approximation is only meant to fix
GADT member selection issues and the example does not involve those,
we probably don't want it as a pos test. At the same time, it should
typecheck, so we shouldn't delete it either.

Author: abgruszecki

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

@@ -11,7 +11,7 @@ import NameKinds.UniqueName
 import util.Spans._
 import util.{Stats, SimpleIdentityMap}
 import Decorators._
-import config.Printers.{gadts, typr}
+import config.Printers.{gadts, typr, debug}
 import annotation.tailrec
 import reporting._
 import collection.mutable
@@ -171,37 +171,45 @@ object Inferencing {
     res
   }
 
-  /** This class is mostly based on IsFullyDefinedAccumulator.
-    * It tries to approximate the given type based on the available GADT constraints.
-    */
+  /** Approximates a type to get rid of as many GADT-constrained abstract types as possible. */
   private class ApproximateGadtAccumulator(implicit ctx: Context) extends TypeMap {
 
     var failed = false
 
-    private def instantiate(tvar: TypeVar, fromBelow: Boolean): Type = {
-      val inst = tvar.instantiate(fromBelow)
-      typr.println(i"forced instantiation of ${tvar.origin} = $inst")
-      inst
-    }
-
-    private def instDirection2(sym: Symbol)(implicit ctx: Context): Int = {
-      val constrained = ctx.gadt.fullBounds(sym)
-      val original = sym.info.bounds
-      val cmp = ctx.typeComparer
-      val approxBelow =
-        if (!cmp.isSubTypeWhenFrozen(constrained.lo, original.lo)) 1 else 0
-      val approxAbove =
-        if (!cmp.isSubTypeWhenFrozen(original.hi, constrained.hi)) 1 else 0
-      approxAbove - approxBelow
-    }
-
-    private[this] var toMaximize: Boolean = false
-
+    /** GADT approximation proceeds differently from type variable approximation.
+      *
+      * Essentially, what we're doing is we're inferring a type ascription that
+      * will remove as many GADT-constrained types as possible. This means that
+      * we want to approximate type T to type S in such a way that no matter how
+      * GADT-constrained types are instantiated, T <: S. In other words, the
+      * relationship _necessarily_ must hold.
+      *
+      * We accomplish that by:
+      *   - replacing covariant occurences with upper GADT bound
+      *   - replacing contravariant occurences with lower GADT bound
+      *   - leaving invariant occurences alone
+      *
+      * Examples:
+      *   - If we have GADT cstr A <: Int, then for all A <: Int, Option[A] <: Option[Int].
+      *     Therefore, we can approximate Option[A] ~~ Option[Int].
+      *   - If we have A >: S <: T, then for all such A, A => A <: S => T. This
+      *     illustrates that it's fine to differently approximate different
+      *     occurences of same type.
+      *   - If we have A <: Int and F <: [A] => Option[A] (note the invariance),
+      *     then we should approximate F[A] ~~ Option[A]. That is, we should
+      *     respect the invariance of the type constructor.
+      *   - If we have A <: Option[B] and B <: Int, we approximate A ~~ Option[Int].
+      *     That is, we recursively approximate all nested GADT-constrained types.
+      *     This is certain to be sound (because we maintain necessary subtyping),
+      *     but not accurate.
+      */
     def apply(tp: Type): Type = tp.dealias match {
-      case tp @ TypeRef(qual, nme) if (qual eq NoPrefix) && ctx.gadt.contains(tp.symbol) =>
+      case tp @ TypeRef(qual, nme) if (qual eq NoPrefix)
+                                   && variance != 0
+                                   && ctx.gadt.contains(tp.symbol)
+                                   =>
         val sym = tp.symbol
-        val res =
-          ctx.gadt.approximation(sym, fromBelow = variance < 0)
+        val res = ctx.gadt.approximation(sym, fromBelow = variance < 0)
         gadts.println(i"approximated $tp  ~~  $res")
         res
 

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

@@ -33,7 +33,7 @@ import collection.mutable
 import annotation.tailrec
 import Implicits._
 import util.Stats.record
-import config.Printers.{gadts, typr}
+import config.Printers.{gadts, typr, debug}
 import config.Feature._
 import config.SourceVersion._
 import rewrites.Rewrites.patch
@@ -3410,25 +3410,25 @@ class Typer extends Namer
         case _ =>
       }
 
-      val approximation = Inferencing.approximateGADT(wtp)
+      val gadtApprox = Inferencing.approximateGADT(wtp)
       gadts.println(
         i"""GADT approximation {
-        approximation = $approximation
+        approximation = $gadtApprox
         pt.isInstanceOf[SelectionProto] = ${pt.isInstanceOf[SelectionProto]}
         ctx.gadt.nonEmpty = ${ctx.gadt.nonEmpty}
         ctx.gadt = ${ctx.gadt.debugBoundsDescription}
         pt.isMatchedBy = ${
           if (pt.isInstanceOf[SelectionProto])
-            pt.asInstanceOf[SelectionProto].isMatchedBy(approximation).toString
+            pt.asInstanceOf[SelectionProto].isMatchedBy(gadtApprox).toString
           else
             "<not a SelectionProto>"
         }
         }
         """
       )
       pt match {
-        case pt: SelectionProto if ctx.gadt.nonEmpty && pt.isMatchedBy(approximation) =>
-          return tpd.Typed(tree, TypeTree(approximation))
+        case pt: SelectionProto if ctx.gadt.nonEmpty && pt.isMatchedBy(gadtApprox) =>
+          return tpd.Typed(tree, TypeTree(gadtApprox))
         case _ => ;
       }
 
@@ -3458,10 +3458,38 @@ class Typer extends Namer
 
       // try an implicit conversion
       val prevConstraint = ctx.typerState.constraint
-      def recover(failure: SearchFailureType) =
+      def recover(failure: SearchFailureType) = {
+        def canTryGADTHealing: Boolean = {
+          def isDummy = tree.hasAttachment(dummyTreeOfType.IsDummyTree)
+          tryGadtHealing // allow GADT healing only once to avoid a loop
+          && ctx.gadt.nonEmpty // GADT healing only makes sense if there are GADT constraints present
+          && !isDummy // avoid healing a dummy tree as it can lead to an error in a very specific case
+        }
+
         if (isFullyDefined(wtp, force = ForceDegree.all) &&
             ctx.typerState.constraint.ne(prevConstraint)) readapt(tree)
-        else err.typeMismatch(tree, pt, failure)
+        else if (canTryGADTHealing) {
+          // try recovering with a GADT approximation
+          // note: this seems be be important only in a very specific case
+          // where we select a member from so
+          val nestedCtx = ctx.fresh.setNewTyperState()
+          val ascribed = tpd.Typed(tree, TypeTree(gadtApprox))
+          val res =
+            readapt(
+              tree = ascribed,
+              shouldTryGadtHealing = false,
+            )(using nestedCtx)
+          if (!nestedCtx.reporter.hasErrors) {
+            // GADT recovery successful
+            nestedCtx.typerState.commit()
+            res
+          } else {
+            // otherwise fail with the error that would have been reported without the GADT recovery
+            err.typeMismatch(tree, pt, failure)
+          }
+        } else err.typeMismatch(tree, pt, failure)
+      }
+
       if ctx.mode.is(Mode.ImplicitsEnabled) && tree.typeOpt.isValueType then
         if pt.isRef(defn.AnyValClass) || pt.isRef(defn.ObjectClass) then
           ctx.error(em"the result of an implicit conversion must be more specific than $pt", tree.sourcePos)
@@ -3472,14 +3500,13 @@ class Typer extends Namer
             checkImplicitConversionUseOK(found.symbol, tree.posd)
             readapt(found)(using ctx.retractMode(Mode.ImplicitsEnabled))
           case failure: SearchFailure =>
-            if (pt.isInstanceOf[ProtoType] && !failure.isAmbiguous) {
+            if (pt.isInstanceOf[ProtoType] && !failure.isAmbiguous) then
               // don't report the failure but return the tree unchanged. This
               // will cause a failure at the next level out, which usually gives
               // a better error message. To compensate, store the encountered failure
               // as an attachment, so that it can be reported later as an addendum.
               rememberSearchFailure(tree, failure)
               tree
-            }
             else recover(failure.reason)
         }
       else recover(NoMatchingImplicits)

tests/neg/gadt-approximation-interaction.scala

@@ -0,0 +1,136 @@
+object MemberHealing {
+  enum SUB[-A, +B]:
+    case Refl[S]() extends SUB[S, S]
+
+  def foo[T](t: T, ev: T SUB Int) =
+    ev match { case SUB.Refl() =>
+      t + 2
+    }
+}
+
+object ImplicitLookup {
+  enum SUB[-A, +B]:
+    case Refl[S]() extends SUB[S, S]
+
+  class Tag[T]
+
+  implicit val ti: Tag[Int] = Tag()
+
+  def foo[T](t: T, ev: T SUB Int) =
+    ev match { case SUB.Refl() =>
+      implicitly[Tag[Int]]
+    }
+}
+
+object GivenLookup {
+  enum SUB[-A, +B]:
+    case Refl[S]() extends SUB[S, S]
+
+  class Tag[T]
+
+  given ti as Tag[Int]
+
+  def foo[T](t: T, ev: T SUB Int) =
+    ev match { case SUB.Refl() =>
+      summon[Tag[Int]]
+    }
+}
+
+object ImplicitConversion {
+  enum SUB[-A, +B]:
+    case Refl[S]() extends SUB[S, S]
+
+  class Pow(self: Int):
+    def **(other: Int): Int = math.pow(self, other).toInt
+
+  implicit def pow(i: Int): Pow = Pow(i)
+
+  def foo[T](t: T, ev: T SUB Int) =
+    ev match { case SUB.Refl() =>
+      t ** 2 // error // implementation limitation
+    }
+
+  def bar[T](t: T, ev: T SUB Int) =
+    ev match { case SUB.Refl() =>
+      (t: Int) ** 2 // sanity check
+    }
+}
+
+object GivenConversion {
+  enum SUB[-A, +B]:
+    case Refl[S]() extends SUB[S, S]
+
+  class Pow(self: Int):
+    def **(other: Int): Int = math.pow(self, other).toInt
+
+  given as Conversion[Int, Pow] = (i: Int) => Pow(i)
+
+  def foo[T](t: T, ev: T SUB Int) =
+    ev match { case SUB.Refl() =>
+      t ** 2 // error (implementation limitation)
+    }
+
+  def bar[T](t: T, ev: T SUB Int) =
+    ev match { case SUB.Refl() =>
+      (t: Int) ** 2 // sanity check
+    }
+}
+
+object ExtensionMethod {
+  enum SUB[-A, +B]:
+    case Refl[S]() extends SUB[S, S]
+
+  extension (x: Int):
+    def **(y: Int) = math.pow(x, y).toInt
+
+  def foo[T](t: T, ev: T SUB Int) =
+    ev match { case SUB.Refl() =>
+      t ** 2
+    }
+}
+
+object HKFun {
+  enum SUB[-A, +B]:
+    case Refl[S]() extends SUB[S, S]
+
+  enum HKSUB[-F[_], +G[_]]:
+    case Refl[H[_]]() extends HKSUB[H, H]
+
+  def foo[F[_], T](ft: F[T], hkev: F HKSUB Option, ev: T SUB Int) =
+    hkev match { case HKSUB.Refl() =>
+      ev match { case SUB.Refl() =>
+        // both should typecheck - we should respect invariance of F
+        // (and not approximate its argument)
+        // but also T <: Int b/c of ev
+        val x: T   = ft.get
+        val y: Int = ft.get
+      }
+    }
+
+  enum COVHKSUB[-F[+_], +G[+_]]:
+    case Refl[H[_]]() extends COVHKSUB[H, H]
+
+  def bar[F[+_], T](ft: F[T], hkev: F COVHKSUB Option, ev: T SUB Int) =
+    hkev match { case COVHKSUB.Refl() =>
+      ev match { case SUB.Refl() =>
+        // Sanity check for `foo`
+        // this is an error only because we blindly approximate covariant type arguments
+        // if it stops being an error, `foo` should be re-thought
+        val x: T   = ft.get // error
+        val y: Int = ft.get
+      }
+    }
+}
+
+object NestedConstrained {
+  enum SUB[-A, +B]:
+    case Refl[S]() extends SUB[S, S]
+
+  def foo[A, B](a: A, ev1: A SUB Option[B], ev2: B SUB Int) =
+    ev1 match { case SUB.Refl() =>
+      ev2 match { case SUB.Refl() =>
+        1 + "a"
+        a.get : Int
+      }
+    }
+}