Lost non-exhaustivity and unreachability warning for union of singletons resulting from match type returned from a method

[TomasMikula]

Compiler version

3.6.4

Minimized code

sealed trait ->[K, V]
sealed trait Append[Init, KV]

type KeyOf[KV] = KV match
  case k -> v => k
  
type KeysOf[KVs] = KVs match
  case k -> v => k
  case Append[init, last] => KeysOf[init] | KeyOf[last]

// Good: Correctly warns about both non-exhaustivity and unreachable case
def ok(k: KeysOf[Append["x" -> String, "y" -> Int]]): Unit =
  k match
    case "x" => println("x")
    case "z" => println("z")

trait Elem[KVs]:
  def key: KeysOf[KVs]

// Bad: only unreachability warning, no non-exhaustivity warning
def ko(elem: Elem[Append["x" -> String, "y" -> Int]]): Unit =
  elem.key match
    case "x" => println("x")
    case "z" => println("z")

// Worse: neither non-exhaustivity nor unreachability warning
def ko2(elem: Elem[Append["x" -> String, "y" -> Int]]): Unit =
  val k = elem.key // the type of `k` is inferred to be `String` instead of `"x" | "y"`
  k match
    case "x" => println("x")
    case "z" => println("z")

Output

-- [E029] Pattern Match Exhaustivity Warning: test.scala:13:2 ------------------
13 |  k match
   |  ^
   |  match may not be exhaustive.
   |
   |  It would fail on pattern case: "y"
   |
   | longer explanation available when compiling with `-explain`
-- [E030] Match case Unreachable Warning: test.scala:15:9 ----------------------
15 |    case "z" => println("z")
   |         ^^^
   |         Unreachable case
-- [E030] Match case Unreachable Warning: test.scala:24:9 ----------------------
24 |    case "z" => println("z")
   |         ^^^
   |         Unreachable case
3 warnings found

Expectation

The compiler should issue both non-exhaustivity and unreachability warning for pattern matches in both ko and ko2 methods, just like it does in method ok.