[BUG] Unhandled exception "at.forsyte.apalache.tla.lir.MalformedTlaError: Checking values of incomparable types for equality"

[shonfeder]

Description

While trying to come up with a minimal reproduction case for #914 I triggered a different unhandled exception due to comparing records with incompatible types:

PASS #12: PostTypeCheckerSnowcat                                  I@17:08:28.379
 > Running Snowcat .::.                                           I@17:08:28.379
 > Your types are great!                                          I@17:08:28.422
 > All expressions are typed                                      I@17:08:28.422
PASS #13: BoundedChecker                                          I@17:08:28.430
State 0: Checking 1 state invariants                              I@17:08:28.739
Step 0: picking a transition out of 1 transition(s)               I@17:08:28.744
State 1: Checking 1 state invariants                              I@17:08:28.753
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],at.forsyte.apalache.tla.lir.MalformedTlaError: Checking values of incomparable types for equality: Record["a" -> Int, "b" -> Record["c" -> Int]] and Record["a" -> Int, "b" -> Int])
<unknown>: unexpected TLA+ expression: Checking values of incomparable types for equality: Record["a" -> Int, "b" -> Record["c" -> Int]] and Record["a" -> Int, "b" -> Int] E@17:08:28.759
at.forsyte.apalache.tla.lir.MalformedTlaError: Checking values of incomparable types for equality: Record["a" -> Int, "b" -> Record["c" -> Int]] and Record["a" -> Int, "b" -> Int]
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:130)
	at at.forsyte.apalache.tla.bmcmt.rules.EqRule.apply(EqRule.scala:38)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:336)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:367)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:401)
	at at.forsyte.apalache.tla.bmcmt.rules.NegRule.apply(NegRule.scala:28)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:336)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:367)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:401)
	at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.assertState(TransitionExecutorImpl.scala:196)
	at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.assertState(FilteredTransitionExecutor.scala:88)
	at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.assertState(ConstrainedTransitionExecutor.scala:102)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$checkInvariants$2(SeqModelChecker.scala:267)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$checkInvariants$2$adapted(SeqModelChecker.scala:255)
	at scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:985)
	at scala.collection.immutable.List.foreach(List.scala:431)
	at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:984)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.checkInvariants(SeqModelChecker.scala:255)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$6(SeqModelChecker.scala:177)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$6$adapted(SeqModelChecker.scala:141)
	at scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:985)
	at scala.collection.immutable.List.foreach(List.scala:431)
	at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:984)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.prepareTransitionsAndCheckInvariants(SeqModelChecker.scala:141)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:63)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:51)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:131)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:98)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:22)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:37)
	at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:187)
	at at.forsyte.apalache.tla.Tool$.$anonfun$run$3(Tool.scala:95)
	at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:322)
	at at.forsyte.apalache.tla.Tool$.run(Tool.scala:95)
	at at.forsyte.apalache.tla.Tool$.main(Tool.scala:45)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)

Input specification

--------------------------- MODULE Example ---------------------------

VARIABLE
    \* @type: [a: Int, b: [ c: Int, d: Int]];
    ra,
    \* @type: [a: Int];
    rb


Init == ra = [a |-> 1] /\ rb = ra

Next ==
    rb' = [a |-> 1, b |-> 2] /\ ra' = [a |-> 1, b |-> [c |-> 2]]

Inv == ra = rb

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

The command line parameters used to run the tool

Expected behavior

Log files

System information

• Apalache version [apalache-mc version]: 0.15.12-SNAPSHOT
• OS [e.g. Ubuntu Linux or Mac OS, and the current version]: Linux system76-pc 5.11.0-7614-generic #15~1622578982~20.10~383c0a9~dev-Ubuntu SMP Wed Jun 2 00:50:39 U x86_64 x86_64 x86_64 GNU/Linux
• JDK version [e.g. OpenJDK 0.8.0]:

openjdk 11.0.11 2021-04-20
OpenJDK Runtime Environment (build 11.0.11+9-Ubuntu-0ubuntu2.20.10)
OpenJDK 64-Bit Server VM (build 11.0.11+9-Ubuntu-0ubuntu2.20.10, mixed mode, sharing)

Additional context

Ideally we'd handle this during static checking, by checking that compatible types are compared in equality tests, but at minimum we should catch the exception, and give a nicer error to users.

[shonfeder]

Looks like @konnov found the cause! #915