Name clash leads to operator being incorrectly marked as recursive

[fan-tom]

Description

$ apalache-mc check  --inv=Inv mod.tla
22:32:44.075 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- 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/alexey/dev/private/tlaplus/apalache/_apalache-out/mod.tla/2024-02-04T22-32-44_2136058718945860754
# APALACHE version: v0.44.3-9-g9fe802934 | build: v0.44.3-9-g9fe802934 I@22:32:44.504
Tuning: search.outputTraces=false                                 I@22:32:44.535
PASS #0: SanyParser                                               I@22:32:44.819
Parsing file /Users/alexey/dev/private/tlaplus/apalache/mod.tla
WORKAROUND #130: labelling operator i as recursive, though SANY did not tell us so. W@22:32:45.064
PASS #1: TypeCheckerSnowcat                                       I@22:32:45.090
 > Running Snowcat .::.                                           I@22:32:45.090
 > Your types are purrfect!                                       I@22:32:45.254
 > All expressions are typed                                      I@22:32:45.255
PASS #2: ConfigurationPass                                        I@22:32:45.256
<unknown>: unexpected expression: RECURSIVE i(). Apalache does not support recursive operators. E@22:32:45.269
Unexpected expressions in the specification (see the error messages) E@22:32:45.270
It took me 0 days  0 hours  0 min  0 sec                          I@22:32:45.270
Total time: 0.764 sec                                             I@22:32:45.270
EXITCODE: ERROR (255)

The issue is that in MyOp we intoduce an operator i and in its definition we introduce a variable of the same name i, so at.forsyte.apalache.tla.imp.ModuleTranslator#workaroundMarkRecursive decides that it is a recursive operator (and prints this warning WORKAROUND #130: labelling operator i as recursive, though SANY did not tell us so. W@22:32:45.064), while in reality these two identifers are not related to each other.

Impact

Workaround exists: rewrite MyOp as MyOp == LET k == CHOOSE i \in {}: TRUE IN TRUE and erorr is gone.

Input specification

-------------------------- MODULE mod --------------------------
VARIABLES
    \* @type: Set(Bool);
    vars

MyOp == LET i == CHOOSE i \in {}: TRUE IN TRUE

Init == vars = {}

Next == MyOp /\ UNCHANGED vars

Spec == /\ Init /\ [][Next]_vars

Inv == TRUE
=====================================================================

The command line parameters used to run the tool

check --inv=Inv mod.tla

Expected behavior

Apalache doesn't produce an error <unknown>: unexpected expression: RECURSIVE i(). Apalache does not support recursive operators. E@22:32:45.269

Log files

System information

• Apalache version [apalache-mc version]: locally built on commit 0549ef7b
• OS [e.g. Ubuntu Linux or Mac OS, and the current version]: irrelevant
• JDK version [e.g. OpenJDK 0.8.0]: irrelevant

Additional context

TLC doesn't report any error in this case

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.

[fan-tom]

Though a workaround exists, in a big specification with lots of short-living variables, usually named the same, it is not obvious which operator we are referring here, as there is no user-defined operator with this name and there is no source location in the error message

[shonfeder]

Interesting behavior here. Thank you for the report!

Maybe a good start here would be to figure out the intention behind at.forsyte.apalache.tla.imp.ModuleTranslator#workaroundMarkRecursive and whether there are any cases where we actually need it, just in case the fix here could be as simple as getting rid of that check.

[fan-tom]

Comment says it is a workaround for this issue #130, which is caused by a bug in SANY, but there is no link to this SANY bug to understand whether we still need it