Fix conversion of Quint nullary polymorphic operators

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

@@ -727,7 +727,7 @@ 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)))
+                tla.appOp(tla.polymorphicName(name, OperT1(Seq(), t)))
               } 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))

tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala

@@ -77,6 +77,14 @@ trait LiteralAndNameBuilder {
     (mi.copy(freeNameScope = scope + (exprName -> finalT), usedNames = mi.usedNames + exprName), ret)
   }
 
+  /**
+   * {{{exprName: t}}}
+   * @param exprName
+   *   can take different types under the same scope (polymorphic operator).
+   */
+  def polymorphicName(exprName: String, t: TlaType1): TBuilderInstruction =
+    unsafeBuilder.name(exprName, t).point[TBuilderInternalState]
+
   /** Attempt to infer the type from the scope. Fails if exprName is not in scope. */
   def nameWithInferredType(exprName: String): TBuilderInstruction = get[TBuilderContext].map { mi: TBuilderContext =>
     val scope = mi.freeNameScope

tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala

@@ -152,5 +152,13 @@ class TestLiteralAndNameBuilder extends BuilderTest {
           } yield ()
       )
     }
+
+    // Should not throw with polymorphic names
+    build(
+        for {
+          _ <- builder.polymorphicName("x", IntT1)
+          _ <- builder.polymorphicName("x", BoolT1)
+        } yield ()
+    )
   }
 }