Row variables are lost when converting Quint operator types about apalache HOT 4 CLOSED

We have a test for this, so I'm not sure how this is arising in the integration test yet:

from apalache.

7ac4e54 adds the support for row-typed records we need to properly type quint records, but the type checking guards in the builder are not hip to row types, so I'm now getting

      > Name updateF1 with type (({ f1: Int }) => { f1: Int }) constructed in scope where expected type is (({ f1: Int, f2: Str, a }) => { f1: Int, f2: Str, a }). E@18:16:20.594

from apalache.

Ah, the row typing is getting lost on the quint side actually:

Given

    def updateF1(r) = r.with("f1", 1) 

    action Next = all {
        rec1' = updateF1(rec1),
        rec2' = rec2.with("f3", true),
        rec3' = updateF1(rec3),
    }

The source map for the declaration of updateF1 looks like:

{
          "id": 20,
          "kind": "def",
          "name": "updateF1",
          "qualifier": "def",
          "expr": {
            "id": 20,
            "kind": "lambda",
            "params": [{ "id": 15, "name": "r" }],
            "qualifier": "def",
            "expr": {
              "id": 19,
              "kind": "app",
              "opcode": "with",
              "args": [
                { "id": 16, "kind": "name", "name": "r" },
                { "id": 17, "kind": "str", "value": "f1" },
                { "id": 18, "kind": "int", "value": 1 }
              ]
            }
          }
        }

But the source map we get for the application of updateF1 looks like this:

                  {
                    "id": 43,
                    "kind": "app",
                    "opcode": "updateF1",
                    "args": [{ "id": 42, "kind": "name", "name": "rec1" }]
                  }

When we then construct the application of updateF1, we need to supply the type for the operator updateF1 to the builder, but we we deduce this its application context alone, which doesn't give us access to the type of the operator at time of declaration. Instead we only have this to work with:

    "43": {
      "typeVariables": {},
      "rowVariables": {},
      "type": {
        "kind": "rec",
        "fields": {
          "kind": "row",
          "fields": [{ "fieldName": "f1", "fieldType": { "kind": "int" } }],
          "other": {
            "kind": "row",
            "fields": [
              { "fieldName": "f2", "fieldType": { "id": 2, "kind": "str" } }
            ],
            "other": { "kind": "var", "name": "r1" }
          }
        }
      }
    },

Since the "scope safe" builder is policing consistent typing of named expressions, once a closed type has been inferred for the operator application, subsequent applications licensed by the polymorphic type of the declared operator, instead are rejected due to the conflict of the
concrete types.

Options:

• Use the builder that doesn't enforce singular typing of names.
• Extend the context of the converter to track the type of declared operator by name.
• Extend the QuintIR so it includes the ID of a name's definition along with each occurence of the name

from apalache.

@gabrielamafra noted that we're not using the lookup table currently, support for exporting this was just added recently, but it will give us a way to derive the type of the defined operator. 🎉

from apalache.