[BUG] Incorrect parsing on global module and INSTANCE name collision

[Kukovec]

Describe the bug
The spec Paxos.tla defines both a nullary operator votes and an instance V of Voting (defined in Voting.tla).
The spec Voting.tla uses a VARIABLE votes and an operator

Spec == Init /\ [][Next]_<<votes, maxBal>>

In the pass immediately after parsing, the internal representation of V!Spec is read as

V!Init() ∧ []([V!Next()]_(<<votes(), maxBal>>))

where votes() is an operator application (to the locally defined nullary votes) instead of a variable.

To Reproduce
Steps to reproduce the behavior:

• The command-line parameters that you use to run the tool :
  check --length=10 --debug --inv=Inv <dir>/Paxos.tla
• The problematic specification (if this cannot be submitted, try to come up with a minimal working example):
  https://github.com/tlaplus/Examples/tree/master/specifications/Paxos

Expected behavior
What did you expect to see?
V!Spec as

V!Init() ∧ []([V!Next()]_(<<V!votes, V!maxBal>>))

or similar.

[konnov]

This is a rare bug, postponing for the next milestone

[konnov]

The issue boils down to the following example:

------------------- MODULE P ----------------------                             
------------------- MODULE Vot ----------------------
------------------- MODULE Cons -------------------
VARIABLE chosen
Init == chosen = {}
Next == chosen = {2}
===================================================
chosen == {1}
C == INSTANCE Cons
===================================================
V == INSTANCE Vot
===================================================

SanyImporter fails to resolve chosen in the module Cons, as it is pointing to the operator V!Chosen. We should fix the code that performs substitution.