Error when running Quint verify: Type constructed in scope

[p-offtermatt]

Apalache is version 0.44.7
Quint version 0.18.3
Spec: https://github.com/cosmos/interchain-security/blob/8184c49ab6f6edb3e53cd7b6a70c127d5b65eb24/tests/mbt/model/ccv_model.qnt#L178

I get this error:

% quint verify ccv_model.qnt --verbosity 5
error: internal error: while parsing in Apalache:
'Input was not a valid representation of the QuintIR: Conversion failed while building operator definition `ccv_model::ccv::AppendConsumerAddrToPrune`: Name ccv_model::ccv::consumerAddrsToPrune_5823 with type (() => (Int -> Seq(Str))) constructed in scope where expected type is (() => (Str -> (Int -> Seq(g)))).'

[p-offtermatt]

I think it comes from this block:

pure def AppendConsumerAddrToPrune(currentState: ProtocolState, oldConsAddr: ConsumerAddr, consumer: Chain): ProtocolState = {
        pure val vscId = currentState.providerState.runningVscId
        pure val consumerAddrsToPrune = currentState.providerState.consumerAddrsToPrune.getOrElse(consumer, Map())
        pure val prevConsAddrs = consumerAddrsToPrune.getOrElse(oldConsAddr, Map()).getOrElse(vscId, [])

        pure val newConsAddrsToPrune = consumerAddrsToPrune.put(vscId, prevConsAddrs.append(oldConsAddr))

        currentState.with(
            "providerState", 
            currentState.providerState.with(
                "consumerAddrsToPrune",
                currentState.providerState.consumerAddrsToPrune.put(consumer, newConsAddrsToPrune)
            )
        )
    }

[p-offtermatt]

I think this is an issue in my model (which never gets caught during typechecking, nor did it ever come up during simulation... makes me a bit suspicious)

The problem is this line

        pure val prevConsAddrs = consumerAddrsToPrune.getOrElse(oldConsAddr, Map()).getOrElse(vscId, [])

I think it should be

pure val prevConsAddrs = consumerAddrsToPrune.getOrElse(vscId, [])

because providerState.consumerAddrsToPrune is defined like this:

consumerAddrsToPrune: Chain -> VscId -> List[ConsumerAddr],

[bugarela]

Discussed in slack. This is indeed a type error that Quint should detect. Fortunately, the fix I'm currently working on for the type checker makes it so it catches the error.

/home/gabriela/projects/interchain-security/tests/mbt/model/ccv_utils.qnt:76:34 - error: [QNT000] Couldn't unify str and int
Trying to unify str and int
Trying to unify ((_t1079 -> _t1080), _t1079, _t1080) => _t1080 and ((VscId -> List[ConsumerAddr]), ConsumerAddr, (_t1076 -> _t1077)) => _t1081

76:         pure val prevConsAddrs = consumerAddrsToPrune.getOrElse(oldConsAddr, Map()).getOrElse(vscId, [])
                                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: typechecking failed

[bugarela]

I merged my type checker fix that fixes this problem as I said above (#1409)