What do we know about the types of Z.add, Z.equal, Z.one, Z.minus_one and Z.of_int?

You need that information if you want to conclude that n, n_1, n_2 and acc all have type Z.t. Presumably, the software which gives you the type hint 'a -> 'b -> 'b -> 'c -> 'c does not have access to that information.

Without knowing the types of functions Z.add and Z.equal, we can conclude that acc and the return value have the same type, because of the then acc branch, and we can conclude that n_1 and n_2 have the same type, because n_2 in place of n_1 in the recursive call. This explains the type 'a -> 'b -> 'b -> 'c -> 'c.