diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index 267deb1f75a7..663a5c37cf4a 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -599,37 +599,70 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
    *
    */
   def instantiate(tp1: Type, tp2: Type)(implicit ctx: Context): Type = {
-    // map `ThisType` of `tp1` to a type variable
-    // precondition: `tp1` should have the shape `path.Child`, thus `ThisType` is always covariant
-    val thisTypeMap = new TypeMap {
-      def apply(t: Type): Type = t match {
-        case tp @ ThisType(tref) if !tref.symbol.isStaticOwner  =>
-          if (tref.symbol.is(Module)) mapOver(tref)
-          else newTypeVar(TypeBounds.upper(tp.underlying))
-        case _ =>
-          mapOver(t)
+    // expose abstract type references to their bounds or tvars according to variance
+    abstract class AbstractTypeMap(maximize: Boolean)(implicit ctx: Context) extends TypeMap {
+      def expose(tp: TypeRef): Type = {
+        val lo = this(tp.info.loBound)
+        val hi = this(tp.info.hiBound)
+        val exposed =
+          if (variance == 0)
+            newTypeVar(TypeBounds(lo, hi))
+          else if (variance == 1)
+            if (maximize) hi else lo
+          else
+            if (maximize) lo else hi
+
+        debug.println(s"$tp exposed to =====> $exposed")
+        exposed
       }
-    }
 
-    // replace type parameter references with bounds
-    val typeParamMap = new TypeMap {
-      def apply(t: Type): Type = t match {
-        case tp: TypeRef if tp.symbol.is(TypeParam) && tp.underlying.isInstanceOf[TypeBounds] =>
+      override def mapOver(tp: Type): Type = tp match {
+        case tp: TypeRef if tp.underlying.isInstanceOf[TypeBounds] =>
           // See tests/patmat/gadt.scala  tests/patmat/exhausting.scala  tests/patmat/t9657.scala
+          expose(tp)
+
+        case AppliedType(tycon: TypeRef, args) if tycon.underlying.isInstanceOf[TypeBounds] =>
+          val args2 = args.map(this)
+          val lo = this(tycon.info.loBound).applyIfParameterized(args2)
+          val hi = this(tycon.info.hiBound).applyIfParameterized(args2)
           val exposed =
-            if (variance == 0) newTypeVar(tp.underlying.bounds)
-            else if (variance == 1) mapOver(tp.underlying.hiBound)
-            else mapOver(tp.underlying.loBound)
+            if (variance == 0)
+              newTypeVar(TypeBounds(lo, hi))
+            else if (variance == 1)
+              if (maximize) hi else lo
+            else
+              if (maximize) lo else hi
 
           debug.println(s"$tp exposed to =====> $exposed")
           exposed
+
         case _ =>
-          mapOver(t)
+          super.mapOver(tp)
       }
     }
 
+    // We are checking the possibility of `tp1 <:< tp2`, thus we should
+    // minimize `tp1` while maximizing `tp2`. See tests/patmat/3645b.scala
+    def childTypeMap(implicit ctx: Context) = new AbstractTypeMap(maximize = false) {
+      def apply(t: Type): Type = t.dealias match {
+        // map `ThisType` of `tp1` to a type variable
+        // precondition: `tp1` should have the same shape as `path.Child`, thus `ThisType` is always covariant
+        case tp @ ThisType(tref) if !tref.symbol.isStaticOwner  =>
+          if (tref.symbol.is(Module)) this(tref)
+          else newTypeVar(TypeBounds.upper(tp.underlying))
+
+        case tp =>
+          mapOver(tp)
+      }
+    }
+
+    // replace type parameter references with bounds
+    def parentTypeMap(implicit ctx: Context) = new AbstractTypeMap(maximize = true) {
+      def apply(tp: Type): Type = mapOver(tp.dealias)
+    }
+
     // replace uninstantiated type vars with WildcardType, check tests/patmat/3333.scala
-    val instUndetMap = new TypeMap {
+    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)
@@ -642,17 +675,27 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     )
 
     val tvars = tp1.typeParams.map { tparam => newTypeVar(tparam.paramInfo.bounds) }
-    val protoTp1 = thisTypeMap(tp1.appliedTo(tvars))
+    val protoTp1 = childTypeMap.apply(tp1.appliedTo(tvars))
+
+    // 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/3645b.scala
+    def parentQualify = tp1.widen.classSymbol.info.parents.exists { parent =>
+      implicit val ictx = ctx.fresh.setNewTyperState()
+      parent.argInfos.nonEmpty && childTypeMap.apply(parent) <:< parentTypeMap.apply(tp2)
+    }
 
     if (protoTp1 <:< tp2) {
       if (isFullyDefined(protoTp1, force)) protoTp1
-      else instUndetMap(protoTp1)
+      else instUndetMap.apply(protoTp1)
     }
     else {
-      val protoTp2 = typeParamMap(tp2)
-      if (protoTp1 <:< protoTp2) {
+      val protoTp2 = parentTypeMap.apply(tp2)
+      if (protoTp1 <:< protoTp2 || parentQualify) {
         if (isFullyDefined(AndType(protoTp1, protoTp2), force)) protoTp1
-        else instUndetMap(protoTp1)
+        else instUndetMap.apply(protoTp1)
       }
       else {
         debug.println(s"$protoTp1 <:< $protoTp2 = false")
diff --git a/tests/patmat/i3645.check b/tests/patmat/i3645.check
new file mode 100644
index 000000000000..a338bef12dd1
--- /dev/null
+++ b/tests/patmat/i3645.check
@@ -0,0 +1 @@
+20: Pattern Match Exhaustivity: KInt
diff --git a/tests/patmat/i3645.scala b/tests/patmat/i3645.scala
new file mode 100644
index 000000000000..e009a6de2310
--- /dev/null
+++ b/tests/patmat/i3645.scala
@@ -0,0 +1,26 @@
+object App {
+  def main(args: Array[String]): Unit = {
+    trait AgeT {
+      type T
+      def subst[F[_]](fa: F[Int]): F[T]
+    }
+
+    type Age = Age.T
+
+    val Age: AgeT = new AgeT {
+      type T = Int
+      def subst[F[_]](fa: F[Int]): F[T] = fa
+    }
+
+    sealed abstract class K[A]
+    final case object KAge extends K[Age]
+    final case object KInt extends K[Int]
+
+    val kint: K[Age] = Age.subst[K](KInt)
+    def get(k: K[Age]): String = k match {
+      case KAge => "Age"
+    }
+
+    get(kint)
+  }
+}
diff --git a/tests/patmat/i3645b.check b/tests/patmat/i3645b.check
new file mode 100644
index 000000000000..3d4d48cd44aa
--- /dev/null
+++ b/tests/patmat/i3645b.check
@@ -0,0 +1 @@
+21: Pattern Match Exhaustivity: K3, K2
diff --git a/tests/patmat/i3645b.scala b/tests/patmat/i3645b.scala
new file mode 100644
index 000000000000..1f1e146ea8a0
--- /dev/null
+++ b/tests/patmat/i3645b.scala
@@ -0,0 +1,29 @@
+object App {
+  def main(args: Array[String]): Unit = {
+    trait FooT {
+      type T
+      def subst[F[_]](fa: F[T]): F[Int]
+    }
+    val Foo: FooT = new FooT {
+      type T = Int
+
+      def subst[F[_]](fa: F[T]): F[Int] = fa
+    }
+    type Foo = Foo.T
+    type Bar = Foo
+
+    sealed abstract class K[A]
+    final case object K1 extends K[Int]
+    final case object K2 extends K[Foo]
+    final case object K3 extends K[Bar]
+
+    val foo: K[Int] = Foo.subst[K](K2)
+    def get(k: K[Int]): Unit = k match {
+      case K1 => ()
+      // case K2 => ()
+      // case K3 => ()
+    }
+
+    get(foo)
+  }
+}
\ No newline at end of file
diff --git a/tests/patmat/i3645c.check b/tests/patmat/i3645c.check
new file mode 100644
index 000000000000..3d4d48cd44aa
--- /dev/null
+++ b/tests/patmat/i3645c.check
@@ -0,0 +1 @@
+21: Pattern Match Exhaustivity: K3, K2
diff --git a/tests/patmat/i3645c.scala b/tests/patmat/i3645c.scala
new file mode 100644
index 000000000000..4b3ba75989c8
--- /dev/null
+++ b/tests/patmat/i3645c.scala
@@ -0,0 +1,29 @@
+object App {
+  def main(args: Array[String]): Unit = {
+    trait FooT {
+      type T
+      def subst[F[_]](fa: F[T]): F[Int]
+    }
+    val Foo: FooT = new FooT {
+      type T = Int
+
+      def subst[F[_]](fa: F[T]): F[Int] = fa
+    }
+    type Foo = Foo.T
+    type Bar = Foo
+
+    sealed abstract class K[+A]
+    final case object K1 extends K[Int]
+    final case object K2 extends K[Foo]
+    final case object K3 extends K[Bar]
+
+    val foo: K[Int] = Foo.subst[K](K2)
+    def get(k: K[Int]): Unit = k match {
+      case K1 => ()
+      // case K2 => ()
+      // case K3 => ()
+    }
+
+    get(foo)
+  }
+}
\ No newline at end of file
diff --git a/tests/patmat/i3645d.check b/tests/patmat/i3645d.check
new file mode 100644
index 000000000000..3d4d48cd44aa
--- /dev/null
+++ b/tests/patmat/i3645d.check
@@ -0,0 +1 @@
+21: Pattern Match Exhaustivity: K3, K2
diff --git a/tests/patmat/i3645d.scala b/tests/patmat/i3645d.scala
new file mode 100644
index 000000000000..3bbe29e20545
--- /dev/null
+++ b/tests/patmat/i3645d.scala
@@ -0,0 +1,29 @@
+object App {
+  def main(args: Array[String]): Unit = {
+    trait FooT {
+      type T
+      def subst[F[_]](fa: F[T]): F[Int]
+    }
+    val Foo: FooT = new FooT {
+      type T = Int
+
+      def subst[F[_]](fa: F[T]): F[Int] = fa
+    }
+    type Foo = Foo.T
+    type Bar = Foo
+
+    sealed abstract class K[-A]
+    final case object K1 extends K[Int]
+    final case object K2 extends K[Foo]
+    final case object K3 extends K[Bar]
+
+    val foo: K[Int] = Foo.subst[K](K2)
+    def get(k: K[Int]): Unit = k match {
+      case K1 => ()
+      // case K2 => ()
+      // case K3 => ()
+    }
+
+    get(foo)
+  }
+}
\ No newline at end of file
diff --git a/tests/patmat/i3645e.check b/tests/patmat/i3645e.check
new file mode 100644
index 000000000000..14a7e9e29ab2
--- /dev/null
+++ b/tests/patmat/i3645e.check
@@ -0,0 +1 @@
+29: Pattern Match Exhaustivity: K1
diff --git a/tests/patmat/i3645e.scala b/tests/patmat/i3645e.scala
new file mode 100644
index 000000000000..7c4b13416712
--- /dev/null
+++ b/tests/patmat/i3645e.scala
@@ -0,0 +1,35 @@
+object App {
+  def main(args: Array[String]): Unit = {
+    trait ModuleSig {
+      type Upper
+
+      trait FooSig {
+        type Type <: Upper
+        def subst[F[_]](fa: F[Int]): F[Type]
+      }
+
+      val Foo: FooSig
+    }
+    val Module: ModuleSig = new ModuleSig {
+      type Upper = Int
+
+      val Foo: FooSig = new FooSig {
+        type Type = Int
+        def subst[F[_]](fa: F[Int]): F[Type] = fa
+      }
+    }
+    type Upper = Module.Upper
+    type Foo = Module.Foo.Type
+
+    sealed abstract class K[F]
+    final case object K1 extends K[Int]
+    final case object K2 extends K[Foo]
+
+    val kv: K[Foo] = Module.Foo.subst[K](K1)
+    def test(k: K[Foo]): Unit = k match {
+      case K2 => ()
+    }
+
+    test(kv)
+  }
+}
diff --git a/tests/patmat/i3645f.check b/tests/patmat/i3645f.check
new file mode 100644
index 000000000000..ee7113bc1140
--- /dev/null
+++ b/tests/patmat/i3645f.check
@@ -0,0 +1 @@
+30: Pattern Match Exhaustivity: K1
diff --git a/tests/patmat/i3645f.scala b/tests/patmat/i3645f.scala
new file mode 100644
index 000000000000..04d31aceea0f
--- /dev/null
+++ b/tests/patmat/i3645f.scala
@@ -0,0 +1,36 @@
+object App {
+  def main(args: Array[String]): Unit = {
+    trait ModuleSig {
+      type U2
+      type U1
+
+      trait FooSig {
+        type Type = (U1 & U2)
+        def subst[F[_]](fa: F[Int]): F[Type]
+      }
+
+      val Foo: FooSig
+    }
+    val Module: ModuleSig = new ModuleSig {
+      type U1 = Int
+      type U2 = Int
+
+      val Foo: FooSig = new FooSig {
+        // type Type = Int
+        def subst[F[_]](fa: F[Int]): F[Type] = fa
+      }
+    }
+    type Foo = Module.Foo.Type
+
+    sealed abstract class K[F]
+    final case object K1 extends K[Int]
+    final case object K2 extends K[Foo]
+
+    val kv: K[Foo] = Module.Foo.subst[K](K1)
+    def test(k: K[Foo]): Unit = k match {
+      case K2 => ()
+    }
+
+    test(kv)
+  }
+}
diff --git a/tests/patmat/i3645g.check b/tests/patmat/i3645g.check
new file mode 100644
index 000000000000..14a7e9e29ab2
--- /dev/null
+++ b/tests/patmat/i3645g.check
@@ -0,0 +1 @@
+29: Pattern Match Exhaustivity: K1
diff --git a/tests/patmat/i3645g.scala b/tests/patmat/i3645g.scala
new file mode 100644
index 000000000000..f1c85b5d9e8c
--- /dev/null
+++ b/tests/patmat/i3645g.scala
@@ -0,0 +1,35 @@
+object App {
+  def main(args: Array[String]): Unit = {
+    trait ModuleSig {
+      type F[_]
+      type U
+
+      trait FooSig {
+        type Type = F[U]
+        def subst[F[_]](fa: F[Int]): F[Type]
+      }
+
+      val Foo: FooSig
+    }
+    val Module: ModuleSig = new ModuleSig {
+      type F[A] = Int
+
+      val Foo: FooSig = new FooSig {
+        // type Type = Int
+        def subst[F[_]](fa: F[Int]): F[Type] = fa
+      }
+    }
+    type Foo = Module.Foo.Type
+
+    sealed abstract class K[F]
+    final case object K1 extends K[Int]
+    final case object K2 extends K[Foo]
+
+    val kv: K[Foo] = Module.Foo.subst[K](K1)
+    def test(k: K[Foo]): Unit = k match {
+      case K2 => ()
+    }
+
+    test(kv)
+  }
+}