Match types could give better error diagnostics

[odersky]

If a match type does not reduce, it simply gets stuck, and we are left with the original type. For instance

trait A
trait B
type M[X] = X match
  case A => Int
  case B => String
val x: String = ??? : M[B]

gives the error message:

6 |val x: String = ??? : M[B]
  |                ^^^^^^^^^^
  |                Found:    M[B]
  |                Required: String

This is not very helpful. It would be great if we could get a more precise diagnostic why the match type reduction did not succeed.
Something like:

6 |val x: String = ??? : M[B]
  |                ^^^^^^^^^^
  |                Found:    M[B]
  |                Required: String

Note: `M[B]` could not be reduced. Reduction got stuck at the case

    case A => Int

Here the selector `B` type does not match `A` but I could not prove that it is disjoint from it either.
Hence, I could not proceed to the next case.

It would be great if we could get error messages like that for the various reasons for getting stuck. Also, if a recursive invocation gets stuck it would be great to see a stack trace of how we got there.

This is sort of similar to the improvements we made for diagnosing implicits.