Fix our dear #693 type checker bug

CHANGELOG.md

@@ -25,6 +25,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   shadowed a nested name from the imported module (#802)
 - Fixed a problem where tests were ignored if they are not defined directly in
   the main module - that is, they were imported (#1161)
+- Fixed a type checker bug where the inferred type was too general for nested
+  definitions, which prevented running `verify` (#1166).
 
 ### Security
 

doc/rfcs/rfc001-sum-types/rfc001-erc-sum-types-example.qnt

@@ -83,8 +83,7 @@ module erc20 {
     // https://github.com/OpenZeppelin/openzeppelin-contracts/blob/ca822213f2275a14c26167bd387ac3522da67fe9/contracts/token/ERC20/ERC20.sol#L222
     pure def _transfer(state: Erc20State,
             fromAddr: Address, toAddr: Address, amount: Uint): Erc20Result = {
-        // FIXME(#693): type annotation below is a workaround, inferred type is too general
-        val fromBalance: int = state.balanceOf.get(fromAddr)
+        val fromBalance = state.balanceOf.get(fromAddr)
         Ok(state)
             .require(fromAddr != ZERO_ADDRESS, "ERC20: transfer from the zero address")
             .require(toAddr != ZERO_ADDRESS, "ERC20: transfer to the zero address")

examples/.scripts/run-example.sh

@@ -52,13 +52,6 @@ result () {
       printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
     elif [[ "$file" == "classic/distributed/Paxos/Voting.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" )]] ; then
       printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
-    elif [[ "$file" == "cosmos/ics20/ics20.qnt" && "$cmd" == "verify" ]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/issues/693</sup>"
-    elif [[ "$file" == "cosmos/ics23/ics23.qnt" && "$cmd" == "verify" ]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/issues/693,</sup>"
-      printf "<sup>https://github.com/informalsystems/quint/pull/975</sup>"
-    elif [[ "$file" == "cosmwasm/zero-to-hero/vote.qnt" && "$cmd" == "verify" ]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/issues/693</sup>"
     elif [[ "$file" == "language-features/option.qnt" && "$cmd" == "verify"  ]] ; then
       printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
     elif [[ "$file" == "language-features/tuples.qnt" && "$cmd" == "verify" ]] ; then
@@ -83,6 +76,8 @@ get_main () {
     main="--main=properChannelsTests"
   elif [[ "$file" == "cosmos/ics20/ics20.qnt" ]] ; then
     main="--main=ics20Test"
+  elif [[ "$file" == "cosmos/ics23/ics23.qnt" ]] ; then
+    main="--main=trees"
   elif [[ "$file" == "cosmos/lightclient/Lightclient.qnt" ]] ; then
     main="--main=Lightclient_4_3_correct"
   elif [[ "$file" == "puzzles/prisoners/prisoners.qnt" ]] ; then
@@ -93,6 +88,8 @@ get_main () {
     main="--main=simplePonziTest"
   elif [[ "$file" == "solidity/GradualPonzi/gradualPonzi.qnt" ]] ; then
     main="--main=gradualPonziTest"
+  elif [[ "$file" == "cosmwasm/zero-to-hero/vote.qnt" ]] ; then
+    main="--main=state"
   fi
   echo "${main}"
 }
@@ -102,6 +99,8 @@ get_test_args () {
   local args=""
   if [[ "$file" == "cosmos/ics20/ics20.qnt" ]] ; then
     args="--max-samples=1000"  # default of 10000 takes too long
+  elif [[ "$file" == "cosmos/tendermint/TendermintModels.qnt" ]] ; then
+    args="--max-samples=1000"  # default of 10000 takes too long
   fi
   echo "${args}"
 }
@@ -115,6 +114,8 @@ get_verify_args () {
     args="--init=Init --step=Next"
   elif [[ "$file" == "cosmos/tendermint/TendermintModels.qnt" ]] ; then
     args="--init=n4_f1::Init --step=n4_f1::Next --invariant=n4_f1::Agreement"
+  elif [[ "$file" == "cosmos/ics23/ics23.qnt" ]] ; then
+    args="--init=Init --step=Next"
   fi
   echo "${args}"
 }

examples/README.md

@@ -58,16 +58,16 @@ listed without any additional command line arguments.
 | [cosmos/ics20/bank.qnt](./cosmos/ics20/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/ics20/base.qnt](./cosmos/ics20/base.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/ics20/denomTrace.qnt](./cosmos/ics20/denomTrace.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [cosmos/ics20/ics20.qnt](./cosmos/ics20/ics20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693</sup> |
-| [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693,</sup><sup>https://github.com/informalsystems/quint/pull/975</sup> |
+| [cosmos/ics20/ics20.qnt](./cosmos/ics20/ics20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/tendermint/Tendermint.qnt](./cosmos/tendermint/Tendermint.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/tendermint/TendermintModels.qnt](./cosmos/tendermint/TendermintModels.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/tendermint/TendermintTest.qnt](./cosmos/tendermint/TendermintTest.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
-| [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693</sup> |
+| [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cryptography/hashes.qnt](./cryptography/hashes.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cryptography/hashesTest.qnt](./cryptography/hashesTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [language-features/booleans.qnt](./language-features/booleans.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

examples/cosmos/ics20/denomTrace.qnt

@@ -51,8 +51,7 @@ module denomTrace {
 
   /// `channelNamesUniquePerChain` is true iff channel names are unique by chain
   pure def channelNamesUniquePerChain(topology: ChannelTopology): bool =
-    // FIXME(#693): type annotation below is a workaround, inferred type is too general
-    pure val chainNames: Set[str] = topology.keys()
+    pure val chainNames = topology.keys()
     and {
       // Check the domain for the second level of chains
       chainNames.forall(chain => topology.get(chain).keys() == chainNames),

examples/cosmwasm/zero-to-hero/vote.qnt

@@ -491,7 +491,8 @@ module state {
       val poll = state.polls.get(poll_id)
       poll.options.listForall(option =>
         val optionKey = option._1
-        val optionSum = option._2
+        // FIXME(#1167): Type annotation below is a workaround, inferred type is too general
+        val optionSum: int = option._2
         // `ballots` only contains entries if there are > 0 votes.
         optionSum > 0 implies and {
           summed_ballots.keys().contains(optionKey),
@@ -513,4 +514,4 @@ module state {
   //        the sum differently based on whether such a ballot is present.]
   val invAllBallotsPositive = query_all_polls(state).polls.listForall(poll =>
                                 poll.options.listForall(opt => opt._2 >= 0))
-}
+}

examples/solidity/ERC20/erc20.qnt

@@ -98,8 +98,7 @@ module erc20 {
     // https://github.com/OpenZeppelin/openzeppelin-contracts/blob/ca822213f2275a14c26167bd387ac3522da67fe9/contracts/token/ERC20/ERC20.sol#L222
     pure def _transfer(state: Erc20State,
             fromAddr: Address, toAddr: Address, amount: Uint): Erc20Result = {
-        // FIXME(#693): type annotation below is a workaround, inferred type is too general
-        val fromBalance: int = state.balanceOf.get(fromAddr)
+        val fromBalance = state.balanceOf.get(fromAddr)
         val err = require(fromAddr != ZERO_ADDRESS, "ERC20: transfer from the zero address")
             .andRequire(toAddr != ZERO_ADDRESS, "ERC20: transfer to the zero address")
             .andRequire(fromBalance >= amount, "ERC20: transfer amount exceeds balance")

examples/solidity/GradualPonzi/gradualPonzi.qnt

@@ -89,9 +89,8 @@ module gradualPonzi {
 
   // an invester may withdraw their rewards
   pure def withdraw(evm: EvmState, ponzi: PonziState, sender: Addr): Result = {
-    // FIXME(#693): type annotation below is a workaround, inferred type is too general
-    pure val reward: int = ponzi.rewards.get(sender)
-    pure val newBalances: Addr -> int =
+    pure val reward = ponzi.rewards.get(sender)
+    pure val newBalances =
       evm.balances
         .setBy(sender, old => old + reward)
         .setBy(ponzi.contract, old => old - reward)

examples/solidity/SimpleAuction/SimpleAuction.qnt

@@ -80,8 +80,7 @@ module SimpleAuction {
     // No gas fees are taken into account.
     pure def evmSend(es: EvmState,
                      fromAddr: Addr, toAddr: Addr, value: int): EvmState = {
-        // FIXME(#693): type annotation below is a workaround, inferred type is too general
-        val bs: Addr -> UInt = es.balances
+        val bs = es.balances
         val fromBal = bs.get(fromAddr) - value
         val toBal = bs.get(toAddr) + value
         // compute the balances after `evmSend`

quint/src/types/constraintGenerator.ts

@@ -30,7 +30,7 @@ import {
   QuintVar,
   isAnnotatedDef,
 } from '../ir/quintIr'
-import { QuintType, typeNames } from '../ir/quintTypes'
+import { QuintType, rowNames, typeNames } from '../ir/quintTypes'
 import { expressionToString, rowToString, typeToString } from '../ir/IRprinting'
 import { Either, left, mergeInMany, right } from '@sweet-monads/either'
 import { Error, ErrorTree, buildErrorLeaf, buildErrorTree, errorTreeToString } from '../errorTree'
@@ -338,6 +338,10 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
     return this.solvingFunction(this.table, constraint)
       .mapLeft(errors => errors.forEach((err, id) => this.errors.set(id, err)))
       .map(subs => {
+        // For every free name we are binding in the substitutions, the names occuring in the value of the substitution
+        // have to become free as well.
+        this.addBindingsToFreeNames(subs)
+
         // Apply substitution to environment
         // FIXME: We have to figure out the scope of the constraints/substitutions
         // https://github.com/informalsystems/quint/issues/690
@@ -411,6 +415,28 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
     }
     return { ...nonFreeNames, type }
   }
+
+  private addBindingsToFreeNames(substitutions: Substitutions) {
+    // Assumes substitutions are topologically sorted, i.e. [ t0 |-> (t1, t2), t1 |-> (t3, t4) ]
+    substitutions.forEach(s => {
+      switch (s.kind) {
+        case 'type':
+          this.freeNames
+            .filter(free => free.typeVariables.has(s.name))
+            .forEach(free => {
+              const names = typeNames(s.value)
+              names.typeVariables.forEach(v => free.typeVariables.add(v))
+              names.rowVariables.forEach(v => free.rowVariables.add(v))
+            })
+          return
+        case 'row':
+          this.freeNames
+            .filter(free => free.rowVariables.has(s.name))
+            .forEach(free => rowNames(s.value).forEach(v => free.rowVariables.add(v)))
+          return
+      }
+    })
+  }
 }
 
 function checkAnnotationGenerality(

quint/test/types/inferrer.test.ts

@@ -158,6 +158,24 @@ describe('inferTypes', () => {
     ])
   })
 
+  it('keeps track of free names properly (#693)', () => {
+    const defs = ['val b(x: int -> str): int = val c = x.keys() { 1 }']
+
+    const [errors, types] = inferTypesForDefs(defs)
+    assert.isEmpty(errors, `Should find no errors, found: ${[...errors.values()].map(errorTreeToString)}`)
+
+    const stringTypes = Array.from(types.entries()).map(([id, type]) => [id, typeSchemeToString(type)])
+    assert.sameDeepMembers(stringTypes, [
+      [1n, '(int -> str)'],
+      [6n, '(int -> str)'],
+      [7n, 'Set[int]'],
+      [8n, 'Set[int]'],
+      [9n, 'int'],
+      [10n, 'int'],
+      [12n, '((int -> str)) => int'],
+    ])
+  })
+
   it('checks annotations', () => {
     const defs = ['def e(p): (t) => t = p + 1']