[FEATURE] Add TLA expression generator with well-typed output

[thpani]

The current IrGenerators produces TLA+ expressions with arbitrary type annotations. This produces errors in property-based testing such as #1364.

Filtering the current (sometimes ill-typed) expressions through the typechecker is probably too expensive.

Fix IrGenerators to produce only well-typed expressions or add an additional generator doing so.

• [ ] Introduce well-typed generators
• [ ] Remove "catch all"s (e.g., for MalformedTlaError) in PBT

[konnov]

I see a value in producing both ill-typed and well-typed expressions. So we could introduce an additional parameter to all generators that requires an expression to be well-typed.

On the first glance, it does not look hard to generate well-type expressions. We have to generate a type with TlaType1Gen and then inductively follow it. Surely, we have to break down all operators into 9-10 categories, which specify the choice of the type constructor in TlaType1.