Enums

[KyrylR]

This PR is re implementation of #336 with the emphasis on nominative enums

[KyrylR]

I do not have a complete understanding of Simplicity's type algebra, so I did a few iterations with Fable 5 to understand how it works

Here is the summary:

Simplicity's type algebra has exactly three constructors: the unit type 1, products A × B, and binary sums A + B. There is no n-ary sum. A SimplicityHL enum with n variants means "exactly one of these n payloads" — so before anything can be compiled, the compiler must express that as some nesting of two-way Eithers. balanced_sum is where that nesting is chosen: it folds the n variant payload types into one canonical tree of Eithers.

The choice being canonical matters more than what the choice is. Four independent pieces of the compiler navigate this tree, and they only interoperate because all four recurse with the same split:

• balanced_sum (types.rs) — builds the structural type;
• inject_variant (compile) — construction wraps a payload in injl/injr down the path to its leaf;
• case_tree + EnumMatch::compile — a match becomes nested case combinators of the same shape;
• enum_injection / as_enum_leaf (value.rs) — witness values are encoded to, and decoded from, the same paths.

If any one of them split differently, a constructed Action::Cold would land on a leaf that the match's case tree interprets as a different variant. And because the leaf-position of a variant is its wire encoding, the shape is also part of the ABI — which is why the ABI ships variants strictly in declaration order.

Theoretical foundation

Finite coproducts from binary ones. In type-theoretic terms an enum is a sum type; categorically, a coproduct A₁ + A₂ + … + Aₙ. A category with binary coproducts automatically has all finite nonempty coproducts, by iteration — and associativity holds up to canonical isomorphism: (A+B)+C ≅ A+(B+C). So semantically, any bracketing represents the enum equally well; all bracketings are isomorphic. The compiler's job is merely to fix one associate and use it everywhere. balanced_sum is exactly the constructive content of that "finite coproducts exist" theorem: a fold of the binary coproduct over the leaf list.

Why nonempty (the panic). The empty coproduct is the initial object 0 — the uninhabited type. Simplicity's algebra is {1, ×, +} with no 0: an uninhabited type is inexpressible (every Simplicity type is inhabited). Hence the expect("at least one leaf") here, and the matching non-empty invariant on EnumInfo::new. A one-leaf "sum" degenerates to the payload itself — a single-variant enum is just a nominal wrapper.

Injections and case analysis. A coproduct comes with injections injᵢ : Aᵢ → ΣA and the universal property that any family of maps fᵢ : Aᵢ → C factors through a unique copairing [f₁,…,fₙ]. Simplicity gives you exactly the binary versions: injl/injr are the two injections, and case f g is the binary copairing. Under the balanced encoding, the n-ary injection injᵢ becomes the composite of injl/injr steps along the path to leaf i (that's inject_variant), and the n-ary copairing becomes the tree of case nodes folded over the match arms (that's case_tree). The enum feature adds no new primitive — it's pure derived structure over Simplicity's existing algebra, which is also why an undeclared variant is unrepresentable: there is no fifth path through a four-leaf tree.

The discriminant is the path. A Simplicity sum value is encoded as a tag bit choosing left/right, then the payload. So a variant's encoding starts with the sequence of tag bits spelling its root-to-leaf path — the path is the discriminant; no separate tag field exists. This is where "why balanced, not a right-nested comb A + (B + (C + …))" gets its answer:

• Comb: variant k sits at depth k+1 (except the last), so its tag costs ~k bits and matching it traverses k nested case nodes — a unary discriminant. A 256-variant enum's last variant pays 255 tag bits and 255 case nodes.
• Balanced: every leaf sits at depth ⌊log₂ n⌋ or ⌈log₂ n⌉, so every variant's tag is ~log₂ n bits and every match dispatch traverses ~log₂ n cases — effectively a fixed-width binary discriminant, the same thing a hand-rolled tag field would give you, but derived instead of stored. (Information-theoretically: with no reason to favor any variant, equal-weight leaves make the complete binary tree the optimal prefix code — Huffman with uniform weights.)

The exact shape. BTreeSlice splits n leaves at btree_split_index(n) = n − 2^(⌈log₂ n⌉−1): the right subtree always gets the largest power of two ≤ n−1 leaves… concretely, the right child is a perfect tree and the left child absorbs the remainder, recursively. For n = 3 that's 1 + (1+1) — matching the enum_structural_type_is_balanced_sum test's expected Either<1, Either<1,1>>. Crucially, this is the same fold the codebase already uses for products (tuples and arrays are balanced products of the same BTreeSlice shape), so sums and products are duals built by one shape rule — one invariant to keep in sync instead of two.

One last practical point hidden in the doc comment: when a value is constructed, only the leaf actually inhabited carries data — the types of all sibling subtrees along the path aren't determined by the injection itself. They get pinned by Simplicity's type inference when the value meets its consumer (the match's case tree or the declared witness type), which is why inject_variant can build the path without ever spelling out the full enum type.