Apply a function slot's domain rule once its kind is resolved, not at each merge - #116
Open
dpmills wants to merge 1 commit into
Open
Apply a function slot's domain rule once its kind is resolved, not at each merge#116dpmills wants to merge 1 commit into
dpmills wants to merge 1 commit into
Conversation
Contributor
Author
|
This change is part of the following stack:
Change managed by git-spice. |
This was referenced Aug 20, 2026
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 20, 2026 20:51
3e99740 to
deda9e9
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 20, 2026 23:24
deda9e9 to
2179abc
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 21, 2026 04:29
2179abc to
500161c
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 21, 2026 04:39
500161c to
873242e
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 21, 2026 04:55
873242e to
b1ae9a5
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 21, 2026 05:47
b1ae9a5 to
adeb0f5
Compare
This was referenced Aug 21, 2026
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
2 times, most recently
from
August 21, 2026 19:42
ab5d9d4 to
f04d474
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 21, 2026 20:45
f04d474 to
5a72e3f
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 21, 2026 22:23
5a72e3f to
b716cf5
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 22, 2026 00:08
b716cf5 to
55f3df8
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
2 times, most recently
from
August 22, 2026 00:35
076ac6c to
f34cf64
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 22, 2026 00:46
f34cf64 to
54cbd24
Compare
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 22, 2026 01:06
54cbd24 to
e3b0c9c
Compare
… each merge
`CompactFun::merge` chose how to combine two domains from the slot's `KindMerge` — union the alternatives for `Data`, take the contravariant meet otherwise — but a slot's kind is not settled until the last bound has merged, so the choice came from an answer that did not exist yet and a later bound could not undo it. Association therefore decided the outcome: an undetermined pair took the meet, `{a} ⊓ {b}` is `{a, b}`, and that deduplicated against a `Data` bound's own `{a, b}`, so a join of three collections over `{a, b}`, `{a}` and `{b}` typed as one collection over `{a, b}` in one association and was rejected in the other. The accepting association is the wrong answer: the kinds join to `Data`, all three domains *are* the data, and `union_domains` states the rule the meet broke — narrowing a data domain drops rows.
A positive join now accumulates the alternatives whatever the kind, and `coalesce_compact_go` applies the resolved kind's rule once: it meets the alternatives for a `Compute` reading and for a kind variable nothing pinned, and requires a single survivor for `Data`. The kind itself joins in the flat semilattice `Unknown < {Data, Compute} < Conflict`, which is the same operation at both polarities, so `merge`'s four kind branches collapse to one. A negative merge still meets its domains directly — that rule never read the kind.
`undetermined_kinds_join_without_deciding_the_domain_rule` pins the exhibit in every association, and `two_undetermined_kinds_join_to_a_capability_over_the_met_domain` pins the join that must keep working: two undetermined-kind bounds over `{a}` and `{b}` are a capability over `{a, b}`, which a rule that merely rejected an undetermined join would have refused. Instrumenting the arm showed no compiled program in the suite reaches a positive undetermined join, and no inferred type changes: the suite passes forward, under `DEEP_TYPECHECK=1`, and under `CAMBRA_REFINEMENT_ORDER=reverse`.
dpmills
force-pushed
the
dmills/domain-rule-at-coalesce
branch
from
August 22, 2026 03:43
e3b0c9c to
d3f11af
Compare
dpmills
marked this pull request as ready for review
August 22, 2026 03:50
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
CompactFun::mergechose how to combine two domains from the slot'sKindMerge— union the alternatives forData, take the contravariant meet otherwise — but a slot's kind is not settled until the last bound has merged, so the choice came from an answer that did not exist yet and a later bound could not undo it. Association therefore decided the outcome: an undetermined pair took the meet,{a} ⊓ {b}is{a, b}, and that deduplicated against aDatabound's own{a, b}, so a join of three collections over{a, b},{a}and{b}typed as one collection over{a, b}in one association and was rejected in the other. The accepting association is the wrong answer: the kinds join toData, all three domains are the data, andunion_domainsstates the rule the meet broke — narrowing a data domain drops rows.A positive join now accumulates the alternatives whatever the kind, and
coalesce_compact_goapplies the resolved kind's rule once: it meets the alternatives for aComputereading and for a kind variable nothing pinned, and requires a single survivor forData. The kind itself joins in the flat semilatticeUnknown < {Data, Compute} < Conflict, which is the same operation at both polarities, somerge's four kind branches collapse to one. A negative merge still meets its domains directly — that rule never read the kind.undetermined_kinds_join_without_deciding_the_domain_rulepins the exhibit in every association, andtwo_undetermined_kinds_join_to_a_capability_over_the_met_domainpins the join that must keep working: two undetermined-kind bounds over{a}and{b}are a capability over{a, b}, which a rule that merely rejected an undetermined join would have refused. Instrumenting the arm showed no compiled program in the suite reaches a positive undetermined join, and no inferred type changes: the suite passes forward, underDEEP_TYPECHECK=1, and underCAMBRA_REFINEMENT_ORDER=reverse.