From d98c1d0b2790411e47bfa4dd8f0a420e133aef0a Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Thu, 5 Oct 2023 22:04:16 -0400
Subject: [PATCH 01/13] Remove `unionMatch`

---
 doc/lang.md                                | 125 ---------------------
 quint/src/builtin.qnt                      |  22 ----
 quint/src/effects/builtinSignatures.ts     |   2 +-
 quint/src/ir/quintIr.ts                    |   1 -
 quint/src/names/base.ts                    |   1 -
 quint/src/runtime/impl/compilerImpl.ts     |   1 -
 quint/src/types/builtinSignatures.ts       |  15 ++-
 quint/test/types/builtinSignatures.test.ts |  18 ---
 8 files changed, 10 insertions(+), 175 deletions(-)

diff --git a/doc/lang.md b/doc/lang.md
index 7d4356a4a..b7b29dcf0 100644
--- a/doc/lang.md
+++ b/doc/lang.md
@@ -1295,131 +1295,6 @@ with discriminated unions.
 
 *Mode:* Stateless, State. Other modes are not allowed.
 
-### Discriminated unions (work-in-progress)
-
-**WARNING:** *We are redesigning discriminated unions*, see
-[#539](https://github.com/informalsystems/quint/issues/539). *As they are not
-fully implemented, please avoid using discriminated unions for now*.
-
-Quint has provides the user with special syntax for constructing and destructing
-discriminated unions.  For the type syntax of discriminated unions, see
-[Types](#types).
-
-**Constructors.** Construct a tagged record by using the record syntax, e.g.:
-
-```scala
-  { tag: "Cat", name: "Ours", year: 2019 }
-```
-
-Note that the above record has the field `tag`. Hence, this record is assigned
-a union type of one element:
-
-```scala
-type CAT_TYPE =
-  | { tag: "Cat", name: str, year: int }
-```
-
-Records of different union types may be mixed in a single set. For example:
-
-```scala
-val Entries =
-  Set(
-    { tag: "Cat", name: "Ours", year: 2019  },
-    { tag: "Cat", name: "Murka", year: 1950 },
-    { tag: "Date", day: 16, month: 11, year: 2021 }
-  )
-```
-
-In the above example, the set elements have the following union type:
-
-```scala
-type ENTRY_TYPE =
-  | { tag: "Cat", name: str, year: int }
-  | { tag: "Date", day: int, month: int, year: int }
-```
-
-When we construct the individual records, they still have singleton union
-types.  For instance, the entry  `{ tag: "Date", day: 16, month: 11, year: 2021
-}` has the type:
-
-```scala
-type DATE_TYPE =
-  { tag: "Date", day: int, month: int, year: int }
-```
-
-**Set filters.** The most common pattern over discriminated union is to filter
-set elements by their tag. Using the above definition of `Entries`, we can
-filter it as follows:
-
-```scala
-Entries.filter(e => e.tag == "Cat")
-```
-
-As expected from the semantics of `filter`, the above set is equal to:
-
-```
-Set(
-  { tag: "Cat", name: "Ours", year: 2019  },
-  { tag: "Cat", name: "Murka", year: 1950 }
-)
-```
-
-Importantly, its elements have the type:
-
-```scala
-type CAT_TYPE =
-  | { tag: "Cat", name: str, year: int }
-```
-
-**Destructors.** Sometimes, we have a value of a union type that is not stored
-in a set. For this case, Quint has the union destructor syntax.  For example,
-given an entry from `Entries`, we can compute the predicate `isValid` by case
-distinction over tags:
-
-```scala
-pure def isValid(entry): ENTRY_TYPE => bool =
-  entry match
-     | "Cat": cat =>
-       name != "" and cat.year > 0
-     | "Date": date =>
-       date.day.in(1 to 31) and date.month.in(1.to(12)) and date.year > 0
-```
-
-In the above example, the names `cat` and `date` have the singleton union types
-of `CAT_TYPE` and `DATE_TYPE`, respectively. Note that the expressions after
-the tag name (e.g., `"Cat":` and `"Date":`) follow the syntax of
-single-argument lambda expressions. As a result, we can use `_` as a name,
-which means that the name is omitted.
-
-Match expressions require all possible values of `tag` to be enumerated. This is
-ensured by the type checker.
-
-We do not introduce parentheses in the syntax of `match`. If you feel uncomfortable
-about it, wrap the whole match-expression with `(...)`.
-
-*Grammar*:
-
-```bnf
-  expr "match" ("|" string ":" (identifier | "_") "=>" expr)+
-```
-
-*Normal form*: Consider the match operator:
-
-```scala
-  ex match
-    | tag_1: x_1 => ex_1
-    ...
-    | tag_n: x_n => ex_n
-```
-
-Its normal form is `unionMatch(ex, tag_1, (x_1 => ex_1), ..., (x_n => ex_n))`.
-
-*Mode:* Stateless, State. Other modes are not allowed.
-
-**Discussion.** In TLA+, there is no separation between discriminated unions
-and records. It is common to use tagged records to distinguish between different
-cases of records. Quint makes this pattern explicit.
-
 ### Tuples
 
 In contrast to TLA+, Quint tuples have length of at least 2.
diff --git a/quint/src/builtin.qnt b/quint/src/builtin.qnt
index 0052fd536..3c4e4579c 100644
--- a/quint/src/builtin.qnt
+++ b/quint/src/builtin.qnt
@@ -1024,26 +1024,4 @@ module builtin {
   // /// run test = (x' = 0).then(any { x' = 1, x' = 2 }).then(assert(or { x == 1, x == 2 }))
   // /// ```
   // pure def actionAny(a*): (bool*) => bool
-
-  // /// `unionMatch(m, (t0, e0), ..., (tn, en))` is the expression `ei` when `ti` is the tag of `m`.
-  // ///
-  // /// The behavior of this operator is undefined if the tag isn't one of the `ti`s.
-  // ///
-  // /// This is the pattern matching operator.
-  // ///
-  // /// Can also be written as `m match | t0: e0, ..., | tn: en }`.
-  // ///
-  // /// ### Examples
-  // ///
-  // /// ```
-  // /// pure val total(w) = w match
-  // ///   // this pattern binds some_w to the "some" version of w, if w.tag == "some"
-  // ///   | "some": some_w => some_w.value
-  // ///   // this pattern
-  // ///   | "none": _ => 0
-  // ///
-  // /// assert(total({ tag = "some", value = 1 }) == 1)
-  // /// assert(total({ tag = "none" }) == 0)
-  // /// ```
-  // pure def unionMatch(m, (t, e)*): (a, (b, ((b) => c))*) => c
 }
diff --git a/quint/src/effects/builtinSignatures.ts b/quint/src/effects/builtinSignatures.ts
index 3111e3ab8..4cb5a2d60 100644
--- a/quint/src/effects/builtinSignatures.ts
+++ b/quint/src/effects/builtinSignatures.ts
@@ -238,7 +238,7 @@ const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [
   ['and', standardPropagation],
   ['or', standardPropagation],
   [
-    'unionMatch',
+    'match',
     (arity: number) => {
       const readVars = times((arity - 1) / 2, i => `r${i}`)
       const args = readVars.map(r => `Pure, (Pure) => Read[${r}]`)
diff --git a/quint/src/ir/quintIr.ts b/quint/src/ir/quintIr.ts
index e5c92e20d..cfd0e517e 100644
--- a/quint/src/ir/quintIr.ts
+++ b/quint/src/ir/quintIr.ts
@@ -209,7 +209,6 @@ export const builtinOpCodes = [
   'to',
   'tuples',
   'union',
-  'unionMatch',
   'variant',
   'weakFair',
   'with',
diff --git a/quint/src/names/base.ts b/quint/src/names/base.ts
index c4edf2631..6c2c3c03a 100644
--- a/quint/src/names/base.ts
+++ b/quint/src/names/base.ts
@@ -226,7 +226,6 @@ export const builtinNames = [
   'field',
   'fieldNames',
   'item',
-  'unionMatch',
   'assign',
   'of',
   'eq',
diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts
index a9cc0b4f4..36f15597b 100644
--- a/quint/src/runtime/impl/compilerImpl.ts
+++ b/quint/src/runtime/impl/compilerImpl.ts
@@ -930,7 +930,6 @@ export class CompilerVisitor implements IRVisitor {
           break
 
         // builtin operators that are not handled by REPL
-        case 'unionMatch':
         case 'variant': // TODO: https://github.com/informalsystems/quint/issues/1033
         case 'match': // TODO: https://github.com/informalsystems/quint/issues/1033
         case 'orKeep':
diff --git a/quint/src/types/builtinSignatures.ts b/quint/src/types/builtinSignatures.ts
index 90f0610c4..528aed63c 100644
--- a/quint/src/types/builtinSignatures.ts
+++ b/quint/src/types/builtinSignatures.ts
@@ -13,7 +13,7 @@
  */
 
 import { parseTypeOrThrow } from './parser'
-import { typeNames } from '../ir/quintTypes'
+import { sumType, typeNames } from '../ir/quintTypes'
 import { Signature, TypeScheme } from './base'
 import { times } from 'lodash'
 import { QuintBuiltinOpcode } from '../ir/quintIr'
@@ -22,9 +22,13 @@ export function getSignatures(): Map<string, Signature> {
   return new Map<string, Signature>(fixedAritySignatures.concat(multipleAritySignatures))
 }
 
-// Signatures for record and tuple related operators cannot be precisely
-// defined with this syntax. Their types are handled directly with constraints
-// in the specialConstraints.ts file
+// NOTE: Signatures operations over products (records and tuples) and sums
+// (unums/disjoint unions/variants) cannot be precisely defined with this
+// syntax, because they are "exotic", in the senes that relect basic language
+// constructions that cannot be represented  in the type system of the language
+// itself.
+//
+// Their types are handled directly with constraints in the specialConstraints.ts file.
 
 const literals = [
   { name: 'Nat', type: 'Set[int]' },
@@ -130,7 +134,6 @@ function uniformArgsWithResult(argsType: string, resultType: string): Signature
   }
 }
 
-// TODO: check arity conditions, see issue https://github.com/informalsystems/quint/issues/169
 const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [
   ['List', uniformArgsWithResult('a', 'List[a]')],
   ['Set', uniformArgsWithResult('a', 'Set[a]')],
@@ -140,7 +143,7 @@ const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [
   ['or', uniformArgsWithResult('bool', 'bool')],
   ['actionAny', uniformArgsWithResult('bool', 'bool')],
   [
-    'unionMatch',
+    'match',
     (arity: number) => {
       const args = times((arity - 1) / 2, () => 'str, (a) => b')
       return parseAndQuantify(`(a, ${args.join(', ')}) => b`)
diff --git a/quint/test/types/builtinSignatures.test.ts b/quint/test/types/builtinSignatures.test.ts
index e0135d7bd..a5ddfe69e 100644
--- a/quint/test/types/builtinSignatures.test.ts
+++ b/quint/test/types/builtinSignatures.test.ts
@@ -26,24 +26,6 @@ describe('getSignatures', () => {
     )
   })
 
-  it('contains quantified signatures for match', () => {
-    const matchSignature = signatures.get('unionMatch')!
-
-    const expectedSignature: TypeScheme = {
-      type: parseTypeOrThrow('(a, str, (a) => b, str, (a) => b) => b'),
-      typeVariables: new Set(['a', 'b']),
-      rowVariables: new Set([]),
-    }
-
-    const result = matchSignature(5)
-
-    assert.deepEqual(
-      result,
-      expectedSignature,
-      `expected ${typeSchemeToString(expectedSignature)}, got ${typeSchemeToString(result)}`
-    )
-  })
-
   it('contains quantified signatures for tuples', () => {
     const tuplesSignature = signatures.get('tuples')!
 

From c3515da8780eb8d0ea0f52fdf6458ae35b2f929e Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Thu, 5 Oct 2023 22:07:04 -0400
Subject: [PATCH 02/13] Improve printing of sum types

---
 quint/src/graphics.ts            |  9 ++++++---
 quint/src/ir/IRprinting.ts       | 22 +++++++++++++---------
 quint/src/types/printing.ts      |  2 ++
 quint/test/ir/IRprinting.test.ts |  2 +-
 4 files changed, 22 insertions(+), 13 deletions(-)

diff --git a/quint/src/graphics.ts b/quint/src/graphics.ts
index 99e541041..d15e29a15 100644
--- a/quint/src/graphics.ts
+++ b/quint/src/graphics.ts
@@ -29,7 +29,7 @@ import {
 import { QuintDeclaration, QuintEx, isAnnotatedDef } from './ir/quintIr'
 import { ExecutionFrame } from './runtime/trace'
 import { zerog } from './idGenerator'
-import { ConcreteFixedRow, QuintType, Row } from './ir/quintTypes'
+import { ConcreteFixedRow, ConcreteRow, isUnitType, QuintType, Row } from './ir/quintTypes'
 import { TypeScheme } from './types/base'
 import { canonicalTypeScheme } from './types/printing'
 import { declarationToString, qualifierToString, rowToString } from './ir/IRprinting'
@@ -220,7 +220,7 @@ function prettyRow(r: Row, showFieldName = true): Doc {
   return group([nest('  ', [linebreak, docJoin([text(','), line()], fieldsDocs)]), ...otherDoc, linebreak])
 }
 
-function prettySumRow(r: ConcreteFixedRow): Doc {
+function prettySumRow(r: ConcreteRow): Doc {
   const row = simplifyRow(r)
   const fields = row.kind === 'row' ? row.fields : []
   const other = row.kind === 'row' ? row.other : undefined
@@ -228,12 +228,15 @@ function prettySumRow(r: ConcreteFixedRow): Doc {
   const fieldsDocs = fields.map(f => {
     if (other?.kind === 'empty') {
       return group(text(f.fieldName))
+    } else if (isUnitType(f.fieldType)) {
+      // Print the variant `Foo({})`
+      return group([text(`${f.fieldName}`)])
     } else {
       return group([text(`${f.fieldName}(`), prettyQuintType(f.fieldType), text(')')])
     }
   })
 
-  return group([nest('  ', [linebreak, docJoin([text(','), line()], fieldsDocs)]), linebreak])
+  return group([nest('  ', [linebreak, docJoin([text('|'), line()], fieldsDocs)]), linebreak])
 }
 
 /**
diff --git a/quint/src/ir/IRprinting.ts b/quint/src/ir/IRprinting.ts
index 3986e75cb..868b8d4a5 100644
--- a/quint/src/ir/IRprinting.ts
+++ b/quint/src/ir/IRprinting.ts
@@ -216,15 +216,19 @@ export function rowToString(r: Row): string {
  * @returns a string with the pretty printed sum
  */
 export function sumToString(s: QuintSumType): string {
-  return s.fields.fields
-    .map((f: RowField) => {
-      if (isUnitType(f.fieldType)) {
-        return `| ${f.fieldName}`
-      } else {
-        return `| ${f.fieldName}(${typeToString(f.fieldType)})`
-      }
-    })
-    .join('\n')
+  return (
+    '(' +
+    s.fields.fields
+      .map((f: RowField) => {
+        if (isUnitType(f.fieldType)) {
+          return `${f.fieldName}`
+        } else {
+          return `${f.fieldName}(${typeToString(f.fieldType)})`
+        }
+      })
+      .join(' | ') +
+    ')'
+  )
 }
 
 /**
diff --git a/quint/src/types/printing.ts b/quint/src/types/printing.ts
index 2e0e430f2..b0bc67e2f 100644
--- a/quint/src/types/printing.ts
+++ b/quint/src/types/printing.ts
@@ -16,6 +16,8 @@ export function constraintToString(c: Constraint): string {
       return `${typeToString(c.types[0])} ~ ${typeToString(c.types[1])}`
     case 'conjunction':
       return c.constraints.map(constraintToString).join(' /\\ ')
+    case 'isDefined':
+      return `${typeToString(c.type)} is defined`
     case 'empty':
       return 'true'
   }
diff --git a/quint/test/ir/IRprinting.test.ts b/quint/test/ir/IRprinting.test.ts
index 1389cfbb7..a8a6c688d 100644
--- a/quint/test/ir/IRprinting.test.ts
+++ b/quint/test/ir/IRprinting.test.ts
@@ -246,7 +246,7 @@ describe('typeToString', () => {
         other: { kind: 'empty' },
       },
     }
-    const expectedType = '| A(int)\n| B'
+    const expectedType = '(A(int) | B)'
     assert.deepEqual(typeToString(type), expectedType)
   })
 

From 063cfd43e6970a13b678038d75a4276137447cbd Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Thu, 5 Oct 2023 22:07:24 -0400
Subject: [PATCH 03/13] Add constraint generator for variant operator

This also requires adding a new constraint `isDefined` that holds iff a
type that unifies with the given type is defined in the context.
---
 quint/src/ir/quintTypes.ts                   | 12 +++++-
 quint/src/types/base.ts                      |  8 +++-
 quint/src/types/constraintGenerator.ts       |  4 ++
 quint/src/types/constraintSolver.ts          | 19 ++++++++-
 quint/src/types/specialConstraints.ts        | 42 +++++++++++++++++++-
 quint/src/types/substitutions.ts             |  6 ++-
 quint/test/types/constraintGenerator.test.ts |  8 ++++
 7 files changed, 91 insertions(+), 8 deletions(-)

diff --git a/quint/src/ir/quintTypes.ts b/quint/src/ir/quintTypes.ts
index 8b9ac270f..cff99ba6f 100644
--- a/quint/src/ir/quintTypes.ts
+++ b/quint/src/ir/quintTypes.ts
@@ -89,7 +89,17 @@ export function isUnitType(r: QuintType): Boolean {
 
 export interface QuintSumType extends WithOptionalId {
   kind: 'sum'
-  fields: ConcreteFixedRow
+  fields: ConcreteRow
+}
+
+export function sumType(
+  labelTypePairs: [string, QuintType][],
+  rowVar: string | undefined,
+  id: bigint | undefined
+): QuintSumType {
+  const fields = labelTypePairs.map(([fieldName, fieldType]) => ({ fieldName, fieldType }))
+  const other: Row = rowVar ? { kind: 'var', name: rowVar } : { kind: 'empty' }
+  return { kind: 'sum', fields: { kind: 'row', fields, other }, id }
 }
 
 export interface QuintUnionType extends WithOptionalId {
diff --git a/quint/src/types/base.ts b/quint/src/types/base.ts
index 0c6ebdba4..3f66d009f 100644
--- a/quint/src/types/base.ts
+++ b/quint/src/types/base.ts
@@ -1,12 +1,16 @@
 import { QuintType } from '../ir/quintTypes'
 
 /*
- * A type constraint can be either an equality of two types, a conjunction of
- * constraints or an empty constraint
+ * Type constraints
  */
 export type Constraint =
+  /// equality of two types, defined as unifiability
   | { kind: 'eq'; types: [QuintType, QuintType]; sourceId: bigint }
+  /// a conjunction of constraints
   | { kind: 'conjunction'; constraints: Constraint[]; sourceId: bigint }
+  /// a type unifying with `type` is defined in the context
+  | { kind: 'isDefined'; type: QuintType; sourceId: bigint }
+  /// the empty constraint (always satisfied)
   | { kind: 'empty' }
 
 export interface TypeScheme {
diff --git a/quint/src/types/constraintGenerator.ts b/quint/src/types/constraintGenerator.ts
index 16bb9f789..ee48a0074 100644
--- a/quint/src/types/constraintGenerator.ts
+++ b/quint/src/types/constraintGenerator.ts
@@ -44,6 +44,7 @@ import {
   itemConstraints,
   recordConstructorConstraints,
   tupleConstructorConstraints,
+  variantConstraints,
   withConstraints,
 } from './specialConstraints'
 import { FreshVarGenerator } from '../FreshVarGenerator'
@@ -218,6 +219,9 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
             )
           case 'item':
             return validateArity(e.opcode, results, l => l === 2, '2').chain(() => itemConstraints(e.id, results, a))
+          // Sum type operators
+          case 'variant':
+            return validateArity(e.opcode, results, l => l === 2, '2').chain(() => variantConstraints(e.id, results, a))
           // Otherwise it's a standard operator with a definition in the context
           default:
             return definedSignature.map(t1 => {
diff --git a/quint/src/types/constraintSolver.ts b/quint/src/types/constraintSolver.ts
index 61fee0b28..e13044921 100644
--- a/quint/src/types/constraintSolver.ts
+++ b/quint/src/types/constraintSolver.ts
@@ -60,6 +60,23 @@ export function solveConstraint(
           .chain(newSubs => result.map(s => compose(table, newSubs, s)))
       }, right([]))
     }
+    case 'isDefined': {
+      const definedType = [...table.values()].find(def => {
+        return def.kind === 'typedef' && def.type && unify(table, def.type, constraint.type).isRight()
+      })
+      if (definedType) {
+        return right([])
+      } else {
+        errors.set(
+          constraint.sourceId,
+          buildErrorLeaf(
+            `Looking for defined type unifying with ${typeToString(constraint.type)}`,
+            'Expected type is not defined'
+          )
+        )
+        return left(errors)
+      }
+    }
     case 'empty':
       return right([])
   }
@@ -103,7 +120,7 @@ export function unify(table: LookupTable, t1: QuintType, t2: QuintType): Either<
     return unifyWithAlias(table, t1, t2)
   } else if (t2.kind === 'const') {
     return unifyWithAlias(table, t2, t1)
-  } else if (t1.kind === 'rec' && t2.kind === 'rec') {
+  } else if ((t1.kind === 'rec' && t2.kind === 'rec') || (t1.kind === 'sum' && t2.kind === 'sum')) {
     return unifyRows(table, t1.fields, t2.fields).mapLeft(error => buildErrorTree(location, error))
   } else if ((t1.kind === 'union' && t2.kind === 'rec') || (t1.kind === 'rec' && t2.kind === 'union')) {
     // FIXME: Implement discriminated unions and remove this hack, see https://github.com/informalsystems/quint/issues/244
diff --git a/quint/src/types/specialConstraints.ts b/quint/src/types/specialConstraints.ts
index de00f151f..a82977958 100644
--- a/quint/src/types/specialConstraints.ts
+++ b/quint/src/types/specialConstraints.ts
@@ -16,10 +16,11 @@
 import { Either, left, mergeInMany, right } from '@sweet-monads/either'
 import { Error, buildErrorLeaf } from '../errorTree'
 import { expressionToString } from '../ir/IRprinting'
-import { QuintEx } from '../ir/quintIr'
+import { QuintEx, QuintStr } from '../ir/quintIr'
 import { QuintType, QuintVarType } from '../ir/quintTypes'
 import { Constraint } from './base'
 import { chunk, times } from 'lodash'
+import { RowField } from '../ir/quintTypes'
 
 export function recordConstructorConstraints(
   id: bigint,
@@ -162,7 +163,7 @@ export function itemConstraints(
 
   // A tuple with item acess of N should have at least N fields
   // Fill previous fileds with type variables
-  const fields: { fieldName: string; fieldType: QuintType }[] = times(Number(itemName.value - 1n)).map(i => {
+  const fields: RowField[] = times(Number(itemName.value - 1n)).map(i => {
     return { fieldName: `${i}`, fieldType: { kind: 'var', name: `tup_${resultTypeVar.name}_${i}` } }
   })
   fields.push({ fieldName: `${itemName.value - 1n}`, fieldType: resultTypeVar })
@@ -179,3 +180,40 @@ export function itemConstraints(
 
   return right([constraint])
 }
+
+export function variantConstraints(
+  id: bigint,
+  args: [QuintEx, QuintType][],
+  resultTypeVar: QuintVarType
+): Either<Error, Constraint[]> {
+  // `_valuEx : valueType` is checked already via the constaintGenerato
+  const [[labelExpr, labelType], [_valueEx, valueType]] = args
+
+  if (labelExpr.kind !== 'str') {
+    return left(
+      buildErrorLeaf(
+        `Generating variant constraints for ${args.map(a => expressionToString(a[0]))}`,
+        `Variant label must be a string expression but is ${labelType.kind}: ${expressionToString(labelExpr)}`
+      )
+    )
+  }
+  // We now know the label must be a quint string
+  const labelStr = labelExpr as QuintStr
+
+  // A tuple with item acess of N should have at least N fields
+  // Fill previous fileds with type variables
+  const variantField: RowField = { fieldName: labelStr.value, fieldType: valueType }
+
+  const generalVarType: QuintType = {
+    kind: 'sum',
+    fields: {
+      kind: 'row',
+      fields: [variantField],
+      other: { kind: 'var', name: `tail_${resultTypeVar.name}` },
+    },
+  }
+  const isDefinedConstraint: Constraint = { kind: 'isDefined', type: generalVarType, sourceId: id }
+  const propagateResultConstraint: Constraint = { kind: 'eq', types: [resultTypeVar, generalVarType], sourceId: id }
+
+  return right([isDefinedConstraint, propagateResultConstraint])
+}
diff --git a/quint/src/types/substitutions.ts b/quint/src/types/substitutions.ts
index 9abe67b6b..581e0097d 100644
--- a/quint/src/types/substitutions.ts
+++ b/quint/src/types/substitutions.ts
@@ -140,6 +140,10 @@ export function applySubstitution(table: LookupTable, subs: Substitutions, t: Qu
  */
 export function applySubstitutionToConstraint(table: LookupTable, subs: Substitutions, c: Constraint): Constraint {
   switch (c.kind) {
+    case 'empty':
+      return c
+    case 'isDefined':
+      return { ...c, type: applySubstitution(table, subs, c.type) }
     case 'eq': {
       const ts: [QuintType, QuintType] = [
         applySubstitution(table, subs, c.types[0]),
@@ -147,8 +151,6 @@ export function applySubstitutionToConstraint(table: LookupTable, subs: Substitu
       ]
       return { kind: c.kind, types: ts, sourceId: c.sourceId }
     }
-    case 'empty':
-      return c
     case 'conjunction': {
       const cs = c.constraints.map(con => applySubstitutionToConstraint(table, subs, con))
       return { kind: 'conjunction', constraints: cs, sourceId: c.sourceId }
diff --git a/quint/test/types/constraintGenerator.test.ts b/quint/test/types/constraintGenerator.test.ts
index d5631d4a5..358e1aebc 100644
--- a/quint/test/types/constraintGenerator.test.ts
+++ b/quint/test/types/constraintGenerator.test.ts
@@ -177,4 +177,12 @@ describe('ConstraintGeneratorVisitor', () => {
       'Operator expects 2 arguments but was given 1'
     )
   })
+
+  it('catches invalid arity on variant operator', () => {
+    testArityError(
+      'val x = variant("foo")',
+      'Checking arity for application of variant',
+      'Operator expects 2 arguments but was given 1'
+    )
+  })
 })

From 3a9cbf0e9664cfff46463ae973dadabcd708ec84 Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Fri, 6 Oct 2023 10:51:17 -0400
Subject: [PATCH 04/13] Add `findMap` utility

Allows us to find and transform values from an iterable
---
 quint/src/util.ts       | 24 ++++++++++++++++++++++++
 quint/test/util.test.ts | 38 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 62 insertions(+)
 create mode 100644 quint/test/util.test.ts

diff --git a/quint/src/util.ts b/quint/src/util.ts
index afbb08ef8..071b06f90 100644
--- a/quint/src/util.ts
+++ b/quint/src/util.ts
@@ -14,6 +14,7 @@
 
 import JSONbig from 'json-bigint'
 import lodash from 'lodash'
+import { Maybe, just, none } from '@sweet-monads/maybe'
 
 /** Add this at the end of a switch statement or if/then sequence to enforce exhaustiveness checking
  *
@@ -44,3 +45,26 @@ export function zip<A, B>(a: A[], b: B[]): [A, B][] {
     }
   })
 }
+
+/** `findMap(xs)` is `just(y)` if there is an `x` in `xs` for which `f(x)` is `just(y)`
+ * otherwise, it is `none`
+ *
+ * This is like `Array.prototype.find`, except that it works on any iterable and
+ * enables trasforming the found value.
+ *
+ * Example:
+ *
+ * ```
+ * const result = findMap([1,2,3], (x) => x % 2 === 0 ? just(x) : none<int>())
+ * lodash.isEqual(result, just(2))
+ * ```
+ * */
+export function findMap<X, Y>(xs: Iterable<X>, f: (x: X) => Maybe<Y>): Maybe<Y> {
+  for (const x of xs) {
+    const maybeY = f(x)
+    if (maybeY.isJust()) {
+      return maybeY
+    }
+  }
+  return none<Y>()
+}
diff --git a/quint/test/util.test.ts b/quint/test/util.test.ts
new file mode 100644
index 000000000..eda8bbfaa
--- /dev/null
+++ b/quint/test/util.test.ts
@@ -0,0 +1,38 @@
+import { assert } from 'chai'
+import { describe, it } from 'mocha'
+
+import { just, none } from '@sweet-monads/maybe'
+
+import { findMap } from '../src/util'
+
+describe('findMap', () => {
+  it('is none on empty iterable', () => {
+    assert(findMap(new Map().values(), _ => just(42)).isNone(), 'should be none on empty iterable')
+  })
+
+  it('is `just` when a vaule can be found', () => {
+    const actual = findMap(
+      new Map([
+        ['a', 1],
+        ['b', 2],
+        ['c', 3],
+      ]).values(),
+      n => (n % 2 === 0 ? just(n) : none<Number>())
+    )
+
+    assert.deepEqual(just(2), actual)
+  })
+
+  it('is `none` when no value can be found', () => {
+    const result = findMap(
+      new Map([
+        ['a', 1],
+        ['b', 2],
+        ['c', 3],
+      ]).values(),
+      n => (n > 3 ? just(n) : none<Number>())
+    )
+
+    assert(result.isNone(), 'should be none')
+  })
+})

From 2762c16e465d6412064011df325db96ac57d983f Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Fri, 6 Oct 2023 15:31:50 -0400
Subject: [PATCH 05/13] Add test for unification of sum types

---
 quint/src/ir/quintTypes.ts                |  6 +-
 quint/src/types/constraintSolver.ts       | 31 +++++-----
 quint/test/types/constraintSolver.test.ts | 71 ++++++++++++++++++++++-
 3 files changed, 88 insertions(+), 20 deletions(-)

diff --git a/quint/src/ir/quintTypes.ts b/quint/src/ir/quintTypes.ts
index cff99ba6f..f8d3435f4 100644
--- a/quint/src/ir/quintTypes.ts
+++ b/quint/src/ir/quintTypes.ts
@@ -92,11 +92,7 @@ export interface QuintSumType extends WithOptionalId {
   fields: ConcreteRow
 }
 
-export function sumType(
-  labelTypePairs: [string, QuintType][],
-  rowVar: string | undefined,
-  id: bigint | undefined
-): QuintSumType {
+export function sumType(labelTypePairs: [string, QuintType][], rowVar?: string, id?: bigint): QuintSumType {
   const fields = labelTypePairs.map(([fieldName, fieldType]) => ({ fieldName, fieldType }))
   const other: Row = rowVar ? { kind: 'var', name: rowVar } : { kind: 'empty' }
   return { kind: 'sum', fields: { kind: 'row', fields, other }, id }
diff --git a/quint/src/types/constraintSolver.ts b/quint/src/types/constraintSolver.ts
index e13044921..c9b01b0fe 100644
--- a/quint/src/types/constraintSolver.ts
+++ b/quint/src/types/constraintSolver.ts
@@ -61,21 +61,24 @@ export function solveConstraint(
       }, right([]))
     }
     case 'isDefined': {
-      const definedType = [...table.values()].find(def => {
-        return def.kind === 'typedef' && def.type && unify(table, def.type, constraint.type).isRight()
-      })
-      if (definedType) {
-        return right([])
-      } else {
-        errors.set(
-          constraint.sourceId,
-          buildErrorLeaf(
-            `Looking for defined type unifying with ${typeToString(constraint.type)}`,
-            'Expected type is not defined'
-          )
-        )
-        return left(errors)
+      for (const def of table.values()) {
+        if (def.kind === 'typedef' && def.type) {
+          const subst = unify(table, def.type, constraint.type)
+          if (subst.isRight()) {
+            // We found a defined type unifying with the given schema
+            // (unwrap the vaule since the left of `unify` doesn't match our needs and isn't relevent)
+            return right(subst.unwrap())
+          }
+        }
       }
+      errors.set(
+        constraint.sourceId,
+        buildErrorLeaf(
+          `Looking for defined type unifying with ${typeToString(constraint.type)}`,
+          'Expected type is not defined'
+        )
+      )
+      return left(errors)
     }
     case 'empty':
       return right([])
diff --git a/quint/test/types/constraintSolver.test.ts b/quint/test/types/constraintSolver.test.ts
index 905a3b4c1..25a13204f 100644
--- a/quint/test/types/constraintSolver.test.ts
+++ b/quint/test/types/constraintSolver.test.ts
@@ -5,7 +5,7 @@ import { parseRowOrThrow, parseTypeOrThrow } from '../../src/types/parser'
 import { Constraint } from '../../src/types/base'
 import { substitutionsToString } from '../../src/types/printing'
 import { Substitutions } from '../../src/types/substitutions'
-import { Row } from '../../src/ir/quintTypes'
+import { Row, sumType, unitType } from '../../src/ir/quintTypes'
 import { errorTreeToString } from '../../src/errorTree'
 import { LookupTable } from '../../src/names/base'
 
@@ -15,6 +15,18 @@ const table: LookupTable = new Map([
   // An uniterpreted type (id 2n)
   [4n, { kind: 'typedef', name: 'MY_UNINTERPRETED', id: 2n }],
   [5n, { kind: 'typedef', name: 'MY_UNINTERPRETED', id: 2n }],
+  [
+    6n,
+    {
+      kind: 'typedef',
+      name: 'SumType',
+      id: 7n,
+      type: sumType([
+        ['A', { kind: 'int' }],
+        ['B', { kind: 'str' }],
+      ]),
+    },
+  ],
 ])
 
 describe('solveConstraint', () => {
@@ -56,6 +68,36 @@ describe('solveConstraint', () => {
     result.map(subs => assert.deepEqual(substitutionsToString(subs), '[ a |-> int, b |-> int ]'))
   })
 
+  it('solves isDefined constraint when unifiable type is defined', () => {
+    const constraint: Constraint = {
+      kind: 'isDefined',
+      type: sumType([['A', { kind: 'int' }]], 'a'),
+      sourceId: 1n,
+    }
+
+    const result = solveConstraint(table, constraint)
+
+    assert.isTrue(result.isRight())
+    result.map(subs => assert.deepEqual(substitutionsToString(subs), '[ a |-> { B: str } ]'))
+  })
+
+  it('isDefined constraint fails when type is not defined', () => {
+    const constraint: Constraint = {
+      kind: 'isDefined',
+      type: sumType([['NotDefined', { kind: 'int' }]], 'a'),
+      sourceId: 1n,
+    }
+
+    const result = solveConstraint(table, constraint)
+
+    assert.isTrue(result.isLeft())
+    result.mapLeft(errs => {
+      const err = errs.get(1n)
+      assert.deepEqual(err?.location, 'Looking for defined type unifying with (NotDefined(int))')
+      assert.deepEqual(err?.message, 'Expected type is not defined')
+    })
+  })
+
   it('solves empty constraint', () => {
     const constraint: Constraint = { kind: 'empty' }
 
@@ -192,6 +234,33 @@ describe('unify', () => {
     result.map(subs => assert.deepEqual(substitutionsToString(subs), '[ a |-> int, b |-> bool ]'))
   })
 
+  it('unifies sum-type', () => {
+    // We do not provide
+    const result = unify(
+      table,
+      sumType([
+        ['A', { kind: 'var', name: 'a' }],
+        ['B', { kind: 'int' }],
+        ['C', unitType(0n)],
+      ]),
+      sumType([
+        ['C', unitType(0n)],
+        ['A', { kind: 'str' }],
+        ['B', { kind: 'var', name: 'b' }],
+      ])
+    )
+
+    assert.isTrue(result.isRight())
+    result.map(subs => assert.deepEqual(substitutionsToString(subs), '[ a |-> str, b |-> int ]'))
+  })
+
+  // it('unifies sum type with open row', () => {
+  //   const result = unify(table, parseTypeOrThrow('A(a)'), parseTypeOrThrow('A(int) | B(str)'))
+
+  //   assert.isTrue(result.isRight())
+  //   result.map(subs => assert.deepEqual(substitutionsToString(subs), '[]'))
+  // })
+
   it("returns error when variable occurs in the other type's body", () => {
     const result = unify(table, parseTypeOrThrow('a'), parseTypeOrThrow('Set[a]'))
 

From fd35a09d4c44ce4ca05a6c4e2f923fe78e94807e Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Fri, 6 Oct 2023 16:54:36 -0400
Subject: [PATCH 06/13] Fix sum type constructor synthesis

- Nullary constructors where being incorrectly defined as lambdas, when
they should just be values.
- We were not adding the type annotation of the defined type to the
operator. But we want this, since in ensures we do not construct open
rowed variants and ensures that we have the right topological sorting to
ensure the variant constructors are after the defined types.
---
 quint/src/parsing/ToIrListener.ts             | 70 ++++++++++++++-----
 quint/testFixture/_1043sumTypeDecl.map.json   |  2 +-
 quint/testFixture/_1043sumTypeDecl.qnt        |  2 +-
 .../testFixture/_1044matchExpression.map.json |  2 +-
 4 files changed, 55 insertions(+), 21 deletions(-)

diff --git a/quint/src/parsing/ToIrListener.ts b/quint/src/parsing/ToIrListener.ts
index 175bd4270..7450fbfc7 100644
--- a/quint/src/parsing/ToIrListener.ts
+++ b/quint/src/parsing/ToIrListener.ts
@@ -17,7 +17,16 @@ import {
   QuintOpDef,
   QuintStr,
 } from '../ir/quintIr'
-import { ConcreteFixedRow, QuintSumType, QuintType, Row, RowField, isUnitType, unitType } from '../ir/quintTypes'
+import {
+  ConcreteFixedRow,
+  QuintSumType,
+  QuintType,
+  Row,
+  RowField,
+  isUnitType,
+  unitType,
+  QuintConstType,
+} from '../ir/quintTypes'
 import { strict as assert } from 'assert'
 import { SourceMap } from './quintParserFrontend'
 import { compact, zipWith } from 'lodash'
@@ -382,6 +391,7 @@ export class ToIrListener implements QuintListener {
     const fields: RowField[] = popMany(this.variantStack, this.variantStack.length)
     const row: ConcreteFixedRow = { kind: 'row', fields, other: { kind: 'empty' } }
     const type: QuintSumType = { id, kind: 'sum', fields: row }
+    const typeName: QuintConstType = { id, kind: 'const', name }
     const def: QuintTypeDef = {
       id: id,
       name,
@@ -418,32 +428,56 @@ export class ToIrListener implements QuintListener {
         // This shouldn't be visible to users
         const paramName = `__${fieldName}Param`
 
-        let params: QuintLambdaParameter[]
-        let expr: QuintEx
         let qualifier: OpQualifier
+        let expr: QuintEx
+        let typeAnnotation: QuintType
 
+        const label: QuintStr = { id: this.getId(variantCtx), kind: 'str', value: fieldName }
         if (isUnitType(fieldType)) {
+          // Its a `val` cause it has no parameters
+          //
+          // E.g., for B we will produce
+          //
+          // ```
+          // val B: T = variant("B", {})
+          // ```
+          qualifier = 'val'
+
           // The nullary variant constructor is actualy
           // a variant pairing a label with the unit.
-          params = []
-          expr = unitValue(this.getId(variantCtx._sumLabel))
-          // Its a `val` cause it takes no arguments
-          qualifier = 'val'
+          const wrappedExpr = unitValue(this.getId(variantCtx._sumLabel))
+
+          typeAnnotation = typeName
+          expr = {
+            id: this.getId(variantCtx),
+            kind: 'app',
+            opcode: 'variant',
+            args: [label, wrappedExpr],
+          }
         } else {
           // Otherwise we will build a constructor that takes one parameter
-          params = [{ id: this.getId(variantCtx.type()!), name: paramName }]
-          expr = { kind: 'name', name: paramName, id: this.getId(variantCtx._sumLabel) }
+          //
+          // E.g., for A(int) we will produce a
+          //
+          // ```
+          // def A(x:int): T = variant("A", x)
+          // ```
           qualifier = 'def'
+
+          const params = [{ id: this.getId(variantCtx.type()!), name: paramName }]
+          const wrappedExpr: QuintName = { kind: 'name', name: paramName, id: this.getId(variantCtx._sumLabel) }
+          const variant: QuintBuiltinApp = {
+            id: this.getId(variantCtx),
+            kind: 'app',
+            opcode: 'variant',
+            args: [label, wrappedExpr],
+          }
+
+          typeAnnotation = { kind: 'oper', args: [fieldType], res: typeName }
+          expr = { id: this.getId(variantCtx), kind: 'lambda', params, qualifier, expr: variant }
         }
-        const label: QuintStr = { id: this.getId(variantCtx), kind: 'str', value: fieldName }
-        const variant: QuintBuiltinApp = {
-          id: this.getId(variantCtx),
-          kind: 'app',
-          opcode: 'variant',
-          args: [label, expr],
-        }
-        const lam: QuintLambda = { id: this.getId(variantCtx), kind: 'lambda', params, qualifier, expr: variant }
-        return { id: this.getId(variantCtx), kind: 'def', name: fieldName, qualifier, expr: lam }
+
+        return { id: this.getId(variantCtx), kind: 'def', name: fieldName, qualifier, typeAnnotation, expr }
       }
     )
 
diff --git a/quint/testFixture/_1043sumTypeDecl.map.json b/quint/testFixture/_1043sumTypeDecl.map.json
index 2f332fe29..9d2b689b9 100644
--- a/quint/testFixture/_1043sumTypeDecl.map.json
+++ b/quint/testFixture/_1043sumTypeDecl.map.json
@@ -1 +1 @@
-{"sourceIndex":{"0":"mocked_path/testFixture/_1043sumTypeDecl.qnt"},"map":{"1":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"2":[0,{"line":3,"col":8,"index":45},{"line":3,"col":10,"index":47}],"3":[0,{"line":1,"col":2,"index":20},{"line":3,"col":30,"index":48}],"4":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"5":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"6":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"7":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"8":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"9":[0,{"line":3,"col":8,"index":45},{"line":3,"col":10,"index":47}],"10":[0,{"line":3,"col":6,"index":43},{"line":3,"col":6,"index":43}],"11":[0,{"line":3,"col":6,"index":43},{"line":3,"col":11,"index":48}],"12":[0,{"line":3,"col":6,"index":43},{"line":3,"col":11,"index":48}],"13":[0,{"line":3,"col":6,"index":43},{"line":3,"col":11,"index":48}],"14":[0,{"line":3,"col":6,"index":43},{"line":3,"col":11,"index":48}],"15":[0,{"line":5,"col":34,"index":85},{"line":5,"col":34,"index":85}],"16":[0,{"line":5,"col":39,"index":90},{"line":5,"col":39,"index":90}],"17":[0,{"line":5,"col":37,"index":88},{"line":5,"col":40,"index":91}],"18":[0,{"line":5,"col":29,"index":80},{"line":5,"col":41,"index":92}],"19":[0,{"line":5,"col":2,"index":53},{"line":5,"col":41,"index":92}],"20":[0,{"line":0,"col":0,"index":0},{"line":6,"col":94,"index":94}]}}
\ No newline at end of file
+{"sourceIndex":{"0":"mocked_path/testFixture/_1043sumTypeDecl.qnt"},"map":{"1":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"2":[0,{"line":3,"col":8,"index":45},{"line":3,"col":10,"index":47}],"3":[0,{"line":1,"col":2,"index":20},{"line":3,"col":30,"index":48}],"4":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"5":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"6":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"7":[0,{"line":2,"col":6,"index":35},{"line":2,"col":6,"index":35}],"8":[0,{"line":3,"col":6,"index":43},{"line":3,"col":11,"index":48}],"9":[0,{"line":3,"col":8,"index":45},{"line":3,"col":10,"index":47}],"10":[0,{"line":3,"col":6,"index":43},{"line":3,"col":6,"index":43}],"11":[0,{"line":3,"col":6,"index":43},{"line":3,"col":11,"index":48}],"12":[0,{"line":3,"col":6,"index":43},{"line":3,"col":11,"index":48}],"13":[0,{"line":3,"col":6,"index":43},{"line":3,"col":11,"index":48}],"14":[0,{"line":5,"col":34,"index":85},{"line":5,"col":34,"index":85}],"15":[0,{"line":5,"col":29,"index":80},{"line":5,"col":35,"index":86}],"16":[0,{"line":5,"col":44,"index":95},{"line":5,"col":44,"index":95}],"17":[0,{"line":5,"col":49,"index":100},{"line":5,"col":49,"index":100}],"18":[0,{"line":5,"col":47,"index":98},{"line":5,"col":50,"index":101}],"19":[0,{"line":5,"col":39,"index":90},{"line":5,"col":51,"index":102}],"20":[0,{"line":5,"col":2,"index":53},{"line":5,"col":51,"index":102}],"21":[0,{"line":0,"col":0,"index":0},{"line":6,"col":104,"index":104}]}}
\ No newline at end of file
diff --git a/quint/testFixture/_1043sumTypeDecl.qnt b/quint/testFixture/_1043sumTypeDecl.qnt
index 42d9dc09d..fcfe54625 100644
--- a/quint/testFixture/_1043sumTypeDecl.qnt
+++ b/quint/testFixture/_1043sumTypeDecl.qnt
@@ -3,5 +3,5 @@ module SumTypes {
     | A
     | B(int)
 
-  val canConstructVariants = List(A, B(2))
+  val canConstructVariants : List[T] = List(A, B(2))
 }
diff --git a/quint/testFixture/_1044matchExpression.map.json b/quint/testFixture/_1044matchExpression.map.json
index 277960ad0..ad6950811 100644
--- a/quint/testFixture/_1044matchExpression.map.json
+++ b/quint/testFixture/_1044matchExpression.map.json
@@ -1 +1 @@
-{"sourceIndex":{"0":"mocked_path/testFixture/_1044matchExpression.qnt"},"map":{"1":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"2":[0,{"line":1,"col":17,"index":35},{"line":1,"col":19,"index":37}],"3":[0,{"line":1,"col":26,"index":44},{"line":1,"col":28,"index":46}],"4":[0,{"line":1,"col":2,"index":20},{"line":1,"col":29,"index":47}],"5":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"6":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"7":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"8":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"9":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"10":[0,{"line":1,"col":17,"index":35},{"line":1,"col":19,"index":37}],"11":[0,{"line":1,"col":15,"index":33},{"line":1,"col":15,"index":33}],"12":[0,{"line":1,"col":15,"index":33},{"line":1,"col":20,"index":38}],"13":[0,{"line":1,"col":15,"index":33},{"line":1,"col":20,"index":38}],"14":[0,{"line":1,"col":15,"index":33},{"line":1,"col":20,"index":38}],"15":[0,{"line":1,"col":15,"index":33},{"line":1,"col":20,"index":38}],"16":[0,{"line":1,"col":26,"index":44},{"line":1,"col":28,"index":46}],"17":[0,{"line":1,"col":24,"index":42},{"line":1,"col":24,"index":42}],"18":[0,{"line":1,"col":24,"index":42},{"line":1,"col":29,"index":47}],"19":[0,{"line":1,"col":24,"index":42},{"line":1,"col":29,"index":47}],"20":[0,{"line":1,"col":24,"index":42},{"line":1,"col":29,"index":47}],"21":[0,{"line":1,"col":24,"index":42},{"line":1,"col":29,"index":47}],"22":[0,{"line":3,"col":12,"index":62},{"line":3,"col":16,"index":66}],"23":[0,{"line":3,"col":10,"index":60},{"line":3,"col":17,"index":67}],"24":[0,{"line":3,"col":2,"index":52},{"line":3,"col":17,"index":67}],"25":[0,{"line":5,"col":17,"index":87},{"line":5,"col":17,"index":87}],"26":[0,{"line":6,"col":14,"index":105},{"line":6,"col":14,"index":105}],"27":[0,{"line":7,"col":14,"index":121},{"line":7,"col":14,"index":121}],"28":[0,{"line":8,"col":15,"index":138},{"line":8,"col":15,"index":138}],"29":[0,{"line":8,"col":14,"index":137},{"line":8,"col":15,"index":138}],"30":[0,{"line":5,"col":11,"index":81},{"line":9,"col":72,"index":142}],"31":[0,{"line":6,"col":6,"index":97},{"line":6,"col":14,"index":105}],"32":[0,{"line":6,"col":6,"index":97},{"line":6,"col":6,"index":97}],"33":[0,{"line":7,"col":6,"index":113},{"line":7,"col":14,"index":121}],"34":[0,{"line":7,"col":6,"index":113},{"line":7,"col":9,"index":116}],"35":[0,{"line":8,"col":6,"index":129},{"line":8,"col":15,"index":138}],"36":[0,{"line":5,"col":2,"index":72},{"line":9,"col":72,"index":142}],"37":[0,{"line":0,"col":0,"index":0},{"line":10,"col":144,"index":144}]}}
\ No newline at end of file
+{"sourceIndex":{"0":"mocked_path/testFixture/_1044matchExpression.qnt"},"map":{"1":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"2":[0,{"line":1,"col":17,"index":35},{"line":1,"col":19,"index":37}],"3":[0,{"line":1,"col":26,"index":44},{"line":1,"col":28,"index":46}],"4":[0,{"line":1,"col":2,"index":20},{"line":1,"col":29,"index":47}],"5":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"6":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"7":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"8":[0,{"line":1,"col":11,"index":29},{"line":1,"col":11,"index":29}],"9":[0,{"line":1,"col":15,"index":33},{"line":1,"col":20,"index":38}],"10":[0,{"line":1,"col":17,"index":35},{"line":1,"col":19,"index":37}],"11":[0,{"line":1,"col":15,"index":33},{"line":1,"col":15,"index":33}],"12":[0,{"line":1,"col":15,"index":33},{"line":1,"col":20,"index":38}],"13":[0,{"line":1,"col":15,"index":33},{"line":1,"col":20,"index":38}],"14":[0,{"line":1,"col":15,"index":33},{"line":1,"col":20,"index":38}],"15":[0,{"line":1,"col":24,"index":42},{"line":1,"col":29,"index":47}],"16":[0,{"line":1,"col":26,"index":44},{"line":1,"col":28,"index":46}],"17":[0,{"line":1,"col":24,"index":42},{"line":1,"col":24,"index":42}],"18":[0,{"line":1,"col":24,"index":42},{"line":1,"col":29,"index":47}],"19":[0,{"line":1,"col":24,"index":42},{"line":1,"col":29,"index":47}],"20":[0,{"line":1,"col":24,"index":42},{"line":1,"col":29,"index":47}],"21":[0,{"line":3,"col":12,"index":62},{"line":3,"col":16,"index":66}],"22":[0,{"line":3,"col":10,"index":60},{"line":3,"col":17,"index":67}],"23":[0,{"line":3,"col":2,"index":52},{"line":3,"col":17,"index":67}],"24":[0,{"line":5,"col":17,"index":87},{"line":5,"col":17,"index":87}],"25":[0,{"line":6,"col":14,"index":105},{"line":6,"col":14,"index":105}],"26":[0,{"line":7,"col":14,"index":121},{"line":7,"col":14,"index":121}],"27":[0,{"line":8,"col":15,"index":138},{"line":8,"col":15,"index":138}],"28":[0,{"line":8,"col":14,"index":137},{"line":8,"col":15,"index":138}],"29":[0,{"line":5,"col":11,"index":81},{"line":9,"col":72,"index":142}],"30":[0,{"line":6,"col":6,"index":97},{"line":6,"col":14,"index":105}],"31":[0,{"line":6,"col":6,"index":97},{"line":6,"col":6,"index":97}],"32":[0,{"line":7,"col":6,"index":113},{"line":7,"col":14,"index":121}],"33":[0,{"line":7,"col":6,"index":113},{"line":7,"col":9,"index":116}],"34":[0,{"line":8,"col":6,"index":129},{"line":8,"col":15,"index":138}],"35":[0,{"line":5,"col":2,"index":72},{"line":9,"col":72,"index":142}],"36":[0,{"line":0,"col":0,"index":0},{"line":10,"col":144,"index":144}]}}
\ No newline at end of file

From 26cac28b4e8b5694ca1e81eb0db946a0609660e6 Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Fri, 6 Oct 2023 17:09:55 -0400
Subject: [PATCH 07/13] Add test for type inference

---
 quint/test/types/inferrer.test.ts | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/quint/test/types/inferrer.test.ts b/quint/test/types/inferrer.test.ts
index 101f2a6ce..6fb67d684 100644
--- a/quint/test/types/inferrer.test.ts
+++ b/quint/test/types/inferrer.test.ts
@@ -4,6 +4,7 @@ import { TypeInferenceResult, TypeInferrer } from '../../src/types/inferrer'
 import { typeSchemeToString } from '../../src/types/printing'
 import { errorTreeToString } from '../../src/errorTree'
 import { parseMockedModule } from '../util'
+import { moduleToString } from '../../src'
 
 describe('inferTypes', () => {
   function inferTypesForDefs(defs: string[]): TypeInferenceResult {
@@ -134,6 +135,31 @@ describe('inferTypes', () => {
     ])
   })
 
+  it('infers types for variants', () => {
+    const defs = ['type T = A(int) | B', 'val a = variant("A", 3)']
+
+    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, [
+      [14n, 'str'],
+      [15n, 'int'],
+      [16n, '(A(int))'],
+      [17n, '(A(int))'],
+      [10n, 'str'],
+      [11n, '{}'],
+      [12n, '(B({}))'],
+      [13n, '(B({}))'],
+      [5n, 'int'],
+      [4n, 'str'],
+      [6n, 'int'],
+      [7n, '(A(int))'],
+      [8n, '(int) => (A(int))'],
+      [9n, '(int) => (A(int))'],
+    ])
+  })
+
   it('keeps track of free variables in nested scopes (#966)', () => {
     const defs = ['def f(a) = a == "x"', 'def g(b) = val nested = (1,2) { f(b) }']
 

From c1f75f3be862daf55f6dbd9af6f78bcede859e1d Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Fri, 6 Oct 2023 17:16:23 -0400
Subject: [PATCH 08/13] Fix formatting

---
 quint/src/graphics.ts                | 2 +-
 quint/src/parsing/ToIrListener.ts    | 2 +-
 quint/src/types/builtinSignatures.ts | 2 +-
 quint/src/util.ts                    | 2 +-
 quint/test/types/inferrer.test.ts    | 1 -
 5 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/quint/src/graphics.ts b/quint/src/graphics.ts
index d15e29a15..0de449d75 100644
--- a/quint/src/graphics.ts
+++ b/quint/src/graphics.ts
@@ -29,7 +29,7 @@ import {
 import { QuintDeclaration, QuintEx, isAnnotatedDef } from './ir/quintIr'
 import { ExecutionFrame } from './runtime/trace'
 import { zerog } from './idGenerator'
-import { ConcreteFixedRow, ConcreteRow, isUnitType, QuintType, Row } from './ir/quintTypes'
+import { ConcreteRow, QuintType, Row, isUnitType } from './ir/quintTypes'
 import { TypeScheme } from './types/base'
 import { canonicalTypeScheme } from './types/printing'
 import { declarationToString, qualifierToString, rowToString } from './ir/IRprinting'
diff --git a/quint/src/parsing/ToIrListener.ts b/quint/src/parsing/ToIrListener.ts
index 7450fbfc7..15392fc17 100644
--- a/quint/src/parsing/ToIrListener.ts
+++ b/quint/src/parsing/ToIrListener.ts
@@ -19,13 +19,13 @@ import {
 } from '../ir/quintIr'
 import {
   ConcreteFixedRow,
+  QuintConstType,
   QuintSumType,
   QuintType,
   Row,
   RowField,
   isUnitType,
   unitType,
-  QuintConstType,
 } from '../ir/quintTypes'
 import { strict as assert } from 'assert'
 import { SourceMap } from './quintParserFrontend'
diff --git a/quint/src/types/builtinSignatures.ts b/quint/src/types/builtinSignatures.ts
index 528aed63c..33631d88e 100644
--- a/quint/src/types/builtinSignatures.ts
+++ b/quint/src/types/builtinSignatures.ts
@@ -13,7 +13,7 @@
  */
 
 import { parseTypeOrThrow } from './parser'
-import { sumType, typeNames } from '../ir/quintTypes'
+import { typeNames } from '../ir/quintTypes'
 import { Signature, TypeScheme } from './base'
 import { times } from 'lodash'
 import { QuintBuiltinOpcode } from '../ir/quintIr'
diff --git a/quint/src/util.ts b/quint/src/util.ts
index 071b06f90..f57dcec2b 100644
--- a/quint/src/util.ts
+++ b/quint/src/util.ts
@@ -14,7 +14,7 @@
 
 import JSONbig from 'json-bigint'
 import lodash from 'lodash'
-import { Maybe, just, none } from '@sweet-monads/maybe'
+import { Maybe, none } from '@sweet-monads/maybe'
 
 /** Add this at the end of a switch statement or if/then sequence to enforce exhaustiveness checking
  *
diff --git a/quint/test/types/inferrer.test.ts b/quint/test/types/inferrer.test.ts
index 6fb67d684..3ae5e1294 100644
--- a/quint/test/types/inferrer.test.ts
+++ b/quint/test/types/inferrer.test.ts
@@ -4,7 +4,6 @@ import { TypeInferenceResult, TypeInferrer } from '../../src/types/inferrer'
 import { typeSchemeToString } from '../../src/types/printing'
 import { errorTreeToString } from '../../src/errorTree'
 import { parseMockedModule } from '../util'
-import { moduleToString } from '../../src'
 
 describe('inferTypes', () => {
   function inferTypesForDefs(defs: string[]): TypeInferenceResult {

From efec3a74de3aad4de43bae8f10537af12b3c4de7 Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Fri, 6 Oct 2023 17:30:36 -0400
Subject: [PATCH 09/13] Add effect signature for variant operator

---
 quint/src/effects/builtinSignatures.ts | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/quint/src/effects/builtinSignatures.ts b/quint/src/effects/builtinSignatures.ts
index 4cb5a2d60..173786de4 100644
--- a/quint/src/effects/builtinSignatures.ts
+++ b/quint/src/effects/builtinSignatures.ts
@@ -226,6 +226,10 @@ const otherOperators = [
     name: 'ite',
     effect: parseAndQuantify('(Read[r1], Read[r2] & Update[u], Read[r3] & Update[u]) => Read[r1, r2, r3] & Update[u]'),
   },
+  {
+    name: 'variant',
+    effect: parseAndQuantify('(Pure, Read[r] & Update[u]) => Read[r] & Update[u]'),
+  },
 ]
 
 const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [

From 58c1bcaa58cdc223a1c5a739c23dea3b390b088e Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Fri, 6 Oct 2023 17:37:09 -0400
Subject: [PATCH 10/13] Add document the rule for the variant operator

---
 quint/src/types/specialConstraints.ts | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/quint/src/types/specialConstraints.ts b/quint/src/types/specialConstraints.ts
index a82977958..e641af15b 100644
--- a/quint/src/types/specialConstraints.ts
+++ b/quint/src/types/specialConstraints.ts
@@ -181,6 +181,15 @@ export function itemConstraints(
   return right([constraint])
 }
 
+// The rule for the `variant` operator:
+//
+//   Γ ⊢ e: (t, c)            Γ ⊢ 'l' : str                v is fresh
+// --------------------------------------------------------------------
+//    Γ ⊢ variant('l', e) : (s, c /\ s ~ < l : t | v > /\ isDefined(s))
+//
+// Where < ... > is a row-based variant.
+//
+// This rule is explained in /doc/rfcs/rfc001-sum-types/rfc001-sum-types.org
 export function variantConstraints(
   id: bigint,
   args: [QuintEx, QuintType][],

From d5dba4be4a3a14b33c79e3e25332acebc074117a Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Fri, 20 Oct 2023 15:42:16 -0400
Subject: [PATCH 11/13] Remove dead code and comments

---
 quint/src/types/specialConstraints.ts     | 4 +---
 quint/test/types/constraintSolver.test.ts | 8 --------
 2 files changed, 1 insertion(+), 11 deletions(-)

diff --git a/quint/src/types/specialConstraints.ts b/quint/src/types/specialConstraints.ts
index e641af15b..f751086f7 100644
--- a/quint/src/types/specialConstraints.ts
+++ b/quint/src/types/specialConstraints.ts
@@ -206,12 +206,10 @@ export function variantConstraints(
       )
     )
   }
-  // We now know the label must be a quint string
-  const labelStr = labelExpr as QuintStr
 
   // A tuple with item acess of N should have at least N fields
   // Fill previous fileds with type variables
-  const variantField: RowField = { fieldName: labelStr.value, fieldType: valueType }
+  const variantField: RowField = { fieldName: labelExpr.value, fieldType: valueType }
 
   const generalVarType: QuintType = {
     kind: 'sum',
diff --git a/quint/test/types/constraintSolver.test.ts b/quint/test/types/constraintSolver.test.ts
index 25a13204f..e65c124b1 100644
--- a/quint/test/types/constraintSolver.test.ts
+++ b/quint/test/types/constraintSolver.test.ts
@@ -235,7 +235,6 @@ describe('unify', () => {
   })
 
   it('unifies sum-type', () => {
-    // We do not provide
     const result = unify(
       table,
       sumType([
@@ -254,13 +253,6 @@ describe('unify', () => {
     result.map(subs => assert.deepEqual(substitutionsToString(subs), '[ a |-> str, b |-> int ]'))
   })
 
-  // it('unifies sum type with open row', () => {
-  //   const result = unify(table, parseTypeOrThrow('A(a)'), parseTypeOrThrow('A(int) | B(str)'))
-
-  //   assert.isTrue(result.isRight())
-  //   result.map(subs => assert.deepEqual(substitutionsToString(subs), '[]'))
-  // })
-
   it("returns error when variable occurs in the other type's body", () => {
     const result = unify(table, parseTypeOrThrow('a'), parseTypeOrThrow('Set[a]'))
 

From e9eafd3482ebeda07fe4e5a011fde911c5eef1fb Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Fri, 20 Oct 2023 15:46:04 -0400
Subject: [PATCH 12/13] Update fixtures

---
 quint/testFixture/_1043sumTypeDecl.json     | 2 +-
 quint/testFixture/_1044matchExpression.json | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/quint/testFixture/_1043sumTypeDecl.json b/quint/testFixture/_1043sumTypeDecl.json
index a8098dfef..67982899d 100644
--- a/quint/testFixture/_1043sumTypeDecl.json
+++ b/quint/testFixture/_1043sumTypeDecl.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"modules":[{"id":20,"name":"SumTypes","declarations":[{"id":3,"name":"T","kind":"typedef","type":{"id":3,"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"}}],"other":{"kind":"empty"}}}},{"id":8,"kind":"def","name":"A","qualifier":"val","expr":{"id":7,"kind":"lambda","params":[],"qualifier":"val","expr":{"id":6,"kind":"app","opcode":"variant","args":[{"id":5,"kind":"str","value":"A"},{"id":4,"kind":"app","opcode":"Rec","args":[]}]}}},{"id":14,"kind":"def","name":"B","qualifier":"def","expr":{"id":13,"kind":"lambda","params":[{"id":9,"name":"__BParam"}],"qualifier":"def","expr":{"id":12,"kind":"app","opcode":"variant","args":[{"id":11,"kind":"str","value":"B"},{"kind":"name","name":"__BParam","id":10}]}}},{"id":19,"kind":"def","name":"canConstructVariants","qualifier":"val","expr":{"id":18,"kind":"app","opcode":"List","args":[{"id":15,"kind":"name","name":"A"},{"id":17,"kind":"app","opcode":"B","args":[{"id":16,"kind":"int","value":2}]}]}}]}],"table":{"10":{"id":9,"name":"__BParam","kind":"param"},"15":{"id":8,"kind":"def","name":"A","qualifier":"val","expr":{"id":7,"kind":"lambda","params":[],"qualifier":"val","expr":{"id":6,"kind":"app","opcode":"variant","args":[{"id":5,"kind":"str","value":"A"},{"id":4,"kind":"app","opcode":"Rec","args":[]}]}},"depth":0},"17":{"id":14,"kind":"def","name":"B","qualifier":"def","expr":{"id":13,"kind":"lambda","params":[{"id":9,"name":"__BParam"}],"qualifier":"def","expr":{"id":12,"kind":"app","opcode":"variant","args":[{"id":11,"kind":"str","value":"B"},{"kind":"name","name":"__BParam","id":10}]}},"depth":0}},"errors":[]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"modules":[{"id":21,"name":"SumTypes","declarations":[{"id":3,"name":"T","kind":"typedef","type":{"id":3,"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"}}],"other":{"kind":"empty"}}}},{"id":13,"kind":"def","name":"B","qualifier":"def","typeAnnotation":{"kind":"oper","args":[{"id":2,"kind":"int"}],"res":{"id":3,"kind":"const","name":"T"}},"expr":{"id":12,"kind":"lambda","params":[{"id":9,"name":"__BParam"}],"qualifier":"def","expr":{"id":11,"kind":"app","opcode":"variant","args":[{"id":8,"kind":"str","value":"B"},{"kind":"name","name":"__BParam","id":10}]}}},{"id":7,"kind":"def","name":"A","qualifier":"val","typeAnnotation":{"id":3,"kind":"const","name":"T"},"expr":{"id":6,"kind":"app","opcode":"variant","args":[{"id":4,"kind":"str","value":"A"},{"id":5,"kind":"app","opcode":"Rec","args":[]}]}},{"id":20,"kind":"def","name":"canConstructVariants","qualifier":"val","expr":{"id":19,"kind":"app","opcode":"List","args":[{"id":16,"kind":"name","name":"A"},{"id":18,"kind":"app","opcode":"B","args":[{"id":17,"kind":"int","value":2}]}]},"typeAnnotation":{"id":15,"kind":"list","elem":{"id":14,"kind":"const","name":"T"}}}]}],"table":{"3":{"id":3,"name":"T","kind":"typedef","type":{"id":3,"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"}}],"other":{"kind":"empty"}}}},"10":{"id":9,"name":"__BParam","kind":"param"},"14":{"id":3,"name":"T","kind":"typedef","type":{"id":3,"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"}}],"other":{"kind":"empty"}}}},"16":{"id":7,"kind":"def","name":"A","qualifier":"val","expr":{"id":6,"kind":"app","opcode":"variant","args":[{"id":4,"kind":"str","value":"A"},{"id":5,"kind":"app","opcode":"Rec","args":[]}]},"depth":0},"18":{"id":13,"kind":"def","name":"B","qualifier":"def","expr":{"id":12,"kind":"lambda","params":[{"id":9,"name":"__BParam"}],"qualifier":"def","expr":{"id":11,"kind":"app","opcode":"variant","args":[{"id":8,"kind":"str","value":"B"},{"kind":"name","name":"__BParam","id":10}]}},"depth":0}},"errors":[]}
\ No newline at end of file
diff --git a/quint/testFixture/_1044matchExpression.json b/quint/testFixture/_1044matchExpression.json
index 39250360d..d57b54398 100644
--- a/quint/testFixture/_1044matchExpression.json
+++ b/quint/testFixture/_1044matchExpression.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"modules":[{"id":37,"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":9,"kind":"def","name":"A","qualifier":"val","expr":{"id":8,"kind":"lambda","params":[],"qualifier":"val","expr":{"id":7,"kind":"app","opcode":"variant","args":[{"id":6,"kind":"str","value":"A"},{"id":5,"kind":"app","opcode":"Rec","args":[]}]}}},{"id":15,"kind":"def","name":"B","qualifier":"def","expr":{"id":14,"kind":"lambda","params":[{"id":10,"name":"__BParam"}],"qualifier":"def","expr":{"id":13,"kind":"app","opcode":"variant","args":[{"id":12,"kind":"str","value":"B"},{"kind":"name","name":"__BParam","id":11}]}}},{"id":21,"kind":"def","name":"C","qualifier":"def","expr":{"id":20,"kind":"lambda","params":[{"id":16,"name":"__CParam"}],"qualifier":"def","expr":{"id":19,"kind":"app","opcode":"variant","args":[{"id":18,"kind":"str","value":"C"},{"kind":"name","name":"__CParam","id":17}]}}},{"id":24,"kind":"def","name":"c","qualifier":"val","expr":{"id":23,"kind":"app","opcode":"C","args":[{"id":22,"kind":"str","value":"Foo"}]}},{"id":36,"kind":"def","name":"ex","qualifier":"val","expr":{"id":30,"kind":"app","opcode":"match","args":[{"id":25,"kind":"name","name":"c"},{"id":31,"kind":"str","value":"A"},{"id":31,"kind":"lambda","qualifier":"def","expr":{"id":26,"kind":"int","value":0},"params":[{"name":"_","id":32}]},{"id":33,"kind":"str","value":"B"},{"id":33,"kind":"lambda","qualifier":"def","expr":{"id":27,"kind":"name","name":"n"},"params":[{"name":"n","id":34}]},{"id":35,"kind":"str","value":"_"},{"id":35,"kind":"lambda","qualifier":"def","expr":{"id":29,"kind":"app","opcode":"iuminus","args":[{"id":28,"kind":"int","value":1}]},"params":[]}]}}]}],"table":{"11":{"id":10,"name":"__BParam","kind":"param"},"17":{"id":16,"name":"__CParam","kind":"param"},"23":{"id":21,"kind":"def","name":"C","qualifier":"def","expr":{"id":20,"kind":"lambda","params":[{"id":16,"name":"__CParam"}],"qualifier":"def","expr":{"id":19,"kind":"app","opcode":"variant","args":[{"id":18,"kind":"str","value":"C"},{"kind":"name","name":"__CParam","id":17}]}},"depth":0},"25":{"id":24,"kind":"def","name":"c","qualifier":"val","expr":{"id":23,"kind":"app","opcode":"C","args":[{"id":22,"kind":"str","value":"Foo"}]},"depth":0},"27":{"name":"n","id":34,"kind":"param"}},"errors":[]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"modules":[{"id":36,"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":35,"kind":"def","name":"ex","qualifier":"val","expr":{"id":29,"kind":"app","opcode":"match","args":[{"id":24,"kind":"name","name":"c"},{"id":30,"kind":"str","value":"A"},{"id":30,"kind":"lambda","qualifier":"def","expr":{"id":25,"kind":"int","value":0},"params":[{"name":"_","id":31}]},{"id":32,"kind":"str","value":"B"},{"id":32,"kind":"lambda","qualifier":"def","expr":{"id":26,"kind":"name","name":"n"},"params":[{"name":"n","id":33}]},{"id":34,"kind":"str","value":"_"},{"id":34,"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":33,"kind":"param"}},"errors":[]}
\ No newline at end of file

From 474b6aa3c2d534539dc1bc89a39abf9d0a04ca84 Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Fri, 20 Oct 2023 15:48:00 -0400
Subject: [PATCH 13/13] Fir formatting

---
 quint/src/types/specialConstraints.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/quint/src/types/specialConstraints.ts b/quint/src/types/specialConstraints.ts
index f751086f7..52dc42cdc 100644
--- a/quint/src/types/specialConstraints.ts
+++ b/quint/src/types/specialConstraints.ts
@@ -16,7 +16,7 @@
 import { Either, left, mergeInMany, right } from '@sweet-monads/either'
 import { Error, buildErrorLeaf } from '../errorTree'
 import { expressionToString } from '../ir/IRprinting'
-import { QuintEx, QuintStr } from '../ir/quintIr'
+import { QuintEx } from '../ir/quintIr'
 import { QuintType, QuintVarType } from '../ir/quintTypes'
 import { Constraint } from './base'
 import { chunk, times } from 'lodash'