> Can a dependent type system catch all type errors at compile time?

I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

> because the value of getKeyboardInput could be anything

That makes my brain hurt. I think implicitly narrowing the type is stylistically better. Maybe just adding a dependent type declaration:

    x = (parseInt(getKey) :: Int(>=0, <=10))

Then you type-annotate everything you can, marking every non-annotated expression as wild:

    w = ... :: Int(>=0, <=10)
    x = ... :: Int(>=0, <=2)
    z :: Int(>=0, <=20)
    y = w * x                 -- :: Wild
    z = y                     -- compiler should Scream!

Asking the compiler to infer arbitrary type declarations seems hard. I think y probably shouldn't be inferred as :: Int(0<=..<=20) unless there is a rule somewhere that Int(a<=..<=b) * Int(c<=..<=d) = .. :: Int(f<=..<=g).

The work still needs to be done (no magic bullet here), but we should be able to use the computer to generate well-defined type combinations.