I don't really understand that statement but it makes me really curious. Can you expand it a bit? (Background: I can read Haskell but I have only a vague idea of dependent types.)
This lets us specify very precise types; commonly-used examples are "Fin n", a type which contains "n" members (ie. "Fin 2" ~= Bool); and "Vect n t", which is a list of exactly "n" elements of type "t" (ie. "Vect 2 t" ~= (t, t)).
This extra precision comes at the price of verbosity, but it forces us to use our code in correct ways. For example, Haskell's "!!" function looks up elements in lists. Its arguments are of type [a] and Int, so we can easily end up with an Int that's bigger than the list (or even negative!). If we use "Fin n" and "Vect n a" instead, we're guaranteed that there will be an element at that position; otherwise we get a compile error.
We can do this with any pure value, and in fact there is a feature called "type providers" which use IO to generate types (eg. reading in database schemas).
One limitation with type-systems is that they can be easily fooled by infinite loops, for example:
loop :: a
loop = loop
To prevent this, most dependently-typed languages don't allow infinite loops, at least at compile-time. Hence we can't write any old value. There are various ways to achieve this (syntactically-guarded recursion, structural recursion, termination proofs, co-recursion, etc.) but a good rule of thumb is that if we can implement something using "fold" then we can use it in our types.
If you're unfamiliar with "fold", see http://jeremykun.com/2013/09/30/the-universal-properties-of-...
One way to limit the completeness of a language is to replace fixed-point recursion (as is embodied in the Y combinator and all recursive languages which are complete) by induction/coinduction. These two concepts "divide general recursion in half" such that you can get a lot of work done without actually having completeness/inconsistency.
Haskell for instance has induction via folds and coinduction via unfolds, but since we're allowed to "cross the streams" in folds and unfolds you end up with general recursion and inconsistency.
Coq disallows stream crossing.
Epic. Coq is the Dr. Egon Spengler of programming languages.
Structural recursion (folds) is to general recursion (let rec) as the "for" loop is to the "while" loop.
So, they are strictly equivalent? </Clanguage>