I am not versed in Ada, but Ada does not seem to have dependent types at all, in fact the author doesn't seem to understand what dependent types are. All his examples seem to revolve about arrays and bounded integers so I will stick to those example (although DT are far richer than that).
In a language with dependent types you don't merely have arrays with arbitrary bounds, but you get a proof that array access is always within bounds. AFAICT this is missing in Ada, even when SPARK is employed. Similarly with bounded integers. In a DT language don't get runtime bound checks, it's all compile time proofs.
In Ada, even the name of the feature makes it pretty clear that it's just runtime verification:
type My_Record (Top, Bottom : My_Integer) is record
Field : My_Array(Bottom .. Top);
end record
with Dynamic_Predicate => Bottom
It's not a dynamic predicate in either a language with DT or refinement types! It's all in compile time proofs!
SPARK does attempt to prove certain properties of programs automatically, including things like bounds checking, which is great, but it's all best effort and it's nowhere at the same level of capability compared to when using DT (or even refinement types). Of course it's far more lightweight (although it can be argued that systems based on refinement types are just as lightweight).
It's very clear that people developing SPARK know a lot about type theory and formal verification, and use as much of the theory as possible to make verification of Ada programs as cheap and ergonomic as possible, but to claim that Ada has DT is quite a stretch. People are using DT to do formal verification of C programs but that doesn't mean that C has dependent types.