v0.19 fix optimizer handling of disjoint types #1500

vyzo · 2026-09-16T10:45:58Z

vyzo commented

2026-09-16 10:45:58 +00:00

the optimizer incorrectly assumed incompatible types for mixins.

diagnosed and fixed by astra

the optimizer incorrectly assumed incompatible types for mixins. diagnosed and fixed by astra

vyzo added 2 commits

2026-09-16 10:45:58 +00:00

fix compiler disjointness reasoning for overlapping mixins a284cd77e2

Require proven disjointness for predicate folding and checked-call rejection. Correct positive match assertions and classify real? as an arbitrary-value predicate. Add cross-module optimized regressions for overlapping types and preserved negative folding.

bootstrap f1fa7c26ff

vyzo requested review from fare

2026-09-16 10:46:05 +00:00

fare commented

2026-09-16 16:54:50 +00:00

Sol says:

I reviewed the functional commit in detail. I don’t see a semantic correctness blocker in the fix itself. The new rule—failure to prove subtyping is not proof of disjointness—is exactly the right correction for Gerbil’s open multiple-inheritance/mixin world. The implementation is pleasingly conservative. (cons.io git)

My review comments would be:

Rebase onto current v0.19-staging and regenerate the bootstrap before merging. The actual source fix is only 7 files, +210/−11, but the PR as a whole is 81 files, +51,338/−48,396 because of the bootstrap commit, and Forgejo currently says the branch is out of date with its base. With generated bootstrap material, I wouldn't merge an out-of-date snapshot even though Git says it merges automatically; rebase first and regenerate so the checked-in bootstrap corresponds exactly to the sources that actually land. (cons.io git)
Non-blocking: I'd add one test for the !procedure? arm of !type-disjoint?. That's the one new proof path that doesn't appear to get exercised directly. The function now explicitly maps compiler procedure types to procedure::t before continuing the proof, whereas the direct tests cover primitive leaves, subtype overlap, multiple-inheritance overlap and nullable types. (cons.io git) A test along the lines of a known procedure against some known-disjoint final/primitive type would pin that behavior down. I don't see anything wrong with the code; it's just an otherwise conspicuous coverage hole.

The important parts look right:

The new !type-disjoint? is deliberately a sufficient proof, not an attempt to decide type intersection. Unknown types, abort types and nullable types conservatively return false; subtype relationships return false; then it only proves disjointness from a final class, a known primitive leaf or incompatible struct tails. That's exactly the polarity you want here: false negatives merely miss an optimization, whereas a false positive miscompiles the program. (cons.io git)

The final-class case is sound: once neither side is a subtype of the other, if either side cannot be subclassed there can be no future class inhabiting their intersection. Likewise, the struct-tail argument makes sense under Gerbil's C4 constraint: two unrelated concrete struct tails cannot later acquire a common subtype merely by adding mixins. The tests specifically exercise final disjointness, unrelated struct bases and mixins carrying incompatible struct bases. (cons.io git)

The change in incompatible-type? / check-expression-type! is particularly important. The old code effectively turned “not known compatible” into “incompatible”; the new code rejects or folds only when !type-disjoint? can actually prove it. Otherwise it retains checked dispatch. That's the correct treatment of an open-world type hierarchy. (cons.io git)

The match optimizer fix also looks correct. A positive assertion that xt holds lets predicate t fold true when xt <: t, not the other way around; otherwise it folds false only on proven disjointness. The explicit separation of ordinary pair/vector/etc. shapes from syntax shapes also avoids accidentally deriving disjointness across representations that may overlap. (cons.io git)

And changing real? from a primitive procedure with a number::t input signature into an arbitrary-value primitive predicate for real::t is correct. (real? 'foo) is a perfectly legitimate predicate call yielding #f; it isn't a signature error. The new regression tests cover #f, a symbol and a real value, including the nullable optional-argument case. (cons.io git)

I especially like the cross-module test design: the provider is compiled before Both/ClassBoth introduces the common subtype of Mixin and Base. That reproduces precisely why absence of a currently known common subclass cannot establish disjointness. It also checks both predicate orders, match predicates, typed calls and contracts, while separately verifying that genuinely proven negative cases still optimize away and that side effects aren't accidentally dropped. (cons.io git)

So my disposition would be: approve the source change; ask Vyzo to rebase and regenerate the bootstrap first. I would not request substantive changes to the disjointness algorithm. The procedure test is a nice-to-have rather than grounds for holding it up.

PR #1500

Sol says: I reviewed the functional commit in detail. I **don’t see a semantic correctness blocker** in the fix itself. The new rule—*failure to prove subtyping is not proof of disjointness*—is exactly the right correction for Gerbil’s open multiple-inheritance/mixin world. The implementation is pleasingly conservative. ([cons.io git][1]) My review comments would be: 1. **Rebase onto current `v0.19-staging` and regenerate the bootstrap before merging.** The actual source fix is only **7 files, +210/−11**, but the PR as a whole is **81 files, +51,338/−48,396** because of the bootstrap commit, and Forgejo currently says the branch is out of date with its base. With generated bootstrap material, I wouldn't merge an out-of-date snapshot even though Git says it merges automatically; rebase first and regenerate so the checked-in bootstrap corresponds exactly to the sources that actually land. ([cons.io git][1]) 2. **Non-blocking: I'd add one test for the `!procedure?` arm of `!type-disjoint?`.** That's the one new proof path that doesn't appear to get exercised directly. The function now explicitly maps compiler procedure types to `procedure::t` before continuing the proof, whereas the direct tests cover primitive leaves, subtype overlap, multiple-inheritance overlap and nullable types. ([cons.io git][1]) A test along the lines of a known procedure against some known-disjoint final/primitive type would pin that behavior down. I don't see anything wrong with the code; it's just an otherwise conspicuous coverage hole. The important parts look right: The new `!type-disjoint?` is deliberately a **sufficient proof**, not an attempt to decide type intersection. Unknown types, abort types and nullable types conservatively return false; subtype relationships return false; then it only proves disjointness from a final class, a known primitive leaf or incompatible struct tails. That's exactly the polarity you want here: false negatives merely miss an optimization, whereas a false positive miscompiles the program. ([cons.io git][1]) The final-class case is sound: once neither side is a subtype of the other, if either side cannot be subclassed there can be no future class inhabiting their intersection. Likewise, the struct-tail argument makes sense under Gerbil's C4 constraint: two unrelated concrete struct tails cannot later acquire a common subtype merely by adding mixins. The tests specifically exercise final disjointness, unrelated struct bases and mixins carrying incompatible struct bases. ([cons.io git][1]) The change in `incompatible-type?` / `check-expression-type!` is particularly important. The old code effectively turned “not known compatible” into “incompatible”; the new code rejects or folds only when `!type-disjoint?` can actually prove it. Otherwise it retains checked dispatch. That's the correct treatment of an open-world type hierarchy. ([cons.io git][1]) The match optimizer fix also looks correct. A positive assertion that `xt` holds lets predicate `t` fold true when **`xt <: t`**, not the other way around; otherwise it folds false only on proven disjointness. The explicit separation of ordinary pair/vector/etc. shapes from syntax shapes also avoids accidentally deriving disjointness across representations that may overlap. ([cons.io git][1]) And changing `real?` from a primitive procedure with a `number::t` input signature into an arbitrary-value primitive predicate for `real::t` is correct. `(real? 'foo)` is a perfectly legitimate predicate call yielding `#f`; it isn't a signature error. The new regression tests cover `#f`, a symbol and a real value, including the nullable optional-argument case. ([cons.io git][1]) I especially like the cross-module test design: the provider is compiled **before** `Both`/`ClassBoth` introduces the common subtype of `Mixin` and `Base`. That reproduces precisely why absence of a currently known common subclass cannot establish disjointness. It also checks both predicate orders, match predicates, typed calls and contracts, while separately verifying that genuinely proven negative cases still optimize away and that side effects aren't accidentally dropped. ([cons.io git][1]) So my disposition would be: **approve the source change; ask Vyzo to rebase and regenerate the bootstrap first.** I would not request substantive changes to the disjointness algorithm. The procedure test is a nice-to-have rather than grounds for holding it up. [PR #1500](https://git.cons.io/mighty-gerbils/gerbil/pulls/1500?utm_source=chatgpt.com) [1]: https://git.cons.io/mighty-gerbils/gerbil/pulls/1500/commits/a284cd77e2a9ffbd3fc0febb093eeccdbbf05cce "#1500 - v0.19 fix optimizer handling of disjoint types - mighty-gerbils/gerbil - cons.io git"

vyzo commented

2026-09-16 17:12:36 +00:00

I don't think we need to regenerate bootstrap, there are no changes in the core since it was generated this morning.