From c1b7e849121ed16906e89a668ecb004edebd4afd Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Mon, 11 Feb 2019 10:25:39 +0100
Subject: [PATCH 01/20] Minor TypeTestsCasts refactoring

---
 .../tools/dotc/transform/TypeTestsCasts.scala | 28 +++++++++----------
 1 file changed, 13 insertions(+), 15 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
index dbd781357c23..0183065650b6 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
@@ -164,19 +164,20 @@ object TypeTestsCasts {
           else tp.classSymbol
 
         def foundCls = effectiveClass(expr.tpe.widen)
-        // println(i"ta $tree, found = $foundCls")
 
         def inMatch =
           fun.symbol == defn.Any_typeTest ||  // new scheme
           expr.symbol.is(Case)                // old scheme
 
-        def transformIsInstanceOf(expr:Tree, testType: Type, flagUnrelated: Boolean): Tree = {
+        def transformIsInstanceOf(expr: Tree, testType: Type, flagUnrelated: Boolean): Tree = {
           def testCls = effectiveClass(testType.widen)
 
-          def unreachable(why: => String) =
+          def unreachable(why: => String): Boolean = {
             if (flagUnrelated)
               if (inMatch) ctx.error(em"this case is unreachable since $why", expr.sourcePos)
               else ctx.warning(em"this will always yield false since $why", expr.sourcePos)
+            false
+          }
 
           /** Are `foundCls` and `testCls` classes that allow checks
            *  whether a test would be always false?
@@ -191,25 +192,22 @@ object TypeTestsCasts {
                // we don't have the logic to handle derived value classes
 
           /** Check whether a runtime test that a value of `foundCls` can be a `testCls`
-           *  can be true in some cases. Issure a warning or an error if that's not the case.
+           *  can be true in some cases. Issues a warning or an error otherwise.
            */
           def checkSensical: Boolean =
             if (!isCheckable) true
             else if (foundCls.isPrimitiveValueClass && !testCls.isPrimitiveValueClass) {
-                ctx.error("cannot test if value types are references", tree.sourcePos)
-                false
-              }
+              ctx.error("cannot test if value types are references", tree.sourcePos)
+              false
+            }
             else if (!foundCls.derivesFrom(testCls)) {
-              if (foundCls.is(Final)) {
+              val unrelated = !testCls.derivesFrom(foundCls) && (
+                testCls.is(Final) || !testCls.is(Trait) && !foundCls.is(Trait)
+              )
+              if (foundCls.is(Final))
                 unreachable(i"$foundCls is not a subclass of $testCls")
-                false
-              }
-              else if (!testCls.derivesFrom(foundCls) &&
-                       (testCls.is(Final) ||
-                        !testCls.is(Trait) && !foundCls.is(Trait))) {
+              else if (unrelated)
                 unreachable(i"$foundCls and $testCls are unrelated")
-                false
-              }
               else true
             }
             else true

From 6e39fcbdb2f028dbb4c88fe8c0832e410e5c0f30 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Mon, 11 Feb 2019 10:26:15 +0100
Subject: [PATCH 02/20] Rename evalOnce to letBind

---
 compiler/src/dotty/tools/dotc/ast/tpd.scala                 | 2 +-
 compiler/src/dotty/tools/dotc/transform/Erasure.scala       | 2 +-
 .../src/dotty/tools/dotc/transform/TypeTestsCasts.scala     | 6 +++---
 .../src/dotty/tools/dotc/transform/VCInlineMethods.scala    | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/ast/tpd.scala b/compiler/src/dotty/tools/dotc/ast/tpd.scala
index 8b6fcfe03dad..073cf19a2411 100644
--- a/compiler/src/dotty/tools/dotc/ast/tpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/tpd.scala
@@ -1139,7 +1139,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
   }
 
   /** Let bind `tree` unless `tree` is at least idempotent */
-  def evalOnce(tree: Tree)(within: Tree => Tree)(implicit ctx: Context): Tree =
+  def letBind(tree: Tree)(within: Tree => Tree)(implicit ctx: Context): Tree =
     letBindUnless(TreeInfo.Idempotent, tree)(within)
 
   def runtimeCall(name: TermName, args: List[Tree])(implicit ctx: Context): Tree = {
diff --git a/compiler/src/dotty/tools/dotc/transform/Erasure.scala b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
index 2fd68a391c43..965cc8e33fb0 100644
--- a/compiler/src/dotty/tools/dotc/transform/Erasure.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
@@ -221,7 +221,7 @@ object Erasure {
               val nullTree = Literal(Constant(null))
               val unboxedNull = adaptToType(nullTree, underlying)
 
-              evalOnce(tree) { t =>
+              letBind(tree) { t =>
                 If(t.select(defn.Object_eq).appliedTo(nullTree),
                   unboxedNull,
                   unboxedTree(t))
diff --git a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
index 0183065650b6..b7061012aba5 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
@@ -265,12 +265,12 @@ object TypeTestsCasts {
           case _: SingletonType =>
             expr.isInstance(testType).withSpan(tree.span)
           case OrType(tp1, tp2) =>
-            evalOnce(expr) { e =>
+            letBind(expr) { e =>
               transformTypeTest(e, tp1, flagUnrelated = false)
                 .or(transformTypeTest(e, tp2, flagUnrelated = false))
             }
           case AndType(tp1, tp2) =>
-            evalOnce(expr) { e =>
+            letBind(expr) { e =>
               transformTypeTest(e, tp1, flagUnrelated)
                 .and(transformTypeTest(e, tp2, flagUnrelated))
             }
@@ -278,7 +278,7 @@ object TypeTestsCasts {
             def isArrayTest(arg: Tree) =
               ref(defn.runtimeMethodRef(nme.isArray)).appliedTo(arg, Literal(Constant(ndims)))
             if (ndims == 1) isArrayTest(expr)
-            else evalOnce(expr) { e =>
+            else letBind(expr) { e =>
               derivedTree(e, defn.Any_isInstanceOf, e.tpe)
                 .and(isArrayTest(e))
             }
diff --git a/compiler/src/dotty/tools/dotc/transform/VCInlineMethods.scala b/compiler/src/dotty/tools/dotc/transform/VCInlineMethods.scala
index 7f5097fd5d27..d3e26a4e1cf2 100644
--- a/compiler/src/dotty/tools/dotc/transform/VCInlineMethods.scala
+++ b/compiler/src/dotty/tools/dotc/transform/VCInlineMethods.scala
@@ -68,7 +68,7 @@ class VCInlineMethods extends MiniPhase with IdentityDenotTransformer {
         val extensionMeth = extensionMethod(origMeth)
 
         if (!ctParams.isEmpty) {
-          evalOnce(qual) { ev =>
+          letBind(qual) { ev =>
             val ctArgs = ctParams.map(tparam =>
               TypeTree(tparam.typeRef.asSeenFrom(ev.tpe, origCls)))
             ref(extensionMeth)

From eef623a831ace6c80907d5626e75a30b9c26b62a Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Mon, 11 Feb 2019 11:03:21 +0100
Subject: [PATCH 03/20] Rename cmp to typeComparer

---
 compiler/src/dotty/tools/dotc/core/Types.scala | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index e4490aa3c599..f70427f9d4b4 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -3772,12 +3772,12 @@ object Types {
 
     def reduced(implicit ctx: Context): Type = {
       val trackingCtx = ctx.fresh.setTypeComparerFn(new TrackingTypeComparer(_))
-      val cmp = trackingCtx.typeComparer.asInstanceOf[TrackingTypeComparer]
+      val typeComparer = trackingCtx.typeComparer.asInstanceOf[TrackingTypeComparer]
 
       def reduceSequential(cases: List[Type])(implicit ctx: Context): Type = cases match {
         case Nil => NoType
         case cas :: cases1 =>
-          val r = cmp.matchCase(scrutinee, cas, instantiate = true)
+          val r = typeComparer.matchCase(scrutinee, cas, instantiate = true)
           if (r.exists) r
           else if (cantPossiblyMatch(cas)) reduceSequential(cases1)
           else NoType
@@ -3785,7 +3785,7 @@ object Types {
 
       def reduceParallel(implicit ctx: Context) = {
         val applicableBranches = cases
-          .map(cmp.matchCase(scrutinee, _, instantiate = true)(trackingCtx))
+          .map(typeComparer.matchCase(scrutinee, _, instantiate = true)(trackingCtx))
           .filter(_.exists)
         applicableBranches match {
           case Nil => NoType
@@ -3815,9 +3815,9 @@ object Types {
 
       def updateReductionContext() = {
         reductionContext = new mutable.HashMap
-        for (tp <- cmp.footprint)
+        for (tp <- typeComparer.footprint)
           reductionContext(tp) = contextInfo(tp)
-        typr.println(i"footprint for $this $hashCode: ${cmp.footprint.toList.map(x => (x, contextInfo(x)))}%, %")
+        typr.println(i"footprint for $this $hashCode: ${typeComparer.footprint.toList.map(x => (x, contextInfo(x)))}%, %")
       }
 
       def upToDate =

From 6755f52d79899b5854cba0ce512eaab11034ee66 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Mon, 18 Feb 2019 14:47:01 +0100
Subject: [PATCH 04/20] Remove reduceParallel

---
 .../src/dotty/tools/dotc/core/Types.scala     | 28 ++-----------------
 1 file changed, 3 insertions(+), 25 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index f70427f9d4b4..f80f7375a5b1 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -3764,9 +3764,6 @@ object Types {
 
     override def tryNormalize(implicit ctx: Context): Type = reduced.normalized
 
-    /** Switch to choose parallel or sequential reduction */
-    private final val reduceInParallel = false
-
     final def cantPossiblyMatch(cas: Type)(implicit ctx: Context): Boolean =
       true  // should be refined if we allow overlapping cases
 
@@ -3783,24 +3780,6 @@ object Types {
           else NoType
       }
 
-      def reduceParallel(implicit ctx: Context) = {
-        val applicableBranches = cases
-          .map(typeComparer.matchCase(scrutinee, _, instantiate = true)(trackingCtx))
-          .filter(_.exists)
-        applicableBranches match {
-          case Nil => NoType
-          case applicableBranch :: Nil => applicableBranch
-          case _ =>
-            record(i"MatchType.multi-branch")
-            ctx.typeComparer.glb(applicableBranches)
-        }
-      }
-
-      def isBounded(tp: Type) = tp match {
-        case tp: TypeParamRef =>
-        case tp: TypeRef => ctx.gadt.contains(tp.symbol)
-      }
-
       def contextInfo(tp: Type): Type = tp match {
         case tp: TypeParamRef =>
           val constraint = ctx.typerState.constraint
@@ -3813,27 +3792,26 @@ object Types {
           tp.underlying
       }
 
-      def updateReductionContext() = {
+      def updateReductionContext(): Unit = {
         reductionContext = new mutable.HashMap
         for (tp <- typeComparer.footprint)
           reductionContext(tp) = contextInfo(tp)
         typr.println(i"footprint for $this $hashCode: ${typeComparer.footprint.toList.map(x => (x, contextInfo(x)))}%, %")
       }
 
-      def upToDate =
+      def isUpToDate: Boolean =
         reductionContext.keysIterator.forall { tp =>
           reductionContext(tp) `eq` contextInfo(tp)
         }
 
       record("MatchType.reduce called")
-      if (!Config.cacheMatchReduced || myReduced == null || !upToDate) {
+      if (!Config.cacheMatchReduced || myReduced == null || !isUpToDate) {
         record("MatchType.reduce computed")
         if (myReduced != null) record("MatchType.reduce cache miss")
         myReduced =
           trace(i"reduce match type $this $hashCode", typr, show = true) {
             try
               if (defn.isBottomType(scrutinee)) defn.NothingType
-              else if (reduceInParallel) reduceParallel(trackingCtx)
               else reduceSequential(cases)(trackingCtx)
             catch {
               case ex: Throwable =>

From 88cfb7e72f5a01661c2a77a8e2c70710e79d3f64 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Thu, 21 Feb 2019 11:54:26 +0100
Subject: [PATCH 05/20] Fix spacing for TypeComparer comments

---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 78 +++++++++----------
 .../src/dotty/tools/dotc/core/Types.scala     |  2 +-
 2 files changed, 40 insertions(+), 40 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 71e032ffb7eb..388b2d9293ea 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -528,7 +528,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
       case tp2: HKTypeLambda =>
         def compareTypeLambda: Boolean = tp1.stripTypeVar match {
           case tp1: HKTypeLambda =>
-            /* Don't compare bounds of lambdas under language:Scala2, or t2994 will fail.
+           /* Don't compare bounds of lambdas under language:Scala2, or t2994 will fail.
             * The issue is that, logically, bounds should compare contravariantly,
             * but that would invalidate a pattern exploited in t2994:
             *
@@ -761,14 +761,14 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
     }
 
     /** Subtype test for the hk application `tp2 = tycon2[args2]`.
-    */
+     */
     def compareAppliedType2(tp2: AppliedType, tycon2: Type, args2: List[Type]): Boolean = {
       val tparams = tycon2.typeParams
       if (tparams.isEmpty) return false // can happen for ill-typed programs, e.g. neg/tcpoly_overloaded.scala
 
       /** True if `tp1` and `tp2` have compatible type constructors and their
-      *  corresponding arguments are subtypes relative to their variance (see `isSubArgs`).
-      */
+       *  corresponding arguments are subtypes relative to their variance (see `isSubArgs`).
+       */
       def isMatchingApply(tp1: Type): Boolean = tp1 match {
         case AppliedType(tycon1, args1) =>
           tycon1.dealiasKeepRefiningAnnots match {
@@ -815,25 +815,25 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
       }
 
       /** `param2` can be instantiated to a type application prefix of the LHS
-      *  or to a type application prefix of one of the LHS base class instances
-      *  and the resulting type application is a supertype of `tp1`,
-      *  or fallback to fourthTry.
-      */
+       *  or to a type application prefix of one of the LHS base class instances
+       *  and the resulting type application is a supertype of `tp1`,
+       *  or fallback to fourthTry.
+       */
       def canInstantiate(tycon2: TypeParamRef): Boolean = {
 
         /** Let
-        *
-        *    `tparams_1, ..., tparams_k-1`    be the type parameters of the rhs
-        *    `tparams1_1, ..., tparams1_n-1`  be the type parameters of the constructor of the lhs
-        *    `args1_1, ..., args1_n-1`        be the type arguments of the lhs
-        *    `d  =  n - k`
-        *
-        *  Returns `true` iff `d >= 0` and `tycon2` can be instantiated to
-        *
-        *      [tparams1_d, ... tparams1_n-1] -> tycon1[args_1, ..., args_d-1, tparams_d, ... tparams_n-1]
-        *
-        *  such that the resulting type application is a supertype of `tp1`.
-        */
+         *
+         *    `tparams_1, ..., tparams_k-1`    be the type parameters of the rhs
+         *    `tparams1_1, ..., tparams1_n-1`  be the type parameters of the constructor of the lhs
+         *    `args1_1, ..., args1_n-1`        be the type arguments of the lhs
+         *    `d  =  n - k`
+         *
+         *  Returns `true` iff `d >= 0` and `tycon2` can be instantiated to
+         *
+         *      [tparams1_d, ... tparams1_n-1] -> tycon1[args_1, ..., args_d-1, tparams_d, ... tparams_n-1]
+         *
+         *  such that the resulting type application is a supertype of `tp1`.
+         */
         def appOK(tp1base: Type) = tp1base match {
           case tp1base: AppliedType =>
             var tycon1 = tp1base.tycon
@@ -874,21 +874,21 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
       }
 
       /** Fall back to comparing either with `fourthTry` or against the lower
-      *  approximation of the rhs.
-      *  @param   tyconLo   The type constructor's lower approximation.
-      */
+       *  approximation of the rhs.
+       *  @param   tyconLo   The type constructor's lower approximation.
+       */
       def fallback(tyconLo: Type) =
         either(fourthTry, isSubApproxHi(tp1, tyconLo.applyIfParameterized(args2)))
 
       /** Let `tycon2bounds` be the bounds of the RHS type constructor `tycon2`.
-      *  Let `app2 = tp2` where the type constructor of `tp2` is replaced by
-      *  `tycon2bounds.lo`.
-      *  If both bounds are the same, continue with `tp1 <:< app2`.
-      *  otherwise continue with either
-      *
-      *    tp1 <:< tp2    using fourthTry (this might instantiate params in tp1)
-      *    tp1 <:< app2   using isSubType (this might instantiate params in tp2)
-      */
+       *  Let `app2 = tp2` where the type constructor of `tp2` is replaced by
+       *  `tycon2bounds.lo`.
+       *  If both bounds are the same, continue with `tp1 <:< app2`.
+       *  otherwise continue with either
+       *
+       *    tp1 <:< tp2    using fourthTry (this might instantiate params in tp1)
+       *    tp1 <:< app2   using isSubType (this might instantiate params in tp2)
+       */
       def compareLower(tycon2bounds: TypeBounds, tyconIsTypeRef: Boolean): Boolean =
         if ((tycon2bounds.lo `eq` tycon2bounds.hi) && !tycon2bounds.isInstanceOf[MatchAlias])
           if (tyconIsTypeRef) recur(tp1, tp2.superType)
@@ -927,7 +927,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
     }
 
     /** Subtype test for the application `tp1 = tycon1[args1]`.
-    */
+     */
     def compareAppliedType1(tp1: AppliedType, tycon1: Type, args1: List[Type]): Boolean =
       tycon1 match {
         case param1: TypeParamRef =>
@@ -973,8 +973,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
     }
 
     /** Like tp1 <:< tp2, but returns false immediately if we know that
-    *  the case was covered previously during subtyping.
-    */
+     *  the case was covered previously during subtyping.
+     */
     def isNewSubType(tp1: Type): Boolean =
       if (isCovered(tp1) && isCovered(tp2)) {
         //println(s"useless subtype: $tp1 <:< $tp2")
@@ -1031,12 +1031,12 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
   }
 
   /** Subtype test for corresponding arguments in `args1`, `args2` according to
-  *   variances in type parameters `tparams2`.
-  *   @param  tp1       The applied type containing `args1`
-  *   @param  tparams2  The type parameters of the type constructor applied to `args2`
-  */
+   *  variances in type parameters `tparams2`.
+   *
+   *  @param  tp1       The applied type containing `args1`
+   *  @param  tparams2  The type parameters of the type constructor applied to `args2`
+   */
   def isSubArgs(args1: List[Type], args2: List[Type], tp1: Type, tparams2: List[ParamInfo]): Boolean = {
-
     /** The bounds of parameter `tparam`, where all references to type paramneters
      *  are replaced by corresponding arguments (or their approximations in the case of
      *  wildcard arguments).
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index f80f7375a5b1..0db9cca05757 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -2415,7 +2415,7 @@ object Types {
     }
   }
 
-  /** A constant type with  single `value`. */
+  /** A constant type with single `value`. */
   abstract case class ConstantType(value: Constant) extends CachedProxyType with SingletonType {
     override def underlying(implicit ctx: Context): Type = value.tpe
 

From bb1515eb6514eaf2277e9dbe872fc0a07bc4d914 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Fri, 22 Feb 2019 10:51:21 +0100
Subject: [PATCH 06/20] Flag ChildrenQueried in hasAnonymousChild

---
 compiler/src/dotty/tools/dotc/transform/SymUtils.scala | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/SymUtils.scala b/compiler/src/dotty/tools/dotc/transform/SymUtils.scala
index 355bef8f1268..02f530494041 100644
--- a/compiler/src/dotty/tools/dotc/transform/SymUtils.scala
+++ b/compiler/src/dotty/tools/dotc/transform/SymUtils.scala
@@ -145,8 +145,11 @@ class SymUtils(val self: Symbol) extends AnyVal {
     }.reverse
   }
 
-  def hasAnonymousChild(implicit ctx: Context): Boolean =
+  def hasAnonymousChild(implicit ctx: Context): Boolean = {
+    if (self.isType)
+      self.setFlag(ChildrenQueried)
     children.exists(_ `eq` self)
+  }
 
   /** Is symbol directly or indirectly owned by a term symbol? */
   @tailrec final def isLocal(implicit ctx: Context): Boolean = {

From f79d93746062773661533519bf0651cec252b9dc Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Fri, 1 Mar 2019 14:53:19 +0100
Subject: [PATCH 07/20] Implement cantPossiblyMatch

This commit implements one of the missing aspects of Match Types: an
algorithm to determine when it is sound to reduce match types (see
discussion in #5300).

To understand the problem that is being solved, we can look at the
motivational example from the [Haskell Role
paper](https://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf)
(adapted to Scala).

Given this class:

```scala
class Foo {
  type Age

  type Type[X] = X match {
    case Age => Char
    case Int => Boolean
  }

  def method[X](x: X): Type[X] = ...
}
```

What is the type of `method(1)`?

On master, the compiler answers with "it depends", it could be either
`Char` or `Boolean`, which is obviously unsound:

```scala
val foo = new Foo { type Age = Int }
foo.method(1): Char
(foo: Foo).method(1): Boolean
```

The current algorithm to reduce match types is as follows:

```
foreach pattern
if (scrutinee <:< pattern)
  return pattern's result type
else
  continue
```

The unsoundness comes from the fact that the answer of `scrutinee <:<
pattern` can change depending on the context, which can result in
equivalent expressions being typed differently.

The proposed solution is to extend the algorithm above with an
additional intersection check:

```
foreach pattern
if (scrutinee <:< pattern)
  return pattern's result type
if (!intersecting(scrutinee, pattern))
  continue
else
  abort
```

Where `intersecting` returns `false` if there is a proof that both of
its arguments are not intersecting. In the absence of such proof, the
reduction is aborted. This algorithm solves the `type Age` example by
preventing the reduction of `Type[X]` (with `X != Age`) when `Age is
abstract. I believe this is enough to have sound type functions without
the need for adding roles to the type system.
---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 185 ++++++++++++++++--
 .../src/dotty/tools/dotc/core/Types.scala     |  14 +-
 .../dotty/tools/dotc/typer/Applications.scala |   2 +-
 .../dotc/reporting/ErrorMessagesTests.scala   |   2 +-
 tests/neg/matchtype-seq.scala                 | 145 ++++++++++++++
 5 files changed, 312 insertions(+), 36 deletions(-)
 create mode 100644 tests/neg/matchtype-seq.scala

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 388b2d9293ea..009e170bee68 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -13,6 +13,7 @@ import TypeErasure.{erasedLub, erasedGlb}
 import TypeApplications._
 import Constants.Constant
 import transform.TypeUtils._
+import transform.SymUtils._
 import scala.util.control.NonFatal
 import typer.ProtoTypes.constrained
 import reporting.trace
@@ -1875,6 +1876,133 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
 
   /** Returns last check's debug mode, if explicitly enabled. */
   def lastTrace(): String = ""
+
+  /** Do `tp1` and `tp2` share a non-null inhabitant?
+   *
+   *  `false` implies that we found a proof; uncertainty default to `true`.
+   *
+   *  Proofs rely on the following properties of Scala types:
+   *
+   *  1. Single inheritance of classes
+   *  2. Final classes cannot be extended
+   *  3. ConstantTypes with distinc values are non intersecting
+   *  4. There is no value of type Nothing
+   */
+  def intersecting(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = {
+    // println(s"intersecting(${tp1.show}, ${tp2.show})")
+    /** Can we enumerate all instantiations of this type? */
+    def isClosed(tp: Symbol): Boolean =
+      tp.is(Sealed) && tp.is(AbstractOrTrait) && !tp.hasAnonymousChild
+
+    /** Splits a close type into a disjunction of smaller types.
+     *  It should hold that `tp` and `decompose(tp).reduce(_ or _)`
+     *  denote the same set of values.
+     */
+    def decompose(sym: Symbol, tp: Type): List[Type] = {
+      import dotty.tools.dotc.transform.patmat.SpaceEngine
+      val se = new SpaceEngine
+      sym.children.map(x => se.refine(tp, x)).filter(_.exists)
+    }
+
+    (tp1.dealias, tp2.dealias) match {
+      case (tp1: ConstantType, tp2: ConstantType) =>
+        tp1 == tp2
+      case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass =>
+        if (isSubType(tp1, tp2) || isSubType(tp2, tp1)) {
+          true
+        } else {
+          val cls1 = tp1.classSymbol
+          val cls2 = tp2.classSymbol
+          if (cls1.is(Final) || cls2.is(Final))
+            // One of these types is final and they are not mutually
+            // subtype, so they must be unrelated.
+            false
+          else if (!cls2.is(Trait) && !cls1.is(Trait))
+            // Both of these types are classes and they are not mutually
+            // subtype, so they must be unrelated by single inheritance
+            // of classes.
+            false
+          else if (isClosed(cls1))
+            decompose(cls1, tp1).exists(x => intersecting(x, tp2))
+          else if (isClosed(cls2))
+            decompose(cls2, tp2).exists(x => intersecting(x, tp1))
+          else
+            true
+        }
+      case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) =>
+        // Unboxed x.zip(y).zip(z).forall { case ((a, b), c) => f(a, b, c) }
+        def zip_zip_forall[A, B, C](x: List[A], y: List[B], z: List[C])(f: (A, B, C) => Boolean): Boolean =
+          x match {
+            case x :: xs => y match {
+              case y :: ys => z match {
+                case z :: zs => f(x, y, z) && zip_zip_forall(xs, ys, zs)(f)
+                case _ => true
+              }
+              case _ => true
+            }
+            case _ => true
+          }
+
+        tycon1 == tycon2 &&
+          zip_zip_forall(args1, args2, tycon1.typeParams) {
+            (arg1, arg2, tparam) =>
+              val v = tparam.paramVariance
+              // Note that the logic below is conservative in that is
+              // assumes that Covariant type parameters are Contravariant
+              // type
+              if (v > 0)
+                intersecting(arg1, arg2) || {
+                  // We still need to proof that `Nothing` is not a valid
+                  // instantiation of this type parameter. We have two ways
+                  // to get to that conclusion:
+                  // 1. `Nothing` does not conform to the type parameter's lb
+                  // 2. `tycon1` has a field typed with this type parameter.
+                  //
+                  // Because of separate compilation, the use of 2. is
+                  // limited to case classes.
+                  import dotty.tools.dotc.typer.Applications.productSelectorTypes
+                  val lowerBoundedByNothing = tparam.paramInfo.bounds.lo eq NothingType
+                  val typeUsedAsField =
+                    productSelectorTypes(tycon1, null).exists {
+                      case tp: TypeRef =>
+                        (tp.designator: Any) == tparam // Bingo!
+                      case _ =>
+                        false
+                    }
+                  lowerBoundedByNothing && !typeUsedAsField
+                }
+              else if (v < 0)
+                // Contravariant case: a value where this type parameter is
+                // instantiated to `Any` belongs to both types.
+                true
+              else
+                isSameType(arg1, arg2) // TODO: handle uninstanciated types
+        }
+      case (tp1: HKLambda, tp2: HKLambda) =>
+        intersecting(tp1.resType, tp2.resType)
+      case (_: HKLambda, _) =>
+        // The intersection is ill kinded and therefore empty.
+        false
+      case (_, _: HKLambda) =>
+        false
+      case (tp1: OrType, _)  =>
+        intersecting(tp1.tp1, tp2) || intersecting(tp1.tp2, tp2)
+      case (_, tp2: OrType)  =>
+        intersecting(tp1, tp2.tp1) || intersecting(tp1, tp2.tp2)
+      case (tp1: AndType, _) =>
+        intersecting(tp1.tp1, tp2) && intersecting(tp1.tp2, tp2) && intersecting(tp1.tp1, tp1.tp2)
+      case (_, tp2: AndType) =>
+        intersecting(tp1, tp2.tp1) && intersecting(tp1, tp2.tp2) && intersecting(tp2.tp1, tp2.tp2)
+      case (tp1: TypeProxy, tp2: TypeProxy) =>
+        intersecting(tp1.underlying, tp2) && intersecting(tp1, tp2.underlying)
+      case (tp1: TypeProxy, _) =>
+        intersecting(tp1.underlying, tp2)
+      case (_, tp2: TypeProxy) =>
+        intersecting(tp1, tp2.underlying)
+      case _ =>
+        true
+    }
+  }
 }
 
 object TypeComparer {
@@ -1969,8 +2097,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
     super.typeVarInstance(tvar)
   }
 
-  def matchCase(scrut: Type, cas: Type, instantiate: Boolean)(implicit ctx: Context): Type = {
-
+  def matchCases(scrut: Type, cases: List[Type])(implicit ctx: Context): Type = {
     def paramInstances = new TypeAccumulator[Array[Type]] {
       def apply(inst: Array[Type], t: Type) = t match {
         case t @ TypeParamRef(b, n) if b `eq` caseLambda =>
@@ -1989,29 +2116,45 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
       }
     }
 
-    val saved = constraint
-    try {
-      inFrozenConstraint {
-        val cas1 = cas match {
-          case cas: HKTypeLambda =>
-            caseLambda = constrained(cas)
-            caseLambda.resultType
-          case _ =>
-            cas
-        }
-        val defn.FunctionOf(pat :: Nil, body, _, _) = cas1
-        if (isSubType(scrut, pat))
-          caseLambda match {
-            case caseLambda: HKTypeLambda if instantiate =>
-              val instances = paramInstances(new Array(caseLambda.paramNames.length), pat)
-              instantiateParams(instances)(body)
+    var result: Type = NoType
+    var remainingCases = cases
+    while (!remainingCases.isEmpty) {
+      val (cas :: cass) = remainingCases
+      remainingCases = cass
+      val saved = constraint
+      try {
+        inFrozenConstraint {
+          val cas1 = cas match {
+            case cas: HKTypeLambda =>
+              caseLambda = constrained(cas)
+              caseLambda.resultType
             case _ =>
-              body
+              cas
           }
-        else NoType
+          val defn.FunctionOf(pat :: Nil, body, _, _) = cas1
+          if (isSubType(scrut, pat)) {
+            // `scrut` is a subtype of `pat`: *It's a Match!*
+            result = caseLambda match {
+              case caseLambda: HKTypeLambda =>
+                val instances = paramInstances(new Array(caseLambda.paramNames.length), pat)
+                instantiateParams(instances)(body)
+              case _ =>
+                body
+            }
+            remainingCases = Nil
+          } else if (!intersecting(scrut, pat)) {
+            // We found a proof that `scrut` and  `pat` are incompatible.
+            // The search continues.
+          } else {
+            // We are stuck: this match type instanciation is irreducible.
+            result = NoType
+            remainingCases = Nil
+          }
+        }
       }
+      finally constraint = saved
     }
-    finally constraint = saved
+    result
   }
 }
 
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 0db9cca05757..acf2b3f33461 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -3764,22 +3764,10 @@ object Types {
 
     override def tryNormalize(implicit ctx: Context): Type = reduced.normalized
 
-    final def cantPossiblyMatch(cas: Type)(implicit ctx: Context): Boolean =
-      true  // should be refined if we allow overlapping cases
-
     def reduced(implicit ctx: Context): Type = {
       val trackingCtx = ctx.fresh.setTypeComparerFn(new TrackingTypeComparer(_))
       val typeComparer = trackingCtx.typeComparer.asInstanceOf[TrackingTypeComparer]
 
-      def reduceSequential(cases: List[Type])(implicit ctx: Context): Type = cases match {
-        case Nil => NoType
-        case cas :: cases1 =>
-          val r = typeComparer.matchCase(scrutinee, cas, instantiate = true)
-          if (r.exists) r
-          else if (cantPossiblyMatch(cas)) reduceSequential(cases1)
-          else NoType
-      }
-
       def contextInfo(tp: Type): Type = tp match {
         case tp: TypeParamRef =>
           val constraint = ctx.typerState.constraint
@@ -3812,7 +3800,7 @@ object Types {
           trace(i"reduce match type $this $hashCode", typr, show = true) {
             try
               if (defn.isBottomType(scrutinee)) defn.NothingType
-              else reduceSequential(cases)(trackingCtx)
+              else typeComparer.matchCases(scrutinee, cases)(trackingCtx)
             catch {
               case ex: Throwable =>
                 handleRecursive("reduce type ", i"$scrutinee match ...", ex)
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index 4900a99cda64..abe881a27da3 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -42,7 +42,7 @@ object Applications {
     val ref = extractorMember(tp, name)
     if (ref.isOverloaded)
       errorType(i"Overloaded reference to $ref is not allowed in extractor", errorPos)
-    ref.info.widenExpr.annotatedToRepeated.dealiasKeepAnnots
+    ref.info.widenExpr.annotatedToRepeated
   }
 
   /** Does `tp` fit the "product match" conditions as an unapply result type
diff --git a/compiler/test/dotty/tools/dotc/reporting/ErrorMessagesTests.scala b/compiler/test/dotty/tools/dotc/reporting/ErrorMessagesTests.scala
index 8d5f692aa65d..c67414b6ae58 100644
--- a/compiler/test/dotty/tools/dotc/reporting/ErrorMessagesTests.scala
+++ b/compiler/test/dotty/tools/dotc/reporting/ErrorMessagesTests.scala
@@ -1362,7 +1362,7 @@ class ErrorMessagesTests extends ErrorMessagesTest {
         assertMessageCount(1, messages)
         val UnapplyInvalidNumberOfArguments(qual, argTypes) :: Nil = messages
         assertEquals("Boo", qual.show)
-        assertEquals("(class Int, class String)", argTypes.map(_.typeSymbol).mkString("(", ", ", ")"))
+        assertEquals("(class Int, type String)", argTypes.map(_.typeSymbol).mkString("(", ", ", ")"))
       }
 
   @Test def unapplyInvalidReturnType =
diff --git a/tests/neg/matchtype-seq.scala b/tests/neg/matchtype-seq.scala
new file mode 100644
index 000000000000..9ea307e9c6df
--- /dev/null
+++ b/tests/neg/matchtype-seq.scala
@@ -0,0 +1,145 @@
+object Test {
+  type T1[X] = X match {
+    case 1 => Int
+    case 2 => String
+  }
+
+  identity[T1[1]](1)
+  identity[T1[2]]("")
+  identity[T1[3]]("") // error
+  identity[T1[3]](1) // error
+  identity[T1[Int]]("") // error
+  identity[T1[Int]](1) // error
+
+  type T2[X] = X match {
+    case 1 => Int
+    case _ => String
+  }
+
+  identity[T2[1]](1)
+  identity[T2[2]]("")
+  identity[T2[Int]]("") // error
+  identity[T2[2]](1) // error
+  identity[T2[Int]](1) // error
+
+  sealed trait A
+  final class B extends A
+  final class C extends A
+
+  type T3[X] = X match {
+    case B => Int
+    case C => String
+  }
+
+  identity[T3[B]](1)
+  identity[T3[C]]("")
+  identity[T3[A]](1) // error
+  identity[T3[A]]("") // error
+
+  type T4[X] = X match {
+    case A => Int
+    case C => String
+  }
+
+  identity[T4[B]](1)
+  identity[T4[C]](1)
+  identity[T4[A]](1)
+
+  type T5[X] = X match {
+    case C => String
+    case A => Int
+  }
+
+  identity[T5[C]]("")
+  identity[T5[B]](1)
+  identity[T5[A]](1) // error
+  identity[T5[A]]("") // error
+
+  class D
+
+  type T6[X] = X match {
+    case A => Int
+    case D => String
+  }
+
+  identity[T6[A]](1)
+  identity[T6[B]](1)
+  identity[T6[C]](1)
+  identity[T6[D]]("")
+
+  trait A2
+  final class B2 extends A2
+  final class C2 extends A2
+
+  type T7[X] = X match {
+    case A2 => Int
+    case D => String
+  }
+
+  identity[T7[A2]](1)
+  identity[T7[B2]](1)
+  identity[T7[C2]](1)
+  identity[T7[D]]("") // error
+  identity[T7[D]](1) // error
+
+  trait E1
+  trait E2
+
+  type T8[X] = X match {
+    case E1 => Int
+    case E2 => String
+  }
+
+  identity[T8[E1]](1)
+  identity[T8[E2]](1) // error
+  identity[T8[E1]]("") // error
+  identity[T8[E2]]("") // error
+
+  type T9[X] = X match {
+    case Tuple2[Int, String] => Int
+    case Tuple2[String, Int] => String
+  }
+
+  identity[T9[Tuple2[Int, String]]](1)
+  identity[T9[Tuple2[String, Int]]]("1")
+  identity[T9[Tuple2[Nothing, String]]](1)
+  identity[T9[Tuple2[String, Nothing]]]("1")
+  identity[T9[Tuple2[Int, Nothing]]](1)
+  identity[T9[Tuple2[Nothing, Int]]]("1")
+  identity[T9[Tuple2[_, _]]]("") // error
+  identity[T9[Tuple2[_, _]]](1) // error
+  identity[T9[Tuple2[Any, Any]]]("") // error
+  identity[T9[Tuple2[Any, Any]]](1) // error
+
+  case class Box2[+A, +B, +C](a: A, b: B)
+
+  type TA[X] = X match {
+    case Box2[Int, Int, Int] => Int
+    case Box2[Int, Int, String] => String
+  }
+
+  identity[TA[Box2[Int, Int, Int]]](1)
+  identity[TA[Box2[Int, Int, String]]](1) // error
+  identity[TA[Box2[Int, Int, String]]]("") // error
+
+  case class Box2_I[A, B, C](a: A, b: B)
+
+  type TC[X] = X match {
+    case Box2_I[Int, Int, Int] => Int
+    case Box2_I[Int, Int, String] => String
+  }
+
+  identity[TC[Box2_I[Int, Int, Int]]](1)
+  identity[TC[Box2_I[Int, Int, String]]]("")
+
+
+  case class Box2_C[A, B, -C](a: A, b: B)
+
+  type TD[X] = X match {
+    case Box2_C[Int, Int, Int] => Int
+    case Box2_C[Int, Int, String] => String
+  }
+
+  identity[TD[Box2_C[Int, Int, Int]]](1)
+  identity[TD[Box2_C[Int, Int, String]]]("") // error
+}

From 60d0e208d58ba2d5547c7ebc6253e8aefe5061a8 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Thu, 28 Feb 2019 13:30:41 +0100
Subject: [PATCH 08/20] Replace Space.inhabited by typeComparer.intersecting

This commit also updates pattern matching exhaustivity tests for the new
type inhavitation decision procedure.

The diffs in t6420 and t7466 comes from a bug a the previous algorithm
that would conclue that given `val a: Int`, `1` and `a.type` are non-
intersecting because they are both singleton types. However, we can only
get to that conclusion when both types are ConstantTypes.

The diff in andtype-opentype-interaction come from the fact that the new
decomposition of sealed types is more powerful than the previous one.
For instance, we can now rule out `SealedClass & OpenTrait` as both
types are provably non intersecting.

i3574.scala is pending for now due to the removal of inhabitation check
of childrens, it will be enabled back in a subsequent commit.
---
 .../tools/dotc/transform/patmat/Space.scala   | 104 +-----------------
 .../patmat/andtype-opentype-interaction.check |  12 +-
 tests/patmat/t6420.check                      |   2 +-
 tests/patmat/t7466.check                      |   2 +-
 tests/{patmat => pending}/i3574.scala         |   0
 5 files changed, 12 insertions(+), 108 deletions(-)
 rename tests/{patmat => pending}/i3574.scala (100%)

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index 3b184b6bb9fd..692d09443ada 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -298,16 +298,14 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       // Since projections of types don't include null, intersection with null is empty.
       return Empty
     }
-    val and = AndType(tp1, tp2)
-    // Then, no leaf of the and-type tree `and` is a subtype of `and`.
-    val res = inhabited(and)
+    val res = ctx.typeComparer.intersecting(tp1, tp2)
 
-    debug.println(s"atomic intersection: ${and.show} = ${res}")
+    debug.println(s"atomic intersection: ${AndType(tp1, tp2).show} = ${res}")
 
     if (!res) Empty
     else if (tp1.isSingleton) Typ(tp1, true)
     else if (tp2.isSingleton) Typ(tp2, true)
-    else Typ(and, true)
+    else Typ(AndType(tp1, tp2), true)
   }
 
   /** Whether the extractor is irrefutable */
@@ -516,101 +514,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
 
     val childTp = if (child.isTerm) child.termRef else child.typeRef
 
-    val resTp = instantiate(childTp, parent)(ctx.fresh.setNewTyperState())
-
-    if (!resTp.exists || !inhabited(resTp)) {
-      debug.println(s"[refine] unqualified child ousted: ${childTp.show} !< ${parent.show}")
-      NoType
-    }
-    else {
-      debug.println(s"$child instantiated ------> $resTp")
-      resTp.dealias
-    }
-  }
-
-  /** Can this type be inhabited by a value?
-   *
-   *  Check is based on the following facts:
-   *
-   *  - single inheritance of classes
-   *  - final class cannot be extended
-   *  - intersection of a singleton type with another irrelevant type  (patmat/i3574.scala)
-   *
-   */
-  def inhabited(tp: Type)(implicit ctx: Context): Boolean = {
-    // convert top-level type shape into "conjunctive normal form"
-    def cnf(tp: Type): Type = tp match {
-      case AndType(OrType(l, r), tp)      =>
-        OrType(cnf(AndType(l, tp)), cnf(AndType(r, tp)))
-      case AndType(tp, o: OrType)         =>
-        cnf(AndType(o, tp))
-      case AndType(l, r)                  =>
-        val l1 = cnf(l)
-        val r1 = cnf(r)
-        if (l1.ne(l) || r1.ne(r)) cnf(AndType(l1, r1))
-        else AndType(l1, r1)
-      case OrType(l, r)                   =>
-        OrType(cnf(l), cnf(r))
-      case tp @ RefinedType(OrType(tp1, tp2), _, _)  =>
-        OrType(
-          cnf(tp.derivedRefinedType(tp1, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo)),
-          cnf(tp.derivedRefinedType(tp2, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo))
-        )
-      case tp: RefinedType                =>
-        val parent1 = cnf(tp.parent)
-        val tp1 = tp.derivedRefinedType(parent1, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo)
-
-        if (parent1.ne(tp.parent)) cnf(tp1) else tp1
-      case tp: TypeAlias                  =>
-        cnf(tp.alias)
-      case _                              =>
-        tp
-    }
-
-    def isSingleton(tp: Type): Boolean = tp.dealias match {
-      case AndType(l, r)  => isSingleton(l) || isSingleton(r)
-      case OrType(l, r)   => isSingleton(l) && isSingleton(r)
-      case tp             => tp.isSingleton
-    }
-
-    def recur(tp: Type): Boolean = tp.dealias match {
-      case AndType(tp1, tp2) =>
-        recur(tp1) && recur(tp2) && {
-          val bases1 = tp1.widenDealias.classSymbols
-          val bases2 = tp2.widenDealias.classSymbols
-
-          debug.println(s"bases of ${tp1.show}: " + bases1)
-          debug.println(s"bases of ${tp2.show}: " + bases2)
-          debug.println(s"${tp1.show} <:< ${tp2.show} : " +  (tp1 <:< tp2))
-          debug.println(s"${tp2.show} <:< ${tp1.show} : " +  (tp2 <:< tp1))
-
-          val noClassConflict =
-            bases1.forall(sym1 => sym1.is(Trait) || bases2.forall(sym2 => sym2.is(Trait) || sym1.isSubClass(sym2))) ||
-            bases1.forall(sym1 => sym1.is(Trait) || bases2.forall(sym2 => sym2.is(Trait) || sym2.isSubClass(sym1)))
-
-          debug.println(s"class conflict for ${tp.show}? " + !noClassConflict)
-
-          noClassConflict &&
-            (!isSingleton(tp1) || tp1 <:< tp2) &&
-            (!isSingleton(tp2) || tp2 <:< tp1) &&
-            (!bases1.exists(_ is Final) || tp1 <:< maxTypeMap.apply(tp2)) &&
-            (!bases2.exists(_ is Final) || tp2 <:< maxTypeMap.apply(tp1))
-        }
-      case OrType(tp1, tp2) =>
-        recur(tp1) || recur(tp2)
-      case tp: RefinedType =>
-        recur(tp.parent)
-      case tp: TypeRef =>
-        recur(tp.prefix) && !(tp.classSymbol.is(AbstractFinal))
-      case _ =>
-        true
-    }
-
-    val res = recur(cnf(tp))
-
-    debug.println(s"${tp.show} inhabited?  " + res)
-
-    res
+    instantiate(childTp, parent)(ctx.fresh.setNewTyperState()).dealias
   }
 
   /** expose abstract type references to their bounds or tvars according to variance */
diff --git a/tests/patmat/andtype-opentype-interaction.check b/tests/patmat/andtype-opentype-interaction.check
index 1d09f03d61e5..a9d8618adad0 100644
--- a/tests/patmat/andtype-opentype-interaction.check
+++ b/tests/patmat/andtype-opentype-interaction.check
@@ -1,6 +1,6 @@
-23: Pattern Match Exhaustivity: _: Trait & OpenTrait, _: Clazz & OpenTrait, _: AbstractClass & OpenTrait, _: SealedTrait & OpenTrait, _: SealedClass & OpenTrait, _: SealedAbstractClass & OpenTrait
-27: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: SealedTrait & OpenTrait & OpenTrait2, _: SealedClass & OpenTrait & OpenTrait2, _: SealedAbstractClass & OpenTrait & OpenTrait2
-31: Pattern Match Exhaustivity: _: Trait & OpenClass, _: SealedTrait & OpenClass
-35: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenClass, _: SealedTrait & OpenTrait & OpenClass
-43: Pattern Match Exhaustivity: _: Trait & OpenAbstractClass, _: SealedTrait & OpenAbstractClass
-47: Pattern Match Exhaustivity: _: Trait & OpenClass & (OpenTrait & OpenClassSubclass), _: SealedTrait & OpenClass & (OpenTrait & OpenClassSubclass)
\ No newline at end of file
+23: Pattern Match Exhaustivity: _: Trait & OpenTrait, _: Clazz & OpenTrait, _: AbstractClass & OpenTrait, _: SealedClass & OpenTrait
+27: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: SealedClass & OpenTrait & OpenTrait2
+31: Pattern Match Exhaustivity: _: Trait & OpenClass
+35: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenClass
+43: Pattern Match Exhaustivity: _: Trait & OpenAbstractClass
+47: Pattern Match Exhaustivity: _: Trait & OpenClass & (OpenTrait & OpenClassSubclass)
diff --git a/tests/patmat/t6420.check b/tests/patmat/t6420.check
index 021a88adc6c3..a572f53bf57b 100644
--- a/tests/patmat/t6420.check
+++ b/tests/patmat/t6420.check
@@ -1 +1 @@
-5: Pattern Match Exhaustivity: (_: List, List(true, _: _*)), (_: List, List(false, _: _*)), (_: List, Nil)
+5: Pattern Match Exhaustivity: (List(true, _: _*), List(true, _: _*)), (List(true, _: _*), List(false, _: _*)), (List(true, _: _*), Nil), (List(false, _: _*), List(true, _: _*)), (List(false, _: _*), List(false, _: _*)), (List(false, _: _*), Nil), (Nil, List(true, _: _*)), (Nil, List(false, _: _*)), (Nil, Nil), (_: List, List(true, _: _*)), (_: List, List(false, _: _*)), (_: List, Nil)
diff --git a/tests/patmat/t7466.check b/tests/patmat/t7466.check
index dfd3b3061f03..4ceeb01233e5 100644
--- a/tests/patmat/t7466.check
+++ b/tests/patmat/t7466.check
@@ -1 +1 @@
-8: Pattern Match Exhaustivity: (_, true), (_, false)
+8: Pattern Match Exhaustivity: (true, true), (true, false), (false, true), (false, false), (_, true), (_, false)
diff --git a/tests/patmat/i3574.scala b/tests/pending/i3574.scala
similarity index 100%
rename from tests/patmat/i3574.scala
rename to tests/pending/i3574.scala

From d1180cce5a76e7275114e8d40d3bdf747bdd8fc0 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Tue, 26 Feb 2019 12:15:26 +0100
Subject: [PATCH 09/20] Move refineUsingParent to Typer

---
 .../dotty/tools/dotc/core/TypeComparer.scala  |   7 +-
 .../tools/dotc/transform/patmat/Space.scala   | 156 +-----------------
 .../src/dotty/tools/dotc/typer/Typer.scala    | 148 +++++++++++++++++
 3 files changed, 152 insertions(+), 159 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 009e170bee68..57df17f018ca 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1898,11 +1898,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
      *  It should hold that `tp` and `decompose(tp).reduce(_ or _)`
      *  denote the same set of values.
      */
-    def decompose(sym: Symbol, tp: Type): List[Type] = {
-      import dotty.tools.dotc.transform.patmat.SpaceEngine
-      val se = new SpaceEngine
-      sym.children.map(x => se.refine(tp, x)).filter(_.exists)
-    }
+    def decompose(sym: Symbol, tp: Type): List[Type] =
+      sym.children.map(x => ctx.typer.refineUsingParent(tp, x)).filter(_.exists)
 
     (tp1.dealias, tp2.dealias) match {
       case (tp1: ConstantType, tp2: ConstantType) =>
diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index 692d09443ada..24ee98750aad 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -466,10 +466,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
         children.map(sym => Typ(sym.termRef, true))
       case tp =>
         val parts = children.map { sym =>
-          if (sym.is(ModuleClass))
-            refine(tp, sym.sourceModule)
-          else
-            refine(tp, sym)
+          val sym1 = if (sym.is(ModuleClass)) sym.sourceModule else sym
+          ctx.typer.refineUsingParent(tp, sym1)
         } filter(_.exists)
 
         debug.println(s"${tp.show} decomposes to [${parts.map(_.show).mkString(", ")}]")
@@ -478,156 +476,6 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     }
   }
 
-  /** Refine child based on parent
-   *
-   *  In child class definition, we have:
-   *
-   *      class Child[Ts] extends path.Parent[Us] with Es
-   *      object Child extends path.Parent[Us] with Es
-   *      val child = new path.Parent[Us] with Es           // enum values
-   *
-   *  Given a parent type `parent` and a child symbol `child`, we infer the prefix
-   *  and type parameters for the child:
-   *
-   *      prefix.child[Vs] <:< parent
-   *
-   *  where `Vs` are fresh type variables and `prefix` is the symbol prefix with all
-   *  non-module and non-package `ThisType` replaced by fresh type variables.
-   *
-   *  If the subtyping is true, the instantiated type `p.child[Vs]` is
-   *  returned. Otherwise, `NoType` is returned.
-   *
-   */
-  def refine(parent: Type, child: Symbol): Type = {
-    if (child.isTerm && child.is(Case, butNot = Module)) return child.termRef // enum vals always match
-
-    // <local child> is a place holder from Scalac, it is hopeless to instantiate it.
-    //
-    // Quote from scalac (from nsc/symtab/classfile/Pickler.scala):
-    //
-    //     ...When a sealed class/trait has local subclasses, a single
-    //     <local child> class symbol is added as pickled child
-    //     (instead of a reference to the anonymous class; that was done
-    //     initially, but seems not to work, ...).
-    //
-    if (child.name == tpnme.LOCAL_CHILD) return child.typeRef
-
-    val childTp = if (child.isTerm) child.termRef else child.typeRef
-
-    instantiate(childTp, parent)(ctx.fresh.setNewTyperState()).dealias
-  }
-
-  /** expose abstract type references to their bounds or tvars according to variance */
-  private class AbstractTypeMap(maximize: Boolean)(implicit ctx: Context) extends TypeMap {
-    def expose(lo: Type, hi: Type): Type =
-      if (variance == 0)
-        newTypeVar(TypeBounds(lo, hi))
-      else if (variance == 1)
-        if (maximize) hi else lo
-      else
-        if (maximize) lo else hi
-
-    def apply(tp: Type): Type = tp match {
-      case tp: TypeRef if isBounds(tp.underlying) =>
-        val lo = this(tp.info.loBound)
-        val hi = this(tp.info.hiBound)
-        // See tests/patmat/gadt.scala  tests/patmat/exhausting.scala  tests/patmat/t9657.scala
-        val exposed = expose(lo, hi)
-        debug.println(s"$tp exposed to =====> $exposed")
-        exposed
-
-      case AppliedType(tycon: TypeRef, args) if isBounds(tycon.underlying) =>
-        val args2 = args.map(this)
-        val lo = this(tycon.info.loBound).applyIfParameterized(args2)
-        val hi = this(tycon.info.hiBound).applyIfParameterized(args2)
-        val exposed = expose(lo, hi)
-        debug.println(s"$tp exposed to =====> $exposed")
-        exposed
-
-      case _ =>
-        mapOver(tp)
-    }
-  }
-
-  private def minTypeMap(implicit ctx: Context) = new AbstractTypeMap(maximize = false)
-  private def maxTypeMap(implicit ctx: Context) = new AbstractTypeMap(maximize = true)
-
-  /** Instantiate type `tp1` to be a subtype of `tp2`
-   *
-   *  Return the instantiated type if type parameters and this type
-   *  in `tp1` can be instantiated such that `tp1 <:< tp2`.
-   *
-   *  Otherwise, return NoType.
-   *
-   */
-  def instantiate(tp1: NamedType, tp2: Type)(implicit ctx: Context): Type = {
-    // Fix subtype checking for child instantiation,
-    // such that `Foo(Test.this.foo) <:< Foo(Foo.this)`
-    // See tests/patmat/i3938.scala
-    class RemoveThisMap extends TypeMap {
-      var prefixTVar: Type = null
-      def apply(tp: Type): Type = tp match {
-        case ThisType(tref: TypeRef) if !tref.symbol.isStaticOwner =>
-          if (tref.symbol.is(Module))
-            TermRef(this(tref.prefix), tref.symbol.sourceModule)
-          else if (prefixTVar != null)
-            this(tref)
-          else {
-            prefixTVar = WildcardType  // prevent recursive call from assigning it
-            prefixTVar = newTypeVar(TypeBounds.upper(this(tref)))
-            prefixTVar
-          }
-        case tp => mapOver(tp)
-      }
-    }
-
-    // replace uninstantiated type vars with WildcardType, check tests/patmat/3333.scala
-    def instUndetMap(implicit ctx: Context) = new TypeMap {
-      def apply(t: Type): Type = t match {
-        case tvar: TypeVar if !tvar.isInstantiated => WildcardType(tvar.origin.underlying.bounds)
-        case _ => mapOver(t)
-      }
-    }
-
-    val removeThisType = new RemoveThisMap
-    val tvars = tp1.typeParams.map { tparam => newTypeVar(tparam.paramInfo.bounds) }
-    val protoTp1 = removeThisType.apply(tp1).appliedTo(tvars)
-
-    val force = new ForceDegree.Value(
-      tvar =>
-        !(ctx.typerState.constraint.entry(tvar.origin) `eq` tvar.origin.underlying) ||
-        (tvar `eq` removeThisType.prefixTVar),
-      minimizeAll = false,
-      allowBottom = false
-    )
-
-    // If parent contains a reference to an abstract type, then we should
-    // refine subtype checking to eliminate abstract types according to
-    // variance. As this logic is only needed in exhaustivity check,
-    // we manually patch subtyping check instead of changing TypeComparer.
-    // See tests/patmat/i3645b.scala
-    def parentQualify = tp1.widen.classSymbol.info.parents.exists { parent =>
-      implicit val ictx = ctx.fresh.setNewTyperState()
-      parent.argInfos.nonEmpty && minTypeMap.apply(parent) <:< maxTypeMap.apply(tp2)
-    }
-
-    if (protoTp1 <:< tp2) {
-      if (isFullyDefined(protoTp1, force)) protoTp1
-      else instUndetMap.apply(protoTp1)
-    }
-    else {
-      val protoTp2 = maxTypeMap.apply(tp2)
-      if (protoTp1 <:< protoTp2 || parentQualify) {
-        if (isFullyDefined(AndType(protoTp1, protoTp2), force)) protoTp1
-        else instUndetMap.apply(protoTp1)
-      }
-      else {
-        debug.println(s"$protoTp1 <:< $protoTp2 = false")
-        NoType
-      }
-    }
-  }
-
   /** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
   def canDecompose(tp: Type): Boolean = {
     val dealiasedTp = tp.dealias
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index d3664fab5270..994c139ef79f 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -2929,4 +2929,152 @@ class Typer extends Namer
         !tree.tpe.isRef(defn.UnitClass) && !isSelfOrSuperConstrCall(tree))
       ctx.warning(PureExpressionInStatementPosition(original, exprOwner), original.sourcePos)
   }
+
+  /** Refine child based on parent
+   *
+   *  In child class definition, we have:
+   *
+   *      class Child[Ts] extends path.Parent[Us] with Es
+   *      object Child extends path.Parent[Us] with Es
+   *      val child = new path.Parent[Us] with Es           // enum values
+   *
+   *  Given a parent type `parent` and a child symbol `child`, we infer the prefix
+   *  and type parameters for the child:
+   *
+   *      prefix.child[Vs] <:< parent
+   *
+   *  where `Vs` are fresh type variables and `prefix` is the symbol prefix with all
+   *  non-module and non-package `ThisType` replaced by fresh type variables.
+   *
+   *  If the subtyping is true, the instantiated type `p.child[Vs]` is
+   *  returned. Otherwise, `NoType` is returned.
+   */
+  def refineUsingParent(parent: Type, child: Symbol)(implicit ctx: Context): Type = {
+    if (child.isTerm && child.is(Case, butNot = Module)) return child.termRef // enum vals always match
+
+    // <local child> is a place holder from Scalac, it is hopeless to instantiate it.
+    //
+    // Quote from scalac (from nsc/symtab/classfile/Pickler.scala):
+    //
+    //     ...When a sealed class/trait has local subclasses, a single
+    //     <local child> class symbol is added as pickled child
+    //     (instead of a reference to the anonymous class; that was done
+    //     initially, but seems not to work, ...).
+    //
+    if (child.name == tpnme.LOCAL_CHILD) return child.typeRef
+
+    val childTp = if (child.isTerm) child.termRef else child.typeRef
+
+    instantiate(childTp, parent)(ctx.fresh.setNewTyperState()).dealias
+  }
+
+  /** Instantiate type `tp1` to be a subtype of `tp2`
+   *
+   *  Return the instantiated type if type parameters and this type
+   *  in `tp1` can be instantiated such that `tp1 <:< tp2`.
+   *
+   *  Otherwise, return NoType.
+   */
+  private def instantiate(tp1: NamedType, tp2: Type)(implicit ctx: Context): Type = {
+    /** expose abstract type references to their bounds or tvars according to variance */
+    class AbstractTypeMap(maximize: Boolean)(implicit ctx: Context) extends TypeMap {
+      def expose(lo: Type, hi: Type): Type =
+        if (variance == 0)
+          newTypeVar(TypeBounds(lo, hi))
+        else if (variance == 1)
+          if (maximize) hi else lo
+        else
+          if (maximize) lo else hi
+
+      def apply(tp: Type): Type = tp match {
+        case tp: TypeRef if isBounds(tp.underlying) =>
+          val lo = this(tp.info.loBound)
+          val hi = this(tp.info.hiBound)
+          // See tests/patmat/gadt.scala  tests/patmat/exhausting.scala  tests/patmat/t9657.scala
+          val exposed = expose(lo, hi)
+          typr.println(s"$tp exposed to =====> $exposed")
+          exposed
+
+        case AppliedType(tycon: TypeRef, args) if isBounds(tycon.underlying) =>
+          val args2 = args.map(this)
+          val lo = this(tycon.info.loBound).applyIfParameterized(args2)
+          val hi = this(tycon.info.hiBound).applyIfParameterized(args2)
+          val exposed = expose(lo, hi)
+          typr.println(s"$tp exposed to =====> $exposed")
+          exposed
+
+        case _ =>
+          mapOver(tp)
+      }
+    }
+
+    def minTypeMap(implicit ctx: Context) = new AbstractTypeMap(maximize = false)
+    def maxTypeMap(implicit ctx: Context) = new AbstractTypeMap(maximize = true)
+
+    // Fix subtype checking for child instantiation,
+    // such that `Foo(Test.this.foo) <:< Foo(Foo.this)`
+    // See tests/patmat/i3938.scala
+    class RemoveThisMap extends TypeMap {
+      var prefixTVar: Type = null
+      def apply(tp: Type): Type = tp match {
+        case ThisType(tref: TypeRef) if !tref.symbol.isStaticOwner =>
+          if (tref.symbol.is(Module))
+            TermRef(this(tref.prefix), tref.symbol.sourceModule)
+          else if (prefixTVar != null)
+            this(tref)
+          else {
+            prefixTVar = WildcardType  // prevent recursive call from assigning it
+            prefixTVar = newTypeVar(TypeBounds.upper(this(tref)))
+            prefixTVar
+          }
+        case tp => mapOver(tp)
+      }
+    }
+
+    // replace uninstantiated type vars with WildcardType, check tests/patmat/3333.scala
+    def instUndetMap(implicit ctx: Context) = new TypeMap {
+      def apply(t: Type): Type = t match {
+        case tvar: TypeVar if !tvar.isInstantiated => WildcardType(tvar.origin.underlying.bounds)
+        case _ => mapOver(t)
+      }
+    }
+
+    val removeThisType = new RemoveThisMap
+    val tvars = tp1.typeParams.map { tparam => newTypeVar(tparam.paramInfo.bounds) }
+    val protoTp1 = removeThisType.apply(tp1).appliedTo(tvars)
+
+    val force = new ForceDegree.Value(
+      tvar =>
+        !(ctx.typerState.constraint.entry(tvar.origin) `eq` tvar.origin.underlying) ||
+        (tvar `eq` removeThisType.prefixTVar),
+      minimizeAll = false,
+      allowBottom = false
+    )
+
+    // If parent contains a reference to an abstract type, then we should
+    // refine subtype checking to eliminate abstract types according to
+    // variance. As this logic is only needed in exhaustivity check,
+    // we manually patch subtyping check instead of changing TypeComparer.
+    // See tests/patmat/i3645b.scala
+    def parentQualify = tp1.widen.classSymbol.info.parents.exists { parent =>
+      implicit val ictx = ctx.fresh.setNewTyperState()
+      parent.argInfos.nonEmpty && minTypeMap.apply(parent) <:< maxTypeMap.apply(tp2)
+    }
+
+    if (protoTp1 <:< tp2) {
+      if (isFullyDefined(protoTp1, force)) protoTp1
+      else instUndetMap.apply(protoTp1)
+    }
+    else {
+      val protoTp2 = maxTypeMap.apply(tp2)
+      if (protoTp1 <:< protoTp2 || parentQualify) {
+        if (isFullyDefined(AndType(protoTp1, protoTp2), force)) protoTp1
+        else instUndetMap.apply(protoTp1)
+      }
+      else {
+        typr.println(s"$protoTp1 <:< $protoTp2 = false")
+        NoType
+      }
+    }
+  }
 }

From b0c1e7b25709347dbe4d8905756ed1e326193df0 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Thu, 28 Feb 2019 13:32:04 +0100
Subject: [PATCH 10/20] Check inhabitation of children in Space

---
 .../dotty/tools/dotc/transform/patmat/Space.scala  | 14 ++++++++++++--
 tests/{pending => patmat}/i3574.scala              |  0
 2 files changed, 12 insertions(+), 2 deletions(-)
 rename tests/{pending => patmat}/i3574.scala (100%)

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index 24ee98750aad..ece0d995933b 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -467,7 +467,18 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       case tp =>
         val parts = children.map { sym =>
           val sym1 = if (sym.is(ModuleClass)) sym.sourceModule else sym
-          ctx.typer.refineUsingParent(tp, sym1)
+          val refined = ctx.typer.refineUsingParent(tp, sym1)
+          val inhabited = new TypeAccumulator[Boolean] {
+            override def apply(x: Boolean, tp: Type) = x && {
+              tp match {
+                case AndType(tp1, tp2) => ctx.typeComparer.intersecting(tp1, tp2)
+                case OrType(tp1, tp2) => foldOver(x, tp1) || foldOver(x, tp2)
+                case _ => foldOver(x, tp)
+              }
+            }
+          }
+          if (inhabited.apply(true, refined)) refined
+          else NoType
         } filter(_.exists)
 
         debug.println(s"${tp.show} decomposes to [${parts.map(_.show).mkString(", ")}]")
@@ -735,7 +746,6 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
               ctx.warning(MatchCaseOnlyNullWarning(), pat.sourcePos)
             case _ =>
           }
-
         }
       }
     }
diff --git a/tests/pending/i3574.scala b/tests/patmat/i3574.scala
similarity index 100%
rename from tests/pending/i3574.scala
rename to tests/patmat/i3574.scala

From c3d23fe83e2b8bdac541b3c5dc38c2ab58bbc233 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Thu, 28 Feb 2019 15:56:55 +0100
Subject: [PATCH 11/20] Only trust isSameType for fully instanciated types

---
 .../src/dotty/tools/dotc/core/TypeComparer.scala | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 57df17f018ca..aac13fdb05e7 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1973,7 +1973,21 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
                 // instantiated to `Any` belongs to both types.
                 true
               else
-                isSameType(arg1, arg2) // TODO: handle uninstanciated types
+                isSameType(arg1, arg2) || {
+                  // We can only trust a "no" from `isSameType` when both
+                  // `arg1` and `arg2` are fully instantiated.
+                  val fullyInstantiated = new TypeAccumulator[Boolean] {
+                    override def apply(x: Boolean, t: Type) =
+                      x && {
+                        t match {
+                          case _: SkolemType | _: TypeVar | _: TypeParamRef => false
+                          case _ => foldOver(x, t)
+                        }
+                      }
+                  }
+                  !(fullyInstantiated.apply(true, arg1) &&
+                    fullyInstantiated.apply(true, arg2))
+                }
         }
       case (tp1: HKLambda, tp2: HKLambda) =>
         intersecting(tp1.resType, tp2.resType)

From 4f934adec05ae3b9134aed9d82d1b4dcba8b3c7b Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Fri, 1 Mar 2019 17:47:16 +0100
Subject: [PATCH 12/20] Use derivesFrom instead of isSubType for classes

`Some isSubType List` returns `false`, so use derivesFrom instead.
---
 compiler/src/dotty/tools/dotc/core/TypeComparer.scala |  6 +++---
 tests/neg/matchtype-seq.scala                         | 10 ++++++++++
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index aac13fdb05e7..41b5175971ea 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1905,11 +1905,11 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
       case (tp1: ConstantType, tp2: ConstantType) =>
         tp1 == tp2
       case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass =>
-        if (isSubType(tp1, tp2) || isSubType(tp2, tp1)) {
+        val cls1 = tp1.classSymbol
+        val cls2 = tp2.classSymbol
+        if (cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1)) {
           true
         } else {
-          val cls1 = tp1.classSymbol
-          val cls2 = tp2.classSymbol
           if (cls1.is(Final) || cls2.is(Final))
             // One of these types is final and they are not mutually
             // subtype, so they must be unrelated.
diff --git a/tests/neg/matchtype-seq.scala b/tests/neg/matchtype-seq.scala
index 9ea307e9c6df..f431c239b01b 100644
--- a/tests/neg/matchtype-seq.scala
+++ b/tests/neg/matchtype-seq.scala
@@ -143,3 +143,13 @@ object Test {
   identity[TD[Box2_C[Int, Int, Int]]](1)
   identity[TD[Box2_C[Int, Int, String]]]("") // error
 }
+
+object Test2 {
+  type M[A] = A match {
+    case Option[Int] => String
+    case Some[_]     => Int
+  }
+
+  def a[A]: M[Some[A]] = 1  // error
+  def b[A]: M[Some[A]] = "" // error
+}

From 80c25e3cf61f363bb18a8e819d3d82f7af7da2ef Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Mon, 4 Mar 2019 11:16:23 +0100
Subject: [PATCH 13/20] Handle type parameters using symbol.is(TypeParam)

---
 .../src/dotty/tools/dotc/core/TypeComparer.scala |  1 +
 tests/neg/matchtype-seq.scala                    | 16 ++++++++++++++++
 2 files changed, 17 insertions(+)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 41b5175971ea..c2b42a7e5228 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1980,6 +1980,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
                     override def apply(x: Boolean, t: Type) =
                       x && {
                         t match {
+                          case tp: TypeRef if tp.symbol.is(TypeParam) => false
                           case _: SkolemType | _: TypeVar | _: TypeParamRef => false
                           case _ => foldOver(x, t)
                         }
diff --git a/tests/neg/matchtype-seq.scala b/tests/neg/matchtype-seq.scala
index f431c239b01b..d899b3964712 100644
--- a/tests/neg/matchtype-seq.scala
+++ b/tests/neg/matchtype-seq.scala
@@ -153,3 +153,19 @@ object Test2 {
   def a[A]: M[Some[A]] = 1  // error
   def b[A]: M[Some[A]] = "" // error
 }
+
+object Test3 {
+  trait Inv[T]
+
+  type M[A] = A match {
+    case Inv[Int] => String
+    case _ => Int
+  }
+
+  def test[A]: Unit = {
+    // We need to be careful here, we cannot trust the output of type
+    // comparer on `isSameType(A, Int)` since `A` is a type parameter...
+    val a: M[Inv[A]] = 1 // error
+    ()
+  }
+}

From ab74827ad2a27785258a47e66d3e57ec595b3112 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Mon, 4 Mar 2019 11:19:49 +0100
Subject: [PATCH 14/20] Fix AppliedType logic

---
 compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index c2b42a7e5228..8323ee7d04c1 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1926,7 +1926,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
           else
             true
         }
-      case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) =>
+      case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 =>
         // Unboxed x.zip(y).zip(z).forall { case ((a, b), c) => f(a, b, c) }
         def zip_zip_forall[A, B, C](x: List[A], y: List[B], z: List[C])(f: (A, B, C) => Boolean): Boolean =
           x match {
@@ -1940,7 +1940,6 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
             case _ => true
           }
 
-        tycon1 == tycon2 &&
           zip_zip_forall(args1, args2, tycon1.typeParams) {
             (arg1, arg2, tparam) =>
               val v = tparam.paramVariance

From 1df0d8b361c935e80640dd5dee69791e1a3ffc44 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Wed, 6 Mar 2019 10:58:55 +0100
Subject: [PATCH 15/20] Revert "Rename evalOnce to letBind"

This reverts commit 6e39fcbdb2f028dbb4c88fe8c0832e410e5c0f30.
---
 compiler/src/dotty/tools/dotc/ast/tpd.scala                 | 2 +-
 compiler/src/dotty/tools/dotc/transform/Erasure.scala       | 2 +-
 .../src/dotty/tools/dotc/transform/TypeTestsCasts.scala     | 6 +++---
 .../src/dotty/tools/dotc/transform/VCInlineMethods.scala    | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/ast/tpd.scala b/compiler/src/dotty/tools/dotc/ast/tpd.scala
index 073cf19a2411..8b6fcfe03dad 100644
--- a/compiler/src/dotty/tools/dotc/ast/tpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/tpd.scala
@@ -1139,7 +1139,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
   }
 
   /** Let bind `tree` unless `tree` is at least idempotent */
-  def letBind(tree: Tree)(within: Tree => Tree)(implicit ctx: Context): Tree =
+  def evalOnce(tree: Tree)(within: Tree => Tree)(implicit ctx: Context): Tree =
     letBindUnless(TreeInfo.Idempotent, tree)(within)
 
   def runtimeCall(name: TermName, args: List[Tree])(implicit ctx: Context): Tree = {
diff --git a/compiler/src/dotty/tools/dotc/transform/Erasure.scala b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
index 965cc8e33fb0..2fd68a391c43 100644
--- a/compiler/src/dotty/tools/dotc/transform/Erasure.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
@@ -221,7 +221,7 @@ object Erasure {
               val nullTree = Literal(Constant(null))
               val unboxedNull = adaptToType(nullTree, underlying)
 
-              letBind(tree) { t =>
+              evalOnce(tree) { t =>
                 If(t.select(defn.Object_eq).appliedTo(nullTree),
                   unboxedNull,
                   unboxedTree(t))
diff --git a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
index b7061012aba5..0183065650b6 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
@@ -265,12 +265,12 @@ object TypeTestsCasts {
           case _: SingletonType =>
             expr.isInstance(testType).withSpan(tree.span)
           case OrType(tp1, tp2) =>
-            letBind(expr) { e =>
+            evalOnce(expr) { e =>
               transformTypeTest(e, tp1, flagUnrelated = false)
                 .or(transformTypeTest(e, tp2, flagUnrelated = false))
             }
           case AndType(tp1, tp2) =>
-            letBind(expr) { e =>
+            evalOnce(expr) { e =>
               transformTypeTest(e, tp1, flagUnrelated)
                 .and(transformTypeTest(e, tp2, flagUnrelated))
             }
@@ -278,7 +278,7 @@ object TypeTestsCasts {
             def isArrayTest(arg: Tree) =
               ref(defn.runtimeMethodRef(nme.isArray)).appliedTo(arg, Literal(Constant(ndims)))
             if (ndims == 1) isArrayTest(expr)
-            else letBind(expr) { e =>
+            else evalOnce(expr) { e =>
               derivedTree(e, defn.Any_isInstanceOf, e.tpe)
                 .and(isArrayTest(e))
             }
diff --git a/compiler/src/dotty/tools/dotc/transform/VCInlineMethods.scala b/compiler/src/dotty/tools/dotc/transform/VCInlineMethods.scala
index d3e26a4e1cf2..7f5097fd5d27 100644
--- a/compiler/src/dotty/tools/dotc/transform/VCInlineMethods.scala
+++ b/compiler/src/dotty/tools/dotc/transform/VCInlineMethods.scala
@@ -68,7 +68,7 @@ class VCInlineMethods extends MiniPhase with IdentityDenotTransformer {
         val extensionMeth = extensionMethod(origMeth)
 
         if (!ctParams.isEmpty) {
-          letBind(qual) { ev =>
+          evalOnce(qual) { ev =>
             val ctArgs = ctParams.map(tparam =>
               TypeTree(tparam.typeRef.asSeenFrom(ev.tpe, origCls)))
             ref(extensionMeth)

From 8827eff59fd82a2b1d4af522434d39e441d419bc Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Wed, 6 Mar 2019 11:01:22 +0100
Subject: [PATCH 16/20] Revert "Flag ChildrenQueried in hasAnonymousChild"

This reverts commit bb1515eb6514eaf2277e9dbe872fc0a07bc4d914.
---
 compiler/src/dotty/tools/dotc/transform/SymUtils.scala | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/SymUtils.scala b/compiler/src/dotty/tools/dotc/transform/SymUtils.scala
index 02f530494041..355bef8f1268 100644
--- a/compiler/src/dotty/tools/dotc/transform/SymUtils.scala
+++ b/compiler/src/dotty/tools/dotc/transform/SymUtils.scala
@@ -145,11 +145,8 @@ class SymUtils(val self: Symbol) extends AnyVal {
     }.reverse
   }
 
-  def hasAnonymousChild(implicit ctx: Context): Boolean = {
-    if (self.isType)
-      self.setFlag(ChildrenQueried)
+  def hasAnonymousChild(implicit ctx: Context): Boolean =
     children.exists(_ `eq` self)
-  }
 
   /** Is symbol directly or indirectly owned by a term symbol? */
   @tailrec final def isLocal(implicit ctx: Context): Boolean = {

From ffa8acf65d446b0149df92ca652490b3587923aa Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Wed, 6 Mar 2019 11:31:37 +0100
Subject: [PATCH 17/20] Address review

---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 23 ++++++++-----------
 tests/neg/matchtype-seq.scala                 | 20 ++++++++++++++++
 2 files changed, 30 insertions(+), 13 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 8323ee7d04c1..b72442cf1561 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1891,10 +1891,10 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
   def intersecting(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = {
     // println(s"intersecting(${tp1.show}, ${tp2.show})")
     /** Can we enumerate all instantiations of this type? */
-    def isClosed(tp: Symbol): Boolean =
+    def isClosedSum(tp: Symbol): Boolean =
       tp.is(Sealed) && tp.is(AbstractOrTrait) && !tp.hasAnonymousChild
 
-    /** Splits a close type into a disjunction of smaller types.
+    /** Splits a closed type into a disjunction of smaller types.
      *  It should hold that `tp` and `decompose(tp).reduce(_ or _)`
      *  denote the same set of values.
      */
@@ -1919,19 +1919,19 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
             // subtype, so they must be unrelated by single inheritance
             // of classes.
             false
-          else if (isClosed(cls1))
+          else if (isClosedSum(cls1))
             decompose(cls1, tp1).exists(x => intersecting(x, tp2))
-          else if (isClosed(cls2))
+          else if (isClosedSum(cls2))
             decompose(cls2, tp2).exists(x => intersecting(x, tp1))
           else
             true
         }
       case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 =>
-        // Unboxed x.zip(y).zip(z).forall { case ((a, b), c) => f(a, b, c) }
-        def zip_zip_forall[A, B, C](x: List[A], y: List[B], z: List[C])(f: (A, B, C) => Boolean): Boolean =
-          x match {
-            case x :: xs => y match {
-              case y :: ys => z match {
+        // Unboxed xs.zip(ys).zip(zs).forall { case ((a, b), c) => f(a, b, c) }
+        def zip_zip_forall[A, B, C](xs: List[A], ys: List[B], zs: List[C])(f: (A, B, C) => Boolean): Boolean =
+          xs match {
+            case x :: xs => ys match {
+              case y :: ys => zs match {
                 case z :: zs => f(x, y, z) && zip_zip_forall(xs, ys, zs)(f)
                 case _ => true
               }
@@ -1943,9 +1943,6 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
           zip_zip_forall(args1, args2, tycon1.typeParams) {
             (arg1, arg2, tparam) =>
               val v = tparam.paramVariance
-              // Note that the logic below is conservative in that is
-              // assumes that Covariant type parameters are Contravariant
-              // type
               if (v > 0)
                 intersecting(arg1, arg2) || {
                   // We still need to proof that `Nothing` is not a valid
@@ -1979,7 +1976,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
                     override def apply(x: Boolean, t: Type) =
                       x && {
                         t match {
-                          case tp: TypeRef if tp.symbol.is(TypeParam) => false
+                          case tp: TypeRef if tp.symbol.isAbstractOrParamType => false
                           case _: SkolemType | _: TypeVar | _: TypeParamRef => false
                           case _ => foldOver(x, t)
                         }
diff --git a/tests/neg/matchtype-seq.scala b/tests/neg/matchtype-seq.scala
index d899b3964712..fed785703fd2 100644
--- a/tests/neg/matchtype-seq.scala
+++ b/tests/neg/matchtype-seq.scala
@@ -169,3 +169,23 @@ object Test3 {
     ()
   }
 }
+
+object Test4 {
+  trait Inv[T]
+
+  type M[A] = A match {
+    case Inv[Int] => String
+    case _ => Int
+  }
+
+  class Foo {
+    type A
+
+    def test: Unit = {
+      // We need to be careful here, we cannot trust the output of type
+      // comparer on `isSameType(A, Int)` since `A` is an abstract type.
+      val a: M[Inv[A]] = 1 // error
+      ()
+    }
+  }
+}

From e7f6049fdf69a4e98ccaff96c92ebeea83a98b99 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Wed, 6 Mar 2019 11:39:26 +0100
Subject: [PATCH 18/20] Move refineUsingParent to TypeOps

---
 .../dotty/tools/dotc/core/TypeComparer.scala  |   2 +-
 .../src/dotty/tools/dotc/core/TypeOps.scala   | 153 ++++++++++++++++++
 .../tools/dotc/transform/TypeUtils.scala      |   3 +-
 .../tools/dotc/transform/patmat/Space.scala   |   2 +-
 .../src/dotty/tools/dotc/typer/Typer.scala    | 148 -----------------
 5 files changed, 157 insertions(+), 151 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index b72442cf1561..32b9cdae1f5e 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1899,7 +1899,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
      *  denote the same set of values.
      */
     def decompose(sym: Symbol, tp: Type): List[Type] =
-      sym.children.map(x => ctx.typer.refineUsingParent(tp, x)).filter(_.exists)
+      sym.children.map(x => ctx.refineUsingParent(tp, x)).filter(_.exists)
 
     (tp1.dealias, tp2.dealias) match {
       case (tp1: ConstantType, tp2: ConstantType) =>
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index 717452cc3a9e..6ba033df4bdf 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -13,6 +13,11 @@ import collection.mutable
 import ast.tpd._
 import reporting.trace
 import reporting.diagnostic.Message
+import config.Printers.{gadts, typr}
+import typer.Applications._
+import typer.ProtoTypes._
+import typer.ForceDegree
+import typer.Inferencing.isFullyDefined
 
 import scala.annotation.internal.sharable
 
@@ -334,6 +339,154 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
    *  This test is used when we are too early in the pipeline to consider imports.
    */
   def scala2Setting = ctx.settings.language.value.contains(nme.Scala2.toString)
+
+  /** Refine child based on parent
+   *
+   *  In child class definition, we have:
+   *
+   *      class Child[Ts] extends path.Parent[Us] with Es
+   *      object Child extends path.Parent[Us] with Es
+   *      val child = new path.Parent[Us] with Es           // enum values
+   *
+   *  Given a parent type `parent` and a child symbol `child`, we infer the prefix
+   *  and type parameters for the child:
+   *
+   *      prefix.child[Vs] <:< parent
+   *
+   *  where `Vs` are fresh type variables and `prefix` is the symbol prefix with all
+   *  non-module and non-package `ThisType` replaced by fresh type variables.
+   *
+   *  If the subtyping is true, the instantiated type `p.child[Vs]` is
+   *  returned. Otherwise, `NoType` is returned.
+   */
+  def refineUsingParent(parent: Type, child: Symbol)(implicit ctx: Context): Type = {
+    if (child.isTerm && child.is(Case, butNot = Module)) return child.termRef // enum vals always match
+
+    // <local child> is a place holder from Scalac, it is hopeless to instantiate it.
+    //
+    // Quote from scalac (from nsc/symtab/classfile/Pickler.scala):
+    //
+    //     ...When a sealed class/trait has local subclasses, a single
+    //     <local child> class symbol is added as pickled child
+    //     (instead of a reference to the anonymous class; that was done
+    //     initially, but seems not to work, ...).
+    //
+    if (child.name == tpnme.LOCAL_CHILD) return child.typeRef
+
+    val childTp = if (child.isTerm) child.termRef else child.typeRef
+
+    instantiate(childTp, parent)(ctx.fresh.setNewTyperState()).dealias
+  }
+
+  /** Instantiate type `tp1` to be a subtype of `tp2`
+   *
+   *  Return the instantiated type if type parameters and this type
+   *  in `tp1` can be instantiated such that `tp1 <:< tp2`.
+   *
+   *  Otherwise, return NoType.
+   */
+  private def instantiate(tp1: NamedType, tp2: Type)(implicit ctx: Context): Type = {
+    /** expose abstract type references to their bounds or tvars according to variance */
+    class AbstractTypeMap(maximize: Boolean)(implicit ctx: Context) extends TypeMap {
+      def expose(lo: Type, hi: Type): Type =
+        if (variance == 0)
+          newTypeVar(TypeBounds(lo, hi))
+        else if (variance == 1)
+          if (maximize) hi else lo
+        else
+          if (maximize) lo else hi
+
+      def apply(tp: Type): Type = tp match {
+        case tp: TypeRef if isBounds(tp.underlying) =>
+          val lo = this(tp.info.loBound)
+          val hi = this(tp.info.hiBound)
+          // See tests/patmat/gadt.scala  tests/patmat/exhausting.scala  tests/patmat/t9657.scala
+          val exposed = expose(lo, hi)
+          typr.println(s"$tp exposed to =====> $exposed")
+          exposed
+
+        case AppliedType(tycon: TypeRef, args) if isBounds(tycon.underlying) =>
+          val args2 = args.map(this)
+          val lo = this(tycon.info.loBound).applyIfParameterized(args2)
+          val hi = this(tycon.info.hiBound).applyIfParameterized(args2)
+          val exposed = expose(lo, hi)
+          typr.println(s"$tp exposed to =====> $exposed")
+          exposed
+
+        case _ =>
+          mapOver(tp)
+      }
+    }
+
+    def minTypeMap(implicit ctx: Context) = new AbstractTypeMap(maximize = false)
+    def maxTypeMap(implicit ctx: Context) = new AbstractTypeMap(maximize = true)
+
+    // Fix subtype checking for child instantiation,
+    // such that `Foo(Test.this.foo) <:< Foo(Foo.this)`
+    // See tests/patmat/i3938.scala
+    class RemoveThisMap extends TypeMap {
+      var prefixTVar: Type = null
+      def apply(tp: Type): Type = tp match {
+        case ThisType(tref: TypeRef) if !tref.symbol.isStaticOwner =>
+          if (tref.symbol.is(Module))
+            TermRef(this(tref.prefix), tref.symbol.sourceModule)
+          else if (prefixTVar != null)
+            this(tref)
+          else {
+            prefixTVar = WildcardType  // prevent recursive call from assigning it
+            prefixTVar = newTypeVar(TypeBounds.upper(this(tref)))
+            prefixTVar
+          }
+        case tp => mapOver(tp)
+      }
+    }
+
+    // replace uninstantiated type vars with WildcardType, check tests/patmat/3333.scala
+    def instUndetMap(implicit ctx: Context) = new TypeMap {
+      def apply(t: Type): Type = t match {
+        case tvar: TypeVar if !tvar.isInstantiated => WildcardType(tvar.origin.underlying.bounds)
+        case _ => mapOver(t)
+      }
+    }
+
+    val removeThisType = new RemoveThisMap
+    val tvars = tp1.typeParams.map { tparam => newTypeVar(tparam.paramInfo.bounds) }
+    val protoTp1 = removeThisType.apply(tp1).appliedTo(tvars)
+
+    val force = new ForceDegree.Value(
+      tvar =>
+        !(ctx.typerState.constraint.entry(tvar.origin) `eq` tvar.origin.underlying) ||
+        (tvar `eq` removeThisType.prefixTVar),
+      minimizeAll = false,
+      allowBottom = false
+    )
+
+    // If parent contains a reference to an abstract type, then we should
+    // refine subtype checking to eliminate abstract types according to
+    // variance. As this logic is only needed in exhaustivity check,
+    // we manually patch subtyping check instead of changing TypeComparer.
+    // See tests/patmat/i3645b.scala
+    def parentQualify = tp1.widen.classSymbol.info.parents.exists { parent =>
+      implicit val ictx = ctx.fresh.setNewTyperState()
+      parent.argInfos.nonEmpty && minTypeMap.apply(parent) <:< maxTypeMap.apply(tp2)
+    }
+
+    if (protoTp1 <:< tp2) {
+      if (isFullyDefined(protoTp1, force)) protoTp1
+      else instUndetMap.apply(protoTp1)
+    }
+    else {
+      val protoTp2 = maxTypeMap.apply(tp2)
+      if (protoTp1 <:< protoTp2 || parentQualify) {
+        if (isFullyDefined(AndType(protoTp1, protoTp2), force)) protoTp1
+        else instUndetMap.apply(protoTp1)
+      }
+      else {
+        typr.println(s"$protoTp1 <:< $protoTp2 = false")
+        NoType
+      }
+    }
+  }
 }
 
 object TypeOps {
diff --git a/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala b/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala
index 4239b8248c10..839fa32892fb 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala
@@ -1,4 +1,5 @@
-package dotty.tools.dotc
+package dotty.tools
+package dotc
 package transform
 
 import core._
diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index ece0d995933b..6024e3e6d961 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -467,7 +467,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       case tp =>
         val parts = children.map { sym =>
           val sym1 = if (sym.is(ModuleClass)) sym.sourceModule else sym
-          val refined = ctx.typer.refineUsingParent(tp, sym1)
+          val refined = ctx.refineUsingParent(tp, sym1)
           val inhabited = new TypeAccumulator[Boolean] {
             override def apply(x: Boolean, tp: Type) = x && {
               tp match {
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 994c139ef79f..d3664fab5270 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -2929,152 +2929,4 @@ class Typer extends Namer
         !tree.tpe.isRef(defn.UnitClass) && !isSelfOrSuperConstrCall(tree))
       ctx.warning(PureExpressionInStatementPosition(original, exprOwner), original.sourcePos)
   }
-
-  /** Refine child based on parent
-   *
-   *  In child class definition, we have:
-   *
-   *      class Child[Ts] extends path.Parent[Us] with Es
-   *      object Child extends path.Parent[Us] with Es
-   *      val child = new path.Parent[Us] with Es           // enum values
-   *
-   *  Given a parent type `parent` and a child symbol `child`, we infer the prefix
-   *  and type parameters for the child:
-   *
-   *      prefix.child[Vs] <:< parent
-   *
-   *  where `Vs` are fresh type variables and `prefix` is the symbol prefix with all
-   *  non-module and non-package `ThisType` replaced by fresh type variables.
-   *
-   *  If the subtyping is true, the instantiated type `p.child[Vs]` is
-   *  returned. Otherwise, `NoType` is returned.
-   */
-  def refineUsingParent(parent: Type, child: Symbol)(implicit ctx: Context): Type = {
-    if (child.isTerm && child.is(Case, butNot = Module)) return child.termRef // enum vals always match
-
-    // <local child> is a place holder from Scalac, it is hopeless to instantiate it.
-    //
-    // Quote from scalac (from nsc/symtab/classfile/Pickler.scala):
-    //
-    //     ...When a sealed class/trait has local subclasses, a single
-    //     <local child> class symbol is added as pickled child
-    //     (instead of a reference to the anonymous class; that was done
-    //     initially, but seems not to work, ...).
-    //
-    if (child.name == tpnme.LOCAL_CHILD) return child.typeRef
-
-    val childTp = if (child.isTerm) child.termRef else child.typeRef
-
-    instantiate(childTp, parent)(ctx.fresh.setNewTyperState()).dealias
-  }
-
-  /** Instantiate type `tp1` to be a subtype of `tp2`
-   *
-   *  Return the instantiated type if type parameters and this type
-   *  in `tp1` can be instantiated such that `tp1 <:< tp2`.
-   *
-   *  Otherwise, return NoType.
-   */
-  private def instantiate(tp1: NamedType, tp2: Type)(implicit ctx: Context): Type = {
-    /** expose abstract type references to their bounds or tvars according to variance */
-    class AbstractTypeMap(maximize: Boolean)(implicit ctx: Context) extends TypeMap {
-      def expose(lo: Type, hi: Type): Type =
-        if (variance == 0)
-          newTypeVar(TypeBounds(lo, hi))
-        else if (variance == 1)
-          if (maximize) hi else lo
-        else
-          if (maximize) lo else hi
-
-      def apply(tp: Type): Type = tp match {
-        case tp: TypeRef if isBounds(tp.underlying) =>
-          val lo = this(tp.info.loBound)
-          val hi = this(tp.info.hiBound)
-          // See tests/patmat/gadt.scala  tests/patmat/exhausting.scala  tests/patmat/t9657.scala
-          val exposed = expose(lo, hi)
-          typr.println(s"$tp exposed to =====> $exposed")
-          exposed
-
-        case AppliedType(tycon: TypeRef, args) if isBounds(tycon.underlying) =>
-          val args2 = args.map(this)
-          val lo = this(tycon.info.loBound).applyIfParameterized(args2)
-          val hi = this(tycon.info.hiBound).applyIfParameterized(args2)
-          val exposed = expose(lo, hi)
-          typr.println(s"$tp exposed to =====> $exposed")
-          exposed
-
-        case _ =>
-          mapOver(tp)
-      }
-    }
-
-    def minTypeMap(implicit ctx: Context) = new AbstractTypeMap(maximize = false)
-    def maxTypeMap(implicit ctx: Context) = new AbstractTypeMap(maximize = true)
-
-    // Fix subtype checking for child instantiation,
-    // such that `Foo(Test.this.foo) <:< Foo(Foo.this)`
-    // See tests/patmat/i3938.scala
-    class RemoveThisMap extends TypeMap {
-      var prefixTVar: Type = null
-      def apply(tp: Type): Type = tp match {
-        case ThisType(tref: TypeRef) if !tref.symbol.isStaticOwner =>
-          if (tref.symbol.is(Module))
-            TermRef(this(tref.prefix), tref.symbol.sourceModule)
-          else if (prefixTVar != null)
-            this(tref)
-          else {
-            prefixTVar = WildcardType  // prevent recursive call from assigning it
-            prefixTVar = newTypeVar(TypeBounds.upper(this(tref)))
-            prefixTVar
-          }
-        case tp => mapOver(tp)
-      }
-    }
-
-    // replace uninstantiated type vars with WildcardType, check tests/patmat/3333.scala
-    def instUndetMap(implicit ctx: Context) = new TypeMap {
-      def apply(t: Type): Type = t match {
-        case tvar: TypeVar if !tvar.isInstantiated => WildcardType(tvar.origin.underlying.bounds)
-        case _ => mapOver(t)
-      }
-    }
-
-    val removeThisType = new RemoveThisMap
-    val tvars = tp1.typeParams.map { tparam => newTypeVar(tparam.paramInfo.bounds) }
-    val protoTp1 = removeThisType.apply(tp1).appliedTo(tvars)
-
-    val force = new ForceDegree.Value(
-      tvar =>
-        !(ctx.typerState.constraint.entry(tvar.origin) `eq` tvar.origin.underlying) ||
-        (tvar `eq` removeThisType.prefixTVar),
-      minimizeAll = false,
-      allowBottom = false
-    )
-
-    // If parent contains a reference to an abstract type, then we should
-    // refine subtype checking to eliminate abstract types according to
-    // variance. As this logic is only needed in exhaustivity check,
-    // we manually patch subtyping check instead of changing TypeComparer.
-    // See tests/patmat/i3645b.scala
-    def parentQualify = tp1.widen.classSymbol.info.parents.exists { parent =>
-      implicit val ictx = ctx.fresh.setNewTyperState()
-      parent.argInfos.nonEmpty && minTypeMap.apply(parent) <:< maxTypeMap.apply(tp2)
-    }
-
-    if (protoTp1 <:< tp2) {
-      if (isFullyDefined(protoTp1, force)) protoTp1
-      else instUndetMap.apply(protoTp1)
-    }
-    else {
-      val protoTp2 = maxTypeMap.apply(tp2)
-      if (protoTp1 <:< protoTp2 || parentQualify) {
-        if (isFullyDefined(AndType(protoTp1, protoTp2), force)) protoTp1
-        else instUndetMap.apply(protoTp1)
-      }
-      else {
-        typr.println(s"$protoTp1 <:< $protoTp2 = false")
-        NoType
-      }
-    }
-  }
 }

From f4df58d05f7f7ae33ba4b62c54ce4d0d84446fd4 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Wed, 6 Mar 2019 13:32:08 +0100
Subject: [PATCH 19/20] Factor out cov. test and use it in the inv. case

---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 92 ++++++++++---------
 1 file changed, 48 insertions(+), 44 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 32b9cdae1f5e..8465bdd80e1c 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1928,7 +1928,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
         }
       case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 =>
         // Unboxed xs.zip(ys).zip(zs).forall { case ((a, b), c) => f(a, b, c) }
-        def zip_zip_forall[A, B, C](xs: List[A], ys: List[B], zs: List[C])(f: (A, B, C) => Boolean): Boolean =
+        def zip_zip_forall[A, B, C](xs: List[A], ys: List[B], zs: List[C])(f: (A, B, C) => Boolean): Boolean = {
           xs match {
             case x :: xs => ys match {
               case y :: ys => zs match {
@@ -1939,52 +1939,56 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
             }
             case _ => true
           }
+        }
+        def covariantIntersecting(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = {
+          intersecting(tp1, tp2) || {
+            // We still need to proof that `Nothing` is not a valid
+            // instantiation of this type parameter. We have two ways
+            // to get to that conclusion:
+            // 1. `Nothing` does not conform to the type parameter's lb
+            // 2. `tycon1` has a field typed with this type parameter.
+            //
+            // Because of separate compilation, the use of 2. is
+            // limited to case classes.
+            import dotty.tools.dotc.typer.Applications.productSelectorTypes
+            val lowerBoundedByNothing = tparam.paramInfo.bounds.lo eq NothingType
+            val typeUsedAsField =
+              productSelectorTypes(tycon1, null).exists {
+                case tp: TypeRef =>
+                  (tp.designator: Any) == tparam // Bingo!
+                case _ =>
+                  false
+              }
+            lowerBoundedByNothing && !typeUsedAsField
+          }
+        }
 
-          zip_zip_forall(args1, args2, tycon1.typeParams) {
-            (arg1, arg2, tparam) =>
-              val v = tparam.paramVariance
-              if (v > 0)
-                intersecting(arg1, arg2) || {
-                  // We still need to proof that `Nothing` is not a valid
-                  // instantiation of this type parameter. We have two ways
-                  // to get to that conclusion:
-                  // 1. `Nothing` does not conform to the type parameter's lb
-                  // 2. `tycon1` has a field typed with this type parameter.
-                  //
-                  // Because of separate compilation, the use of 2. is
-                  // limited to case classes.
-                  import dotty.tools.dotc.typer.Applications.productSelectorTypes
-                  val lowerBoundedByNothing = tparam.paramInfo.bounds.lo eq NothingType
-                  val typeUsedAsField =
-                    productSelectorTypes(tycon1, null).exists {
-                      case tp: TypeRef =>
-                        (tp.designator: Any) == tparam // Bingo!
-                      case _ =>
-                        false
-                    }
-                  lowerBoundedByNothing && !typeUsedAsField
-                }
-              else if (v < 0)
-                // Contravariant case: a value where this type parameter is
-                // instantiated to `Any` belongs to both types.
-                true
-              else
-                isSameType(arg1, arg2) || {
-                  // We can only trust a "no" from `isSameType` when both
-                  // `arg1` and `arg2` are fully instantiated.
-                  val fullyInstantiated = new TypeAccumulator[Boolean] {
-                    override def apply(x: Boolean, t: Type) =
-                      x && {
-                        t match {
-                          case tp: TypeRef if tp.symbol.isAbstractOrParamType => false
-                          case _: SkolemType | _: TypeVar | _: TypeParamRef => false
-                          case _ => foldOver(x, t)
-                        }
+        zip_zip_forall(args1, args2, tycon1.typeParams) {
+          (arg1, arg2, tparam) =>
+            val v = tparam.paramVariance
+            if (v > 0)
+              covariantIntersecting(arg1, arg2, tparam)
+            else if (v < 0)
+              // Contravariant case: a value where this type parameter is
+              // instantiated to `Any` belongs to both types.
+              true
+            else
+              covariantIntersecting(arg1, arg2, tparam) && (isSameType(arg1, arg2) || {
+                // We can only trust a "no" from `isSameType` when both
+                // `arg1` and `arg2` are fully instantiated.
+                val fullyInstantiated = new TypeAccumulator[Boolean] {
+                  override def apply(x: Boolean, t: Type) =
+                    x && {
+                      t match {
+                        case tp: TypeRef if tp.symbol.isAbstractOrParamType => false
+                        case _: SkolemType | _: TypeVar | _: TypeParamRef => false
+                        case _ => foldOver(x, t)
                       }
-                  }
-                  !(fullyInstantiated.apply(true, arg1) &&
-                    fullyInstantiated.apply(true, arg2))
+                    }
                 }
+                !(fullyInstantiated.apply(true, arg1) &&
+                  fullyInstantiated.apply(true, arg2))
+              })
         }
       case (tp1: HKLambda, tp2: HKLambda) =>
         intersecting(tp1.resType, tp2.resType)

From ea04343f99a912cd94e2afd3106cd0c85e2c6cc1 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Wed, 6 Mar 2019 14:52:41 +0100
Subject: [PATCH 20/20] Update inhabited check in Space

To be more conservative during the traversal. As pointed out in the
review "nested non-inhabitable intersection type does not necessarily
mean the outer type is non-inhabited".
---
 .../tools/dotc/transform/patmat/Space.scala   | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index 6024e3e6d961..0341f66e6b85 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -468,16 +468,17 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
         val parts = children.map { sym =>
           val sym1 = if (sym.is(ModuleClass)) sym.sourceModule else sym
           val refined = ctx.refineUsingParent(tp, sym1)
-          val inhabited = new TypeAccumulator[Boolean] {
-            override def apply(x: Boolean, tp: Type) = x && {
-              tp match {
-                case AndType(tp1, tp2) => ctx.typeComparer.intersecting(tp1, tp2)
-                case OrType(tp1, tp2) => foldOver(x, tp1) || foldOver(x, tp2)
-                case _ => foldOver(x, tp)
-              }
+
+          def inhabited(tp: Type): Boolean =
+            tp.dealias match {
+              case AndType(tp1, tp2) => ctx.typeComparer.intersecting(tp1, tp2)
+              case OrType(tp1, tp2) => inhabited(tp1) || inhabited(tp2)
+              case tp: RefinedType => inhabited(tp.parent)
+              case tp: TypeRef => inhabited(tp.prefix)
+              case _ => true
             }
-          }
-          if (inhabited.apply(true, refined)) refined
+
+          if (inhabited(refined)) refined
           else NoType
         } filter(_.exists)