[BUG] Checking fails when Cardinality is called on statically empty set

[Kukovec]

Input specification

---------- MODULE test ----------
EXTENDS  FiniteSets

Init == TRUE
Next == TRUE
Inv == Cardinality({}) = 0

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

The command line parameters used to run the tool

--inv=Inv --length=1

Description

Succeeds when -inv=Inv1, but BMC pass throws on -inv=Inv2:

...
PASS #13: BoundedChecker                                          I@15:46:51.144
State 0: Checking 1 state invariants                              I@15:46:51.661
Type checker error: Unexpected type VarT1                         E@15:46:51.667
at.forsyte.apalache.tla.lir.TypingException: Unexpected type VarT1
	at at.forsyte.apalache.tla.bmcmt.types.package$CellT$.fromType1(package.scala:166)
	at at.forsyte.apalache.tla.bmcmt.types.package$CellT$.fromType1(package.scala:168)
	at at.forsyte.apalache.tla.bmcmt.types.package$CellT$.fromTypeTag(package.scala:191)
	at at.forsyte.apalache.tla.bmcmt.rules.SetCtorRule.apply(SetCtorRule.scala:29)
	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.EqRule.apply(EqRule.scala:30)
	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:47)
	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)

Likely caused by the typechecker inventing a variable type for the set contents.

Expected behavior

Spec terminates with no problems OR typechecker demands annotation of empty set OR typechecker assigns arbitrary ground type to set elements.