Skip to content

Match Types: implement cantPossiblyMatch #5996

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.

Sign up for GitHub

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 20 commits into from
Mar 9, 2019
Merged

Match Types: implement cantPossiblyMatch #5996

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
c1b7e84
Minor TypeTestsCasts refactoring
OlivierBlanvillain Feb 11, 2019
6e39fcb
Rename evalOnce to letBind
OlivierBlanvillain Feb 11, 2019
eef623a
Rename cmp to typeComparer
OlivierBlanvillain Feb 11, 2019
6755f52
Remove reduceParallel
OlivierBlanvillain Feb 18, 2019
88cfb7e
Fix spacing for TypeComparer comments
OlivierBlanvillain Feb 21, 2019
bb1515e
Flag ChildrenQueried in hasAnonymousChild
OlivierBlanvillain Feb 22, 2019
f79d937
Implement cantPossiblyMatch
OlivierBlanvillain Mar 1, 2019
60d0e20
Replace Space.inhabited by typeComparer.intersecting
OlivierBlanvillain Feb 28, 2019
d1180cc
Move refineUsingParent to Typer
OlivierBlanvillain Feb 26, 2019
b0c1e7b
Check inhabitation of children in Space
OlivierBlanvillain Feb 28, 2019
c3d23fe
Only trust isSameType for fully instanciated types
OlivierBlanvillain Feb 28, 2019
4f934ad
Use derivesFrom instead of isSubType for classes
OlivierBlanvillain Mar 1, 2019
80c25e3
Handle type parameters using symbol.is(TypeParam)
OlivierBlanvillain Mar 4, 2019
ab74827
Fix AppliedType logic
OlivierBlanvillain Mar 4, 2019
1df0d8b
Revert "Rename evalOnce to letBind"
OlivierBlanvillain Mar 6, 2019
8827eff
Revert "Flag ChildrenQueried in hasAnonymousChild"
OlivierBlanvillain Mar 6, 2019
ffa8acf
Address review
OlivierBlanvillain Mar 6, 2019
e7f6049
Move refineUsingParent to TypeOps
OlivierBlanvillain Mar 6, 2019
f4df58d
Factor out cov. test and use it in the inv. case
OlivierBlanvillain Mar 6, 2019
ea04343
Update inhabited check in Space
OlivierBlanvillain Mar 6, 2019
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
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/ast/tpd.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1139,7 +1139,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
}

/** Let bind `tree` unless `tree` is at least idempotent */
def evalOnce(tree: Tree)(within: Tree => Tree)(implicit ctx: Context): Tree =
def letBind(tree: Tree)(within: Tree => Tree)(implicit ctx: Context): Tree =
letBindUnless(TreeInfo.Idempotent, tree)(within)

def runtimeCall(name: TermName, args: List[Tree])(implicit ctx: Context): Tree = {
Expand Down
260 changes: 200 additions & 60 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ import TypeErasure.{erasedLub, erasedGlb}
import TypeApplications._
import Constants.Constant
import transform.TypeUtils._
import transform.SymUtils._
import scala.util.control.NonFatal
import typer.ProtoTypes.constrained
import reporting.trace
Expand Down Expand Up @@ -528,7 +529,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
case tp2: HKTypeLambda =>
def compareTypeLambda: Boolean = tp1.stripTypeVar match {
case tp1: HKTypeLambda =>
/* Don't compare bounds of lambdas under language:Scala2, or t2994 will fail.
/* Don't compare bounds of lambdas under language:Scala2, or t2994 will fail.
* The issue is that, logically, bounds should compare contravariantly,
* but that would invalidate a pattern exploited in t2994:
*
Expand Down Expand Up @@ -761,14 +762,14 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
}

/** Subtype test for the hk application `tp2 = tycon2[args2]`.
*/
*/
def compareAppliedType2(tp2: AppliedType, tycon2: Type, args2: List[Type]): Boolean = {
val tparams = tycon2.typeParams
if (tparams.isEmpty) return false // can happen for ill-typed programs, e.g. neg/tcpoly_overloaded.scala

/** True if `tp1` and `tp2` have compatible type constructors and their
* corresponding arguments are subtypes relative to their variance (see `isSubArgs`).
*/
* corresponding arguments are subtypes relative to their variance (see `isSubArgs`).
*/
def isMatchingApply(tp1: Type): Boolean = tp1 match {
case AppliedType(tycon1, args1) =>
tycon1.dealiasKeepRefiningAnnots match {
Expand Down Expand Up @@ -815,25 +816,25 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
}

/** `param2` can be instantiated to a type application prefix of the LHS
* or to a type application prefix of one of the LHS base class instances
* and the resulting type application is a supertype of `tp1`,
* or fallback to fourthTry.
*/
* or to a type application prefix of one of the LHS base class instances
* and the resulting type application is a supertype of `tp1`,
* or fallback to fourthTry.
*/
def canInstantiate(tycon2: TypeParamRef): Boolean = {

/** Let
*
* `tparams_1, ..., tparams_k-1` be the type parameters of the rhs
* `tparams1_1, ..., tparams1_n-1` be the type parameters of the constructor of the lhs
* `args1_1, ..., args1_n-1` be the type arguments of the lhs
* `d = n - k`
*
* Returns `true` iff `d >= 0` and `tycon2` can be instantiated to
*
* [tparams1_d, ... tparams1_n-1] -> tycon1[args_1, ..., args_d-1, tparams_d, ... tparams_n-1]
*
* such that the resulting type application is a supertype of `tp1`.
*/
*
* `tparams_1, ..., tparams_k-1` be the type parameters of the rhs
* `tparams1_1, ..., tparams1_n-1` be the type parameters of the constructor of the lhs
* `args1_1, ..., args1_n-1` be the type arguments of the lhs
* `d = n - k`
*
* Returns `true` iff `d >= 0` and `tycon2` can be instantiated to
*
* [tparams1_d, ... tparams1_n-1] -> tycon1[args_1, ..., args_d-1, tparams_d, ... tparams_n-1]
*
* such that the resulting type application is a supertype of `tp1`.
*/
def appOK(tp1base: Type) = tp1base match {
case tp1base: AppliedType =>
var tycon1 = tp1base.tycon
Expand Down Expand Up @@ -874,21 +875,21 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
}

/** Fall back to comparing either with `fourthTry` or against the lower
* approximation of the rhs.
* @param tyconLo The type constructor's lower approximation.
*/
* approximation of the rhs.
* @param tyconLo The type constructor's lower approximation.
*/
def fallback(tyconLo: Type) =
either(fourthTry, isSubApproxHi(tp1, tyconLo.applyIfParameterized(args2)))

/** Let `tycon2bounds` be the bounds of the RHS type constructor `tycon2`.
* Let `app2 = tp2` where the type constructor of `tp2` is replaced by
* `tycon2bounds.lo`.
* If both bounds are the same, continue with `tp1 <:< app2`.
* otherwise continue with either
*
* tp1 <:< tp2 using fourthTry (this might instantiate params in tp1)
* tp1 <:< app2 using isSubType (this might instantiate params in tp2)
*/
* Let `app2 = tp2` where the type constructor of `tp2` is replaced by
* `tycon2bounds.lo`.
* If both bounds are the same, continue with `tp1 <:< app2`.
* otherwise continue with either
*
* tp1 <:< tp2 using fourthTry (this might instantiate params in tp1)
* tp1 <:< app2 using isSubType (this might instantiate params in tp2)
*/
def compareLower(tycon2bounds: TypeBounds, tyconIsTypeRef: Boolean): Boolean =
if ((tycon2bounds.lo `eq` tycon2bounds.hi) && !tycon2bounds.isInstanceOf[MatchAlias])
if (tyconIsTypeRef) recur(tp1, tp2.superType)
Expand Down Expand Up @@ -927,7 +928,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
}

/** Subtype test for the application `tp1 = tycon1[args1]`.
*/
*/
def compareAppliedType1(tp1: AppliedType, tycon1: Type, args1: List[Type]): Boolean =
tycon1 match {
case param1: TypeParamRef =>
Expand Down Expand Up @@ -973,8 +974,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
}

/** Like tp1 <:< tp2, but returns false immediately if we know that
* the case was covered previously during subtyping.
*/
* the case was covered previously during subtyping.
*/
def isNewSubType(tp1: Type): Boolean =
if (isCovered(tp1) && isCovered(tp2)) {
//println(s"useless subtype: $tp1 <:< $tp2")
Expand Down Expand Up @@ -1031,12 +1032,12 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
}

/** Subtype test for corresponding arguments in `args1`, `args2` according to
* variances in type parameters `tparams2`.
* @param tp1 The applied type containing `args1`
* @param tparams2 The type parameters of the type constructor applied to `args2`
*/
* variances in type parameters `tparams2`.
*
* @param tp1 The applied type containing `args1`
* @param tparams2 The type parameters of the type constructor applied to `args2`
*/
def isSubArgs(args1: List[Type], args2: List[Type], tp1: Type, tparams2: List[ParamInfo]): Boolean = {

/** The bounds of parameter `tparam`, where all references to type paramneters
* are replaced by corresponding arguments (or their approximations in the case of
* wildcard arguments).
Expand Down Expand Up @@ -1875,6 +1876,130 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {

/** Returns last check's debug mode, if explicitly enabled. */
def lastTrace(): String = ""

/** Do `tp1` and `tp2` share a non-null inhabitant?
*
* `false` implies that we found a proof; uncertainty default to `true`.
*
* Proofs rely on the following properties of Scala types:
*
* 1. Single inheritance of classes
* 2. Final classes cannot be extended
* 3. ConstantTypes with distinc values are non intersecting
* 4. There is no value of type Nothing
*/
def intersecting(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = {
// println(s"intersecting(${tp1.show}, ${tp2.show})")
/** Can we enumerate all instantiations of this type? */
def isClosed(tp: Symbol): Boolean =
tp.is(Sealed) && tp.is(AbstractOrTrait) && !tp.hasAnonymousChild

/** Splits a close type into a disjunction of smaller types.
* It should hold that `tp` and `decompose(tp).reduce(_ or _)`
* denote the same set of values.
*/
def decompose(sym: Symbol, tp: Type): List[Type] =
sym.children.map(x => ctx.typer.refineUsingParent(tp, x)).filter(_.exists)

(tp1.dealias, tp2.dealias) match {
case (tp1: ConstantType, tp2: ConstantType) =>
tp1 == tp2
case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass =>
if (isSubType(tp1, tp2) || isSubType(tp2, tp1)) {
true
} else {
val cls1 = tp1.classSymbol
val cls2 = tp2.classSymbol
if (cls1.is(Final) || cls2.is(Final))
// One of these types is final and they are not mutually
// subtype, so they must be unrelated.
false
else if (!cls2.is(Trait) && !cls1.is(Trait))
// Both of these types are classes and they are not mutually
// subtype, so they must be unrelated by single inheritance
// of classes.
false
else if (isClosed(cls1))
decompose(cls1, tp1).exists(x => intersecting(x, tp2))
else if (isClosed(cls2))
decompose(cls2, tp2).exists(x => intersecting(x, tp1))
else
true
}
case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) =>
// Unboxed x.zip(y).zip(z).forall { case ((a, b), c) => f(a, b, c) }
def zip_zip_forall[A, B, C](x: List[A], y: List[B], z: List[C])(f: (A, B, C) => Boolean): Boolean =
x match {
case x :: xs => y match {
case y :: ys => z match {
case z :: zs => f(x, y, z) && zip_zip_forall(xs, ys, zs)(f)
case _ => true
}
case _ => true
}
case _ => true
}

tycon1 == tycon2 &&
zip_zip_forall(args1, args2, tycon1.typeParams) {
(arg1, arg2, tparam) =>
val v = tparam.paramVariance
// Note that the logic below is conservative in that is
// assumes that Covariant type parameters are Contravariant
// type
if (v > 0)
intersecting(arg1, arg2) || {
// We still need to proof that `Nothing` is not a valid
// instantiation of this type parameter. We have two ways
// to get to that conclusion:
// 1. `Nothing` does not conform to the type parameter's lb
// 2. `tycon1` has a field typed with this type parameter.
//
// Because of separate compilation, the use of 2. is
Copy link
Contributor

Choose a reason for hiding this comment

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

Nice trick!

// limited to case classes.
import dotty.tools.dotc.typer.Applications.productSelectorTypes
val lowerBoundedByNothing = tparam.paramInfo.bounds.lo eq NothingType
val typeUsedAsField =
productSelectorTypes(tycon1, null).exists {
case tp: TypeRef =>
(tp.designator: Any) == tparam // Bingo!
Copy link
Contributor

Choose a reason for hiding this comment

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

Why the upcast to Any?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Scalac (wrongly) complains without the upcast:

dotty.tools.dotc.core.Names.Designator
and
dotty.tools.dotc.core.ParamInfo{type ThisName = dotty.tools.dotc.core.Names.TypeName}
are unrelated: they will most likely never compare equal

case _ =>
false
}
lowerBoundedByNothing && !typeUsedAsField
}
else if (v < 0)
// Contravariant case: a value where this type parameter is
// instantiated to `Any` belongs to both types.
true
else
isSameType(arg1, arg2) // TODO: handle uninstanciated types
}
case (tp1: HKLambda, tp2: HKLambda) =>
intersecting(tp1.resType, tp2.resType)
case (_: HKLambda, _) =>
// The intersection is ill kinded and therefore empty.
false
case (_, _: HKLambda) =>
false
case (tp1: OrType, _) =>
intersecting(tp1.tp1, tp2) || intersecting(tp1.tp2, tp2)
case (_, tp2: OrType) =>
intersecting(tp1, tp2.tp1) || intersecting(tp1, tp2.tp2)
case (tp1: AndType, _) =>
intersecting(tp1.tp1, tp2) && intersecting(tp1.tp2, tp2) && intersecting(tp1.tp1, tp1.tp2)
case (_, tp2: AndType) =>
intersecting(tp1, tp2.tp1) && intersecting(tp1, tp2.tp2) && intersecting(tp2.tp1, tp2.tp2)
case (tp1: TypeProxy, tp2: TypeProxy) =>
intersecting(tp1.underlying, tp2) && intersecting(tp1, tp2.underlying)
case (tp1: TypeProxy, _) =>
intersecting(tp1.underlying, tp2)
case (_, tp2: TypeProxy) =>
intersecting(tp1, tp2.underlying)
case _ =>
true
}
}
}

object TypeComparer {
Expand Down Expand Up @@ -1969,8 +2094,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
super.typeVarInstance(tvar)
}

def matchCase(scrut: Type, cas: Type, instantiate: Boolean)(implicit ctx: Context): Type = {

def matchCases(scrut: Type, cases: List[Type])(implicit ctx: Context): Type = {
def paramInstances = new TypeAccumulator[Array[Type]] {
def apply(inst: Array[Type], t: Type) = t match {
case t @ TypeParamRef(b, n) if b `eq` caseLambda =>
Expand All @@ -1989,29 +2113,45 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
}
}

val saved = constraint
try {
inFrozenConstraint {
val cas1 = cas match {
case cas: HKTypeLambda =>
caseLambda = constrained(cas)
caseLambda.resultType
case _ =>
cas
}
val defn.FunctionOf(pat :: Nil, body, _, _) = cas1
if (isSubType(scrut, pat))
caseLambda match {
case caseLambda: HKTypeLambda if instantiate =>
val instances = paramInstances(new Array(caseLambda.paramNames.length), pat)
instantiateParams(instances)(body)
var result: Type = NoType
var remainingCases = cases
while (!remainingCases.isEmpty) {
Copy link
Contributor

Choose a reason for hiding this comment

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

Why not use a tail-recursive function for matchCases?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I don't want constraints created while trying to evaluate one case to be carried over to the following cases, but I'm not sure if having these extra constraints could change anything...

val (cas :: cass) = remainingCases
remainingCases = cass
val saved = constraint
try {
inFrozenConstraint {
val cas1 = cas match {
case cas: HKTypeLambda =>
caseLambda = constrained(cas)
caseLambda.resultType
case _ =>
body
cas
}
else NoType
val defn.FunctionOf(pat :: Nil, body, _, _) = cas1
if (isSubType(scrut, pat)) {
// `scrut` is a subtype of `pat`: *It's a Match!*
result = caseLambda match {
case caseLambda: HKTypeLambda =>
val instances = paramInstances(new Array(caseLambda.paramNames.length), pat)
instantiateParams(instances)(body)
case _ =>
body
}
remainingCases = Nil
} else if (!intersecting(scrut, pat)) {
// We found a proof that `scrut` and `pat` are incompatible.
// The search continues.
} else {
// We are stuck: this match type instanciation is irreducible.
result = NoType
remainingCases = Nil
}
}
}
finally constraint = saved
}
finally constraint = saved
result
}
}

Expand Down
Loading