Type aliases not working as expected

[danwt]

Description

Type aliases do not work (intuitively).

Impact

Yes, this is blocking .

Input specification

---- MODULE main ----

EXTENDS Integers, FiniteSets, Sequences, TLC, Apalache

(*

    @typeAlias: X = Str;

*)

CONSTANTS
    \* @type: Set(X);
    XS

VARIABLES
    \* @type: Int;
    a

CInit == XS = {"k", "u", "v"}

Init == a = 42

Go == a' = 42

Next == Go

Inv == TRUE

====

The command line parameters used to run the tool

apalache typecheck main.tla

Expected behavior

It to typecheck.

Log files

15:32:22.608 [main] INFO at.forsyte.apalache.tla.tooling.opt.TypeCheckCmd - Loading configuration
# Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Output directory: /Users/danwt/Documents/work/interchain-security/x/ccv/provider/keeper/prototyping/model/_apalache-out/main.tla/2022-09-20T15-32-22_13182915876821651716
# APALACHE version: 0.29.1 | build: 146de56                       I@15:32:22.770
Type checking main.tla                                            I@15:32:22.779
PASS #0: SanyParser                                               I@15:32:22.868
Parsing file /Users/danwt/Documents/work/interchain-security/x/ccv/provider/keeper/prototyping/model/main.tla
Parsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/Integers.tla
Parsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/FiniteSets.tla
Parsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/__rewire_sequences_in_apalache.tla
Parsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/__rewire_tlc_in_apalache.tla
Parsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/Apalache.tla
Parsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/Naturals.tla
Parsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/__apalache_folds.tla
PASS #1: TypeCheckerSnowcat                                       I@15:32:23.070
 > Running Snowcat .::.                                           I@15:32:23.070
[main.tla:19:10-19:29]: Arguments to = should have the same type. For arguments XS, {"k", "u", "v"} with types Set(X), Set(Str), in expression XS = {"k", "u", "v"} E@15:32:23.371
[main.tla:19:1-19:29]: Error when computing the type of CInit     E@15:32:23.373
 > Snowcat asks you to fix the types. Meow.                       I@15:32:23.373
Type checker [FAILED]                                             I@15:32:23.374
It took me 0 days  0 hours  0 min  0 sec                          I@15:32:23.374
Total time: 0.603 sec                                             I@15:32:23.374
EXITCODE: ERROR (120)

System information

• Apalache version [apalache-mc version]: 0.29.1 | build: 146de56
• OS [e.g. Ubuntu Linux or Mac OS, and the current version]: OSX
• JDK version [e.g. OpenJDK 0.8.0]: OpenJDK 64-Bit Server VM Zulu17.30+15-CA (build 17.0.1+12-LTS, mixed mode, sharing)

Additional context

Triage checklist (for maintainers)

• [ ] Reproduce the bug on the main development branch.
• [ ] Add the issue to the apalache GitHub project.
• [ ] If the bug is high impact, ensure someone available is assigned to fix it.

[shonfeder]

The following changes produce a type correct spec:

---- MODULE main ----

EXTENDS Integers, FiniteSets, Sequences, TLC, Apalache

(*

    @typeAlias: x = Str;
*)
TypeAliases == TRUE

CONSTANTS
    \* @type: Set($x);
    XS

VARIABLES
    \* @type: Int;
    a

CInit == XS = {"k", "u", "v"}

Init == a = 42

Go == a' = 42

Next == Go

Inv == TRUE

====

The needed changes:

• the alias declaration needs to associated with an operator (or else the comment isn't preserved for us to extract the annotation).
• type aliases now have to be in camel case (so can't start with a caps)
• references to type aliases must now start with a $

These finicky details are recorded in the manual https://apalache.informal.systems/docs/adr/002adr-types.html?highlight=type%20aliase#12-type-aliases

We discussed a it with @danwt in a different context, and all agreed that better error messages would help users with this kind of thing. See #955 and #943.