First argument of Variant must be a string, found: A()

[lemmy]

Description:
When working with variant types, it's easy to introduce typos in variant string values (It took me a while to understand Apalache's error message because it used "AE" to refer to an AppendEntries message, instead of the expected "A"). To prevent these errors, one might want to extract these variant strings into "enums". Unfortunately, Apalache fails to handle cases where variant strings are extracted into an enum: Typing input error: The first argument of Variant must be a string, found: A() (see error below):

------ MODULE VariantTypo ------
EXTENDS Variants, Integers

\* @typeAlias: message = A({foo: Int});
typedefs == TRUE

A == "A"

VARIABLE
    \* @type: Set($message);
    msgs

Init ==
    \E As \in SUBSET [ foo: Int ] :
        msgs = { Variant(A, a) : a \in As }

Next ==
    \E msg \in msgs:
        /\ VariantTag(msg) = A
        /\ LET a == VariantGetUnsafe(A, msg)
           IN  msgs' = msgs \cup { Variant(A, [foo|-> a.foo + 1]) }

======

-> % ~/apalache/apalache-0.47.0/bin/apalache-mc typecheck VariantTypo.tla
Output directory: VariantTypo.tla/2024-11-12T10-08-39_14294268185456317134
# APALACHE version: 0.47.0 | build: 2c576d8                       I@10:14:46.725
Type checking VariantTypo.tla                                     I@10:14:46.736
PASS #0: SanyParser                                               I@10:14:46.843
Parsing file /Users/markus/src/TLA/_specs/MSFT/pirateship-tla/VariantTypo.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Variants.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Integers.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Naturals.tla
PASS #1: TypeCheckerSnowcat                                       I@10:14:47.007
 > Running Snowcat .::.                                           I@10:14:47.007
Typing input error: The first argument of Variant must be a string, found: A() E@10:14:47.079
It took me 0 days  0 hours  0 min  0 sec                          I@10:14:47.079
Total time: 0.351 sec                                             I@10:14:47.080
EXITCODE: ERROR (255)