Fix #6570: Don't reduce MT with empty scrutinies

Author: OlivierBlanvillain

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -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
@@ -2136,6 +2137,35 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
   /** Returns last check's debug mode, if explicitly enabled. */
   def lastTrace(): String = ""
 
+  private def typeparamCorrespondsToField(tycon: Type, tparam: TypeParamInfo): Boolean =
+    productSelectorTypes(tycon, null).exists {
+      case tp: TypeRef =>
+        (tp.designator: Any) == tparam // Bingo!
+      case _ =>
+        false
+    }
+
+  /** Is `tp` an empty type?
+   *
+   *  `true` implies that we found a proof; uncertainty default to `false`.
+   */
+  def provablyEmpty(tp: Type): Boolean =
+    tp.dealias match {
+      case tp if tp.isBottomType => true
+      case AndType(tp1, tp2) => disjoint(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` disjoint types?
    *
    *  `true` implies that we found a proof; uncertainty default to `false`.
@@ -2144,8 +2174,12 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *
    *  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, a 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})")
@@ -2187,27 +2221,13 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
           else
             false
       case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 =>
+        // It is possible to conclude that two types applies are disjoints 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
-          }
+          disjoint(tp1, tp2) && typeparamCorrespondsToField(tycon1, tparam)
 
         args1.lazyZip(args2).lazyZip(tycon1.typeParams).exists {
           (arg1, arg2, tparam) =>
@@ -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 {
@@ -2433,7 +2454,7 @@ 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.
+        // We found a proof that `scrut` and `pat` are incompatible.
         // The search continues.
         None
       else
@@ -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 `disjoint`.
+      if (provablyEmpty(scrut))
+        NoType
+      else
+        recur(cases)
+    }
   }
 }
 

tests/neg/6314-1.scala

@@ -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)

tests/neg/6314-2.scala

@@ -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)

tests/neg/6570-1.scala

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

tests/neg/6570.scala

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

tests/neg/matchtype-seq.scala

@@ -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

tests/run/tuples1.scala

@@ -62,7 +62,8 @@ object Test extends App {
   def head2[X <: NonEmptyTuple](x: X): Tuple.Head[X] = x.head
 
   val hd1: Int = head1(x3)
-  val hd2: Int = head2(x3)
+  // Without an explicit type parameter type inferance infers Nothing here.
+  val hd2: Int = head2[x3.type](x3)
 
   def tail1(x: NonEmptyTuple): Tuple.Tail[x.type] = x.tail
   def tail2[X <: NonEmptyTuple](x: X): Tuple.Tail[X] = x.tail