diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 71e032ffb7eb..8465bdd80e1c 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
@@ -528,7 +529,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 +762,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 +816,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 +875,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 +928,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 +974,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 +1032,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).
@@ -1875,6 +1876,145 @@ 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 isClosedSum(tp: Symbol): Boolean =
+      tp.is(Sealed) && tp.is(AbstractOrTrait) && !tp.hasAnonymousChild
+
+    /** 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.
+     */
+    def decompose(sym: Symbol, tp: Type): List[Type] =
+      sym.children.map(x => ctx.refineUsingParent(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 =>
+        val cls1 = tp1.classSymbol
+        val cls2 = tp2.classSymbol
+        if (cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1)) {
+          true
+        } else {
+          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 (isClosedSum(cls1))
+            decompose(cls1, tp1).exists(x => intersecting(x, tp2))
+          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 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
+              }
+              case _ => true
+            }
+            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)
+              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))
+              })
+        }
+      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 +2109,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 +2128,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
+          }
+          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
           }
-        else NoType
+        }
       }
+      finally constraint = saved
     }
-    finally constraint = saved
+    result
   }
 }
 
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/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index e4490aa3c599..acf2b3f33461 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
 
@@ -3764,42 +3764,9 @@ 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
-
     def reduced(implicit ctx: Context): Type = {
       val trackingCtx = ctx.fresh.setTypeComparerFn(new TrackingTypeComparer(_))
-      val cmp = 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)
-          if (r.exists) r
-          else if (cantPossiblyMatch(cas)) reduceSequential(cases1)
-          else NoType
-      }
-
-      def reduceParallel(implicit ctx: Context) = {
-        val applicableBranches = cases
-          .map(cmp.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)
-      }
+      val typeComparer = trackingCtx.typeComparer.asInstanceOf[TrackingTypeComparer]
 
       def contextInfo(tp: Type): Type = tp match {
         case tp: TypeParamRef =>
@@ -3813,28 +3780,27 @@ object Types {
           tp.underlying
       }
 
-      def updateReductionContext() = {
+      def updateReductionContext(): Unit = {
         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 =
+      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)
+              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/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
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 3b184b6bb9fd..0341f66e6b85 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 */
@@ -468,10 +466,20 @@ 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
+          val refined = ctx.refineUsingParent(tp, sym1)
+
+          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(refined)) refined
+          else NoType
         } filter(_.exists)
 
         debug.println(s"${tp.show} decomposes to [${parts.map(_.show).mkString(", ")}]")
@@ -480,250 +488,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
-
-    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
-  }
-
-  /** 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
@@ -983,7 +747,6 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
               ctx.warning(MatchCaseOnlyNullWarning(), pat.sourcePos)
             case _ =>
           }
-
         }
       }
     }
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..fed785703fd2
--- /dev/null
+++ b/tests/neg/matchtype-seq.scala
@@ -0,0 +1,191 @@
+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
+}
+
+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
+}
+
+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
+    ()
+  }
+}
+
+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
+      ()
+    }
+  }
+}
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)