Fix non-exhaustive switches

CONTRIBUTING.md

@@ -82,6 +82,97 @@ FP code in this language, so we keep the balance between readability and
 FPness.  When the idiomatic JavaScript code is shorter and clearer than
 equivalent FP code, we write the idiomatic JavaScript code.
 
+### Ensure exhaustive matches
+
+The type system should help us keep the code base maintainable. But when
+`switch` statements and conditionals are used purely for side effects, we can
+lose the advantage of exhaustivness checking. Here's an example:
+
+Assume we have a type `T`
+
+```typescript
+type T = 'a' | 'b' | 'c'
+```
+
+We should structure our program such that
+
+- we can be sure every alternative is considered (as needed), and
+- whenever a new alternative is added to this type, the type system will warn us
+  about all the places we need to account for the new kind of data.
+
+If we use `T` with a `switch` or `if`/`then` statement that *returns values*,
+this indispensable help is ensured. E.g., if we try to write the following:
+
+```typescript
+function f(x:T): Number {
+  switch x {
+    case 'a':
+      return 0
+    case 'b':
+      return 1
+  }
+}
+```
+
+we will end up with a type error, because the annotation on `f` promises it will
+return a `Number`, but it might in fact return `undefined` since we are not
+handling `c`.
+
+However, if we are only using side effects in the switch, we lose this check!
+
+```typescript
+function f(x:T): Number {
+  let n = -1
+  switch x {
+    case 'a':
+      n = 0
+      break
+    case 'b':
+      n = 1
+      break
+  }
+  return ret
+}
+```
+
+Now the typechecker sees that we will be returning a number no matter what
+happens, even if none of our cases are hit, and we will not get a warning on the
+omitted check for `c`, or for any other data added to this type in the future.
+
+Now, sometimes this kind of catch-all default is what we want, but we should be
+very careful in relying on it, because it creates blind spots. As a rule, we
+should only allow cath-all defaults when the computation we are performing
+**must** be invariant under any expansion of the domain we are computing from.
+
+For all other cases, we can avoid these typechecking blind spots by following two guidelines:
+
+1. Prefer passing data by returning values whenever, and avoid needless mutable
+   assignments.
+2. When switches need to be used for side effects, provide a default that
+   calls `unreachable` on the expression to ensure all cases are handled:
+
+   ```typescript
+   import { unreachable } from './util'
+
+   function f(x:T): Number {
+     let n = -1
+     switch x {
+       case 'a':
+         n = 0
+         break
+       case 'b':
+         n = 1
+         break
+       default:
+         unreachable(x)
+     }
+     return ret
+   }
+   ```
+
+   Now the type checker will warn us that we aren't accounting for `c` (or any
+   additional alternatives added down the line).
+
 ### Using Either
 
 TODO
@@ -186,7 +277,7 @@ executable and the VSCode plugin.
 
   This will trigger the release and publication of the package to npm and
   GitHub.
-  
+
 ### VSCode Plugin
 
 #### Prerequisites
@@ -207,10 +298,9 @@ executable and the VSCode plugin.
   - Run `vsce publish`
     - requires access to https://dev.azure.com/informalsystems/
     - which allows creating the required PAT (see
-      https://code.visualstudio.com/api/working-with-extensions/publishing-extension) 
+      https://code.visualstudio.com/api/working-with-extensions/publishing-extension)
   - Use the web interface
     - Run `vsce package` to produce a the `.visx` archive
     - Navigate to
       https://marketplace.visualstudio.com/manage/publishers/informal, and click
       the `...` visible when hovering over `Quint` to upload the archive.
-

examples/.scripts/run-example.sh

@@ -55,7 +55,7 @@ result () {
       printf "<sup>https://github.com/informalsystems/quint/pull/1023</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" == "test" || "$cmd" == "verify" ) ]] ; then
+    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
       printf "<sup>https://github.com/informalsystems/apalache/issues/2670</sup>"

examples/README.md

@@ -76,7 +76,7 @@ listed without any additional command line arguments.
 | [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
+| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
 | [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/apalache/issues/2670</sup> |

quint/src/IRTransformer.ts

@@ -15,6 +15,7 @@
 
 import * as ir from './quintIr'
 import * as t from './quintTypes'
+import { unreachable } from './util'
 
 export class IRTransformer {
   enterModule?: (module: ir.QuintModule) => ir.QuintModule
@@ -81,6 +82,8 @@ export class IRTransformer {
   exitTupleType?: (type: t.QuintTupleType) => t.QuintTupleType
   enterRecordType?: (type: t.QuintRecordType) => t.QuintRecordType
   exitRecordType?: (type: t.QuintRecordType) => t.QuintRecordType
+  enterSumType?: (type: t.QuintSumType) => t.QuintSumType
+  exitSumType?: (type: t.QuintSumType) => t.QuintSumType
   enterUnionType?: (type: t.QuintUnionType) => t.QuintUnionType
   exitUnionType?: (type: t.QuintUnionType) => t.QuintUnionType
 
@@ -247,6 +250,18 @@ export function transformType(transformer: IRTransformer, type: t.QuintType): t.
         newType = transformer.exitUnionType(newType)
       }
       break
+
+    case 'sum':
+      if (transformer.enterSumType) {
+        newType = transformer.enterSumType(newType)
+      }
+      if (transformer.exitSumType) {
+        newType = transformer.exitSumType(newType)
+      }
+      break
+
+    default:
+      unreachable(newType)
   }
 
   if (transformer.exitType) {
@@ -346,6 +361,8 @@ export function transformDefinition(transformer: IRTransformer, def: ir.QuintDef
         newDef = transformer.exitAssume(newDef)
       }
       break
+    default:
+      unreachable(newDef)
   }
   if (transformer.exitDef) {
     newDef = transformer.exitDef(newDef)
@@ -410,26 +427,30 @@ function transformExpression(transformer: IRTransformer, expr: ir.QuintEx): ir.Q
         newExpr = transformer.exitLambda(newExpr)
       }
       break
-    case 'let': {
-      if (transformer.enterLet) {
-        newExpr = transformer.enterLet(newExpr)
-      }
-
-      const opdef = transformDefinition(transformer, newExpr.opdef)
-      if (opdef.kind !== 'def') {
-        // This should only happen if we write a bad transformer. Should never
-        // be a user facing issue.
-        throw new Error('Let operator definition transformed into non-operator definition')
-      }
-
-      newExpr.opdef = opdef
-      newExpr.expr = transformExpression(transformer, newExpr.expr)
-
-      if (transformer.exitLet) {
-        newExpr = transformer.exitLet(newExpr)
+    case 'let':
+      {
+        if (transformer.enterLet) {
+          newExpr = transformer.enterLet(newExpr)
+        }
+
+        const opdef = transformDefinition(transformer, newExpr.opdef)
+        if (opdef.kind !== 'def') {
+          // This should only happen if we write a bad transformer. Should never
+          // be a user facing issue.
+          throw new Error('Let operator definition transformed into non-operator definition')
+        }
+
+        newExpr.opdef = opdef
+        newExpr.expr = transformExpression(transformer, newExpr.expr)
+
+        if (transformer.exitLet) {
+          newExpr = transformer.exitLet(newExpr)
+        }
       }
       break
-    }
+
+    default:
+      unreachable(newExpr)
   }
 
   if (transformer.exitExpr) {

quint/src/IRVisitor.ts

@@ -15,6 +15,7 @@
 
 import * as ir from './quintIr'
 import * as t from './quintTypes'
+import { unreachable } from './util'
 
 /**
  * Interface to be implemented by visitor classes.
@@ -81,6 +82,8 @@ export interface IRVisitor {
   exitTupleType?: (_type: t.QuintTupleType) => void
   enterRecordType?: (_type: t.QuintRecordType) => void
   exitRecordType?: (_type: t.QuintRecordType) => void
+  enterSumType?: (_type: t.QuintSumType) => void
+  exitSumType?: (_type: t.QuintSumType) => void
   enterUnionType?: (_type: t.QuintUnionType) => void
   exitUnionType?: (_type: t.QuintUnionType) => void
 
@@ -242,6 +245,14 @@ export function walkType(visitor: IRVisitor, type: t.QuintType): void {
         visitor.exitUnionType(type)
       }
       break
+
+    case 'sum':
+      visitor.enterSumType?.(type)
+      visitor.exitSumType?.(type)
+      break
+
+    default:
+      unreachable(type)
   }
 
   if (visitor.exitType) {
@@ -393,6 +404,8 @@ function walkExpression(visitor: IRVisitor, expr: ir.QuintEx): void {
         visitor.exitLet(expr)
       }
       break
+    default:
+      unreachable(expr)
   }
 
   if (visitor.exitExpr) {
@@ -432,6 +445,9 @@ function walkRow(visitor: IRVisitor, r: t.Row) {
       if (visitor.exitEmptyRow) {
         visitor.exitEmptyRow(r)
       }
+      break
+    default:
+      unreachable(r)
   }
   if (visitor.exitRow) {
     visitor.exitRow(r)

quint/src/cliCommands.ts

@@ -513,34 +513,21 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
       }
     }
 
-    // If nothing found, return a success. Otherwise, return an error.
-    let msg
-    switch (result.status) {
-      case 'ok':
-        return right({
-          ...simulator,
-          status: result.status,
-          trace: result.states,
-        })
-
-      case 'violation':
-        msg = 'Invariant violated'
-        break
-
-      case 'failure':
-        msg = 'Runtime error'
-        break
-
-      default:
-        msg = 'Unknown error'
+    if (result.status === 'ok') {
+      return right({
+        ...simulator,
+        status: result.status,
+        trace: result.states,
+      })
+    } else {
+      const msg = result.status === 'violation' ? 'Invariant violated' : 'Runtime error'
+      return cliErr(msg, {
+        ...simulator,
+        status: result.status,
+        trace: result.states,
+        errors: result.errors,
+      })
     }
-
-    return cliErr(msg, {
-      ...simulator,
-      status: result.status,
-      trace: result.states,
-      errors: result.errors,
-    })
   }
 }
 

quint/src/effects/EffectVisitor.ts

@@ -13,6 +13,7 @@
  * @module
  */
 
+import { unreachable } from '../util'
 import { ArrowEffect, ConcreteEffect, Effect, EffectVariable } from './base'
 
 /**
@@ -58,17 +59,21 @@ export function walkEffect(visitor: EffectVisitor, effect: Effect): void {
       }
       break
     }
-    case 'arrow': {
-      if (visitor.enterArrow) {
-        visitor.enterArrow(effect)
-      }
+    case 'arrow':
+      {
+        if (visitor.enterArrow) {
+          visitor.enterArrow(effect)
+        }
 
-      effect.params.forEach(e => walkEffect(visitor, e))
-      walkEffect(visitor, effect.result)
+        effect.params.forEach(e => walkEffect(visitor, e))
+        walkEffect(visitor, effect.result)
 
-      if (visitor.exitArrow) {
-        visitor.exitArrow(effect)
+        if (visitor.exitArrow) {
+          visitor.exitArrow(effect)
+        }
       }
-    }
+      break
+    default:
+      unreachable(effect)
   }
 }

quint/src/effects/builtinSignatures.ts

@@ -15,6 +15,7 @@
 import { ComponentKind, Effect, EffectComponent, EffectScheme, Entity, Signature, effectNames, toScheme } from './base'
 import { parseEffectOrThrow } from './parser'
 import { range, times } from 'lodash'
+import { QuintBuiltinOpcode } from '../quintIr'
 
 export function getSignatures(): Map<string, Signature> {
   return new Map<string, Signature>(fixedAritySignatures.concat(multipleAritySignatures))
@@ -227,7 +228,7 @@ const otherOperators = [
   },
 ]
 
-const multipleAritySignatures: [string, Signature][] = [
+const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [
   ['List', standardPropagation],
   ['Set', standardPropagation],
   ['Map', standardPropagation],