diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index 81b00c4572e7..081af65a3403 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -278,21 +278,8 @@ trait SpaceLogic {
   }
 }
 
-object SpaceEngine {
-  private sealed trait Implementability {
-    def show(implicit ctx: Context) = this match {
-      case SubclassOf(classSyms) => s"SubclassOf(${classSyms.map(_.show)})"
-      case other => other.toString
-    }
-  }
-  private case object ClassOrTrait extends Implementability
-  private case class SubclassOf(classSyms: List[Symbol]) extends Implementability
-  private case object Unimplementable extends Implementability
-}
-
 /** Scala implementation of space logic */
 class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
-  import SpaceEngine._
   import tpd._
 
   private val scalaSomeClass       = ctx.requiredClass("scala.Some")
@@ -301,77 +288,15 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   private val scalaNilType         = ctx.requiredModuleRef("scala.collection.immutable.Nil")
   private val scalaConsType        = ctx.requiredClassRef("scala.collection.immutable.::")
 
-  /** Checks if it's possible to create a trait/class which is a subtype of `tp`.
-   *
-   * - doesn't handle member collisions (will not declare a type unimplementable because of one)
-   * - expects that neither Any nor Object reach it
-   *   (this is currently true due to both isSubType and and/or type simplification)
-   *
-   * See [[intersectUnrelatedAtomicTypes]].
-   */
-  private def implementability(tp: Type): Implementability = tp.dealias match {
-    case AndType(tp1, tp2) =>
-      (implementability(tp1), implementability(tp2)) match {
-        case (Unimplementable, _) | (_, Unimplementable) => Unimplementable
-        case (SubclassOf(classSyms1), SubclassOf(classSyms2)) =>
-          (for {
-            sym1 <- classSyms1
-            sym2 <- classSyms2
-            result <-
-              if (sym1 isSubClass sym2) List(sym1)
-              else if (sym2 isSubClass sym1) List(sym2)
-              else Nil
-          } yield result) match {
-            case Nil => Unimplementable
-            case lst => SubclassOf(lst)
-          }
-        case (ClassOrTrait, ClassOrTrait) => ClassOrTrait
-        case (SubclassOf(clss), _) => SubclassOf(clss)
-        case (_, SubclassOf(clss)) => SubclassOf(clss)
-      }
-    case OrType(tp1, tp2) =>
-      (implementability(tp1), implementability(tp2)) match {
-        case (ClassOrTrait, _) | (_, ClassOrTrait) => ClassOrTrait
-        case (SubclassOf(classSyms1), SubclassOf(classSyms2)) =>
-          SubclassOf(classSyms1 ::: classSyms2)
-        case (SubclassOf(classSyms), _) => SubclassOf(classSyms)
-        case (_, SubclassOf(classSyms)) => SubclassOf(classSyms)
-        case _ => Unimplementable
-      }
-    case _: SingletonType =>
-      // singleton types have no instantiable subtypes
-      Unimplementable
-    case tp: RefinedType =>
-      // refinement itself is not considered - it would at most make
-      // a type unimplementable because of a member collision
-      implementability(tp.parent)
-    case other =>
-      val classSym = other.classSymbol
-      if (classSym.exists) {
-        if (classSym is Final) Unimplementable
-        else if (classSym is Trait) ClassOrTrait
-        else SubclassOf(List(classSym))
-      } else {
-        // if no class symbol exists, conservatively say that anything
-        // can implement `tp`
-        ClassOrTrait
-      }
-  }
-
   override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type) = {
     val and = AndType(tp1, tp2)
     // Precondition: !(tp1 <:< tp2) && !(tp2 <:< tp1)
     // Then, no leaf of the and-type tree `and` is a subtype of `and`.
-    // Then, to create a value of type `and` you must instantiate a trait (class/module)
-    // which is a subtype of all the leaves of `and`.
-    val imp = implementability(and)
+    val res = inhabited(and)
 
-    debug.println(s"atomic intersection: ${and.show} ~ ${imp.show}")
+    debug.println(s"atomic intersection: ${and.show} = ${res}")
 
-    imp match {
-      case Unimplementable => Empty
-      case _ => Typ(and, true)
-    }
+    if (res) Typ(and, true) else Empty
   }
 
   /* Whether the extractor is irrefutable */
@@ -574,21 +499,92 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
 
   /** Can this type be inhabited by a value?
    *
-   *  Intersection between singleton types and other types is always empty
-   *  the singleton type is not a subtype of the other type.
-   *  See patmat/i3573.scala for an example.
+   *  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(tpe: Type)(implicit ctx: Context): Boolean = {
-    val emptySingletonIntersection = new ExistsAccumulator({
-      case AndType(s: SingletonType, t) =>
-        !(s <:< t)
-      case AndType(t, s: SingletonType) =>
-        !(s <:< t)
-      case x =>
-        false
-    })
-
-    !emptySingletonIntersection(false, tpe)
+  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 superType(tp: Type): Type = tp match {
+      case tp: TypeProxy     => tp.superType
+      case OrType(tp1, tp2)  => OrType(superType(tp1), superType(tp2))
+      case AndType(tp1, tp2) => AndType(superType(tp1), superType(tp2))
+      case _                 => tp
+    }
+
+    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)
+
+          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 <:< superType(tp2)) &&
+            (!bases2.exists(_ is Final) || tp2 <:< superType(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 type `tp1` to be a subtype of `tp2`
@@ -708,8 +704,10 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   /** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
   def canDecompose(tp: Type): Boolean = {
     val dealiasedTp = tp.dealias
-    val res = tp.classSymbol.is(allOf(Abstract, Sealed)) ||
-      tp.classSymbol.is(allOf(Trait, Sealed)) ||
+    val res =
+      (tp.classSymbol.is(Sealed) &&
+        tp.classSymbol.is(AbstractOrTrait) &&
+        tp.classSymbol.children.nonEmpty ) ||
       dealiasedTp.isInstanceOf[OrType] ||
       (dealiasedTp.isInstanceOf[AndType] && {
         val and = dealiasedTp.asInstanceOf[AndType]
@@ -905,24 +903,25 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   def checkRedundancy(_match: Match): Unit = {
     val Match(sel, cases) = _match
     // ignore selector type for now
-    // val selTyp = sel.tpe.widen.dealias
-
-    if (cases.length == 1) return
+    val selTyp = sel.tpe.widen.dealias
 
-    // starts from the second, the first can't be redundant
-    (1 until cases.length).foreach { i =>
+    (0 until cases.length).foreach { i =>
       // in redundancy check, take guard as false in order to soundly approximate
-      val prevs = cases.take(i).map { x =>
-        if (x.guard.isEmpty) project(x.pat)
-        else Empty
-      }.reduce((a, b) => Or(List(a, b)))
+      val prevs =
+        if (i == 0)
+          Empty
+        else
+          cases.take(i).map { x =>
+            if (x.guard.isEmpty) project(x.pat)
+            else Empty
+          }.reduce((a, b) => Or(List(a, b)))
 
       val curr = project(cases(i).pat)
 
       debug.println(s"---------------reachable? ${show(curr)}")
       debug.println(s"prev: ${show(prevs)}")
 
-      if (isSubspace(curr, prevs)) {
+      if (isSubspace(intersect(curr, Typ(selTyp, false)), prevs)) {
         ctx.warning(MatchCaseUnreachable(), cases(i).body.pos)
       }
     }
diff --git a/tests/patmat/3144.check b/tests/patmat/3144.check
new file mode 100644
index 000000000000..78d2e4638a32
--- /dev/null
+++ b/tests/patmat/3144.check
@@ -0,0 +1 @@
+6: Pattern Match Exhaustivity: _: Foo
diff --git a/tests/patmat/3144c.check b/tests/patmat/3144c.check
new file mode 100644
index 000000000000..78d2e4638a32
--- /dev/null
+++ b/tests/patmat/3144c.check
@@ -0,0 +1 @@
+6: Pattern Match Exhaustivity: _: Foo
diff --git a/tests/patmat/3144c.scala b/tests/patmat/3144c.scala
new file mode 100644
index 000000000000..b92c231af25b
--- /dev/null
+++ b/tests/patmat/3144c.scala
@@ -0,0 +1,9 @@
+sealed trait Foo
+case class Bar(s: String)
+
+object Test {
+  def shouldError(foo: Foo): String =
+    foo match {
+      case bar: Bar => bar.s
+    }
+}
\ No newline at end of file
diff --git a/tests/patmat/3145.scala b/tests/patmat/3145.scala
new file mode 100644
index 000000000000..b8fc5d9b135e
--- /dev/null
+++ b/tests/patmat/3145.scala
@@ -0,0 +1,43 @@
+object Test {
+  sealed trait Foo
+  class Bar(val s: String) extends Foo
+  sealed abstract class Baz(val s: String) extends Foo
+
+  val f: Foo => String = {
+    case bar: Bar => bar.s
+    case baz: Baz => baz.s
+  }
+}
+
+object Test2 {
+  sealed trait Foo
+  class Bar extends Foo
+  sealed trait Baz extends Foo
+
+  def f(x: Foo) = x match {
+    case bar: Bar => 1
+    case baz: Baz => 2
+  }
+}
+
+object Test3 {
+  sealed trait Foo
+  class Bar extends Foo
+  sealed trait Baz extends Foo
+
+  def foo = {
+    val x: Foo = new Baz {}
+    x match {
+      case bar: Bar => 1
+      case baz: Baz => 2
+    }
+  }
+
+  def bar = {
+    val x: Baz  = new Baz {}
+    x match {
+      case bar: Bar => 1
+      case baz: Baz => 2
+    }
+  }
+}
\ No newline at end of file
diff --git a/tests/patmat/andtype-opentype-interaction.check b/tests/patmat/andtype-opentype-interaction.check
index 4ef4731d64bd..cf7ea560f42d 100644
--- a/tests/patmat/andtype-opentype-interaction.check
+++ b/tests/patmat/andtype-opentype-interaction.check
@@ -1,6 +1,7 @@
-23: Pattern Match Exhaustivity: _: SealedClass & OpenTrait, _: AbstractClass & OpenTrait, _: Clazz & OpenTrait, _: Trait & OpenTrait
-27: Pattern Match Exhaustivity: _: SealedClass & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: Trait & 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
+23: Pattern Match Exhaustivity: _: SealedAbstractClass & OpenTrait, _: SealedClass & OpenTrait, _: SealedTrait & OpenTrait, _: AbstractClass & OpenTrait, _: Clazz & OpenTrait, _: Trait & OpenTrait
+27: Pattern Match Exhaustivity: _: SealedAbstractClass & OpenTrait & OpenTrait2, _: SealedClass & OpenTrait & OpenTrait2, _: SealedTrait & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: Trait & OpenTrait & OpenTrait2
+31: Pattern Match Exhaustivity: _: SealedTrait & OpenClass, _: Trait & OpenClass
+35: Pattern Match Exhaustivity: _: SealedTrait & OpenTrait & OpenClass, _: Trait & OpenTrait & OpenClass
+40: Match case Unreachable
+43: Pattern Match Exhaustivity: _: SealedTrait & OpenAbstractClass, _: Trait & OpenAbstractClass
+47: Pattern Match Exhaustivity: _: SealedTrait & OpenClass & OpenTrait & OpenClassSubclass, _: Trait & OpenClass & OpenTrait & OpenClassSubclass
diff --git a/tests/patmat/andtype-refinedtype-interaction.check b/tests/patmat/andtype-refinedtype-interaction.check
index 2f8687a868e5..ce6d6e51b2d1 100644
--- a/tests/patmat/andtype-refinedtype-interaction.check
+++ b/tests/patmat/andtype-refinedtype-interaction.check
@@ -1,6 +1,9 @@
 32: Pattern Match Exhaustivity: _: Trait & C1{x: Int}
+37: Match case Unreachable
+43: Match case Unreachable
 48: Pattern Match Exhaustivity: _: Clazz & (C1 | C2 | T1){x: Int} & (C3 | C4 | T2){x: Int}, _: Trait & (C1 | C2 | T1){x: Int} & (C3 | C4 | T2){x: Int}
 54: Pattern Match Exhaustivity: _: Trait & (C1 | C2 | T1){x: Int} & C3{x: Int}
+60: Match case Unreachable
 65: Pattern Match Exhaustivity: _: Trait & (C1 | C2){x: Int} & (C3 | SubC1){x: Int}
 72: Pattern Match Exhaustivity: _: Trait & (T1 & (C1 | SubC2)){x: Int} & (T2 & (C2 | C3 | SubC1)){x: Int} &
   SubSubC1{x: Int}
diff --git a/tests/patmat/i2253.check b/tests/patmat/i2253.check
index 5c86a1ef824b..d43092db6263 100644
--- a/tests/patmat/i2253.check
+++ b/tests/patmat/i2253.check
@@ -1,3 +1,5 @@
-27: Pattern Match Exhaustivity: HasIntXIntM, HasIntXStringM
-28: Pattern Match Exhaustivity: HasIntXIntM
+28: Pattern Match Exhaustivity: HasIntXIntM, HasIntXStringM
 29: Pattern Match Exhaustivity: HasIntXIntM
+29: Match case Unreachable
+30: Pattern Match Exhaustivity: HasIntXIntM
+30: Match case Unreachable
diff --git a/tests/patmat/i2253.scala b/tests/patmat/i2253.scala
index 0344a6a5d2f1..33e4e0e87ec5 100644
--- a/tests/patmat/i2253.scala
+++ b/tests/patmat/i2253.scala
@@ -22,6 +22,7 @@ object HasIntXIntM extends S {
 }
 
 trait T
+case class TA(val x: Int) extends T with S
 
 class Test {
   def onlyIntX(s: S { val x: Int }) = s match { case _: T => ; }
diff --git a/tests/patmat/patmatexhaust.check b/tests/patmat/patmatexhaust.check
index e5e7ac397383..28927e2fedeb 100644
--- a/tests/patmat/patmatexhaust.check
+++ b/tests/patmat/patmatexhaust.check
@@ -4,6 +4,7 @@
 49: Pattern Match Exhaustivity: _: Gp
 59: Pattern Match Exhaustivity: Nil
 75: Pattern Match Exhaustivity: _: B
+87: Pattern Match Exhaustivity: _: C1
 100: Pattern Match Exhaustivity: _: C1
 114: Pattern Match Exhaustivity: D2(), D1
 126: Pattern Match Exhaustivity: _: C1
diff --git a/tests/patmat/patmatexhaust.scala b/tests/patmat/patmatexhaust.scala
index 26f0c12a919c..0649620d31ef 100644
--- a/tests/patmat/patmatexhaust.scala
+++ b/tests/patmat/patmatexhaust.scala
@@ -84,7 +84,7 @@ class TestSealedExhaustive { // compile only
     case class C3() extends C
     case object C4 extends C
 
-    def ma10(x: C) = x match {  // exhaustive: abstract sealed C1 is dead end.
+    def ma10(x: C) = x match {  // treat abstract sealed C1 is as inhabited.
       case C3()     => true
       case C2 | C4  => true
     }
diff --git a/tests/patmat/t6450.scala b/tests/patmat/t6450.scala
index 157f1ce8124e..92194c2e48ab 100644
--- a/tests/patmat/t6450.scala
+++ b/tests/patmat/t6450.scala
@@ -1,5 +1,5 @@
 sealed abstract class FoundNode[T]
-// case class A[T](x: T) extends FoundNode[T]
+case class A[T](x: T) extends FoundNode[T]
 
 object Foo {
   val v: (Some[_], FoundNode[_]) = (???, ???)
diff --git a/tests/patmat/t8511.check b/tests/patmat/t8511.check
index 6f63f1040f5b..121e0ab874e0 100644
--- a/tests/patmat/t8511.check
+++ b/tests/patmat/t8511.check
@@ -1 +1 @@
-18: Pattern Match Exhaustivity: Baz(), Bar(_)
+18: Pattern Match Exhaustivity: EatsExhaustiveWarning(_), Baz(), Bar(_)
diff --git a/tests/patmat/t9677.check b/tests/patmat/t9677.check
deleted file mode 100644
index 3d9e1c4e2bbb..000000000000
--- a/tests/patmat/t9677.check
+++ /dev/null
@@ -1 +0,0 @@
-20: Match case Unreachable
diff --git a/tests/patmat/virtpatmat_reach_sealed_unsealed.check b/tests/patmat/virtpatmat_reach_sealed_unsealed.check
index 6b0ea7f8e1e6..3d9eff70f640 100644
--- a/tests/patmat/virtpatmat_reach_sealed_unsealed.check
+++ b/tests/patmat/virtpatmat_reach_sealed_unsealed.check
@@ -1,3 +1,4 @@
 16: Pattern Match Exhaustivity: false
 18: Match case Unreachable
 19: Match case Unreachable
+20: Match case Unreachable