Use the empty tuple for the unit

[shonfeder]

Closes #1401

The integration tests assume fixes to Apalache added in
apalache-mc/apalache#2860,
so we'll need to cut a release for that, then update the expected version here,
before the CI will pass.

• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• Feature table on README.md updated for any listed functionality

[bugarela]

This is not working with the integration with Apalache, even after the new release. I can't understand what is happening, but it seems like a direct consequences of using tuples int the ETC type checker.

Before this change, we had something like:

(List((({  }) => {  })), args: ArraySeq(E3@(((() => {  })) )))

And after the change, we get:

(List(((<<>>) => <<>>)), args: ArraySeq(E3@Seq(l)))

Which results in the error:

[unknown location]: An operator with the signature ((<<>>) => <<>>) cannot be applied to the provided argument of type Seq(l)

I'm out of ideas on how to debug this, and I have no clue where the Seq is coming from here. My one thought is that it can be related to building empty values that can sometimes require an annotation (i.e. empty set, empty seq).

I'll leave this open for a bit to see if anything pops up.

[shonfeder]

My one thought is that it can be related to building empty values that can sometimes require an annotation (i.e. empty set, empty seq).

This should be accounted for in https://github.com/informalsystems/apalache/blob/main/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala#L238-L250

But if quint is tying the applicand as a tuple, then the conversion should be converting it to a tuple and nothing else, as per https://github.com/informalsystems/apalache/blob/8366559116b5147a506f8162f73f161bdd81be79/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala#L573

I think I don't understand the examples you posted, because if, in

(List((({  }) => {  })), args: ArraySeq(E3@(((() => {  })) )))

args is meant to indicate the type of the argument to which an operator of type ({ }) => { } is applied, then that also indicates some very wrong conversion afaict...

Sorry this is not working as expected!

[shonfeder]

Maybe it would help to detail the particulars of the error case you are hitting with Apalache, because at

https://github.com/informalsystems/quint/pull/1406/files#diff-91eb548c828cf03653ee4b7ad8ad4bf71803fa45efb441853c4b68d61a935405

and

https://github.com/informalsystems/quint/pull/1406/files#diff-309e4c37edc4cfff3079aded89b649280575e6b691db8e8c8ce5ba859aa6e526R229

We are testing that variants can be parsed and converted, and this includes a converted empty tuple: https://github.com/informalsystems/quint/pull/1406/files#diff-309e4c37edc4cfff3079aded89b649280575e6b691db8e8c8ce5ba859aa6e526R240

So seeing concretely where this is failing may help. I'm sure you've checked this, but if not, sanity checking that the quint inference is all as expected can't hurt.

[shonfeder]

Ah, could it be happening here?

https://github.com/informalsystems/apalache/blob/8366559116b5147a506f8162f73f161bdd81be79/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala#L454-L456

[shonfeder]

I think it may be the mix of the type inference rule linked above and the way that the types builder does its type validation? And the latter can be quite tricky to unravel, unfortunately.

Here's an idea: since the current way the builder is set up doesn't seem to allow constructing empty tuples (since it insists they are Seq), try adding a special case in the converter for when the Tup quint operator is applied to no arguments, and then a special builder rule that just directly constructs the empty tuple, without doing any type validation (because it cannot be ill-typed). This should just require constructing a TlaEx of the right shape, with the empty tuple type tag, and then returning it into the TBuilderInstruction monad. Similar to https://github.com/informalsystems/apalache/blob/8366559116b5147a506f8162f73f161bdd81be79/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala#L54

[bugarela]

Ah, could it be happening here?

https://github.com/informalsystems/apalache/blob/8366559116b5147a506f8162f73f161bdd81be79/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala#L454-L456

Aaaah, it has to be it! Thanks so much for looking this up!

I think I understand your suggestion, and I'll try to implement it!

[bugarela]

Ok, I tried it but it doesn't help. The problem is not happening at the building stage, but at the typechecking pass. I think the only way to fix this in the building stage would be to build the empty tuples with the Seq(fresh) type, so it can match the expectation later at the typechecking stage.

[bugarela]

I had an idea and I quite like it. I changed conversion so the empty tuple is always translated into the uninterpreted type "UNIT" (as it is defined in Variants.tla). And then, the module looks like this:

-------------------------- MODULE ApalacheCompilation --------------------------

EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants

VARIABLE x

A == Variant("A", "U_OF_UNIT")

B(__BParam_27) == Variant("B", __BParam_27)

foo_bar(id__123_31) == id__123_31

importedValue == 0

ApalacheCompilation_ModuleToInstantiate_C == 0

step == x' := (x + 1)

inv == x >= 0

ApalacheCompilation_ModuleToInstantiate_instantiatedValue ==
  ApalacheCompilation_ModuleToInstantiate_C

init ==
  x'
    := (importedValue
      + ApalacheCompilation_ModuleToInstantiate_instantiatedValue)

[shonfeder]

Ah yeah! That's perfect. I think that is the right fix!

We could always introduce a distinct

type Unit = | U

or something on the quint side if we want to match that more closely. But I think this is a great approach!