Ensure that Quint's quantified variables are freshly generated for ea…

…ch opdef

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

@@ -671,7 +671,7 @@ class Quint(quintOutput: QuintOutput) {
   }
 
   private val opDefConverter: QuintDef.QuintOpDef => NullaryOpReader[(TBuilderOperDeclInstruction, Option[String])] = {
-    case QuintDef.QuintOpDef(_, name, _, expr) =>
+    case QuintDef.QuintOpDef(id, name, _, expr) =>
       (expr match {
         // Parameterized operators are defined in Quint using Lambdas
         case lam: QuintLambda =>
@@ -680,6 +680,13 @@ class Quint(quintOutput: QuintOutput) {
         case other => tlaExpression(other).map(b => (b, List()))
       }).map {
         case (body, params) => {
+          // Quint quantifies types at the opdef level, so here is where we need
+          // to account for quantified variables. The only thing we need to do
+          // is to clear those names from the var number generator memory, so if
+          // they ever appear again, we get fresh TlaType1 var numbers (and not
+          // the same ones).
+          typeConv.clearNames(types(id))
+
           val nullaryName = if (params.isEmpty) Some(name) else None
           (tla.decl(name, body, params: _*), nullaryName)
         }

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

@@ -129,10 +129,9 @@ private[quint] object QuintModule {
 
 /** The representation of types in the type map */
 private[quint] case class QuintTypeScheme(
-    @key("type") typ: QuintType
-    // TODO Will we need these for anything?
-    // typeVariables: List[String],
-    // rowVariables: List[String]
+    @key("type") typ: QuintType,
+    typeVariables: List[String],
+    rowVariables: List[String]
   )
 private[quint] object QuintTypeScheme {
   implicit val rw: RW[QuintTypeScheme] = macroRW

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

@@ -35,6 +35,13 @@ private class QuintTypeConverter extends LazyLogging {
     }
   }
 
+  // Clear the variable names from the state so when the same quantified Quint
+  // variable is used again, we generate a fresh TlaType1 var number for it.
+  def clearNames(typ: QuintTypeScheme): Unit = {
+    typ.typeVariables.foreach(vars.remove)
+    typ.rowVariables.foreach(vars.remove)
+  }
+
   import QuintType._
 
   private def rowToTupleT1(row: Row): TlaType1 = {

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

@@ -52,6 +52,14 @@ class TestQuintEx extends AnyFunSuite {
       exp
     }
 
+    // Register the type of a defintion in the typeMap.
+    // Think of this as a type annotation.
+    def d[D <: QuintDef](definition: D, typ: QuintType): D = {
+      typeMap += (definition.id -> typ)
+      definition
+    }
+
+
     // Operator application
     //
     // The optional `refId` is the id of the declaration defining
@@ -133,15 +141,15 @@ class TestQuintEx extends AnyFunSuite {
     val namedInt2ToBoolOp = e(QuintName(uid, "int2ToBoolOp"), QuintOperT(Seq(QuintIntT(), QuintIntT()), QuintBoolT()))
 
     // Definitions and compound data types
-    val fooDef = QuintDef.QuintOpDef(uid, "foo", "val", tt)
+    val fooDef = d(QuintDef.QuintOpDef(uid, "foo", "val", tt), QuintBoolT())
     val letFooBeTrueIn42 = e(QuintLet(uid, fooDef, _42), QuintIntT())
     val lambda = e(QuintLambda(uid, List(xParam), "def", s), QuintOperT(List(QuintIntT()), QuintStrT()))
     // Applications can only be by name (lambdas are not first class)
     val barDef = opDef("bar", List("x" -> QuintIntT()), s, QuintStrT())
     val appBar = app("bar", _42)(QuintStrT(), barDef.id)
     val letBarBeLambdaInAppBar = e(QuintLet(uid, barDef, appBar), QuintStrT())
     val nIsGreaterThan0 = app("igt", name, _0)(QuintBoolT())
-    val nDefindedAs42 = QuintDef.QuintOpDef(uid, "n", "val", _42)
+    val nDefindedAs42 = d(QuintDef.QuintOpDef(uid, "n", "val", _42), QuintIntT())
     val letNbe42inNisGreaterThan0 = e(QuintLet(uid, nDefindedAs42, nIsGreaterThan0), QuintBoolT())
     // A predicate on ints
     val intIsGreaterThanZero =
@@ -165,7 +173,7 @@ class TestQuintEx extends AnyFunSuite {
     val chooseSomeFromIntSet = app("chooseSome", intSet)(QuintIntT())
     val oneOfSet = app("oneOf", intSet)(QuintIntT())
     val nondetBinding =
-      e(QuintLet(uid, QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), nIsGreaterThan0), QuintIntT())
+      e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintIntT())
     // Requires ID registered with type
     val selectGreaterThanZero = app("select", intList, intIsGreaterThanZero)(QuintSeqT(QuintIntT()))
     val addOne = app("iadd", name, _1)(QuintIntT())
@@ -180,7 +188,7 @@ class TestQuintEx extends AnyFunSuite {
         modules = List(QuintModule(0, "MockedModule", List())),
         types = typeMap.map { case (id, typ) =>
           // Wrap each type in the TypeScheme required by the Quint IR
-          id -> QuintTypeScheme(typ)
+          id -> QuintTypeScheme(typ, List(), List())
         }.toMap,
         table = lookupMap.toMap,
     )