Can't substitute concrete types like Int or Str when instantiating module.

[BGR360]

Description

When I have a module which has some CONSTANTS like:

CONSTANTS
    \* @type: Set(ID);
    Ids,
    \* @type: Set(NAME);
    Names

I expect to be able to substitute these with concrete values for model checking and/or unit tests, like so:

Ids == { 0, 1 }
Names == { "leslie", "ada" }
INSTANCE TheOtherModule

Or maybe even like so:

\* @type: Set(ID);
Ids == { 0, 1 }
\* @type: Set(NAME);
Names == { "leslie", "ada" }
INSTANCE TheOtherModule

However, it reports type checking errors, saying it expected ID but found Int, or expected NAME but found Str.

Is this a known problem? Am I doing it wrong? Can anybody point me to the part of the code where I might be able to fix this?

Impact

Not terrible, but I can't typecheck my unit test modules.

Input specification

------------------- MODULE SubstituteProblem -------------------

---------------- MODULE Interface ----------------
CONSTANTS
    \* @type: Set(ID);
    Ids,
    \* @type: Set(NAME);
    Names

\* @typeAlias: record = { id: ID, name : NAME };
Record == [ id : Ids, name : Names ]

\* @type: (ID, NAME) => $record;
MkRecord(id, name) == [ id |-> id, name |-> name ]
==================================================

Ids == { 0, 1}
Names == { "leslie", "ada" }

INSTANCE Interface

\* @type: $record;
LESLIE == MkRecord(0, "leslie")
\* @type: $record;
ADA == MkRecord(1, "ada")

================================================================

The command line parameters used to run the tool

$ apalache-mc typecheck SubstituteProblem.tla

Log files

CLI output:

> Running Snowcat .::.                                           I@17:23:28.007
[SubstituteProblem.tla:23:11-23:31]: The operator MkRecord of type ((ID, NAME) => { id: ID, name: NAME }) is applied to arguments of incompatible types in MkRecord(0, "leslie"):
Argument 0 should have type ID but has type Int.
Argument "leslie" should have type NAME but has type Str. E@17:23:28.136
[SubstituteProblem.tla:23:1-23:31]: Error when computing the type of LESLIE E@17:23:28.138

And the output when trying to annotate the concrete sets with Set(ID) or Set(NAME):

 > Running Snowcat .::.                                           I@17:31:16.307
[SubstituteProblem.tla:18:1-18:14]: Expected (() => Set(ID)) in Ids. Found: (() => Set(Int)) E@17:31:16.393
[SubstituteProblem.tla:18:1-18:14]: Error when computing the type of Ids E@17:31:16.395
 > Snowcat asks you to fix the types. Meow.                       I@17:31:16.395

System information

• Apalache version [apalache-mc version]: main built from source

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.

[Kukovec]

This is not a bug, you're using uninterpreted types, described here.
I'm guessing what you are trying to do is define type aliases, which you can read about here

[Kukovec]

The minimal-edit fix to your spec is changing the lines to

Ids == { "0_OF_ID", "1_OF_ID"}
Names == { "leslie_OF_NAME", "ada_OF_NAME" }

You might want them in this form, if you're going to be using some of the name literals explicitly:

leslie == "leslie_OF_NAME"
ada == "ada_OF_NAME" 
Names == { leslie, ada }

[BGR360]

I'm aware of type aliases, as you'll see in my example. How would they help me here?

The *_OF_* is probably the ticket.

[Kukovec]

I'm aware of type aliases, as you'll see in my example. How would they help me here?

Another alternative would have been to define ID as an alias (e.g. $id), then use

CONSTANT
\* @type: Set($id);
    Ids,
...
\* @typeAlias: id = Int;
Ids == { 0, 1}

[Kukovec]

The downside would be that the inner module would cease to be type-checkable in a vacuum. Uninterpreted literals are the better solution, IMO.

[konnov]

I'm aware of type aliases, as you'll see in my example. How would they help me here?

The *_OF_* is probably the ticket.

Just to give you a bit more context. The string literals of the form "identifier_OF_TYPENAME" have a special treatment in the type checker. Such a string is understood as a value called "identifier" of the uninterpreted type "TYPENAME". All other string literals are automatically assigned the string type, that is, "Str". So in your example, the types are declared as uninterpreted, that is, NAME and ID, whereas the literals are "leslie", "ada", 0, and 1, which are treated as strings and integers by the type checker.

Hence, the type checker behaves as expected. It may be confusing, since we also changed the notation for uninterpreted types and values, before we found this relatively simple solution.

Although it is not a bug, it is an interesting discussion. I will convert it to a discussion.