From 284268d304eb7d489039d1f88ac2214516ae79dc Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Wed, 8 Mar 2023 04:31:36 -0500
Subject: [PATCH] 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     |  1 +
 .../at/forsyte/apalache/io/quint/Quint.scala  | 23 +++++++++++++------
 .../apalache/io/quint/TestQuintEx.scala       | 11 ++++++++-
 3 files changed, 27 insertions(+), 8 deletions(-)
 create mode 100644 .unreleased/bug-fixes/quint-empty-sets.md

diff --git a/.unreleased/bug-fixes/quint-empty-sets.md b/.unreleased/bug-fixes/quint-empty-sets.md
new file mode 100644
index 0000000000..5fb2df7349
--- /dev/null
+++ b/.unreleased/bug-fixes/quint-empty-sets.md
@@ -0,0 +1 @@
+Fix the typing of quint empty sets during conversion (see #2466)
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
index c813e2b7da..09bc911d52 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
+++ b/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)
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
index 2afc47c9bc..dbae85f67d 100644
--- a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
+++ b/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)")