wip

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