Invalid representation of quintIR error when running verify

[zaphar]

Minimal reproducible example:

module minimal {
    type MyId = Id(int)

    pure val Ids: Set[MyId] = Set(Id(1), Id(2), Id(3))

    var IdSet: Set[MyId]

    action init = all {
        IdSet' = Set()
    }

    action nextStep(id: MyId): bool = all {
        IdSet' = IdSet.union(Set(id))
    }

    action step = {
        nondet id: MyId = Ids.oneOf()
        all {
            nextStep(id)
        }
    }

    val idSetIsIds = IdSet == Ids 
}

Produces the following error when run with

$> quint verify --max-steps=1 minimal.qnt --invariant=idSetIsIds
11:41:44.120 [main] INFO at.forsyte.apalache.tla.tooling.opt.ServerCmd -- Loading configuration
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Output directory: /Users/zaphar/vae/models/formal/_apalache-out/server/2024-08-31T11-41-44_3553926767883274806
# APALACHE version: 0.44.11 | build: 5dee24e                      I@11:41:44.333
Starting server on port 8822...                                   I@11:41:44.340
The Apalache server is running on port 8822. Press Ctrl-C to stop.
PASS #0: SanyParser                                               I@11:41:48.061
  > Error parsing file StringSource(Qnt)                          E@11:41:48.347
  > Input was not a valid representation of the QuintIR: Conversion failed while building operator definition `step`: Operator EXISTS3 cannot be applied to arguments of types (Id(Int), Set(Id(Int) | d), Bool) E@11:41:48.34
7
error: internal error: while parsing in Apalache:
'Input was not a valid representation of the QuintIR: Conversion failed while building operator definition `step`: Operator EXISTS3 cannot be applied to arguments of types (Id(Int), Set(Id(Int) | d), Bool)'
Please report an issue: https://github.com/informalsystems/quint/issues/new

a quint typecheck and quint run all succeed just fine.

[zaphar]

I note that if I change type MyId = Id(int) to type MyId = Id(int) | Unused It works. So I assume that Avalache has issues with sumtypes where there is only one type constructor. The parser allows this just fine though and the run command handles it so I'm not clear where the error is. The quint typechecker, avalache, or the Parser. The docs don't make it super clear.

[bugarela]

Hi! Thanks for reporting.

The error arises from a mismatch of what Quint allows and what Apalache expects, so it can be both that Quint is being over-permissive or that Apalache is requiring something weird.

Your hypothesis

So I assume that Avalache has issues with sumtypes where there is only one type constructor.

seems like a good one to me. I'll try to explore more on this direction. Is this | Unused workaround enough to unblock your work for now?

[zaphar]

Yeah, I can work around it fine with that. If I can help with debugging or anything let me know. I like the language so far.