diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index a3cfefb12d07..906642b95434 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -292,7 +292,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   private val nullType             = ConstantType(Constant(null))
   private val nullSpace            = Typ(nullType)
 
-  override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type) = {
+  override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type): Space = {
     val and = AndType(tp1, tp2)
     // Precondition: !(tp1 <:< tp2) && !(tp2 <:< tp1)
     // Then, no leaf of the and-type tree `and` is a subtype of `and`.
@@ -656,18 +656,18 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     // Fix subtype checking for child instantiation,
     // such that `Foo(Test.this.foo) <:< Foo(Foo.this)`
     // See tests/patmat/i3938.scala
-    def removeThisType(implicit ctx: Context) = new TypeMap {
-      // is in tvarBounds? Don't create new tvars if true
-      private var tvarBounds: Boolean = false
+    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 (tvarBounds)
+          else if (prefixTVar != null)
             this(tref)
           else {
-            tvarBounds = true
-            newTypeVar(TypeBounds.upper(this(tref)))
+            prefixTVar = WildcardType  // prevent recursive call from assigning it
+            prefixTVar = newTypeVar(TypeBounds.upper(this(tref)))
+            prefixTVar
           }
         case tp => mapOver(tp)
       }
@@ -681,14 +681,18 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       }
     }
 
-    val force = new ForceDegree.Value(
-      tvar => !(ctx.typerState.constraint.entry(tvar.origin) eq tvar.origin.underlying),
-      minimizeAll = false
-    )
-
+    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,
diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
index 66adb91941b1..07036a81635a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -115,7 +115,7 @@ object Inferencing {
             val minimize =
               force.minimizeAll ||
               variance >= 0 && !(
-                force == ForceDegree.noBottom &&
+                !force.allowBottom &&
                 defn.isBottomType(ctx.typeComparer.approximation(tvar.origin, fromBelow = true)))
             if (minimize) instantiate(tvar, fromBelow = true)
             else toMaximize = true
@@ -466,9 +466,9 @@ trait Inferencing { this: Typer =>
 
 /** An enumeration controlling the degree of forcing in "is-dully-defined" checks. */
 @sharable object ForceDegree {
-  class Value(val appliesTo: TypeVar => Boolean, val minimizeAll: Boolean)
+  class Value(val appliesTo: TypeVar => Boolean, val minimizeAll: Boolean, val allowBottom: Boolean = true)
   val none = new Value(_ => false, minimizeAll = false)
   val all = new Value(_ => true, minimizeAll = false)
-  val noBottom = new Value(_ => true, minimizeAll = false)
+  val noBottom = new Value(_ => true, minimizeAll = false, allowBottom = false)
 }
 
diff --git a/tests/patmat/i4880.check b/tests/patmat/i4880.check
new file mode 100644
index 000000000000..da0a6804ac08
--- /dev/null
+++ b/tests/patmat/i4880.check
@@ -0,0 +1 @@
+10: Pattern Match Exhaustivity: _: ZipArchive, _: VirtualFile, _: PlainFile
diff --git a/tests/patmat/i4880.scala b/tests/patmat/i4880.scala
new file mode 100644
index 000000000000..29c9e77d6c10
--- /dev/null
+++ b/tests/patmat/i4880.scala
@@ -0,0 +1,13 @@
+sealed abstract class AbstractFile
+class PlainFile(path: String) extends AbstractFile
+class VirtualFile(name: String) extends AbstractFile
+abstract class ZipArchive(path: String) extends AbstractFile {
+  sealed abstract class Entry(name: String) extends VirtualFile(name)
+  class DirEntry(path: String) extends Entry(path)
+}
+
+object Test {
+  def foo(file: AbstractFile) = file match {
+    case ze: ZipArchive#Entry =>
+  }
+}
diff --git a/tests/patmat/i4880a.scala b/tests/patmat/i4880a.scala
new file mode 100644
index 000000000000..edd160f1a3ce
--- /dev/null
+++ b/tests/patmat/i4880a.scala
@@ -0,0 +1,17 @@
+sealed abstract class AbstractFile
+class PlainFile(path: String) extends AbstractFile
+class VirtualFile(name: String) extends AbstractFile
+abstract class ZipArchive(path: String) extends AbstractFile {
+  sealed abstract class Entry(name: String) extends VirtualFile(name)
+  class DirEntry(path: String) extends Entry(path)
+}
+
+object Test {
+  def foo(file: AbstractFile) = file match {
+    case a: PlainFile =>
+    case b: ZipArchive =>
+    case c1: ZipArchive#Entry =>
+    case c1: ZipArchive#DirEntry =>
+    case c: VirtualFile =>
+  }
+}
diff --git a/tests/patmat/i4880b.scala b/tests/patmat/i4880b.scala
new file mode 100644
index 000000000000..a31ffb7c46f2
--- /dev/null
+++ b/tests/patmat/i4880b.scala
@@ -0,0 +1,16 @@
+sealed abstract class AbstractFile
+class PlainFile(path: String) extends AbstractFile
+class VirtualFile(name: String) extends AbstractFile
+abstract class ZipArchive(path: String) extends AbstractFile {
+  sealed abstract class Entry(name: String) extends VirtualFile(name)
+  class DirEntry(path: String) extends Entry(path)
+}
+
+object Test {
+  def foo(file: AbstractFile) = file match {
+    case a: PlainFile =>
+    case b: ZipArchive =>
+    case c1: ZipArchive#Entry =>
+    case c: VirtualFile =>
+  }
+}