> "Write a program to sort the words you find in the input file"

That's as trivial to write in a dependently typed language as it is in, say, Python (leaving aside the fact that you don't like monads), e.g. Idris:

  main : IO ()
  main = do
    Right contents <- readFile "myfile.txt"
    let theLines = lines contents
    let sorted = sort theLines
    -- do something with sorted

Of course, that doesn't use any dependent types, but nobody says that you have to use dependent types for a program so trivial you're unlikely to screw anything up.

(And also: the standard library could have instead defined the functions "lines" such that it does use a dependent type. In that case, almost nothing about the program would change, except you would now write "let (n * theLines)" because the length is now part of the return value.)

Dependent types are for where it makes sense to encode invariants, e.g.

  matMult : Matrix k m -> Matrix m n -> Matrix k n

And of course, that function works for matrices of arbitrary dimensions, so the argument "we can't know the size of the matrices at compile time" doesn't apply.

People have been giving you counter examples left and right while you keep it abstract and non-concrete. Why not just provide simple examples that show what you mean? Stomping your feet and calling other people maniacs is not really a great look.