The benefit is not only about "documenting the contracts" but documenting the contracts in a way that we can trust those contracts can not be violated when the program is running.

That is a very good thing to help us reason about the program, we have invariants we know must hold true if the program does not stop in a type-error.