That's an unusual use for "type soundness". To me, type soundness has more to do with whether all the functions in a program are total, i.e. defined across their entire range of inputs (can't throw exceptions, can't crash, always return values belong to the return type they declare).