Nesting actions does not work, when putting effects inline does

[p-offtermatt]

Hi!

I am not sure if it is a bug or a feature request. I have the following spec:

module main {
    var myMap: int -> int

    action op1(): bool =
        myMap' =  myMap.set(3,4)

    action op2(): bool =
        myMap' = myMap.set(1,2)

    action noop(): bool =
        myMap' = myMap

    // not working
    // action main0(boolean: bool): bool =
    //     if(boolean){
    //         noop()
    //     } else {
    //         op1()
    //     }

    // not working
    // action main1(boolean: bool): bool =
    //     if(boolean){
    //         op1()
    //     } else {
    //         op2()
    //     }

    // not working
    // action main2(boolean: bool): bool =
    //     any {
    //         op1(),
    //         op2()
    //     }

    // fine
    action main3(boolean: bool): bool =
        if(boolean){
            myMap' = myMap.set(1,2)
        } else {
            myMap' = myMap.set(3,4)
        }
}

The first three variants of the main function do not work, only the last one does. The error in each case is something along the lines of this:

Couldn't unify bool and oper
Trying to unify bool and () => t12
quint(QNT000)
Can't unify different types of effects
Trying to unify Read['myMap'] & Update['myMap'] and () => e5
Trying to infer effect for operator application in noop()
quint(QNT000)

Is this a bug? Intended behaviour? I would like to be able to use the syntax from main0/main1.

Quick reasoning behind why I want this: My spec touches on various modules (of the Cosmos SDK), and what I am trying to do is essentially have actions for each module, such that the only actions modifying the variables of a given module are its own actions.

Having everything inline like in main3 is not really an option, since this would become an absolutely massive blob.

[bugarela]

Hi! We talked briefly over slack, but here is my official response :grimacing:

This is a bug involving nullary operators, similar to https://github.com/informalsystems/quint/issues/881. Removing the empty parenthesis in the action invocation should fix it for now.

However, we should support this scenario afaiu (and if don't, provide a better error message). I did some investigation and there is a problem with the way we parse type annotations: action op1(): bool is being parsed with the annotation bool but, iiuc, it should be parsed as () => bool. If the parsing was correct, I believe that type and effect checking should go through.