Fix typing for quint empty sets (#2466)

The converter for quint empty types was constructing types wrapped in a
Set. This fixes that error, and expands the test to check for this.

Going forward, I write the quint integration while I expand the
converter to catch this earlier.

.unreleased/bug-fixes/quint-empty-sets.md

@@ -0,0 +1 @@
+Fix the typing of quint empty sets during conversion (see #2466)

tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala

@@ -201,6 +201,21 @@ class Quint(moduleData: QuintOutput) {
         case tooManyArgs => throwOperatorArityError(op, "binary", tooManyArgs)
       }
 
+    private def setEnumeration(id: Int): Seq[QuintEx] => TBuilderInstruction = {
+      variadicApp {
+        // Empty sets must be handled specially since we cannot infer their type
+        // from the given arguments
+        case Seq() =>
+          val elementType = types(id).typ match {
+            case QuintSetT(t) => Quint.typeToTlaType(t)
+            case invalidType =>
+              throw new QuintIRParseError(s"Set with id ${id} has invalid type ${invalidType}")
+          }
+          tla.emptySet(elementType)
+        case args => tla.enumSet(args: _*)
+      }
+    }
+
     private val tlaApplication: QuintApp => TBuilderInstruction = { case QuintApp(id, opName, quintArgs) =>
       val applicationBuilder: Seq[QuintEx] => TBuilderInstruction = opName match {
         // First we check for application of builtin operators
@@ -228,13 +243,7 @@ class Quint(moduleData: QuintOutput) {
         case "iuminus" => unaryApp(opName, tla.uminus)
 
         // Sets
-        case "Set" =>
-          variadicApp {
-            // Empty sets must be handled specially since we cannot infer their type
-            // from the given arguments
-            case Seq() => tla.emptySet(Quint.typeToTlaType(types(id).typ))
-            case args  => tla.enumSet(args: _*)
-          }
+        case "Set"       => setEnumeration(id)
         case "exists"    => binaryBindingApp(opName, tla.exists)
         case "forall"    => binaryBindingApp(opName, tla.forall)
         case "in"        => binaryApp(opName, tla.in)

tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala

@@ -6,6 +6,9 @@ import org.scalatestplus.junit.JUnitRunner
 
 import QuintType._
 import QuintEx._
+import at.forsyte.apalache.tla.lir.Typed
+import at.forsyte.apalache.tla.lir.SetT1
+import at.forsyte.apalache.tla.lir.IntT1
 
 /**
  * Tests the conversion of quint expressions and declarations into TLA expressions
@@ -206,7 +209,13 @@ class TestQuintEx extends AnyFunSuite {
   }
 
   test("can convert builtin Set operator application for empty sets") {
-    assert(convert(Q.emptyIntSet) == """{}""")
+    val tlaEx = quint.exToTla(Q.emptyIntSet).get
+    // Ensure the constructed empty set has the required type
+    assert(tlaEx.typeTag match {
+      case Typed(SetT1(IntT1)) => true
+      case _                   => false
+    })
+    assert(tlaEx.toString() == """{}""")
   }
   test("can convert builtin exists operator application") {
     assert(convert(Q.app("exists", Q.intSet, Q.intIsGreaterThanZero)) == "∃n ∈ {1, 2, 3}: (n > 0)")