2b9666c · jibb · git.iko.soy

git.iko.soy/jibb

Pass projected pairs to the overlap witness and state its order

2b9666cClaude7 hours ago

docs/compiler.md+1−1

@@ -66,7 +66,7 @@ Before the empty-capital optimization below, single sequential eval runs includi

67Restricted-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.

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.

71A 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.

jibb-dev/lib/jibb.hoon+12−9

@@ -11068,14 +11068,16 @@

11068 (weld pairs $(cases t.cases))

11069::

11070:: 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

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

11072−:: nested literal cells; the source slice is tried only when some pair

11075+:: source slice is tried only when some pair is unknown, for its one-hop

11073−:: is unknown, for its one-hop generic applications. A missing witness

11076+:: generic applications. A missing witness does not mean the cases are

11074−:: does not mean the cases are disjoint.

11077+:: disjoint.

11075++ mold-overlap-witness

11078++ mold-overlap-witness

11076− |= [cases=(list shape) molds=imolds]

11079+ |= [cases=(list shape) pairs=(list upair) molds=imolds]

11077 ^- (unit upair)

11080 ^- (unit upair)

11078− =/ pairs=(list upair) (union-pairs cases molds)

11079 =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))

11081 =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))

11080 ?^ overlapping `i.overlapping

11082 ?^ overlapping `i.overlapping

11081 ?. (lien pairs |=(p=upair =(%unknown relation.p))) ~

11083 ?. (lien pairs |=(p=upair =(%unknown relation.p))) ~

@@ -11219,14 +11221,14 @@

11219 (of-wain:format ~[(crip "+$ {(trip name.d)}: type hole needs a determined type") text])

11221 (of-wain:format ~[(crip "+$ {(trip name.d)}: type hole needs a determined type") text])

11220 =? sh ?=(%generic -.sh) body.sh

11222 =? sh ?=(%generic -.sh) body.sh

11221 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")

11223 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")

11224+ =/ pairs=(list upair) (union-pairs cases.sh molds)

11222− =/ witness=(unit upair) (mold-overlap-witness cases.sh molds)

11225+ =/ witness=(unit upair) (mold-overlap-witness cases.sh pairs molds)

11223 ?^ witness

11226 ?^ witness

11224 =/ p=upair u.witness

11227 =/ p=upair u.witness

11225 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")

11228 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")

11226 =/ first=@t (show-error src [file line.beg.first.p col.beg.first.p "first union case"])

11229 =/ first=@t (show-error src [file line.beg.first.p col.beg.first.p "first union case"])

11227 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])

11230 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])

11228 (of-wain:format ~[summary first second])

11231 (of-wain:format ~[summary first second])

11229− =/ pairs=(list upair) (union-pairs cases.sh molds)

11230 ?: (lien pairs |=(p=upair =(%unknown relation.p)))

11232 ?: (lien pairs |=(p=upair =(%unknown relation.p)))

11231 ?. (union-source-distinct-tags cases.sh molds 256)

11233 ?. (union-source-distinct-tags cases.sh molds 256)

11232 (crip "+$ {(trip name.d)}: case disjointness unresolved; mold not checked")

11234 (crip "+$ {(trip name.d)}: case disjointness unresolved; mold not checked")

@@ -11573,7 +11575,8 @@

11573 ?. valid ~

11575 ?. valid ~

11574 =? sh ?=(%generic -.sh) body.sh

11576 =? sh ?=(%generic -.sh) body.sh

11575 ?. ?=(%union -.sh) ~

11577 ?. ?=(%union -.sh) ~

11578+ :: A failed inference keeps no projection, so it is computed once more.

11576− (mold-overlap-witness cases.sh molds)

11579+ (mold-overlap-witness cases.sh (union-pairs cases.sh molds) molds)

11577++ module-mold-types-detail

11580++ module-mold-types-detail

11578 |= [molds=imolds state=istate]

11581 |= [molds=imolds state=istate]

11579 ^- (each imold-types imold-failure)

11582 ^- (each imold-types imold-failure)

tests/lib/jibb-full-overlap-basic.hoon+44−10

@@ -14,6 +14,7 @@

14/* atoms %txt /tests/type-full-overlap/atoms/txt

15/* flag %txt /tests/type-full-overlap/flag/txt

16/* nested %txt /tests/type-full-overlap/nested/txt

17+/* order %txt /tests/type-full-overlap/order/txt

17/* expected %txt /tests/type-full-overlap/expected-basic/txt

18/* expected %txt /tests/type-full-overlap/expected-basic/txt

18|%

19|%

19+$ overlap-evidence [file=path source=@t name=term cases=upair:jibb]

20+$ overlap-evidence [file=path source=@t name=term cases=upair:jibb]

@@ -33,18 +34,32 @@

33 ?~ cases.sh ~

34 ?~ cases.sh ~

34 ?~ t.cases.sh ~

35 ?~ t.cases.sh ~

35 `[at.i.cases.sh at.i.t.cases.sh %overlap]

36 `[at.i.cases.sh at.i.t.cases.sh %overlap]

36−++ source-witness

37+++ source-overlap

37 |= [file=path source=@t name=term]

38 |= [file=path source=@t name=term]

38− ^- ?

39+ ^- (unit upair:jibb)

39 =/ parsed (parse:jibb file source)

40 =/ parsed (parse:jibb file source)

40− ?: ?=(%| -.parsed) |

41+ ?: ?=(%| -.parsed) ~

41 =/ molds=imolds:jibb (collect-simple-molds:jibb defs.p.parsed)

42 =/ molds=imolds:jibb (collect-simple-molds:jibb defs.p.parsed)

42 =/ found=(unit shape:jibb) (find-simple-mold:jibb name molds)

43 =/ found=(unit shape:jibb) (find-simple-mold:jibb name molds)

43− ?~ found |

44+ ?~ found ~

44 =/ sh=shape:jibb u.found

45 =/ sh=shape:jibb u.found

45 =? sh ?=(%generic -.sh) body.sh

46 =? sh ?=(%generic -.sh) body.sh

46− ?. ?=(%union -.sh) |

47+ ?. ?=(%union -.sh) ~

47− ?=(^ (union-source-overlap:jibb cases.sh molds 256))

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+ ==

48++ detailed

63++ detailed

49 |= [file=path source=@t modules=jbundle:jibb]

64 |= [file=path source=@t modules=jbundle:jibb]

50 ^- detailed-result

65 ^- detailed-result

@@ -79,7 +94,7 @@

79 ?: ?=(%& -.result) |

94 ?: ?=(%& -.result) |

80 &(!=(0 message.p.result) ?=(~ overlap.p.result))

95 &(!=(0 message.p.result) ?=(~ overlap.p.result))

81++ run

96++ 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]

83 ^- (list [@t ?])

98 ^- (list [@t ?])

84 =/ root=path /ui/root/jibb

99 =/ root=path /ui/root/jibb

85 =/ names256=(list @t) (turn (gulf 0 255) |=(n=@ud (scot %ud n)))

100 =/ names256=(list @t) (turn (gulf 0 255) |=(n=@ud (scot %ud n)))

@@ -103,6 +118,22 @@

103 =/ legacy-projected=?

118 =/ legacy-projected=?

104 ?: ?=(%& -.legacy-atoms) |

119 ?: ?=(%& -.legacy-atoms) |

105 =((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' ' ^'])

120 =((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+ ==

106 =/ imported=detailed-result (detailed root parent ~[[child-file child]])

137 =/ imported=detailed-result (detailed root parent ~[[child-file child]])

107 =/ child-pair=(unit upair:jibb) (source-pair child-file child %child-bad)

138 =/ child-pair=(unit upair:jibb) (source-pair child-file child %child-bad)

108 =/ import-valid=?

139 =/ import-valid=?

@@ -125,6 +156,9 @@

125 ['two auras have source-bound overlap' (expected-overlap root atoms %bad 2)]

156 ['two auras have source-bound overlap' (expected-overlap root atoms %bad 2)]

126 ['flag and yes have source-bound overlap' (expected-overlap root flag %bad 2)]

157 ['flag and yes have source-bound overlap' (expected-overlap root flag %bad 2)]

127 ['nested equal tags have source-bound overlap' (expected-overlap root nested %bad 2)]

158 ['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]

128 ['duplicate generic parameters remain unstructured' (plain-failure root duplicate-generic)]

162 ['duplicate generic parameters remain unstructured' (plain-failure root duplicate-generic)]

129 ['unsupported remains unstructured' (plain-failure root unsupported)]

163 ['unsupported remains unstructured' (plain-failure root unsupported)]

130 ['later overlap exists in precedence source' (source-witness root precedence %bad)]

164 ['later overlap exists in precedence source' (source-witness root precedence %bad)]

@@ -142,14 +176,14 @@

142 ^- @t

176 ^- @t

143 (rap 3 (turn lines |=(line=@t (cat 3 line '\0a'))))

177 (rap 3 (turn lines |=(line=@t (cat 3 line '\0a'))))

144++ output

178++ 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]

146 ^- @t

180 ^- @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)

148 (of-wain:format (turn result |=(entry=[@t ?] (crip "{(trip -.entry)}: {?:(+.entry "ok" "BAD")}"))))

182 (of-wain:format (turn result |=(entry=[@t ?] (crip "{(trip -.entry)}: {?:(+.entry "ok" "BAD")}"))))

149++ test-full-overlap-basic

183++ test-full-overlap-basic

150 ^- tang

184 ^- tang

151 ?~ expected ~[leaf+"expected output missing"]

185 ?~ 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))

153 ?. =((to-wain:format (cat 3 actual '\0a')) expected)

187 ?. =((to-wain:format (cat 3 actual '\0a')) expected)

154 ~[leaf+"full-module overlap output differs"]

188 ~[leaf+"full-module overlap output differs"]

155 ~

189 ~

tests/type-full-overlap/about.txt+1−1

@@ -1,3 +1,3 @@

1source: 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.

3expect: shared eval and ship guards

tests/type-full-overlap/expected-basic.txt+3

@@ -7,6 +7,9 @@ generic wrapper has source-bound overlap: ok

7two auras have source-bound overlap: ok

8flag and yes have source-bound overlap: ok

9nested 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

10duplicate generic parameters remain unstructured: ok

13duplicate generic parameters remain unstructured: ok

11unsupported remains unstructured: ok

14unsupported remains unstructured: ok

12later overlap exists in precedence source: ok

15later 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):

379 {f'tests/type-full-overlap/{name}.txt' for name in (

380 'same', 'zero', 'unsupported', 'precedence', 'duplicate',

381 'invalid', 'distinct', 'parent', 'child', 'generic',

382− 'duplicate-generic', 'atoms', 'flag', 'nested', 'expected-basic',

382+ 'duplicate-generic', 'atoms', 'flag', 'nested', 'order',

383− 'expected-graph')} <= set(normal.files))

383+ 'expected-basic', 'expected-graph')} <= set(normal.files))

384 check('deferred transaction and resolver sources are assembled',

385 {'tests/type-deferred/nested-src.txt', 'tests/type-deferred/principal-src.txt',

386 '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')

14args = parser.parse_args()

15fixture = root / 'tests/type-full-overlap'

16cases = {

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'],

18 'graph': ['parent', 'child', 'distinct'],

19}

20for kind, names in cases.items():