The compiler alone cannot do this, but the compiler combined with judicious use of the type system can. This is really the big value-add of Haskell/ML-style typ

The compiler alone cannot do this, but the compiler combined with judicious use of the type system can. This is really the big value-add of Haskell/ML-style type systems; you can fit so many useful constraints into the type system that you can enlist the compiler into proving that you haven't made various common mistakes. If you can formalize an application logic error into a type error, you can use the compiler to enforce a wide variety of application logic error checking at compile time. A simple example: suppose that every web form input is mapped into an "UnsafeUserInput rawtype" (that is, an algebraic data type parametrized over the raw input type). By simply ensuring that your output code only works on "SanitizedUserInput" types, you enforce that at some point in the code you apply a sanitization function to any unsafe input. Now the compiler is working for you, checking that your overall data flow respects the constraints you've encoded into the type system. In this style of programming, the type system becomes a way of encoding your desired integrity constraints inline with the functions and data types rather than outside the application logic in test suites.