Annotations with multiline LET-INs

[konnov]

Following the bug report in #1946, type annotations in multiple-line LET-IN definitions do not work:

---- MODULE Apalache_M0 ----

EXTENDS Naturals, FiniteSets

\* @type: (Set(a), Set(b)) => Set(a -> b);
FSets(D, R) ==
    LET
        \* @type: Int -> Set(a -> b);
        F[n \in 0..Cardinality(D)] ==
            IF n = 0
            THEN {<<>>}
            ELSE
                LET
                    \* @type: Set(a -> b);
                    F0 == F[n - 1]
                    \* All functions in F0 have the same domain, choose any one
                    \* @type: a -> b;
                    f0 == CHOOSE f \in F0 : TRUE
                    \* @type: Set(a);
                    D_smaller == DOMAIN f0
                    \* @type: a;
                    d1 == CHOOSE d \in (D \ D_smaller) : TRUE
                    \* @type: Set(a);
                    D_bigger == D_smaller \union {d1}
                IN
                    {
                        [d \in D_bigger |-> IF d \in DOMAIN f THEN f[d] ELSE r]
                        : f \in F0, r \in R
                    }
    IN
        F[Cardinality(D)]

ASSUME 
    \A d \in SUBSET (0..3) :
    \A r \in SUBSET (4..5) :
        [d -> r] = FSets(d, r)

====

We should figure out, whether this problem arises from SANY, or we translate the SANY representation incorrectly.

[konnov]

For the multiline LET-IN definitions, there is an easy workaround, e.g., we can rewrite the above example as:

                LET \* @type: Set(a -> b);
                    F0 == F[n - 1]
                IN
                LET   \* @type: a -> b;
                    f0 == CHOOSE f \in F0 : TRUE
                IN
                LET    \* @type: Set(a);
                    D_smaller == DOMAIN f0
                IN
                LET \* @type: a;
                    d1 == CHOOSE d \in (D \ D_smaller) : TRUE
                IN
                LET \* @type: Set(a);
                    D_bigger == D_smaller \union {d1}
                IN
...