Check that a file is consistently annotated with effects

[JonathanAldrich]

Right now, effects are only checked for functions that include annotations. But it is easy to intend to check for effects consistently, but leave off effects on one particular declaration in the file. This compromises soundness of effect checking.

There should be some way to indicate that effect checking is desired throughout a file. One approach is an annotation at the top. Another might be to say that if there is one annotation, then the whole file should be annotated.

Regardless, the check should make sure that every function is annotated with its effects.