You are right. The biggest problem I was trying to point out is that you need to make your static type system much more complex in order to be able to even state some things that are easy to check dynamically. Also, dependent types on their own dont solve the problem of interfacing with dynamic code.