diff --git a/doc/adr005-type-system.md b/doc/adr005-type-system.md
index a886dca43..a80d5fdcd 100644
--- a/doc/adr005-type-system.md
+++ b/doc/adr005-type-system.md
@@ -123,7 +123,7 @@ substitution to the context and generate constraints for the result expression.
               Γ ⊢ val n = e1 { e2 }: (t2, s(c1 ∧ c2))
 ```
 
-Whenever we fetch a type scheme from the constant, any quantified variables are
+Whenever we fetch a type scheme from the context, any quantified variables are
 replaced with fresh type variables. The class state is used to track free type
 variables in the context, and operator signatures always assume quantification
 of all names that are not free in the context.
diff --git a/doc/rfcs/rfc001-sum-types/rfc001-erc-sum-types-example.qnt b/doc/rfcs/rfc001-sum-types/rfc001-erc-sum-types-example.qnt
new file mode 100644
index 000000000..30fe17ee4
--- /dev/null
+++ b/doc/rfcs/rfc001-sum-types/rfc001-erc-sum-types-example.qnt
@@ -0,0 +1,209 @@
+// -*- mode: Bluespec; -*-
+
+/**
+ *
+ * This is a fragment of https://github.com/informalsystems/quint/tree/main/examples/solidity/ERC20/erc20.qnt
+ * adapted to illustrate the proposed sum-type syntax.
+ *
+ */
+module erc20 {
+    // An address is simply is string. The particular format is not essential.
+    type Address = str
+    // the special zero address, which corresponds to the address 0 in EVM
+    pure val ZERO_ADDRESS = "0"
+
+    // We fix the pool of all addresses, as this make the specification easier to write.
+    // To instantiate erc20 with a fixed set of addresses, use:
+    // import erc20(AllAddresses = Set(ZERO_ADDRESS, "a", "b", "c")) as myToken
+    // val myTokenState = myToken::newErc20("b", 1000)
+    const AllAddresses: Set[Address]
+
+    // An EVM integer is 256 bits.
+    // We are using big integers and check for overflows manually.
+    type Uint = int
+    pure val MAX_UINT = 2^256 - 1
+    pure def isUint(i: int): bool = 0 <= i and i <= MAX_UINT
+
+    // A state of an ERC20 contract/token
+    type Erc20State = {
+        balanceOf: Address -> Uint,
+        totalSupply: Uint,
+        allowance: (Address, Address) -> Uint,
+        owner: Address,
+    }
+
+    // Example of a sum type representing a
+    // NOTE: Once we support parametric sum-types we can generalize this alias and the map operators
+    type Erc20Result =
+         | Ok(Erc20State)
+         | Error(str)
+
+    pure def mapState(r:Erc20Result, f:Erc20State => Erc20State): Erc20Result =
+         match r {
+            | Ok(s)    => Ok(f(s))
+            | Error(_) => r
+        }
+
+    pure def flatMap(r:Erc20Result, f:Erc20State => Erc20Result): Erc20Result =
+         match r {
+            | Ok(s)    => f(s)
+            | Error(_) => r
+        }
+
+    // An auxilliary definition similar to Solidity's require
+    pure def require(r: Erc20Result, cond: bool, msg: str): Erc20Result =
+        match r {
+            | Error(_) => r
+            | _        => if (cond) r else Error(msg)
+        }
+
+    // contract initialization
+    pure def newErc20(sender: Address, initialSupply: Uint): Erc20State = {
+        balanceOf: AllAddresses.mapBy(a => if (a != sender) 0 else initialSupply),
+        totalSupply: initialSupply,
+        allowance: tuples(AllAddresses, AllAddresses).mapBy(p => 0),
+        owner: sender,
+    }
+
+    /**
+     * Returns the amount of tokens in existence.
+     */
+    pure def totalSupply(state: Erc20State): Uint = {
+        state.totalSupply
+    }
+
+    /**
+     * Returns the amount of tokens owned by account.
+     */
+    pure def balanceOf(state: Erc20State, account: Address): Uint = {
+        state.balanceOf.get(account)
+    }
+
+    // An internal implementation, similar to OpenZeppelin's
+    // https://github.com/OpenZeppelin/openzeppelin-contracts/blob/ca822213f2275a14c26167bd387ac3522da67fe9/contracts/token/ERC20/ERC20.sol#L222
+    pure def _transfer(state: Erc20State,
+            fromAddr: Address, toAddr: Address, amount: Uint): Erc20Result = {
+        // FIXME(#693): type annotation below is a workaround, inferred type is too general
+        val fromBalance: int = state.balanceOf.get(fromAddr)
+        Ok(state)
+            .require(fromAddr != ZERO_ADDRESS, "ERC20: transfer from the zero address")
+            .require(toAddr != ZERO_ADDRESS, "ERC20: transfer to the zero address")
+            .require(fromBalance >= amount, "ERC20: transfer amount exceeds balance")
+            .mapState(s => {
+                val newBalances =
+                    if (fromAddr == toAddr) {
+                        s.balanceOf
+                    } else {
+                        // Comment from ERC20.sol (see the above link):
+                        // Overflow not possible: the sum of all balances is capped
+                        // by totalSupply, and the sum is preserved by
+                        // decrementing then incrementing.
+                        s.balanceOf
+                        .set(fromAddr, fromBalance - amount)
+                        .setBy(toAddr, old => old + amount)
+                    }
+                {...s, balanceOf: newBalances}
+            })
+    }
+
+    /**
+     * ERC20: Moves amount tokens from the sender’s account to `toAddress`.
+     * Returns a boolean value indicating whether the operation succeeded.
+     *
+     * Quint: also return an error code and the new state.
+     * If the error != "", the new state should be applied.
+     */
+    pure def transfer(state: Erc20State, sender: Address,
+            toAddr: Address, amount: Uint): Erc20Result = {
+        // `transfer` always returns true, but we should check Erc20Result.error
+        _transfer(state, sender, toAddr, amount)
+    }
+
+    /**
+     * ERC20: Returns the remaining number of tokens that spender will be allowed to
+     * spend on behalf of owner through transferFrom. This is zero by default.
+     *
+     * This value may change when approve or transferFrom are called.
+     *
+     * Quint: the actual allowance is set up to 0 in newErc20.
+     */
+    pure def allowance(state: Erc20State, owner: Address, spender: Address): Uint = {
+        state.allowance.get((owner, spender))
+    }
+
+    /**
+     * ERC20: Sets amount as the allowance of spender over the caller’s tokens.
+     *
+     * Returns a boolean value (and the new state) indicating whether the
+     * operation succeeded.
+     *
+     * Quint: also return an error code and the new state.
+     * If the error != "", the new state should be applied.
+     */
+    pure def approve(state: Erc20State, sender: Address,
+            spender: Address, amount: Uint): Erc20Result = {
+        Ok(state)
+            .require(sender != ZERO_ADDRESS, "ERC20: transfer from the zero address")
+            .require(spender != ZERO_ADDRESS, "ERC20: transfer to the zero address")
+            .mapState(s => {
+                // the case of sender == spender seems to be allowed
+                val newAllowance = state.allowance.set((sender, spender), amount)
+                {...s, allowance: newAllowance}
+            })
+    }
+
+    /**
+     * Moves amount tokens from `fromAddr` to `toAddr` using the allowance mechanism.
+     * amount is then deducted from the caller’s allowance.
+     *
+     * Returns a boolean value indicating whether the operation succeeded.
+     *
+     * Quint: also return an error code and the new state.
+     * If the error != "", the new state should be applied.
+     */
+    pure def transferFrom(state: Erc20State, sender: Address,
+            fromAddr: Address, toAddr: Address, amount: Uint): Erc20Result = {
+        // _spendAllowance
+        val currentAllowance = state.allowance(fromAddr, sender)
+        Ok(state)
+            .require(currentAllowance >= amount, "ERC20: insufficient allowance")
+            .require(fromAddr != ZERO_ADDRESS, "ERC20: approve from the zero address")
+            .require(toAddr != ZERO_ADDRESS, "ERC20: approve to the zero address")
+            .mapState(s => {
+                if (currentAllowance == MAX_UINT) {
+                    // allowance is not subtracted in this case
+                    s
+                } else {
+                    // update allowances
+                    val newAllowance = s.allowance.setBy((fromAddr, sender), old => old - amount)
+                    {...s, allowance: newAllowance}
+                }})
+            // do the transfer
+            .flatMap(s => s._transfer(fromAddr, toAddr, amount))
+    }
+
+    // Properties that do not belong to the original EIP20 spec,
+    // but they should hold true.
+
+    pure def sumOverBalances(balances: Address -> int): int = {
+        balances.keys().fold(0, (sum, a) => sum + balances.get(a))
+    }
+
+    // The total supply, as stored in the state,
+    // is equal to the sum of amounts over all balances.
+    pure def isTotalSupplyCorrect(state: Erc20State): bool = {
+      state.balanceOf.sumOverBalances() == state.totalSupply
+    }
+
+    // Zero address should not carry coins.
+    pure def isZeroAddressEmpty(state: Erc20State): bool = {
+        state.balanceOf.get(ZERO_ADDRESS) == 0
+    }
+
+    // There are no overflows in totalSupply, balanceOf, and approve.
+    pure def isNoOverflows(state: Erc20State): bool = and {
+        isUint(state.totalSupply),
+        state.balanceOf.keys().forall(a => isUint(state.balanceOf.get(a))),
+        state.allowance.keys().forall(a => isUint(state.allowance.get(a))),
+    }
+}
diff --git a/doc/rfcs/rfc001-sum-types/rfc001-sum-types.org b/doc/rfcs/rfc001-sum-types/rfc001-sum-types.org
new file mode 100644
index 000000000..ce6131536
--- /dev/null
+++ b/doc/rfcs/rfc001-sum-types/rfc001-sum-types.org
@@ -0,0 +1,1124 @@
+#+TITLE: RFC 001: Extend Quint with Row-Polymorphic Sum Types
+#+AUTHOR: Shon Feder
+#+DATE: <2023-08-03 Thu>
+#+LATEX_COMPILER: xelatex
+
+* Overview
+This section gives a concise overview of the principle proposal. In
+depth discussion follows in [[Discussion][Discuisson]].
+
+** Concrete syntax
+The concrete syntax falls into three categories, corresponding three aspects of
+the semantics:
+
+- Declaring that a type is allowed in a context.
+- Constructing an element of the declared type.
+- Eliminating an element of the declared type (to derive an element of some
+  other type).
+
+Here we merely state the proposed syntax. See [[Concrete Syntax][the discussion of concrete syntax]]
+for consideration of motivations and trade offs.
+
+*** Declaration
+The proposed syntax fits complements our syntax for records and follows the
+precedent of most languages that include support for general sum-types:
+
+#+begin_src quint
+type T =
+  | A(int)
+  | B(str)
+  | C
+#+end_src
+
+As indicated by =C=, labels with no associated expression type are allowed.
+These are sugar for a label associated with the unit type (i.e., the empty
+record). The above is therefore a representation of
+
+#+begin_src quint
+type T =
+  | A(int)
+  | B(str)
+  | C({})
+#+end_src
+
+*** Constructors
+
+Internally, we need to need add an operator =variant= similar to the "injection"
+operator from [[https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/][Leijen05]]:
+
+#+begin_src haskell
+<l = _> :: ∀αr . α → <l :: α | r > -- injection
+#+end_src
+
+
+This operation injects an expression of type =α= into a sum-type that includes a
+variant associating label =l= with type =α=.  However, if we don't want to
+expose the row-polymorphism to users, we'll need a more restrictive typing. This
+is discussed in the section on typing rules.
+
+We provide syntax sugar for users: when a sum type declaration is parsed,
+constructor operations for each variant will be generated internally. E.g., for
+the type =T= defined above, we will add to the context the following operators:
+
+#+begin_src quint
+pure def A(x:int): T = variant(A, x)
+pure def B(x:str): T = variant(B, x)
+pure def C(): T      = variant(C, {})
+#+end_src
+
+*** Case analyses
+Expressions of a sum type can be eliminated using a case analysis via
+a =match= statement. Following Rust's syntax, we write that as
+
+#+begin_src quint
+match e {
+  | A(a) => ...
+  | B(b) => ...
+  | C    => ...
+}
+#+end_src
+
+This construct can either be a primitive or syntax sugar for a more
+primitive =decompose= operator, discussed below.
+
+We could also consider a case analysis ={ A(a) => e1, B(b) => e2, C => e3 }= --
+where =e1, e2, e3 : S= -- as syntax sugar for an anonymous operator of type =T
+=> S=. =match= would then be syntax sugar for operator application. This follows
+Scala's case blocks or OCaml's =function= keyword and would allow idioms such
+as:
+
+#+begin_src quint
+setOfTs.map({ A(a) => e1 | B(b) => e2 | C => e3 })
+#+end_src
+
+instead of requiring
+
+#+begin_src quint
+setOfTs.map(x => match x { A(a) => e1| B(b) => e2| C => e3 })
+#+end_src
+
+** Statics
+These type rules assume we keep our current approach of using quint
+strings for labels. But see my argument for simplifying our approach
+under [[*Drop the exotic operators][Drop the exotic operators]]. See the
+discussion in [[*Statics][Statics]] below for a detailed explanation and
+analysis.
+
+*** Construction
+The typing rule for constructing a variant of a sum type:
+
+#+CAPTION: SUM-INTRO
+$$
+\frac
+{
+\Gamma \vdash e \colon (t, c) \quad
+\Gamma \vdash `l' \colon str \quad
+definedType(s) \quad
+free(v)
+}
+{
+\Gamma \vdash \ variant(`l', e) \ :
+(s, c \land s \sim \langle \ l \colon t | v \ \rangle)
+}
+$$
+
+
+This rule is substantially different from [[https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/][Leijen05]]'s
+
+#+begin_src haskell
+<l = i> :: ∀αr . α → <l :: α | r > -- injection
+#+end_src
+
+
+because we have decided not to expose the underlying row-polymorphism for sum
+types at this point. This introduces the non-trivial complication of needing to
+introduce the typing context onto our judgments (this is what we gesture at with
+the side condition =definedType(s)=).
+
+*** Elimination
+
+The typing rule for eliminating a variant of a sum type via case
+analysis:
+
+#+CAPTION: SUM-ELIM
+$$
+\frac{
+\Gamma \vdash e : (s, c) \quad
+\Gamma, x_1 \vdash e_1 : (t, c_1) \quad \ldots \quad \Gamma, x_n \vdash e_n : (t, c_n) \quad
+\Gamma, \langle v \rangle \vdash e_{n+1} : (t, c_{n+1}) \quad
+fresh(v)
+}{
+\Gamma \vdash \ match \ e \ \{ i_1 : x_1 \Rightarrow e_1, \ldots, i_n : x_n \Rightarrow e_n \} : (t,
+c \land c_1 \land \ldots \land c_n \land c_{n+1} \land
+s \sim \langle i_1 : t_1, \ldots, i_n : t_n | v \rangle)
+}
+$$
+
+
+This gives a rule in our system that is sufficient to capture [[https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/][Leijen05]]'s
+
+#+begin_src haskell
+(l ∈ _ ? _ : _) :: ∀αβr . <l :: α | r> → (α → β) → (<r> → β) → β -- decomposition
+#+end_src
+
+since we can define decomposition for any label =L= via
+
+#+begin_src quint
+def decomposeL(e: (L(a) | r), f: a => b, default : r => b) = 
+  match e { 
+    | L(x) => f(x) 
+    | r    => default(r) 
+  }
+#+end_src
+
+However we can define =match= as syntax sugar for the decompose
+primitive if we prefer.
+
+** Dynamics
+The dynamics in the simulator should be straightforward and is not
+discussed here. Translation to Apalache for symbolic execution in the
+model checker is also expected to be relatively straight forward, since
+Apalache has a very similar form of row-based sum typing.
+
+The general rules for eager evaluation can be found in
+[[https://www.cs.cmu.edu/~rwh/pfpl.html][PFPL]], section 11.2.
+Additional design work for this will be prepared if needed.
+
+--------------
+
+This concludes the tl;dr overview of the proposal. The remaining is an
+indepth (still v. rough in places, discussion).
+
+* Discussion
+** Motivation
+Quint's type system currently supports product types. Product types
+(i.e., records, with tuples as a special case where fields are indexed
+by an ordinal) let us specify /conjunctions/ of data types in a way that
+is verifiable statically. This lets us describe more complex data
+structures in terms of values of specific types that *must* be packaged
+together. E.g., we might define a rectangle by its length and width and
+a triangle by the lengths of its three sides. Using Quint's existing
+syntax for product types, we'd specify this as follows:
+
+#+begin_src quint
+type Rectangle = 
+  { l : int
+  , w : int }
+type Triangle = 
+  { a : int
+  , b : int
+  , c : int }
+#+end_src
+
+Quint's type system does not yet have the the dual construct,
+[[https://en.wikipedia.org/wiki/Tagged_union][sum types]] (aka
+"variants", "co-products", or "tagged unions"). Sum types specify
+/disjunctions/ of data types in a way that is verifiable statically.
+This lets us describe mutually exclusive alternatives between distinct
+data structures that *may* occur together and be treated uniformly in
+some context. E.g., we might wish to specify a datatype for shapes, so
+we can work with collections that include both rectangles and triangles.
+Using one of the proposed syntax option that will be motivated in the
+following, this could be specified as
+
+#+begin_src quint
+type Shape =
+  | Rect(rectangle)
+  | Tri(triangle)
+#+end_src
+
+Having both product types and sum types (co-product types) gives us a
+simple and powerful idiom for specifying families of data structures:
+
+- We describe /what must be given together/ to form a product of the
+  specified type, and so /what we may always make use of/ by projection
+  when we are given such a product.
+- We describe /which alternatives may be supplied/ to form a co-product
+  of a specified type, and so /what we must be prepared to handle/
+  during case analysis when we are given such a co-product.
+
+E.g., a =rectangle= is defined by /both/ a length /and/ a width,
+packaged together, while a =shape= is defined /either/ by a rectangle
+/or/ a triangle. With these definitions established, we can then go on
+to form and reason about collections of shapes like =Set[shape]=, or
+define properties common to all shapes like
+=isEquilateral : shape => bool=[fn:1].
+
+** Context
+*** Existing plans and previous work
+We have always planned to support co-products in quint: their utility is well
+known and widely appreciated by engineers with experience in modern programming
+languages. We introduced co-products to Apalache in
+[[https://github.com/informalsystems/apalache/milestone/60]] for the same reasons.
+The design and implementation of the latter was worked out by [cite/t:@konnov]
+based on the paper [[https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/]["Extensible Records with Scoped Labels"]]. At the core of this
+design is a simple use of row-polymorphism that enables both extensible variants
+and extensible records, giving us products and co-products in a one neat
+package. The quint type system was also developed using row-polymorphism
+following this design. As a result of this forethought, extension of quint's
+type system and addition of syntax to support sum-types is expected to be
+relatively straightforward.
+
+*** The gist of extensible row-typed records and sum types
+The core concept in the row-based approach we've opted for is the
+following: we can use the same construct, called a "row", to represent
+the /conjoined/ labeled fields of a product type and the /alternative/
+labeled choices of a sum type. That the row types are polymorphic lets
+us extend the products and sums using row variables.
+
+E.g., given the row
+
+$$
+i_1 : t_1 \ , \ldots \ , i_n : i_n | v
+$$
+
+with each \(t_k\)-typed field indexed by label \(i_k\) for
+\(1 \le k \le n\) and the free row variable \(v\), then
+
+$$
+\{i_1 : t_1 \ , \ldots \ , i_n : i_n | v\}
+$$
+
+is an open record conjoining the fields, and
+
+$$
+\langle i_1 : t_1 \ , \ldots \ , i_n : i_n | v \rangle
+$$
+
+is an open sum type presenting the fields as (mutually exclusive)
+alternatives. Both types are extensible by substituting \(v\) with
+another (possibly open row). To represent a closed row, we omit the
+trailing \(| v\).
+
+*** Quint's current type system
+
+The [[https://github.com/informalsystems/quint/tree/main/doc/adr005-type-system.md][current type system supported by quint]] is based on a simplified version of
+the constraint-based system presented in [[https://www.microsoft.com/en-us/research/publication/complete-and-decidable-type-inference-for-gadts/]["Complete and Decidable Type Inference
+for GADTs"]] augmented with extensible (currently, just) records based on
+"Extensible Records with Scoped Labels". A wrinkle in this genealogy is that
+quint's type system includes neither GADTs nor scoped labels (and even the
+extensiblity supported for records is limited). Moreover, due to their
+respective foci, neither of the referenced papers includes a formalization the
+complete statics for product types or sum types, and while we have implemented
+support for product types in quint, we don't have our typing rules recorded.
+
+** Statics
+This section discusses the typing judgements that will allow us to
+statically verify correct introduction and elimination of expressions
+that are variants of a sum type. The following considerations have
+informed the structure in which the proposed statics are discussed:
+
+- Since sum-types are dual to product types, I consider their
+  complementary typing rules together: first I will present the relevant
+  rule for product types, then propose the complementary rule for sum
+  types. This should help maintain consistency between the two kinds of
+  typing judgements and ensure our implementations of both harmonize.
+- Since we don't have our existing product formation or elimination
+  rules described separate from the implementation, transcribing them
+  here can serve to juice our intuition, supplement our design
+  documentation, and perhaps give opportunity for refinement.
+- Since our homegrown type system has some idiosyncrasies that can
+  obscure the essence of the constructs under discussion, I precede the
+  exposition of each rule with a text-book example adapted from
+  [[https://www.cs.cmu.edu/~rwh/pfpl.html][Practical Foundations for
+  Programming Languages]]. This is only meant as a clarifying
+  touchstone.
+
+*** Eliminating products and introducing sums
+The elimination of products via projection and the introduction of sums
+via injection are the simplest of the two pairs of rules.
+
+**** Projection
+Here is a concrete example of projecting a value out of a record using
+our current syntax:
+
+#+begin_src quint
+val r : {a:int} = {a:1}
+val ex : int = r.a
+// Or, using our exotic field operator, which is currently the normal form
+val ex_ : int = r.field("a")
+#+end_src
+
+A textbook rule for eliminating an expression with a finite product
+types can be given as
+
+$$
+\frac
+{ \Gamma \vdash e \colon \{ i_1 \hookrightarrow \tau_1, \ \ldots, \ i_n \hookrightarrow \tau_n \} \quad (1 \le k \le n)}
+{ \Gamma \vdash e.i_k \colon \tau_k }
+$$
+
+Where \(i\) is drawn from a finite set of indexes used to label the
+components of the product (e.g., fields of a record or positions in a
+tuple) and \(i_j \hookrightarrow \tau_j\) maps the index \(i_j\) to the
+corresponding type \(\tau_j\).
+
+This rule tells us that, when an expression \(e\) with a product type is
+derivable from a context, we can eliminate it by projecting out of \(e\)
+with an index \(i_k\) (included in the type), giving an expression of
+the type \(t_k\) corresponding to that index. If we're given a bunch of
+stuff packaged together we can take out just the one part we want.
+
+In our current system, typechecking the projection of a value out of a record
+[[https://github.com/informalsystems/quint/blob/545b14fb8c19ac71d8f08fb8500ce9cc3cabf678/quint/src/types/specialConstraints.ts#L91-L120][implements]] the following rule
+
+$$
+\frac
+{ \Gamma \vdash e \colon (r, c) \quad \Gamma \vdash `l' \colon str \quad fresh(t) }
+{ \Gamma \vdash \ field(e, `l') \ \colon (t, c \land r \sim \{ \ l \colon t | tail\_t \ \}) }
+$$
+
+where
+
+- we use the judgement syntax established in
+  [[https://github.com/informalsystems/quint/tree/main/doc/adr005-type-system.md][ADR5]],
+  in which \(\Gamma \vdash e : (t, c)\) means that, in the typing
+  context \(\Gamma\), expression \(e\) can be derived with type \(t\)
+  under constraints \(c\),
+- \(fresh(t)\) is a side condition requiring the type variable \(t\) to
+  be fresh in \(\Gamma\),
+- \(`l'\) is a string literal with the internal representation \(l\),
+- \(c\) are the constraints derived for the type \(r\),
+- \(tail\_t\) is a free row-variable constructed by prefixing the fresh
+  variable \(t\) with "tail",
+- \(\{ \ l \colon t | tail\_t \ \}\) is the open row-based record type
+  with field, \(l\) assigned type \(t\) and free row- left as a free
+  variable,
+- and \(r \sim \{ \ l \colon t | tail\_t \ \}\) is a unification
+  constraint.
+
+Comparing the textbook rule with the rule in our system helps make the
+particular qualities and idiosyncrasies of our system very clear.
+
+The most critical difference w/r/t to the complexity of the typing rules
+derives form the fact that our system subordinates construction and
+elimination of records to the language level operator application rather
+than implementing it via a special constructs that work with product
+indexes (labels) directly. This is what necessitates the consideration
+of the string literal \(`l'\) in our premise. In our rule for type
+checking record projections we "lift" quint expressions (string literals
+for records and ints for products) into product indexes.
+
+The most salient difference is the use of unification constraints. This
+saves us having to "inspect" the record type to ensure the label is
+present and obtain its type. These are both accomplished instead via the
+unification of \(r\) with the minimal open record including the fresh
+type \(t\), which will end up holding the inferred type for the
+projected value iff the unification goes through. This feature of our
+type system is of special note for our aim of introducing sum-types:
+almost all the logic for ensuring the correctness of our typing
+judgements is delegated to the unification rules for the row-types that
+carry our fields for product type and sum types alike.
+
+**** Injection
+Here is a concrete example of injecting a value into a sum type:
+
+#+begin_src quint
+val n : int = 1
+val ex : A(int) = A(1)
+#+end_src
+
+A textbook rule for eliminating an expression belonging to a finite
+product type can be given as
+
+$$
+\frac
+{ \Gamma \vdash e \colon \tau_k  \quad (1 \le k \le n)}
+{ \Gamma \vdash i_k \cdot e \colon \langle i_1 \hookrightarrow \tau_1, \ \ldots, \ i_n \hookrightarrow \tau_n \rangle }
+$$
+
+Where \(i\) is drawn from a finite set of indexes used to label the
+possible alternatives of the co-product and
+\(i_j \hookrightarrow \tau_j\) maps the index \(i_j\) to the
+corresponding type \(\tau_j\). We use \(\langle \ldots \rangle\) to
+indicate the labeling is now disjunctive and \(i_k \cdot e\) as the
+injection of \(e\) into the sum type using label \(i_k\). Note the
+symmetry with complementary rule for projection out of a record: the
+only difference is that the (now disjunctive) row (resp. (now injected)
+expression) is swapped from premise to conclusion (resp. from conclusion
+to premise).
+
+This rule tells us that, when an expression \(e\) with a type \(t_k\) is
+derivable from a context, we can include it as an alternative in our sum
+type by injecting it with the label \(i_k\), giving an element of our
+sum type. If we're given a thing that has a type allowed by our
+alternatives, it can included among our alternatives.
+
+If we were following the row-based approach outlined in
+[[https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/][Leijen05]],
+then the proposed rule in our system, formed by seeking the same
+symmetry w/r/t projection out from a product, would be:
+
+$$
+\frac
+{ \Gamma \vdash e \colon (t, c) \quad \Gamma \vdash `l' \colon str \quad fresh(s) }
+{ \Gamma \vdash \ variant(`l', e) \ \colon (s, c \land s \sim \{ \ l \colon t | tail\_s \ \}) }
+$$
+
+Comparing this with our current rule for projecting out of records, we
+see the same symmetry: the (now disjunctive) row type is synthesized
+instead of being taken from the context.
+
+However, if we don't want to expose the row-polymorphism to users, we need a
+more constrained rule that will ensure the free row variable is not surfaced. We
+can address this by replacing the side condition requiring $s$ to be free with a side
+condition requiring that there it be defined, and in our constraint check that
+we can unify that defined type with a row that contains the given label with the
+expected type and is otherwise open.
+
+$$
+\frac
+{
+\Gamma \vdash e \colon (t, c) \quad
+\Gamma \vdash `l' \colon str \quad
+definedType(s) \quad
+free(v)
+}
+{
+\Gamma \vdash \ variant(`l', e) \ :
+(s, c \land s \sim \langle \ l \colon t | v \ \rangle)
+}
+$$
+
+
+Igor has voiced a strong preference that we do not allow anonymous or
+row-polymorphic sum types, which is why the last rule is proposed. It does
+complicate our typing rules, as it requires we draw from the typing context.
+
+
+*** Introducing products and eliminating sums
+Forming expressions of product types by backing them into records and
+eliminating expressions of sum types by case analysis exhibit the same
+duality, tho they are a bit more complex.
+
+**** Packing expressions into records
+Here is a concrete example of forming a record using our current syntax:
+
+#+begin_src quint
+val n : int = 1
+val s : str = "one"
+val ex : {a : int, b : str} = {a : n, b : s}
+// Or, using our exotic Rec operator, which is currently the normal form
+val ex_ : {a : int, b : str} = Rec("a", n, "b", s)
+#+end_src
+
+A textbook introduction rule for finite products is given as
+
+$$
+\frac
+{ \Gamma \vdash e_1 \colon \tau_1 \quad \ldots \quad \Gamma \vdash e_n \colon \tau_n }
+{ \Gamma \vdash \{ i_1 \hookrightarrow e_1, \ldots, i_n \hookrightarrow e_n \} \colon \{ i_1 \hookrightarrow \tau_1, \ldots, i_n \hookrightarrow \tau_n \} }
+$$
+
+This tells us that for any expressions
+\(e_1 : \tau_1, \ldots, e_n : \tau_n\) derivable from our context we can
+form a product that indexes those \(n\) expressions by
+\(i_1, \ldots, i_n\) distinct labels, and packages all data together in
+an expression of type
+\(\{ i_1 \hookrightarrow \tau_1, \ldots, i_n \hookrightarrow \tau_n \}\).
+If we're given all the things of the needed types, we can conjoint them
+all together into one compound package.
+
+The following rule describes our current implementation:
+
+$$
+\frac
+{ \Gamma \vdash (`i_1`, e_1 \colon (t_1, c_1)) \quad \ldots \quad \Gamma \vdash (`i_1`, e_n \colon (t_n, c_n)) \quad fresh(s) }
+{ \Gamma \vdash Rec(`i_1`, e_1, \ldots, `i_n`, e_n) \ \colon \ (s, c_1 \land \ldots \land c_n \land s \sim \{ i_1 \colon t_1, \ldots, i_n \colon t_n \}) }
+$$
+
+The requirement that our labels show up in the premise as quint strings
+paired with each element of the appropriate type is, again, an artifact
+of the exotic operator discussed later, as is the =Rec= operator in the
+conclusion that consumes these strings. Ignoring those details, this
+rule is quite similar to the textbook rule, except we use unification of
+the fresh variable =s= to propagate the type of the constructed record,
+and we have to do some bookkeeping with the constraints from each of the
+elements that will be packaged into the record.
+
+**** Performing case analysis
+Here is a concrete example of case analysis to eliminate an expression
+belonging to a sum type using the proposed syntax variants:
+
+#+begin_src quint
+val e : T = A(1)
+def describeInt(n: int): str = if (n < 0) then "negative" else "positive"
+val ex : str = match e {
+  | A(x) => describeInt(x)
+  | B(x) => x
+}
+#+end_src
+
+A textbook rule for eliminating an expression that is a variant of a
+finite sum type can be given as
+
+$$
+\frac{
+\Gamma \vdash e \colon 
+\langle i_1 \hookrightarrow \tau_1, \ldots, i_n \hookrightarrow \tau_n \rangle 
+\quad 
+\Gamma, x_1 : \tau_1 \vdash e_1 \colon \tau
+\quad 
+\ldots
+\quad 
+\Gamma, x_n : \tau_n \vdash e_n \colon \tau
+}
+{ \Gamma \vdash \ match \ e \ 
+\{ i_1 \cdot x_1 \hookrightarrow e_1 | \ldots | i_n \cdot x_n \hookrightarrow e_n \} : \tau }
+$$
+
+Note the complementary symmetry compared with the textbook rule for
+product construction: product construction requires =n= expressions to
+conclude with a single record-type expression combining them all; while
+sum type elimination requires a single sum-typed expression and =n= ways
+to convert each of the =n= alternatives of the sum type to conclude with
+a single expression of a type that does not need to appear in the sum
+type at all.
+
+The proposed rule for quint's type system is given without an attempt to
+reproduce our practice of using quint strings. This can be added in
+later if needed:
+
+$$
+\frac{
+\Gamma \vdash e : (s, c) \quad
+\Gamma, x_1 \vdash e_1 : (t, c_1) \quad \ldots \quad \Gamma, x_n \vdash e_n : (t, c_n) \quad
+\Gamma, \langle v \rangle \vdash e_{n+1} : (t, c_{n+1}) \quad
+fresh(v)
+}{
+\Gamma \vdash \ match \ e \ \{ i_1 : x_1 \Rightarrow e_1, \ldots, i_n : x_n \Rightarrow e_n \} : (t,
+c \land c_1 \land \ldots \land c_n \land c_{n+1} \land
+s \sim \langle i_1 : t_1, \ldots, i_n : t_n | v \rangle)
+}
+$$
+
+Compared with quint's rule for product construction we see the same
+complementary symmetry. However, we also see a striking difference:
+there is no row variable occurring in the product construction, but the
+row variable plays an essential function in sum type elimination of
+row-based variants. Row types in records are useful for extension
+operations (i.e., which we don't support in quint currently) and for
+operators that work over some known fields but leave the rest of the
+record contents variable. But the core idea formalized in a product type
+is that the constructor /must/ package all the specified things together
+so that the recipient /can/ chose any thing; thus, when a record is
+constructed we must supply all the things and there is no room for
+variability in the row. For sum types, in contrast the constructor /can/
+supply any one thing (of a valid alternate type), and requires the
+recipient /must/ be prepared to handle every possible alternative.
+
+In the presence of row-polymorphis, however, the responsibility of the
+recipient is relaxed: the recipient can just handle a subset of the
+possible alternatives, and if the expression falls under a label they
+are not prepared to handle, they can pass the remaining responsibility
+on to another handler.
+
+Here is a concrete example using the proposed syntax, note how we narrow
+the type of =T=:
+
+#+begin_src quint
+type T = A | B;;
+def f(e) = match e {
+  | A => 1
+  | B => 2
+  | _ => 0
+}
+
+// f can be applied to a value of type T
+let a : T = A
+let ex : int = f(A)
+
+// but since it has a fallback for an open row, it can also handle any other variant
+let foo = Foo
+let ex_ : int = f(foo)
+#+end_src
+
+Here's the equivalent evaluated in OCaml as proof of concept:
+
+#+begin_src ocaml
+utop # 
+type t = [`A | `B]
+let f = function
+  | `A -> 1
+  | `B -> 2
+  | _  -> 0
+let ex = f `A, f `Foo
+;;
+type t = [ `A | `B ]
+val f : [> `A | `B ] -> int = <fun>
+val ex : int * int = (1, 0)
+#+end_src
+
+All the features just discussed that come from row-polymorphism will not be
+available since we are choosing to suppress the row-typing.
+
+** Concrete Syntax
+
+*** Why not support "polymorphic variants"
+Our sum type system is based on row-polymorphism. The only widely used language
+I've found that uses row-polymorphism for extensible sum types is OCaml (and the
+alternative surface syntax, ReScript/Reason). For examples of their syntax for
+this interesting construct, see
+
+- ReScript :: https://rescript-lang.org/docs/manual/latest/polymorphic-variant
+- OCaml :: https://v2.ocaml.org/manual/polyvariant.html
+
+These very flexible types are powerful, but they introduce challenges to the
+syntax (and semantics) of programs. For example, supporting anonymous variant
+types requires a way of constructing variants without pre-defined constructors.
+Potential approaches to address this include:
+
+  - A special syntax that (ideally) mirrors the syntax of the type.
+  - A special lexical marker on the labels (what ReScrips and OCaml do),
+    e.g., =`A 1= or =#a 1= instead of =A(1)=.
+
+However, we have instead opted to hide the row-polymorphism, and not expose
+this.
+
+*** Declaration
+
+**** Why use the =|= syntax to separate alternatives?
+
+- In programming =|= is [[https://en.wikipedia.org/wiki/Vertical_bar#Disjunction][widely used for disjunction]]:
+  - regex
+  - boolean "or"
+  - bitwise "or"
+  - alternatives in BNF
+  - parallel execution on the pi-calculus
+- Many modern languages with support for sum types (or the more general union
+  types) use =|=, including
+  - [[https://docs.python.org/3/library/typing.html#typing.Union][Python]]
+  - [[https://www.typescriptlang.org/docs/handbook/2/everyday-types.html#union-types][TypeScript]]
+  - (of course) the MLs, Haskell, F#, Elm, OCaml, etc.
+
+**** Why not use =,= to separate alternatives?
+
+We have discussed modeling our concrete syntax for sum type declarations on
+Rust. But without changes to other parts of our language, this would leave the
+concrete syntax for type declarations too similar to record type declarations.
+
+This similarity is aggravated by the fact that we currently don't enforce any
+case-based syntactic rules to differentiate identifiers used for  operator
+names, variables, or module names, and we are currently planning to extend this
+same flexibility to variant labels, just as we do for record field labels.
+Thus, we could end up with a pair of declarations like:
+
+#+begin_src quint
+type T = {
+    A : int,
+    b : str,
+}
+
+type S = {
+    A(int),
+    b(str),
+}
+#+end_src
+
+We are not confident that the difference between =_:_= and =_(_)= will be enough
+to keep readers from confusing the two.
+
+But the chance of mistaking a record and sum type declaration is actually
+compounding a worse possible confusion: the part of a sum-type record enclosed
+in brackets is syntactically indistinguishable from a block of operators
+applications.
+
+Given we tend to read data structures from the outside in, we feel confident
+that we were going to avoid confusion by requiring declarations to use =|= to
+demarcate alternatives:
+
+#+begin_src quint
+type T = {
+    a : int,
+    B : str,
+}
+
+type S =
+    | A(int)
+    | b(str)
+#+end_src
+
+The latter seems much clearer to our team, and if we reflect this syntax also in
+=match=, it will give another foothold to help readers gather meaning when
+skimming the code.
+
+
+**** Could we just copy Rust exactly?
+
+In Rust, sum types are declared like this:
+
+#+begin_src rust
+enum T {
+  A(i64),
+  B(i64),
+  C
+}
+#+end_src
+
+If we just adopted this syntax directly without also changing our syntax for
+records, we would introduce
+
+- Breaks with our current convention around type declarations and
+  use of keywords.
+- May mislead users to try injecting values into the type via Rust's
+  =T::A(x)= syntax, which clashes with our current module syntax.
+- This would move us closer to Rust but further from languages like [[https://www.typescriptlang.org/docs/handbook/2/everyday-types.html#type-aliases][TypeScript]]
+  and Python.
+
+Rust't syntax makes pretty good sense _within the context of the rest of Rust's
+syntax_. Here is an overview:
+
+*declaration*
+
+#+begin_src rust
+struct Pair {
+    fst: u64,
+    snd: String
+}
+
+enum Either {
+    Left(u64),
+    Right(String)
+}
+#+end_src
+
+*construction*
+
+#+begin_src rust
+let s = Either::Left(4)
+let p = Pair{
+    fst: 4,
+    snd: "Two"
+}
+#+end_src
+
+*elimination*
+
+#+begin_src rust
+let two = p.snd
+let four = s match {
+    Either::Left(_) => 4,
+    Either::Right(_) => 4
+}
+#+end_src
+
+Note how the various syntactic elements work together to give consistent yet
+clearly differentiated forms of expression for dual constructs:
+
+- The prefix keyword for declarations consistently (=enum= vs. =struct=).
+- A unique constructor name is used consistently for forming a record or
+  variant.
+- Lexical rules add clear syntactic markers:
+  - Data constructors must begin with a capital letter
+  - Field names of a struct (and method names of a trait, and module names) must
+  begin with a lowercase letter.
+  - This ensures the syntax for module access and sum type construction are
+    unambiguous: =mymod::foo(x)= vs =MySumType::Foo(x)=.
+  - The caps/lower difference also helps reflect the duality between record
+    fields and sum type alternatives.
+
+Compare with the syntax proposed for quint this RFC:
+
+*declaration*
+
+#+begin_src quint
+type Pair = {
+  fst: int,
+  snd: str,
+}
+
+type Either =
+  | left(int),
+  | right(str)
+#+end_src
+
+*construction*
+
+#+begin_src quint
+let s = left(4)
+let p = {
+    fst: 4,
+    snd: "Two"
+}
+#+end_src
+
+*elimination*
+
+#+begin_src rust
+let two = p.snd
+let four = s match {
+    | left(_) => 4
+    | right(_) => 4
+}
+#+end_src
+
+Following the current quint syntax, we don't differentiate declaration with
+keywords or data construction with prefix use of type names. But we make up for
+this lost signal with the evident difference between =|= and =,=. This also
+compensates for the inability to differentiate based on capitalization.
+
+Finally, by adopting a syntax that if very similar to C++-like languages (like
+Rust), we risk presenting false friends. There are numerous subtle differences
+between quint and Rust, and if we lull users into thinking the syntax is
+roughly the same, they are likely to be disappointed when they discover that, e.g.,
+
+- Unlike Rust, conditions in =if= must be wrapped in =(...)=
+- Unlike Rust, conditions must have an =else= branch
+- Unlike Rust, =let= is not used for binding
+- Unlike Rust, type parameters are surrounded in =[...]= rather than =<...>=
+- Unlike Rust, operator are declared with =def=
+- Unlike Rust, type variables must begin with a lower-case letter
+
+In short, given how many ways we differ from Rust syntax already, adopting
+Rust's syntax for sum types would be confusing in the context of our current
+suntax and possibly lead to incorrect expectations.
+
+**** What if we want to be more Rust-like
+
+If we want to use a syntax for sum types that is closer to, or exactly the same
+as, Rust's, then we should make at least the following changes to the rest of
+our syntax to preserve harmony:
+
+- Require a prefix name relating to a type when constructing data, e.g., =Foo
+  {a: 1, b: 2}= for constructing a record of type =Foo=. (Note this would mean
+  dropping support for anonymous records types.)
+- Introduce a lexical distinction between capitalized identifiers, used for
+  data constructors (and type constants), and uncapitalized identifiers, used
+  for records field labels and operators.
+- Use keywords consistently for type declarations.
+
+Taking these changes into account, we could render the previous quint examples
+thus:
+
+*declaration*
+
+#+begin_src quint
+type Pair = struct {
+  fst: u64,
+  snd: String
+}
+
+type Either = enum {
+  Left(u64),
+  Right(String)
+}
+#+end_src
+
+*construction*
+
+#+begin_src quint
+let s = Left(4)
+let p = Pair {
+    fst: 4,
+    snd: "Two"
+}
+#+end_src
+
+*elimination*
+
+#+begin_src rust
+let two = p.snd
+let four = s match {
+    Left(_) => 4,
+    Right(_) => 4,
+}
+#+end_src
+
+
+*** Case analysis
+Ergonomic support for sum types requires eliminators, ideally in the
+form if case analysis by pattern matching.
+
+The proposed syntax is close to [[https://doc.rust-lang.org/book/ch18-03-pattern-syntax.html#matching-literals][Rust's pattern syntax]], modulo swapping =|=
+for =,= to be consistent with the type declaration syntax.
+
+Here's some example Rust for comparison
+
+#+begin_src rust
+    match x {
+        A    => println!("a"),
+        B    => println!("b"),
+        C(v) => println!("cv"),
+        _    => println!("anything"),
+    }
+#+end_src
+
+The =match= is a close analogue to our existing =if= expressions, and
+the reuse of the ==>= hints at the connection between case elimination
+and anonymous operators. The comma separated alternatives enclosed in
+={...}= follow the variadic boolean action operators, which seems
+fitting, since sum types are disjunction over data.
+
+One question if we adopt some form of pattern-based case analysis is how far we
+generalize the construct. Do we support pattern matching on scalars like ints
+and symbols? Do we support pattern matching to deconstruct compound data such as
+records and lists? What about sets? Do we allow pattern expressions to serve as
+anonymous operator (like Scala)?
+
+My guess is that in most cases the gains in expressivity of specs would justify
+the investment, but it is probably best to start with limiting support to
+defined sum types and seeing where we are after that.
+
+Until we have pattern matching introduced, we should flag a parsing error if the
+deconstructor argument is not a free variable, and inform the user that full pattern
+matching isn't yet supported.
+
+*** Sketch of an alternative syntax
+The syntax being proposed is chosen because it is familiar to Rust programmers,
+and is deemed sufficient so long as we don't need to expose the underlying row
+polymorphism. However, it has the down-sides of being very similar to the syntax
+for records, which might lead to confusion. I've also considered a more distinctive alternative which
+is also more consistently complementary to our records syntax. This group of alternatives follows [[https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/][Leijen05]]:
+
+**** Declaration
+
+Reflecting the fact that both records and sum types are based on rows, we
+use the same pairing (=:=) and enumerating (=,=) syntax, but signal to move from
+a conjunctive to a disjunctive meaning of the row by changing the brackets:
+
+#+begin_src quint
+type T =
+  < A : int
+  , B : str
+  >
+#+end_src
+
+**** Injection
+
+Injection uses a syntax that is dual with projection on records: =.= projects
+values out of products and injects them into co-products:
+
+#+begin_src quint
+val a : T = <A.1>
+#+end_src
+
+Since this option gives a syntactically unambiguous representation of
+variant formation, there is no need to generate special injector operator, and
+=<_._>= can be the normal form for injection.
+
+Annotation of anonymous sum types is clear and unambiguous:
+
+#+begin_src quint
+def f(n: int): <C:int, D:str | s> =
+  if (n >= 0) <C.n> else <D."negative">
+#+end_src
+
+Compare with the corresponding annotation for a record type:
+
+#+begin_src quint
+def f(n: int): {C:int, D:str | s} =
+  if (n >= 0) {C:n, D:"positive"} else {C:n, B:"negative"}
+#+end_src
+
+**** Elimination
+
+Finally, elimination uses a syntax that is dual to record construction,
+signaling the similarity thru use of the surrounding curly braces, and
+difference via the presence of the fat arrows (this syntax is similar to the
+one proposed):
+
+#+begin_src quint
+match e {
+  A : a => ...,
+  B : b => ...
+}
+#+end_src
+
+** High-level implementation plan
+
+- Add parsing and extension of the IR for the syntax :: https://github.com/informalsystems/quint/pull/1092
+- Add generation of constructor operators :: https://github.com/informalsystems/quint/pull/1093
+- Add rules for type checking :: https://github.com/informalsystems/quint/issues/244
+- Add support in the simulator :: https://github.com/informalsystems/quint/issues/1033
+- Add support for converting to Apalache :: https://github.com/informalsystems/quint/issues/1034
+
+** Additional consideration
+*** Pattern matching
+We may want to consider support for pattern matching at some point. I suspect
+the =match= construct will make users want this, but then again perhaps quint
+is simple enough that we can do without this complication. We'd also have to
+consider carefully how this would work with conversion to the Apalache IR.
+
+*** User defined parametric type constructors
+
+If we want to gain the most value from the addition of sum types we should allow
+users to define parametric types such as =Option= and =Either=. See
+https://github.com/informalsystems/quint/issues/1073 .
+
+*** Drop the exotic operators
+- Remove the special product type operators =fieldNames=, =Rec=, =with=,
+  =label=, and =index=, or add support for first-class labels As is, I
+  think these are not worth the complexity and overhead.
+
+Compare our rule with the projection operation from "Extensible Records
+with Scoped Labels", which does not receive the label `l' as a string,
+instead treating it as a special piece of syntax:
+
+#+begin_src haskell
+(_.l) :: ∀r α. (l|r) ⇒ {l :: α | r } → α`
+#+end_src
+
+Another point of comparison is Haskell's
+[[https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-490003.15]["Datatypes
+with Field Labels"]], which generates a projection function for each
+label, so that defining the datatype
+
+#+begin_src haskell
+data S = S1 { a :: Int, b :: String }
+#+end_src
+
+will produce functions
+
+#+begin_src haskell
+a :: S -> Int
+b :: S -> String
+#+end_src
+
+**** Benefits
+
+***** Simplified typing rules
+Abandoning this subordination to normal operator application would leave
+us with a rule like the following for record projection:
+
+$$
+\frac
+{ \Gamma \vdash e \colon (r, c) \quad fresh(t) }
+{ \Gamma \vdash \ e.l \ \colon (t, c \land r \sim \{ \ l \colon t | tail\_t \ \}) }
+$$
+
+This would allow us to remove the checks for string literals, instead leaving that
+to the outermost, syntactic level of our static analysis. A similar
+simplification would follow for record construction: the rule for =Rec= would
+not need to validate that it had received an even number of argument of
+alternating string literals and values, since this would be statically
+guaranteed by the parsing rules for the \(\{ l_1 : v_1, \ldots, l_n : v_n \}\)
+syntax. This would be a case of opting for the [[https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/]["Parse, don't validate"]] strategy.
+
+***** Safer language
+
+The added surface area introduced by these operators have contributed to several
+bugs, including at least the ones discussed here:
+
+- https://github.com/informalsystems/quint/issues/169
+- https://github.com/informalsystems/quint/issues/816
+- https://github.com/informalsystems/quint/issues/1081
+
+***** More maintainable code base
+
+We are losing structure in our internal representation of expressions, which
+means we get less value out of typescript type system, have to do more work
+when converting to the Apalache IR, and have to deal with more fussy details. By
+converting the rich structures of records into an internal representation
+=Rec(expr1, ..., expr1)=
+
+- we lose the ability to ensure we are forming records correctly statically
+- have to do manual arithmetic to ensure fields and values are paired up
+  correctly
+- essentially reduce ourselves to a "stringly typed" representation, relying
+  entirely on detecting the =Rec= value in the =kind= field.
+
+
+[fn:1] The expressive power of these simple constructs comes from the
+       nice algebraic properties revealed when values of a type are
+       treated as equal up-to ismorphism. See, e.g.,
+       [[https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types]]
diff --git a/doc/rfcs/rfc001-sum-types/rfc001-sum-types.pdf b/doc/rfcs/rfc001-sum-types/rfc001-sum-types.pdf
new file mode 100644
index 000000000..c5da544e1
Binary files /dev/null and b/doc/rfcs/rfc001-sum-types/rfc001-sum-types.pdf differ
diff --git a/doc/rfcs/rfc001-sum-types/rfc001-sum-types.tex b/doc/rfcs/rfc001-sum-types/rfc001-sum-types.tex
new file mode 100644
index 000000000..817236dbb
--- /dev/null
+++ b/doc/rfcs/rfc001-sum-types/rfc001-sum-types.tex
@@ -0,0 +1,1236 @@
+% Created 2023-08-05 Sat 00:09
+% Intended LaTeX compiler: xelatex
+\documentclass[11pt]{article}
+\usepackage{graphicx}
+\usepackage{longtable}
+\usepackage{wrapfig}
+\usepackage{rotating}
+\usepackage[normalem]{ulem}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{capt-of}
+\usepackage{hyperref}
+\author{Shon Feder}
+\date{\textit{<2023-08-03 Thu>}}
+\title{RFC 001: Extend Quint with Row-Polymorphic Sum Types}
+\hypersetup{
+ pdfauthor={Shon Feder},
+ pdftitle={RFC 001: Extend Quint with Row-Polymorphic Sum Types},
+ pdfkeywords={},
+ pdfsubject={},
+ pdfcreator={Emacs 28.1 (Org mode 9.6.1)}, 
+ pdflang={English}}
+\begin{document}
+
+\maketitle
+\tableofcontents
+
+
+\section{Overview}
+\label{sec:orgabf3583}
+This section gives a concise overview of the principle proposal. In
+depth discussion follows in \hyperref[sec:org050246d]{Discuisson}.
+
+\subsection{Concrete syntax}
+\label{sec:orga6e64d7}
+The concrete syntax falls into three categories, corresponding three aspects of
+the semantics:
+
+\begin{itemize}
+\item Declaring that a type is allowed in a context.
+\item Constructing an element of the declared type.
+\item Eliminating an element of the declared type (to derive an element of some
+other type).
+\end{itemize}
+
+Here we merely state the proposed syntax. See \hyperref[sec:orgb377490]{the discussion of concrete syntax}
+for consideration of motivations and trade offs.
+
+\subsubsection{Declaration}
+\label{sec:orgf216e02}
+The proposed syntax fits complements our syntax for records and follows the
+precedent of most languages that include support for general sum-types:
+
+\begin{verbatim}
+type T =
+  | A(int)
+  | B(str)
+  | C
+\end{verbatim}
+
+As indicated by \texttt{C}, labels with no associated expression type are allowed.
+These are sugar for a label associated with the unit type (i.e., the empty
+record). The above is therefore a representation of
+
+\begin{verbatim}
+type T =
+  | A(int)
+  | B(str)
+  | C({})
+\end{verbatim}
+
+\subsubsection{Constructors}
+\label{sec:orgc7e9737}
+
+Internally, we need to need add an operator \texttt{variant} similar to the ``injection''
+operator from \href{https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/}{Leijen05}:
+
+\begin{verbatim}
+<l = _> :: ∀αr . α → <l :: α | r > -- injection
+\end{verbatim}
+
+
+This operation injects an expression of type \texttt{α} into a sum-type that includes a
+variant associating label \texttt{l} with type \texttt{α}.  However, if we don't want to
+expose the row-polymorphism to users, we'll need a more restrictive typing. This
+is discussed in the section on typing rules.
+
+We provide syntax sugar for users: when a sum type declaration is parsed,
+constructor operations for each variant will be generated internally. E.g., for
+the type \texttt{T} defined above, we will add to the context the following operators:
+
+\begin{verbatim}
+pure def A(x:int): T = variant(A, x)
+pure def B(x:str): T = variant(B, x)
+pure def C(): T      = variant(C, {})
+\end{verbatim}
+
+\subsubsection{Case analyses}
+\label{sec:orgc4b162c}
+Expressions of a sum type can be eliminated using a case analysis via
+a \texttt{match} statement. Following Rust's syntax, we write that as
+
+\begin{verbatim}
+match e {
+  | A(a) => ...
+  | B(b) => ...
+  | C    => ...
+}
+\end{verbatim}
+
+This construct can either be a primitive or syntax sugar for a more
+primitive \texttt{decompose} operator, discussed below.
+
+We could also consider a case analysis \texttt{\{ A(a) => e1, B(b) => e2, C => e3 \}} --
+where \texttt{e1, e2, e3 : S} -- as syntax sugar for an anonymous operator of type \texttt{T
+=> S}. \texttt{match} would then be syntax sugar for operator application. This follows
+Scala's case blocks or OCaml's \texttt{function} keyword and would allow idioms such
+as:
+
+\begin{verbatim}
+setOfTs.map({ A(a) => e1 | B(b) => e2 | C => e3 })
+\end{verbatim}
+
+instead of requiring
+
+\begin{verbatim}
+setOfTs.map(x => match x { A(a) => e1| B(b) => e2| C => e3 })
+\end{verbatim}
+
+\subsection{Statics}
+\label{sec:org04cad71}
+These type rules assume we keep our current approach of using quint
+strings for labels. But see my argument for simplifying our approach
+under \hyperref[sec:orgd5aba72]{Drop the exotic operators}. See the
+discussion in \hyperref[sec:org6da5dcb]{Statics} below for a detailed explanation and
+analysis.
+
+\subsubsection{Construction}
+\label{sec:org23575b1}
+The typing rule for constructing a variant of a sum type:
+
+$$
+\frac
+{
+\Gamma \vdash e \colon (t, c) \quad
+\Gamma \vdash `l' \colon str \quad
+definedType(s) \quad
+free(v)
+}
+{
+\Gamma \vdash \ variant(`l', e) \ :
+(s, c \land s \sim \langle \ l \colon t | v \ \rangle)
+}
+$$
+
+
+This rule is substantially different from \href{https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/}{Leijen05}'s
+
+\begin{verbatim}
+<l = i> :: ∀αr . α → <l :: α | r > -- injection
+\end{verbatim}
+
+
+because we have decided not to expose the underlying row-polymorphism for sum
+types at this point. This introduces the non-trivial complication of needing to
+introduce the typing context onto our judgments (this is what we gesture at with
+the side condition \texttt{definedType(s)}).
+
+\subsubsection{Elimination}
+\label{sec:orgf258cbd}
+
+The typing rule for eliminating a variant of a sum type via case
+analysis:
+
+$$
+\frac{
+\Gamma \vdash e : (s, c) \quad
+\Gamma, x_1 \vdash e_1 : (t, c_1) \quad \ldots \quad \Gamma, x_n \vdash e_n : (t, c_n) \quad
+\Gamma, \langle v \rangle \vdash e_{n+1} : (t, c_{n+1}) \quad
+fresh(v)
+}{
+\Gamma \vdash \ match \ e \ \{ i_1 : x_1 \Rightarrow e_1, \ldots, i_n : x_n \Rightarrow e_n \} : (t,
+c \land c_1 \land \ldots \land c_n \land c_{n+1} \land
+s \sim \langle i_1 : t_1, \ldots, i_n : t_n | v \rangle)
+}
+$$
+
+
+This gives a rule in our system that is sufficient to capture \href{https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/}{Leijen05}'s
+
+\begin{verbatim}
+(l ∈ _ ? _ : _) :: ∀αβr . <l :: α | r> → (α → β) → (<r> → β) → β -- decomposition
+\end{verbatim}
+
+since we can define decomposition for any label \texttt{L} via
+
+\begin{verbatim}
+def decomposeL(e: (L(a) | r), f: a => b, default : r => b) = 
+  match e { 
+    | L(x) => f(x) 
+    | r    => default(r) 
+  }
+\end{verbatim}
+
+However we can define \texttt{match} as syntax sugar for the decompose
+primitive if we prefer.
+
+\subsection{Dynamics}
+\label{sec:orgd77d8b6}
+The dynamics in the simulator should be straightforward and is not
+discussed here. Translation to Apalache for symbolic execution in the
+model checker is also expected to be relatively straight forward, since
+Apalache has a very similar form of row-based sum typing.
+
+The general rules for eager evaluation can be found in
+\href{https://www.cs.cmu.edu/\~rwh/pfpl.html}{PFPL}, section 11.2.
+Additional design work for this will be prepared if needed.
+
+\noindent\rule{\textwidth}{0.5pt}
+
+This concludes the tl;dr overview of the proposal. The remaining is an
+indepth (still v. rough in places, discussion).
+
+\section{Discussion}
+\label{sec:org050246d}
+\subsection{Motivation}
+\label{sec:org2103e46}
+Quint's type system currently supports product types. Product types
+(i.e., records, with tuples as a special case where fields are indexed
+by an ordinal) let us specify \emph{conjunctions} of data types in a way that
+is verifiable statically. This lets us describe more complex data
+structures in terms of values of specific types that \textbf{must} be packaged
+together. E.g., we might define a rectangle by its length and width and
+a triangle by the lengths of its three sides. Using Quint's existing
+syntax for product types, we'd specify this as follows:
+
+\begin{verbatim}
+type Rectangle = 
+  { l : int
+  , w : int }
+type Triangle = 
+  { a : int
+  , b : int
+  , c : int }
+\end{verbatim}
+
+Quint's type system does not yet have the the dual construct,
+\href{https://en.wikipedia.org/wiki/Tagged\_union}{sum types} (aka
+``variants'', ``co-products'', or ``tagged unions''). Sum types specify
+\emph{disjunctions} of data types in a way that is verifiable statically.
+This lets us describe mutually exclusive alternatives between distinct
+data structures that \textbf{may} occur together and be treated uniformly in
+some context. E.g., we might wish to specify a datatype for shapes, so
+we can work with collections that include both rectangles and triangles.
+Using one of the proposed syntax option that will be motivated in the
+following, this could be specified as
+
+\begin{verbatim}
+type Shape =
+  | Rect(rectangle)
+  | Tri(triangle)
+\end{verbatim}
+
+Having both product types and sum types (co-product types) gives us a
+simple and powerful idiom for specifying families of data structures:
+
+\begin{itemize}
+\item We describe \emph{what must be given together} to form a product of the
+specified type, and so \emph{what we may always make use of} by projection
+when we are given such a product.
+\item We describe \emph{which alternatives may be supplied} to form a co-product
+of a specified type, and so \emph{what we must be prepared to handle}
+during case analysis when we are given such a co-product.
+\end{itemize}
+
+E.g., a \texttt{rectangle} is defined by \emph{both} a length \emph{and} a width,
+packaged together, while a \texttt{shape} is defined \emph{either} by a rectangle
+\emph{or} a triangle. With these definitions established, we can then go on
+to form and reason about collections of shapes like \texttt{Set[shape]}, or
+define properties common to all shapes like
+\texttt{isEquilateral : shape => bool}\footnote{The expressive power of these simple constructs comes from the
+nice algebraic properties revealed when values of a type are
+treated as equal up-to ismorphism. See, e.g.,
+\url{https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types}}.
+
+\subsection{Context}
+\label{sec:orgea625f3}
+\subsubsection{Existing plans and previous work}
+\label{sec:orgc77cf04}
+We have always planned to support co-products in quint: their utility is well
+known and widely appreciated by engineers with experience in modern programming
+languages. We introduced co-products to Apalache in
+\url{https://github.com/informalsystems/apalache/milestone/60} for the same reasons.
+The design and implementation of the latter was worked out by ?? (????)
+based on the paper \href{https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/}{``Extensible Records with Scoped Labels''}. At the core of this
+design is a simple use of row-polymorphism that enables both extensible variants
+and extensible records, giving us products and co-products in a one neat
+package. The quint type system was also developed using row-polymorphism
+following this design. As a result of this forethought, extension of quint's
+type system and addition of syntax to support sum-types is expected to be
+relatively straightforward.
+
+\subsubsection{The gist of extensible row-typed records and sum types}
+\label{sec:org6428ac3}
+The core concept in the row-based approach we've opted for is the
+following: we can use the same construct, called a ``row'', to represent
+the \emph{conjoined} labeled fields of a product type and the \emph{alternative}
+labeled choices of a sum type. That the row types are polymorphic lets
+us extend the products and sums using row variables.
+
+E.g., given the row
+
+$$
+i_1 : t_1 \ , \ldots \ , i_n : i_n | v
+$$
+
+with each \(t_k\)-typed field indexed by label \(i_k\) for
+\(1 \le k \le n\) and the free row variable \(v\), then
+
+$$
+\{i_1 : t_1 \ , \ldots \ , i_n : i_n | v\}
+$$
+
+is an open record conjoining the fields, and
+
+$$
+\langle i_1 : t_1 \ , \ldots \ , i_n : i_n | v \rangle
+$$
+
+is an open sum type presenting the fields as (mutually exclusive)
+alternatives. Both types are extensible by substituting \(v\) with
+another (possibly open row). To represent a closed row, we omit the
+trailing \(| v\).
+
+\subsubsection{Quint's current type system}
+\label{sec:org12dc16c}
+
+The \href{https://github.com/informalsystems/quint/tree/main/doc/adr005-type-system.md}{current type system supported by quint} is based on a simplified version of
+the constraint-based system presented in \href{https://www.microsoft.com/en-us/research/publication/complete-and-decidable-type-inference-for-gadts/}{``Complete and Decidable Type Inference
+for GADTs''} augmented with extensible (currently, just) records based on
+``Extensible Records with Scoped Labels''. A wrinkle in this genealogy is that
+quint's type system includes neither GADTs nor scoped labels (and even the
+extensiblity supported for records is limited). Moreover, due to their
+respective foci, neither of the referenced papers includes a formalization the
+complete statics for product types or sum types, and while we have implemented
+support for product types in quint, we don't have our typing rules recorded.
+
+\subsection{Statics}
+\label{sec:org6da5dcb}
+This section discusses the typing judgements that will allow us to
+statically verify correct introduction and elimination of expressions
+that are variants of a sum type. The following considerations have
+informed the structure in which the proposed statics are discussed:
+
+\begin{itemize}
+\item Since sum-types are dual to product types, I consider their
+complementary typing rules together: first I will present the relevant
+rule for product types, then propose the complementary rule for sum
+types. This should help maintain consistency between the two kinds of
+typing judgements and ensure our implementations of both harmonize.
+\item Since we don't have our existing product formation or elimination
+rules described separate from the implementation, transcribing them
+here can serve to juice our intuition, supplement our design
+documentation, and perhaps give opportunity for refinement.
+\item Since our homegrown type system has some idiosyncrasies that can
+obscure the essence of the constructs under discussion, I precede the
+exposition of each rule with a text-book example adapted from
+\href{https://www.cs.cmu.edu/\~rwh/pfpl.html}{Practical Foundations for
+Programming Languages}. This is only meant as a clarifying
+touchstone.
+\end{itemize}
+
+\subsubsection{Eliminating products and introducing sums}
+\label{sec:org5178260}
+The elimination of products via projection and the introduction of sums
+via injection are the simplest of the two pairs of rules.
+
+\begin{enumerate}
+\item Projection
+\label{sec:org6c8b9ea}
+Here is a concrete example of projecting a value out of a record using
+our current syntax:
+
+\begin{verbatim}
+val r : {a:int} = {a:1}
+val ex : int = r.a
+// Or, using our exotic field operator, which is currently the normal form
+val ex_ : int = r.field("a")
+\end{verbatim}
+
+A textbook rule for eliminating an expression with a finite product
+types can be given as
+
+$$
+\frac
+{ \Gamma \vdash e \colon \{ i_1 \hookrightarrow \tau_1, \ \ldots, \ i_n \hookrightarrow \tau_n \} \quad (1 \le k \le n)}
+{ \Gamma \vdash e.i_k \colon \tau_k }
+$$
+
+Where \(i\) is drawn from a finite set of indexes used to label the
+components of the product (e.g., fields of a record or positions in a
+tuple) and \(i_j \hookrightarrow \tau_j\) maps the index \(i_j\) to the
+corresponding type \(\tau_j\).
+
+This rule tells us that, when an expression \(e\) with a product type is
+derivable from a context, we can eliminate it by projecting out of \(e\)
+with an index \(i_k\) (included in the type), giving an expression of
+the type \(t_k\) corresponding to that index. If we're given a bunch of
+stuff packaged together we can take out just the one part we want.
+
+In our current system, typechecking the projection of a value out of a record
+\href{https://github.com/informalsystems/quint/blob/545b14fb8c19ac71d8f08fb8500ce9cc3cabf678/quint/src/types/specialConstraints.ts\#L91-L120}{implements} the following rule
+
+$$
+\frac
+{ \Gamma \vdash e \colon (r, c) \quad \Gamma \vdash `l' \colon str \quad fresh(t) }
+{ \Gamma \vdash \ field(e, `l') \ \colon (t, c \land r \sim \{ \ l \colon t | tail\_t \ \}) }
+$$
+
+where
+
+\begin{itemize}
+\item we use the judgement syntax established in
+\href{https://github.com/informalsystems/quint/tree/main/doc/adr005-type-system.md}{ADR5},
+in which \(\Gamma \vdash e : (t, c)\) means that, in the typing
+context \(\Gamma\), expression \(e\) can be derived with type \(t\)
+under constraints \(c\),
+\item \(fresh(t)\) is a side condition requiring the type variable \(t\) to
+be fresh in \(\Gamma\),
+\item \(`l'\) is a string literal with the internal representation \(l\),
+\item \(c\) are the constraints derived for the type \(r\),
+\item \(tail\_t\) is a free row-variable constructed by prefixing the fresh
+variable \(t\) with ``tail'',
+\item \(\{ \ l \colon t | tail\_t \ \}\) is the open row-based record type
+with field, \(l\) assigned type \(t\) and free row- left as a free
+variable,
+\item and \(r \sim \{ \ l \colon t | tail\_t \ \}\) is a unification
+constraint.
+\end{itemize}
+
+Comparing the textbook rule with the rule in our system helps make the
+particular qualities and idiosyncrasies of our system very clear.
+
+The most critical difference w/r/t to the complexity of the typing rules
+derives form the fact that our system subordinates construction and
+elimination of records to the language level operator application rather
+than implementing it via a special constructs that work with product
+indexes (labels) directly. This is what necessitates the consideration
+of the string literal \(`l'\) in our premise. In our rule for type
+checking record projections we ``lift'' quint expressions (string literals
+for records and ints for products) into product indexes.
+
+The most salient difference is the use of unification constraints. This
+saves us having to ``inspect'' the record type to ensure the label is
+present and obtain its type. These are both accomplished instead via the
+unification of \(r\) with the minimal open record including the fresh
+type \(t\), which will end up holding the inferred type for the
+projected value iff the unification goes through. This feature of our
+type system is of special note for our aim of introducing sum-types:
+almost all the logic for ensuring the correctness of our typing
+judgements is delegated to the unification rules for the row-types that
+carry our fields for product type and sum types alike.
+
+\item Injection
+\label{sec:orgc77f012}
+Here is a concrete example of injecting a value into a sum type:
+
+\begin{verbatim}
+val n : int = 1
+val ex : A(int) = A(1)
+\end{verbatim}
+
+A textbook rule for eliminating an expression belonging to a finite
+product type can be given as
+
+$$
+\frac
+{ \Gamma \vdash e \colon \tau_k  \quad (1 \le k \le n)}
+{ \Gamma \vdash i_k \cdot e \colon \langle i_1 \hookrightarrow \tau_1, \ \ldots, \ i_n \hookrightarrow \tau_n \rangle }
+$$
+
+Where \(i\) is drawn from a finite set of indexes used to label the
+possible alternatives of the co-product and
+\(i_j \hookrightarrow \tau_j\) maps the index \(i_j\) to the
+corresponding type \(\tau_j\). We use \(\langle \ldots \rangle\) to
+indicate the labeling is now disjunctive and \(i_k \cdot e\) as the
+injection of \(e\) into the sum type using label \(i_k\). Note the
+symmetry with complementary rule for projection out of a record: the
+only difference is that the (now disjunctive) row (resp. (now injected)
+expression) is swapped from premise to conclusion (resp. from conclusion
+to premise).
+
+This rule tells us that, when an expression \(e\) with a type \(t_k\) is
+derivable from a context, we can include it as an alternative in our sum
+type by injecting it with the label \(i_k\), giving an element of our
+sum type. If we're given a thing that has a type allowed by our
+alternatives, it can included among our alternatives.
+
+If we were following the row-based approach outlined in
+\href{https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/}{Leijen05},
+then the proposed rule in our system, formed by seeking the same
+symmetry w/r/t projection out from a product, would be:
+
+$$
+\frac
+{ \Gamma \vdash e \colon (t, c) \quad \Gamma \vdash `l' \colon str \quad fresh(s) }
+{ \Gamma \vdash \ variant(`l', e) \ \colon (s, c \land s \sim \{ \ l \colon t | tail\_s \ \}) }
+$$
+
+Comparing this with our current rule for projecting out of records, we
+see the same symmetry: the (now disjunctive) row type is synthesized
+instead of being taken from the context.
+
+However, if we don't want to expose the row-polymorphism to users, we need a
+more constrained rule that will ensure the free row variable is not surfaced. We
+can address this by replacing the side condition requiring \(s\) to be free with a side
+condition requiring that there it be defined, and in our constraint check that
+we can unify that defined type with a row that contains the given label with the
+expected type and is otherwise open.
+
+$$
+\frac
+{
+\Gamma \vdash e \colon (t, c) \quad
+\Gamma \vdash `l' \colon str \quad
+definedType(s) \quad
+free(v)
+}
+{
+\Gamma \vdash \ variant(`l', e) \ :
+(s, c \land s \sim \langle \ l \colon t | v \ \rangle)
+}
+$$
+
+
+Igor has voiced a strong preference that we do not allow anonymous or
+row-polymorphic sum types, which is why the last rule is proposed. It does
+complicate our typing rules, as it requires we draw from the typing context.
+\end{enumerate}
+
+
+\subsubsection{Introducing products and eliminating sums}
+\label{sec:org6a0635d}
+Forming expressions of product types by backing them into records and
+eliminating expressions of sum types by case analysis exhibit the same
+duality, tho they are a bit more complex.
+
+\begin{enumerate}
+\item Packing expressions into records
+\label{sec:org254ef28}
+Here is a concrete example of forming a record using our current syntax:
+
+\begin{verbatim}
+val n : int = 1
+val s : str = "one"
+val ex : {a : int, b : str} = {a : n, b : s}
+// Or, using our exotic Rec operator, which is currently the normal form
+val ex_ : {a : int, b : str} = Rec("a", n, "b", s)
+\end{verbatim}
+
+A textbook introduction rule for finite products is given as
+
+$$
+\frac
+{ \Gamma \vdash e_1 \colon \tau_1 \quad \ldots \quad \Gamma \vdash e_n \colon \tau_n }
+{ \Gamma \vdash \{ i_1 \hookrightarrow e_1, \ldots, i_n \hookrightarrow e_n \} \colon \{ i_1 \hookrightarrow \tau_1, \ldots, i_n \hookrightarrow \tau_n \} }
+$$
+
+This tells us that for any expressions
+\(e_1 : \tau_1, \ldots, e_n : \tau_n\) derivable from our context we can
+form a product that indexes those \(n\) expressions by
+\(i_1, \ldots, i_n\) distinct labels, and packages all data together in
+an expression of type
+\(\{ i_1 \hookrightarrow \tau_1, \ldots, i_n \hookrightarrow \tau_n \}\).
+If we're given all the things of the needed types, we can conjoint them
+all together into one compound package.
+
+The following rule describes our current implementation:
+
+$$
+\frac
+{ \Gamma \vdash (`i_1`, e_1 \colon (t_1, c_1)) \quad \ldots \quad \Gamma \vdash (`i_1`, e_n \colon (t_n, c_n)) \quad fresh(s) }
+{ \Gamma \vdash Rec(`i_1`, e_1, \ldots, `i_n`, e_n) \ \colon \ (s, c_1 \land \ldots \land c_n \land s \sim \{ i_1 \colon t_1, \ldots, i_n \colon t_n \}) }
+$$
+
+The requirement that our labels show up in the premise as quint strings
+paired with each element of the appropriate type is, again, an artifact
+of the exotic operator discussed later, as is the \texttt{Rec} operator in the
+conclusion that consumes these strings. Ignoring those details, this
+rule is quite similar to the textbook rule, except we use unification of
+the fresh variable \texttt{s} to propagate the type of the constructed record,
+and we have to do some bookkeeping with the constraints from each of the
+elements that will be packaged into the record.
+
+\item Performing case analysis
+\label{sec:org0e6979d}
+Here is a concrete example of case analysis to eliminate an expression
+belonging to a sum type using the proposed syntax variants:
+
+\begin{verbatim}
+val e : T = A(1)
+def describeInt(n: int): str = if (n < 0) then "negative" else "positive"
+val ex : str = match e {
+  | A(x) => describeInt(x)
+  | B(x) => x
+}
+\end{verbatim}
+
+A textbook rule for eliminating an expression that is a variant of a
+finite sum type can be given as
+
+$$
+\frac{
+\Gamma \vdash e \colon 
+\langle i_1 \hookrightarrow \tau_1, \ldots, i_n \hookrightarrow \tau_n \rangle 
+\quad 
+\Gamma, x_1 : \tau_1 \vdash e_1 \colon \tau
+\quad 
+\ldots
+\quad 
+\Gamma, x_n : \tau_n \vdash e_n \colon \tau
+}
+{ \Gamma \vdash \ match \ e \ 
+\{ i_1 \cdot x_1 \hookrightarrow e_1 | \ldots | i_n \cdot x_n \hookrightarrow e_n \} : \tau }
+$$
+
+Note the complementary symmetry compared with the textbook rule for
+product construction: product construction requires \texttt{n} expressions to
+conclude with a single record-type expression combining them all; while
+sum type elimination requires a single sum-typed expression and \texttt{n} ways
+to convert each of the \texttt{n} alternatives of the sum type to conclude with
+a single expression of a type that does not need to appear in the sum
+type at all.
+
+The proposed rule for quint's type system is given without an attempt to
+reproduce our practice of using quint strings. This can be added in
+later if needed:
+
+$$
+\frac{
+\Gamma \vdash e : (s, c) \quad
+\Gamma, x_1 \vdash e_1 : (t, c_1) \quad \ldots \quad \Gamma, x_n \vdash e_n : (t, c_n) \quad
+\Gamma, \langle v \rangle \vdash e_{n+1} : (t, c_{n+1}) \quad
+fresh(v)
+}{
+\Gamma \vdash \ match \ e \ \{ i_1 : x_1 \Rightarrow e_1, \ldots, i_n : x_n \Rightarrow e_n \} : (t,
+c \land c_1 \land \ldots \land c_n \land c_{n+1} \land
+s \sim \langle i_1 : t_1, \ldots, i_n : t_n | v \rangle)
+}
+$$
+
+Compared with quint's rule for product construction we see the same
+complementary symmetry. However, we also see a striking difference:
+there is no row variable occurring in the product construction, but the
+row variable plays an essential function in sum type elimination of
+row-based variants. Row types in records are useful for extension
+operations (i.e., which we don't support in quint currently) and for
+operators that work over some known fields but leave the rest of the
+record contents variable. But the core idea formalized in a product type
+is that the constructor \emph{must} package all the specified things together
+so that the recipient \emph{can} chose any thing; thus, when a record is
+constructed we must supply all the things and there is no room for
+variability in the row. For sum types, in contrast the constructor \emph{can}
+supply any one thing (of a valid alternate type), and requires the
+recipient \emph{must} be prepared to handle every possible alternative.
+
+In the presence of row-polymorphis, however, the responsibility of the
+recipient is relaxed: the recipient can just handle a subset of the
+possible alternatives, and if the expression falls under a label they
+are not prepared to handle, they can pass the remaining responsibility
+on to another handler.
+
+Here is a concrete example using the proposed syntax, note how we narrow
+the type of \texttt{T}:
+
+\begin{verbatim}
+type T = A | B;;
+def f(e) = match e {
+  | A => 1
+  | B => 2
+  | _ => 0
+}
+
+// f can be applied to a value of type T
+let a : T = A
+let ex : int = f(A)
+
+// but since it has a fallback for an open row, it can also handle any other variant
+let foo = Foo
+let ex_ : int = f(foo)
+\end{verbatim}
+
+Here's the equivalent evaluated in OCaml as proof of concept:
+
+\begin{verbatim}
+utop # 
+type t = [`A | `B]
+let f = function
+  | `A -> 1
+  | `B -> 2
+  | _  -> 0
+let ex = f `A, f `Foo
+;;
+type t = [ `A | `B ]
+val f : [> `A | `B ] -> int = <fun>
+val ex : int * int = (1, 0)
+\end{verbatim}
+
+All the features just discussed that come from row-polymorphism will not be
+available since we are choosing to suppress the row-typing.
+\end{enumerate}
+
+\subsection{Concrete Syntax}
+\label{sec:orgb377490}
+
+\subsubsection{Why not support ``polymorphic variants''}
+\label{sec:org4566b03}
+Our sum type system is based on row-polymorphism. The only widely used language
+I've found that uses row-polymorphism for extensible sum types is OCaml (and the
+alternative surface syntax, ReScript/Reason). For examples of their syntax for
+this interesting construct, see
+
+\begin{description}
+\item[{ReScript}] \url{https://rescript-lang.org/docs/manual/latest/polymorphic-variant}
+\item[{OCaml}] \url{https://v2.ocaml.org/manual/polyvariant.html}
+\end{description}
+
+These very flexible types are powerful, but they introduce challenges to the
+syntax (and semantics) of programs. For example, supporting anonymous variant
+types requires a way of constructing variants without pre-defined constructors.
+Potential approaches to address this include:
+
+\begin{itemize}
+\item A special syntax that (ideally) mirrors the syntax of the type.
+\item A special lexical marker on the labels (what ReScrips and OCaml do),
+e.g., \texttt{`A 1} or \texttt{\#a 1} instead of \texttt{A(1)}.
+\end{itemize}
+
+However, we have instead opted to hide the row-polymorphism, and not expose
+this.
+
+\subsubsection{Declaration}
+\label{sec:org9d13082}
+
+\begin{enumerate}
+\item Why use the \texttt{|} syntax to separate alternatives?
+\label{sec:org2585d56}
+
+\begin{itemize}
+\item In programming \texttt{|} is \href{https://en.wikipedia.org/wiki/Vertical\_bar\#Disjunction}{widely used for disjunction}:
+\begin{itemize}
+\item regex
+\item boolean ``or''
+\item bitwise ``or''
+\item alternatives in BNF
+\item parallel execution on the pi-calculus
+\end{itemize}
+\item Many modern languages with support for sum types (or the more general union
+types) use \texttt{|}, including
+\begin{itemize}
+\item \href{https://docs.python.org/3/library/typing.html\#typing.Union}{Python}
+\item \href{https://www.typescriptlang.org/docs/handbook/2/everyday-types.html\#union-types}{TypeScript}
+\item (of course) the MLs, Haskell, F\#, Elm, OCaml, etc.
+\end{itemize}
+\end{itemize}
+
+\item Why not use \texttt{,} to separate alternatives?
+\label{sec:org36d828e}
+
+We have discussed modeling our concrete syntax for sum type declarations on
+Rust. But without changes to other parts of our language, this would leave the
+concrete syntax for type declarations too similar to record type declarations.
+
+This similarity is aggravated by the fact that we currently don't enforce any
+case-based syntactic rules to differentiate identifiers used for  operator
+names, variables, or module names, and we are currently planning to extend this
+same flexibility to variant labels, just as we do for record field labels.
+Thus, we could end up with a pair of declarations like:
+
+\begin{verbatim}
+type T = {
+    A : int,
+    b : str,
+}
+
+type S = {
+    A(int),
+    b(str),
+}
+\end{verbatim}
+
+We are not confident that the difference between \texttt{\_:\_} and \texttt{\_(\_)} will be enough
+to keep readers from confusing the two.
+
+But the chance of mistaking a record and sum type declaration is actually
+compounding a worse possible confusion: the part of a sum-type record enclosed
+in brackets is syntactically indistinguishable from a block of operators
+applications.
+
+Given we tend to read data structures from the outside in, we feel confident
+that we were going to avoid confusion by requiring declarations to use \texttt{|} to
+demarcate alternatives:
+
+\begin{verbatim}
+type T = {
+    a : int,
+    B : str,
+}
+
+type S =
+    | A(int)
+    | b(str)
+\end{verbatim}
+
+The latter seems much clearer to our team, and if we reflect this syntax also in
+\texttt{match}, it will give another foothold to help readers gather meaning when
+skimming the code.
+
+
+\item Could we just copy Rust exactly?
+\label{sec:org9e9a2cd}
+
+In Rust, sum types are declared like this:
+
+\begin{verbatim}
+enum T {
+  A(i64),
+  B(i64),
+  C
+}
+\end{verbatim}
+
+If we just adopted this syntax directly without also changing our syntax for
+records, we would introduce
+
+\begin{itemize}
+\item Breaks with our current convention around type declarations and
+use of keywords.
+\item May mislead users to try injecting values into the type via Rust's
+\texttt{T::A(x)} syntax, which clashes with our current module syntax.
+\item This would move us closer to Rust but further from languages like \href{https://www.typescriptlang.org/docs/handbook/2/everyday-types.html\#type-aliases}{TypeScript}
+and Python.
+\end{itemize}
+
+Rust't syntax makes pretty good sense \uline{within the context of the rest of Rust's
+syntax}. Here is an overview:
+
+\textbf{declaration}
+
+\begin{verbatim}
+struct Pair {
+    fst: u64,
+    snd: String
+}
+
+enum Either {
+    Left(u64),
+    Right(String)
+}
+\end{verbatim}
+
+\textbf{construction}
+
+\begin{verbatim}
+let s = Either::Left(4)
+let p = Pair{
+    fst: 4,
+    snd: "Two"
+}
+\end{verbatim}
+
+\textbf{elimination}
+
+\begin{verbatim}
+let two = p.snd
+let four = s match {
+    Either::Left(_) => 4,
+    Either::Right(_) => 4
+}
+\end{verbatim}
+
+Note how the various syntactic elements work together to give consistent yet
+clearly differentiated forms of expression for dual constructs:
+
+\begin{itemize}
+\item The prefix keyword for declarations consistently (\texttt{enum} vs. \texttt{struct}).
+\item A unique constructor name is used consistently for forming a record or
+variant.
+\item Lexical rules add clear syntactic markers:
+\begin{itemize}
+\item Data constructors must begin with a capital letter
+\item Field names of a struct (and method names of a trait, and module names) must
+\end{itemize}
+begin with a lowercase letter.
+\begin{itemize}
+\item This ensures the syntax for module access and sum type construction are
+unambiguous: \texttt{mymod::foo(x)} vs \texttt{MySumType::Foo(x)}.
+\item The caps/lower difference also helps reflect the duality between record
+fields and sum type alternatives.
+\end{itemize}
+\end{itemize}
+
+Compare with the syntax proposed for quint this RFC:
+
+\textbf{declaration}
+
+\begin{verbatim}
+type Pair = {
+  fst: int,
+  snd: str,
+}
+
+type Either =
+  | left(int),
+  | right(str)
+\end{verbatim}
+
+\textbf{construction}
+
+\begin{verbatim}
+let s = left(4)
+let p = {
+    fst: 4,
+    snd: "Two"
+}
+\end{verbatim}
+
+\textbf{elimination}
+
+\begin{verbatim}
+let two = p.snd
+let four = s match {
+    | left(_) => 4
+    | right(_) => 4
+}
+\end{verbatim}
+
+Following the current quint syntax, we don't differentiate declaration with
+keywords or data construction with prefix use of type names. But we make up for
+this lost signal with the evident difference between \texttt{|} and \texttt{,}. This also
+compensates for the inability to differentiate based on capitalization.
+
+Finally, by adopting a syntax that if very similar to C++-like languages (like
+Rust), we risk presenting false friends. There are numerous subtle differences
+between quint and Rust, and if we lull users into thinking the syntax is
+roughly the same, they are likely to be disappointed when they discover that, e.g.,
+
+\begin{itemize}
+\item Unlike Rust, conditions in \texttt{if} must be wrapped in \texttt{(...)}
+\item Unlike Rust, conditions must have an \texttt{else} branch
+\item Unlike Rust, \texttt{let} is not used for binding
+\item Unlike Rust, type parameters are surrounded in \texttt{[...]} rather than \texttt{<...>}
+\item Unlike Rust, operator are declared with \texttt{def}
+\item Unlike Rust, type variables must begin with a lower-case letter
+\end{itemize}
+
+In short, given how many ways we differ from Rust syntax already, adopting
+Rust's syntax for sum types would be confusing in the context of our current
+suntax and possibly lead to incorrect expectations.
+
+\item What if we want to be more Rust-like
+\label{sec:org714fa9b}
+
+If we want to use a syntax for sum types that is closer to, or exactly the same
+as, Rust's, then we should make at least the following changes to the rest of
+our syntax to preserve harmony:
+
+\begin{itemize}
+\item Require a prefix name relating to a type when constructing data, e.g., \texttt{Foo
+  \{a: 1, b: 2\}} for constructing a record of type \texttt{Foo}. (Note this would mean
+dropping support for anonymous records types.)
+\item Introduce a lexical distinction between capitalized identifiers, used for
+data constructors (and type constants), and uncapitalized identifiers, used
+for records field labels and operators.
+\item Use keywords consistently for type declarations.
+\end{itemize}
+
+Taking these changes into account, we could render the previous quint examples
+thus:
+
+\textbf{declaration}
+
+\begin{verbatim}
+type Pair = struct {
+  fst: u64,
+  snd: String
+}
+
+type Either = enum {
+  Left(u64),
+  Right(String)
+}
+\end{verbatim}
+
+\textbf{construction}
+
+\begin{verbatim}
+let s = Left(4)
+let p = Pair {
+    fst: 4,
+    snd: "Two"
+}
+\end{verbatim}
+
+\textbf{elimination}
+
+\begin{verbatim}
+let two = p.snd
+let four = s match {
+    Left(_) => 4,
+    Right(_) => 4,
+}
+\end{verbatim}
+\end{enumerate}
+
+
+\subsubsection{Case analysis}
+\label{sec:org1404ef7}
+Ergonomic support for sum types requires eliminators, ideally in the
+form if case analysis by pattern matching.
+
+The proposed syntax is close to \href{https://doc.rust-lang.org/book/ch18-03-pattern-syntax.html\#matching-literals}{Rust's pattern syntax}, modulo swapping \texttt{|}
+for \texttt{,} to be consistent with the type declaration syntax.
+
+Here's some example Rust for comparison
+
+\begin{verbatim}
+    match x {
+        A    => println!("a"),
+        B    => println!("b"),
+        C(v) => println!("cv"),
+        _    => println!("anything"),
+    }
+\end{verbatim}
+
+The \texttt{match} is a close analogue to our existing \texttt{if} expressions, and
+the reuse of the \texttt{=>} hints at the connection between case elimination
+and anonymous operators. The comma separated alternatives enclosed in
+\texttt{\{...\}} follow the variadic boolean action operators, which seems
+fitting, since sum types are disjunction over data.
+
+One question if we adopt some form of pattern-based case analysis is how far we
+generalize the construct. Do we support pattern matching on scalars like ints
+and symbols? Do we support pattern matching to deconstruct compound data such as
+records and lists? What about sets? Do we allow pattern expressions to serve as
+anonymous operator (like Scala)?
+
+My guess is that in most cases the gains in expressivity of specs would justify
+the investment, but it is probably best to start with limiting support to
+defined sum types and seeing where we are after that.
+
+Until we have pattern matching introduced, we should flag a parsing error if the
+deconstructor argument is not a free variable, and inform the user that full pattern
+matching isn't yet supported.
+
+\subsubsection{Sketch of an alternative syntax}
+\label{sec:org726607c}
+The syntax being proposed is chosen because it is familiar to Rust programmers,
+and is deemed sufficient so long as we don't need to expose the underlying row
+polymorphism. However, it has the down-sides of being very similar to the syntax
+for records, which might lead to confusion. I've also considered a more distinctive alternative which
+is also more consistently complementary to our records syntax. This group of alternatives follows \href{https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/}{Leijen05}:
+
+\begin{enumerate}
+\item Declaration
+\label{sec:org78427f0}
+
+Reflecting the fact that both records and sum types are based on rows, we
+use the same pairing (\texttt{:}) and enumerating (\texttt{,}) syntax, but signal to move from
+a conjunctive to a disjunctive meaning of the row by changing the brackets:
+
+\begin{verbatim}
+type T =
+  < A : int
+  , B : str
+  >
+\end{verbatim}
+
+\item Injection
+\label{sec:orgd20c363}
+
+Injection uses a syntax that is dual with projection on records: \texttt{.} projects
+values out of products and injects them into co-products:
+
+\begin{verbatim}
+val a : T = <A.1>
+\end{verbatim}
+
+Since this option gives a syntactically unambiguous representation of
+variant formation, there is no need to generate special injector operator, and
+\texttt{<\_.\_>} can be the normal form for injection.
+
+Annotation of anonymous sum types is clear and unambiguous:
+
+\begin{verbatim}
+def f(n: int): <C:int, D:str | s> =
+  if (n >= 0) <C.n> else <D."negative">
+\end{verbatim}
+
+Compare with the corresponding annotation for a record type:
+
+\begin{verbatim}
+def f(n: int): {C:int, D:str | s} =
+  if (n >= 0) {C:n, D:"positive"} else {C:n, B:"negative"}
+\end{verbatim}
+
+\item Elimination
+\label{sec:org84c35ee}
+
+Finally, elimination uses a syntax that is dual to record construction,
+signaling the similarity thru use of the surrounding curly braces, and
+difference via the presence of the fat arrows (this syntax is similar to the
+one proposed):
+
+\begin{verbatim}
+match e {
+  A : a => ...,
+  B : b => ...
+}
+\end{verbatim}
+\end{enumerate}
+
+\subsection{High-level implementation plan}
+\label{sec:orgd09f6a5}
+
+\begin{description}
+\item[{Add parsing and extension of the IR for the syntax}] \url{https://github.com/informalsystems/quint/pull/1092}
+\item[{Add generation of constructor operators}] \url{https://github.com/informalsystems/quint/pull/1093}
+\item[{Add rules for type checking}] \url{https://github.com/informalsystems/quint/issues/244}
+\item[{Add support in the simulator}] \url{https://github.com/informalsystems/quint/issues/1033}
+\item[{Add support for converting to Apalache}] \url{https://github.com/informalsystems/quint/issues/1034}
+\end{description}
+
+\subsection{Additional consideration}
+\label{sec:org0d2407a}
+\subsubsection{Pattern matching}
+\label{sec:orgbddbca7}
+We may want to consider support for pattern matching at some point. I suspect
+the \texttt{match} construct will make users want this, but then again perhaps quint
+is simple enough that we can do without this complication. We'd also have to
+consider carefully how this would work with conversion to the Apalache IR.
+
+\subsubsection{User defined parametric type constructors}
+\label{sec:org1a4beae}
+
+If we want to gain the most value from the addition of sum types we should allow
+users to define parametric types such as \texttt{Option} and \texttt{Either}. See
+\url{https://github.com/informalsystems/quint/issues/1073} .
+
+\subsubsection{Drop the exotic operators}
+\label{sec:orgd5aba72}
+\begin{itemize}
+\item Remove the special product type operators \texttt{fieldNames}, \texttt{Rec}, \texttt{with},
+\texttt{label}, and \texttt{index}, or add support for first-class labels As is, I
+think these are not worth the complexity and overhead.
+\end{itemize}
+
+Compare our rule with the projection operation from ``Extensible Records
+with Scoped Labels'', which does not receive the label `l' as a string,
+instead treating it as a special piece of syntax:
+
+\begin{verbatim}
+(_.l) :: ∀r α. (l|r) ⇒ {l :: α | r } → α`
+\end{verbatim}
+
+Another point of comparison is Haskell's
+\href{https://www.haskell.org/onlinereport/haskell2010/haskellch3.html\#x8-490003.15}{``Datatypes
+with Field Labels''}, which generates a projection function for each
+label, so that defining the datatype
+
+\begin{verbatim}
+data S = S1 { a :: Int, b :: String }
+\end{verbatim}
+
+will produce functions
+
+\begin{verbatim}
+a :: S -> Int
+b :: S -> String
+\end{verbatim}
+
+\begin{enumerate}
+\item Benefits
+\label{sec:org36441ad}
+
+\begin{enumerate}
+\item Simplified typing rules
+\label{sec:org0e97219}
+Abandoning this subordination to normal operator application would leave
+us with a rule like the following for record projection:
+
+$$
+\frac
+{ \Gamma \vdash e \colon (r, c) \quad fresh(t) }
+{ \Gamma \vdash \ e.l \ \colon (t, c \land r \sim \{ \ l \colon t | tail\_t \ \}) }
+$$
+
+This would allow us to remove the checks for string literals, instead leaving that
+to the outermost, syntactic level of our static analysis. A similar
+simplification would follow for record construction: the rule for \texttt{Rec} would
+not need to validate that it had received an even number of argument of
+alternating string literals and values, since this would be statically
+guaranteed by the parsing rules for the \(\{ l_1 : v_1, \ldots, l_n : v_n \}\)
+syntax. This would be a case of opting for the \href{https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/}{``Parse, don't validate''} strategy.
+
+\item Safer language
+\label{sec:org53a2258}
+
+The added surface area introduced by these operators have contributed to several
+bugs, including at least the ones discussed here:
+
+\begin{itemize}
+\item \url{https://github.com/informalsystems/quint/issues/169}
+\item \url{https://github.com/informalsystems/quint/issues/816}
+\item \url{https://github.com/informalsystems/quint/issues/1081}
+\end{itemize}
+
+\item More maintainable code base
+\label{sec:org03c9b45}
+
+We are losing structure in our internal representation of expressions, which
+means we get less value out of typescript type system, have to do more work
+when converting to the Apalache IR, and have to deal with more fussy details. By
+converting the rich structures of records into an internal representation
+\texttt{Rec(expr1, ..., expr1)}
+
+\begin{itemize}
+\item we lose the ability to ensure we are forming records correctly statically
+\item have to do manual arithmetic to ensure fields and values are paired up
+correctly
+\item essentially reduce ourselves to a ``stringly typed'' representation, relying
+entirely on detecting the \texttt{Rec} value in the \texttt{kind} field.
+\end{itemize}
+\end{enumerate}
+\end{enumerate}
+\end{document}
\ No newline at end of file
diff --git a/quint/src/flattening.ts b/quint/src/flattening.ts
index 47508e07c..62e3acb0b 100644
--- a/quint/src/flattening.ts
+++ b/quint/src/flattening.ts
@@ -257,8 +257,8 @@ class Flatenner {
     return defsToFlatten.map(protoDef => this.copyDef(protoDef, qualifiedName))
   }
 
-  private copyDef(decl: QuintDef, qualifier: string | undefined): QuintDef {
-    const defWithQualifier = qualifier ? addNamespaceToDefinition(decl, qualifier, this.currentModuleNames) : decl
+  private copyDef(def: QuintDef, qualifier: string | undefined): QuintDef {
+    const defWithQualifier = qualifier ? addNamespaceToDefinition(def, qualifier, this.currentModuleNames) : def
     const defWithNewId = generateFreshIds(defWithQualifier, this.idGenerator, this.sourceMap, this.analysisOutput)
 
     return defWithNewId
diff --git a/quint/src/flattening/flattener.ts b/quint/src/flattening/flattener.ts
index 20b43e4b5..3082252e9 100644
--- a/quint/src/flattening/flattener.ts
+++ b/quint/src/flattening/flattener.ts
@@ -12,7 +12,7 @@
  * @module
  */
 
-import { Definition, LookupTable, builtinNames } from '../names/base'
+import { LookupDefinition, LookupTable, builtinNames } from '../names/base'
 import {
   QuintApp,
   QuintDef,
@@ -165,7 +165,7 @@ class Flattener implements IRVisitor {
   }
 }
 
-function getNamespaceForDef(def: Definition): string | undefined {
+function getNamespaceForDef(def: LookupDefinition): string | undefined {
   if (!def.namespaces) {
     return
   }
diff --git a/quint/src/ir/IRTransformer.ts b/quint/src/ir/IRTransformer.ts
index c471514d6..a451cb60f 100644
--- a/quint/src/ir/IRTransformer.ts
+++ b/quint/src/ir/IRTransformer.ts
@@ -274,7 +274,7 @@ export function transformType(transformer: IRTransformer, type: t.QuintType): t.
 }
 
 /**
- * Transforms a Quint declaration with a transformer, invoking the correspondent function for each
+ * Transforms a Quint declaration with a transformer, invoking the corresponding function for each
  * inner component.
  *
  * @param transformer: the IRTransformer instance with the functions to be invoked
diff --git a/quint/src/ir/IRprinting.ts b/quint/src/ir/IRprinting.ts
index 961614588..76315910c 100644
--- a/quint/src/ir/IRprinting.ts
+++ b/quint/src/ir/IRprinting.ts
@@ -31,8 +31,8 @@ export function moduleToString(quintModule: QuintModule): string {
 
 /**
  * Pretty prints a declaration. Includes a type annotation if the definition is
- * annotated, or if a type is provided. The annotation is preferred over the
- * type.
+ * annotated, or if a type is provided. A type annotation, if present, takes
+ * precedence over a type provided as argument to this function.
  *
  * @param decl the Quint declaration to be formatted
  * @param includeBody optional, whether to include the body of the declaration,
diff --git a/quint/src/names/base.ts b/quint/src/names/base.ts
index 132d55e3c..7561226a0 100644
--- a/quint/src/names/base.ts
+++ b/quint/src/names/base.ts
@@ -23,25 +23,18 @@ export type DefinitionKind = 'module' | 'def' | 'val' | 'assumption' | 'param' |
 /**
  * A definition to be stored in `DefinitionsByName` and `LookupTable`. Either a `QuintDef`
  * or a `QuintLambdaParameter`, with additional metadata fields
- *
- * A definition can be hidden, meaning it
- *
- * A definition can also have a list of `namespaces` and a `importedFrom` reference, to be used
- * to track the origins of a definition. Namespaces are added to the definition's name when it
- * is copied over to a module with a qualified name. `importedFrom` is a reference to the import/instance/export
- * statement that originated the definition, when the definition was copied from another module.
  */
-export type Definition = (QuintDef | ({ kind: 'param' } & QuintLambdaParameter)) & {
+export type LookupDefinition = (QuintDef | ({ kind: 'param' } & QuintLambdaParameter)) & {
   /* Hidden definitions won't be copied over to a module when an
    * import/intance/export statement is resolved. `hidden` can be removed with
    * `export` statements for the hidden definitions. */
   hidden?: boolean
   /* `namespaces` are names to add to the definition's name, when it
    * is copied from one module to another with a qualified name. Ordered from
-   * innermost to the outtermost. */
+   * innermost to the outermost namespace. */
   namespaces?: string[]
   /* importedFrom` is a reference to the import/instance/export statement that
-   * originated the definition, when the definition was copied from another
+   * originated the definition, if the definition was copied from another
    * module. */
   importedFrom?: QuintImport | QuintInstance | QuintExport
   /* `typeAnnotation` is the type annotation of the definition, if it has one.
@@ -55,7 +48,7 @@ export type Definition = (QuintDef | ({ kind: 'param' } & QuintLambdaParameter))
 /**
  * A module's definitions, indexed by name.
  */
-export type DefinitionsByName = Map<string, Definition & { hidden?: boolean }>
+export type DefinitionsByName = Map<string, LookupDefinition & { hidden?: boolean }>
 
 /**
  * Definitions for each module
@@ -73,7 +66,7 @@ export type DefinitionsByModule = Map<string, DefinitionsByName>
  *
  * This should be created by `resolveNames` from `resolver.ts`
  */
-export type LookupTable = Map<bigint, Definition>
+export type LookupTable = Map<bigint, LookupDefinition>
 
 /**
  * Copy the names of a definitions table to a new one, ignoring hidden
@@ -111,7 +104,7 @@ export function copyNames(
  *
  * @returns The definition with the namespaces added
  */
-export function addNamespacesToDef(def: Definition, namespaces: string[]): Definition {
+export function addNamespacesToDef(def: LookupDefinition, namespaces: string[]): LookupDefinition {
   // FIXME(#1111): This doesn't take care of some corner cases.
   return namespaces.reduce((def, namespace) => {
     if (def.namespaces && def.namespaces[def.namespaces?.length - 1] === namespace) {
diff --git a/quint/src/names/collector.ts b/quint/src/names/collector.ts
index 3a15e2527..33cb54529 100644
--- a/quint/src/names/collector.ts
+++ b/quint/src/names/collector.ts
@@ -27,7 +27,7 @@ import {
   qualifier,
 } from '../ir/quintIr'
 import {
-  Definition,
+  LookupDefinition,
   DefinitionsByModule,
   DefinitionsByName,
   LookupTable,
@@ -244,7 +244,7 @@ export class NameCollector implements IRVisitor {
    * @param source - An optional source identifier for the definition, if the
    * source is different than `def.id` (i.e. in import-like statements).
    */
-  collectDefinition(def: Definition, importedFrom?: QuintImport | QuintExport | QuintInstance): void {
+  collectDefinition(def: LookupDefinition, importedFrom?: QuintImport | QuintExport | QuintInstance): void {
     const identifier = (importedFrom as QuintImport)?.defName ?? def.name
     const source = importedFrom?.id ?? def.id
     if (identifier === '_') {
@@ -285,7 +285,7 @@ export class NameCollector implements IRVisitor {
    * @returns The definition object for the given identifier, or undefined if a
    * definitions with that identifier was never collected.
    */
-  getDefinition(identifier: string): Definition | undefined {
+  getDefinition(identifier: string): LookupDefinition | undefined {
     return this.definitionsByName.get(identifier)
   }
 
@@ -303,7 +303,7 @@ export class NameCollector implements IRVisitor {
     importedFrom?: QuintImport | QuintExport | QuintInstance
   ): void {
     const namespaces = importedFrom ? this.namespaces(importedFrom) : []
-    const newEntries: [string, Definition][] = [...newDefs.entries()].map(([identifier, def]) => {
+    const newEntries: [string, LookupDefinition][] = [...newDefs.entries()].map(([identifier, def]) => {
       const existingEntry = this.definitionsByName.get(identifier)
       if (existingEntry && existingEntry.id !== def.id) {
         this.recordConflict(identifier, existingEntry.id, def.id)
diff --git a/quint/src/types/aliasInliner.ts b/quint/src/types/aliasInliner.ts
index 92ce5ed2a..69df7ab39 100644
--- a/quint/src/types/aliasInliner.ts
+++ b/quint/src/types/aliasInliner.ts
@@ -14,7 +14,7 @@
  */
 
 import { IRTransformer, transformDefinition, transformModule, transformType } from '../ir/IRTransformer'
-import { Definition, LookupTable } from '../names/base'
+import { LookupDefinition, LookupTable } from '../names/base'
 import { AnalysisOutput } from '../quintAnalyzer'
 import { QuintDef, QuintModule } from '../ir/quintIr'
 import { QuintType } from '../ir/quintTypes'
@@ -35,7 +35,7 @@ export function inlineTypeAliases(
 ): { modules: QuintModule[]; table: LookupTable; analysisOutput: AnalysisOutput } {
   const modulesWithInlinedAliases = modules.map(m => inlineAliasesInModule(m, table))
   const tableWithInlinedAliases = new Map(
-    [...table.entries()].map(([id, def]): [bigint, Definition] => {
+    [...table.entries()].map(([id, def]): [bigint, LookupDefinition] => {
       if (def.kind === 'param') {
         const typeAnnotation = def.typeAnnotation ? inlineAliasesInType(def.typeAnnotation, table) : undefined
         return [id, { ...def, typeAnnotation }]
diff --git a/quint/test/builders/ir.ts b/quint/test/builders/ir.ts
index b6480eabc..6ba966c3a 100644
--- a/quint/test/builders/ir.ts
+++ b/quint/test/builders/ir.ts
@@ -39,7 +39,7 @@ export function buildDef(def: string): QuintDef {
   const quintModule = buildModuleWithDecls([def])
   const decl = quintModule.declarations[0]
   if (!isDef(decl)) {
-    throw new Error(`Error trying to build def from declaration that is not a def - ${JSONbig.stringify(decl)}`)
+    throw new Error(`Error trying to build def from declaration that is not a def: ${JSONbig.stringify(decl)}`)
   }
   return decl
 }