Precise type checking for records

[konnov]

What is discussed below is implemented in Type System 1.2, see the Transition to Type System 1.2.

---

As discussed in ADR002, the type checker is not checking the record types precisely. Consider the following operator:

Foo ==
  LET S == {[ type |-> "A", a |-> 1], [ type |-> "B", b |-> 2 ]} IN
  \E m \in S:
    m.a > m.b

The type checker assigns the type Set([type: Str, a: Int, b: Int]) to S. As a result, one can write the expression m.a > m.b, which does not make a lot of sense. This may lead to unexpected results in a large specification. In the above example, the model checker would just produce some values for m.a or m.b, which will probably result in a strange counterexample.

In issue #401, we have started the discussion on improving the type checker (and the model checker as well). We have to identify code patterns that admit precise type checking for records. The following example demonstrates available patterns and potential solutions. Some of them (A, C, F) are more stable than the other (B, D, E).

Please let us know what you think!

-------------------------- MODULE AwesomeRecords ------------------------------
VARIABLE
  (*
    @typeDef: MSG = [ type -> "A", a: Int ]
                 | [ type -> "B", b: Int ];
    @type: Set(MSG);
   *)
  msgs;

Init ==
    msgs = {[ type |-> "A", a |-> 0 ]}

(*
  This pattern appears in:
  https://github.com/tlaplus/Examples/blob/616c4c2e00dd7084c623d1dcc83b140279652fb4/specifications/Paxos/Paxos.tla#L131-L133

  This pattern is closed under negation.
  If A is well-typed, then ~A is well-typed.
 *)
A ==
    \* Pattern 1: filter a set of records by giving a precise type
    \E mm \in { m \in msgs: m.type = "A" }:
        msgs' = msgs \union { [ type |-> "B", b |-> mm.a + 1 ] }

(*
  This pattern appears in:

https://github.com/tlaplus/Examples/blob/616c4c2e00dd7084c623d1dcc83b140279652fb4/specifications/Paxos/Paxos.tla#L100-L106  https://github.com/tlaplus/Examples/blob/616c4c2e00dd7084c623d1dcc83b140279652fb4/specifications/allocator/AllocatorImplementation.tla#L90-L93

  This pattern is not closed under negation.
  Whereas B(m) is well-typed, ~B(m) is not.
  In this case, this should not be a problem, as B(m) is used as an action.
 *)

B(m) ==
    \* Pattern 2: We already have a record.
    \* Check its type and introduce a new name for it.
    \* The fields of record B may be accessed via the new name mb.
    /\ m.type = "B"
    \* The new name mm should be resolved as [ type -> "B", b: Int ]
    /\ LET mb == m IN
       msgs' = msgs \union { [ type -> "A", a |-> mb.b + 2 ] }
      
(*
  This pattern appears nowhere.
  It is closed under negation. If C(m) is well-typed, then ~C(m) is well-typed.
 *)
C(m) ==
    \* Pattern 3: compute the result by matching record types.
    \* This pattern looks appealing as it is similar to pattern matching in functional languages.
    LET new ==
        CASE m.type = "A" ->
            \* the new name ma should be resolved as [ type -> "A", a: Int ]
            LET ma == m IN 
            [ type |-> "B", ma + 1 ]

          [] m.type = "B" ->
            \* the new name mb should be resolved as [ type -> "B", b: Int ]
            LET mb == m IN
            [ type |-> "A", mb.b + 2 ]
    IN
    msgs' = msgs \union { new }
      
(*
  This pattern appears nowhere.
  The problem with this pattern is that it is not closed under negation.
  Whereas D(m) is well-typed, ~D(m) is not.
 *)
D(m) ==
    \* Pattern 4: refine the type with IF-THEN-ELSE.
    IF m.type = "B"
        \* The new name mm should be resolved as [ type -> "B", b: Int ]
        LET mb == m IN
        msgs' = msgs \union { [ type |-> "A", a |-> mb.b + 2 ] }
    ELSE
        \* It is obvious to a human that m.type = "A" here.
        \* However, to keep name resolution simple,
        \* the type checker will play dumb and complain.
        UNCHANGED msgs

(*
  This pattern appears in:
  https://github.com/tlaplus/Examples/blob/616c4c2e00dd7084c623d1dcc83b140279652fb4/specifications/Paxos/Paxos.tla#L208-L215

  This pattern is strange, as it is using short-circuiting of "=>".
  If we rewrite m.type = "A" => e in the equivalent form (m.type /= "A") \/ e, then the expression becomes ill-typed.
 *)
E ==
    \A m \in msgs:
        /\ m.type = "A" =>
            LET ma == m IN ma.a < 10
        /\ m.type = "B" =>
            LET mb == m IN mb.b < 10

\* We can make E closed under negation by rewriting it as F.
F ==
  /\ \A ma \in { m \in msgs: m.type = "A" }:
     ma.a < 10
  /\ \A mb \in { m \in msgs: m.type = "B" }:
     mb.b < 10

Next ==
    \/ A
    \/ \E m \in msgs:
       \/ B(m)
       \/ C(m)
       \/ D(m)

===============================================================================

[Isaac-DeFrain]

@konnov I know the point of this is make type inference of records more precise (I think this is a noble goal and I support your efforts here), but personally, I don't find it to be such a big deal to write type annotations for each operator in my specs. That being said, if it was still required to write annotations for the patterns that are not closed under negation and no longer required for the ones that are closed under negation, that would already be a nice improvement!
My main point: as long as the error messages are good enough, i.e. give sufficient evidence for a user to track down the problem without digging through output files, I don't see any problem with requiring users to write type annotations for certain patterns.
This may not be the correct venue for this discussion, but I want to make public my 👍 for a VS Code extension for apalache. It would be super nice to set a keybinding and run apalache typecheck with it.

[konnov]

A VSCode extension is a nice idea!

[konnov]

Yeah, I was not precise here. It is actually type checking, just making record information precise, as we have seen several people missing record fields, and that resulted in not so nice effects in the model checker. Our type checker does a bit of type inference too, that is why we sometimes confuse these too things :)

[lemmy]

Why not build on top of the existing VSCode extension (, which should eventually migrate to LSP)?

[Isaac-DeFrain]

@lemmy I agree with this suggestion! I am only the idea man here, I don't have any experience with VSCode extensions yet...

[konnov]

I can see, how we could update the type checker to deal with the patterns A, C, and F. They would not require any complex control-flow tracking. The patterns B, D, and E would require control-sensitive type checking.

[shonfeder]

@konnov Could you explain a bit why B is not well typed under negation? The problem isn't clear to me.

[konnov]

If you take a formal negation of B(m), it looks like this:

    \/ m.type /= "B"
    \* The new name mm should be resolved as [ type -> "B", b: Int ]
    \/ LET mb == m IN
       msgs' /= msgs \union { [ type -> "A", a |-> mb.b + 2 ] }

Even if the type checker could figure that m.type = "A", the access mb.b would result in a type-incorrect access.

[shonfeder]

Ah ha. I see. Thanks. Tricky :/

[shonfeder]

I'm not sure how useful my view will be, but I'm sharing in case the different
perspective might help clarify something or inspire some ideas.

After looking over these examples (here and in
https://github.com/tlaplus/Examples/blob/master/specifications/Paxos/Paxos.tla)
and getting some helpful points on our internal slack and from reading the
discussion on #401, it seems that we really are looking at cases where a sum
type is wanted.

It looks like this "type field" convention with records is an idiom for encoding
disjoint sets of heterogenous terms, and encoding of disjoint sets of
heterogenous terms is exactly what sum types are for.

iiuc, a perfectly adequate alternative representation of the messages in the
Paxos spec would be to use disjoint sets for the different message type. Then
instead of using subclauses to filter the correct message type out of the
heterogenous set of msgs, you'd just check for messages in the appropriate
set, e.g.,

Phase1b(acc) ==  
  \E m \in msgs : 
    /\ m.type = "phase1a"
    /\ aState[m.ins][acc].mbal < m.bal
    /\ ... 

would become

Phase1b(acc) ==
  \E m \in phase1a_msgs : 
    /\ aState[m.ins][acc].mbal < m.bal
    /\ ... 

This would be cumbersome to write and read in practice (mostly due to the need
for UNCHANGED, I think), but it seems to confirm that we're really looking at
a roundabout encoding of a disjoint set in this case.

There is a separate question of how we might refine the type checking of records
in general, but for the particular cases presented here, it looks to me like
our problem might be phrased as: "How do we codify this convention for encoding
sum types into our type system".

With this narrow focus, I wonder if we might not justify imposing some more
rigid constraints? Rather than supporting lots of different ways to deal with
these variants, could we treat this use of type-field pattern as a
special case -- only expecting it to be used to encode sum types -- and then only
allow eliminating it by a singleCASE?

With this constraint, something like

Phase1b(acc) ==
  \E m \in msgs : 
    /\ m.type = "phase1a"
    /\ ...

would need to be rewritten as

Phase1b(acc) ==
 \E m \in msgs :
   CASE m.type == "phase1a" -> 
        /\ <the rest of body of the operator>
   [] OTHER -> FALSE

I'm presupposing here that limiting the ways of typing and eliminating these
variants would make it feasible to support a less cumbersome syntax for
narrowing the types. In particular, this example assumes we could follow the
gradually typed languages like TypeScript and Python 3.7+, and use "type
narrowing" or "type guards" (see
https://www.typescriptlang.org/docs/handbook/2/narrowing.html#typeof-type-guards).
But in this case, we'd make it easier on ourselves by only using it in this
special situation to mimic the nice interface of eliminating disjoint unions by
case analysis.

Of course, as an alternative, we could explore going the other direction:
instead of narrowing the focus by treating this as a hack for bolting on support
for sum types, we could introduce union types into our type system, along with
general type narrowing, and then make this use of "type-fields" a special case.

As someone who has not written much TLA+, either of these two options are more
attractive solutions than going with variant types ala Ada. I can see how they'd
be a reasonable fit here, but it seems to me that combining record subtyping
with sum types needlessly conflates two unrelated kinds of types, and I'd expect
lots of needless confusion and complication to result from mixing these two
things up. (The conflation seems needless, imo, because it seems easy to
represent variant records in terms sum types.)

[konnov]

I am not sure how to make the model checker work with your example:

Phase1b(acc) ==
 \E m \in msgs :
   CASE m.type == "phase1a" -> 
        /\ <the rest of body of the operator>
   [] OTHER -> FALSE

Languages like TypeScript work without introducing an additional variable, probably, because they interpret the code after all. But we need an additional name to refer to the narrowed type. That's why I wanted to write the example like:

Phase1b(acc) ==
 \E m \in msgs :
   CASE m.type == "phase1a" -> 
        LET m1a == m IN
        /\ <the rest of body of the operator using m1a>
   [] OTHER -> FALSE

In this case, the type checker should figure out that m1a should have the narrowed type of 1a, and the model checker can do some form of coercion or casting.

[shonfeder]

Not sure about type script, by Python's gradual typing is via static analysis, not interpreting the language. Of course, maybe it uses machinery we don't want to support, but I think it'd be worth taking a look at how they do it before we force this kind of cumbersome idiom on users.

[konnov]

Sure. There are two questions:

1. Whether you can guarantee safety by type checking.
2. Whether you can compile into the right data structures after type checking.

As far as I understand, python and TypeScript solve problem 1. It is sufficient to ensure type safety. We have to solve problem 2.

[konnov]

I think that is why Scala requires you to give new names to the matched expressions. Otherwise, it should have been possible to use the name before matching.

[shonfeder]

If the type checker (and downstream phases) cannot function without having an intermediary variable, couldn't we have a transformation pass that detects this specific pattern ("destructuring" a sum type encoded in a record with a "type" field via case analysis) and inserts the intermediate variables?

[lemmy]

The farsite spec might be another source for common patterns related to records.

[konnov]

Wow. Is there any reason for why this spec is buried under the tlalplus source tree and does not appear in tlaplus-examples?

[konnov]

It looks like most of the record uses in the farsite spec are pretty standard. ServerLeaseResourcesModule.tla is probably the most interesting module here.

I don't know the spec, but it is surprising that the tests come in this order:

(*Defn*)PathRequestMessageConsumesResource(msg,resource)==
  /\ resource.fileID=msg.destFile
  /\ resource.type=SLRTDown

(*Defn*)PathRecallMessageRequiresResource(msg,resource)==
  /\ resource.fileID=msg.destFile
  /\ resource.type \in{SLRTRead,SLRTDown}

Also, this one looks like heavy artillery:

(*Defn*)LeaseRequestMessageConsumesResource(msg,resource)==
  /\ resource.fileID=msg.fileID
  /\ IF
       msg \in
       UNION
       {
       ReadFileRequestMessage,
       ResolveLabelRequestMessage,
       IdentifyParentRequestMessage
       }
     THEN
       resource.type=SLRTRead
     ELSE
       resource.type \in{SLRTRead,SLRTWrite}

[konnov]

I think that actually pattern A should be sufficient. It makes the most sense, as it is narrowing a set, and it is already used in the specs. Although pattern C would be probably nice to have, it requires more machinery and its benefits are not clear to me. After all, one can rewrite the spec a bit, it is not a programming language :D

[konnov]

An alternative proposed by @shonfeder and written by @Kukovec: https://apalache.informal.systems/docs/idiomatic/003record-sets.html

[shonfeder]

As we've discussed internally, a proper RFC fleshing out the rationale for this proposal and and its impact etc. is forthcomming.

[shonfeder]

I've not been able to muster the full RFC, but here are some rough notes.

Basic idea:

Enums (sum types) represent [[https://en.wikipedia.org/wiki/Disjoint_union][disjoint unions]].
Rather than trying to wedge something like sum types into TLA+'s records, what if we instead
follow the mathematical structure, and use TLA+'s existing support for reasoning
about sets to represent the mathematical structure we need.

I'm here suggesting an approach coming from a slightly different point of view
than that which we've taken for most of the discussion here: the aim in this
proposal is not to accommodate the current practice of dealing with collections
of heterogenous values, nor is it to figure out a workaround that will let
records more-or-less let us represent sum types; instead, the point of departure
here is to ask what would be a sensible and principled encoding of sum types
within the set theory that TLA+ already offers. Our approach to supporting
well-typed programs in Apalache could then be to provide some nice combinators
or syntax sugar allowing users to write statically type-safe specs that then
desugar into run-time safe TLA+.

To properly focus on the general problem, I don't discuss the particular
application to records. My assumption is that if we find a nice and general
solution to encoding sum types, then we can just treat record typing the same as
we do tuples, and encourage users to migrate to the sum-types.

Note that I am assuming (perhaps naively) that we could represent any sum-type
definition we can parse out of the source spec using smt2's declare-datatype.

Please note also that the spirit of this note is: "Could this be possible? Is
the following a useful way of thinking about the problem? What if we tried
this?"

Trivial recapitulation of the problem space

This section just presents the basic problem that sum-types are meant to solve.

Suppose our domain of discourse is represented by a set of heterogeneous
elements:

{{1}, "one", 1, 2, "two", {1, 2}, "three", 3, {1,2,3}}

To help reduce the clutter in the universe, we can organize this set into three
separate sets of homogeneous elements:

Ints == {1, 2, 3}
Strs == {"one", "two", "three"}
Sets == {{1}, {1, 2}, {1,2,3}}

This is nice, because we can now apply transformations and predicates to these
collections, without worrying if something will end up trying to compute
nonsense. So, e.g., we can do FoldSet(Plus(_,_), 0, Ints) or \E x \in IntSets: 3 \in x, without worrying that we'll try to add 1 and "one" or
check whether "one" \in 1. The pragmatic motivation for this segregation is
more the less the same one that leads us to keep shirts and pants in different
drawers.

However, we often do need to talk about heterogeneous collections of things!
For a contrived example, let's say that we want to talk about all the things in
our domain that exhibit "threeness", according to this definition:

IntThreeness(x) ==              x = 3
StrThreeness(x) ==              x = "three"
SetThreeness(x) == Cardinality(x) = 3

We can form:

Threes == { x \in Ints: IntThreeness(x) } \union { x \in Strs: StrThreeness(x) } \union { x \in Sets: SetThreeness(x) }

To end up with Threes = {3, "three", {1,2,3}}.

Of course, now we have mixed things up again, and we'll likely run into trouble
if we try to do stuff across all the members of Threes.

It'd be nice to have a way of talking about collections of heterogenous
things that lets us only concern ourselves with their commonalities when
appropriate, but also ensures we respect their distinctive differences, and
prevents us from inapt treatment to any member of the group.

A record of sets

The idom suggested in
https://apalache.informal.systems/docs/idiomatic/003record-sets.html let us
address a special case of this problem. The idea there is to always keep the
elements segregated into different sets, label each set with a field in a
record, and then pass around the record when we want to talk about the
collection. This essentially amounts to using a single record to represent the
same sets we've labeled above with operators. Our domain of discourse is now

Domain ==
  [ ints |-> {1, 2, 3}
  , strs |-> {"one", "two", "three"}
  , sets |-> {{1}, {1,2}, {1,2,3}}
  ]

Now our collection of Threes can be given as:

Threes ==
  [ ints |-> {x \in Domain.ints: IntThreeness(x)}
  , strs |-> {x \in Domain.strs: StrThreeness(x)}
  , sets |-> {x \in Domain.sets: SetThreeness(x)}
  ]

Which is quite cumbersome, but we can easily imagine all kinds of combinators to
make it easier to abstract away this detail, and let us treat the Domain (more
or less), as if it were a single collection. And, obviously, our typing
discipline is entirely adequate to give us static warnings if someone tries to,
e.g., FoldSet(Plus(_,_), 0, Threes).

There are evident limitations of this approach. The most important limitation is
that it is not a general solution. E.g., it doesn't help us at all with ordered
heterogenous sequences or functions with heterogeneous sources or targets. Less
important is that this solution doesn't expose any of the useful algebraic
properties that make sum types so useful.

Tagging with tuples

A naive approach following the example of discriminated unions provided on
Wikipedia would
use tuples to index each element with the set it comes from. This would give us
the following representation of the domain:

Domain ==
  { <<"Int", 1>>, <<"Int", 2>>, <<"Int", 3>>
  , <<"Str", "one">>, <<"Str", "two">>, <<"Str", "three">>
  , <<"Set", {1}>>, <<"Set", {1,2}>>, <<"Set", {1,2,3}>>
  }

Combinators to make working with such collections safe are easy to write, and
this representation works just as well for ordered sequences or functions.

Eliminators for these kinds of values is straight forward. E.g.,

ToInt(v) ==
  CASE v[1] = "Int" -> v[2]
  CASE v[1] = "Str" -> StrToInt(v[2])
  CASE v[1] = "Set" -> Cardinality(v[2])

Of course, neither Domain and ToInt is not well-typed according to the
current typing discipline! But bear in mind that the idea here is not that users
would write their spec using tuples to encode sum types. Rather, we would
present combinators or sugar that let's us guarantee correct static analysis,
and to preserve whatever typing information we need to produce a correct SMT
encoding. And, we have in mind the bonus that it can be desguared into TLA+ that
TLC can run.

Example combinators:

\* The type of elements in our domain
\* @type: Element = | Int of Int | Str of Str | Set of Set(Int);

\* >> Generated constructors (need not be visible to user):
\* @type: Int => Element;
ElementInt(x) == <<"Int", x>>
\* @type: Str => Element;
ElementStr(x) == <<"Str", x>>
\* @type: Set(Int) => Element;
ElementSet(x) == <<"Set", x>>

Domain == {ElementInt(1), ElementStr("one"), ElementSet({1}) (* etc... *)}
\* >> Generated eliminator
\* This is just the usual functional case-analysis
\* @type: (Element, Int => A, Str => A, Set => A) => A;
ElementCase(el, int(_), str(_), set(_)) ==
  CASE el[1] = "Int" -> int(el[2])
    [] el[1] = "Str" -> str(el[2])
    [] el[1] = "Set" -> set(el[2])

\* @type: A => A;
Id(x) == x

\* @type: Str => Int;
StrToInt(x) ==
  CASE x = "one"   -> 1
    [] x = "two"   -> 2
    [] x = "three" -> 3

\* @type: Element => Int;
ElementToInt(el) ==
  ElementCase(el
    Id,
    StrToInt,
    Cardinality
  )

There's a lot of handwaving here, but you get the idea.

Snowcat Compatible Representations

Clearly, a disadvantage of the representation using tuples as described above is
that it is incompatible with Snowcat, so even if it's feasible, it we'd need a
lot of magic relative to our current type checking to infer when an operator was
actually constructing a value of a sum type. We might try resolving this by
instead using a tuple of sets:

\* @type: Element = | Int of Int | Str of Str | Set of Set(Int);

\* >> Generated constructors:
\* @type: Int -> Element;
ElementInt(x) == <<{x}, {}, {}>>
ElementStr(x) == <<{}, {x}, {}>>
ElementSet(x) == <<{}, {}, {x}>>

Domain == {ElementInt(1), ElementStr("one"), ElementSet({1}) (* etc... *)}
\* Equivalent to {<<{1}, {}, {}>>, <<{}, {"one"}, {}>>, <<{}, {}, {{1}}>>}
 
\** >> Generated eliminator:
\* @type: (Element, Int => A, Str => A, Set => A) => A;
ElementCase(el, int(_), str(_), set(_)) ==
  CASE Cardinality(el[1]) = 1 -> int(CHOOSE x \in el[1]: TRUE)
    [] Cardinality(el[2]) = 1 -> str(CHOOSE x \in el[2]: TRUE)
    [] Cardinality(el[3]) = 1 -> set(CHOOSE x \in el[3]: TRUE)

Obviously, what we can do with tuples, we can also do with records.

Here is an attempted sketch exploring whether we can use a similar encoding, but
with records, to represent the prototypical sum type, usually called Either.
It also attempts to show the "algebraic" quality by giving an example of how we
might derive a representation of the Option type from the representation of
the Either.

\* sum type: A type /\ B type => A + B type
Either(A, B) == [left : A, right : B]

\* Intro
InLeft(x) == [left |-> {x}, right |-> {}]
InRight(x) == [left |-> {}, right |-> {x}]

\* Elim

\* @type: ([left: Set(A), right: Set(B)]) => Bool;
IsLeft(e) == Cardinality(e.left) = 1

\* @type: ([left: Set(A), right: Set(B)]) => Bool;
IsRight(e) == Cardinality(e.right) = 1

\* @type: ([left: Set(A), right: Set(B)], A => C, B => C) => C;
EitherElim(e, l(_), r(_)) ==
    IF IsLeft(e) THEN
        l(CHOOSE x \in e.left: TRUE)
    ELSE
        r(CHOOSE x \in e.right: TRUE)


\* @typeAlias: UNIT = Set(Str);
EXTypeAliases == TRUE

UNIT == "__UNIT__"

Option(A) == Either(A, {UNIT})

\* @type: A => [left: Set(A), right: UNIT];
Some(x) == InLeft(x)
\* @type: Set(A) => [left: Set(A), right: UNIT];
None(T) == InRight(UNIT)

\* TODO: Cannot constraint these types to only work on encoding of option...
\* @type: [left: Set(A), right: Set(B)] => Bool;
IsNone(o) == IsRight(o)

\* @type: [left: Set(A), right: Set(B)] => Bool;
IsSome(o) == IsLeft(o)

MapSome(T, f(_), o) ==
    EitherElim(o
    , LAMBDA x: Some(f(x))
    , LAMBDA x: None(T)
    )

In theory, if we can successfully encode the Either type in this (or a similar
way), then all other sum types can just be desugared into Either types.

Relation to record type checking

IIUC, if we can find a suitable encoding for general sum types, then we can deal with heterogenous
collections of records using that mechanism, and the record typing itself can just be reduced to the
simple typing of a product type (i.e., a tuple). I wonder if this can help us resolve both the type-safety
of the spec and also provide enough information to let us derive the types we need for the SMT encoding.

[konnov]

Thanks for the detailed write-up! This is a fresh idea. I especially like the idea of using eliminators with lambda operators. This is probably the way to go with eliminators, independently of the chosen approach. I am less certain about the representation with sets inside tuples, though I like this trick quite a bit! Especially, the test Cardinality(X) = 1 could be expensive. Alternatively, we could introduce the option type in the type system, so this check would not be expensive.

You are probably right in that there is no other way but to pack all possible options of a tagged union in a tuple or record. We can try to avoid it by using ADTs in z3, but I don't know how well z3 works with ADTs.

[shonfeder]

Very glad to hear that the notes might be of some use, at least for introducing possible approaches to consider.

re:

the test Cardinality(X) = 1 could be expensive

I take it that this means it could be expensive due to the resulting SMT encoding? I think my naive notion was indeed that we could track these generated TLA+ eliminators, and translate them into SMT ADTs. But that this encoding would serve to make the generated TLA+ specs coherent as such (perhaps even allowing them to be run in TLC)?

we could introduce the option type in the type system

Since the option type is equivalent to an either type with a unit for one of its disjuncts:

type 'a option = ('a, unit) either

I wonder if introducing an option type is any easier than introducing an either type? This is an important question, because, iiuc, if we can introduce an either type, then all other sum-types can be encoded in terms of the either, but this isn't the case with the option. In other words, afaict, introducing the option type is just a special case of introducing sum types generally, so I'm not clear on how introducing those will help us in this case?

You are probably right in that there is no other way but to pack all possible options of a tagged union in a tuple or record. We can try to avoid it by using ADTs in z3, but I don't know how well z3 works with ADTs.

What I had in mind was that we represent sum types via tuples or records in the TLA, but then we compile this to ADTs in the SMT translation. Tho I suppose you could leave the encoding in place. Note the caveat in my preamble:

... I am assuming (perhaps naively) that we could represent any sum-type
definition we can parse out of the source spec using smt2's declare-datatype

[konnov]

For the note, this idea is fully implemented now, see: https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html