Skip to content

Commit

Permalink
Merge pull request scala#7364 from dotty-staging/fix-6570-1
Browse files Browse the repository at this point in the history
Fix scala#6570: Don't reduce match types with empty scrutinies
  • Loading branch information
OlivierBlanvillain authored Oct 10, 2019
2 parents 157ef5d + 04b2c3e commit cef08d9
Show file tree
Hide file tree
Showing 9 changed files with 234 additions and 52 deletions.
121 changes: 80 additions & 41 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ import transform.TypeUtils._
import transform.SymUtils._
import scala.util.control.NonFatal
import typer.ProtoTypes.constrained
import typer.Applications.productSelectorTypes
import reporting.trace

final class AbsentContext
Expand Down Expand Up @@ -2136,19 +2137,52 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
/** Returns last check's debug mode, if explicitly enabled. */
def lastTrace(): String = ""

/** Are `tp1` and `tp2` disjoint types?
private def typeparamCorrespondsToField(tycon: Type, tparam: TypeParamInfo): Boolean =
productSelectorTypes(tycon, null).exists {
case tp: TypeRef =>
tp.designator.eq(tparam) // Bingo!
case _ =>
false
}

/** Is `tp` an empty type?
*
* `true` implies that we found a proof; uncertainty default to `false`.
* `true` implies that we found a proof; uncertainty defaults to `false`.
*/
def provablyEmpty(tp: Type): Boolean =
tp.dealias match {
case tp if tp.isBottomType => true
case AndType(tp1, tp2) => provablyDisjoint(tp1, tp2)
case OrType(tp1, tp2) => provablyEmpty(tp1) && provablyEmpty(tp2)
case at @ AppliedType(tycon, args) =>
args.lazyZip(tycon.typeParams).exists { (arg, tparam) =>
tparam.paramVariance >= 0
&& provablyEmpty(arg)
&& typeparamCorrespondsToField(tycon, tparam)
}
case tp: TypeProxy =>
provablyEmpty(tp.underlying)
case _ => false
}


/** Are `tp1` and `tp2` provablyDisjoint types?
*
* `true` implies that we found a proof; uncertainty defaults to `false`.
*
* 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
* 3. ConstantTypes with distinct values are non intersecting
* 4. There is no value of type Nothing
*
* Note on soundness: the correctness of match types relies on on the
* property that in all possible contexts, the same match type expression
* is either stuck or reduces to the same case.
*/
def disjoint(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = {
// println(s"disjoint(${tp1.show}, ${tp2.show})")
def provablyDisjoint(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = {
// println(s"provablyDisjoint(${tp1.show}, ${tp2.show})")
/** Can we enumerate all instantiations of this type? */
def isClosedSum(tp: Symbol): Boolean =
tp.is(Sealed) && tp.isOneOf(AbstractOrTrait) && !tp.hasAnonymousChild
Expand Down Expand Up @@ -2181,33 +2215,19 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
// of classes.
true
else if (isClosedSum(cls1))
decompose(cls1, tp1).forall(x => disjoint(x, tp2))
decompose(cls1, tp1).forall(x => provablyDisjoint(x, tp2))
else if (isClosedSum(cls2))
decompose(cls2, tp2).forall(x => disjoint(x, tp1))
decompose(cls2, tp2).forall(x => provablyDisjoint(x, tp1))
else
false
case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 =>
// It is possible to conclude that two types applies are disjoint by
// looking at covariant type parameters if the said type parameters
// are disjoin and correspond to fields.
// (Type parameter disjointness is not enough by itself as it could
// lead to incorrect conclusions for phantom type parameters).
def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
disjoint(tp1, tp2) && {
// 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
// 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!
case _ =>
false
}
!lowerBoundedByNothing || typeUsedAsField
}
provablyDisjoint(tp1, tp2) && typeparamCorrespondsToField(tycon1, tparam)

args1.lazyZip(args2).lazyZip(tycon1.typeParams).exists {
(arg1, arg2, tparam) =>
Expand Down Expand Up @@ -2236,29 +2256,29 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
}
}
case (tp1: HKLambda, tp2: HKLambda) =>
disjoint(tp1.resType, tp2.resType)
provablyDisjoint(tp1.resType, tp2.resType)
case (_: HKLambda, _) =>
// The intersection of these two types would be ill kinded, they are therefore disjoint.
// The intersection of these two types would be ill kinded, they are therefore provablyDisjoint.
true
case (_, _: HKLambda) =>
true
case (tp1: OrType, _) =>
disjoint(tp1.tp1, tp2) && disjoint(tp1.tp2, tp2)
provablyDisjoint(tp1.tp1, tp2) && provablyDisjoint(tp1.tp2, tp2)
case (_, tp2: OrType) =>
disjoint(tp1, tp2.tp1) && disjoint(tp1, tp2.tp2)
provablyDisjoint(tp1, tp2.tp1) && provablyDisjoint(tp1, tp2.tp2)
case (tp1: AndType, tp2: AndType) =>
(disjoint(tp1.tp1, tp2.tp1) || disjoint(tp1.tp2, tp2.tp2)) &&
(disjoint(tp1.tp1, tp2.tp2) || disjoint(tp1.tp2, tp2.tp1))
(provablyDisjoint(tp1.tp1, tp2.tp1) || provablyDisjoint(tp1.tp2, tp2.tp2)) &&
(provablyDisjoint(tp1.tp1, tp2.tp2) || provablyDisjoint(tp1.tp2, tp2.tp1))
case (tp1: AndType, _) =>
disjoint(tp1.tp2, tp2) || disjoint(tp1.tp1, tp2)
provablyDisjoint(tp1.tp2, tp2) || provablyDisjoint(tp1.tp1, tp2)
case (_, tp2: AndType) =>
disjoint(tp1, tp2.tp2) || disjoint(tp1, tp2.tp1)
provablyDisjoint(tp1, tp2.tp2) || provablyDisjoint(tp1, tp2.tp1)
case (tp1: TypeProxy, tp2: TypeProxy) =>
disjoint(tp1.underlying, tp2) || disjoint(tp1, tp2.underlying)
provablyDisjoint(tp1.underlying, tp2) || provablyDisjoint(tp1, tp2.underlying)
case (tp1: TypeProxy, _) =>
disjoint(tp1.underlying, tp2)
provablyDisjoint(tp1.underlying, tp2)
case (_, tp2: TypeProxy) =>
disjoint(tp1, tp2.underlying)
provablyDisjoint(tp1, tp2.underlying)
case _ =>
false
}
Expand Down Expand Up @@ -2419,6 +2439,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
}.apply(tp)

val defn.MatchCase(pat, body) = cas1

if (isSubType(scrut, pat))
// `scrut` is a subtype of `pat`: *It's a Match!*
Some {
Expand All @@ -2432,8 +2453,8 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
}
else if (isSubType(widenAbstractTypes(scrut), widenAbstractTypes(pat)))
Some(NoType)
else if (disjoint(scrut, pat))
// We found a proof that `scrut` and `pat` are incompatible.
else if (provablyDisjoint(scrut, pat))
// We found a proof that `scrut` and `pat` are incompatible.
// The search continues.
None
else
Expand All @@ -2445,7 +2466,25 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
case Nil => NoType
}

inFrozenConstraint(recur(cases))
inFrozenConstraint {
// Empty types break the basic assumption that if a scrutinee and a
// pattern are disjoint it's OK to reduce passed that pattern. Indeed,
// empty types viewed as a set of value is always a subset of any other
// types. As a result, we first check that the scrutinee isn't empty
// before proceeding with reduction. See `tests/neg/6570.scala` and
// `6570-1.scala` for examples that exploit emptiness to break match
// type soundness.

// If we revered the uncertainty case of this empty check, that is,
// `!provablyNonEmpty` instead of `provablyEmpty`, that would be
// obviously sound, but quite restrictive. With the current formulation,
// we need to be careful that `provablyEmpty` covers all the conditions
// used to conclude disjointness in `provablyDisjoint`.
if (provablyEmpty(scrut))
NoType
else
recur(cases)
}
}
}

Expand Down
4 changes: 2 additions & 2 deletions compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
Original file line number Diff line number Diff line change
Expand Up @@ -302,7 +302,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
// Since projections of types don't include null, intersection with null is empty.
if (tp1 == nullType || tp2 == nullType) Empty
else {
val res = ctx.typeComparer.disjoint(tp1, tp2)
val res = ctx.typeComparer.provablyDisjoint(tp1, tp2)

if (res) Empty
else if (tp1.isSingleton) Typ(tp1, true)
Expand Down Expand Up @@ -529,7 +529,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {

def inhabited(tp: Type): Boolean =
tp.dealias match {
case AndType(tp1, tp2) => !ctx.typeComparer.disjoint(tp1, tp2)
case AndType(tp1, tp2) => !ctx.typeComparer.provablyDisjoint(tp1, tp2)
case OrType(tp1, tp2) => inhabited(tp1) || inhabited(tp2)
case tp: RefinedType => inhabited(tp.parent)
case tp: TypeRef => inhabited(tp.prefix)
Expand Down
2 changes: 1 addition & 1 deletion tests/neg/6314-1.scala
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ object G {
}

def main(args: Array[String]): Unit = {
val a: Bar[X & Y] = "hello"
val a: Bar[X & Y] = "hello" // error
val i: Bar[Y & Foo] = Foo.apply[Bar](a)
val b: Int = i // error
println(b + 1)
Expand Down
4 changes: 2 additions & 2 deletions tests/neg/6314-2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,11 @@ object G {
case Y => Int
}

val a: Bar[X & Foo] = "hello"
val a: Bar[X & Foo] = "hello" // error
val b: Bar[Y & Foo] = 1 // error

def main(args: Array[String]): Unit = {
val a: Bar[X & Foo] = "hello"
val a: Bar[X & Foo] = "hello" // error
val i: Bar[Y & Foo] = Foo.apply[Bar](a)
val b: Int = i // error
println(b + 1)
Expand Down
33 changes: 33 additions & 0 deletions tests/neg/6570-1.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
import scala.Tuple._

trait Trait1
trait Trait2

case class Box[+T](t: T)

type N[x] = x match {
case Box[String] => Trait1
case Box[Int] => Trait2
}

trait Cov[+T]
type M[t] = t match {
case Cov[x] => N[x]
}

trait Root[A] {
def thing: M[A]
}

class Asploder extends Root[Cov[Box[Int & String]]] {
def thing = new Trait1 {} // error
}

object Main {
def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing

def explode = foo(new Asploder)

def main(args: Array[String]): Unit =
explode
}
109 changes: 109 additions & 0 deletions tests/neg/6570.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,109 @@
object Base {
trait Trait1
trait Trait2
type N[t] = t match {
case String => Trait1
case Int => Trait2
}
}
import Base._

object UpperBoundParametricVariant {
trait Cov[+T]
type M[t] = t match {
case Cov[x] => N[x]
}

trait Root[A] {
def thing: M[A]
}

trait Child[A <: Cov[Int]] extends Root[A]

// we reduce `M[T]` to `Trait2`, even though we cannot be certain of that
def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing

class Asploder extends Child[Cov[String & Int]] {
def thing = new Trait1 {} // error
}

def explode = foo(new Asploder) // ClassCastException
}

object InheritanceVariant {
// allows binding a variable to the UB of a type member
type Trick[a] = { type A <: a }
type M[t] = t match { case Trick[a] => N[a] }

trait Root {
type B
def thing: M[B]
}

trait Child extends Root { type B <: { type A <: Int } }

def foo(c: Child): Trait2 = c.thing

class Asploder extends Child {
type B = { type A = String & Int }
def thing = new Trait1 {} // error
}
}

object ThisTypeVariant {
type Trick[a] = { type A <: a }
type M[t] = t match { case Trick[a] => N[a] }

trait Root {
def thing: M[this.type]
}

trait Child extends Root { type A <: Int }

def foo(c: Child): Trait2 = c.thing

class Asploder extends Child {
type A = String & Int
def thing = new Trait1 {} // error
}
}

object ParametricVariant {
type Trick[a] = { type A <: a }
type M[t] = t match { case Trick[a] => N[a] }

trait Root[B] {
def thing: M[B]
}

trait Child[B <: { type A <: Int }] extends Root[B]

def foo[T <: { type A <: Int }](c: Child[T]): Trait2 = c.thing

class Asploder extends Child[{ type A = String & Int }] {
def thing = new Trait1 {} // error
}

def explode = foo(new Asploder)
}

object UpperBoundVariant {
trait Cov[+T]
type M[t] = t match { case Cov[t] => N[t] }

trait Root {
type A
def thing: M[A]
}

trait Child extends Root { type A <: Cov[Int] }

def foo(c: Child): Trait2 = c.thing

class Asploder extends Child {
type A = Cov[String & Int]
def thing = new Trait1 {} // error
}

def explode = foo(new Asploder)
}
8 changes: 4 additions & 4 deletions tests/neg/matchtype-seq.scala
Original file line number Diff line number Diff line change
Expand Up @@ -102,10 +102,10 @@ object Test {

identity[T9[Tuple2[Int, String]]](1)
identity[T9[Tuple2[String, Int]]]("1")
identity[T9[Tuple2[Nothing, String]]](1)
identity[T9[Tuple2[String, Nothing]]]("1")
identity[T9[Tuple2[Int, Nothing]]](1)
identity[T9[Tuple2[Nothing, Int]]]("1")
identity[T9[Tuple2[Nothing, String]]](1) // error
identity[T9[Tuple2[String, Nothing]]]("1") // error
identity[T9[Tuple2[Int, Nothing]]](1) // error
identity[T9[Tuple2[Nothing, Int]]]("1") // error
identity[T9[Tuple2[_, _]]]("") // error
identity[T9[Tuple2[_, _]]](1) // error
identity[T9[Tuple2[Any, Any]]]("") // error
Expand Down
Loading

0 comments on commit cef08d9

Please sign in to comment.