I think a better example is the partial functions in Haskell like head or tail. They throw an exception on empty lists. You could make it return maybe [a] or a default value, but a common usage of head might be where you know yourself that the list is non-empty. Like:

head . sort . f

where f is a function that you know returns a non-empty list, perhaps because that's just the way it operates or because you checked it further up. You know that head won't crash since any reasonable implementation of sort returns a list which is just as long as the one that was given to it. Similarly:

tail . sort . f

won't crash. Moreover, the list will still be sorted, since you just removed the head of the list.

This is all known to you, but you can't necessarily easily show it to the compiler.

I don't know the motivation for wanting to know the input before it is given. Putting it in a Maybe is the only sensible option. Some things are just not known/unknowable before running a program. You wouldn't even need to run the program if you could prove absolutely anything about the properties of a program.

Will the user input bleed through to all corners of the program? Well, why would it? You could have a sanitizing loop that refuses to pass "wrong" data to the pure (and dependently typed!) parts of the program, just looping over and over until the correct input is given.