In Scala 2 or 3, is there a higher kind argument extractor without using match type?

Here is a short example in Scala 3:

  type Ext[S <: Seq[_]] = S match {
    case Seq[t] => t
  }
  
trait XX[A, B <: Seq[A]]

trait XX1[B <: Seq[_]] extends XX[Ext[B], B]

So far it appears to be working, but when combining with type class the mask started to peel off

implicitly[Ext[Seq[Int]] =:= Int] // e.scala: Cannot prove that e.Ext[Seq[Int]] =:= Int

It may be caused by a bug in compatibility between Scala type class & match types. At this moment, the only way to circumvent this appears to be not using match type. Is it possible in Scala 2 or Scala 3?

UPDATE 1: I have tried the following alternatives:

  type Ext[S] = S match {
    case Seq[t] => t
  } // success!

  type Ext[S <: Any] = S match {
    case Seq[t] => t
  } // success!

  type Ext[S <: Seq[Any]] = S match {
    case Seq[t] => t
  } // same error

So I'm fairly certain this is a bug. Again, the problem is how to avoid using match type from the beginning?

Looks like a bug.

There are bugs in match types with type bounds:

https://github.com/lampepfl/dotty/issues/11205

https://github.com/lampepfl/dotty/issues/16058

https://github.com/lampepfl/dotty/issues/16504

Some of them are fixed:

https://github.com/lampepfl/dotty/issues/6758

https://github.com/lampepfl/dotty/issues/6697

https://github.com/lampepfl/dotty/issues/14151

https://github.com/lampepfl/dotty/issues/14477

https://github.com/lampepfl/dotty/issues?page=1&q=is%3Aissue+is%3Aopen+label%3Aarea%3Amatch-types

An alternative to match types is type classes

trait ExtTC[S]:
  type Out
object ExtTC:
  type Aux[S, Out0] = ExtTC[S] { type Out = Out0 }

  given [S <: Seq[T], T]: Aux[S, T] = null

val ext = summon[ExtTC[Seq[Int]]]
summon[ext.Out =:= Int] // compiles

This can't help with type inference (In scala 3, is it possible to make covariant/contravariant type constructor to honour coercive subtyping?)

trait XX[A, B <: Seq[A]]

// doesn't compile: Type argument B does not conform to upper bound Seq[XX1.this.ext.Out]
trait XX1[B <: Seq[_]](using val ext: ExtTC[B]) extends XX[ext.Out, B] 

but can help with implicit resolution

trait XX[A, B](using B <:< Seq[A])

trait XX1[B <: Seq[_]](using val ext: ExtTC[B]) extends XX[ext.Out, B] // compiles