diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs index c6e9b5a..ddbcdb2 100644 --- a/crates/ail/tests/e2e.rs +++ b/crates/ail/tests/e2e.rs @@ -395,6 +395,28 @@ fn std_either_demo() { ); } +/// Iter 15g: `std_either_list` end-to-end. First stdlib fn set that +/// imports three other stdlib modules (`std_list`, `std_either`, +/// `std_pair`) and returns a compound polymorphic ADT tree +/// (`partition_eithers : List> -> Pair, List>`). +/// +/// Property protected: monomorphisation across `List × Either × Pair` +/// in a single call chain — `std_either_list.partition_eithers` is +/// instantiated at `(e=Int, a=Int)` and the result feeds +/// `std_pair.fst` / `std_pair.snd` (each at `(a=List, b=List)`) +/// into `std_list.length` (at `a=Int`). If cross-module ctor resolution +/// or substitution-through-nested-Con regressed, one of the +/// instantiations would either fail to emit or produce a wrong length. +/// The four expected outputs (2, 3, 2, 3) also pin the order +/// preservation of `lefts` and `rights` against the input +/// `[Left 1, Right 10, Left 2, Right 20, Right 30]`. +#[test] +fn std_either_list_demo() { + let stdout = build_and_run("std_either_list_demo.ail.json"); + let lines: Vec<&str> = stdout.lines().collect(); + assert_eq!(lines, vec!["2", "3", "2", "3"]); +} + /// Guards `ail diff`: a modified body changes the hash of `sum`, while /// `main` stays unchanged. Expects exit code 1, `changed` contains exactly /// `sum`, `unchanged` contains `main`, `added`/`removed` empty. diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 1fac678..39ac7de 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -2889,3 +2889,105 @@ section. Spot-checked each — all match current implementation. 17a (per-fn arena). 17a remains the explicit checkpoint before any broader memory-management work — that decision is gated on a joint conversation with the user. + +--- + +## Iter 15g — std_either_list: first 3-way cross-module stdlib fn + +**Goal.** Through 15f the stdlib had 4 modules but no fn imported +more than one foreign module (e.g. `std_list.head` returning +`std_maybe.Maybe`). 15g introduces the first stdlib module whose +every fn imports three others — `std_list`, `std_either`, +`std_pair` — and returns a compound polymorphic ADT tree +(`Pair, List>`). Designed to stress monomorphisation +across `List × Either × Pair`, cross-module ctor resolution at +qualified `term-ctor` sites, and the 16a desugar layer's nested- +Ctor pattern handling at depth 2. + +**What shipped.** + +- `examples/std_either_list.ailx` — three combinators, all + `forall (vars e a)`, all using qualified cross-module names at + `con` and `term-ctor` sites: + - `lefts : List> -> List` — depth-2 nested-Ctor + match per Cons arm (`Cons (Left l) t` / `Cons (Right _) t`) + plus a wildcard tail to anchor the desugar's fall-through + chain in `List` rather than the synthetic `Unit` fallback. + - `rights : List> -> List` — symmetric to + `lefts`. + - `partition_eithers : List> -> Pair, + List>` — `Nil → MkPair(Nil, Nil)`; `Cons h t →` let-bind + `rest = partition_eithers t`, then a flat match on `h` to + splice `l` / `r` onto `fst rest` / `snd rest`. Single pass. +- `examples/std_either_list_demo.ailx` — first demo importing four + stdlib modules. Drives all three combinators on the same five- + element list `[Left 1, Right 10, Left 2, Right 20, Right 30]`; + prints lengths via `std_list.length`. Output: `2 / 3 / 2 / 3`. +- `crates/ail/tests/e2e.rs::std_either_list_demo` (e2e count + 34 → 35). + +**16a desugar exercised.** Yes — `lefts` and `rights` use depth-2 +nested Ctor patterns (`(pat-ctor Cons (pat-ctor Left l) t)`). Each +expands into a chain of single-level matches via the 16a pass; the +explicit trailing wildcard arm prevents the synthetic `Unit` +fallback (the desugar's documented "valid programs never reach it" +terminator) from leaking into the function's return type. Without +the wildcard the checker reports `expected std_list.List, got +Unit` because the chain's `else`-arm body is `Lit Unit` — confirms +the design note in `desugar.rs::desugar_match` that exhaustiveness +is the caller's responsibility, not the desugar's. + +**New compiler bug surfaced.** Yes — and it is **not** in the new +combinators themselves but in the existing monomorphiser, surfaced +the moment one tries to construct an inline list literal mixing +`(term-ctor std_either.Either Left n)` and `(term-ctor +std_either.Either Right n)`. Reduced repro is just `(app +std_list.length (term-ctor std_list.List Cons (Left 1) (term-ctor +std_list.List Cons (Right 10) (term-ctor std_list.List Nil))))` — +no `lefts` / `rights` / `partition_eithers` involved. + +Cause: `synth_arg_type` produces `Either` for `Left 1` and +`Either<$u, Int>` for `Right 10`. The outer `Cons`'s parameter +type `List` unifies first against `List>` +(binds `a = Either`) and then against `List>` for the tail. `unify_for_subst` recurses into the prev +binding and ends up unifying param `$u` (from `Either`) +against arg `Int` — the existing `if name.starts_with("$u") { +return Ok(()); }` early-return only fires when `$u` is on the +**arg** side. Param-side `$u` falls through to the catch-all error +`cannot match param `$u` to arg `Int``. + +**Workaround in the demo.** Two monomorphic helpers `mkleft : Int +-> Either` and `mkright : Int -> Either` pin +both type vars at the call site, so each list element arrives with +fully concrete `Either` and the synth-time `$u` never +appears. Documented in the demo's header comment with a pointer +back to this entry. The combinators themselves (`lefts`, `rights`, +`partition_eithers`) are bug-free — the demo just couldn't build +the input list inline without dodging the `$u`-on-param-side path. + +**Bug fix sketch (queued, not landed).** A symmetric early-return +in `unify_for_subst` for param-side `$u` would close this — the +wildcard semantics ("don't care, defer") are direction-agnostic. +Filed as candidate iter 15g-aux. Single-line patch + a unit test +under `ailang-codegen/src/lib.rs`. + +**Tests: 94/94.** + +- e2e: 35 (was 34, +1 for `std_either_list_demo`). +- All other crates unchanged. + +**Cumulative state, post-15g.** + +- Stdlib: 5 modules (`std_maybe`, `std_list`, `std_either`, + `std_pair`, `std_either_list`); 27 combinators total (24 + 3). +- Deepest cross-module composition reached so far: `List × Either + × Pair` in a single fn (`partition_eithers`). +- Compiler bugs surfaced and fixed in dogfood since 14a: still 4 + fixed; 1 new (the `$u`-on-param-side case above), worked around + in the demo, queued as 15g-aux. + +**Queue update.** 15g done. Remaining: 15g-aux (param-side `$u` +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). diff --git a/examples/std_either_list.ail.json b/examples/std_either_list.ail.json new file mode 100644 index 0000000..f5d9c7f --- /dev/null +++ b/examples/std_either_list.ail.json @@ -0,0 +1 @@ +{"defs":[{"body":{"arms":[{"body":{"args":[{"name":"l","t":"var"},{"args":[{"name":"t","t":"var"}],"fn":{"name":"lefts","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"std_list.List"},"pat":{"ctor":"Cons","fields":[{"ctor":"Left","fields":[{"name":"l","p":"var"}],"p":"ctor"},{"name":"t","p":"var"}],"p":"ctor"}},{"body":{"args":[{"name":"t","t":"var"}],"fn":{"name":"lefts","t":"var"},"t":"app"},"pat":{"ctor":"Cons","fields":[{"ctor":"Right","fields":[{"p":"wild"}],"p":"ctor"},{"name":"t","p":"var"}],"p":"ctor"}},{"body":{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"},"pat":{"p":"wild"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Project the Left payloads of a list of Eithers into a List. Order-preserving. Uses the 16a nested-Ctor pattern to inline the inner Either dispatch within each Cons arm; the trailing wildcard arm seals the desugar's fall-through chain into a List rather than the synthetic Unit fallback.","kind":"fn","name":"lefts","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"args":[{"k":"var","name":"e"},{"k":"var","name":"a"}],"k":"con","name":"std_either.Either"}],"k":"con","name":"std_list.List"}],"ret":{"args":[{"k":"var","name":"e"}],"k":"con","name":"std_list.List"}},"k":"forall","vars":["e","a"]}},{"body":{"arms":[{"body":{"args":[{"name":"t","t":"var"}],"fn":{"name":"rights","t":"var"},"t":"app"},"pat":{"ctor":"Cons","fields":[{"ctor":"Left","fields":[{"p":"wild"}],"p":"ctor"},{"name":"t","p":"var"}],"p":"ctor"}},{"body":{"args":[{"name":"r","t":"var"},{"args":[{"name":"t","t":"var"}],"fn":{"name":"rights","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"std_list.List"},"pat":{"ctor":"Cons","fields":[{"ctor":"Right","fields":[{"name":"r","p":"var"}],"p":"ctor"},{"name":"t","p":"var"}],"p":"ctor"}},{"body":{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"},"pat":{"p":"wild"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Project the Right payloads of a list of Eithers into a List. Symmetric to lefts; same nested-Ctor + wildcard-tail pattern shape.","kind":"fn","name":"rights","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"args":[{"k":"var","name":"e"},{"k":"var","name":"a"}],"k":"con","name":"std_either.Either"}],"k":"con","name":"std_list.List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"std_list.List"}},"k":"forall","vars":["e","a"]}},{"body":{"arms":[{"body":{"args":[{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"body":{"arms":[{"body":{"args":[{"args":[{"name":"l","t":"var"},{"args":[{"name":"rest","t":"var"}],"fn":{"name":"std_pair.fst","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"std_list.List"},{"args":[{"name":"rest","t":"var"}],"fn":{"name":"std_pair.snd","t":"var"},"t":"app"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"},"pat":{"ctor":"Left","fields":[{"name":"l","p":"var"}],"p":"ctor"}},{"body":{"args":[{"args":[{"name":"rest","t":"var"}],"fn":{"name":"std_pair.fst","t":"var"},"t":"app"},{"args":[{"name":"r","t":"var"},{"args":[{"name":"rest","t":"var"}],"fn":{"name":"std_pair.snd","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"},"pat":{"ctor":"Right","fields":[{"name":"r","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"h","t":"var"},"t":"match"},"name":"rest","t":"let","value":{"args":[{"name":"t","t":"var"}],"fn":{"name":"partition_eithers","t":"var"},"t":"app"}},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Partition a list of Eithers into a Pair, List>: lefts on the left, rights on the right. Single pass via direct recursion; head dispatch is a flat match on the recursive result's projections.","kind":"fn","name":"partition_eithers","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"args":[{"k":"var","name":"e"},{"k":"var","name":"a"}],"k":"con","name":"std_either.Either"}],"k":"con","name":"std_list.List"}],"ret":{"args":[{"args":[{"k":"var","name":"e"}],"k":"con","name":"std_list.List"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"std_list.List"}],"k":"con","name":"std_pair.Pair"}},"k":"forall","vars":["e","a"]}}],"imports":[{"module":"std_list"},{"module":"std_either"},{"module":"std_pair"}],"name":"std_either_list","schema":"ailang/v0"} \ No newline at end of file diff --git a/examples/std_either_list.ailx b/examples/std_either_list.ailx new file mode 100644 index 0000000..d423860 --- /dev/null +++ b/examples/std_either_list.ailx @@ -0,0 +1,71 @@ +; Iter 15g — fifth stdlib module: first 3-way cross-module fn set. +; Imports std_list, std_either, std_pair simultaneously. All three +; combinators dispatch over List>; partition_eithers +; additionally returns Pair, List>. Stresses +; monomorphisation across List × Either × Pair, cross-module ctor +; resolution at qualified term-ctor sites, and the 16a desugar +; layer at depth-2 nested Ctor patterns (in `lefts` / `rights`). + +(module std_either_list + + (import std_list) + (import std_either) + (import std_pair) + + (fn lefts + (doc "Project the Left payloads of a list of Eithers into a List. Order-preserving. Uses the 16a nested-Ctor pattern to inline the inner Either dispatch within each Cons arm; the trailing wildcard arm seals the desugar's fall-through chain into a List rather than the synthetic Unit fallback.") + (type + (forall (vars e a) + (fn-type + (params (con std_list.List (con std_either.Either e a))) + (ret (con std_list.List e))))) + (params xs) + (body + (match xs + (case (pat-ctor Cons (pat-ctor Left l) t) + (term-ctor std_list.List Cons l (app lefts t))) + (case (pat-ctor Cons (pat-ctor Right _) t) + (app lefts t)) + (case _ (term-ctor std_list.List Nil))))) + + (fn rights + (doc "Project the Right payloads of a list of Eithers into a List. Symmetric to lefts; same nested-Ctor + wildcard-tail pattern shape.") + (type + (forall (vars e a) + (fn-type + (params (con std_list.List (con std_either.Either e a))) + (ret (con std_list.List a))))) + (params xs) + (body + (match xs + (case (pat-ctor Cons (pat-ctor Left _) t) + (app rights t)) + (case (pat-ctor Cons (pat-ctor Right r) t) + (term-ctor std_list.List Cons r (app rights t))) + (case _ (term-ctor std_list.List Nil))))) + + (fn partition_eithers + (doc "Partition a list of Eithers into a Pair, List>: lefts on the left, rights on the right. Single pass via direct recursion; head dispatch is a flat match on the recursive result's projections.") + (type + (forall (vars e a) + (fn-type + (params (con std_list.List (con std_either.Either e a))) + (ret (con std_pair.Pair (con std_list.List e) (con std_list.List a)))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) + (term-ctor std_pair.Pair MkPair + (term-ctor std_list.List Nil) + (term-ctor std_list.List Nil))) + (case (pat-ctor Cons h t) + (let rest (app partition_eithers t) + (match h + (case (pat-ctor Left l) + (term-ctor std_pair.Pair MkPair + (term-ctor std_list.List Cons l (app std_pair.fst rest)) + (app std_pair.snd rest))) + (case (pat-ctor Right r) + (term-ctor std_pair.Pair MkPair + (app std_pair.fst rest) + (term-ctor std_list.List Cons r (app std_pair.snd rest))))))))))) diff --git a/examples/std_either_list_demo.ail.json b/examples/std_either_list_demo.ail.json new file mode 100644 index 0000000..66cb28b --- /dev/null +++ b/examples/std_either_list_demo.ail.json @@ -0,0 +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 diff --git a/examples/std_either_list_demo.ailx b/examples/std_either_list_demo.ailx new file mode 100644 index 0000000..75ab079 --- /dev/null +++ b/examples/std_either_list_demo.ailx @@ -0,0 +1,46 @@ +; 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 +; 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. + +(module std_either_list_demo + + (import std_list) + (import std_either) + (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))))))))))))))))