Skip to content

Fix #7044: Approximate GADT bounds to avoid explicit type ascriptions #8728

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
May 12, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@ sealed abstract class GadtConstraint extends Showable {
def contains(sym: Symbol)(implicit ctx: Context): Boolean

def isEmpty: Boolean
final def nonEmpty: Boolean = !isEmpty

/** See [[ConstraintHandling.approximation]] */
def approximation(sym: Symbol, fromBelow: Boolean)(implicit ctx: Context): Type
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/transform/Erasure.scala
Original file line number Diff line number Diff line change
Expand Up @@ -954,7 +954,7 @@ object Erasure {
(stats2.filter(!_.isEmpty), finalCtx)
}

override def adapt(tree: Tree, pt: Type, locked: TypeVars)(using Context): Tree =
override def adapt(tree: Tree, pt: Type, locked: TypeVars, tryGadtHealing: Boolean)(using Context): Tree =
trace(i"adapting ${tree.showSummary}: ${tree.tpe} to $pt", show = true) {
if ctx.phase != ctx.erasurePhase && ctx.phase != ctx.erasurePhase.next then
// this can happen when reading annotations loaded during erasure,
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
Original file line number Diff line number Diff line change
Expand Up @@ -511,7 +511,7 @@ class TreeChecker extends Phase with SymTransformer {
override def ensureNoLocalRefs(tree: Tree, pt: Type, localSyms: => List[Symbol])(using Context): Tree =
tree

override def adapt(tree: Tree, pt: Type, locked: TypeVars)(using Context): Tree = {
override def adapt(tree: Tree, pt: Type, locked: TypeVars, tryGadtHealing: Boolean)(using Context): Tree = {
def isPrimaryConstructorReturn =
ctx.owner.isPrimaryConstructor && pt.isRef(ctx.owner.owner) && tree.tpe.isRef(defn.UnitClass)
def infoStr(tp: Type) = tp match {
Expand Down
56 changes: 56 additions & 0 deletions compiler/src/dotty/tools/dotc/typer/Inferencing.scala
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@ import collection.mutable
import scala.annotation.internal.sharable
import scala.annotation.threadUnsafe

import config.Printers.gadts

object Inferencing {

import tpd._
Expand Down Expand Up @@ -162,6 +164,60 @@ object Inferencing {
)
}

def approximateGADT(tp: Type)(implicit ctx: Context): Type = {
val map = new ApproximateGadtAccumulator
val res = map(tp)
assert(!map.failed)
res
}

/** This class is mostly based on IsFullyDefinedAccumulator.
* It tries to approximate the given type based on the available GADT constraints.
*/
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

def apply(tp: Type): Type = tp.dealias match {
case tp @ TypeRef(qual, nme) if (qual eq NoPrefix) && ctx.gadt.contains(tp.symbol) =>
val sym = tp.symbol
val res =
ctx.gadt.approximation(sym, fromBelow = variance < 0)
gadts.println(i"approximated $tp ~~ $res")
res

case _: WildcardType | _: ProtoType =>
failed = true
NoType

case tp =>
mapOver(tp)
}

def process(tp: Type): Type = {
apply(tp)
}
}

/** For all type parameters occurring in `tp`:
* If the bounds of `tp` in the current constraint are equal wrt =:=,
* instantiate the type parameter to the lower bound's approximation
Expand Down
10 changes: 9 additions & 1 deletion compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ import Decorators._
import Uniques._
import config.Printers.typr
import util.SourceFile
import util.Property

import scala.annotation.internal.sharable

Expand Down Expand Up @@ -684,7 +685,14 @@ object ProtoTypes {

/** Dummy tree to be used as an argument of a FunProto or ViewProto type */
object dummyTreeOfType {
def apply(tp: Type)(implicit src: SourceFile): Tree = untpd.Literal(Constant(null)) withTypeUnchecked tp
/*
* 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, ())
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we should introduce a proper internal construct for these trees. Maybe have a scala.internal.bla.dummyTree[T] .

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same for the unapply

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can improve on this later.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@nicolasstucki can you elaborate on what scala.internal.bla.dummyTree[T] should be? Some sort of special fictional value? I think creating a special Tree subclass for this purpose would work.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@smarter it turned out that it was dummyTreeOfType that was the source of the null we talked about. Could you chime in with an opinion on whether it ever makes sense to adapt dummy trees created by this function?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

honestly no clue, I myself only learned about dummyTreeOfType recently.

def unapply(tree: untpd.Tree): Option[Type] = tree match {
case Literal(Constant(null)) => Some(tree.typeOpt)
case _ => None
Expand Down
62 changes: 54 additions & 8 deletions compiler/src/dotty/tools/dotc/typer/Typer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2771,20 +2771,21 @@ class Typer extends Namer
* If all this fails, error
* Parameters as for `typedUnadapted`.
*/
def adapt(tree: Tree, pt: Type, locked: TypeVars)(using Context): Tree =
trace(i"adapting $tree to $pt", typr, show = true) {
def adapt(tree: Tree, pt: Type, locked: TypeVars, tryGadtHealing: Boolean = true)(using Context): Tree = {
trace(i"adapting $tree to $pt ${if (tryGadtHealing) "" else "(tryGadtHealing=false)" }\n", typr, show = true) {
record("adapt")
adapt1(tree, pt, locked)
adapt1(tree, pt, locked, tryGadtHealing)
}
}

final def adapt(tree: Tree, pt: Type)(using Context): Tree =
adapt(tree, pt, ctx.typerState.ownedVars)

private def adapt1(tree: Tree, pt: Type, locked: TypeVars)(using Context): Tree = {
private def adapt1(tree: Tree, pt: Type, locked: TypeVars, tryGadtHealing: Boolean)(using Context): Tree = {
assert(pt.exists && !pt.isInstanceOf[ExprType] || ctx.reporter.errorsReported)
def methodStr = err.refStr(methPart(tree).tpe)

def readapt(tree: Tree)(using Context) = adapt(tree, pt, locked)
def readapt(tree: Tree, shouldTryGadtHealing: Boolean = tryGadtHealing)(using Context) = adapt(tree, pt, locked, shouldTryGadtHealing)
def readaptSimplified(tree: Tree)(using Context) = readapt(simplify(tree, pt, locked))

def missingArgs(mt: MethodType) = {
Expand Down Expand Up @@ -3244,7 +3245,6 @@ class Typer extends Namer
if (folded ne tree)
return adaptConstant(folded, folded.tpe.asInstanceOf[ConstantType])

// Try to capture wildcards in type
val captured = captureWildcards(wtp)
if (captured `ne` wtp)
return readapt(tree.cast(captured))
Expand Down Expand Up @@ -3275,6 +3275,28 @@ class Typer extends Namer
case _ =>
}

val approximation = Inferencing.approximateGADT(wtp)
gadts.println(
i"""GADT approximation {
approximation = $approximation
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
else
"<not a SelectionProto>"
}
}
"""
)
pt match {
case pt: SelectionProto if ctx.gadt.nonEmpty && pt.isMatchedBy(approximation) =>
return tpd.Typed(tree, TypeTree(approximation))
case _ => ;
}

// try an extension method in scope
pt match {
case SelectionProto(name, mbrType, _, _) =>
Expand All @@ -3299,10 +3321,34 @@ class Typer extends Namer

// try an implicit conversion
val prevConstraint = ctx.typerState.constraint
def recover(failure: SearchFailureType) =
def recover(failure: SearchFailureType) = {
def canTryGADTHealing: Boolean = {
val 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
val nestedCtx = ctx.fresh.setNewTyperState()
val res =
readapt(
tree = tpd.Typed(tree, TypeTree(Inferencing.approximateGADT(wtp))),
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)
Expand Down
13 changes: 0 additions & 13 deletions tests/neg/boundspropagation.scala
Original file line number Diff line number Diff line change
Expand Up @@ -25,19 +25,6 @@ object test3 {
}
}

// Example contributed by Jason.
Copy link
Contributor Author

@radeusgd radeusgd Apr 15, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This test has been removed as we discussed with @AleksanderBG and we think it is correct for it to actually compile.

My reasoning is following:
we have y: Tree[S, T] where Nothing <: S, Option[Nothing] <: Option[S] <: T
we ascribe y: Tree[Nothing, Option[Nothing]]

  • we can do that because:
    Nothing <: S, Option[Nothing] <: T so Tree[S, T] <: Tree[Nothing, Option[Nothing]]
    (because Tree is contravariant in both its parameters)

we want y to conform to Tree[A,B] where B <: Option[N], as Option[Nothing] <: Option[N], it typechecks

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this be re added as a pos test?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed, I have added it.

object test4 {
class Base {
type N

class Tree[-S, -T >: Option[S]]

def g(x: Any): Tree[_, _ <: Option[N]] = x match {
case y: Tree[_, _] => y // error -- used to work (because of capture conversion?)
}
}
}

class Test5 {
"": ({ type U = this.type })#U // error
}
13 changes: 13 additions & 0 deletions tests/pos/boundspropagation.scala
Original file line number Diff line number Diff line change
Expand Up @@ -29,3 +29,16 @@ object test2 {
}
}
*/

// Example contributed by Jason.
object test2 {
class Base {
type N

class Tree[-S, -T >: Option[S]]

def g(x: Any): Tree[_, _ <: Option[N]] = x match {
case y: Tree[_, _] => y
}
}
}
15 changes: 15 additions & 0 deletions tests/pos/gadt-infer-ascription.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// test based on an example code by @Blaisorblade
object GadtAscription {
enum Var[G, A] {
case Z[G, A]() extends Var[(A, G), A]
case S[G, A, B](x: Var[G, A]) extends Var[(B, G), A]
}

import Var._
def evalVar[G, A](x: Var[G, A])(rho: G): A = x match {
case _: Z[g, a] =>
rho(0)
case s: S[g, a, b] =>
evalVar(s.x)(rho(1))
}
}
14 changes: 14 additions & 0 deletions tests/pos/i7044.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
object i7044 {
case class Seg[T](pat:Pat[T], body:T)

trait Pat[T]
object Pat {
case class Expr() extends Pat[Int]
case class Opt[S](el:Pat[S]) extends Pat[Option[S]]
}

def test[T](s:Seg[T]):Int = s match {
case Seg(Pat.Expr(),body) => body + 1
case Seg(Pat.Opt(Pat.Expr()),body) => body.get
}
}