From c7aea0e07e93f5498dbefed1e3aebdf9cc1ee980 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Tue, 7 Jul 2020 13:48:08 +0200 Subject: [PATCH 1/5] 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. --- .../dotty/tools/dotc/typer/Inferencing.scala | 60 ++++---- .../src/dotty/tools/dotc/typer/Typer.scala | 47 ++++-- .../neg/gadt-approximation-interaction.scala | 136 ++++++++++++++++++ .../boundspropagation.scala} | 0 tests/pos/{i7044.scala.ignore => i7044.scala} | 0 5 files changed, 207 insertions(+), 36 deletions(-) create mode 100644 tests/neg/gadt-approximation-interaction.scala rename tests/{pos/boundspropagation.scala.ignore => pending/boundspropagation.scala} (100%) rename tests/pos/{i7044.scala.ignore => i7044.scala} (100%) diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala index d21d61bb427c..491c8165f3a2 100644 --- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala +++ b/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(using 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)(using 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 diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 57095721628c..b2e65c1991d2 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/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 @@ -3407,16 +3407,16 @@ 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 "" } @@ -3424,8 +3424,8 @@ class Typer extends Namer """ ) 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 _ => ; } @@ -3455,10 +3455,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) @@ -3469,14 +3497,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) diff --git a/tests/neg/gadt-approximation-interaction.scala b/tests/neg/gadt-approximation-interaction.scala new file mode 100644 index 000000000000..4ece60c2533a --- /dev/null +++ b/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 + } + } +} diff --git a/tests/pos/boundspropagation.scala.ignore b/tests/pending/boundspropagation.scala similarity index 100% rename from tests/pos/boundspropagation.scala.ignore rename to tests/pending/boundspropagation.scala diff --git a/tests/pos/i7044.scala.ignore b/tests/pos/i7044.scala similarity index 100% rename from tests/pos/i7044.scala.ignore rename to tests/pos/i7044.scala From baaaa6cb732294421de8876950276065abee33e1 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Thu, 9 Jul 2020 11:34:51 +0200 Subject: [PATCH 2/5] Make i7044 typecheck with old version of recover --- .../dotty/tools/dotc/core/TypeComparer.scala | 2 +- .../dotty/tools/dotc/typer/Inferencing.scala | 10 +++--- .../src/dotty/tools/dotc/typer/Typer.scala | 31 ++----------------- 3 files changed, 9 insertions(+), 34 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index f0615f8afeda..c41ecd76dc27 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -751,7 +751,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w case _ => false } case _ => false - comparePaths || isNewSubType(tp1.underlying.widenExpr) + comparePaths || isSubType(tp1.underlying.widenExpr, tp2, approx.addLow) case tp1: RefinedType => isNewSubType(tp1.parent) case tp1: RecType => diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala index 491c8165f3a2..561243a75832 100644 --- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala +++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala @@ -198,10 +198,12 @@ object Inferencing { * - 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. + * - If we have A <: Option[B] and B <: Int, we approximate A ~~ + * Option[B]. That is, we don't recurse into already approximated + * types. Since GADT approximation is (for now) only used for member + * selection, this behaviour is expected, as nested types cannot affect + * member selection (note that given/extension lookup doesn't need GADT + * approx, see gadt-approximation-interaction.scala). */ def apply(tp: Type): Type = tp.dealias match { case tp @ TypeRef(qual, nme) if (qual eq NoPrefix) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index b2e65c1991d2..6001384e063e 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -3455,37 +3455,10 @@ class Typer extends Namer // try an implicit conversion val prevConstraint = ctx.typerState.constraint - 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 - } - + def recover(failure: SearchFailureType) = if (isFullyDefined(wtp, force = ForceDegree.all) && ctx.typerState.constraint.ne(prevConstraint)) readapt(tree) - 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) - } + 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 From 72916eaa070cb804c1855aebf5b2030cae314ad1 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Mon, 13 Jul 2020 10:28:52 +0200 Subject: [PATCH 3/5] Clean up adaptToSubType Add an explanatory comment and calculate GADT approx lazily. --- compiler/src/dotty/tools/dotc/typer/Typer.scala | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 6001384e063e..5f7d1b4162cf 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -3407,13 +3407,14 @@ class Typer extends Namer case _ => } - val gadtApprox = Inferencing.approximateGADT(wtp) + // try GADT approximation, but only if we're trying to select a member + // Member lookup cannot take GADTs into account b/c of cache, so we + // approximate types based on GADT constraints instead. For an example, + // see MemberHealing in gadt-approximation-interaction.scala. + lazy val gadtApprox = Inferencing.approximateGADT(wtp) gadts.println( i"""GADT 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(gadtApprox).toString From 089698125565ce5b4be38d4c23686068c879af49 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Mon, 13 Jul 2020 14:57:03 +0200 Subject: [PATCH 4/5] Adjust based on review feedback --- .../src/dotty/tools/dotc/typer/Typer.scala | 22 ++++++------------- 1 file changed, 7 insertions(+), 15 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 5f7d1b4162cf..65bcb940e557 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -3411,22 +3411,14 @@ class Typer extends Namer // Member lookup cannot take GADTs into account b/c of cache, so we // approximate types based on GADT constraints instead. For an example, // see MemberHealing in gadt-approximation-interaction.scala. - lazy val gadtApprox = Inferencing.approximateGADT(wtp) - gadts.println( - i"""GADT approximation { - approximation = $gadtApprox - pt.isMatchedBy = ${ - if (pt.isInstanceOf[SelectionProto]) - pt.asInstanceOf[SelectionProto].isMatchedBy(gadtApprox).toString - else - "" - } - } - """ - ) pt match { - case pt: SelectionProto if ctx.gadt.nonEmpty && pt.isMatchedBy(gadtApprox) => - return tpd.Typed(tree, TypeTree(gadtApprox)) + case pt: SelectionProto if ctx.gadt.nonEmpty => + gadts.println(i"Trying to heal member selection by GADT-approximating $wtp") + val gadtApprox = Inferencing.approximateGADT(wtp) + gadts.println(i"GADT-approximated $wtp ~~ $gadtApprox") + if pt.isMatchedBy(gadtApprox) then + gadts.println(i"Member selection healed by GADT approximation") + return tpd.Typed(tree, TypeTree(gadtApprox)) case _ => ; } From c43494959e5e4e05be3923155061abed89592b26 Mon Sep 17 00:00:00 2001 From: Aleksander Boruch-Gruszecki Date: Tue, 14 Jul 2020 13:46:11 +0200 Subject: [PATCH 5/5] Remove unnecessary tree attachment --- compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala index 75e9caef6c12..22e1d10cb02d 100644 --- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala +++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala @@ -687,14 +687,8 @@ object ProtoTypes { /** Dummy tree to be used as an argument of a FunProto or ViewProto type */ object dummyTreeOfType { - /* - * A property indicating that the given tree was created with dummyTreeOfType. - * It is sometimes necessary to detect the dummy trees to avoid unwanted readaptations on them. - */ - val IsDummyTree = new Property.Key[Unit] - def apply(tp: Type)(implicit src: SourceFile): Tree = - (untpd.Literal(Constant(null)) withTypeUnchecked tp).withAttachment(IsDummyTree, ()) + untpd.Literal(Constant(null)) withTypeUnchecked tp def unapply(tree: untpd.Tree): Option[Type] = tree match { case Literal(Constant(null)) => Some(tree.typeOpt) case _ => None