> What ensures that the “rest of the string” is, in fact, a suffix of the input?

Nothing, unless you have unit tests. Or use Liquid Haskell:

https://ucsd-progsys.github.io/liquidhaskell/

There are languages that let you express stronger guarantees/requirements via type system, but it’s better not to go down the rabbit hole of dependent typing.