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?