diff --git a/compiler/src/dotty/tools/dotc/config/Printers.scala b/compiler/src/dotty/tools/dotc/config/Printers.scala
index 8e13e50e59b7..de8f20c8ad1e 100644
--- a/compiler/src/dotty/tools/dotc/config/Printers.scala
+++ b/compiler/src/dotty/tools/dotc/config/Printers.scala
@@ -21,7 +21,7 @@ object Printers {
   val derive = noPrinter
   val desugar = noPrinter
   val scaladoc = noPrinter
-  val exhaustivity = noPrinter
+  val exhaustivity = default
   val gadts = noPrinter
   val gadtsConstr = noPrinter
   val hk = noPrinter
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 45d02ca9538e..d682e2755585 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -2526,10 +2526,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         case _ => false
       })
 
-    /** Can we enumerate all instantiations of this type? */
-    def isClosedSum(tp: Symbol): Boolean =
-      tp.is(Sealed) && tp.isOneOf(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.
@@ -2570,9 +2566,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             // subtype, so they must be unrelated by single inheritance
             // of classes.
             true
-          else if (isClosedSum(cls1))
+          else if (cls1.isClosedSum)
             decompose(cls1, tp1).forall(x => provablyDisjoint(x, tp2))
-          else if (isClosedSum(cls2))
+          else if (cls2.isClosedSum)
             decompose(cls2, tp2).forall(x => provablyDisjoint(x, tp1))
           else
             false
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index c25403b68e00..5a5a3669182b 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -11,7 +11,7 @@ import StdNames._
 import collection.mutable
 import ast.tpd._
 import reporting.{trace, Message}
-import config.Printers.{gadts, typr}
+import config.Printers.{exhaustivity, gadts, typr}
 import config.Feature
 import typer.Applications._
 import typer.ProtoTypes._
@@ -694,6 +694,8 @@ object TypeOps:
    *  Otherwise, return NoType.
    */
   private def instantiateToSubType(tp1: NamedType, tp2: Type)(using Context): Type = {
+    exhaustivity.println(i"instantiate $tp1 to a subtype of $tp2")
+
     // In order for a child type S to qualify as a valid subtype of the parent
     // T, we need to test whether it is possible S <: T.
     //
@@ -701,7 +703,7 @@ object TypeOps:
     // `this`. We perform the following operations to approximate the parameters:
     //
     // 1. Replace type parameters in T with tvars
-    // 2. Replace `A.this.C` with `A#C` (see tests/patmat/i12681.scala)
+    // 2. Replace non-class applied types with a tvar, bounded by its type constructor's underlying type
     // 3. Replace non-reducing MatchType with its bound
     //
     val approximateParent = new TypeMap {
@@ -715,9 +717,6 @@ object TypeOps:
                                  // then to avoid it failing the <:<
                                  // we'll approximate by widening to its bounds
 
-        case ThisType(tref: TypeRef) if !tref.symbol.isStaticOwner =>
-          tref
-
         case tp: TypeRef if !tp.symbol.isClass =>
           def lo = LazyRef.of(apply(tp.underlying.loBound))
           def hi = LazyRef.of(apply(tp.underlying.hiBound))
@@ -786,7 +785,7 @@ object TypeOps:
             this(tref)
           else {
             prefixTVar = WildcardType  // prevent recursive call from assigning it
-            val tref2 = this(tref.applyIfParameterized(tref.typeParams.map(_ => TypeBounds.empty)))
+            val tref2 = inferPrefix(tref.applyIfParameterized(tref.typeParams.map(_ => TypeBounds.empty)))
             prefixTVar = newTypeVar(TypeBounds.upper(tref2))
             prefixTVar
           }
@@ -794,9 +793,15 @@ object TypeOps:
       }
     }
 
-    val inferThisMap = new InferPrefixMap
-    val tvars = tp1.typeParams.map { tparam => newTypeVar(tparam.paramInfo.bounds) }
-    val protoTp1 = inferThisMap.apply(tp1).appliedTo(tvars)
+    def inferPrefix(tp: Type): Type =
+      val inferThisMap = new InferPrefixMap
+      val tvars = tp.typeParams.map(tparam => newTypeVar(tparam.paramInfo.bounds))
+      val pt = inferThisMap(tp).appliedTo(tvars)
+      if tp ne pt then
+        exhaustivity.println(i"inferPrefix: $tp -> $pt")
+      pt
+
+    val protoTp1 = inferPrefix(tp1)
 
     // If parent contains a reference to an abstract type, then we should
     // refine subtype checking to eliminate abstract types according to
@@ -807,15 +812,41 @@ object TypeOps:
       parent.argInfos.nonEmpty && approximateParent(parent) <:< tp2
     }
 
-    def instantiate(): Type = {
+    def maximizeLoop(): Type =
       maximizeType(protoTp1, NoSpan, fromScala2x = false)
-      wildApprox(protoTp1)
+      exhaustivity.println(i"maximized protoTp1, now: $protoTp1")
+      if variances(protoTp1).forallBinding((tvar, _) => tvar.isInstantiated) then protoTp1
+      else maximizeLoop()
+
+    def instantiate(): Type = {
+      maximizeLoop()
+      val res = wildApprox(protoTp1)
+      exhaustivity.println(i"approximated wildcards in protoTp1, now: $res")
+      res
     }
 
-    if (protoTp1 <:< tp2) instantiate()
-    else {
-      val approxTp2 = approximateParent(tp2)
-      if (protoTp1 <:< approxTp2 || parentQualify(protoTp1, approxTp2)) instantiate()
+    exhaustivity.println(TypeComparer.explained(_.isSubType(protoTp1, tp2)))
+
+    val isSub = protoTp1 <:< tp2
+    exhaustivity.println(i"$protoTp1 <:< $tp2 = $isSub")
+    if (isSub) {
+      instantiate()
+    } else {
+      val approxTp2E = approximateParent(tp2)
+      val approxTp2  = inferPrefix(approxTp2E)
+      if tp2 ne approxTp2 then
+        exhaustivity.println(i"approximateParent: $tp2 -> $approxTp2E -> $approxTp2")
+        exhaustivity.println(i"      tp2 =${tp2.toString}")
+        exhaustivity.println(i"approxTp2E=${approxTp2E.toString}")
+        exhaustivity.println(i"approxTp2 =${approxTp2.toString}")
+      exhaustivity.println(TypeComparer.explained(_.isSubType(protoTp1, approxTp2)))
+      val isSub2 = protoTp1 <:< approxTp2
+      exhaustivity.println(i"$protoTp1 <:< $approxTp2 = $isSub2")
+      if (isSub2 || {
+        val qual = parentQualify(protoTp1, approxTp2)
+        exhaustivity.println(i"parentQualify($protoTp1, $approxTp2) = $qual")
+        qual
+      }) instantiate()
       else NoType
     }
   }
diff --git a/compiler/src/dotty/tools/dotc/transform/SymUtils.scala b/compiler/src/dotty/tools/dotc/transform/SymUtils.scala
index acfb4be5c022..20ba32f0898f 100644
--- a/compiler/src/dotty/tools/dotc/transform/SymUtils.scala
+++ b/compiler/src/dotty/tools/dotc/transform/SymUtils.scala
@@ -246,6 +246,10 @@ object SymUtils:
     def hasAnonymousChild(using Context): Boolean =
       self.children.exists(_ `eq` self)
 
+    /** Can we enumerate all instantiations of this type? */
+    def isClosedSum(using Context): Boolean =
+      self.is(Sealed) && self.isOneOf(AbstractOrTrait) && !self.hasAnonymousChild
+
     /** Is this symbol directly owner by a term symbol, i.e., is it local to a block? */
     def isLocalToBlock(using Context): Boolean =
       self.owner.isTerm
diff --git a/compiler/src/dotty/tools/dotc/transform/SyntheticMembers.scala b/compiler/src/dotty/tools/dotc/transform/SyntheticMembers.scala
index ac8d96afb604..abe313b8e9f8 100644
--- a/compiler/src/dotty/tools/dotc/transform/SyntheticMembers.scala
+++ b/compiler/src/dotty/tools/dotc/transform/SyntheticMembers.scala
@@ -517,13 +517,19 @@ class SyntheticMembers(thisPhase: DenotTransformer) {
   def ordinalBody(cls: Symbol, param: Tree)(using Context): Tree =
     if (cls.is(Enum)) param.select(nme.ordinal).ensureApplied
     else {
+      def collect(children: List[Symbol], seen: Set[Symbol], acc: List[Symbol]): List[Symbol] = children match {
+        case c :: rest if seen(c)       => collect(rest, seen, acc)
+        case c :: rest if c.isClosedSum => collect(c.children ::: rest, seen + c, acc)
+        case c :: rest                  => collect(rest, seen + c, c :: acc)
+        case _                          => acc
+      }
       val cases =
-        for ((child, idx) <- cls.children.zipWithIndex) yield {
+        for ((child, idx) <- collect(List(cls), Set(), Nil).reverseIterator.zipWithIndex) yield {
           val patType = if (child.isTerm) child.reachableTermRef else child.reachableRawTypeRef
-          val pat = Typed(untpd.Ident(nme.WILDCARD).withType(patType), TypeTree(patType))
+          val pat = Typed(Underscore(patType), TypeTree(patType))
           CaseDef(pat, EmptyTree, Literal(Constant(idx)))
         }
-      Match(param.annotated(New(defn.UncheckedAnnot.typeRef, Nil)), cases)
+      Match(param, cases.toList)
     }
 
   /** - If `impl` is the companion of a generic sum, add `deriving.Mirror.Sum` parent
diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
index 7654b98995ff..98052d3cce5c 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -449,7 +449,7 @@ object Inferencing {
    *
    *  we want to instantiate U to x.type right away. No need to wait further.
    */
-  private def variances(tp: Type)(using Context): VarianceMap = {
+  final def variances(tp: Type)(using Context): VarianceMap = {
     Stats.record("variances")
     val constraint = ctx.typerState.constraint
 
diff --git a/tests/patmat/i3938.check b/tests/patmat/i3938.check
index 5aaefe2263e1..3fe53d7c93bc 100644
--- a/tests/patmat/i3938.check
+++ b/tests/patmat/i3938.check
@@ -1 +1 @@
-34: Pattern Match Exhaustivity: bar.C()
+34: Pattern Match Exhaustivity: Foo#Bar & (Test.this.foo.bar : Test.this.foo.Bar).C()
diff --git a/tests/patmat/t6146.nest1.scala b/tests/patmat/t6146.nest1.scala
new file mode 100644
index 000000000000..06c0aa8e06bb
--- /dev/null
+++ b/tests/patmat/t6146.nest1.scala
@@ -0,0 +1,20 @@
+// Like the "tricksier" variantion in t6146, but less tricksy (less nesting)
+// but also with a non-Any type argument, and some invariant usage of the type.
+// Used to study why `case _: C.type =>` is considered unreachable
+// in the ordinal method object A synthesises.
+trait T[X] {
+  sealed trait A
+  object A {
+    case object B extends A
+  }
+
+  def give: X
+  def take(x: X): X
+}
+
+object O extends T[String] {
+  def give            = "O"
+  def take(x: String) = s"$x. Love, O."
+}
+
+case object C extends O.A
diff --git a/tests/patmat/t6146.nest2.scala b/tests/patmat/t6146.nest2.scala
new file mode 100644
index 000000000000..dd48ff49f180
--- /dev/null
+++ b/tests/patmat/t6146.nest2.scala
@@ -0,0 +1,27 @@
+// Like nest1, but nested twice.
+trait T1[X] {
+  trait T2[Y] {
+    sealed trait A
+    object A {
+      case object B extends A
+    }
+
+    def provide: Y
+    def consume(y: Y): Y
+  }
+
+  def give: X
+  def take(x: X): X
+}
+
+object O1 extends T1[String] {
+  object O2 extends T2[Thread] {
+    def provide            = new Thread("O2")
+    def consume(y: Thread) = new Thread(y, "Love, O2")
+  }
+
+  def give            = "O1"
+  def take(x: String) = s"$x. Love, O1."
+}
+
+case object C extends O1.O2.A
diff --git a/tests/run-custom-args/fatal-warnings/i11050.scala b/tests/run-custom-args/fatal-warnings/i11050.scala
index f0bdd23031fa..7763385cf03d 100644
--- a/tests/run-custom-args/fatal-warnings/i11050.scala
+++ b/tests/run-custom-args/fatal-warnings/i11050.scala
@@ -79,9 +79,9 @@ object Test:
     val d         = D()
     val e         = E()
 
-    assertEq(List(d, e).map(m.ordinal), List(0, 0))
+    assertEq(List(d, e).map(m.ordinal), List(0, 1))
     assertShow[A](d, "[0] [0] D")
-    assertShow[A](e, "[0] [1] E")
+    assertShow[A](e, "[1] [1] E")
   end testFromAkkaCB
 
   def testFromAkkaCB2() =