Just like Haskell types can depend on other types, like "Maybe Int" (which contains an Int or "Nothing") or "Either String Bool" (which contains a String or a Bool), dependent types can depend on any value.
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
This type-checks in Haskell, but it has a completely-general type: we can use it
anywhere without the type-checker complaining. This undermines our confidence: we might
think we understand what some code will do, based on its type, but the author may have been lazy and just written "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-...