Yeah, that's exactly how dynamic data can enter a statically typed regime of code. Dependent types make it so that it's impossible to bring dynamic data into type-controlled parts of your code without first performing and passing those tests.
Which seems weak since smart developers should do that anyway, but (a) there's still some divide between "should" and "it's impossible" and (b) this is just the tip of the iceberg about what dependent types offer anyway.
