Variables and Constant should not be allowed to have quantified type variables

[konnov]

I have accidentally introduced a type error in the variable declaration:

// it should be:
// var erc20State: Erc20State
var erc20State: erc20State

https://github.com/informalsystems/quint/blob/56abbcd46437c8b515b7c7b50e4dc1b899da61ab/examples/solidity/ERC20/erc20.qnt#L244-L257

The type checker did not detect a problem in the variable declaration. Moreover, I had a type error in the following action:

https://github.com/informalsystems/quint/blob/56abbcd46437c8b515b7c7b50e4dc1b899da61ab/examples/solidity/ERC20/erc20.qnt#L253-L257

We should figure out, what is going on with the type checker.

[bugarela]

I understand the problem! Our language manual specifyies:

Uninterpreted type or type name: IDENTIFIER_IN_CAPS. Type variable (parameter): a, ..., z.

So erc20State here is parsed as a (quantified) type variable.

This is actually a language design problem 😅 Should we prevent state variables to have quantified type variables at all? @konnov

[konnov]

So erc20State here is parsed as a (quantified) type variable.

This is actually a language design problem 😅 Should we prevent state variables to have quantified type variables at all? @konnov

Oh, wow. Yes, we cannot do much about polymorphic state variables. This should be caught by the type checker.

[bugarela]

Ok! I'll change the issue name to reflect the specifics of what the type checker misses.

[bugarela]

I'll also add this check to constants as we discussed at some quint meeting.

[shonfeder]

As a special case of this we should not allow declaration of these to include free row variables. This is currently accepted:

    var rec1: { f1: int, f2: str | r1 }
    var rec2: { f2: str, f3: bool | r2 }

[shonfeder]

This is related to #456 and can probably be fixed at the same time. It is another case where we are allowing type annotations for things that cannot be values (nothing can have type 'a since we don't have a bottom or non-termination).