447a592 · jibb · git.iko.soy

git.iko.soy/jibb

Report projected union overlaps from the full module check

447a592Claude7 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. `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. Existing pairwise union analysis, parsing, atom and name sizes, source-excerpt rendering, and downstream checking 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 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.

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+19−10

@@ -11067,6 +11067,20 @@

11067 [at.first at.second (union-relate a (project-union-mold second molds ~))]

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

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.

11075+++ mold-overlap-witness

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

11077+ ^- (unit upair)

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

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

11080+ ?^ overlapping `i.overlapping

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

11082+ (union-source-overlap cases molds 256)

11083+::

11070:: A closed structural mold supplies no equation to determine a hole.

11084:: A closed structural mold supplies no equation to determine a hole.

11071:: Applications, references, unbound capitals and unions are unproved.

11085:: Applications, references, unbound capitals and unions are unproved.

11072++ simple-mold-hole

11086++ simple-mold-hole

@@ -11205,19 +11219,14 @@

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

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

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

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

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

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

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

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

11210− =. overlapping

11211− ?^ overlapping overlapping

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

11213− =/ witness=(unit upair) (union-source-overlap cases.sh molds 256)

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

11214− ?~(witness ~ ~[u.witness])

11223+ ?^ witness

11215− ?^ overlapping

11224+ =/ p=upair u.witness

11216− =/ p=upair i.overlapping

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -11564,7 +11573,7 @@

11564 ?. valid ~

11573 ?. valid ~

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

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

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

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

11567− (union-source-overlap cases.sh molds 256)

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

11568++ module-mold-types-detail

11577++ module-mold-types-detail

11569 |= [molds=imolds state=istate]

11578 |= [molds=imolds state=istate]

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

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

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

@@ -11,6 +11,9 @@

11/* child %txt /tests/type-full-overlap/child/txt

12/* generic %txt /tests/type-full-overlap/generic/txt

13/* duplicate-generic %txt /tests/type-full-overlap/duplicate-generic/txt

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

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

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

15|%

18|%

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

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

@@ -46,8 +49,9 @@

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

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

47 ^- detailed-result

50 ^- detailed-result

48 (infer-jibb-file-detailed:jibb file source ~ ~ modules ~[file] ~ ~ ~ ~)

51 (infer-jibb-file-detailed:jibb file source ~ ~ modules ~[file] ~ ~ ~ ~)

52+:: The first two cases overlap, written on consecutive lines from .line.

49++ expected-overlap

53++ expected-overlap

50− |= [file=path source=@t name=term]

54+ |= [file=path source=@t name=term line=@ud]

51 ^- ?

55 ^- ?

52 =/ expected=(unit upair:jibb) (source-pair file source name)

56 =/ expected=(unit upair:jibb) (source-pair file source name)

53 ?~ expected |

57 ?~ expected |

@@ -61,9 +65,9 @@

61 =(name.ev name)

65 =(name.ev name)

62 =(cases.ev u.expected)

66 =(cases.ev u.expected)

63 =(%overlap relation.cases.ev)

67 =(%overlap relation.cases.ev)

64− =(3 line.beg.first.cases.ev)

68+ =(line line.beg.first.cases.ev)

65 =(3 col.beg.first.cases.ev)

69 =(3 col.beg.first.cases.ev)

66− =(4 line.beg.second.cases.ev)

70+ =(+(line) line.beg.second.cases.ev)

67 =(3 col.beg.second.cases.ev)

71 =(3 col.beg.second.cases.ev)

68 ==

72 ==

69++ plain-failure

73++ plain-failure

@@ -75,7 +79,7 @@

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

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

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

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

77++ run

81++ run

78− |= [same=@t zero=@t unsupported=@t precedence=@t duplicate=@t invalid=@t distinct=@t parent=@t child=@t generic=@t duplicate-generic=@t]

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]

79 ^- (list [@t ?])

83 ^- (list [@t ?])

80 =/ root=path /ui/root/jibb

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

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

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

@@ -94,6 +98,11 @@

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

98 ?: ?=(%& -.legacy) |

95 =/ lines=wain (to-wain:format p.legacy)

99 =/ lines=wain (to-wain:format p.legacy)

96 &((lien lines |=(line=@t =(line '/ui/root.jibb:3:3: first union case'))) (lien lines |=(line=@t =(line '/ui/root.jibb:4:3: overlapping case'))))

100 &((lien lines |=(line=@t =(line '/ui/root.jibb:3:3: first union case'))) (lien lines |=(line=@t =(line '/ui/root.jibb:4:3: overlapping case'))))

101+ :: A projected overlap renders the same error as a source witness.

102+ =/ legacy-atoms=jfile-result:jibb (infer-jibb-file:jibb root atoms ~ ~ ~ ~[root] ~ ~ ~ ~)

103+ =/ legacy-projected=?

104+ ?: ?=(%& -.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' ' ^'])

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

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

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

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

99 =/ import-valid=?

108 =/ import-valid=?

@@ -110,9 +119,12 @@

110 :~ ['256 generic parameters accepted by scan' (module-mold-params-valid:jibb names256 *(set @t) 256)]

119 :~ ['256 generic parameters accepted by scan' (module-mold-params-valid:jibb names256 *(set @t) 256)]

111 ['257 generic parameters exhaust scan' !(module-mold-params-valid:jibb names257 *(set @t) 256)]

120 ['257 generic parameters exhaust scan' !(module-mold-params-valid:jibb names257 *(set @t) 256)]

112 ['duplicate generic parameters fail scan' !(module-mold-params-valid:jibb ~['A' 'A'] *(set @t) 256)]

121 ['duplicate generic parameters fail scan' !(module-mold-params-valid:jibb ~['A' 'A'] *(set @t) 256)]

113− ['same head has source-bound overlap' (expected-overlap root same %bad)]

122+ ['same head has source-bound overlap' (expected-overlap root same %bad 3)]

114− ['zero spelling has source-bound overlap' (expected-overlap root zero %bad)]

123+ ['zero spelling has source-bound overlap' (expected-overlap root zero %bad 3)]

115− ['generic wrapper has source-bound overlap' (expected-overlap root generic %bad)]

124+ ['generic wrapper has source-bound overlap' (expected-overlap root generic %bad 3)]

125+ ['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)]

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

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

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

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

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

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

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

@@ -122,6 +134,7 @@

122 ['distinct alias source parses and checks' &(?=(%& -.good-parsed) ?=(%& -.good-result))]

134 ['distinct alias source parses and checks' &(?=(%& -.good-parsed) ?=(%& -.good-result))]

123 ['parent itself has different positive overlap' (source-witness root parent %parent-bad)]

135 ['parent itself has different positive overlap' (source-witness root parent %parent-bad)]

124 ['legacy full-module error contains both excerpts' legacy-excerpts]

136 ['legacy full-module error contains both excerpts' legacy-excerpts]

137+ ['legacy projected overlap error is exact' legacy-projected]

125 ['import overlap retains exact child source' import-valid]

138 ['import overlap retains exact child source' import-valid]

126 ==

139 ==

127++ text

140++ text

@@ -129,14 +142,14 @@

129 ^- @t

142 ^- @t

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

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

131++ output

144++ output

132− |= [same=@t zero=@t unsupported=@t precedence=@t duplicate=@t invalid=@t distinct=@t parent=@t child=@t generic=@t duplicate-generic=@t]

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]

133 ^- @t

146 ^- @t

134− =/ result=(list [@t ?]) (run same zero unsupported precedence duplicate invalid distinct parent child generic duplicate-generic)

147+ =/ result=(list [@t ?]) (run same zero unsupported precedence duplicate invalid distinct parent child generic duplicate-generic atoms flag nested)

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

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

136++ test-full-overlap-basic

149++ test-full-overlap-basic

137 ^- tang

150 ^- tang

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

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

139− =/ 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))

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

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

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

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

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

142 ~

155 ~

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. 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. 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/atoms.txtnew file+4

@@ -0,0 +1,4 @@

1++$ bad

2+ @t

3+ @ud

4+++ identity |=(x x)

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

@@ -4,6 +4,9 @@ duplicate generic parameters fail scan: ok

4same head has source-bound overlap: ok

5zero spelling has source-bound overlap: ok

6generic wrapper has source-bound overlap: ok

7+two auras have source-bound overlap: ok

8+flag and yes have source-bound overlap: ok

9+nested equal tags have source-bound overlap: ok

7duplicate generic parameters remain unstructured: ok

10duplicate generic parameters remain unstructured: ok

8unsupported remains unstructured: ok

11unsupported remains unstructured: ok

9later overlap exists in precedence source: ok

12later overlap exists in precedence source: ok

@@ -13,4 +16,5 @@ invalid source rejects without overlap: ok

13distinct alias source parses and checks: ok

16distinct alias source parses and checks: ok

14parent itself has different positive overlap: ok

17parent itself has different positive overlap: ok

15legacy full-module error contains both excerpts: ok

18legacy full-module error contains both excerpts: ok

19+legacy projected overlap error is exact: ok

16import overlap retains exact child source: ok

20import overlap retains exact child source: ok

tests/type-full-overlap/flag.txtnew file+4

@@ -0,0 +1,4 @@

1++$ bad

2+ ?

3+ %.y

4+++ identity |=(x x)

tests/type-full-overlap/nested.txtnew file+4

@@ -0,0 +1,4 @@

1++$ bad

2+ [%a [%b @ud]]

3+ [%a [%b @t]]

4+++ identity |=(x x)

tools/testdata/ship-selftest+2−1

@@ -379,7 +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', 'expected-basic', 'expected-graph')} <= set(normal.files))

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

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

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

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

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

385 'tests/type-deferred/expected.txt', 'tests/type-deferred-resolver/good.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'],

17+ 'basic': ['same', 'zero', 'unsupported', 'precedence', 'duplicate', 'invalid', 'distinct', 'parent', 'child', 'generic', 'duplicate-generic', 'atoms', 'flag', 'nested'],

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

19}

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