Iter 15g-aux — symmetric $u early-return in unify_for_subst
Fix the codegen asymmetry that 15g surfaced. unify_for_subst had an arg-side-only early-return for $u-prefixed synth wildcards. The function's prev-binding recursion can swap a $u from arg into param position when re-unifying a previously-bound type against a fresh arg. Reduced repro: `length [Left 1, Right 10]` — `a` first binds to `Either<Int, $u>`, then the recursive unification against `Either<$u, Int>` lands $u in param-pos[1] and falls through to the catch-all error. Fix is three lines: add a symmetric $u early-return for param side. $u is a synth-only wildcard regardless of which side it ends up on after the prev-binding swap. Doc comment expanded to record the origin and justification. std_either_list_demo refactored: mkleft/mkright workaround helpers removed; the list is now constructed inline by mixing (term-ctor std_either.Either Left 1) and (... 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 without changing observable behaviour for any prior fixture.
This commit is contained in:
@@ -2687,18 +2687,36 @@ fn unify_for_subst(
|
||||
vars: &BTreeSet<&str>,
|
||||
subst: &mut BTreeMap<String, Type>,
|
||||
) -> 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<a>` 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<a>` 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<Int, $u>` 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() {
|
||||
|
||||
@@ -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<e, a>` 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<Int, $u>` and `Either<$u, Int>`. The first
|
||||
element pins `a = Either<Int, $u>` for `Cons`'s parameter `a`. The
|
||||
second element triggers a recursive unification of the previously-
|
||||
bound `Either<Int, $u>` 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).
|
||||
|
||||
File diff suppressed because one or more lines are too long
@@ -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<Either<Int, Int>> 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<Either<Int, Int>> 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<a>`'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<Int, Int>`
|
||||
; 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<Int, Int>. 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<Int, Int>. 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<Either<Int, Int>> (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))))))))))))))))
|
||||
|
||||
Reference in New Issue
Block a user