Special treatment of type annotations in type-checking mode.

In the current approach to Rank-N types, when we leave the scope of some type variable, we disallow it to occur in all types that will be substituted for unification variables. While this restriction is reasonable from the point of view of both predictability and simplicity of the implementation, a naive treatment of type annotations may lead to some errors, when the programmer omits some parts of the annotation, because it is used in type-checking mode. For this reason, we removed test `test/ok/ok0037_checkScheme.fram` from the test suite. However, in type-checking mode we can have a special function for checking type-annotations, and allow them to provide some information complementary to the one known from the context.