Add a dynamic cast in Typing

[konnov]

There is at least one idiom that cannot be solved by the type system. Sometimes, a function Int -> Int can be transformed into a sequence. For instance, here is the piece of code from Queens:

IsSolution(queens) ==
  \A i \in 1 .. Len(queens)-1 : \A j \in i+1 .. Len(queens) : 
       ~ Attacks(queens,i,j)

Solutions == { queens \in [1..N -> 1..N] : IsSolution(queens) }

The operator IsSolution needs a sequence, whereas the operator Solutions produces a set of functions from integers to integers. This is not an issue in the untyped semantics of TLA+. However, I do not see a way for a sound transformation of a function into a sequence without an additional test in runtime (e.g., when doing model checking).

We should introduce an operator that allows the user to perform such a transformation in "runtime". In this case, the operator would be called like follows:

Solutions == { queens \in [1..N -> 1..N] : IsSolution(DynCast(queens, "Seq(Int)")) }

Both the type checker and type inferer should check, whether the transformation makes sense, e.g., Int should not be transformed into Set(Int). A concrete implementation of the casting will be left to the implementation,
e.g., the model checker.