From 187dfd6e411fe25c79a4fef90e331d8ce8d1a86c Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@bright-it.com>
Date: Thu, 16 Nov 2017 11:01:02 +0100
Subject: [PATCH 1/6] Add new space definitions and operations

---
 .../dotc/transform/patmat/SpaceLogic.scala    | 198 ++++++++++++++++++
 .../tools/dotc/transform/patmat/Spaces.scala  |  58 +++++
 2 files changed, 256 insertions(+)
 create mode 100644 compiler/src/dotty/tools/dotc/transform/patmat/SpaceLogic.scala
 create mode 100644 compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/SpaceLogic.scala b/compiler/src/dotty/tools/dotc/transform/patmat/SpaceLogic.scala
new file mode 100644
index 000000000000..a5ca403c2d43
--- /dev/null
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/SpaceLogic.scala
@@ -0,0 +1,198 @@
+package dotty.tools.dotc.transform.patmat
+package `new logic`
+
+import dotty.tools.dotc.core.Symbols.Symbol
+import dotty.tools.dotc.core.Types.Type
+
+/** Space logic for checking exhaustivity and unreachability of pattern matching.
+ *
+ *  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. For a type T, `Typ(T)` is a space
+ *      2. `Prod(S1, S2, ..., Sn)` is a product space.
+ *
+ *  To correctly handle GADTs, we think in terms of _constrained_ spaces.
+ *  A constrained space containst a list of spaces and represents a set of _vectors_
+ *  of values. This would be a natural representation if we could pattern match on multiple values.
+ *  Additionally, as the name suggests, a constrained space can have _constraints_,
+ *  both term and type-level. The constraints are simply predicates restricting the value vectors
+ *  contained in the set represented by a constrained space.
+ *  Finally, a list of constrained spaces is used exactly like a union would.
+ *
+ *  For the problem of exhaustivity check, its formulation in terms of space is as follows:
+ *
+ *      Is the space Typ(T) a subspace of the union of spaces covered by all the patterns?
+ *
+ *  The problem of unreachable patterns can be formulated as follows:
+ *
+ *      Is the space covered by a pattern a subspace of the spaces covered by previous patterns?
+ *
+ *  Assumption:
+ *    (1) One case class cannot be inherited directly or indirectly by another
+ *        case class.
+ *    (2) Inheritance of a case class cannot be well handled by the algorithm.
+ *
+ */
+trait SpaceLogic {
+  /** Display space in string format */
+  def show(spaces: List[Space]): String
+
+  def debugShow(s: ConstrainedSpace): String
+
+  def show(a: ConstrainedSpace): String = {
+    val shownVec = show(a.vec)
+    if (a.vec.length == 1) shownVec else s"[$shownVec]"
+  }
+
+  def show(as: Seq[ConstrainedSpace]): String =
+    as.map(show).mkString("{", ", ", "}")
+
+  def debugShow(as: Seq[ConstrainedSpace]): String =
+    as.map(debugShow).mkString("{", ", ", "}")
+
+  /** Run `thunk` in a debugging block, indenting all messages */
+  def doDebug[T](pre: => String, post: T => String)(thunk: => T): T
+
+  /** Is `tp1` a subtype of `tp2`? */
+  def isSubType(tp1: Type, tp2: Type): Boolean
+
+  /** Is `tp1` the same type as `tp2`? */
+  def isEqualType(tp1: Type, tp2: Type): Boolean
+
+  /** Return a space containing the values of both types.
+   *
+   * The types should be atomic (non-decomposable) and unrelated (neither
+   * should be a subtype of the other).
+   */
+  def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type): Option[Space]
+
+  /** Is the type `tp` decomposable? i.e. all values of the type can be covered
+   * by its decomposed types.
+   *
+   * Abstract sealed class, OrType, Boolean and Java enums can be decomposed.
+   */
+  def canDecompose(tp: Type): Boolean
+
+  /** Return term parameter types of the extractor `unapp` */
+  def signature(unapp: Type, unappSym: Symbol, argLen: Int): List[Type]
+
+  /** Get components of decomposable types */
+  def decompose(a: ConstrainedSpace): List[ConstrainedSpace]
+
+  /** Intersection of two spaces */
+  def intersect(a: ConstrainedSpace, b: ConstrainedSpace): List[ConstrainedSpace] =
+  doDebug[List[ConstrainedSpace]](s"${debugShow(a)} intersect ${debugShow(b)}", res => s"= ${debugShow(res)}") {
+    def doDecomposeA = decompose(a).flatMap(intersect(_, b))
+    def doDecomposeB = decompose(b).flatMap(intersect(a, _))
+
+    val res: List[ConstrainedSpace] = (a.vec, b.vec) match {
+      case (Nil, Nil) =>
+        // TODO: optimize this?
+        def union[T](l1: List[T], l2: List[T]) =
+          (l1 ::: l2).distinct
+
+        List(ConstrainedSpace(Nil, union(a.termConstraints, b.termConstraints), union(a.typeConstraints, b.typeConstraints)))
+
+      case (n :: ns, m :: ms) => (n, m) match {
+        case (nprod@Prod(_, nfun, nsym, nss, _), Prod(_, mfun, msym, mss, _)) =>
+          if (nsym != msym || !isEqualType(nfun, mfun)) Nil
+          else {
+            val arity = nss.length // assuming arity == mps.length
+            intersect(a withVec (nss ::: ns), b withVec (mss ::: ms)).map { c =>
+              val (kps, rest) = c.vec.splitAt(arity)
+              c.withVec(nprod.copy(params = kps) :: rest)
+            }
+          }
+
+        case (Prod(tp1, _, _, _, _), Typ(tp2, _)) =>
+          if (isSubType(tp1, tp2) || isSubType(tp2, tp1)) List(a)
+          else if (canDecompose(tp2)) doDecomposeB
+          else Nil
+
+        case (Typ(tp1, _), Prod(tp2, _, _, _, _)) =>
+          if (isSubType(tp1, tp2) || isSubType(tp2, tp1)) List(b)
+          else if (canDecompose(tp1)) doDecomposeA
+          else Nil
+
+        case (Typ(tp1, _), Typ(tp2, _)) =>
+          if (isSubType(tp1, tp2)) List(a)
+          else if (isSubType(tp2, tp1)) List(b)
+          else if (canDecompose(tp1)) doDecomposeA
+          else if (canDecompose(tp2)) doDecomposeB
+          else intersectUnrelatedAtomicTypes(tp1, tp2) match {
+            case None => Nil
+            case Some(space) =>
+              intersect(a.withVec(ns), b.withVec(ms)).map {
+                c => c.withVec(space :: c.vec)
+              }
+          }
+
+        case _ => Nil
+      }
+      case _ => Nil
+    }
+
+    res
+  }
+
+  /** The space of a not covered by b */
+  def subtract(a: ConstrainedSpace, b: ConstrainedSpace): List[ConstrainedSpace] =
+  doDebug[List[ConstrainedSpace]](s"${debugShow(a)} substract ${debugShow(b)}", res => s"= ${debugShow(res)}") {
+    def doDecomposeA = decompose(a).flatMap(subtract(_, b))
+    def doDecomposeB = decompose(b).foldLeft(List(a)) { (as, b) => as.flatMap(subtract(_, b)) }
+
+    val res = (a.vec, b.vec) match {
+      case (Nil, Nil) =>
+        if (b.termConstraints.isEmpty) Nil
+        else b.termConstraints.map { d => a.withTermConstraints(d.neg :: a.termConstraints) }
+
+      case (n :: ns, m :: ms) => (n, m) match {
+        case (nprod@Prod(_, nfun, nsym, nss, _), Prod(_, mfun, msym, mss, _)) =>
+          if (nsym != msym || !isEqualType(nfun, mfun)) List(a)
+          else {
+            val arity = nss.length // assuming nss.length == mss.length
+            subtract(a withVec (nss ::: ns), b withVec (mss ::: ms)).map { c =>
+              val (kps, rest) = c.vec.splitAt(arity)
+              c.withVec(nprod.copy(params = kps) :: rest)
+            }
+          }
+
+        case (p@Prod(tp1, _, _, _, full), Typ(tp2, _)) =>
+          if (isSubType(tp1, tp2)) {
+            val tailSubtraction = subtract(a withVec ns, b withVec ms)
+            tailSubtraction.map(_.withPrependendSpace(p))
+          } else if (full && canDecompose(tp2)) doDecomposeB
+          else List(a)
+
+        case (Typ(_, _), Prod(_, _, _, _, false)) =>
+          List(a) // approximation
+
+        case (Typ(tp1, _), p@Prod(tp2, fun, sym, ss, true)) =>
+          if (isSubType(tp1, tp2)) {
+            val newParams = signature(fun, sym, ss.length).map(Typ(_))
+            val _a = a.withVec(p.copy(tp = tp2, params = newParams) :: ns)
+            subtract(_a, b)
+          } else if (canDecompose(tp1)) doDecomposeA
+          else List(a)
+
+        case (Typ(tp1, _), Typ(tp2, _)) =>
+          if (isSubType(tp1, tp2)) {
+            val tailSubtraction = subtract(a withVec ns, b withVec ms)
+            tailSubtraction.map(_.withPrependendSpace(Typ(tp1)))
+          } else if (canDecompose(tp1)) doDecomposeA
+          else if (canDecompose(tp2)) doDecomposeB
+          else List(a)
+
+        case _ => List(a)
+      }
+      case _ => List(a)
+    }
+
+    res
+  }
+}
diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala
new file mode 100644
index 000000000000..b5cbb2264da5
--- /dev/null
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala
@@ -0,0 +1,58 @@
+package dotty.tools.dotc.transform.patmat
+package `new logic`
+
+import dotty.tools.dotc.core.Symbols.Symbol
+import dotty.tools.dotc.core.Types.Type
+
+/** Space definition */
+sealed trait Space
+
+/** Space representing the set of all values of a type
+ *
+ * @param tp: the type this space represents
+ * @param decomposed: does the space result from decomposition? Used for pretty print
+ *
+ */
+case class Typ(tp: Type, decomposed: Boolean = false) extends Space
+
+/** Space representing an extractor pattern */
+case class Prod(tp: Type, unappTp: Type, unappSym: Symbol, params: List[Space], full: Boolean) extends Space
+
+/** Represents a set of _vectors_ of values, possibly constrained
+  *
+  * Before and after exhaustivity checks, [[vec]] is exactly one space long.
+  */
+case class ConstrainedSpace(
+    vec: List[Space],
+    termConstraints: List[TermConstraint],
+    typeConstraints: List[TypeConstraint]
+) {
+  def withPrependendSpace(s: Space) = copy(vec = s :: vec)
+  def withVec(vec: List[Space]) = copy(vec = vec)
+  def withTermConstraints(termConstraints: List[TermConstraint]) = copy(termConstraints = termConstraints)
+  def withTypeConstraints(typeConstraints: List[TypeConstraint]) = copy(typeConstraints = typeConstraints)
+}
+
+/** A term-level constraint */
+sealed trait TermConstraint {
+  final def neg: TermConstraint = this match {
+    case Neg(c) => c
+    case c: PositiveTermConstraint => Neg(c)
+  }
+}
+
+/** Negated constraint. Cannot be nested by construction */
+case class Neg(c: PositiveTermConstraint) extends TermConstraint
+
+/** A constraint which isn't negated */
+sealed trait PositiveTermConstraint extends TermConstraint
+
+/** Represents a presence of some constraint (like a pattern guard) */
+case object Dummy extends PositiveTermConstraint
+
+/** A constraint which is always satisfied */
+case object AlwaysSatisfied extends PositiveTermConstraint
+
+/** A type-level constraint */
+sealed trait TypeConstraint
+case class TypeEquality(tp1: Type, tp2: Type) extends TypeConstraint

From 0c00c38c88e4215522707b1838828e3375aac737 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@bright-it.com>
Date: Thu, 16 Nov 2017 11:19:06 +0100
Subject: [PATCH 2/6] Add NaiveConstraintChecker

---
 .../patmat/NaiveConstraintChecker.scala       | 38 +++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 compiler/src/dotty/tools/dotc/transform/patmat/NaiveConstraintChecker.scala

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/NaiveConstraintChecker.scala b/compiler/src/dotty/tools/dotc/transform/patmat/NaiveConstraintChecker.scala
new file mode 100644
index 000000000000..a0e6d9910f5e
--- /dev/null
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/NaiveConstraintChecker.scala
@@ -0,0 +1,38 @@
+package dotty.tools.dotc.transform.patmat
+package `new logic`
+
+import dotty.tools.dotc.core.Contexts.Context
+
+/** Checks satisfiability of constraints in an extremely naive way */
+object NaiveConstraintChecker {
+  def hasUnsatisfiableConstraints(s: ConstrainedSpace)(implicit ctx: Context): Boolean =
+    !termsPotentiallySatisfiable(s.termConstraints) ||
+    !typesPotentiallySatisfiable(s.typeConstraints)
+
+  def termsPotentiallySatisfiable(constraints: List[TermConstraint]): Boolean =
+    constraints.forall {
+      case Dummy | Neg(Dummy) => true
+      case AlwaysSatisfied => true
+      case Neg(AlwaysSatisfied) => false
+    }
+
+  @annotation.tailrec
+  def typesPotentiallySatisfiable(constraints: List[TypeConstraint])(implicit ctx: Context): Boolean = {
+    def comparePair(tpeq1: TypeEquality, tpeq2: TypeEquality) =
+      if (tpeq1.tp1 =:= tpeq2.tp1) tpeq1.tp2 =:= tpeq2.tp2 else true
+
+    @annotation.tailrec
+    def compareOneVsList(tpeq: TypeEquality, constraints: List[TypeConstraint]): Boolean =
+      constraints match {
+        case Nil => true
+        case (tpeq2: TypeEquality) :: rest =>
+          comparePair(tpeq, tpeq2) && compareOneVsList(tpeq, rest)
+      }
+
+    constraints match {
+      case Nil => true
+      case (tpeq: TypeEquality) :: tail =>
+        compareOneVsList(tpeq, tail) && typesPotentiallySatisfiable(tail)
+    }
+  }
+}

From 54c21b756a10cc69df5a461b3543d591b2ea85b3 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@bright-it.com>
Date: Thu, 16 Nov 2017 11:09:32 +0100
Subject: [PATCH 3/6] SpaceEngine: implement debug functions

---
 .../tools/dotc/transform/patmat/Space.scala   | 60 +++++++++++++------
 1 file changed, 41 insertions(+), 19 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index 3f9f7d3143af..7d0692c24df7 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -19,7 +19,7 @@ import Inferencing._
 import ProtoTypes._
 import transform.SymUtils._
 import reporting.diagnostic.messages._
-import config.Printers.{exhaustivity => debug}
+import config.Printers.exhaustivity
 
 /** Space logic for checking exhaustivity and unreachability of pattern matching
  *
@@ -178,7 +178,7 @@ trait SpaceLogic {
         sym1 == sym2 && isEqualType(fun1, fun2) && ss1.zip(ss2).forall((isSubspace _).tupled)
     }
 
-    debug.println(s"${show(a)} < ${show(b)} = $res")
+    exhaustivity.println(s"${show(a)} < ${show(b)} = $res")
 
     res
   }
@@ -222,7 +222,7 @@ trait SpaceLogic {
         else Prod(tp1, fun1, sym1, ss1.zip(ss2).map((intersect _).tupled), full)
     }
 
-    debug.println(s"${show(a)} & ${show(b)} = ${show(res)}")
+    exhaustivity.println(s"${show(a)} & ${show(b)} = ${show(res)}")
 
     res
   }
@@ -272,7 +272,7 @@ trait SpaceLogic {
 
     }
 
-    debug.println(s"${show(a)} - ${show(b)} = ${show(res)}")
+    exhaustivity.println(s"${show(a)} - ${show(b)} = ${show(res)}")
 
     res
   }
@@ -301,6 +301,28 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   private val scalaNilType         = ctx.requiredModuleRef("scala.collection.immutable.Nil")
   private val scalaConsType        = ctx.requiredClassRef("scala.collection.immutable.::")
 
+  private var indent = 0
+  private def indentStr = "|  " * indent
+  def doDebug[T](pre: => String, post: (T) => String = (_: T) => "")(thunk: => T): T = {
+    val pre0 = pre
+    if (pre0.nonEmpty) exhaustivity.println(indentStr + pre)
+    var unindented = false
+    try {
+      indent += 1
+      val t = thunk
+      indent -= 1
+      unindented = true
+      val post0 = post(t)
+      if (post0.nonEmpty) exhaustivity.println(s"$indentStr$pre0 $post0")
+      else exhaustivity.println(indentStr + "-")
+      t
+    } finally if (!unindented) indent -= 1
+  }
+
+  def debug(msg: => String): Unit = {
+    exhaustivity.println(indentStr + msg)
+  }
+
   /** Checks if it's possible to create a trait/class which is a subtype of `tp`.
    *
    * - doesn't handle member collisions (will not declare a type unimplementable because of one)
@@ -366,7 +388,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     // which is a subtype of all the leaves of `and`.
     val imp = implementability(and)
 
-    debug.println(s"atomic intersection: ${and.show} ~ ${imp.show}")
+    debug(s"atomic intersection: ${and.show} ~ ${imp.show}")
 
     imp match {
       case Unimplementable => Empty
@@ -407,7 +429,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     case Typed(expr, tpt) =>
       Typ(erase(expr.tpe.stripAnnots), true)
     case _ =>
-      debug.println(s"unknown pattern: $pat")
+      debug(s"unknown pattern: $pat")
       Empty
   }
 
@@ -446,7 +468,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   /** Is `tp1` a subtype of `tp2`?  */
   def isSubType(tp1: Type, tp2: Type): Boolean = {
     val res = tp1 <:< tp2
-    debug.println(s"${tp1.show} <:< ${tp2.show} = $res")
+    debug(s"${tp1.show} <:< ${tp2.show} = $res")
     res
   }
 
@@ -494,7 +516,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
         }
       }
 
-    debug.println(s"signature of ${unappSym.showFullName} ----> ${sig.map(_.show).mkString(", ")}")
+    debug(s"signature of ${unappSym.showFullName} ----> ${sig.map(_.show).mkString(", ")}")
 
     sig
   }
@@ -503,7 +525,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   def decompose(tp: Type): List[Space] = {
     val children = tp.classSymbol.children
 
-    debug.println(s"candidates for ${tp.show} : [${children.map(_.show).mkString(", ")}]")
+    debug(s"candidates for ${tp.show} : [${children.map(_.show).mkString(", ")}]")
 
     tp.dealias match {
       case AndType(tp1, tp2) =>
@@ -528,7 +550,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
             refine(tp, sym)
         } filter(_.exists)
 
-        debug.println(s"${tp.show} decomposes to [${parts.map(_.show).mkString(", ")}]")
+        debug(s"${tp.show} decomposes to [${parts.map(_.show).mkString(", ")}]")
 
         parts.map(Typ(_, true))
     }
@@ -562,11 +584,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     val resTp = instantiate(childTp, parent)(ctx.fresh.setNewTyperState())
 
     if (!resTp.exists)  {
-      debug.println(s"[refine] unqualified child ousted: ${childTp.show} !< ${parent.show}")
+      debug(s"[refine] unqualified child ousted: ${childTp.show} !< ${parent.show}")
       NoType
     }
     else {
-      debug.println(s"$child instantiated ------> $resTp")
+      debug(s"$child instantiated ------> $resTp")
       resTp.dealias
     }
   }
@@ -602,7 +624,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
             else if (variance == 1) mapOver(tp.underlying.hiBound)
             else mapOver(tp.underlying.loBound)
 
-          debug.println(s"$tp exposed to =====> $exposed")
+          debug(s"$tp exposed to =====> $exposed")
           exposed
         case _ =>
           mapOver(t)
@@ -636,7 +658,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
         else instUndetMap(protoTp1)
       }
       else {
-        debug.println(s"$protoTp1 <:< $protoTp2 = false")
+        debug(s"$protoTp1 <:< $protoTp2 = false")
         NoType
       }
     }
@@ -655,7 +677,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       tp.isRef(defn.BooleanClass) ||
       tp.classSymbol.is(allOf(Enum, Sealed))  // Enum value doesn't have Sealed flag
 
-    debug.println(s"decomposable: ${tp.show} = $res")
+    debug(s"decomposable: ${tp.show} = $res")
 
     res
   }
@@ -771,7 +793,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
 
     val Match(sel, cases) = tree
     val res = isCheckable(sel.tpe.widen.dealiasKeepAnnots)
-    debug.println(s"checkable: ${sel.show} = $res")
+    debug(s"checkable: ${sel.show} = $res")
     res
   }
 
@@ -782,7 +804,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
 
     val patternSpace = cases.map({ x =>
       val space = project(x.pat)
-      debug.println(s"${x.pat.show} ====> ${show(space)}")
+      debug(s"${x.pat.show} ====> ${show(space)}")
       space
     }).reduce((a, b) => Or(List(a, b)))
     val uncovered = simplify(minus(Typ(selTyp, true), patternSpace), aggressive = true)
@@ -807,9 +829,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       }.reduce((a, b) => Or(List(a, b)))
 
       val curr = project(cases(i).pat)
+      debug(s"---------------reachable? ${show(curr)}")
+      debug(s"prev: ${show(prevs)}")
 
-      debug.println(s"---------------reachable? ${show(curr)}")
-      debug.println(s"prev: ${show(prevs)}")
 
       if (isSubspace(curr, prevs)) {
         ctx.warning(MatchCaseUnreachable(), cases(i).body.pos)

From 9a3e016a34a6958b69b62f57b48985c8bc95fc7f Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@bright-it.com>
Date: Thu, 16 Nov 2017 11:25:16 +0100
Subject: [PATCH 4/6] Rename Space.scala to SpaceEngine.scala

---
 .../dotc/transform/patmat/{Space.scala => SpaceEngine.scala}      | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename compiler/src/dotty/tools/dotc/transform/patmat/{Space.scala => SpaceEngine.scala} (100%)

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/SpaceEngine.scala
similarity index 100%
rename from compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
rename to compiler/src/dotty/tools/dotc/transform/patmat/SpaceEngine.scala

From 6260c6283329b9c68228f5d37d453d5705591be7 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@bright-it.com>
Date: Thu, 16 Nov 2017 11:32:00 +0100
Subject: [PATCH 5/6] Use new code in SpaceEngine

Adapt tests to new output:
- exhausting: reflect improved GADT handling
- patmatexhaust: result of mirroring `scalac` guard handling
- t8511: this seems like the correct output for this test

All other changes are merely equivalent, but different, warnings.
---
 .../patmat/NaiveConstraintChecker.scala       |   1 -
 .../dotc/transform/patmat/SpaceEngine.scala   | 519 +++++++-----------
 .../dotc/transform/patmat/SpaceLogic.scala    |   1 -
 .../tools/dotc/transform/patmat/Spaces.scala  |   1 -
 tests/patmat/exhausting.check                 |   2 +-
 tests/patmat/gadt-basic.scala                 |  23 +
 tests/patmat/gadt-nontrivial.check            |   1 +
 tests/patmat/gadt-nontrivial.scala            |  12 +
 tests/patmat/gadt-nontrivial2.check           |   1 +
 tests/patmat/gadt-nontrivial2.scala.ignore    |  16 +
 tests/patmat/patmat-adt.check                 |   4 +-
 tests/patmat/patmatexhaust.check              |   1 +
 tests/patmat/t10019.check                     |   2 +-
 tests/patmat/t4526.check                      |   2 +-
 tests/patmat/t6420.check                      |   2 +-
 tests/patmat/t7466.check                      |   2 +-
 tests/patmat/t8511.check                      |   2 +-
 tests/patmat/t9129.check                      |   2 +-
 tests/patmat/t9351.check                      |   2 +-
 19 files changed, 254 insertions(+), 342 deletions(-)
 create mode 100644 tests/patmat/gadt-basic.scala
 create mode 100644 tests/patmat/gadt-nontrivial.check
 create mode 100644 tests/patmat/gadt-nontrivial.scala
 create mode 100644 tests/patmat/gadt-nontrivial2.check
 create mode 100644 tests/patmat/gadt-nontrivial2.scala.ignore

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/NaiveConstraintChecker.scala b/compiler/src/dotty/tools/dotc/transform/patmat/NaiveConstraintChecker.scala
index a0e6d9910f5e..4b754f0747fd 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/NaiveConstraintChecker.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/NaiveConstraintChecker.scala
@@ -1,5 +1,4 @@
 package dotty.tools.dotc.transform.patmat
-package `new logic`
 
 import dotty.tools.dotc.core.Contexts.Context
 
diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/SpaceEngine.scala b/compiler/src/dotty/tools/dotc/transform/patmat/SpaceEngine.scala
index 7d0692c24df7..f93696856b19 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/SpaceEngine.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/SpaceEngine.scala
@@ -21,263 +21,6 @@ import transform.SymUtils._
 import reporting.diagnostic.messages._
 import config.Printers.exhaustivity
 
-/** Space logic for checking exhaustivity and unreachability of pattern matching
- *
- *  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
- *      3. A union of spaces `S1 | S2 | ...` is a space
- *      4. `Prod(S1, S2, ..., Sn)` is a product space.
- *
- *  For the problem of exhaustivity check, its formulation in terms of space is as follows:
- *
- *      Is the space Typ(T) a subspace of the union of space covered by all the patterns?
- *
- *  The problem of unreachable patterns can be formulated as follows:
- *
- *      Is the space covered by a pattern a subspace of the space covered by previous patterns?
- *
- *  Assumption:
- *    (1) One case class cannot be inherited directly or indirectly by another
- *        case class.
- *    (2) Inheritance of a case class cannot be well handled by the algorithm.
- *
- */
-
-
-/** space definition */
-sealed trait Space
-
-/** Empty space */
-case object Empty extends Space
-
-/** Space representing the set of all values of a type
- *
- * @param tp: the type this space represents
- * @param decomposed: does the space result from decomposition? Used for pretty print
- *
- */
-case class Typ(tp: Type, decomposed: Boolean) extends Space
-
-/** Space representing an extractor pattern */
-case class Prod(tp: Type, unappTp: Type, unappSym: Symbol, params: List[Space], full: Boolean) extends Space
-
-/** Union of spaces */
-case class Or(spaces: List[Space]) extends Space
-
-/** abstract space logic */
-trait SpaceLogic {
-  /** Is `tp1` a subtype of `tp2`? */
-  def isSubType(tp1: Type, tp2: Type): Boolean
-
-  /** Is `tp1` the same type as `tp2`? */
-  def isEqualType(tp1: Type, tp2: Type): Boolean
-
-  /** Return a space containing the values of both types.
-   *
-   * The types should be atomic (non-decomposable) and unrelated (neither
-   * should be a subtype of the other).
-   */
-  def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type): Space
-
-  /** Is the type `tp` decomposable? i.e. all values of the type can be covered
-   *  by its decomposed types.
-   *
-   * Abstract sealed class, OrType, Boolean and Java enums can be decomposed.
-   */
-  def canDecompose(tp: Type): Boolean
-
-  /** Return term parameter types of the extractor `unapp` */
-  def signature(unapp: Type, unappSym: Symbol, argLen: Int): List[Type]
-
-  /** Get components of decomposable types */
-  def decompose(tp: Type): List[Space]
-
-  /** Display space in string format */
-  def show(sp: Space): String
-
-  /** Simplify space using the laws, there's no nested union after simplify
-   *
-   *  @param aggressive if true and OR space has less than 5 components, `simplify` will
-   *                    collapse `sp1 | sp2` to `sp1` if `sp2` is a subspace of `sp1`.
-   *
-   *                    This reduces noise in counterexamples.
-   */
-  def simplify(space: Space, aggressive: Boolean = false): Space = space match {
-    case Prod(tp, fun, sym, spaces, full) =>
-      val sp = Prod(tp, fun, sym, spaces.map(simplify(_)), full)
-      if (sp.params.contains(Empty)) Empty
-      else sp
-    case Or(spaces) =>
-      val set = spaces.map(simplify(_)).flatMap {
-        case Or(ss) => ss
-        case s => Seq(s)
-      } filter (_ != Empty)
-
-      if (set.isEmpty) Empty
-      else if (set.size == 1) set.toList(0)
-      else if (aggressive && spaces.size < 5) {
-        val res = set.map(sp => (sp, set.filter(_ ne sp))).find {
-          case (sp, sps) =>
-            isSubspace(sp, Or(sps))
-        }
-        if (res.isEmpty) Or(set)
-        else simplify(Or(res.get._2), aggressive)
-      }
-      else Or(set)
-    case Typ(tp, _) =>
-      if (canDecompose(tp) && decompose(tp).isEmpty) Empty
-      else space
-    case _ => space
-  }
-
-  /** Flatten space to get rid of `Or` for pretty print */
-  def flatten(space: Space): List[Space] = space match {
-    case Prod(tp, fun, sym, spaces, full) =>
-      spaces.map(flatten) match {
-        case Nil => Prod(tp, fun, sym, Nil, full) :: Nil
-        case ss  =>
-          ss.foldLeft(List[Prod]()) { (acc, flat) =>
-            if (acc.isEmpty) flat.map(s => Prod(tp, fun, sym, s :: Nil, full))
-            else for (Prod(tp, fun, sym, ss, full) <- acc; s <- flat) yield Prod(tp, fun, sym, ss :+ s, full)
-          }
-      }
-    case Or(spaces) =>
-      spaces.flatMap(flatten _)
-    case _ => List(space)
-  }
-
-  /** Is `a` a subspace of `b`? Equivalent to `a - b == Empty`, but faster */
-  def isSubspace(a: Space, b: Space): Boolean = {
-    def tryDecompose1(tp: Type) = canDecompose(tp) && isSubspace(Or(decompose(tp)), b)
-    def tryDecompose2(tp: Type) = canDecompose(tp) && isSubspace(a, Or(decompose(tp)))
-
-    val res = (simplify(a), b) match {
-      case (Empty, _) => true
-      case (_, Empty) => false
-      case (Or(ss), _) =>
-        ss.forall(isSubspace(_, b))
-      case (Typ(tp1, _), Typ(tp2, _)) =>
-        isSubType(tp1, tp2)
-      case (Typ(tp1, _), Or(ss)) =>  // optimization: don't go to subtraction too early
-        ss.exists(isSubspace(a, _)) || tryDecompose1(tp1)
-      case (_, Or(_)) =>
-        simplify(minus(a, b)) == Empty
-      case (Prod(tp1, _, _, _, _), Typ(tp2, _)) =>
-        isSubType(tp1, tp2)
-      case (Typ(tp1, _), Prod(tp2, fun, sym, ss, full)) =>
-        // approximation: a type can never be fully matched by a partial extractor
-        full && isSubType(tp1, tp2) && isSubspace(Prod(tp2, fun, sym, signature(fun, sym, ss.length).map(Typ(_, false)), full), b)
-      case (Prod(_, fun1, sym1, ss1, _), Prod(_, fun2, sym2, ss2, _)) =>
-        sym1 == sym2 && isEqualType(fun1, fun2) && ss1.zip(ss2).forall((isSubspace _).tupled)
-    }
-
-    exhaustivity.println(s"${show(a)} < ${show(b)} = $res")
-
-    res
-  }
-
-  /** Intersection of two spaces  */
-  def intersect(a: Space, b: Space): Space = {
-    def tryDecompose1(tp: Type) = intersect(Or(decompose(tp)), b)
-    def tryDecompose2(tp: Type) = intersect(a, Or(decompose(tp)))
-
-    val res: Space = (a, b) match {
-      case (Empty, _) | (_, Empty) => Empty
-      case (_, Or(ss)) => Or(ss.map(intersect(a, _)).filterConserve(_ ne Empty))
-      case (Or(ss), _) => Or(ss.map(intersect(_, b)).filterConserve(_ ne Empty))
-      case (Typ(tp1, _), Typ(tp2, _)) =>
-        if (isSubType(tp1, tp2)) a
-        else if (isSubType(tp2, tp1)) b
-        else if (canDecompose(tp1)) tryDecompose1(tp1)
-        else if (canDecompose(tp2)) tryDecompose2(tp2)
-        else intersectUnrelatedAtomicTypes(tp1, tp2)
-      case (Typ(tp1, _), Prod(tp2, fun, _, ss, true)) =>
-        if (isSubType(tp2, tp1)) b
-        else if (isSubType(tp1, tp2)) a // problematic corner case: inheriting a case class
-        else if (canDecompose(tp1)) tryDecompose1(tp1)
-        else Empty
-      case (Typ(tp1, _), Prod(tp2, _, _, _, false)) =>
-        if (isSubType(tp1, tp2) || isSubType(tp2, tp1)) b  // prefer extractor space for better approximation
-        else if (canDecompose(tp1)) tryDecompose1(tp1)
-        else Empty
-      case (Prod(tp1, fun, _, ss, true), Typ(tp2, _)) =>
-        if (isSubType(tp1, tp2)) a
-        else if (isSubType(tp2, tp1)) a  // problematic corner case: inheriting a case class
-        else if (canDecompose(tp2)) tryDecompose2(tp2)
-        else Empty
-      case (Prod(tp1, _, _, _, false), Typ(tp2, _)) =>
-        if (isSubType(tp1, tp2) || isSubType(tp2, tp1)) a
-        else if (canDecompose(tp2)) tryDecompose2(tp2)
-        else Empty
-      case (Prod(tp1, fun1, sym1, ss1, full), Prod(tp2, fun2, sym2, ss2, _)) =>
-        if (sym1 != sym2 || !isEqualType(fun1, fun2)) Empty
-        else if (ss1.zip(ss2).exists(p => simplify(intersect(p._1, p._2)) == Empty)) Empty
-        else Prod(tp1, fun1, sym1, ss1.zip(ss2).map((intersect _).tupled), full)
-    }
-
-    exhaustivity.println(s"${show(a)} & ${show(b)} = ${show(res)}")
-
-    res
-  }
-
-  /** The space of a not covered by b */
-  def minus(a: Space, b: Space): Space = {
-    def tryDecompose1(tp: Type) = minus(Or(decompose(tp)), b)
-    def tryDecompose2(tp: Type) = minus(a, Or(decompose(tp)))
-
-    val res = (a, b) match {
-      case (Empty, _) => Empty
-      case (_, Empty) => a
-      case (Typ(tp1, _), Typ(tp2, _)) =>
-        if (isSubType(tp1, tp2)) Empty
-        else if (canDecompose(tp1)) tryDecompose1(tp1)
-        else if (canDecompose(tp2)) tryDecompose2(tp2)
-        else a
-      case (Typ(tp1, _), Prod(tp2, fun, sym, ss, true)) =>
-        // rationale: every instance of `tp1` is covered by `tp2(_)`
-        if (isSubType(tp1, tp2)) minus(Prod(tp2, fun, sym, signature(fun, sym, ss.length).map(Typ(_, false)), true), b)
-        else if (canDecompose(tp1)) tryDecompose1(tp1)
-        else a
-      case (_, Or(ss)) =>
-        ss.foldLeft(a)(minus)
-      case (Or(ss), _) =>
-        Or(ss.map(minus(_, b)))
-      case (Prod(tp1, fun, _, ss, true), Typ(tp2, _)) =>
-        // uncovered corner case: tp2 :< tp1
-        if (isSubType(tp1, tp2)) Empty
-        else if (simplify(a) == Empty) Empty
-        else if (canDecompose(tp2)) tryDecompose2(tp2)
-        else a
-      case (Prod(tp1, _, _, _, false), Typ(tp2, _)) =>
-        if (isSubType(tp1, tp2)) Empty
-        else a
-      case (Typ(tp1, _), Prod(tp2, _, _, _, false)) =>
-        a  // approximation
-      case (Prod(tp1, fun1, sym1, ss1, full), Prod(tp2, fun2, sym2, ss2, _)) =>
-        if (sym1 != sym2 || !isEqualType(fun1, fun2)) a
-        else if (ss1.zip(ss2).exists(p => simplify(intersect(p._1, p._2)) == Empty)) a
-        else if (ss1.zip(ss2).forall((isSubspace _).tupled)) Empty
-        else
-          // `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)`
-          Or(ss1.zip(ss2).map((minus _).tupled).zip(0 to ss2.length - 1).map {
-              case (ri, i) => Prod(tp1, fun1, sym1, ss1.updated(i, ri), full)
-            })
-
-    }
-
-    exhaustivity.println(s"${show(a)} - ${show(b)} = ${show(res)}")
-
-    res
-  }
-}
-
 object SpaceEngine {
   private sealed trait Implementability {
     def show(implicit ctx: Context) = this match {
@@ -288,6 +31,31 @@ object SpaceEngine {
   private case object ClassOrTrait extends Implementability
   private case class SubclassOf(classSyms: List[Symbol]) extends Implementability
   private case object Unimplementable extends Implementability
+
+
+  /** Returns a _product_ list of list - each list in the output
+   * contains exactly one element from each list in the input.
+   *
+   * ```
+   * productList(List(
+   *   List(a1, a2),
+   *   List(b1, b2),
+   *   List(c1, c2)
+   * )) == List(
+   *   List(a1, b1, c1),
+   *   List(a1, b1, c2),
+   *   List(a1, b2, c1),
+   *   ???,
+   *   List(a2, b2, c2)
+   * )
+   * ```
+   */
+  private def productList[T](ls: List[List[T]]): List[List[T]] = ls match {
+    case Nil => List(Nil)
+    case hs :: ts =>
+      val ats = productList(ts)
+      hs.flatMap { h => ats.map(h :: _) }
+  }
 }
 
 /** Scala implementation of space logic */
@@ -323,6 +91,19 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     exhaustivity.println(indentStr + msg)
   }
 
+  def debugShow(s: ConstrainedSpace): String = {
+    s.vec.iterator.map(debugShow).mkString("[", ", ", "]")
+  }
+
+  def debugShow(s: Space): String = s match {
+    case Typ(c: ConstantType, _) => s"Typ<${c.value.show}>"
+    case Typ(tp: TermRef, _) => s"Typ<${tp.symbol.showName}>"
+    case Typ(tp, _) => s"Typ<${showType(tp)}>"
+    case Prod(tp, _, _, params, full) =>
+      val description = if (full) "Prod" else "ProdPartial"
+      params.iterator.map(debugShow).mkString(s"$description<${showType(tp)}>(", ", ", ")")
+  }
+
   /** Checks if it's possible to create a trait/class which is a subtype of `tp`.
    *
    * - doesn't handle member collisions (will not declare a type unimplementable because of one)
@@ -380,7 +161,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       }
   }
 
-  override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type) = {
+  override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type): Option[Space] = {
     val and = AndType(tp1, tp2)
     // Precondition: !(tp1 <:< tp2) && !(tp2 <:< tp1)
     // Then, no leaf of the and-type tree `and` is a subtype of `and`.
@@ -391,8 +172,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     debug(s"atomic intersection: ${and.show} ~ ${imp.show}")
 
     imp match {
-      case Unimplementable => Empty
-      case _ => Typ(and, true)
+      case Unimplementable => None
+      case _ => Some(Typ(and, true))
     }
   }
 
@@ -404,33 +185,53 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       productArity(unapp.tpe.widen.finalResultType) > 0
   }
 
-  /** Return the space that represents the pattern `pat`
+  /** Returns a list of [[ConstrainedSpace]]s representing `_case` pattern.
+   *
+   * The returned list has more than one element if the pattern contains or-patterns anywhere.
    */
-  def project(pat: Tree): Space = pat match {
-    case Literal(c) =>
-      if (c.value.isInstanceOf[Symbol])
-        Typ(c.value.asInstanceOf[Symbol].termRef, false)
-      else
-        Typ(ConstantType(c), false)
-    case _: BackquotedIdent => Typ(pat.tpe, false)
+  def project(_case: tpd.CaseDef): List[ConstrainedSpace] = {
+    val spaces = projectPattern(_case.pat)
+    val termConstraints = projectGuard(_case.guard)
+    spaces.map { s =>
+      ConstrainedSpace(List(s), termConstraints, Nil)
+    }
+  }
+
+  def projectPattern(pat: Tree): List[Space] = pat match {
+    case Literal(c) => c.value match {
+      case s: Symbol => List(Typ(s.termRef))
+      case _ => List(Typ(ConstantType(c)))
+    }
+    case _: BackquotedIdent => List(Typ(pat.tpe))
     case Ident(_) | Select(_, _) =>
-      Typ(pat.tpe.stripAnnots, false)
-    case Alternative(trees) => Or(trees.map(project(_)))
-    case Bind(_, pat) => project(pat)
+      List(Typ(pat.tpe.stripAnnots))
+    case Alternative(trees) => trees.flatMap(projectPattern)
+    case Bind(_, pat) => projectPattern(pat)
     case UnApply(fun, _, pats) =>
       if (fun.symbol.name == nme.unapplySeq)
         if (fun.symbol.owner == scalaSeqFactoryClass)
-          projectSeq(pats)
-        else
-          Prod(pat.tpe.stripAnnots, fun.tpe.widen, fun.symbol, projectSeq(pats) :: Nil, irrefutable(fun))
-      else
-        Prod(pat.tpe.stripAnnots, fun.tpe.widen, fun.symbol, pats.map(project), irrefutable(fun))
-    case Typed(pat @ UnApply(_, _, _), _) => project(pat)
-    case Typed(expr, tpt) =>
-      Typ(erase(expr.tpe.stripAnnots), true)
+          projectSeqPattern(pats)
+        else projectSeqPattern(pats).map { s =>
+          Prod(pat.tpe.stripAnnots, fun.tpe.widen, fun.symbol, List(s), irrefutable(fun))
+        }
+      else productList(pats.map(projectPattern)).map { spaces =>
+        Prod(pat.tpe.stripAnnots, fun.tpe.widen, fun.symbol, spaces, irrefutable(fun))
+      }
+    case Typed(pat @ UnApply(_, _, _), _) => projectPattern(pat)
+    case Typed(expr, _) =>
+      List(Typ(erase(expr.tpe.stripAnnots), true))
     case _ =>
       debug(s"unknown pattern: $pat")
-      Empty
+      Nil
+  }
+
+  def projectGuard(guard: Tree): List[TermConstraint] = guard match {
+    case empty if empty.isEmpty => Nil
+    case Literal(c) if c.value.isInstanceOf[Boolean] =>
+      if (c.booleanValue) List(AlwaysSatisfied) else List(AlwaysSatisfied.neg)
+    case _ => Nil // scalac gives up when guard can't be constant folded
+    // TODO: return this if a flag is toggled on to emit more accurate warnings
+    // List(Dummy)
   }
 
   /* Erase a type binding according to erasure semantics in pattern matching */
@@ -447,21 +248,22 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     case _ => tp
   }
 
-  /** Space of the pattern: unapplySeq(a, b, c: _*)
-   */
-  def projectSeq(pats: List[Tree]): Space = {
-    if (pats.isEmpty) return Typ(scalaNilType, false)
+  def projectSeqPattern(pats: List[Tree]): List[Space] = {
+    if (pats.isEmpty) return List(Typ(scalaNilType))
 
     val (items, zero) = if (pats.last.tpe.isRepeatedParam)
-      (pats.init, Typ(scalaListType.appliedTo(pats.last.tpe.argTypes.head), false))
+      (pats.init, Typ(scalaListType.appliedTo(pats.last.tpe.argTypes.head)))
     else
-      (pats, Typ(scalaNilType, false))
+      (pats, Typ(scalaNilType))
+
+    val consTp = scalaConsType.appliedTo(pats.head.tpe.widen)
+    val unapplySym = consTp.classSymbol.linkedClass.info.member(nme.unapply).symbol
+    val unapplyTp = unapplySym.info.appliedTo(pats.head.tpe.widen)
 
-    items.foldRight[Space](zero) { (pat, acc) =>
-      val consTp = scalaConsType.appliedTo(pats.head.tpe.widen)
-      val unapplySym = consTp.classSymbol.linkedClass.info.member(nme.unapply).symbol
-      val unapplyTp = unapplySym.info.appliedTo(pats.head.tpe.widen)
-      Prod(consTp, unapplyTp, unapplySym, project(pat) :: acc :: Nil, true)
+    productList(items.map(projectPattern)).map { spaces =>
+      spaces.foldRight[Space](zero) { (head, tail) =>
+        Prod(consTp, unapplyTp, unapplySym, List(head, tail), true)
+      }
     }
   }
 
@@ -521,27 +323,49 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     sig
   }
 
+  def gadtConstraints(parentTp: Type, childTp: Type): List[TypeConstraint] = {
+    val candidates = parentTp.classSymbol.typeParams
+    val appliedInfos = childTp.baseType(parentTp.classSymbol).argInfos
+
+    candidates.iterator.zip(appliedInfos.iterator).flatMap {
+      case (sym, info) if sym.variance == 0 =>
+        Some(TypeEquality(sym.typeRef, info))
+      case _ => None
+    }.toList
+  }
+
   /** Decompose a type into subspaces -- assume the type can be decomposed */
-  def decompose(tp: Type): List[Space] = {
+  def decompose(a: ConstrainedSpace): List[ConstrainedSpace] = {
+    val (Typ(tp, _)) :: t = a.vec
+
     val children = tp.classSymbol.children
 
     debug(s"candidates for ${tp.show} : [${children.map(_.show).mkString(", ")}]")
 
     tp.dealias match {
       case AndType(tp1, tp2) =>
-        intersect(Typ(tp1, false), Typ(tp2, false)) match {
-          case Or(spaces) => spaces
-          case Empty => Nil
-          case space => List(space)
-        }
-      case OrType(tp1, tp2) => List(Typ(tp1, true), Typ(tp2, true))
+        intersect(
+          a.withVec(List(Typ(tp1, true))),
+          a.withVec(List(Typ(tp2, true)))
+        ).map { c => c.withVec(c.vec ::: t)}
+
+      case OrType(tp1, tp2) =>
+        List(
+          a.withVec(Typ(tp1, true) :: t),
+          a.withVec(Typ(tp2, true) :: t)
+        )
+
       case tp if tp.isRef(defn.BooleanClass) =>
         List(
-          Typ(ConstantType(Constant(true)), true),
-          Typ(ConstantType(Constant(false)), true)
+          a.withVec(Typ(ConstantType(Constant(true)), true) :: t),
+          a.withVec(Typ(ConstantType(Constant(false)), true) :: t)
         )
+
       case tp if tp.classSymbol.is(Enum) =>
-        children.map(sym => Typ(sym.termRef, true))
+        children.map { sym =>
+          a.withVec(Typ(sym.termRef, true) :: t)
+        }
+
       case tp =>
         val parts = children.map { sym =>
           if (sym.is(ModuleClass))
@@ -552,7 +376,14 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
 
         debug(s"${tp.show} decomposes to [${parts.map(_.show).mkString(", ")}]")
 
-        parts.map(Typ(_, true))
+        parts.map { childTp =>
+          val constrs = gadtConstraints(tp, childTp)
+
+          a.copy(
+            vec = Typ(childTp, true) :: t,
+            typeConstraints = constrs ::: a.typeConstraints
+          )
+        }
     }
   }
 
@@ -665,7 +496,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   }
 
   /** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
-  def canDecompose(tp: Type): Boolean = {
+  def canDecompose(tp: Type): Boolean =
+  doDebug[Boolean](s"decomposable: ${tp.show}", res => s"= $res") {
     val dealiasedTp = tp.dealias
     val res = tp.classSymbol.is(allOf(Abstract, Sealed)) ||
       tp.classSymbol.is(allOf(Trait, Sealed)) ||
@@ -677,8 +509,6 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       tp.isRef(defn.BooleanClass) ||
       tp.classSymbol.is(allOf(Enum, Sealed))  // Enum value doesn't have Sealed flag
 
-    debug(s"decomposable: ${tp.show} = $res")
-
     res
   }
 
@@ -731,7 +561,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   }
 
   /** Display spaces */
-  def show(s: Space): String = {
+  def show(spaces: List[Space]): String = {
     def params(tp: Type): List[Type] = tp.classSymbol.primaryConstructor.info.firstParamTypes
 
     /** does the companion object of the given symbol have custom unapply */
@@ -742,7 +572,6 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     }
 
     def doShow(s: Space, mergeList: Boolean = false): String = s match {
-      case Empty => ""
       case Typ(c: ConstantType, _) => c.value.show
       case Typ(tp: TermRef, _) => tp.symbol.showName
       case Typ(tp, decomposed) =>
@@ -759,7 +588,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
           showType(tp) + params(tp).map(_ => "_").mkString("(", ", ", ")")
         else if (decomposed) "_: " + showType(tp)
         else "_"
-      case Prod(tp, fun, sym, params, _) =>
+      case Prod(tp, _, sym, params, _) =>
         if (ctx.definitions.isTupleType(tp))
           "(" + params.map(doShow(_)).mkString(", ") + ")"
         else if (tp.isRef(scalaConsType.symbol))
@@ -767,11 +596,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
           else params.map(doShow(_, true)).filter(_ != "Nil").mkString("List(", ", ", ")")
         else
           showType(sym.owner.typeRef) + params.map(doShow(_)).mkString("(", ", ", ")")
-      case Or(_) =>
-        throw new Exception("incorrect flatten result " + s)
     }
 
-    flatten(s).map(doShow(_, false)).distinct.mkString(", ")
+    spaces.map(doShow(_, false)).distinct.mkString(", ")
   }
 
   def checkable(tree: Match): Boolean = {
@@ -801,20 +628,50 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     val Match(sel, cases) = _match
     val selTyp = sel.tpe.widen.dealias
 
+    val projectedPats = cases.flatMap { x =>
+      val spaces = project(x)
+      debug(s"${x.pat.show} ====> ${debugShow(spaces)}")
+      spaces.map { (_, x.body.pos) }
+    }
+
+    val uncoveredSpaces = {
+      var currentPossibleScrutinees =
+        List(ConstrainedSpace(List(Typ(selTyp, decomposed = true)), Nil, Nil))
 
-    val patternSpace = cases.map({ x =>
-      val space = project(x.pat)
-      debug(s"${x.pat.show} ====> ${show(space)}")
-      space
-    }).reduce((a, b) => Or(List(a, b)))
-    val uncovered = simplify(minus(Typ(selTyp, true), patternSpace), aggressive = true)
+      for { (space, pos) <- projectedPats } {
+        if (!UseOldRedundancyCheck) {
+          val possibleMatches = currentPossibleScrutinees
+            .flatMap(intersect(_, space))
+            .filterNot(NaiveConstraintChecker.hasUnsatisfiableConstraints)
+
+          if (possibleMatches.isEmpty) {
+            ctx.warning(MatchCaseUnreachable(), pos)
+          }
+        }
 
-    if (uncovered != Empty)
-      ctx.warning(PatternMatchExhaustivity(show(uncovered)), sel.pos)
+        currentPossibleScrutinees = currentPossibleScrutinees
+          .flatMap(subtract(_, space))
+          .filterNot(NaiveConstraintChecker.hasUnsatisfiableConstraints)
+      }
+
+      currentPossibleScrutinees
+    }
+
+    if (uncoveredSpaces.nonEmpty) {
+      debug("Uncovered spaces:")
+      uncoveredSpaces.foreach { _space =>
+        debug(s"\t${debugShow(_space)}")
+      }
+
+      assert( uncoveredSpaces.forall(_.vec.length == 1) )
+      ctx.warning(PatternMatchExhaustivity(uncoveredSpaces.map(show).mkString(", ")), sel.pos)
+    } else {
+      debug("No uncovered spaces.")
+    }
   }
 
-  def checkRedundancy(_match: Match): Unit = {
-    val Match(sel, cases) = _match
+  def checkRedundancy(_match: Match): Unit = if (UseOldRedundancyCheck) {
+    val Match(_, cases) = _match
     // ignore selector type for now
     // val selTyp = sel.tpe.widen.dealias
 
@@ -823,19 +680,23 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     // starts from the second, the first can't be redundant
     (1 until cases.length).foreach { i =>
       // in redundancy check, take guard as false in order to soundly approximate
-      val prevs = cases.take(i).map { x =>
-        if (x.guard.isEmpty) project(x.pat)
-        else Empty
-      }.reduce((a, b) => Or(List(a, b)))
+      val prevs: List[ConstrainedSpace] = cases.take(i).flatMap { x =>
+        if (x.guard.isEmpty) project(x) else Nil
+      }
 
-      val curr = project(cases(i).pat)
-      debug(s"---------------reachable? ${show(curr)}")
-      debug(s"prev: ${show(prevs)}")
+      val curr = project(cases(i))
 
+      debug(s"---------------reachable? ${debugShow(curr)}")
+      debug(s"prev: ${debugShow(prevs)}")
 
-      if (isSubspace(curr, prevs)) {
+      def doSubtract(as: List[ConstrainedSpace], bs: List[ConstrainedSpace]) =
+        bs.foldLeft(as) { (as, b) => as.flatMap(subtract(_, b)) }
+
+      if (doSubtract(curr, prevs).isEmpty) {
         ctx.warning(MatchCaseUnreachable(), cases(i).body.pos)
       }
     }
   }
+
+  val UseOldRedundancyCheck: Boolean = true
 }
diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/SpaceLogic.scala b/compiler/src/dotty/tools/dotc/transform/patmat/SpaceLogic.scala
index a5ca403c2d43..db8f9e2c837d 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/SpaceLogic.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/SpaceLogic.scala
@@ -1,5 +1,4 @@
 package dotty.tools.dotc.transform.patmat
-package `new logic`
 
 import dotty.tools.dotc.core.Symbols.Symbol
 import dotty.tools.dotc.core.Types.Type
diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala
index b5cbb2264da5..a74c94f9ab20 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala
@@ -1,5 +1,4 @@
 package dotty.tools.dotc.transform.patmat
-package `new logic`
 
 import dotty.tools.dotc.core.Symbols.Symbol
 import dotty.tools.dotc.core.Types.Type
diff --git a/tests/patmat/exhausting.check b/tests/patmat/exhausting.check
index d17c5f36bc80..4b8fa9fa72a4 100644
--- a/tests/patmat/exhausting.check
+++ b/tests/patmat/exhausting.check
@@ -3,4 +3,4 @@
 32: Pattern Match Exhaustivity: List(_, _: _*)
 39: Pattern Match Exhaustivity: Bar3
 44: Pattern Match Exhaustivity: (Bar2, Bar2)
-53: Pattern Match Exhaustivity: (Bar2, Bar2), (Bar2, Bar1), (Bar1, Bar3), (Bar1, Bar2)
+53: Pattern Match Exhaustivity: (Bar2, Bar2)
diff --git a/tests/patmat/gadt-basic.scala b/tests/patmat/gadt-basic.scala
new file mode 100644
index 000000000000..228b713f75bc
--- /dev/null
+++ b/tests/patmat/gadt-basic.scala
@@ -0,0 +1,23 @@
+object O1 {
+  sealed trait Expr[T]
+  case class BExpr(bool: Boolean) extends Expr[Boolean]
+  case class IExpr(int: Int) extends Expr[Int]
+
+  def join[T](e1: Expr[T], e2: Expr[T]): Expr[T] = (e1, e2) match {
+    case (IExpr(i1), IExpr(i2)) => IExpr(i1 + i2)
+    case (BExpr(b1), BExpr(b2)) => BExpr(b1 & b2)
+  }
+}
+
+object O2 {
+  sealed trait GADT[A, B]
+  case object IntString extends GADT[Int, String]
+  case object IntFloat extends GADT[Int, Float]
+  case object FloatFloat extends GADT[Float, Float]
+
+  def m[A, B](g1: GADT[A, B], g2: GADT[A, B]) = (g1, g2) match {
+    case (IntString, IntString) => ;
+    case (IntFloat, IntFloat) => ;
+    case (FloatFloat, FloatFloat) => ;
+  }
+}
diff --git a/tests/patmat/gadt-nontrivial.check b/tests/patmat/gadt-nontrivial.check
new file mode 100644
index 000000000000..c005f8d1c0cc
--- /dev/null
+++ b/tests/patmat/gadt-nontrivial.check
@@ -0,0 +1 @@
+7: Pattern Match Exhaustivity: (IntExpr(_), AddExpr(_, _))
diff --git a/tests/patmat/gadt-nontrivial.scala b/tests/patmat/gadt-nontrivial.scala
new file mode 100644
index 000000000000..a9ab5f3da7a2
--- /dev/null
+++ b/tests/patmat/gadt-nontrivial.scala
@@ -0,0 +1,12 @@
+object O {
+  sealed trait Expr[T]
+  case class BoolExpr(v: Boolean) extends Expr[Boolean]
+  case class IntExpr(v: Int) extends Expr[Int]
+  case class AddExpr(e1: Expr[Int], e2: Expr[Int]) extends Expr[Int]
+
+  def join[T](e1: Expr[T], e2: Expr[T]): Expr[T] = (e1, e2) match {
+    case (BoolExpr(b1), BoolExpr(b2)) => BoolExpr(b1 && b2)
+    case (IntExpr(i1), IntExpr(i2)) => IntExpr(i1 + i2)
+    case (AddExpr(ei1, ei2), ie) => join(join(ei1, ei2), ie)
+  }
+}
diff --git a/tests/patmat/gadt-nontrivial2.check b/tests/patmat/gadt-nontrivial2.check
new file mode 100644
index 000000000000..7598863e53c8
--- /dev/null
+++ b/tests/patmat/gadt-nontrivial2.check
@@ -0,0 +1 @@
+13:
diff --git a/tests/patmat/gadt-nontrivial2.scala.ignore b/tests/patmat/gadt-nontrivial2.scala.ignore
new file mode 100644
index 000000000000..d6fd595f004d
--- /dev/null
+++ b/tests/patmat/gadt-nontrivial2.scala.ignore
@@ -0,0 +1,16 @@
+object O {
+  sealed trait Nat
+  type Zero = Nat
+  sealed trait Succ[N <: Nat] extends Nat
+
+  sealed trait NVec[N <: Nat, +A]
+  case object NEmpty extends NVec[Zero, Nothing]
+  case class NCons[N <: Nat, +A](head: A, tail: NVec[N, A]) extends NVec[Succ[N], A]
+
+  def nzip[N <: Nat, A, B](v1: NVec[N, A], v2: NVec[N, B]): NVec[N, (A, B)] =
+    (v1, v2) match {
+      case (NEmpty, NEmpty) => NEmpty
+      case (NCons(a, atail), NCons(b, btail)) =>
+        NCons((a, b), nzip(atail, btail))
+    }
+}
diff --git a/tests/patmat/patmat-adt.check b/tests/patmat/patmat-adt.check
index 7a938792fee8..f771aa1e35a8 100644
--- a/tests/patmat/patmat-adt.check
+++ b/tests/patmat/patmat-adt.check
@@ -1,5 +1,5 @@
 7: Pattern Match Exhaustivity: Bad(Good(_)), Good(Bad(_))
 19: Pattern Match Exhaustivity: Some(_)
-24: Pattern Match Exhaustivity: (_, Some(_))
-29: Pattern Match Exhaustivity: (None, None), (Some(_), Some(_))
+24: Pattern Match Exhaustivity: (Some(_), Some(_)), (None, Some(_))
+29: Pattern Match Exhaustivity: (Some(_), Some(_)), (None, None)
 50: Pattern Match Exhaustivity: LetL(BooleanLit), LetL(IntLit)
diff --git a/tests/patmat/patmatexhaust.check b/tests/patmat/patmatexhaust.check
index e5e7ac397383..4b7007629fc0 100644
--- a/tests/patmat/patmatexhaust.check
+++ b/tests/patmat/patmatexhaust.check
@@ -2,6 +2,7 @@
 11: Pattern Match Exhaustivity: Bar(_)
 23: Pattern Match Exhaustivity: (Qult(), Qult()), (Kult(_), Kult(_))
 49: Pattern Match Exhaustivity: _: Gp
+53: Pattern Match Exhaustivity: _
 59: Pattern Match Exhaustivity: Nil
 75: Pattern Match Exhaustivity: _: B
 100: Pattern Match Exhaustivity: _: C1
diff --git a/tests/patmat/t10019.check b/tests/patmat/t10019.check
index 49f5b152d1fb..afe1f8bca10c 100644
--- a/tests/patmat/t10019.check
+++ b/tests/patmat/t10019.check
@@ -1,2 +1,2 @@
-2: Pattern Match Exhaustivity: (List(_, _: _*), Nil), (List(_, _: _*), List(_, _, _: _*)), (Nil, List(_, _: _*)), (List(_, _, _: _*), List(_, _: _*))
+2: Pattern Match Exhaustivity: (Nil, List(_, _: _*)), (List(_), Nil), (List(_), List(_, _, _: _*)), (List(_, _, _: _*), _: List)
 11: Pattern Match Exhaustivity: (Foo(None), Foo(_))
diff --git a/tests/patmat/t4526.check b/tests/patmat/t4526.check
index 802d0fe22d54..ac3ef01bcc23 100644
--- a/tests/patmat/t4526.check
+++ b/tests/patmat/t4526.check
@@ -1,3 +1,3 @@
 2: Pattern Match Exhaustivity: _: Int
 7: Pattern Match Exhaustivity: (_, _)
-12: Pattern Match Exhaustivity: (false, false), (true, true)
+12: Pattern Match Exhaustivity: (true, true), (false, false)
diff --git a/tests/patmat/t6420.check b/tests/patmat/t6420.check
index cacdd5c8c92e..024719ef5f30 100644
--- a/tests/patmat/t6420.check
+++ b/tests/patmat/t6420.check
@@ -1 +1 @@
-5: Pattern Match Exhaustivity: (_: List, Nil), (_: List, List(true, _: _*)), (_: List, List(false, _: _*))
+5: Pattern Match Exhaustivity: (Nil, _: List), (List(true, _: _*), _: List), (List(false, _: _*), _: List)
diff --git a/tests/patmat/t7466.check b/tests/patmat/t7466.check
index dfd3b3061f03..7e6210cf021e 100644
--- a/tests/patmat/t7466.check
+++ b/tests/patmat/t7466.check
@@ -1 +1 @@
-8: Pattern Match Exhaustivity: (_, true), (_, false)
+8: Pattern Match Exhaustivity: (true, _), (false, _)
diff --git a/tests/patmat/t8511.check b/tests/patmat/t8511.check
index 6f63f1040f5b..121e0ab874e0 100644
--- a/tests/patmat/t8511.check
+++ b/tests/patmat/t8511.check
@@ -1 +1 @@
-18: Pattern Match Exhaustivity: Baz(), Bar(_)
+18: Pattern Match Exhaustivity: EatsExhaustiveWarning(_), Baz(), Bar(_)
diff --git a/tests/patmat/t9129.check b/tests/patmat/t9129.check
index f14f34ec9cfb..b112b1289226 100644
--- a/tests/patmat/t9129.check
+++ b/tests/patmat/t9129.check
@@ -1 +1 @@
-21: Pattern Match Exhaustivity: Two(_, A2)
+21: Pattern Match Exhaustivity: Two(B2, A2), Two(B1, A2)
diff --git a/tests/patmat/t9351.check b/tests/patmat/t9351.check
index 6a785fa26077..379adffd5a61 100644
--- a/tests/patmat/t9351.check
+++ b/tests/patmat/t9351.check
@@ -1,3 +1,3 @@
 8: Pattern Match Exhaustivity: _: A
-17: Pattern Match Exhaustivity: (_, None), (_, Some(_))
+17: Pattern Match Exhaustivity: (_, _)
 28: Pattern Match Exhaustivity: (_, _)

From 94103c8a7c949ad9d40a277342c0157747e4a024 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@bright-it.com>
Date: Wed, 22 Nov 2017 21:07:05 +0100
Subject: [PATCH 6/6] Workaround for #3479 #1932

---
 .../src/dotty/tools/dotc/transform/patmat/Spaces.scala     | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala
index a74c94f9ab20..d12fbe041c8b 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Spaces.scala
@@ -32,8 +32,11 @@ case class ConstrainedSpace(
   def withTypeConstraints(typeConstraints: List[TypeConstraint]) = copy(typeConstraints = typeConstraints)
 }
 
-/** A term-level constraint */
-sealed trait TermConstraint {
+/** A term-level constraint
+ *
+ * @note Cannot be sealed because of #3479 #1932
+ */
+/*sealed*/ trait TermConstraint {
   final def neg: TermConstraint = this match {
     case Neg(c) => c
     case c: PositiveTermConstraint => Neg(c)