fix SI-9657 about type bounds

Author: liufengyun

src/dotty/tools/dotc/transform/patmat/Space.scala

@@ -14,10 +14,14 @@ import core.StdNames._
 import core.NameOps._
 import core.Constants._
 
-/** Space logic for checking exhaustivity and unreachability of pattern matching.
+/** Space logic for checking exhaustivity and unreachability of pattern matching
  *
- *  The core idea of the algorithm is that patterns and types are value
- *  spaces, which is recursively defined as follows:
+ *  Space can be thought of as a set of possible values. A type or a pattern
+ *  both refer to spaces. The space of a type is the values that inhabit the
+ *  type. The space of a pattern is the values that can be covered by the
+ *  pattern.
+ *
+ *  Space is recursively defined as follows:
  *
  *      1. `Empty` is a space
  *      2. For a type T, `Typ(T)` is a space
@@ -279,7 +283,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   }
 
   /** Is `tp1` a subtype of `tp2`?  */
-  def isSubType(tp1: Type, tp2: Type): Boolean = tp1 <:< tp2
+  def isSubType(tp1: Type, tp2: Type): Boolean = {
+    // expose is important due to type bounds
+    // check SI-9657 and tests/patmat/gadt.scala
+    tp1 <:< expose(tp2)
+  }
 
   def isEqualType(tp1: Type, tp2: Type): Boolean = tp1 =:= tp2
 
@@ -472,6 +480,59 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     isCheckable(sel.tpe.widen.elimAnonymousClass)
   }
 
+
+  /** Expose refined type to eliminate reference to type variables
+   *
+   *  A = B                      M { type T = A }        ~~>  M { type T = B }
+   *
+   *  A <: X :> Y                M { type T = A }        ~~>  M { type T <: X :> Y }
+   *
+   *  A <: X :> Y  B <: U :> V   M { type T <: A :> B }  ~~>  M { type T <: X :> B }
+   *
+   *  A = X  B = Y               M { type T <: A :> B }  ~~>  M { type T <: X :> Y }
+   */
+  def expose(tp: Type): Type = {
+    def follow(tp: Type, up: Boolean): Type = tp match {
+      case tp: TypeProxy =>
+        tp.underlying match {
+          case TypeBounds(lo, hi) =>
+            follow(if (up) hi else lo, up)
+          case _ =>
+            tp
+        }
+      case OrType(tp1, tp2) =>
+        OrType(follow(tp1, up), follow(tp2, up))
+      case AndType(tp1, tp2) =>
+        AndType(follow(tp1, up), follow(tp2, up))
+    }
+
+    tp match {
+      case tp: RefinedType =>
+        tp.refinedInfo match {
+          case tpa : TypeAlias =>
+            val hi = follow(tpa.alias, true)
+            val lo = follow(tpa.alias, false)
+            val refined = if (hi =:= lo)
+              tpa.derivedTypeAlias(hi)
+            else
+              tpa.derivedTypeBounds(lo, hi)
+
+            tp.derivedRefinedType(
+              expose(tp.parent),
+              tp.refinedName,
+              refined
+            )
+          case tpb @ TypeBounds(lo, hi) =>
+            tp.derivedRefinedType(
+              expose(tp.parent),
+              tp.refinedName,
+              tpb.derivedTypeBounds(follow(lo, false), follow(hi, true))
+            )
+        }
+      case _ => tp
+    }
+  }
+
   def checkExhaustivity(_match: Match): Unit = {
     val Match(sel, cases) = _match
     val selTyp = sel.tpe.widen.elimAnonymousClass.dealias
@@ -491,7 +552,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
 
   def checkRedundancy(_match: Match): Unit = {
     val Match(sel, cases) = _match
-    val selTyp = sel.tpe.widen.elimAnonymousClass
+    // ignore selector type for now
+    // val selTyp = sel.tpe.widen.elimAnonymousClass.dealias
 
     // starts from the second, the first can't be redundant
     (1 until cases.length).foreach { i =>

tests/patmat/gadt.check

@@ -10,4 +10,8 @@ It would fail on the following input: Or(_, _)
 It would fail on the following input: BooleanLit(_), IntLit(_)
   def foo4b(x: Expr) = x match {
                          ^
-three warnings found
+./tests/patmat/gadt.scala:55: warning: match may not be exhaustive.
+It would fail on the following input: Sum(_, _)
+  def foo5b[T <: Int](x: Expr[T]) = x match {
+                                      ^
+four warnings found

tests/patmat/gadt.scala

@@ -46,4 +46,13 @@ object Test {
     case _: Sum => true
     case _: Or => true
   }
-}
+
+  def foo5a[T <: Int](x: Expr[T]) = x match {
+    case _: IntLit => true
+    case _: Sum => true
+  }
+
+  def foo5b[T <: Int](x: Expr[T]) = x match {
+    case _: IntLit => true
+  }
+}

tests/patmat/t9657.check

@@ -0,0 +1,17 @@
+./tests/patmat/t9657.scala:29: warning: match may not be exhaustive.
+It would fail on the following input: Bus(_)
+  def refuel2[P <: Petrol.type](vehicle: Vehicle {type A = P} ): Vehicle = vehicle match {
+                                                                                   ^
+./tests/patmat/t9657.scala:38: warning: match may not be exhaustive.
+It would fail on the following input: Bus(_)
+  def foo2(vehicle: Vehicle {type A <: Petrol.type} ): Vehicle = vehicle match {
+                                                                         ^
+./tests/patmat/t9657.scala:49: warning: match may not be exhaustive.
+It would fail on the following input: Bus(_)
+  def bar2(vehicle: Vehicle {type A <: P} ): Vehicle = vehicle match {
+                                                               ^
+./tests/patmat/t9657.scala:58: warning: match may not be exhaustive.
+It would fail on the following input: Bus(_)
+  def qux2[P <: Petrol.type](vehicle: Vehicle {type A <: P} ): Vehicle = vehicle match {
+                                                                                 ^
+four warnings found

tests/patmat/t9657.scala

@@ -0,0 +1,62 @@
+sealed trait PowerSource
+
+case object Petrol extends PowerSource
+
+case object Pedal extends PowerSource
+
+sealed abstract class Vehicle {
+  type A <: PowerSource
+}
+
+case object Bicycle extends Vehicle {
+  type A = Pedal.type
+}
+
+case class Bus(fuel: Int) extends Vehicle {
+  type A = Petrol.type
+}
+
+case class Car(fuel: Int) extends Vehicle {
+  type A = Petrol.type
+}
+
+class Test {
+  def refuel[P <: Petrol.type](vehicle: Vehicle {type A = P} ): Vehicle = vehicle match {
+    case Car(_) => Car(100)
+    case Bus(_) => Bus(100)
+  }
+
+  def refuel2[P <: Petrol.type](vehicle: Vehicle {type A = P} ): Vehicle = vehicle match {
+    case Car(_) => Car(100)
+  }
+
+  def foo1(vehicle: Vehicle {type A <: Petrol.type} ): Vehicle = vehicle match {
+    case Car(_) => Car(100)
+    case Bus(_) => Bus(100)
+  }
+
+  def foo2(vehicle: Vehicle {type A <: Petrol.type} ): Vehicle = vehicle match {
+    case Car(_) => Car(100)
+  }
+
+  type P = Petrol.type
+
+  def bar1(vehicle: Vehicle {type A <: P} ): Vehicle = vehicle match {
+    case Car(_) => Car(100)
+    case Bus(_) => Bus(100)
+  }
+
+  def bar2(vehicle: Vehicle {type A <: P} ): Vehicle = vehicle match {
+    case Car(_) => Car(100)
+  }
+
+  def qux1[P <: Petrol.type](vehicle: Vehicle {type A <: P} ): Vehicle = vehicle match {
+    case Car(_) => Car(100)
+    case Bus(_) => Bus(100)
+  }
+
+  def qux2[P <: Petrol.type](vehicle: Vehicle {type A <: P} ): Vehicle = vehicle match {
+    case Car(_) => Car(100)
+  }
+
+}