Merge pull request #3044 from apalache-mc/gabriela/fix-quint-nullary-…

…polymorphism

Fix conversion of Quint nullary polymorphic operators

.unreleased/bug-fixes/quint-nullary-operators.md

@@ -0,0 +1 @@
+Fix a problem when translating Quint nullary operators used polymorphically, see #3044

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

@@ -4,16 +4,14 @@ import at.forsyte.apalache.io.quint.QuintEx._
 import at.forsyte.apalache.io.quint.QuintType._
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.typecomp._
+import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeLiteralAndNameBuilder
 import at.forsyte.apalache.tla.types.tla
 
 // scalaz is brought in For the Reader monad, which we use for
 // append-only, context local state for tracking reference to nullary TLA
 // operators
 import scalaz._
-// list and traverse give us monadic mapping over lists
-// see https://github.com/scalaz/scalaz/blob/88fc7de1c439d152d40fce6b20d90aea33cbb91b/example/src/main/scala-2/scalaz/example/TraverseUsage.scala
-import scalaz.std.list._
-import scalaz.syntax.traverse._
+import Scalaz._
 
 import scala.util.{Failure, Success, Try}
 import at.forsyte.apalache.tla.lir.values.TlaStr
@@ -31,6 +29,8 @@ import at.forsyte.apalache.tla.lir.values.TlaStr
 class Quint(quintOutput: QuintOutput) {
   private val nameGen = new QuintNameGen // name generator, reused across the entire spec
   private val typeConv = new QuintTypeConverter
+  private val unsafeBuilder = new UnsafeLiteralAndNameBuilder {}
+
   private val table = quintOutput.table
   private val types = quintOutput.types
 
@@ -727,7 +727,12 @@ class Quint(quintOutput: QuintOutput) {
             val t = typeConv.convert(types(id).typ)
             Reader { nullaryOpNames =>
               if (nullaryOpNames.contains(name)) {
-                tla.appOp(tla.name(name, OperT1(Seq(), t)))
+                // Name can be a polymorphic operator, but we need to give it the
+                // specialized type inferred by Quint to avoid type errors in
+                // Apalache. So we use the unsafe builder instead, as the safe
+                // builder enforces that same names have the same types under
+                // the scope.
+                tla.appOp(unsafeBuilder.name(name, OperT1(Seq(), t)).point[TBuilderInternalState])
               } else {
                 tla.name(name, t)
               }

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

@@ -205,7 +205,7 @@ class TestQuintEx extends AnyFunSuite {
 
   def translate(qex: QuintEx): TlaEx = {
     val translator = new Quint(Q.quintOutput)
-    val nullaryOps = Set[String]()
+    val nullaryOps = Set[String]("None")
     val tlaEx = build(translator.tlaExpression(qex).run(nullaryOps))
     tlaEx
   }
@@ -793,13 +793,13 @@ class TestQuintEx extends AnyFunSuite {
     val polyConst1 = "polyConst1"
 
     // We want to test that we can use this polymorphic operator by applying it to two
-    // different values of the same type.
+    // different values of different types.
     val appliedToStr = Q.app(polyConst1, Q.s)(QuintIntT(), oper.id)
     val appliedToBool = Q.app(polyConst1, Q.tt)(QuintIntT(), oper.id)
     // We'll combine these two applications using addition, just to form a compound expression that includes both
     val body = Q.app("iadd", appliedToStr, appliedToBool)(QuintIntT())
 
-    // Putting it all to gether, we have the let expression
+    // Putting it all together, we have the let expression
     //
     // ```
     // def polyConst1(x): a => int = 1;
@@ -811,6 +811,18 @@ class TestQuintEx extends AnyFunSuite {
     assert(convert(expr) == """LET polyConst1(x) ≜ 1 IN (polyConst1("s")) + (polyConst1(TRUE))""")
   }
 
+  test("can convert nullary polymorphic operator used polymorphically") {
+    val optionInt = QuintSumT.ofVariantTypes("Some" -> QuintIntT(), "None" -> QuintRecordT.ofFieldTypes())
+    val noneInt = Q.nam("None", optionInt)
+
+    val optionBool = QuintSumT.ofVariantTypes("Some" -> QuintBoolT(), "None" -> QuintRecordT.ofFieldTypes())
+    val noneBool = Q.nam("None", optionBool)
+
+    val expr = Q.app("Tup", noneInt, noneBool)(QuintTupleT.ofTypes(optionInt, optionBool))
+
+    assert(convert(expr) == """<<None(), None()>>""")
+  }
+
   test("oneOf operator occuring outside of a nondet binding is an error") {
     // See https://github.com/informalsystems/apalache/issues/2774
     val err = intercept[QuintIRParseError](convert(Q.oneOfSet))