diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index 3288dcd..d649233 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -2687,18 +2687,36 @@ fn unify_for_subst( vars: &BTreeSet<&str>, subst: &mut BTreeMap, ) -> Result<()> { - // Iter 14a fix: an arg-side `$u`-prefixed var is a synth-only - // wildcard produced by `synth_arg_type` for nullary ctors of a - // parameterised ADT (e.g. `Nil : List<$u>`). It carries no real - // constraint — accept without binding so a sibling arg can pin - // the type var instead. Without this, `Cons(Int, Nil)` synth - // would unify `a = Int` (from head) and then `a = $u` (from - // tail's recursive `List` slot) and falsely error. + // Iter 14a fix, extended in 15g-aux: a `$u`-prefixed var is a + // synth-only wildcard produced by `synth_arg_type` for nullary + // ctors of a parameterised ADT (e.g. `Nil : List<$u>`). It + // carries no real constraint — accept without binding so a + // sibling arg can pin the type var instead. Without this, + // `Cons(Int, Nil)` synth would unify `a = Int` (from head) and + // then `a = $u` (from tail's recursive `List` slot) and + // falsely error. + // + // 15g-aux: the early-return must accept `$u` on **either** side. + // `$u` enters in arg position from synth, but the prev-binding + // recursion below (`unify_for_subst(&prev, arg, ...)`) can swap + // a `$u` onto the param side when a previously-bound type is + // unified against a fresher arg whose roles differ. Reduced + // repro: `length [Left 1, Right 10]` — `a` first binds to + // `Either` from `Left 1`, then a recursive unification + // against `Either<$u, Int>` from `Right 10` lands `$u` in the + // param-pos[1] slot. Symmetric early-return is correct because + // `$u` is a synth-only wildcard regardless of which side carries + // it after the prev-binding swap. if let Type::Var { name } = arg { if name.starts_with("$u") { return Ok(()); } } + if let Type::Var { name } = param { + if name.starts_with("$u") { + return Ok(()); + } + } match (param, arg) { (Type::Var { name }, _) if vars.contains(name.as_str()) => { if let Some(prev) = subst.get(name).cloned() { diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 39ac7de..ba332c6 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -2991,3 +2991,54 @@ under `ailang-codegen/src/lib.rs`. acceptance — small, one-line in `unify_for_subst`); 16b (local recursive `let`); 16c (Lit-in-Ctor patterns); 17a (per-fn arena, gated on user discussion). + +--- + +## Iter 15g-aux — symmetric `$u` early-return in `unify_for_subst` + +**Goal.** Fix the codegen asymmetry that 15g surfaced: inline list +literals mixing `Left n` and `Right n` ctor calls of the same +`Either` errored at synth time even though both elements have +fully-determined concrete-after-pinning types. + +**Diagnosis.** `unify_for_subst` (`crates/ailang-codegen/src/lib.rs`) +had an arg-side-only early-return for `$u`-prefixed synth wildcards. +The function has a prev-binding recursion path that re-invokes +itself with the previously-bound type as the new param and the +fresh arg, which can swap a `$u` from arg position into param +position. Concretely, `length [Left 1, Right 10]` synths the list +elements as `Either` and `Either<$u, Int>`. The first +element pins `a = Either` for `Cons`'s parameter `a`. The +second element triggers a recursive unification of the previously- +bound `Either` against `Either<$u, Int>`, walking +pairwise: `Int` vs `$u` (arg-side `$u`, ok) and `$u` vs `Int` +(param-side `$u`, **falls through** to the catch-all error). + +**Fix.** Three lines in `unify_for_subst`: add a symmetric early- +return for param-side `$u`. Doc comment expanded to record the +asymmetry's origin and the symmetric extension's justification +(`$u` is a synth-only wildcard regardless of which side it ends +up on after the prev-binding swap). + +**Demo refactor.** `examples/std_either_list_demo.ailx` no longer +uses the `mkleft`/`mkright` monomorphic helpers introduced as the +15g workaround. The list is now constructed inline by mixing +`(term-ctor std_either.Either Left 1)` and `(term-ctor +std_either.Either Right 10)` directly. Same expected output +(2, 3, 2, 3); the demo doubles as the 15g-aux regression fixture. + +**Tests: 94/94, unchanged.** The fix expanded what compiles, did +not change observable behaviour for any prior fixture. + +**Cumulative state, post-15g-aux.** + +- Stdlib unchanged (5 modules, 27 combinators). +- One latent codegen bug retired. The bug count in the dogfood + audit since 14a stays at 4 surfaced + fixed (this is a fresh + surface from 15g, so 5 surfaced / 5 fixed). +- The std_either_list_demo workaround is gone, leaving the inline + cross-module mixed-ctor list as the canonical idiom. + +**Queue update.** 15g-aux done. Unchanged: 16b (local recursive +let), 16c (Lit-in-Ctor patterns), 17a (per-fn arena, gated on +user discussion of memory management). diff --git a/examples/std_either_list_demo.ail.json b/examples/std_either_list_demo.ail.json index 66cb28b..71dfcd5 100644 --- a/examples/std_either_list_demo.ail.json +++ b/examples/std_either_list_demo.ail.json @@ -1 +1 @@ -{"defs":[{"body":{"args":[{"name":"x","t":"var"}],"ctor":"Left","t":"ctor","type":"std_either.Either"},"doc":"Monomorphic Left-injector at Either. Pins both type vars at the call site so the codegen synth doesn't leave a `$u` wildcard on the second var.","kind":"fn","name":"mkleft","params":["x"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"args":[{"k":"con","name":"Int"},{"k":"con","name":"Int"}],"k":"con","name":"std_either.Either"}}},{"body":{"args":[{"name":"x","t":"var"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},"doc":"Monomorphic Right-injector at Either. Symmetric to mkleft.","kind":"fn","name":"mkright","params":["x"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"args":[{"k":"con","name":"Int"},{"k":"con","name":"Int"}],"k":"con","name":"std_either.Either"}}},{"body":{"lhs":{"args":[{"args":[{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"mkleft","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"fn":{"name":"mkleft","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":20},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":30},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"fn":{"name":"std_either_list.lefts","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"mkleft","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"fn":{"name":"mkleft","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":20},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":30},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"fn":{"name":"std_either_list.rights","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"mkleft","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"fn":{"name":"mkleft","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":20},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":30},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"fn":{"name":"std_either_list.partition_eithers","t":"var"},"t":"app"}],"fn":{"name":"std_pair.fst","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"args":[{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"mkleft","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"fn":{"name":"mkleft","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":20},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[{"args":[{"lit":{"kind":"int","value":30},"t":"lit"}],"fn":{"name":"mkright","t":"var"},"t":"app"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"fn":{"name":"std_either_list.partition_eithers","t":"var"},"t":"app"}],"fn":{"name":"std_pair.snd","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"t":"seq"},"doc":"Drive lefts, rights, and partition_eithers on the same five-element List> (Left 1, Right 10, Left 2, Right 20, Right 30). Expected output (one per line): 2, 3, 2, 3.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[{"module":"std_list"},{"module":"std_either"},{"module":"std_pair"},{"module":"std_either_list"}],"name":"std_either_list_demo","schema":"ailang/v0"} \ No newline at end of file +{"defs":[{"body":{"lhs":{"args":[{"args":[{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"ctor":"Left","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"ctor":"Left","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":20},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":30},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"fn":{"name":"std_either_list.lefts","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"ctor":"Left","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"ctor":"Left","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":20},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":30},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"fn":{"name":"std_either_list.rights","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"ctor":"Left","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"ctor":"Left","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":20},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":30},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"fn":{"name":"std_either_list.partition_eithers","t":"var"},"t":"app"}],"fn":{"name":"std_pair.fst","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"args":[{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"ctor":"Left","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"ctor":"Left","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":20},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[{"args":[{"lit":{"kind":"int","value":30},"t":"lit"}],"ctor":"Right","t":"ctor","type":"std_either.Either"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"fn":{"name":"std_either_list.partition_eithers","t":"var"},"t":"app"}],"fn":{"name":"std_pair.snd","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"t":"seq"},"doc":"Drive lefts, rights, and partition_eithers on the same five-element List> (Left 1, Right 10, Left 2, Right 20, Right 30). Expected output (one per line): 2, 3, 2, 3.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[{"module":"std_list"},{"module":"std_either"},{"module":"std_pair"},{"module":"std_either_list"}],"name":"std_either_list_demo","schema":"ailang/v0"} \ No newline at end of file diff --git a/examples/std_either_list_demo.ailx b/examples/std_either_list_demo.ailx index 75ab079..b0018f6 100644 --- a/examples/std_either_list_demo.ailx +++ b/examples/std_either_list_demo.ailx @@ -1,20 +1,16 @@ -; Iter 15g — fifth consumer demo. First demo to import four stdlib -; modules (std_list, std_either, std_pair, std_either_list); first to -; thread a List> through three combinators that +; Iter 15g (refactored in 15g-aux) — fifth consumer demo. Imports four +; stdlib modules (std_list, std_either, std_pair, std_either_list); +; threads a List> through three combinators that ; together exercise every monomorphisation site introduced by 15g. ; -; The list is constructed via the monomorphic helpers `mkleft` and -; `mkright` rather than bare `(term-ctor std_either.Either Left ...)` / -; `(term-ctor std_either.Either Right ...)`. This sidesteps a codegen -; bug that 15g surfaced: when an inline list literal mixes -; `Either Left n` (pins e, leaves a as `$u`) and `Either Right n` (pins -; a, leaves e as `$u`), the synth-time unification of the outer -; `List`'s parameter against the `$u`-bearing element types fails -; on the param side because `unify_for_subst` only accepts arg-side -; `$u` wildcards. The helpers fully pin both type vars at the call -; site, so each list element arrives with concrete `Either` -; and the bug is dodged. Logged as known-debt under 15g; the fix is -; a one-line symmetric extension of the `$u` early-return. +; The list is constructed inline by mixing `(term-ctor std_either.Either +; Left ...)` and `(... Right ...)`. Iter 15g surfaced a `unify_for_subst` +; asymmetry that would have rejected this construction at synth time; +; 15g-aux fixed it by accepting `$u` synth-wildcards on either side of +; the param/arg unification (see ailang-codegen/src/lib.rs's +; `unify_for_subst`). This demo is the regression fixture: if the +; symmetric early-return is reverted, the inline form below errors out +; before reaching codegen. (module std_either_list_demo @@ -23,24 +19,12 @@ (import std_pair) (import std_either_list) - (fn mkleft - (doc "Monomorphic Left-injector at Either. Pins both type vars at the call site so the codegen synth doesn't leave a `$u` wildcard on the second var.") - (type (fn-type (params (con Int)) (ret (con std_either.Either (con Int) (con Int))))) - (params x) - (body (term-ctor std_either.Either Left x))) - - (fn mkright - (doc "Monomorphic Right-injector at Either. Symmetric to mkleft.") - (type (fn-type (params (con Int)) (ret (con std_either.Either (con Int) (con Int))))) - (params x) - (body (term-ctor std_either.Either Right x))) - (fn main (doc "Drive lefts, rights, and partition_eithers on the same five-element List> (Left 1, Right 10, Left 2, Right 20, Right 30). Expected output (one per line): 2, 3, 2, 3.") (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body - (seq (do io/print_int (app std_list.length (app std_either_list.lefts (term-ctor std_list.List Cons (app mkleft 1) (term-ctor std_list.List Cons (app mkright 10) (term-ctor std_list.List Cons (app mkleft 2) (term-ctor std_list.List Cons (app mkright 20) (term-ctor std_list.List Cons (app mkright 30) (term-ctor std_list.List Nil))))))))) - (seq (do io/print_int (app std_list.length (app std_either_list.rights (term-ctor std_list.List Cons (app mkleft 1) (term-ctor std_list.List Cons (app mkright 10) (term-ctor std_list.List Cons (app mkleft 2) (term-ctor std_list.List Cons (app mkright 20) (term-ctor std_list.List Cons (app mkright 30) (term-ctor std_list.List Nil))))))))) - (seq (do io/print_int (app std_list.length (app std_pair.fst (app std_either_list.partition_eithers (term-ctor std_list.List Cons (app mkleft 1) (term-ctor std_list.List Cons (app mkright 10) (term-ctor std_list.List Cons (app mkleft 2) (term-ctor std_list.List Cons (app mkright 20) (term-ctor std_list.List Cons (app mkright 30) (term-ctor std_list.List Nil)))))))))) - (do io/print_int (app std_list.length (app std_pair.snd (app std_either_list.partition_eithers (term-ctor std_list.List Cons (app mkleft 1) (term-ctor std_list.List Cons (app mkright 10) (term-ctor std_list.List Cons (app mkleft 2) (term-ctor std_list.List Cons (app mkright 20) (term-ctor std_list.List Cons (app mkright 30) (term-ctor std_list.List Nil)))))))))))))))) + (seq (do io/print_int (app std_list.length (app std_either_list.lefts (term-ctor std_list.List Cons (term-ctor std_either.Either Left 1) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 10) (term-ctor std_list.List Cons (term-ctor std_either.Either Left 2) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 20) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 30) (term-ctor std_list.List Nil))))))))) + (seq (do io/print_int (app std_list.length (app std_either_list.rights (term-ctor std_list.List Cons (term-ctor std_either.Either Left 1) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 10) (term-ctor std_list.List Cons (term-ctor std_either.Either Left 2) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 20) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 30) (term-ctor std_list.List Nil))))))))) + (seq (do io/print_int (app std_list.length (app std_pair.fst (app std_either_list.partition_eithers (term-ctor std_list.List Cons (term-ctor std_either.Either Left 1) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 10) (term-ctor std_list.List Cons (term-ctor std_either.Either Left 2) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 20) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 30) (term-ctor std_list.List Nil)))))))))) + (do io/print_int (app std_list.length (app std_pair.snd (app std_either_list.partition_eithers (term-ctor std_list.List Cons (term-ctor std_either.Either Left 1) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 10) (term-ctor std_list.List Cons (term-ctor std_either.Either Left 2) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 20) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 30) (term-ctor std_list.List Nil))))))))))))))))