diff --git a/tests/neg/i17121.check b/tests/neg/i17121.check
new file mode 100644
index 000000000000..9570cb597335
--- /dev/null
+++ b/tests/neg/i17121.check
@@ -0,0 +1,24 @@
+-- [E189] Type Error: tests/neg/i17121.scala:13:17 ---------------------------------------------------------------------
+13 |  type G1[X] = X match { case Consumer[List[t]] => t } // error
+   |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |               The match type contains an illegal case:
+   |                   case Consumer[List[t]] => t
+   |               (this error can be ignored for now with `-source:3.3`)
+-- [E189] Type Error: tests/neg/i17121.scala:15:17 ---------------------------------------------------------------------
+15 |  type G2[X] = X match { case Consumer[Consumer[t]] => t } // error
+   |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |               The match type contains an illegal case:
+   |                   case Consumer[Consumer[t]] => t
+   |               (this error can be ignored for now with `-source:3.3`)
+-- [E189] Type Error: tests/neg/i17121.scala:17:17 ---------------------------------------------------------------------
+17 |  type G3[X] = X match { case Consumer[Consumer[Consumer[t]]] => t } // error
+   |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |               The match type contains an illegal case:
+   |                   case Consumer[Consumer[Consumer[t]]] => t
+   |               (this error can be ignored for now with `-source:3.3`)
+-- [E189] Type Error: tests/neg/i17121.scala:19:17 ---------------------------------------------------------------------
+19 |  type G4[X] = X match { case Consumer[List[Consumer[t]]] => t } // error
+   |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |               The match type contains an illegal case:
+   |                   case Consumer[List[Consumer[t]]] => t
+   |               (this error can be ignored for now with `-source:3.3`)
diff --git a/tests/neg/i17121.scala b/tests/neg/i17121.scala
new file mode 100644
index 000000000000..0e845cf3266d
--- /dev/null
+++ b/tests/neg/i17121.scala
@@ -0,0 +1,20 @@
+class Consumer[-T]
+
+object Test:
+  type F1[X] = X match { case List[t] => t } // OK
+  summon[F1[List[?]] =:= Any]
+
+  type F2[X] = X match { case Consumer[t] => t } // OK
+  summon[F2[Consumer[?]] =:= Nothing]
+
+  type F3[X] = X match { case List[Consumer[t]] => t } // OK
+  summon[F3[List[Consumer[?]]] =:= Nothing]
+
+  type G1[X] = X match { case Consumer[List[t]] => t } // error
+
+  type G2[X] = X match { case Consumer[Consumer[t]] => t } // error
+
+  type G3[X] = X match { case Consumer[Consumer[Consumer[t]]] => t } // error
+
+  type G4[X] = X match { case Consumer[List[Consumer[t]]] => t } // error
+end Test
diff --git a/tests/neg/i17944.check b/tests/neg/i17944.check
new file mode 100644
index 000000000000..80dfaac8c4c8
--- /dev/null
+++ b/tests/neg/i17944.check
@@ -0,0 +1,46 @@
+-- [E172] Type Error: tests/neg/i17944.scala:40:87 ---------------------------------------------------------------------
+40 |    val s = Selector.selectorInst[("s" ->> String) *: ("i" ->> Int) *: EmptyTuple, "i"] // error
+   |                                                                                       ^
+   |No singleton value available for Tuple.Elem[test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)], (1 : Int)]; eligible singleton types for `ValueOf` synthesis include literals and stable paths.
+   |
+   |Note: a match type could not be fully reduced:
+   |
+   |  trying to reduce  Tuple.Elem[test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)], (1 : Int)]
+   |  trying to reduce  test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)]
+   |  trying to reduce  test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)]
+   |  failed since selector (("s" : String) ->> String, ("i" : String) ->> Int)
+   |  does not match  case (("i" : String) ->> f) *: _ => (f, (0 : Int))
+   |  and cannot be shown to be disjoint from it either.
+   |  Therefore, reduction cannot advance to the remaining case
+   |
+   |    case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]]
+   |  trying to reduce  test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)]
+   |  trying to reduce  test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)]
+   |  failed since selector (("s" : String) ->> String, ("i" : String) ->> Int)
+   |  does not match  case (("i" : String) ->> f) *: _ => (f, (0 : Int))
+   |  and cannot be shown to be disjoint from it either.
+   |  Therefore, reduction cannot advance to the remaining case
+   |
+   |    case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]]
+   |  trying to reduce  test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)]
+   |  failed since selector (("s" : String) ->> String, ("i" : String) ->> Int)
+   |  does not match  case (("i" : String) ->> f) *: _ => (f, (0 : Int))
+   |  and cannot be shown to be disjoint from it either.
+   |  Therefore, reduction cannot advance to the remaining case
+   |
+   |    case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]]
+   |  trying to reduce  test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)]
+   |  trying to reduce  test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)]
+   |  failed since selector (("s" : String) ->> String, ("i" : String) ->> Int)
+   |  does not match  case (("i" : String) ->> f) *: _ => (f, (0 : Int))
+   |  and cannot be shown to be disjoint from it either.
+   |  Therefore, reduction cannot advance to the remaining case
+   |
+   |    case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]]
+   |  trying to reduce  test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)]
+   |  failed since selector (("s" : String) ->> String, ("i" : String) ->> Int)
+   |  does not match  case (("i" : String) ->> f) *: _ => (f, (0 : Int))
+   |  and cannot be shown to be disjoint from it either.
+   |  Therefore, reduction cannot advance to the remaining case
+   |
+   |    case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]]
diff --git a/tests/neg/i17944.scala b/tests/neg/i17944.scala
new file mode 100644
index 000000000000..214dfaebbfcf
--- /dev/null
+++ b/tests/neg/i17944.scala
@@ -0,0 +1,44 @@
+package test {
+
+  import types._
+
+  object types {
+    opaque type ->>[K, V] = V
+    extension [K <: Singleton](k: K) def ->>[V](v: V): K ->> V = v.asInstanceOf[K ->> V]
+  }
+
+  type FindField[T <: Tuple, K] = FindField0[T, K, 0]
+
+  type FindField0[T <: Tuple, K, I <: Int] <: (Any, Int) = T match {
+    case (K ->> f) *: _ => (f, I)
+    case _ *: t => FindField0[t, K, compiletime.ops.int.S[I]]
+  }
+
+  trait Selector[T, Key, Out] {
+    def apply(t: T): Out
+  }
+
+  object Selector {
+    inline def selectorInst[T <: Tuple, K](
+      using idx: ValueOf[Tuple.Elem[FindField[T, K], 1]],
+    ): Selector[T, K, Tuple.Head[FindField[T, K]]] =
+      new Selector[T, K, Tuple.Head[FindField[T, K]]] {
+        def apply(t: T): Tuple.Head[FindField[T, K]] =
+          val i: Int = idx.value.asInstanceOf[Int]
+          t.productElement(i).asInstanceOf[Tuple.Head[FindField[T, K]]]
+      }
+  }
+
+}
+
+object Test {
+  def main(args: Array[String]): Unit = {
+    import test._
+    import test.types._
+
+    val t = ("s" ->> "foo") *: ("i" ->> 3) *: EmptyTuple
+    val s = Selector.selectorInst[("s" ->> String) *: ("i" ->> Int) *: EmptyTuple, "i"] // error
+    val r = s(t)
+    println(r)
+  }
+}
diff --git a/tests/pos/i18488.scala b/tests/pos/i18488.scala
new file mode 100644
index 000000000000..c225a2c20711
--- /dev/null
+++ b/tests/pos/i18488.scala
@@ -0,0 +1,15 @@
+trait AbstractTable[T]
+
+trait Query[E, U]
+
+class TableQuery[E <: AbstractTable[?]] extends Query[E, Extract[E]]
+
+type Extract[E] = E match
+  case AbstractTable[t] => t
+
+trait BaseCrudRepository[E[T[_]]]:
+
+  type EntityTable <: AbstractTable[E[Option]]
+
+  def filterById: Query[EntityTable, Extract[EntityTable]] =
+    new TableQuery[EntityTable]