The problem is with the assumed injectivity of the abstract type 'a succ. You should write:
type 'a succ = Succ
then everything works out.
Injectivity was assumed to hold for types *defined* to be abstract, but does not hold for types *declared* as abstract (That may have been defined concretely as just "int" in their implementation). For consistency, defined-abstract type are no more assumed to be injective, so you should always use a constructor for that (using a constructor makes your type nominal/generative/fresh, which enforces injectivity).
Remark: I'll let you work out while it would be problematic to consider a ('a succ succ nat)-matching branch as dead when matching over a ('a succ nat) value, under the definition (type 'a succ = int).