Still wouldn't work, since there is no way for the compiler to distinguish between a pure function and an impure function which just don't have an annotation - e.g. a third-party library written before "impure" was introduced to the language.

If pure functions were explicitly marked as "pure" the compiler could just conservatively assume all other functions were impure. But the opposite does not work.