Type erasure has nothing to do with soundness - ocaml also erases types at runtime but it is sound. In typescript "any" type, unsafe casting, non null assertion

Type erasure has nothing to do with soundness - ocaml also erases types at runtime but it is sound. In typescript "any" type, unsafe casting, non null assertions and couple of other constructs are unsound. Gradual typing at package level was addressed by (also unsound) declaration repository (overall successful I'd say - primary reason it won over flow in my opinion). I have a problem reconciling "sound gradual typing" - is there such thing at all? Sounds like contradiction to me, no? Untyped function's result can be considered "unknown" (as opposed to "any" using typescript terminology) and require runtime checks at call site (as if it was i/o boundary) - that's fine but arguments on the other hand must have some type declaration on its signature to be considered sound. Injecting runtime checks in untyped library for arguments feels nonsensical because if you can do it then you already did static code analysis that did infer argument types and you can shove it into function signature as static type declaration - ie. that's just more sophisticated static inference that doesn't require runtime code injection. You could argue that there may be some dynamism that cannot be expressed at type level and that requires runtime checks deeper in the untyped code but if it cannot be expressed then by definition it's unsound and frankly who cares about runtime checks nested deeply in untyped code - what's the difference if it blows up at runtime in the middle of that untyped function with type error or some other error?