Feature FTC: type checker Snowcat

[konnov]

This is a meta-issue that summarizes the work to be done to make the type checker a fully-functional feature. All issues for this feature are labelled with FTC-Snowcat.

The user annotates some variable and operator declarations as specified in ADR002. The type checker either infers the types of all expressions and declarations in the specification or points to a type error.

• java-like annotations in the comments, [FEATURE] Parse annotations from the SANY comments #226 and [FEATURE] Extend operator declarations with annotations #262
• integrate java-like annotations in the type checker, [FEATURE] Integrate in-comment annotations in the type checker #504
• introduce type tags in TLA expressions, Implicit type tag in TLA expressions (cherry-picked) #561
• integrate with the model checker, [FEATURE] Integrate the type checker Snowcat into the model checker #521: PRs step+2 to #521 #641, One more step to #521 #632, Recover types from the type checker #618, Integrating types 3: Refactored tla.lir.Builder and made several passes type-aware #650, Integrating types 5: made Inliner, Unroller, and ParameterNormalizer type-aware #657, Integrating types 6: made Desugarer type aware #658, Integrating types 7: victory over enthropy #663, Integrating types 8: using new types in the checker core #668
• update the manual, [FEATURE] Update the manual on Snowcat #688
• add types to the language manual, [FEATURE] Add types to the standard operators in the language manual #547
• write a tutorial, [FEATURE] Write a tutorial on Snowcat #689
• integrate TLC configs, [FEATURE] Typechecker should be able to read TLC configs #520
• fix numerous bug reports
• memo on the type checker, [FEATURE] Prepare a memo on how the type checker is working #905
• fix instantiation of user-defined operators [BUG] Type variables are not instantiated during type-checking  #869, [BUG] Snowcat doesn't infer a type from equality #864, [FEATURE] Fix operator inlining to support polymorphism #953
• improve the expression builder framework
  • its own milestone: Typed builder
• precise type checking for records: Meta-issue: variants and precise record types #401, [FEATURE] Write an ADR about an extension of Type System 1 #1151, closes #1151: ADR-014 on precise type inference for records and variants #1170
• introduce a few missing features: [FEATURE] Add support for different uninterpreted types in Rewriter #570, [FEATURE] Translate FunAsSeq in the model checker #569
• change the syntax for type aliases: Change the syntax for type aliases #1843

[konnov]

Since most of the planned work has been done, I am closing this meta-issue. A few left-overs can be found in the milestone 48. These issues do not require a lot of active work. Rather they have to be done at proper time. Also, unpinning this issue.