option type breaking in `quint verify`

[konnov]

Consider the following specification:

module option {
    type Option[a] = None | Some(a)
}

module none {
    import option.*

    type State = {
        x: Option[int],
        y: Option[str],
    }

    var state: State

    action init = {
        state' = {
            x: None,
            y: None,
        }
    }

    action step = {
        state' = state
    }
}

The simulator runs on it without any issue:

$ quint run --main=none none.qnt
...
[ok] No violation found (300ms).

However, quint verify produces a hard-to-understand error:

$ quint verify --main=none none.qnt
error: internal error: while parsing in Apalache:
'Input was not a valid representation of the QuintIR: Conversion failed while building operator definition `init`: Name None with type (() => None(UNIT) | Some(Str)) constructed in scope where expected type is (() => None(UNIT) | Some(Int)).'
Please report an issue: https://github.com/informalsystems/quint/issues/new

When I introduce auxiliary pure val definitions for the two cases of None above, everything works. I suspect that the issue is caused by type inference for the two instances of None, which technically should be of the types Option[int] and Option[str].

[konnov]

If this helps, any use of this definition does not work either:

    def option_map(opt: Option[a], mapper: a => b): Option[b] = {
        match (opt) {
            | None => None
            | Some(e) => Some(mapper(e))
        }
    }

[bugarela]

Thanks for the reporting! We never got to extensively test the polymorphic sum types in the integration with Apalache, seems like we are not setting a correct polymorphic type for None at translation.

[bugarela]

This is fixed (I think by apalache-mc/apalache#3044 but not 100% sure). The problem does not happen on main anymore 🙏