[BUG] Typecheck fails on tuples in quantifiers

[konnov]

Though we have fixed the issue #476 in the model checker, it is surfacing in the type checker. See test/tla/ExistTuple476.tla:

------------------ MODULE ExistTuple476 ----------------------
(* A regression test for the issue:
   /~https://github.com/informalsystems/apalache/issues/476
 *)
EXTENDS Integers

VARIABLES x, y

Init ==
    x = 0 /\ y = 0

Next ==
    \E <<i, j>> \in (1..2) \X (3..4):
        /\ x' = i
        /\ y' = j
==============================================================

[konnov]

Once #531 is there, we have to add Desugarer as a preprocessing pass to the type checker.

[konnov]

In the end, we will not use Desugarer as a preprocessing pass for the typechecker. It makes type information less precise. ToEtcExpr already has the code to deal with tuples in set comprehensions and function constructors. Quantifiers is just a missing case here.

[shonfeder]

Let's wait to close issues until the PR that fixes them is actually merged going forward. Github will take care of this for us, if the PR includes the phrase closes #nnn, and this will ensure that fixes are actually in before we say they are resolved. This is useful for users and for our own tracking.