Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]

[lemmy]

https://apalache-mc.org/docs/adr/006rfc-unit-testing.html?highlight=gen(#51-using-apalache-generators advises to conjoin TypeOK to the predicate involving the Gen operator.

---- MODULE Foobar ----
EXTENDS Apalache, Integers

VARIABLE
    \* @type: { p : Set({ q : Set(Int) }) };
    v

TypeOK ==
    v \in [ p: SUBSET [ q: SUBSET Int ] ]   \* Infinite sets such as Int trigger the error.

Init ==
    /\ v = [ p |-> {[ q |-> { 1 } ]} ]
    /\ TypeOK    \* Conjoining  TypeOK  triggers the error.

GenInit ==
    /\ v = Gen(1)
    /\ TypeOK    \* Conjoining  TypeOK  triggers the error.

Next ==
    UNCHANGED v

====

Init

-> % ~/apalache/apalache-0.45.3/bin/apalache-mc check --init=Init --next=Next Foobar.tla
17:37:44.762 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- Loading configuration
17:37:44.787 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd --   > TLC config file found in specification directory. To enable it, pass --config=Foobar.cfg.
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Output directory: /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/Foobar.tla/2024-08-27T17-37-44_41841269002290680
# APALACHE version: 0.45.3 | build: 0b3ae56                       I@17:37:44.978
Tuning: search.outputTraces=false                                 I@17:37:45.006
PASS #0: SanyParser                                               I@17:37:45.146
Parsing file /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/Foobar.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Apalache.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Integers.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Naturals.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__rewire_sequences_in_apalache.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__apalache_folds.tla
PASS #1: TypeCheckerSnowcat                                       I@17:37:45.331
 > Running Snowcat .::.                                           I@17:37:45.331
 > Your types are purrfect!                                       I@17:37:45.501
 > All expressions are typed                                      I@17:37:45.501
PASS #2: ConfigurationPass                                        I@17:37:45.501
  > Set the initialization predicate to Init                      I@17:37:45.503
  > Set the transition predicate to Next                          I@17:37:45.503
PASS #3: DesugarerPass                                            I@17:37:45.505
  > Desugaring...                                                 I@17:37:45.505
PASS #4: InlinePass                                               I@17:37:45.516
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next I@17:37:45.516
PASS #5: TemporalPass                                             I@17:37:45.530
  > Rewriting temporal operators...                               I@17:37:45.530
  > No temporal property specified, nothing to encode             I@17:37:45.530
PASS #6: InlinePass                                               I@17:37:45.530
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next I@17:37:45.530
PASS #7: PrimingPass                                              I@17:37:45.531
  > Introducing InitPrimed for Init'                              I@17:37:45.532
PASS #8: VCGen                                                    I@17:37:45.672
  > No invariant given. Only deadlocks will be checked            I@17:37:45.672
PASS #9: PreprocessingPass                                        I@17:37:45.672
  > Before preprocessing: unique renaming                         I@17:37:45.672
 > Applying standard transformations:                             I@17:37:45.677
  > PrimePropagation                                              I@17:37:45.677
  > Desugarer                                                     I@17:37:45.678
  > UniqueRenamer                                                 I@17:37:45.678
  > Normalizer                                                    I@17:37:45.679
  > Keramelizer                                                   I@17:37:45.680
  > After preprocessing: UniqueRenamer                            I@17:37:45.683
PASS #10: TransitionFinderPass                                    I@17:37:45.686
  > Found 1 initializing transitions                              I@17:37:45.695
  > Found 1 transitions                                           I@17:37:45.695
  > No constant initializer                                       I@17:37:45.695
  > Applying unique renaming                                      I@17:37:45.696
PASS #11: OptimizationPass                                        I@17:37:45.697
 > Applying optimizations:                                        I@17:37:45.701
  > ConstSimplifier                                               I@17:37:45.702
  > ExprOptimizer                                                 I@17:37:45.702
  > SetMembershipSimplifier                                       I@17:37:45.704
  > ConstSimplifier                                               I@17:37:45.704
PASS #12: AnalysisPass                                            I@17:37:45.705
 > Marking skolemizable existentials and sets to be expanded...   I@17:37:45.706
  > Skolemization                                                 I@17:37:45.707
  > Expansion                                                     I@17:37:45.707
  > Remove unused let-in defs                                     I@17:37:45.707
 > Running analyzers...                                           I@17:37:45.709
  > Introduced expression grades                                  I@17:37:45.710
PASS #13: BoundedChecker                                          I@17:37:45.710
<unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)] E@17:37:46.491
at.forsyte.apalache.infra.AdaptedException: <unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
        at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:39)
        at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:135)
        at at.forsyte.apalache.tla.Tool$.runCommand(Tool.scala:138)
        at at.forsyte.apalache.tla.Tool$.run(Tool.scala:118)
        at at.forsyte.apalache.tla.Tool$.main(Tool.scala:40)
        at at.forsyte.apalache.tla.Tool.main(Tool.scala)
Please report an issue at [https://github.com/informalsystems/apalache/issues]: at.forsyte.apalache.infra.AdaptedException: <unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
A bug report template has been generated at [/Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/Foobar.tla/2024-08-27T17-37-44_41841269002290680/BugReport.md].
If you choose to use it, please complete the template with a description of the expected behavior and impact.
It took me 0 days  0 hours  0 min  1 sec                          I@17:37:46.496
Total time: 1.504 sec                                             I@17:37:46.496
EXITCODE: ERROR (255)

GenInit

-> % ~/apalache/apalache-0.45.3/bin/apalache-mc check --init=GenInit --next=Next Foobar.tla
17:38:42.548 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- Loading configuration
17:38:42.573 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd --   > TLC config file found in specification directory. To enable it, pass --config=Foobar.cfg.
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Output directory: /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/Foobar.tla/2024-08-27T17-38-42_12136351957546524448
# APALACHE version: 0.45.3 | build: 0b3ae56                       I@17:38:42.761
Tuning: search.outputTraces=false                                 I@17:38:42.781
PASS #0: SanyParser                                               I@17:38:42.913
Parsing file /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/Foobar.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Apalache.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Integers.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Naturals.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__rewire_sequences_in_apalache.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__apalache_folds.tla
PASS #1: TypeCheckerSnowcat                                       I@17:38:43.099
 > Running Snowcat .::.                                           I@17:38:43.099
 > Your types are purrfect!                                       I@17:38:43.260
 > All expressions are typed                                      I@17:38:43.260
PASS #2: ConfigurationPass                                        I@17:38:43.261
  > Set the initialization predicate to GenInit                   I@17:38:43.262
  > Set the transition predicate to Next                          I@17:38:43.263
PASS #3: DesugarerPass                                            I@17:38:43.265
  > Desugaring...                                                 I@17:38:43.265
PASS #4: InlinePass                                               I@17:38:43.273
Leaving only relevant operators: CInitPrimed, GenInit, GenInitPrimed, Next I@17:38:43.273
PASS #5: TemporalPass                                             I@17:38:43.289
  > Rewriting temporal operators...                               I@17:38:43.290
  > No temporal property specified, nothing to encode             I@17:38:43.290
PASS #6: InlinePass                                               I@17:38:43.290
Leaving only relevant operators: CInitPrimed, GenInit, GenInitPrimed, Next I@17:38:43.290
PASS #7: PrimingPass                                              I@17:38:43.291
  > Introducing GenInitPrimed for GenInit'                        I@17:38:43.292
PASS #8: VCGen                                                    I@17:38:43.434
  > No invariant given. Only deadlocks will be checked            I@17:38:43.434
PASS #9: PreprocessingPass                                        I@17:38:43.434
  > Before preprocessing: unique renaming                         I@17:38:43.434
 > Applying standard transformations:                             I@17:38:43.438
  > PrimePropagation                                              I@17:38:43.439
  > Desugarer                                                     I@17:38:43.439
  > UniqueRenamer                                                 I@17:38:43.439
  > Normalizer                                                    I@17:38:43.440
  > Keramelizer                                                   I@17:38:43.441
  > After preprocessing: UniqueRenamer                            I@17:38:43.443
PASS #10: TransitionFinderPass                                    I@17:38:43.446
  > Found 1 initializing transitions                              I@17:38:43.454
  > Found 1 transitions                                           I@17:38:43.454
  > No constant initializer                                       I@17:38:43.455
  > Applying unique renaming                                      I@17:38:43.455
PASS #11: OptimizationPass                                        I@17:38:43.456
 > Applying optimizations:                                        I@17:38:43.461
  > ConstSimplifier                                               I@17:38:43.461
  > ExprOptimizer                                                 I@17:38:43.462
  > SetMembershipSimplifier                                       I@17:38:43.463
  > ConstSimplifier                                               I@17:38:43.464
PASS #12: AnalysisPass                                            I@17:38:43.464
 > Marking skolemizable existentials and sets to be expanded...   I@17:38:43.466
  > Skolemization                                                 I@17:38:43.466
  > Expansion                                                     I@17:38:43.466
  > Remove unused let-in defs                                     I@17:38:43.467
 > Running analyzers...                                           I@17:38:43.468
  > Introduced expression grades                                  I@17:38:43.469
PASS #13: BoundedChecker                                          I@17:38:43.469
<unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)] E@17:38:44.247
at.forsyte.apalache.infra.AdaptedException: <unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
        at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:39)
        at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:135)
        at at.forsyte.apalache.tla.Tool$.runCommand(Tool.scala:138)
        at at.forsyte.apalache.tla.Tool$.run(Tool.scala:118)
        at at.forsyte.apalache.tla.Tool$.main(Tool.scala:40)
        at at.forsyte.apalache.tla.Tool.main(Tool.scala)
Please report an issue at [https://github.com/informalsystems/apalache/issues]: at.forsyte.apalache.infra.AdaptedException: <unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
A bug report template has been generated at [/Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/Foobar.tla/2024-08-27T17-38-42_12136351957546524448/BugReport.md].
If you choose to use it, please complete the template with a description of the expected behavior and impact.
It took me 0 days  0 hours  0 min  1 sec                          I@17:38:44.252
Total time: 1.486 sec                                             I@17:38:44.252
EXITCODE: ERROR (255)

Exception

at.forsyte.apalache.tla.bmcmt.CheckerException: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:171)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.fieldsEq\$1(LazyEquality.scala:532)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.\$anonfun\$mkRowRecordEq\$1(LazyEquality.scala:536)
	at scala.collection.StrictOptimizedIterableOps.map(StrictOptimizedIterableOps.scala:100)
	at scala.collection.StrictOptimizedIterableOps.map\$(StrictOptimizedIterableOps.scala:87)
	at scala.collection.immutable.TreeSet.map(TreeSet.scala:39)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.mkRowRecordEq(LazyEquality.scala:536)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:155)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.makeOne\$1(LazyEquality.scala:107)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.\$anonfun\$cacheEqConstraints\$2(LazyEquality.scala:110)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
	at scala.collection.LinearSeqOps.foldLeft\$(LinearSeq.scala:179)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheEqConstraints(LazyEquality.scala:110)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.subsetEq(LazyEquality.scala:318)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.mkSetEq(LazyEquality.scala:247)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:145)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.fieldsEq\$1(LazyEquality.scala:532)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.\$anonfun\$mkRowRecordEq\$1(LazyEquality.scala:536)
	at scala.collection.StrictOptimizedIterableOps.map(StrictOptimizedIterableOps.scala:100)
	at scala.collection.StrictOptimizedIterableOps.map\$(StrictOptimizedIterableOps.scala:87)
	at scala.collection.immutable.TreeSet.map(TreeSet.scala:39)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.mkRowRecordEq(LazyEquality.scala:536)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:155)
	at at.forsyte.apalache.tla.bmcmt.rules.EqRule.apply(EqRule.scala:55)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.skolemExistsByPick(QuantRule.scala:300)
	at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.apply(QuantRule.scala:53)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.mapArg\$1(AndRule.scala:62)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.\$anonfun\$apply\$2(AndRule.scala:66)
	at scala.collection.immutable.List.map(List.scala:251)
	at scala.collection.immutable.List.map(List.scala:79)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.apply(AndRule.scala:66)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.prepareTransition(TransitionExecutorImpl.scala:107)
	at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.prepareTransition(FilteredTransitionExecutor.scala:48)
	at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.prepareTransition(ConstrainedTransitionExecutor.scala:98)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.\$anonfun\$prepareTransitionsAndCheckInvariants\$5(SeqModelChecker.scala:217)
	at scala.runtime.java8.JFunction1\$mcVI\$sp.apply(JFunction1\$mcVI\$sp.scala:18)
	at scala.collection.immutable.Range.foreach(Range.scala:190)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.prepareTransitionsAndCheckInvariants(SeqModelChecker.scala:211)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:123)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:62)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:128)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:81)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.exec(PassChainExecutor.scala:64)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$3(PassChainExecutor.scala:53)
	at scala.util.Either.flatMap(Either.scala:360)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$1(PassChainExecutor.scala:51)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
	at scala.collection.LinearSeqOps.foldLeft\$(LinearSeq.scala:179)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.runOnPasses(PassChainExecutor.scala:44)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:34)
	at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:135)
	at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:138)
	at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:118)
	at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)