Expected compiler behavior?

Does anyone know whether it is expected that the compiler doesn’t know that Succ[predM] is equal to M in this piece of code?

ticket with discussion: Lack of type refinement for match case · Issue #15958 · lampepfl/dotty · GitHub