Fix handling of wildcard match cases

examples/language-features/option.qnt

@@ -37,4 +37,9 @@ module option {
     },
     outcome' = SumVotes
   }
+
+  run matchWithDefaultTest = {
+    val expected = match Some(42) { _ => "default" }
+    assert(expected == "default")
+  }
 }

quint/src/parsing/ToIrListener.ts

@@ -998,27 +998,16 @@ export class ToIrListener implements QuintListener {
   private formMatchCase([caseExpr, caseCtx]: [QuintEx, p.MatchSumCaseContext]): (QuintStr | QuintLambda)[] {
     const labelId = this.getId(caseCtx)
     const elimId = this.getId(caseCtx)
-    let label: string
-    let params: QuintLambdaParameter[]
-    if (caseCtx._wildCardMatch) {
-      // a wildcard case: _ => expr
-      label = '_'
-      params = []
-    } else if (caseCtx._variantMatch) {
-      const variant = caseCtx._variantMatch
-      let name: string
-      if (variant._variantParam) {
-        name = variant._variantParam.text
-      } else {
-        // We either have a hole or no param specified, in which case our lambda only needs a hole
-        name = '_'
-      }
-      label = variant._variantLabel.text
-      params = [{ name, id: this.getId(variant) }]
-    } else {
-      throw new Error('impossible: either _wildCardMatch or _variantMatch must be present')
-    }
+    const variantMatch = caseCtx._variantMatch
+
+    // If there is not a variant param, then we have a wildcard case, `_ => foo`, or a hole in the paramater position, `Foo(_) => bar`
+    const name = variantMatch && variantMatch._variantParam ? variantMatch._variantParam.text : '_'
+    const params = [{ name, id: this.getId(caseCtx) }]
+
+    // If there is not a variant label, then we have a wildcard case
+    const label = variantMatch ? variantMatch._variantLabel.text : '_'
     const labelStr: QuintStr = { id: labelId, kind: 'str', value: label }
+
     const elim: QuintLambda = { id: elimId, kind: 'lambda', qualifier: 'def', expr: caseExpr, params }
     return [labelStr, elim]
   }

quint/src/runtime/impl/compilerImpl.ts

@@ -713,12 +713,7 @@ export class CompilerVisitor implements IRVisitor {
             let result: Maybe<RuntimeValue> | undefined
             for (const [caseLabel, caseElim] of chunk(cases, 2)) {
               const caseLabelStr = caseLabel.toStr()
-              if (caseLabelStr === '_') {
-                // The wilcard case ignores the value.
-                // NOTE: This SHOULD be a nullary lambda, but by this point the compiler
-                // has already converted it into a value. Confusing!
-                result = just(caseElim as RuntimeValueLambda)
-              } else if (caseLabelStr === label) {
+              if (caseLabelStr === '_' || caseLabelStr === label) {
                 // Type checking ensures the second item of each case is a lambda
                 const eliminator = caseElim as RuntimeValueLambda
                 result = eliminator.eval([just(value)]).map(r => r as RuntimeValue)

quint/src/types/specialConstraints.ts

@@ -256,39 +256,46 @@ export function matchConstraints(
   // Now we verify that each label is a string literal and each eliminator is a unary operator.
   // This is a well-formedness check prior to checking that the match expression fits the
   // `sumType` of the value we are matching on.
-  const fieldValidationError: (msg: string) => Either<ErrorTree, [string, QuintType]> = msg =>
-    left(buildErrorLeaf(`Generating match constraints for ${labelsAndcases.map(a => expressionToString(a[0]))}`, msg))
-
-  const validatedFields: Either<ErrorTree, [string, QuintType]>[] = labelAndElimPairs.map(
-    ([[labelExpr, _labelType], [elimExpr, elimType]]) => {
-      return labelExpr.kind !== 'str'
-        ? fieldValidationError(
-            `Match variant name must be a string literal but it is a ${labelExpr.kind}: ${expressionToString(
-              labelExpr
-            )}`
-          )
-        : elimType.kind !== 'oper'
-        ? fieldValidationError(
-            `Match case eliminator must be an operator expression but it is a ${elimType.kind}: ${expressionToString(
-              elimExpr
-            )}`
-          )
-        : elimType.args.length !== 1
-        ? fieldValidationError(
-            `Match case eliminator must be a unary operator but it is an operator of ${
-              elimType.args.length
-            } arguments: ${expressionToString(elimExpr)}`
-          )
-        : right([labelExpr.value, elimType.args[0]]) // The label and associated type of a varaint case
-    }
-  )
+  const validatedFields: Either<ErrorTree, [string, QuintType]>[] = []
+  const fieldValidationError = (msg: string) =>
+    validatedFields.push(
+      left(buildErrorLeaf(`Generating match constraints for ${labelsAndcases.map(a => expressionToString(a[0]))}`, msg))
+    )
+  let wildCardMatch = false
+  for (const [[labelExpr, _labelType], [elimExpr, elimType]] of labelAndElimPairs) {
+    labelExpr.kind !== 'str'
+      ? fieldValidationError(
+          `Match variant name must be a string literal but it is a ${labelExpr.kind}: ${expressionToString(labelExpr)}`
+        )
+      : elimType.kind !== 'oper'
+      ? fieldValidationError(
+          `Match case eliminator must be an operator expression but it is a ${elimType.kind}: ${expressionToString(
+            elimExpr
+          )}`
+        )
+      : elimType.args.length !== 1
+      ? fieldValidationError(
+          `Match case eliminator must be a unary operator but it is an operator of ${
+            elimType.args.length
+          } arguments: ${expressionToString(elimExpr)}`
+        )
+      : !wildCardMatch && labelExpr.value === '_'
+      ? (wildCardMatch = true) // The wildcard case, `_ => foo`, means we can match anything else
+      : wildCardMatch // There should only ever be 1 wilcard match, and it should be the last case
+      ? fieldValidationError(
+          `Invalid wildcard match ('_') in match expression: ${expressionToString(
+            elimExpr
+          )}. Only one wildcard can appear and it must be the final case of a match.`
+        )
+      : validatedFields.push(right([labelExpr.value, elimType.args[0]])) // The label and associated type of a variant case
+  }
 
   // TODO: Support more expressive and informative type errors.
   //       This will require tying into the constraint checking system.
   //       See https://github.com/informalsystems/quint/issues/1231
   return mergeInMany(validatedFields).map((fields: [string, QuintType][]): Constraint[] => {
     // Form a constraint ensuring that the match expression fits the sum-type it is applied to:
-    const matchCaseType = sumType(fields) // The sum-type implied by the match elimination cases.
+    const matchCaseType = wildCardMatch ? sumType(fields, `${resultTypeVar.name}_wildcard`) : sumType(fields) // The sum-type implied by the match elimination cases.
     // s ~ < i1 : t1, ..., in : tn > )
     const variantTypeIsMatchCaseType: Constraint = { kind: 'eq', types: [variantType, matchCaseType], sourceId: id }
 

quint/test/types/inferrer.test.ts

@@ -197,6 +197,13 @@ describe('inferTypes', () => {
     ])
   })
 
+  it('infers types for match expression with wildcard case', () => {
+    const defs = ['type T = A(int) | B', 'val nine : int = match B { _ => 9 }']
+
+    const [errors, _] = inferTypesForDefs(defs)
+    assert.isEmpty(errors)
+  })
+
   it('reports a type error for match expressions that return inconsitent types in cases', () => {
     const defs = [
       'type T = A(int) | B',
@@ -209,6 +216,30 @@ describe('inferTypes', () => {
     assert.match([...errors.values()].map(errorTreeToString)[0], RegExp("Couldn't unify int and str"))
   })
 
+  it('reports a type error for match expressions with multiple wildcard cases', () => {
+    const defs = [
+      'type T = A(int) | B | C',
+      'val a = variant("A", 3)',
+      'val nine = match B { A(n) => "OK" | _ => "first wilcard" | _ => "second, invalid wildcard" }',
+    ]
+
+    const [errors, _] = inferTypesForDefs(defs)
+    assert.isNotEmpty(errors)
+    assert.match([...errors.values()].map(errorTreeToString)[0], RegExp('Invalid wildcard match'))
+  })
+
+  it('reports a type error for match expressions with non-final wildcard case', () => {
+    const defs = [
+      'type T = A(int) | B | C',
+      'val a = variant("A", 3)',
+      'val nine = match B { A(n) => "OK" | _ => "invalid, non-final wilcard" | C => "OK" }',
+    ]
+
+    const [errors, _] = inferTypesForDefs(defs)
+    assert.isNotEmpty(errors)
+    assert.match([...errors.values()].map(errorTreeToString)[0], RegExp('Invalid wildcard match'))
+  })
+
   it('reports a type error for match expressions on non-variant expressions', () => {
     const defs = [
       'val notAVariant = "this is not a variant"',
@@ -221,7 +252,7 @@ describe('inferTypes', () => {
   })
 
   it('reports a type error for matchVariant operator with non-label arguments', () => {
-    const defs = ['type T = A(int) | B', 'val a = variant("A", 3)', 'val nine = matchVariant(a, 3, 9)']
+    const defs = ['type T = A(int) | B', 'val a = variant("A", 3)', 'val nine = matchVariant(a, 3, (_ => 9))']
 
     const [errors, _] = inferTypesForDefs(defs)
     assert.isNotEmpty(errors)

quint/testFixture/_1044matchExpression.json

@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"modules":[{"id":39,"name":"SumTypes","declarations":[{"id":4,"name":"T","kind":"typedef","type":{"id":4,"kind":"sum","fields":{"kind":"row","fields":[{"fieldName":"A","fieldType":{"id":1,"kind":"rec","fields":{"kind":"row","fields":[],"other":{"kind":"empty"}}}},{"fieldName":"B","fieldType":{"id":2,"kind":"int"}},{"fieldName":"C","fieldType":{"id":3,"kind":"str"}}],"other":{"kind":"empty"}}}},{"id":14,"kind":"def","name":"B","qualifier":"def","typeAnnotation":{"kind":"oper","args":[{"id":2,"kind":"int"}],"res":{"id":4,"kind":"const","name":"T"}},"expr":{"id":13,"kind":"lambda","params":[{"id":10,"name":"__BParam"}],"qualifier":"def","expr":{"id":12,"kind":"app","opcode":"variant","args":[{"id":9,"kind":"str","value":"B"},{"kind":"name","name":"__BParam","id":11}]}}},{"id":20,"kind":"def","name":"C","qualifier":"def","typeAnnotation":{"kind":"oper","args":[{"id":3,"kind":"str"}],"res":{"id":4,"kind":"const","name":"T"}},"expr":{"id":19,"kind":"lambda","params":[{"id":16,"name":"__CParam"}],"qualifier":"def","expr":{"id":18,"kind":"app","opcode":"variant","args":[{"id":15,"kind":"str","value":"C"},{"kind":"name","name":"__CParam","id":17}]}}},{"id":8,"kind":"def","name":"A","qualifier":"val","typeAnnotation":{"id":4,"kind":"const","name":"T"},"expr":{"id":7,"kind":"app","opcode":"variant","args":[{"id":5,"kind":"str","value":"A"},{"id":6,"kind":"app","opcode":"Rec","args":[]}]}},{"id":23,"kind":"def","name":"c","qualifier":"val","expr":{"id":22,"kind":"app","opcode":"C","args":[{"id":21,"kind":"str","value":"Foo"}]}},{"id":38,"kind":"def","name":"ex","qualifier":"val","expr":{"id":29,"kind":"app","opcode":"matchVariant","args":[{"id":24,"kind":"name","name":"c"},{"id":30,"kind":"str","value":"A"},{"id":31,"kind":"lambda","qualifier":"def","expr":{"id":25,"kind":"int","value":0},"params":[{"name":"_","id":32}]},{"id":33,"kind":"str","value":"B"},{"id":34,"kind":"lambda","qualifier":"def","expr":{"id":26,"kind":"name","name":"n"},"params":[{"name":"n","id":35}]},{"id":36,"kind":"str","value":"_"},{"id":37,"kind":"lambda","qualifier":"def","expr":{"id":28,"kind":"app","opcode":"iuminus","args":[{"id":27,"kind":"int","value":1}]},"params":[]}]}}]}],"table":{"4":{"id":4,"name":"T","kind":"typedef","type":{"id":4,"kind":"sum","fields":{"kind":"row","fields":[{"fieldName":"A","fieldType":{"id":1,"kind":"rec","fields":{"kind":"row","fields":[],"other":{"kind":"empty"}}}},{"fieldName":"B","fieldType":{"id":2,"kind":"int"}},{"fieldName":"C","fieldType":{"id":3,"kind":"str"}}],"other":{"kind":"empty"}}}},"11":{"id":10,"name":"__BParam","kind":"param"},"17":{"id":16,"name":"__CParam","kind":"param"},"22":{"id":20,"kind":"def","name":"C","qualifier":"def","expr":{"id":19,"kind":"lambda","params":[{"id":16,"name":"__CParam"}],"qualifier":"def","expr":{"id":18,"kind":"app","opcode":"variant","args":[{"id":15,"kind":"str","value":"C"},{"kind":"name","name":"__CParam","id":17}]}},"depth":0},"24":{"id":23,"kind":"def","name":"c","qualifier":"val","expr":{"id":22,"kind":"app","opcode":"C","args":[{"id":21,"kind":"str","value":"Foo"}]},"depth":0},"26":{"name":"n","id":35,"kind":"param"}},"errors":[]}
+{"stage":"parsing","warnings":[],"modules":[{"id":40,"name":"SumTypes","declarations":[{"id":4,"name":"T","kind":"typedef","type":{"id":4,"kind":"sum","fields":{"kind":"row","fields":[{"fieldName":"A","fieldType":{"id":1,"kind":"rec","fields":{"kind":"row","fields":[],"other":{"kind":"empty"}}}},{"fieldName":"B","fieldType":{"id":2,"kind":"int"}},{"fieldName":"C","fieldType":{"id":3,"kind":"str"}}],"other":{"kind":"empty"}}}},{"id":14,"kind":"def","name":"B","qualifier":"def","typeAnnotation":{"kind":"oper","args":[{"id":2,"kind":"int"}],"res":{"id":4,"kind":"const","name":"T"}},"expr":{"id":13,"kind":"lambda","params":[{"id":10,"name":"__BParam"}],"qualifier":"def","expr":{"id":12,"kind":"app","opcode":"variant","args":[{"id":9,"kind":"str","value":"B"},{"kind":"name","name":"__BParam","id":11}]}}},{"id":20,"kind":"def","name":"C","qualifier":"def","typeAnnotation":{"kind":"oper","args":[{"id":3,"kind":"str"}],"res":{"id":4,"kind":"const","name":"T"}},"expr":{"id":19,"kind":"lambda","params":[{"id":16,"name":"__CParam"}],"qualifier":"def","expr":{"id":18,"kind":"app","opcode":"variant","args":[{"id":15,"kind":"str","value":"C"},{"kind":"name","name":"__CParam","id":17}]}}},{"id":8,"kind":"def","name":"A","qualifier":"val","typeAnnotation":{"id":4,"kind":"const","name":"T"},"expr":{"id":7,"kind":"app","opcode":"variant","args":[{"id":5,"kind":"str","value":"A"},{"id":6,"kind":"app","opcode":"Rec","args":[]}]}},{"id":23,"kind":"def","name":"c","qualifier":"val","expr":{"id":22,"kind":"app","opcode":"C","args":[{"id":21,"kind":"str","value":"Foo"}]}},{"id":39,"kind":"def","name":"ex","qualifier":"val","expr":{"id":29,"kind":"app","opcode":"matchVariant","args":[{"id":24,"kind":"name","name":"c"},{"id":30,"kind":"str","value":"A"},{"id":31,"kind":"lambda","qualifier":"def","expr":{"id":25,"kind":"int","value":0},"params":[{"name":"_","id":32}]},{"id":33,"kind":"str","value":"B"},{"id":34,"kind":"lambda","qualifier":"def","expr":{"id":26,"kind":"name","name":"n"},"params":[{"name":"n","id":35}]},{"id":36,"kind":"str","value":"_"},{"id":37,"kind":"lambda","qualifier":"def","expr":{"id":28,"kind":"app","opcode":"iuminus","args":[{"id":27,"kind":"int","value":1}]},"params":[{"name":"_","id":38}]}]}}]}],"table":{"4":{"id":4,"name":"T","kind":"typedef","type":{"id":4,"kind":"sum","fields":{"kind":"row","fields":[{"fieldName":"A","fieldType":{"id":1,"kind":"rec","fields":{"kind":"row","fields":[],"other":{"kind":"empty"}}}},{"fieldName":"B","fieldType":{"id":2,"kind":"int"}},{"fieldName":"C","fieldType":{"id":3,"kind":"str"}}],"other":{"kind":"empty"}}}},"11":{"id":10,"name":"__BParam","kind":"param"},"17":{"id":16,"name":"__CParam","kind":"param"},"22":{"id":20,"kind":"def","name":"C","qualifier":"def","expr":{"id":19,"kind":"lambda","params":[{"id":16,"name":"__CParam"}],"qualifier":"def","expr":{"id":18,"kind":"app","opcode":"variant","args":[{"id":15,"kind":"str","value":"C"},{"kind":"name","name":"__CParam","id":17}]}},"depth":0},"24":{"id":23,"kind":"def","name":"c","qualifier":"val","expr":{"id":22,"kind":"app","opcode":"C","args":[{"id":21,"kind":"str","value":"Foo"}]},"depth":0},"26":{"name":"n","id":35,"kind":"param"}},"errors":[]}