Merge pull request #1272 from informalsystems/gabriela/fix-match-effect

Fix effect signature for the `match` operator

CHANGELOG.md

@@ -19,6 +19,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Produce proper error messages on invalid module name (#1260)
 - Fix JSON output when running multiple tests (#1264)
 - Topological sorting of modules (#1268)
+- The effect checker will now check for consistency of updates across different
+  cases inside `match` (#1272)
 
 ### Security
 

quint/src/effects/builtinSignatures.ts

@@ -16,7 +16,6 @@ import { ComponentKind, Effect, EffectComponent, EffectScheme, Entity, Signature
 import { parseEffectOrThrow } from './parser'
 import { range, times } from 'lodash'
 import { QuintBuiltinOpcode } from '../ir/quintIr'
-import { zip } from '../util'
 
 export function getSignatures(): Map<string, Signature> {
   return new Map<string, Signature>(fixedAritySignatures.concat(multipleAritySignatures))
@@ -251,26 +250,26 @@ const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [
     //
     // has an effect signature matching the scheme
     //
-    // (a, Pure, (a) => Read[r0] & Update[u0], ..., (a) => Read[rn] & Update[un])
-    //   => Read[r0,...,rn] & Update[u0,...,un]
+    // (a, Pure, (a) => Read[r0] & Update[u], ..., (a) => Read[rn] & Update[u])
+    //   => Read[r0,...,rn] & Update[u]
     //
     // Because:
     //
     // - Assuming `expr` has effect `a`, each eliminator must take a parameter with effect `a`.
     // - Each label is a string literal, which must be `Pure`.
     // - The result of applying the operator may have the effect of the body of any of the eliminators:
     //   the union of effect variables here corresponding to the disjunctive structure of the sum-type eliminator.
+    // - All eliminators must have the same update effect.
     'matchVariant',
     (arity: number) => {
       // We need indexes for each eliminator (i.e., lambdas), so that we can number
       // the effect variables corresponding to body of each respective eliminator.
       const eliminatorIdxs = range((arity - 1) / 2)
       const readVars = eliminatorIdxs.map(i => `r${i}`)
-      const updateVars = eliminatorIdxs.map(i => `u${i}`)
       const matchedExprEffect = 'a'
-      const eliminationCaseEffects = zip(readVars, updateVars).map(([r, u]) => `Pure, (a) => Read[${r}] & Update[${u}]`)
+      const eliminationCaseEffects = readVars.map(r => `Pure, (a) => Read[${r}] & Update[u]`)
       const argumentEffects = [matchedExprEffect, ...eliminationCaseEffects].join(', ')
-      const resultEffect = `Read[${readVars.join(',')}] & Update[${updateVars.join(',')}]`
+      const resultEffect = `Read[${readVars.join(',')}] & Update[u]`
       return parseAndQuantify(`(${argumentEffects}) => ${resultEffect}`)
     },
   ],

quint/test/effects/inferrer.test.ts

@@ -248,12 +248,22 @@ describe('inferEffects', () => {
 
     const [errors] = inferEffectsForDefs(defs)
 
-    errors.forEach(v =>
-      assert.deepEqual(v, {
-        children: [],
-        location: 'Inferring effect for f',
-        message: 'Result cannot be an opperator',
-      })
-    )
+    assert.deepEqual([...errors.values()][0], {
+      children: [],
+      location: 'Inferring effect for f',
+      message: 'Result cannot be an opperator',
+    })
+  })
+
+  it('returns error when `match` branches update different variables', () => {
+    const defs = ['type Result = | Some(int) | None', "val foo = match Some(1) { | Some(n) => x' = n | None => true }"]
+
+    const [errors] = inferEffectsForDefs(defs)
+
+    assert.deepEqual([...errors.values()][0].children[0].children[0].children[0].children[0], {
+      children: [],
+      location: "Trying to unify entities ['x'] and []",
+      message: 'Expected [x] and [] to be the same',
+    })
   })
 })