From 97c6a6ad2b7ededf490c136e48f4b7700a08b33d Mon Sep 17 00:00:00 2001
From: bugarela <gabrielamoreira05@gmail.com>
Date: Mon, 27 Nov 2023 14:39:06 -0300
Subject: [PATCH 1/2] Update effect signature for `match` to enforce same
 updates on all eliminators

---
 quint/src/effects/builtinSignatures.ts | 11 +++++------
 quint/test/effects/inferrer.test.ts    | 24 +++++++++++++++++-------
 2 files changed, 22 insertions(+), 13 deletions(-)

diff --git a/quint/src/effects/builtinSignatures.ts b/quint/src/effects/builtinSignatures.ts
index eab9e8d72..a562851cc 100644
--- a/quint/src/effects/builtinSignatures.ts
+++ b/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,8 +250,8 @@ 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:
     //
@@ -260,17 +259,17 @@ const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [
     // - 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}`)
     },
   ],
diff --git a/quint/test/effects/inferrer.test.ts b/quint/test/effects/inferrer.test.ts
index 498089f75..cba870e1d 100644
--- a/quint/test/effects/inferrer.test.ts
+++ b/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',
+    })
   })
 })

From d1367bced75f92dad9a0071e9a488d526b3e3967 Mon Sep 17 00:00:00 2001
From: bugarela <gabrielamoreira05@gmail.com>
Date: Mon, 27 Nov 2023 14:43:24 -0300
Subject: [PATCH 2/2] Add CHANGELOG entry

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4527035c5..afc262c01 100644
--- a/CHANGELOG.md
+++ b/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