Predicates/ghost functions for higher-order annotations

[levjj]

There is already adhoc support for higher-order annotations by using spec with verification-only functions. However, this should become a core langauge feature to provide better support for parametric polymorphism, etc.