[refactor] move some logic-related code

3 files changed, 358 insertions, 352 deletions

diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
index 6a890c5bb5..23c0272a30 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
@@ -52,7 +52,8 @@ trait Logic { self: PatternMatching =>
 
   // http://www.cis.upenn.edu/~cis510/tcl/chap3.pdf
   // http://users.encs.concordia.ca/~ta_ahmed/ms_thesis.pdf
-  trait FirstOrderLogic {
+  // propositional logic with constants and equality
+  trait PropositionalLogic {
     class Prop
     case class Eq(p: Var, q: Const) extends Prop
 
@@ -297,7 +298,7 @@ trait Logic { self: PatternMatching =>
     def findAllModelsFor(f: Formula): List[Model]
   }
 
-  trait CNF extends FirstOrderLogic {
+  trait CNF extends PropositionalLogic {
 
     /** Override Array creation for efficiency (to not go through reflection). */
     private implicit val clauseTag: scala.reflect.ClassTag[Clause] = new scala.reflect.ClassTag[Clause] {
@@ -404,7 +405,6 @@ trait Logic { self: PatternMatching =>
 //      patmatDebug("cnf for\n"+ p +"\nis:\n"+cnfString(res))
       res
     }
-
   }
 
   trait DPLLSolver extends CNF {
@@ -524,4 +524,335 @@ trait Logic { self: PatternMatching =>
         satisfiableWithModel
     }
   }
+
+  trait TreesAndTypesDomain extends PropositionalLogic with CheckableTreeAndTypeAnalysis {
+    // resets hash consing -- only supposed to be called by TreeMakersToProps
+    def prepareNewAnalysis(): Unit = { Var.resetUniques(); Const.resetUniques() }
+
+    object Var extends VarExtractor {
+      private var _nextId = 0
+      def nextId = {_nextId += 1; _nextId}
+
+      def resetUniques() = {_nextId = 0; uniques.clear()}
+      private val uniques = new mutable.HashMap[Tree, Var]
+      def apply(x: Tree): Var = uniques getOrElseUpdate(x, new Var(x, x.tpe))
+      def unapply(v: Var) = Some(v.path)
+    }
+    class Var(val path: Tree, staticTp: Type) extends AbsVar {
+      private[this] val id: Int = Var.nextId
+
+      // private[this] var canModify: Option[Array[StackTraceElement]] = None
+      private[this] def ensureCanModify() = {} //if (canModify.nonEmpty) patmatDebug("BUG!"+ this +" modified after having been observed: "+ canModify.get.mkString("\n"))
+
+      private[this] def observed() = {} //canModify = Some(Thread.currentThread.getStackTrace)
+
+      // don't access until all potential equalities have been registered using registerEquality
+      private[this] val symForEqualsTo = new mutable.HashMap[Const, Sym]
+
+      // when looking at the domain, we only care about types we can check at run time
+      val staticTpCheckable: Type = checkableType(staticTp)
+
+      private[this] var _mayBeNull = false
+      def registerNull(): Unit = { ensureCanModify; if (NullTp <:< staticTpCheckable) _mayBeNull = true }
+      def mayBeNull: Boolean = _mayBeNull
+
+      // case None => domain is unknown,
+      // case Some(List(tps: _*)) => domain is exactly tps
+      // we enumerate the subtypes of the full type, as that allows us to filter out more types statically,
+      // once we go to run-time checks (on Const's), convert them to checkable types
+      // TODO: there seems to be bug for singleton domains (variable does not show up in model)
+      lazy val domain: Option[Set[Const]] = {
+        val subConsts = enumerateSubtypes(staticTp).map{ tps =>
+          tps.toSet[Type].map{ tp =>
+            val domainC = TypeConst(tp)
+            registerEquality(domainC)
+            domainC
+          }
+        }
+
+        val allConsts =
+          if (mayBeNull) {
+            registerEquality(NullConst)
+            subConsts map (_ + NullConst)
+          } else
+            subConsts
+
+        observed; allConsts
+      }
+
+      // populate equalitySyms
+      // don't care about the result, but want only one fresh symbol per distinct constant c
+      def registerEquality(c: Const): Unit = {ensureCanModify; symForEqualsTo getOrElseUpdate(c, Sym(this, c))}
+
+      // return the symbol that represents this variable being equal to the constant `c`, if it exists, otherwise False (for robustness)
+      // (registerEquality(c) must have been called prior, either when constructing the domain or from outside)
+      def propForEqualsTo(c: Const): Prop = {observed; symForEqualsTo.getOrElse(c, False)}
+
+      // [implementation NOTE: don't access until all potential equalities have been registered using registerEquality]p
+      /** the information needed to construct the boolean proposition that encods the equality proposition (V = C)
+       *
+       * that models a type test pattern `_: C` or constant pattern `C`, where the type test gives rise to a TypeConst C,
+       * and the constant pattern yields a ValueConst C
+       *
+       * for exhaustivity, we really only need implication (e.g., V = 1 implies that V = 1 /\ V = Int, if both tests occur in the match,
+       * and thus in this variable's equality symbols), but reachability also requires us to model things like V = 1 precluding V = "1"
+       */
+      lazy val implications = {
+        /** when we know V = C, which other equalities must hold
+         *
+         * in general, equality to some type implies equality to its supertypes
+         * (this multi-valued kind of equality is necessary for unreachability)
+         * note that we use subtyping as a model for implication between instanceof tests
+         * i.e., when S <:< T we assume x.isInstanceOf[S] implies x.isInstanceOf[T]
+         * unfortunately this is not true in general (see e.g. SI-6022)
+         */
+        def implies(lower: Const, upper: Const): Boolean =
+          // values and null
+            lower == upper ||
+          // type implication
+            (lower != NullConst && !upper.isValue &&
+             instanceOfTpImplies(if (lower.isValue) lower.wideTp else lower.tp, upper.tp))
+
+          // if(r) patmatDebug("implies    : "+(lower, lower.tp, upper, upper.tp))
+          // else  patmatDebug("NOT implies: "+(lower, upper))
+
+
+        /** does V = C preclude V having value `other`?
+         (1) V = null is an exclusive assignment,
+         (2) V = A and V = B, for A and B value constants, are mutually exclusive unless A == B
+             we err on the safe side, for example:
+               - assume `val X = 1; val Y = 1`, then
+                 (2: Int) match { case X => case Y =>  <falsely considered reachable>  }
+               - V = 1 does not preclude V = Int, or V = Any, it could be said to preclude V = String, but we don't model that
+
+         (3) for types we could try to do something fancy, but be conservative and just say no
+         */
+        def excludes(a: Const, b: Const): Boolean =
+          a != b && ((a == NullConst || b == NullConst) || (a.isValue && b.isValue))
+
+          // if(r) patmatDebug("excludes    : "+(a, a.tp, b, b.tp))
+          // else  patmatDebug("NOT excludes: "+(a, b))
+
+/*
+[ HALF BAKED FANCINESS: //!equalitySyms.exists(common => implies(common.const, a) && implies(common.const, b)))
+ when type tests are involved, we reason (conservatively) under a closed world assumption,
+ since we are really only trying to counter the effects of the symbols that we introduce to model type tests
+ we don't aim to model the whole subtyping hierarchy, simply to encode enough about subtyping to do unreachability properly
+
+ consider the following hierarchy:
+
+    trait A
+    trait B
+    trait C
+    trait AB extends B with A
+
+  // two types are mutually exclusive if there is no equality symbol whose constant implies both
+  object Test extends App {
+    def foo(x: Any) = x match {
+      case _ : C  => println("C")
+      case _ : AB => println("AB")
+      case _ : (A with B) => println("AB'")
+      case _ : B  => println("B")
+      case _ : A  => println("A")
+    }
+
+ of course this kind of reasoning is not true in general,
+ but we can safely pretend types are mutually exclusive as long as there are no counter-examples in the match we're analyzing}
+*/
+
+        val excludedPair = new mutable.HashSet[ExcludedPair]
+
+        case class ExcludedPair(a: Const, b: Const) {
+          override def equals(o: Any) = o match {
+            case ExcludedPair(aa, bb) => (a == aa && b == bb) || (a == bb && b == aa)
+            case _ => false
+          }
+          // make ExcludedPair(a, b).hashCode == ExcludedPair(b, a).hashCode
+          override def hashCode = a.hashCode ^ b.hashCode
+        }
+
+        equalitySyms map { sym =>
+          // if we've already excluded the pair at some point (-A \/ -B), then don't exclude the symmetric one (-B \/ -A)
+          // (nor the positive implications -B \/ A, or -A \/ B, which would entail the equality axioms falsifying the whole formula)
+          val todo = equalitySyms filterNot (b => (b.const == sym.const) || excludedPair(ExcludedPair(b.const, sym.const)))
+          val (excluded, notExcluded) = todo partition (b => excludes(sym.const, b.const))
+          val implied = notExcluded filter (b => implies(sym.const, b.const))
+
+          patmatDebug("eq axioms for: "+ sym.const)
+          patmatDebug("excluded: "+ excluded)
+          patmatDebug("implied: "+ implied)
+
+          excluded foreach { excludedSym => excludedPair += ExcludedPair(sym.const, excludedSym.const)}
+
+          (sym, implied, excluded)
+        }
+      }
+
+      // accessing after calling registerNull will result in inconsistencies
+      lazy val domainSyms: Option[Set[Sym]] = domain map { _ map symForEqualsTo }
+
+      lazy val symForStaticTp: Option[Sym]  = symForEqualsTo.get(TypeConst(staticTpCheckable))
+
+      // don't access until all potential equalities have been registered using registerEquality
+      private lazy val equalitySyms = {observed; symForEqualsTo.values.toList}
+
+      // don't call until all equalities have been registered and registerNull has been called (if needed)
+      def describe = {
+        def domain_s = domain match {
+          case Some(d) => d mkString (" ::= ", " | ", "// "+ symForEqualsTo.keys)
+          case _       => symForEqualsTo.keys mkString (" ::= ", " | ", " | ...")
+        }
+        s"$this: ${staticTp}${domain_s} // = $path"
+      }
+      override def toString = "V"+ id
+    }
+
+
+    import global.{ConstantType, Constant, SingletonType, Literal, Ident, singleType}
+    import global.definitions.{AnyClass, UnitClass}
+
+
+    // all our variables range over types
+    // a literal constant becomes ConstantType(Constant(v)) when the type allows it (roughly, anyval + string + null)
+    // equality between variables: SingleType(x) (note that pattern variables cannot relate to each other -- it's always patternVar == nonPatternVar)
+    object Const {
+      def resetUniques() = {_nextTypeId = 0; _nextValueId = 0; uniques.clear() ; trees.clear()}
+
+      private var _nextTypeId = 0
+      def nextTypeId = {_nextTypeId += 1; _nextTypeId}
+
+      private var _nextValueId = 0
+      def nextValueId = {_nextValueId += 1; _nextValueId}
+
+      private val uniques = new mutable.HashMap[Type, Const]
+      private[TreesAndTypesDomain] def unique(tp: Type, mkFresh: => Const): Const =
+        uniques.get(tp).getOrElse(
+          uniques.find {case (oldTp, oldC) => oldTp =:= tp} match {
+            case Some((_, c)) =>
+              patmatDebug("unique const: "+ (tp, c))
+              c
+            case _ =>
+              val fresh = mkFresh
+              patmatDebug("uniqued const: "+ (tp, fresh))
+              uniques(tp) = fresh
+              fresh
+          })
+
+      private val trees = mutable.HashSet.empty[Tree]
+
+      // hashconsing trees (modulo value-equality)
+      private[TreesAndTypesDomain] def uniqueTpForTree(t: Tree): Type =
+        // a new type for every unstable symbol -- only stable value are uniqued
+        // technically, an unreachable value may change between cases
+        // thus, the failure of a case that matches on a mutable value does not exclude the next case succeeding
+        // (and thuuuuus, the latter case must be considered reachable)
+        if (!t.symbol.isStable) t.tpe.narrow
+        else trees find (a => a.correspondsStructure(t)(sameValue)) match {
+          case Some(orig) =>
+            patmatDebug("unique tp for tree: "+ (orig, orig.tpe))
+            orig.tpe
+          case _ =>
+            // duplicate, don't mutate old tree (TODO: use a map tree -> type instead?)
+            val treeWithNarrowedType = t.duplicate setType t.tpe.narrow
+            patmatDebug("uniqued: "+ (t, t.tpe, treeWithNarrowedType.tpe))
+            trees += treeWithNarrowedType
+            treeWithNarrowedType.tpe
+        }
+    }
+
+    sealed abstract class Const {
+      def tp: Type
+      def wideTp: Type
+
+      def isAny = wideTp.typeSymbol == AnyClass
+      def isValue: Boolean //= tp.isStable
+
+      // note: use reference equality on Const since they're hash-consed (doing type equality all the time is too expensive)
+      // the equals inherited from AnyRef does just this
+    }
+
+    // find most precise super-type of tp that is a class
+    // we skip non-class types (singleton types, abstract types) so that we can
+    // correctly compute how types relate in terms of the values they rule out
+    // e.g., when we know some value must be of type T, can it still be of type S? (this is the positive formulation of what `excludes` on Const computes)
+    // since we're talking values, there must have been a class involved in creating it, so rephrase our types in terms of classes
+    // (At least conceptually: `true` is an instance of class `Boolean`)
+    private def widenToClass(tp: Type): Type =
+      if (tp.typeSymbol.isClass) tp
+      else tp.baseType(tp.baseClasses.head)
+
+    object TypeConst extends TypeConstExtractor {
+      def apply(tp: Type) = {
+        if (tp =:= NullTp) NullConst
+        else if (tp.isInstanceOf[SingletonType]) ValueConst.fromType(tp)
+        else Const.unique(tp, new TypeConst(tp))
+      }
+      def unapply(c: TypeConst): Some[Type] = Some(c.tp)
+    }
+
+    // corresponds to a type test that does not imply any value-equality (well, except for outer checks, which we don't model yet)
+    sealed class TypeConst(val tp: Type) extends Const {
+      assert(!(tp =:= NullTp))
+      /*private[this] val id: Int = */ Const.nextTypeId
+
+      val wideTp = widenToClass(tp)
+      def isValue = false
+      override def toString = tp.toString //+"#"+ id
+    }
+
+    // p is a unique type or a constant value
+    object ValueConst extends ValueConstExtractor {
+      def fromType(tp: Type) = {
+        assert(tp.isInstanceOf[SingletonType])
+        val toString = tp match {
+          case ConstantType(c) => c.escapedStringValue
+          case _ => tp.toString
+        }
+        Const.unique(tp, new ValueConst(tp, tp.widen, toString))
+      }
+      def apply(p: Tree) = {
+        val tp = p.tpe.normalize
+        if (tp =:= NullTp) NullConst
+        else {
+          val wideTp = widenToClass(tp)
+
+          val narrowTp =
+            if (tp.isInstanceOf[SingletonType]) tp
+            else p match {
+              case Literal(c) =>
+                if (c.tpe.typeSymbol == UnitClass) c.tpe
+                else ConstantType(c)
+              case Ident(_) if p.symbol.isStable =>
+                // for Idents, can encode uniqueness of symbol as uniqueness of the corresponding singleton type
+                // for Selects, which are handled by the next case, the prefix of the select varies independently of the symbol (see pos/virtpatmat_unreach_select.scala)
+                singleType(tp.prefix, p.symbol)
+              case _ =>
+                Const.uniqueTpForTree(p)
+            }
+
+          val toString =
+            if (hasStableSymbol(p)) p.symbol.name.toString // tp.toString
+            else p.toString //+"#"+ id
+
+          Const.unique(narrowTp, new ValueConst(narrowTp, checkableType(wideTp), toString)) // must make wide type checkable so that it is comparable to types from TypeConst
+        }
+      }
+    }
+    sealed class ValueConst(val tp: Type, val wideTp: Type, override val toString: String) extends Const {
+      // patmatDebug("VC"+(tp, wideTp, toString))
+      assert(!(tp =:= NullTp)) // TODO: assert(!tp.isStable)
+      /*private[this] val id: Int = */Const.nextValueId
+      def isValue = true
+    }
+
+
+    lazy val NullTp = ConstantType(Constant(null))
+    case object NullConst extends Const {
+      def tp     = NullTp
+      def wideTp = NullTp
+
+      def isValue = true
+      override def toString = "null"
+    }
+  }
 }
\ No newline at end of file
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
index 421207f24f..1e12975880 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
@@ -19,7 +19,7 @@ import scala.reflect.internal.util.Statistics
 import scala.reflect.internal.Types
 import scala.reflect.internal.util.HashSet
 
-trait TypeAnalysis extends Debugging {
+trait TreeAndTypeAnalysis extends Debugging {
   val global: Global
   import global.{Tree, Type, Symbol, definitions, analyzer,
     ConstantType, Literal, Constant,  appliedType, WildcardType, TypeRef, ModuleClassSymbol,
@@ -54,7 +54,7 @@ trait TypeAnalysis extends Debugging {
     case _                      => false
   })
 
-  trait CheckableTypeAnalysis {
+  trait CheckableTreeAndTypeAnalysis {
     val typer: Typer
 
     // TODO: domain of other feasibly enumerable built-in types (char?)
@@ -135,7 +135,7 @@ trait TypeAnalysis extends Debugging {
   }
 }
 
-trait Analysis extends TypeAnalysis { self: PatternMatching =>
+trait Analysis extends TreeAndTypeAnalysis { self: PatternMatching =>
   import PatternMatchingStats._
   val global: Global
   import global.{Tree, Type, Symbol, CaseDef, Position, atPos, NoPosition,
@@ -154,7 +154,7 @@ trait Analysis extends TypeAnalysis { self: PatternMatching =>
    * Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types)
    *
    */
-  trait TreeMakerApproximation extends TreeMakers with FirstOrderLogic with CheckableTypeAnalysis { self: CodegenCore =>
+  trait TreeMakerApproximation extends TreeMakers with PropositionalLogic with TreesAndTypesDomain with CheckableTreeAndTypeAnalysis { self: CodegenCore =>
     object Test {
       var currId = 0
     }
@@ -173,25 +173,6 @@ trait Analysis extends TypeAnalysis { self: PatternMatching =>
     }
 
 
-    object IrrefutableExtractorTreeMaker {
-      // will an extractor with unapply method of methodtype `tp` always succeed?
-      // note: this assumes the other side-conditions implied by the extractor are met
-      // (argument of the right type, length check succeeds for unapplySeq,...)
-      def irrefutableExtractorType(tp: Type): Boolean = tp.resultType.dealias match {
-        case TypeRef(_, SomeClass, _) => true
-        // probably not useful since this type won't be inferred nor can it be written down (yet)
-        case ConstantType(Constant(true)) => true
-        case _ => false
-      }
-
-      def unapply(xtm: ExtractorTreeMaker): Option[(Tree, Symbol)] = xtm match {
-        case ExtractorTreeMaker(extractor, None, nextBinder) if irrefutableExtractorType(extractor.tpe) =>
-          Some((extractor, nextBinder))
-        case _ =>
-          None
-      }
-    }
-
     class TreeMakersToPropsIgnoreNullChecks(root: Symbol) extends TreeMakersToProps(root) {
       override def uniqueNonNullProp(p: Tree): Prop = True
     }
@@ -364,331 +345,6 @@ trait Analysis extends TypeAnalysis { self: PatternMatching =>
     def approximateMatchConservative(root: Symbol, cases: List[List[TreeMaker]]): List[List[Test]] =
       (new TreeMakersToProps(root)).approximateMatch(cases)
 
-    // resets hash consing -- only supposed to be called by TreeMakersToProps
-    def prepareNewAnalysis(): Unit = { Var.resetUniques(); Const.resetUniques() }
-
-    object Var extends VarExtractor {
-      private var _nextId = 0
-      def nextId = {_nextId += 1; _nextId}
-
-      def resetUniques() = {_nextId = 0; uniques.clear()}
-      private val uniques = new mutable.HashMap[Tree, Var]
-      def apply(x: Tree): Var = uniques getOrElseUpdate(x, new Var(x, x.tpe))
-      def unapply(v: Var) = Some(v.path)
-    }
-    class Var(val path: Tree, staticTp: Type) extends AbsVar {
-      private[this] val id: Int = Var.nextId
-
-      // private[this] var canModify: Option[Array[StackTraceElement]] = None
-      private[this] def ensureCanModify() = {} //if (canModify.nonEmpty) patmatDebug("BUG!"+ this +" modified after having been observed: "+ canModify.get.mkString("\n"))
-
-      private[this] def observed() = {} //canModify = Some(Thread.currentThread.getStackTrace)
-
-      // don't access until all potential equalities have been registered using registerEquality
-      private[this] val symForEqualsTo = new mutable.HashMap[Const, Sym]
-
-      // when looking at the domain, we only care about types we can check at run time
-      val staticTpCheckable: Type = checkableType(staticTp)
-
-      private[this] var _mayBeNull = false
-      def registerNull(): Unit = { ensureCanModify; if (NullTp <:< staticTpCheckable) _mayBeNull = true }
-      def mayBeNull: Boolean = _mayBeNull
-
-      // case None => domain is unknown,
-      // case Some(List(tps: _*)) => domain is exactly tps
-      // we enumerate the subtypes of the full type, as that allows us to filter out more types statically,
-      // once we go to run-time checks (on Const's), convert them to checkable types
-      // TODO: there seems to be bug for singleton domains (variable does not show up in model)
-      lazy val domain: Option[Set[Const]] = {
-        val subConsts = enumerateSubtypes(staticTp).map{ tps =>
-          tps.toSet[Type].map{ tp =>
-            val domainC = TypeConst(tp)
-            registerEquality(domainC)
-            domainC
-          }
-        }
-
-        val allConsts =
-          if (mayBeNull) {
-            registerEquality(NullConst)
-            subConsts map (_ + NullConst)
-          } else
-            subConsts
-
-        observed; allConsts
-      }
-
-      // populate equalitySyms
-      // don't care about the result, but want only one fresh symbol per distinct constant c
-      def registerEquality(c: Const): Unit = {ensureCanModify; symForEqualsTo getOrElseUpdate(c, Sym(this, c))}
-
-      // return the symbol that represents this variable being equal to the constant `c`, if it exists, otherwise False (for robustness)
-      // (registerEquality(c) must have been called prior, either when constructing the domain or from outside)
-      def propForEqualsTo(c: Const): Prop = {observed; symForEqualsTo.getOrElse(c, False)}
-
-      // [implementation NOTE: don't access until all potential equalities have been registered using registerEquality]p
-      /** the information needed to construct the boolean proposition that encods the equality proposition (V = C)
-       *
-       * that models a type test pattern `_: C` or constant pattern `C`, where the type test gives rise to a TypeConst C,
-       * and the constant pattern yields a ValueConst C
-       *
-       * for exhaustivity, we really only need implication (e.g., V = 1 implies that V = 1 /\ V = Int, if both tests occur in the match,
-       * and thus in this variable's equality symbols), but reachability also requires us to model things like V = 1 precluding V = "1"
-       */
-      lazy val implications = {
-        /** when we know V = C, which other equalities must hold
-         *
-         * in general, equality to some type implies equality to its supertypes
-         * (this multi-valued kind of equality is necessary for unreachability)
-         * note that we use subtyping as a model for implication between instanceof tests
-         * i.e., when S <:< T we assume x.isInstanceOf[S] implies x.isInstanceOf[T]
-         * unfortunately this is not true in general (see e.g. SI-6022)
-         */
-        def implies(lower: Const, upper: Const): Boolean =
-          // values and null
-            lower == upper ||
-          // type implication
-            (lower != NullConst && !upper.isValue &&
-             instanceOfTpImplies(if (lower.isValue) lower.wideTp else lower.tp, upper.tp))
-
-          // if(r) patmatDebug("implies    : "+(lower, lower.tp, upper, upper.tp))
-          // else  patmatDebug("NOT implies: "+(lower, upper))
-
-
-        /** does V = C preclude V having value `other`?
-         (1) V = null is an exclusive assignment,
-         (2) V = A and V = B, for A and B value constants, are mutually exclusive unless A == B
-             we err on the safe side, for example:
-               - assume `val X = 1; val Y = 1`, then
-                 (2: Int) match { case X => case Y =>  <falsely considered reachable>  }
-               - V = 1 does not preclude V = Int, or V = Any, it could be said to preclude V = String, but we don't model that
-
-         (3) for types we could try to do something fancy, but be conservative and just say no
-         */
-        def excludes(a: Const, b: Const): Boolean =
-          a != b && ((a == NullConst || b == NullConst) || (a.isValue && b.isValue))
-
-          // if(r) patmatDebug("excludes    : "+(a, a.tp, b, b.tp))
-          // else  patmatDebug("NOT excludes: "+(a, b))
-
-/*
-[ HALF BAKED FANCINESS: //!equalitySyms.exists(common => implies(common.const, a) && implies(common.const, b)))
- when type tests are involved, we reason (conservatively) under a closed world assumption,
- since we are really only trying to counter the effects of the symbols that we introduce to model type tests
- we don't aim to model the whole subtyping hierarchy, simply to encode enough about subtyping to do unreachability properly
-
- consider the following hierarchy:
-
-    trait A
-    trait B
-    trait C
-    trait AB extends B with A
-
-  // two types are mutually exclusive if there is no equality symbol whose constant implies both
-  object Test extends App {
-    def foo(x: Any) = x match {
-      case _ : C  => println("C")
-      case _ : AB => println("AB")
-      case _ : (A with B) => println("AB'")
-      case _ : B  => println("B")
-      case _ : A  => println("A")
-    }
-
- of course this kind of reasoning is not true in general,
- but we can safely pretend types are mutually exclusive as long as there are no counter-examples in the match we're analyzing}
-*/
-
-        val excludedPair = new mutable.HashSet[ExcludedPair]
-
-        case class ExcludedPair(a: Const, b: Const) {
-          override def equals(o: Any) = o match {
-            case ExcludedPair(aa, bb) => (a == aa && b == bb) || (a == bb && b == aa)
-            case _ => false
-          }
-          // make ExcludedPair(a, b).hashCode == ExcludedPair(b, a).hashCode
-          override def hashCode = a.hashCode ^ b.hashCode
-        }
-
-        equalitySyms map { sym =>
-          // if we've already excluded the pair at some point (-A \/ -B), then don't exclude the symmetric one (-B \/ -A)
-          // (nor the positive implications -B \/ A, or -A \/ B, which would entail the equality axioms falsifying the whole formula)
-          val todo = equalitySyms filterNot (b => (b.const == sym.const) || excludedPair(ExcludedPair(b.const, sym.const)))
-          val (excluded, notExcluded) = todo partition (b => excludes(sym.const, b.const))
-          val implied = notExcluded filter (b => implies(sym.const, b.const))
-
-          patmatDebug("eq axioms for: "+ sym.const)
-          patmatDebug("excluded: "+ excluded)
-          patmatDebug("implied: "+ implied)
-
-          excluded foreach { excludedSym => excludedPair += ExcludedPair(sym.const, excludedSym.const)}
-
-          (sym, implied, excluded)
-        }
-      }
-
-      // accessing after calling registerNull will result in inconsistencies
-      lazy val domainSyms: Option[Set[Sym]] = domain map { _ map symForEqualsTo }
-
-      lazy val symForStaticTp: Option[Sym]  = symForEqualsTo.get(TypeConst(staticTpCheckable))
-
-      // don't access until all potential equalities have been registered using registerEquality
-      private lazy val equalitySyms = {observed; symForEqualsTo.values.toList}
-
-      // don't call until all equalities have been registered and registerNull has been called (if needed)
-      def describe = {
-        def domain_s = domain match {
-          case Some(d) => d mkString (" ::= ", " | ", "// "+ symForEqualsTo.keys)
-          case _       => symForEqualsTo.keys mkString (" ::= ", " | ", " | ...")
-        }
-        s"$this: ${staticTp}${domain_s} // = $path"
-      }
-      override def toString = "V"+ id
-    }
-
-
-    // all our variables range over types
-    // a literal constant becomes ConstantType(Constant(v)) when the type allows it (roughly, anyval + string + null)
-    // equality between variables: SingleType(x) (note that pattern variables cannot relate to each other -- it's always patternVar == nonPatternVar)
-    object Const {
-      def resetUniques() = {_nextTypeId = 0; _nextValueId = 0; uniques.clear() ; trees.clear()}
-
-      private var _nextTypeId = 0
-      def nextTypeId = {_nextTypeId += 1; _nextTypeId}
-
-      private var _nextValueId = 0
-      def nextValueId = {_nextValueId += 1; _nextValueId}
-
-      private val uniques = new mutable.HashMap[Type, Const]
-      private[TreeMakerApproximation] def unique(tp: Type, mkFresh: => Const): Const =
-        uniques.get(tp).getOrElse(
-          uniques.find {case (oldTp, oldC) => oldTp =:= tp} match {
-            case Some((_, c)) =>
-              patmatDebug("unique const: "+ (tp, c))
-              c
-            case _ =>
-              val fresh = mkFresh
-              patmatDebug("uniqued const: "+ (tp, fresh))
-              uniques(tp) = fresh
-              fresh
-          })
-
-      private val trees = mutable.HashSet.empty[Tree]
-
-      // hashconsing trees (modulo value-equality)
-      private[TreeMakerApproximation] def uniqueTpForTree(t: Tree): Type =
-        // a new type for every unstable symbol -- only stable value are uniqued
-        // technically, an unreachable value may change between cases
-        // thus, the failure of a case that matches on a mutable value does not exclude the next case succeeding
-        // (and thuuuuus, the latter case must be considered reachable)
-        if (!t.symbol.isStable) t.tpe.narrow
-        else trees find (a => a.correspondsStructure(t)(sameValue)) match {
-          case Some(orig) =>
-            patmatDebug("unique tp for tree: "+ (orig, orig.tpe))
-            orig.tpe
-          case _ =>
-            // duplicate, don't mutate old tree (TODO: use a map tree -> type instead?)
-            val treeWithNarrowedType = t.duplicate setType t.tpe.narrow
-            patmatDebug("uniqued: "+ (t, t.tpe, treeWithNarrowedType.tpe))
-            trees += treeWithNarrowedType
-            treeWithNarrowedType.tpe
-        }
-    }
-
-    sealed abstract class Const {
-      def tp: Type
-      def wideTp: Type
-
-      def isAny = wideTp.typeSymbol == AnyClass
-      def isValue: Boolean //= tp.isStable
-
-      // note: use reference equality on Const since they're hash-consed (doing type equality all the time is too expensive)
-      // the equals inherited from AnyRef does just this
-    }
-
-    // find most precise super-type of tp that is a class
-    // we skip non-class types (singleton types, abstract types) so that we can
-    // correctly compute how types relate in terms of the values they rule out
-    // e.g., when we know some value must be of type T, can it still be of type S? (this is the positive formulation of what `excludes` on Const computes)
-    // since we're talking values, there must have been a class involved in creating it, so rephrase our types in terms of classes
-    // (At least conceptually: `true` is an instance of class `Boolean`)
-    private def widenToClass(tp: Type): Type =
-      if (tp.typeSymbol.isClass) tp
-      else tp.baseType(tp.baseClasses.head)
-
-    object TypeConst extends TypeConstExtractor {
-      def apply(tp: Type) = {
-        if (tp =:= NullTp) NullConst
-        else if (tp.isInstanceOf[SingletonType]) ValueConst.fromType(tp)
-        else Const.unique(tp, new TypeConst(tp))
-      }
-      def unapply(c: TypeConst): Some[Type] = Some(c.tp)
-    }
-
-    // corresponds to a type test that does not imply any value-equality (well, except for outer checks, which we don't model yet)
-    sealed class TypeConst(val tp: Type) extends Const {
-      assert(!(tp =:= NullTp))
-      /*private[this] val id: Int = */ Const.nextTypeId
-
-      val wideTp = widenToClass(tp)
-      def isValue = false
-      override def toString = tp.toString //+"#"+ id
-    }
-
-    // p is a unique type or a constant value
-    object ValueConst extends ValueConstExtractor {
-      def fromType(tp: Type) = {
-        assert(tp.isInstanceOf[SingletonType])
-        val toString = tp match {
-          case ConstantType(c) => c.escapedStringValue
-          case _ => tp.toString
-        }
-        Const.unique(tp, new ValueConst(tp, tp.widen, toString))
-      }
-      def apply(p: Tree) = {
-        val tp = p.tpe.normalize
-        if (tp =:= NullTp) NullConst
-        else {
-          val wideTp = widenToClass(tp)
-
-          val narrowTp =
-            if (tp.isInstanceOf[SingletonType]) tp
-            else p match {
-              case Literal(c) =>
-                if (c.tpe.typeSymbol == UnitClass) c.tpe
-                else ConstantType(c)
-              case Ident(_) if p.symbol.isStable =>
-                // for Idents, can encode uniqueness of symbol as uniqueness of the corresponding singleton type
-                // for Selects, which are handled by the next case, the prefix of the select varies independently of the symbol (see pos/virtpatmat_unreach_select.scala)
-                singleType(tp.prefix, p.symbol)
-              case _ =>
-                Const.uniqueTpForTree(p)
-            }
-
-          val toString =
-            if (hasStableSymbol(p)) p.symbol.name.toString // tp.toString
-            else p.toString //+"#"+ id
-
-          Const.unique(narrowTp, new ValueConst(narrowTp, checkableType(wideTp), toString)) // must make wide type checkable so that it is comparable to types from TypeConst
-        }
-      }
-    }
-    sealed class ValueConst(val tp: Type, val wideTp: Type, override val toString: String) extends Const {
-      // patmatDebug("VC"+(tp, wideTp, toString))
-      assert(!(tp =:= NullTp)) // TODO: assert(!tp.isStable)
-      /*private[this] val id: Int = */Const.nextValueId
-      def isValue = true
-    }
-
-    lazy val NullTp = ConstantType(Constant(null))
-    case object NullConst extends Const {
-      def tp     = NullTp
-      def wideTp = NullTp
-
-      def isValue = true
-      override def toString = "null"
-    }
-
-
     // turns a case (represented as a list of abstract tests)
     // into a proposition that is satisfiable if the case may match
     protected final def caseWithoutBodyToProp(tests: List[Test]): Prop =
@@ -706,7 +362,7 @@ trait Analysis extends TypeAnalysis { self: PatternMatching =>
   }
 
   trait SymbolicMatchAnalysis extends TreeMakerApproximation  { self: CodegenCore =>
-     // TODO: model dependencies between variables: if V1 corresponds to (x: List[_]) and V2 is (x.hd), V2 cannot be assigned when V1 = null or V1 = Nil
+    // TODO: model dependencies between variables: if V1 corresponds to (x: List[_]) and V2 is (x.hd), V2 cannot be assigned when V1 = null or V1 = Nil
     // right now hackily implement this by pruning counter-examples
     // unreachability would also benefit from a more faithful representation
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMakers.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMakers.scala
index 575e531231..b334a6b228 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMakers.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMakers.scala
@@ -279,6 +279,25 @@ trait TreeMaking { self: PatternMatching =>
       override def toString = "P"+(prevBinder.name,  extraCond getOrElse "", localSubstitution)
     }
 
+    object IrrefutableExtractorTreeMaker {
+      // will an extractor with unapply method of methodtype `tp` always succeed?
+      // note: this assumes the other side-conditions implied by the extractor are met
+      // (argument of the right type, length check succeeds for unapplySeq,...)
+      def irrefutableExtractorType(tp: Type): Boolean = tp.resultType.dealias match {
+        case TypeRef(_, SomeClass, _) => true
+        // probably not useful since this type won't be inferred nor can it be written down (yet)
+        case ConstantType(Constant(true)) => true
+        case _ => false
+      }
+
+      def unapply(xtm: ExtractorTreeMaker): Option[(Tree, Symbol)] = xtm match {
+        case ExtractorTreeMaker(extractor, None, nextBinder) if irrefutableExtractorType(extractor.tpe) =>
+          Some((extractor, nextBinder))
+        case _ =>
+          None
+      }
+    }
+
     object TypeTestTreeMaker {
       // factored out so that we can consistently generate other representations of the tree that implements the test
       // (e.g. propositions for exhaustivity and friends, boolean for isPureTypeTest)