git.iko.soy/jibb
on master help sign in
Pass projected pairs to the overlap witness and state its order

+mold-overlap-witness now takes the union's projected pairs instead of computing them, so the partial report projects each union once. The full check still projects once more on a failed union mold, because a failed inference does not return the projection it made. Behaviour is unchanged from the previous commit. That commit did change one result, recorded here: when the source witness proves an earlier pair and the projection a later one, the full check's evidence now names the later, projected pair, as the partial report already did. For "+$ bad" with cases (tagged @t), [%wrapped @p], @t and @ud it names lines 5 and 6 instead of 3 and 4. The new order fixture in the basic full-overlap test pins that order for both paths, and that the source witness alone still finds the earlier pair. docs/compiler.md said the full check projects only unions whose inference failed; it projects every union whose cases it infers, and once more on failure. It also said both paths always name the same pair; they do for the same union, but the full check attaches evidence only when that union is the first mold to fail, so an earlier failing mold, such as one that refers to it, keeps the generic error. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U4FzmSdubYxmZGDp2VJRAQ

commit2b9666cb8a2f1624a573c228221378b05d612a62 authorClaude <noreply@anthropic.com> dateMon 2 Nov 2026, 17:32 (5 hours ago) parent447a592
8 files changed+71−24
compare with master
unifiedsplit
docs/compiler.md+1−1 jibb-dev/lib/jibb.hoon+12−9 tests/lib/jibb-full-overlap-basic.hoon+44−10 tests/type-full-overlap/about.txt+1−1 tests/type-full-overlap/expected-basic.txt+3 tests/type-full-overlap/order.txt+7 tools/testdata/ship-selftest+2−2 tools/type-full-overlap-test+1−1
docs/compiler.md+1−1
@@ -66,7 +66,7 @@ Before the empty-capital optimization below, single sequential eval runs includi
6666
6767Restricted-number promotion only applies to written capital variables. If none are present, it returns immediately instead of traversing the environment. In one startup-inclusive pair of runs on 2,000 independent gates, output was byte-identical and user CPU fell from 71.67 to 38.26 seconds; wall time was 72.80 versus 51.66 seconds while other checks were running. This does not establish a bound for dependent modules or a complete-checker benchmark.
6868
69−A bounded source proof can also establish distinct literal heads when a union case is a one-hop application of a uniquely resolved local generic mold. It compares literal runtime nouns and checks the original mold normally before publishing an interface. The same source proof improves the partial report, which still says the mold is not checked. The new proof declines nested or qualified applications, opaque references, recursive-index states, holes and deferred obligations; other valid unions can remain unsupported. A 256-node source budget and a separate 256-entry inherited-state budget apply per attempt. They do not bound the existing pairwise union pass, parsing, atom or name sizes, or downstream checking. Prepared interfaces and inference state remain trusted inputs. `tools/type-union-source-test` and the shared ship guard exercise source resolution, reporting, rollback and these bounds. A separate positive witness can identify overlap in two-field, literal-headed cases when a unique one-hop local, one-parameter generic alias is applied to a concrete primitive payload. It compares the literal noun values and proves the payloads have a shared noun, so an empty or unknown payload is not a witness. The partial report identifies both original case sites. The partial report and the full module check find overlaps with one helper, `mold-overlap-witness`: it takes the first overlapping pair from the pairwise projection, which covers atoms, `?` and literal constants, and nested literal-headed cells, and tries this source witness only when some pair stays unknown. Both paths therefore name the same pair. `infer-jibb-file-detailed` returns structured overlap evidence for the first failed mold, including the originating path, exact source, mold name and both case spans. Ordinary Jibb imports preserve a child’s evidence through source and cache checks; the legacy `infer-jibb-file` API remains a text-result adapter and renders both excerpts. Specialized API and prepared-prelude paths retain their existing generic or text-only error boundaries. This witness uses a shared 256-node source/pair budget per attempt; generic-wrapper parameter validation has a separate 256-entry cap. An unsupported earlier case may hide a later overlap. The pairwise projection has no budget; the full check runs it only on a union mold whose inference failed. Parsing, atom and name sizes, source-excerpt rendering, and downstream checking also remain outside these budgets. `tools/type-union-alias-overlap-test` checks the source proof and partial report; `tools/type-full-overlap-test` checks the detailed and legacy full-module paths, source attribution and cache behavior.
69+A bounded source proof can also establish distinct literal heads when a union case is a one-hop application of a uniquely resolved local generic mold. It compares literal runtime nouns and checks the original mold normally before publishing an interface. The same source proof improves the partial report, which still says the mold is not checked. The new proof declines nested or qualified applications, opaque references, recursive-index states, holes and deferred obligations; other valid unions can remain unsupported. A 256-node source budget and a separate 256-entry inherited-state budget apply per attempt. They do not bound the existing pairwise union pass, parsing, atom or name sizes, or downstream checking. Prepared interfaces and inference state remain trusted inputs. `tools/type-union-source-test` and the shared ship guard exercise source resolution, reporting, rollback and these bounds. A separate positive witness can identify overlap in two-field, literal-headed cases when a unique one-hop local, one-parameter generic alias is applied to a concrete primitive payload. It compares the literal noun values and proves the payloads have a shared noun, so an empty or unknown payload is not a witness. The partial report identifies both original case sites. The partial report and the full module check find overlaps with one helper, `mold-overlap-witness`: it takes the first overlapping pair from the pairwise projection, which covers atoms, `?` and literal constants, and nested literal-headed cells, and tries this source witness only when no pair overlaps and some pair stays unknown. A projected overlap is therefore named even when the source witness would prove an earlier pair. For the same union both paths name the same pair, but the full check attaches evidence only when that union is the first mold whose inference fails and its generic parameters are valid; an earlier failing mold, including one that refers to the union, and a union with duplicate or too many parameters keep the generic error. `infer-jibb-file-detailed` returns structured overlap evidence for the first failed mold, including the originating path, exact source, mold name and both case spans. Ordinary Jibb imports preserve a child’s evidence through source and cache checks; the legacy `infer-jibb-file` API remains a text-result adapter and renders both excerpts. Specialized API and prepared-prelude paths retain their existing generic or text-only error boundaries. This witness uses a shared 256-node source/pair budget per attempt; generic-wrapper parameter validation has a separate 256-entry cap. An unsupported earlier case may hide a later overlap. The pairwise projection has no budget: the full check runs it before inferring a union's cases, and once more, to find the pair, on a failed union mold whose generic parameters are valid. Parsing, atom and name sizes, source-excerpt rendering, and downstream checking also remain outside these budgets. `tools/type-union-alias-overlap-test` checks the source proof and partial report; `tools/type-full-overlap-test` checks the detailed and legacy full-module paths, source attribution and cache behavior.
7070
7171A single-arm cell pattern can bind two or more positions, with its last binder capturing the remaining tail. Duplicate and shadowed names are rejected. A definite non-cell spine fails; an intermediate union or collection that might contain a cell remains unsupported. For a known non-union cell, a separate one-arm rule also accepts structured patterns, including nested literal and wildcard positions, when the existing coverage proof establishes the whole pattern. It binds payloads with their original types and checks result context; unknown, partially covered, union or recursive spines stay unsupported.
7272
jibb-dev/lib/jibb.hoon+12−9
@@ -11068,14 +11068,16 @@
1106811068 (weld pairs $(cases t.cases))
1106911069::
1107011070:: The partial report and the full module check share one overlap proof,
11071−:: so both name the same pair. The projection proves atoms, flags and
11072−:: nested literal cells; the source slice is tried only when some pair
11073−:: is unknown, for its one-hop generic applications. A missing witness
11074−:: does not mean the cases are disjoint.
11071+:: so for the same union both name the same pair. The caller passes the
11072+:: projected .pairs, which the partial report reads again. The projection
11073+:: proves atoms, flags and nested literal cells, and its first overlap is
11074+:: named even when the source slice would prove an earlier pair. The
11075+:: source slice is tried only when some pair is unknown, for its one-hop
11076+:: generic applications. A missing witness does not mean the cases are
11077+:: disjoint.
1107511078++ mold-overlap-witness
11076− |= [cases=(list shape) molds=imolds]
11079+ |= [cases=(list shape) pairs=(list upair) molds=imolds]
1107711080 ^- (unit upair)
11078− =/ pairs=(list upair) (union-pairs cases molds)
1107911081 =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))
1108011082 ?^ overlapping `i.overlapping
1108111083 ?. (lien pairs |=(p=upair =(%unknown relation.p))) ~
@@ -11219,14 +11221,14 @@
1121911221 (of-wain:format ~[(crip "+$ {(trip name.d)}: type hole needs a determined type") text])
1122011222 =? sh ?=(%generic -.sh) body.sh
1122111223 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
11222− =/ witness=(unit upair) (mold-overlap-witness cases.sh molds)
11224+ =/ pairs=(list upair) (union-pairs cases.sh molds)
11225+ =/ witness=(unit upair) (mold-overlap-witness cases.sh pairs molds)
1122311226 ?^ witness
1122411227 =/ p=upair u.witness
1122511228 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")
1122611229 =/ first=@t (show-error src [file line.beg.first.p col.beg.first.p "first union case"])
1122711230 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])
1122811231 (of-wain:format ~[summary first second])
11229− =/ pairs=(list upair) (union-pairs cases.sh molds)
1123011232 ?: (lien pairs |=(p=upair =(%unknown relation.p)))
1123111233 ?. (union-source-distinct-tags cases.sh molds 256)
1123211234 (crip "+$ {(trip name.d)}: case disjointness unresolved; mold not checked")
@@ -11573,7 +11575,8 @@
1157311575 ?. valid ~
1157411576 =? sh ?=(%generic -.sh) body.sh
1157511577 ?. ?=(%union -.sh) ~
11576− (mold-overlap-witness cases.sh molds)
11578+ :: A failed inference keeps no projection, so it is computed once more.
11579+ (mold-overlap-witness cases.sh (union-pairs cases.sh molds) molds)
1157711580++ module-mold-types-detail
1157811581 |= [molds=imolds state=istate]
1157911582 ^- (each imold-types imold-failure)
tests/lib/jibb-full-overlap-basic.hoon+44−10
@@ -14,6 +14,7 @@
1414/* atoms %txt /tests/type-full-overlap/atoms/txt
1515/* flag %txt /tests/type-full-overlap/flag/txt
1616/* nested %txt /tests/type-full-overlap/nested/txt
17+/* order %txt /tests/type-full-overlap/order/txt
1718/* expected %txt /tests/type-full-overlap/expected-basic/txt
1819|%
1920+$ overlap-evidence [file=path source=@t name=term cases=upair:jibb]
@@ -33,18 +34,32 @@
3334 ?~ cases.sh ~
3435 ?~ t.cases.sh ~
3536 `[at.i.cases.sh at.i.t.cases.sh %overlap]
36−++ source-witness
37+++ source-overlap
3738 |= [file=path source=@t name=term]
38− ^- ?
39+ ^- (unit upair:jibb)
3940 =/ parsed (parse:jibb file source)
40− ?: ?=(%| -.parsed) |
41+ ?: ?=(%| -.parsed) ~
4142 =/ molds=imolds:jibb (collect-simple-molds:jibb defs.p.parsed)
4243 =/ found=(unit shape:jibb) (find-simple-mold:jibb name molds)
43− ?~ found |
44+ ?~ found ~
4445 =/ sh=shape:jibb u.found
4546 =? sh ?=(%generic -.sh) body.sh
46− ?. ?=(%union -.sh) |
47− ?=(^ (union-source-overlap:jibb cases.sh molds 256))
47+ ?. ?=(%union -.sh) ~
48+ (union-source-overlap:jibb cases.sh molds 256)
49+++ source-witness
50+ |= [file=path source=@t name=term]
51+ ^- ?
52+ ?=(^ (source-overlap file source name))
53+:: An overlapping pair of cases written at column 3 of the given lines.
54+++ pair-at
55+ |= [pair=upair:jibb first=@ud second=@ud]
56+ ^- ?
57+ ?& =(%overlap relation.pair)
58+ =(first line.beg.first.pair)
59+ =(3 col.beg.first.pair)
60+ =(second line.beg.second.pair)
61+ =(3 col.beg.second.pair)
62+ ==
4863++ detailed
4964 |= [file=path source=@t modules=jbundle:jibb]
5065 ^- detailed-result
@@ -79,7 +94,7 @@
7994 ?: ?=(%& -.result) |
8095 &(!=(0 message.p.result) ?=(~ overlap.p.result))
8196++ run
82− |= [same=@t zero=@t unsupported=@t precedence=@t duplicate=@t invalid=@t distinct=@t parent=@t child=@t generic=@t duplicate-generic=@t atoms=@t flag=@t nested=@t]
97+ |= [same=@t zero=@t unsupported=@t precedence=@t duplicate=@t invalid=@t distinct=@t parent=@t child=@t generic=@t duplicate-generic=@t atoms=@t flag=@t nested=@t order=@t]
8398 ^- (list [@t ?])
8499 =/ root=path /ui/root/jibb
85100 =/ names256=(list @t) (turn (gulf 0 255) |=(n=@ud (scot %ud n)))
@@ -103,6 +118,22 @@
103118 =/ legacy-projected=?
104119 ?: ?=(%& -.legacy-atoms) |
105120 =((to-wain:format p.legacy-atoms) ~['module mold bad has overlapping cases' '/ui/root.jibb:2:3: first union case' ' @t' ' ^' '/ui/root.jibb:3:3: overlapping case' ' @ud' ' ^'])
121+ :: The source witness alone proves the first two cases of .order, but
122+ :: the projection proves the last two and is consulted first, so both
123+ :: the full check and the partial report name the later pair.
124+ =/ order-source=(unit upair:jibb) (source-overlap root order %bad)
125+ =/ order-result=detailed-result (detailed root order ~)
126+ =/ order-full=?
127+ ?: ?=(%& -.order-result) |
128+ ?~ overlap.p.order-result |
129+ =/ ev=overlap-evidence u.overlap.p.order-result
130+ &(=(file.ev root) =(name.ev %bad) (pair-at cases.ev 5 6))
131+ =/ order-partial=wain (to-wain:format (golden-types:jibb root order))
132+ =/ order-reported=?
133+ ?& (lien order-partial |=(line=@t =(line '+$ bad: overlapping cases; mold not checked')))
134+ (lien order-partial |=(line=@t =(line '/ui/root.jibb:5:3: first union case')))
135+ (lien order-partial |=(line=@t =(line '/ui/root.jibb:6:3: overlapping case')))
136+ ==
106137 =/ imported=detailed-result (detailed root parent ~[[child-file child]])
107138 =/ child-pair=(unit upair:jibb) (source-pair child-file child %child-bad)
108139 =/ import-valid=?
@@ -125,6 +156,9 @@
125156 ['two auras have source-bound overlap' (expected-overlap root atoms %bad 2)]
126157 ['flag and yes have source-bound overlap' (expected-overlap root flag %bad 2)]
127158 ['nested equal tags have source-bound overlap' (expected-overlap root nested %bad 2)]
159+ ['source witness alone names the earlier pair' ?~(order-source | (pair-at u.order-source 3 4))]
160+ ['full check names the later projected pair' order-full]
161+ ['partial report names the same later pair' order-reported]
128162 ['duplicate generic parameters remain unstructured' (plain-failure root duplicate-generic)]
129163 ['unsupported remains unstructured' (plain-failure root unsupported)]
130164 ['later overlap exists in precedence source' (source-witness root precedence %bad)]
@@ -142,14 +176,14 @@
142176 ^- @t
143177 (rap 3 (turn lines |=(line=@t (cat 3 line '\0a'))))
144178++ output
145− |= [same=@t zero=@t unsupported=@t precedence=@t duplicate=@t invalid=@t distinct=@t parent=@t child=@t generic=@t duplicate-generic=@t atoms=@t flag=@t nested=@t]
179+ |= [same=@t zero=@t unsupported=@t precedence=@t duplicate=@t invalid=@t distinct=@t parent=@t child=@t generic=@t duplicate-generic=@t atoms=@t flag=@t nested=@t order=@t]
146180 ^- @t
147− =/ result=(list [@t ?]) (run same zero unsupported precedence duplicate invalid distinct parent child generic duplicate-generic atoms flag nested)
181+ =/ result=(list [@t ?]) (run same zero unsupported precedence duplicate invalid distinct parent child generic duplicate-generic atoms flag nested order)
148182 (of-wain:format (turn result |=(entry=[@t ?] (crip "{(trip -.entry)}: {?:(+.entry "ok" "BAD")}"))))
149183++ test-full-overlap-basic
150184 ^- tang
151185 ?~ expected ~[leaf+"expected output missing"]
152− =/ actual=@t (output (text same) (text zero) (text unsupported) (text precedence) (text duplicate) (text invalid) (text distinct) (text parent) (text child) (text generic) (text duplicate-generic) (text atoms) (text flag) (text nested))
186+ =/ actual=@t (output (text same) (text zero) (text unsupported) (text precedence) (text duplicate) (text invalid) (text distinct) (text parent) (text child) (text generic) (text duplicate-generic) (text atoms) (text flag) (text nested) (text order))
153187 ?. =((to-wain:format (cat 3 actual '\0a')) expected)
154188 ~[leaf+"full-module overlap output differs"]
155189 ~
tests/type-full-overlap/about.txt+1−1
@@ -1,3 +1,3 @@
11source: docs/spec/grammar.md, Molds: “Cases must differ as nouns”.
2−tests: Full-module overlap evidence retains the defining source and both case spans through ordinary Jibb imports, and legacy errors render the excerpts. Overlaps that the partial report proves by projection (two auras, `?` and `%.y`, equal nested literal heads) carry the same evidence. Distinct cases check; duplicate names, stale caches, cycles, private imports and other unsupported inputs retain their own earlier errors. Specialized API and prelude paths remain outside this diagnostic slice.
2+tests: Full-module overlap evidence retains the defining source and both case spans through ordinary Jibb imports, and legacy errors render the excerpts. Overlaps that the partial report proves by projection (two auras, `?` and `%.y`, equal nested literal heads) carry the same evidence, and both paths name a projected pair before an earlier pair that only the source witness proves. Distinct cases check; duplicate names, stale caches, cycles, private imports and other unsupported inputs retain their own earlier errors. Specialized API and prelude paths remain outside this diagnostic slice.
33expect: shared eval and ship guards
tests/type-full-overlap/expected-basic.txt+3
@@ -7,6 +7,9 @@ generic wrapper has source-bound overlap: ok
77two auras have source-bound overlap: ok
88flag and yes have source-bound overlap: ok
99nested equal tags have source-bound overlap: ok
10+source witness alone names the earlier pair: ok
11+full check names the later projected pair: ok
12+partial report names the same later pair: ok
1013duplicate generic parameters remain unstructured: ok
1114unsupported remains unstructured: ok
1215later overlap exists in precedence source: ok
tests/type-full-overlap/order.txtnew file+7
@@ -0,0 +1,7 @@
1++$ tagged |$ [A] [%wrapped A]
2++$ bad
3+ (tagged @t)
4+ [%wrapped @p]
5+ @t
6+ @ud
7+++ identity |=(x x)
tools/testdata/ship-selftest+2−2
@@ -379,8 +379,8 @@ def generator_checks(tmp):
379379 {f'tests/type-full-overlap/{name}.txt' for name in (
380380 'same', 'zero', 'unsupported', 'precedence', 'duplicate',
381381 'invalid', 'distinct', 'parent', 'child', 'generic',
382− 'duplicate-generic', 'atoms', 'flag', 'nested', 'expected-basic',
383− 'expected-graph')} <= set(normal.files))
382+ 'duplicate-generic', 'atoms', 'flag', 'nested', 'order',
383+ 'expected-basic', 'expected-graph')} <= set(normal.files))
384384 check('deferred transaction and resolver sources are assembled',
385385 {'tests/type-deferred/nested-src.txt', 'tests/type-deferred/principal-src.txt',
386386 'tests/type-deferred/expected.txt', 'tests/type-deferred-resolver/good.txt',
tools/type-full-overlap-test+1−1
@@ -14,7 +14,7 @@ parser.add_argument('--update', action='store_true')
1414args = parser.parse_args()
1515fixture = root / 'tests/type-full-overlap'
1616cases = {
17− 'basic': ['same', 'zero', 'unsupported', 'precedence', 'duplicate', 'invalid', 'distinct', 'parent', 'child', 'generic', 'duplicate-generic', 'atoms', 'flag', 'nested'],
17+ 'basic': ['same', 'zero', 'unsupported', 'precedence', 'duplicate', 'invalid', 'distinct', 'parent', 'child', 'generic', 'duplicate-generic', 'atoms', 'flag', 'nested', 'order'],
1818 'graph': ['parent', 'child', 'distinct'],
1919}
2020for kind, names in cases.items():