Can we add dependent type into an existing imperative programming language?
So, it's possible, but there are certainly some barriers:


What kinds of expressions are allowed in types? What does it mean for a type to have a side-effect? Can typrchecking my program perform IO?
Just because dependent types are in the system doesn't mean they provide a type safe language. It may be possible to produce proofs of False if the underlying type system is not consistent.
Many imperative languages don't have type systems complex enough to make dependent types useful. For example, Go has no higher kinded types, so if you can't index types by types, indexing types by values probably won't work.
Depending on the language, some additional type annotations might be necessary to make type checking decidable.
It may be hard to interpret dependent types in the context of side effects. What does a value of type $x=y$ even mean if $x,y$ can change their values at runtime? Does this mean a term can be well typed at one point, and dynamically become ill typed? Or can you only use dependent types for immutable values?


I'm sure that imperative dependent types are possible. In particular, I'd keep my eyes on Rust for adding these in a limited way.

But doing dependent types in a pure functional language is just so much easier.