Well, yes and no. You can prove all the properties liquid types can without actually using liquid types, just by running the algorithms that infer them. Either way (inferring with or without types) the problem of indexing is undecidable, and cannot be verified in the general case (but it can in many common usages).
The point to using types is that they make static analyses more compositional. Types enforce invariants across module boundaries, without requiring the entire program to be checked in a single pass.
Yes, but they may also lose information in the process... As usual, it's a tradeoff.