Scala: pattern matching on a path-dependent type

Can't figure out why Scala 2.13 is unhappy about pattern matching here

  trait A {
    sealed trait T
    case class TImpl() extends T
  }

  trait Fail[B <: A] {
    val a: B // no error if `a: A`
    def foo(t : a.T): Unit = t match {
      case _: a.TImpl => // "match may not be exhaustive. It would fail on the following input: TImpl()"
    }
  }

Any reasonable workaround? Seems to be fine with Dotty

If you want to see why in principle the pattern matching can be not exhaustive, for instance see the following example

trait A {
  sealed trait T
  case class TImpl() extends T
}

trait Fail[B <: A] {
  val a: B
  def foo(t : a.T): Unit = t match {
    case _: a.TImpl => 
  }
}

class B extends A
val b = new B
class FailImpl extends Fail[b.type] {
  override val a: b.type = b
}
val fail: Fail[b.type] = new FailImpl

class C
case class CImpl() extends C with b.T
val x = CImpl()
fail.foo(x) // MatchError

You could say that actually we didn't have C. Well, compiler should be smart enough to figure out that.

If you want to switch the warning off you can write @unchecked

def foo(t : a.T): Unit = (t: @unchecked) match {
  case _: a.TImpl => 
}

According to specification,

If the selector of a pattern match is an instance of a sealed class, the compilation of pattern matching can emit warnings which diagnose that a given set of patterns is not exhaustive, i.e. that there is a possibility of a MatchError being raised at run-time.

https://scala-lang.org/files/archive/spec/2.13/08-pattern-matching.html#pattern-matching-expressions

Compiler can emit a warning but not must. So absence of warning doesn't guarantee that a pattern matching is exhaustive.