on master help sign in
Propagate union context through unit branches
commit743dfd80c0e029664f05f512cf37a9905f7ac0b3 authoriko <mail@iko.soy> dateFri 30 Oct 2026, 21:03 (1 day ago) parente878edc
9 files changed+688−17
docs/compiler.md+1−1 docs/status.md+7−6 jibb-dev/lib/jibb.hoon+12−5 tests/golden/types-unit-context/about.txt+4 tests/golden/types-unit-context/source.jibb+70 tests/golden/types-unit-context/tokens.txt+374 tests/golden/types-unit-context/tree.txt+182 tests/golden/types-unit-context/types.txt+27 tests/lib/jibb.hoon+11−5
docs/compiler.md+1−1
@@ -62,7 +62,7 @@ For supported closed unions, the type printer keeps the union’s origin separat
6262
6363A known union of `~` and a null-headed cell can be matched by `~` and `[~ value]` arms in either order. The payload binder is checked for shadowing. Unknown subjects, missing or duplicate arms, and unresolved branch results remain unsupported; this fragment infers the prelude’s `fall` and `need` signatures.
6464
65−A known closed union can also provide context to each arm of a complete loobean branch in a cast or a call with a known union sample. Nested branches and transparent groups work; a mismatch reports the expected union and the offending arm. General patterns and context through bodies with local definitions remain unsupported, and unrelated unresolved tags stay pending.
65+A known closed union can also provide context to each arm of a complete loobean or unit-shaped branch in a cast or a call with a known union sample. Nested branches and transparent groups work; a mismatch reports the expected union and the offending arm. General patterns and context through bodies with local definitions remain unsupported, and unrelated unresolved tags stay pending.
6666
6767The separate `jibb-dev/lib/jibb-import.hoon` is an unfinished reader for selected Hoon type graphs. It handles named recursion, nested map, set, queue, list, unit, jar and jug arguments, direct ordered maps, and direct `$^` unions whose source branches can be proved disjoint. It also reads ordered map fields in records when the map arguments are syntactically fixed atom molds and other fields are fixed atom molds or standard collections of static atom molds. Collection names must not be shadowed. The reader can also import a mark door sample, removing its outer sample face and validating its build subject. The reader checks explicit Hoon `$%`, `$?` and `$^` unions against the Grammar’s disjointness rule (doc question 22). It re-evaluates statically recognizable source branches before Hoon can collapse them, checks materialized fork cases, and rejects shapes it cannot prove disjoint. Static records may also have verified standard-collection and `path` siblings. One direct explicit union argument in a standard list, set, map or unit is accepted when its call wrapper and collection provenance are verified and its static cases are pairwise disjoint. A synthetic regression checks that forged wrapper subjects, samples and tails are rejected. Other collection-union forms, nested ordered maps, general source-level disjointness and complete integration with the checker remain unfinished. `+golden-types-imports` can consume fixed-aura atoms, valid term singletons, nested faced or unfaced cells, unions of supported, pairwise-disjoint cases, and opaque standard collections with supported arguments from caller-supplied reader results for declared `/-` imports; `+golden-types-with-marks` accepts the same shapes for declared marks. The caller must pass unchanged results from the source-aware reader: the bridge validates the supplied graph but cannot detect source cases Hoon collapsed before that graph was built. The opaque collection types retain their names and arguments for identity, unification and printing; Jibb-written collection molds and their prelude operations are not yet connected. Other forms remain unsupported. Its disjointness proof is conservative and can reject a valid union it cannot prove disjoint. Collection recognition requires the originating `/sur` core. The reader validates direct zuse subjects and Ford subjects consisting of faced imported cores and a validated tail, checking imported cores transitively; it rejects shadowed names, inconsistent core subjects and other subject shapes. For a recursive reference, the reader matches the exact Hoon hold against named arms in validated cores, including transitive Ford imports; it rejects missing, unlabelled or ambiguous origins. Its fixtures include three real Tlon files; `tools/importer-test` compares the internal projection under eval, and the ship test compares the same golden output. `tools/type-import-test` and `tools/type-mark-test` compare bridge reports under eval and on the ship. `tools/clay-fixtures` also passes Clay-built `/sur` molds and mark samples through the Clay-built importer and partial checker.
6868
docs/status.md+7−6
@@ -19,7 +19,7 @@ On 2026-10-30, @iko decided that Jibb drops `$?`, so a `+$` takes a union's case
1919
2020## Milestone 2: in progress
2121
22−The repository spec records the subsequent type-system and prelude decisions; those changes also need synchronization to the Claude document. An initial inference fragment and a standalone Hoon type reader are being tested. The fragment explicitly reports that it does not check a module; partial bridges pass selected Hoon atoms, term singletons, nested faced or unfaced cells, supported disjoint unions and opaque standard collections from `/sur` molds and marks into inference. Collections retain their names and supported arguments for printing and unification; nested supported union arguments are retained too. The bridge trusts unchanged results from the source-aware reader; a materialized type graph alone cannot reveal cases Hoon already collapsed. Jibb-written collection molds and prelude collection operations are not yet connected to this representation; malformed names and arities fail closed. Selected self-recursive `/sur` molds cross as opaque module-and-name identities; aliases, foreign references, recursive marks, unfolding and construction remain unsupported. The reader handles mark samples, recursive molds whose origins can be verified through Ford imports, nested collections, direct ordered maps, certain ordered-map fields, direct `$^` unions whose cases can be proved disjoint, and one verified explicit union argument in a list, set, map or unit. Ambiguous recursive origins fail closed; recognizable explicit unions are checked from source before Hoon can collapse their cases (doc question 22), while other nested unions, nested ordered maps, general union disjointness and complete import integration remain unfinished. The partial checker resolves a subset of ordinary library imports in dependency order using supplied Jibb sources and the current prelude names, caches completed interfaces per run, and detects missing sources and cycles. It does not yet check API or kind semantics, and the prelude inventory is incomplete. The inference fragment supports unrestricted `@`, selected one-way widenings including aura-family ancestors, generalized atom constraints arising from explicit capitals or bare sample binders, acyclic local value definitions with captures, simple and nonrecursive generic mold aliases, selected faced record casts and field reads, and contextual tags, `~` and constructors for closed disjoint unions, including direct nonrecursive generic unions and propagation through complete loobean branches in casts and known union-sample calls. Contextual null-headed cells fit their cases, but do not supply a `|=%$` constructor; unresolved nulls remain pending and are reported separately from tags. A known union of `~` and a null-headed cell supports a complete `~` / `[~ value]` branch in either order, including shadow checks; unknown subjects, missing or duplicate arms, and unresolved branch results remain unsupported. This fragment infers the prelude’s `fall` and `need` signatures. A value with type variable `A` can fit a field whose type is that same `A`, including in generic union payloads and nested or repeated record fields. Other variable-dependent face merges remain unsupported. Supported closed unions print using an in-scope name or imported alias; an unnamed nongeneric union prints its cases, parenthesized when nested. The latter is print-only. Generic union types retain all arguments in their printed name; if that name is unavailable, the partial printer reports the limitation. Different import faces for the same origin remain compatible; compatibility across distinct union origins and some generic-argument comparisons remain unsupported. Nonrecursive generic aliases can reorder, repeat or omit parameters while retaining a union’s origin, including through local scopes and library interfaces. A generic union declared directly inside a body remains unsupported, as do differing-variable face constraints in a union payload. A transitive generic union whose name is unavailable is reported as unsupported instead of hiding its arguments. Unfixed decimal literals default to `@ud` in gate-free inferred types; recursive local groups and molds, general branch tag context, other constraint cases and defaulting inside gate types still need work. Collection recognition checks the originating core and fails closed on shadows or unsupported Ford subject shapes; a wrapper regression also rejects forged subjects, samples and tails. Its golden fixtures include three real Tlon files. A Clay test passes a Ford-built nested union through the reader into partial inference. The partial prelude includes `murn`, `join`, `snip` and `rear`, parsed but still awaiting checker and backend validation, and [prelude-inventory.md](prelude-inventory.md) is a source audit, not the complete inventory or signatures. The milestone remains unfinished.
22+The repository spec records the subsequent type-system and prelude decisions; those changes also need synchronization to the Claude document. An initial inference fragment and a standalone Hoon type reader are being tested. The fragment explicitly reports that it does not check a module; partial bridges pass selected Hoon atoms, term singletons, nested faced or unfaced cells, supported disjoint unions and opaque standard collections from `/sur` molds and marks into inference. Collections retain their names and supported arguments for printing and unification; nested supported union arguments are retained too. The bridge trusts unchanged results from the source-aware reader; a materialized type graph alone cannot reveal cases Hoon already collapsed. Jibb-written collection molds and prelude collection operations are not yet connected to this representation; malformed names and arities fail closed. Selected self-recursive `/sur` molds cross as opaque module-and-name identities; aliases, foreign references, recursive marks, unfolding and construction remain unsupported. The reader handles mark samples, recursive molds whose origins can be verified through Ford imports, nested collections, direct ordered maps, certain ordered-map fields, direct `$^` unions whose cases can be proved disjoint, and one verified explicit union argument in a list, set, map or unit. Ambiguous recursive origins fail closed; recognizable explicit unions are checked from source before Hoon can collapse their cases (doc question 22), while other nested unions, nested ordered maps, general union disjointness and complete import integration remain unfinished. The partial checker resolves a subset of ordinary library imports in dependency order using supplied Jibb sources and the current prelude names, caches completed interfaces per run, and detects missing sources and cycles. It does not yet check API or kind semantics, and the prelude inventory is incomplete. The inference fragment supports unrestricted `@`, selected one-way widenings including aura-family ancestors, generalized atom constraints arising from explicit capitals or bare sample binders, acyclic local value definitions with captures, simple and nonrecursive generic mold aliases, selected faced record casts and field reads, and contextual tags, `~` and constructors for closed disjoint unions, including direct nonrecursive generic unions and propagation through complete loobean and unit-shaped branches in casts and known union-sample calls, including nested branches. Contextual null-headed cells fit their cases, but do not supply a `|=%$` constructor; unresolved nulls remain pending and are reported separately from tags. A known union of `~` and a null-headed cell supports a complete `~` / `[~ value]` branch in either order, including shadow checks; unknown subjects, missing or duplicate arms, and unresolved branch results remain unsupported. This fragment infers the prelude’s `fall` and `need` signatures. A value with type variable `A` can fit a field whose type is that same `A`, including in generic union payloads and nested or repeated record fields. Other variable-dependent face merges remain unsupported. Supported closed unions print using an in-scope name or imported alias; an unnamed nongeneric union prints its cases, parenthesized when nested. The latter is print-only. Generic union types retain all arguments in their printed name; if that name is unavailable, the partial printer reports the limitation. Different import faces for the same origin remain compatible; compatibility across distinct union origins and some generic-argument comparisons remain unsupported. Nonrecursive generic aliases can reorder, repeat or omit parameters while retaining a union’s origin, including through local scopes and library interfaces. A generic union declared directly inside a body remains unsupported, as do differing-variable face constraints in a union payload. A transitive generic union whose name is unavailable is reported as unsupported instead of hiding its arguments. Unfixed decimal literals default to `@ud` in gate-free inferred types; recursive local groups and molds, general branch tag context, other constraint cases and defaulting inside gate types still need work. Collection recognition checks the originating core and fails closed on shadows or unsupported Ford subject shapes; a wrapper regression also rejects forged subjects, samples and tails. Its golden fixtures include three real Tlon files. A Clay test passes a Ford-built nested union through the reader into partial inference. The partial prelude includes `murn`, `join`, `snip` and `rear`, parsed but still awaiting checker and backend validation, and [prelude-inventory.md](prelude-inventory.md) is a source audit, not the complete inventory or signatures. The milestone remains unfinished.
2323
2424## Milestone 1: parser and mark
2525
@@ -37,8 +37,8 @@ What the plan asks for, and where it is:
3737
3838Besides the plan's list:
3939
40−- 494 golden cases: 278 that parse and 216 that fail, each failure at a stated line and column. One failing case has an unclear expectation (corpus question 3). The newer type-output cases exercise only the partial inference fragment. Each case's `about.txt` quotes the doc's words it tests.
41−- The 494-case corpus passed under `urbit eval` in 59.4 s. The fake ship passed all 499 tests, including the importer, importer/checker and mark/checker bridges, module scope and unification checks, with 25.3 s for sync and 24.3 s for tests. The importer golden compares 141 projections; `tools/clay-fixtures` builds the example Hoon fixtures through Clay, checks a recursive Ford import's origin, and passes Clay-built types through the Clay-built importer and partial checker.
40+- 495 golden cases: 279 that parse and 216 that fail, each failure at a stated line and column. One failing case has an unclear expectation (corpus question 3). The newer type-output cases exercise only the partial inference fragment. Each case's `about.txt` quotes the doc's words it tests.
41+- The 495-case corpus passed under `urbit eval` in 60.3 s. The fake ship passed all 500 tests, including the importer, importer/checker and mark/checker bridges, module scope and unification checks, with 26.8 s for sync and 32.6 s for tests. The importer golden compares 141 projections; `tools/clay-fixtures` builds the example Hoon fixtures through Clay, checks a recursive Ford import's origin, and passes Clay-built types through the Clay-built importer and partial checker.
4242- `tools/testdata/selftest` (22 checks) and `tools/testdata/ship-selftest` test the tools themselves.
4343- Two independent audits before 7c739b7, one of which compared the library with a reference parser written in Python from the doc over about 19,000 generated programs. Before ab797a9, a second Python parser, written from the decisions, agreed with the library on 8,000 generated programs and 900 hand-written probes.
4444- Speed: starting `urbit eval` and building the library takes about 8 s. After that, a 2,000-line module of 400 definitions parses in about a second. Loops over definitions, arms, lines and items grow no stack; nesting costs a few stack frames a level, and 100,000 nested brackets still parse (library section 3).
@@ -75,14 +75,15 @@ Besides the plan's list:
7575| e95ef8f | 2026-10-30 | Bridge selected Hoon unions into partial inference and support generic union aliases |
7676| 56a899f | 2026-10-30 | Infer matching variable types in faced fields and bridge opaque Hoon collections |
7777| 4d45d2f | 2026-10-30 | Resolve selected contextual null literals |
78−| This change | 2026-10-30 | Infer complete unit-shaped branches and bridge selected recursive Hoon molds |
78+| e878edc | 2026-10-30 | Infer complete unit-shaped branches and bridge selected recursive Hoon molds |
79+| This change | 2026-10-30 | Propagate union context through unit-shaped branches |
7980
8081## Checking it
8182
8283On a machine set up as [development.md](development.md) says:
8384
8485```
85−tools/golden # 494 cases under urbit eval
86+tools/golden # 495 cases under urbit eval
8687tools/importer-test # the Hoon importer fixture projection
8788tools/type-import-test # the importer/checker bridge fixture
8889tools/type-mark-test # the mark/checker bridge fixture
@@ -92,7 +93,7 @@ tools/testdata/selftest # the tools themselves
9293tools/doc-blocks docs/spec # the doc's examples are golden cases
9394tools/ship start
9495tools/ship gen-tests --check # tests/lib/jibb.hoon is up to date
95−tools/ship test # the same 494 cases as -test arms on the ship
96+tools/ship test # the same 495 cases as -test arms on the ship
9697tools/testdata/ship-selftest
9798tools/ship check-commit # |commit stores .jibb files
9899tools/clay-fixtures # example /sur files and marks build through Clay
jibb-dev/lib/jibb.hoon+12−5
@@ -6084,7 +6084,7 @@
60846084 ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
60856085 $(fields t.fields, typ i.found)
60866086::
6087−:: Propagate a known union through a direct loobean branch. Empty bodies
6087+:: Propagate a known union through supported loobean and unit branches. Empty bodies
60886088:: and groups are transparent; bodies with definitions keep their normal
60896089:: scoping and wait for general bidirectional inference.
60906090::
@@ -6109,6 +6109,8 @@
61096109 ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
61106110 =/ x=arm i.arms.e
61116111 =/ y=arm i.t.arms.e
6112+ ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
6113+ (infer-unit-branch e env state `[expected context])
61126114 ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y))
61136115 [%| ["branch pattern is not supported by partial inference" ~]]
61146116 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
@@ -6181,7 +6183,7 @@
61816183 ~
61826184::
61836185++ infer-unit-branch
6184− |= [e=expr env=ienv state=istate]
6186+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
61856187 ^- iresult
61866188 ?> ?=(%branch -.e)
61876189 ?~ arms.e [%| ["unit branch is not supported by partial inference" ~]]
@@ -6204,10 +6206,15 @@
62046206 =/ payload=(unit itype) (unit-union-payload typ)
62056207 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
62066208 =/ extended=ienv [[u.binder [u.payload ~]] env]
6207− =/ left=iresult (infer-fragment val.x ?:(first-empty env extended) state.p.subject)
6209+ =/ left=iresult
6210+ ?~ expected (infer-fragment val.x ?:(first-empty env extended) state.p.subject)
6211+ (infer-union-context val.x typ.u.expected ?:(first-empty env extended) state.p.subject context.u.expected)
62086212 ?: ?=(%| -.left) left
6209− =/ right=iresult (infer-fragment val.y ?:(first-empty extended env) state.p.left)
6213+ =/ right=iresult
6214+ ?~ expected (infer-fragment val.y ?:(first-empty extended env) state.p.left)
6215+ (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
62106216 ?: ?=(%| -.right) right
6217+ ?^ expected [%& typ.u.expected state.p.right]
62116218 =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
62126219 ?~ joined [%| ["unit branch results need unsupported inference" ~]]
62136220 [%& typ.p.left state.p.right(sub u.joined)]
@@ -6280,7 +6287,7 @@
62806287 =/ x=arm i.arms.e
62816288 =/ y=arm i.t.arms.e
62826289 ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
6283− (infer-unit-branch e env state)
6290+ (infer-unit-branch e env state ~)
62846291 ?. ?=(%lit -.pat.x) [%| ["branch pattern is not supported by partial inference" ~]]
62856292 ?. ?=(%lit -.pat.y) [%| ["branch pattern is not supported by partial inference" ~]]
62866293 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
tests/golden/types-unit-context/about.txtnew file+4
@@ -0,0 +1,4 @@
1+source: Grammar, Tag resolution: "A tag literal or `~` gets a fresh type variable and a pending constraint"; Patterns: "A name in a pattern always binds anew".
2+tests: A cast or known sample supplies union context to both unit branch arms, including nested unit and loobean branches; bad cases, unknown subjects, shadowing and unrelated pending tags or nulls fail closed.
3+expect: parses
4+expect-types: a partial inference report
tests/golden/types-unit-context/source.jibbnew file+70
@@ -0,0 +1,70 @@
1++$ maybe
2+ ~
3+ [~ value=@t]
4++$ msg
5+ %add
6+ [%note text=@t]
7+++ cast |= x=maybe
8+ ^- msg
9+ ?- x
10+ ~ %add
11+ [~ text] [%note text]
12+++ reversed |= x=maybe
13+ ^- msg
14+ ?- x
15+ [~ text] [%note text]
16+ ~ %add
17+++ consume |= x=msg "ok"
18+++ call |= x=maybe
19+ (consume
20+ ?- x
21+ ~ %add
22+ [~ text] [%note text]
23+++ nested |= x=maybe
24+ ^- msg
25+ ?- x
26+ ~
27+ ?- %.y
28+ %.y %add
29+ %.n [%note "hi"]
30+ [~ text] [%note text]
31+++ bad-empty |= x=maybe
32+ ^- msg
33+ ?- x
34+ ~ %missing
35+ [~ text] [%note text]
36+++ bad-present |= x=maybe
37+ ^- msg
38+ ?- x
39+ ~ %add
40+ [~ text] %missing
41+++ unknown |= x
42+ ^- msg
43+ ?- x
44+ ~ %add
45+ [~ text] [%note text]
46+++ shadow |= x=maybe
47+ ^- msg
48+ ?- x
49+ ~ %add
50+ [~ x] [%note x]
51+++ pending |= x=maybe
52+ ~& %unknown
53+ ^- msg
54+ ?- x
55+ ~ %add
56+ [~ text] [%note text]
57+++ nested-unit |= x=maybe
58+ ^- msg
59+ ?- x
60+ ~
61+ ?- x
62+ ~ %add
63+ [~ inner] [%note inner]
64+ [~ text] [%note text]
65+++ pending-null |= x=maybe
66+ ~& ~
67+ ^- msg
68+ ?- x
69+ ~ %add
70+ [~ text] [%note text]
tests/golden/types-unit-context/tokens.txtnew file+374
@@ -0,0 +1,374 @@
1+1:1 glyph +$
2+1:4 name maybe
3+2:3 INDENT
4+2:3 lit ~
5+3:3 NEWLINE
6+3:3 glyph [
7+3:4 tight lit ~
8+3:6 name value
9+3:11 tight glyph =
10+3:12 tight aura @t
11+3:14 tight glyph ]
12+4:1 DEDENT
13+4:1 NEWLINE
14+4:1 glyph +$
15+4:4 name msg
16+5:3 INDENT
17+5:3 lit %add
18+6:3 NEWLINE
19+6:3 glyph [
20+6:4 tight lit %note
21+6:10 name text
22+6:14 tight glyph =
23+6:15 tight aura @t
24+6:17 tight glyph ]
25+7:1 DEDENT
26+7:1 NEWLINE
27+7:1 glyph ++
28+7:4 name cast
29+7:9 glyph |=
30+7:12 name x
31+7:13 tight glyph =
32+7:14 tight name maybe
33+8:3 INDENT
34+8:3 glyph ^-
35+8:6 name msg
36+9:5 INDENT
37+9:5 glyph ?-
38+9:8 name x
39+10:7 INDENT
40+10:7 lit ~
41+10:9 lit %add
42+11:7 NEWLINE
43+11:7 glyph [
44+11:8 tight lit ~
45+11:10 name text
46+11:14 tight glyph ]
47+11:16 glyph [
48+11:17 tight lit %note
49+11:23 name text
50+11:27 tight glyph ]
51+12:1 DEDENT
52+12:1 DEDENT
53+12:1 DEDENT
54+12:1 NEWLINE
55+12:1 glyph ++
56+12:4 name reversed
57+12:13 glyph |=
58+12:16 name x
59+12:17 tight glyph =
60+12:18 tight name maybe
61+13:3 INDENT
62+13:3 glyph ^-
63+13:6 name msg
64+14:5 INDENT
65+14:5 glyph ?-
66+14:8 name x
67+15:7 INDENT
68+15:7 glyph [
69+15:8 tight lit ~
70+15:10 name text
71+15:14 tight glyph ]
72+15:16 glyph [
73+15:17 tight lit %note
74+15:23 name text
75+15:27 tight glyph ]
76+16:7 NEWLINE
77+16:7 lit ~
78+16:9 lit %add
79+17:1 DEDENT
80+17:1 DEDENT
81+17:1 DEDENT
82+17:1 NEWLINE
83+17:1 glyph ++
84+17:4 name consume
85+17:12 glyph |=
86+17:15 name x
87+17:16 tight glyph =
88+17:17 tight name msg
89+17:21 str "ok"
90+18:1 NEWLINE
91+18:1 glyph ++
92+18:4 name call
93+18:9 glyph |=
94+18:12 name x
95+18:13 tight glyph =
96+18:14 tight name maybe
97+19:3 INDENT
98+19:3 glyph (
99+19:4 tight name consume
100+20:5 INDENT
101+20:5 glyph ?-
102+20:8 name x
103+21:7 INDENT
104+21:7 lit ~
105+21:9 lit %add
106+22:7 NEWLINE
107+22:7 glyph [
108+22:8 tight lit ~
109+22:10 name text
110+22:14 tight glyph ]
111+22:16 glyph [
112+22:17 tight lit %note
113+22:23 name text
114+22:27 tight glyph ]
115+23:1 DEDENT
116+23:1 DEDENT
117+23:1 DEDENT
118+23:1 NEWLINE
119+23:1 glyph ++
120+23:4 name nested
121+23:11 glyph |=
122+23:14 name x
123+23:15 tight glyph =
124+23:16 tight name maybe
125+24:3 INDENT
126+24:3 glyph ^-
127+24:6 name msg
128+25:5 INDENT
129+25:5 glyph ?-
130+25:8 name x
131+26:7 INDENT
132+26:7 lit ~
133+27:9 INDENT
134+27:9 glyph ?-
135+27:12 lit %.y
136+28:11 INDENT
137+28:11 lit %.y
138+28:15 lit %add
139+29:11 NEWLINE
140+29:11 lit %.n
141+29:15 glyph [
142+29:16 tight lit %note
143+29:22 str "hi"
144+29:26 tight glyph ]
145+30:7 DEDENT
146+30:7 DEDENT
147+30:7 NEWLINE
148+30:7 glyph [
149+30:8 tight lit ~
150+30:10 name text
151+30:14 tight glyph ]
152+30:16 glyph [
153+30:17 tight lit %note
154+30:23 name text
155+30:27 tight glyph ]
156+31:1 DEDENT
157+31:1 DEDENT
158+31:1 DEDENT
159+31:1 NEWLINE
160+31:1 glyph ++
161+31:4 name bad-empty
162+31:14 glyph |=
163+31:17 name x
164+31:18 tight glyph =
165+31:19 tight name maybe
166+32:3 INDENT
167+32:3 glyph ^-
168+32:6 name msg
169+33:5 INDENT
170+33:5 glyph ?-
171+33:8 name x
172+34:7 INDENT
173+34:7 lit ~
174+34:9 lit %missing
175+35:7 NEWLINE
176+35:7 glyph [
177+35:8 tight lit ~
178+35:10 name text
179+35:14 tight glyph ]
180+35:16 glyph [
181+35:17 tight lit %note
182+35:23 name text
183+35:27 tight glyph ]
184+36:1 DEDENT
185+36:1 DEDENT
186+36:1 DEDENT
187+36:1 NEWLINE
188+36:1 glyph ++
189+36:4 name bad-present
190+36:16 glyph |=
191+36:19 name x
192+36:20 tight glyph =
193+36:21 tight name maybe
194+37:3 INDENT
195+37:3 glyph ^-
196+37:6 name msg
197+38:5 INDENT
198+38:5 glyph ?-
199+38:8 name x
200+39:7 INDENT
201+39:7 lit ~
202+39:9 lit %add
203+40:7 NEWLINE
204+40:7 glyph [
205+40:8 tight lit ~
206+40:10 name text
207+40:14 tight glyph ]
208+40:16 lit %missing
209+41:1 DEDENT
210+41:1 DEDENT
211+41:1 DEDENT
212+41:1 NEWLINE
213+41:1 glyph ++
214+41:4 name unknown
215+41:12 glyph |=
216+41:15 name x
217+42:3 INDENT
218+42:3 glyph ^-
219+42:6 name msg
220+43:5 INDENT
221+43:5 glyph ?-
222+43:8 name x
223+44:7 INDENT
224+44:7 lit ~
225+44:9 lit %add
226+45:7 NEWLINE
227+45:7 glyph [
228+45:8 tight lit ~
229+45:10 name text
230+45:14 tight glyph ]
231+45:16 glyph [
232+45:17 tight lit %note
233+45:23 name text
234+45:27 tight glyph ]
235+46:1 DEDENT
236+46:1 DEDENT
237+46:1 DEDENT
238+46:1 NEWLINE
239+46:1 glyph ++
240+46:4 name shadow
241+46:11 glyph |=
242+46:14 name x
243+46:15 tight glyph =
244+46:16 tight name maybe
245+47:3 INDENT
246+47:3 glyph ^-
247+47:6 name msg
248+48:5 INDENT
249+48:5 glyph ?-
250+48:8 name x
251+49:7 INDENT
252+49:7 lit ~
253+49:9 lit %add
254+50:7 NEWLINE
255+50:7 glyph [
256+50:8 tight lit ~
257+50:10 name x
258+50:11 tight glyph ]
259+50:13 glyph [
260+50:14 tight lit %note
261+50:20 name x
262+50:21 tight glyph ]
263+51:1 DEDENT
264+51:1 DEDENT
265+51:1 DEDENT
266+51:1 NEWLINE
267+51:1 glyph ++
268+51:4 name pending
269+51:12 glyph |=
270+51:15 name x
271+51:16 tight glyph =
272+51:17 tight name maybe
273+52:3 INDENT
274+52:3 glyph ~&
275+52:6 lit %unknown
276+53:5 INDENT
277+53:5 glyph ^-
278+53:8 name msg
279+54:7 INDENT
280+54:7 glyph ?-
281+54:10 name x
282+55:9 INDENT
283+55:9 lit ~
284+55:11 lit %add
285+56:9 NEWLINE
286+56:9 glyph [
287+56:10 tight lit ~
288+56:12 name text
289+56:16 tight glyph ]
290+56:18 glyph [
291+56:19 tight lit %note
292+56:25 name text
293+56:29 tight glyph ]
294+57:1 DEDENT
295+57:1 DEDENT
296+57:1 DEDENT
297+57:1 DEDENT
298+57:1 NEWLINE
299+57:1 glyph ++
300+57:4 name nested-unit
301+57:16 glyph |=
302+57:19 name x
303+57:20 tight glyph =
304+57:21 tight name maybe
305+58:3 INDENT
306+58:3 glyph ^-
307+58:6 name msg
308+59:5 INDENT
309+59:5 glyph ?-
310+59:8 name x
311+60:7 INDENT
312+60:7 lit ~
313+61:9 INDENT
314+61:9 glyph ?-
315+61:12 name x
316+62:11 INDENT
317+62:11 lit ~
318+62:13 lit %add
319+63:11 NEWLINE
320+63:11 glyph [
321+63:12 tight lit ~
322+63:14 name inner
323+63:19 tight glyph ]
324+63:21 glyph [
325+63:22 tight lit %note
326+63:28 name inner
327+63:33 tight glyph ]
328+64:7 DEDENT
329+64:7 DEDENT
330+64:7 NEWLINE
331+64:7 glyph [
332+64:8 tight lit ~
333+64:10 name text
334+64:14 tight glyph ]
335+64:16 glyph [
336+64:17 tight lit %note
337+64:23 name text
338+64:27 tight glyph ]
339+65:1 DEDENT
340+65:1 DEDENT
341+65:1 DEDENT
342+65:1 NEWLINE
343+65:1 glyph ++
344+65:4 name pending-null
345+65:17 glyph |=
346+65:20 name x
347+65:21 tight glyph =
348+65:22 tight name maybe
349+66:3 INDENT
350+66:3 glyph ~&
351+66:6 lit ~
352+67:5 INDENT
353+67:5 glyph ^-
354+67:8 name msg
355+68:7 INDENT
356+68:7 glyph ?-
357+68:10 name x
358+69:9 INDENT
359+69:9 lit ~
360+69:11 lit %add
361+70:9 NEWLINE
362+70:9 glyph [
363+70:10 tight lit ~
364+70:12 name text
365+70:16 tight glyph ]
366+70:18 glyph [
367+70:19 tight lit %note
368+70:25 name text
369+70:29 tight glyph ]
370+70:30 DEDENT
371+70:30 DEDENT
372+70:30 DEDENT
373+70:30 DEDENT
374+70:30 NEWLINE
tests/golden/types-unit-context/tree.txtnew file+182
@@ -0,0 +1,182 @@
1+(module
2+ (mold 1:1 maybe
3+ (union 2:3
4+ (const 2:3 ~)
5+ (cell 3:3
6+ (const 3:4 ~)
7+ (face 3:6 value (aura 3:12 @t)))))
8+ (mold 4:1 msg
9+ (union 5:3
10+ (const 5:3 %add)
11+ (cell 6:3
12+ (const 6:4 %note)
13+ (face 6:10 text (aura 6:15 @t)))))
14+ (value 7:1 cast
15+ (gate 7:9
16+ (face 7:12 x (ref 7:14 maybe))
17+ (body 8:3
18+ (cast 8:3
19+ (ref 8:6 msg)
20+ (body 9:5
21+ (branch 9:5
22+ (wing 9:8 x)
23+ (arm 10:7 (lit 10:7 ~) (lit 10:9 %add))
24+ (arm 11:7
25+ (cell 11:7 (lit 11:8 ~) (bind 11:10 text))
26+ (tuple 11:16 (lit 11:17 %note) (wing 11:23 text)))))))))
27+ (value 12:1 reversed
28+ (gate 12:13
29+ (face 12:16 x (ref 12:18 maybe))
30+ (body 13:3
31+ (cast 13:3
32+ (ref 13:6 msg)
33+ (body 14:5
34+ (branch 14:5
35+ (wing 14:8 x)
36+ (arm 15:7
37+ (cell 15:7 (lit 15:8 ~) (bind 15:10 text))
38+ (tuple 15:16 (lit 15:17 %note) (wing 15:23 text)))
39+ (arm 16:7 (lit 16:7 ~) (lit 16:9 %add))))))))
40+ (value 17:1 consume
41+ (gate 17:12
42+ (face 17:15 x (ref 17:17 msg))
43+ (str 17:21 "ok")))
44+ (value 18:1 call
45+ (gate 18:9
46+ (face 18:12 x (ref 18:14 maybe))
47+ (body 19:3
48+ (group 19:3
49+ (call 19:4
50+ (wing 19:4 consume)
51+ (branch 20:5
52+ (wing 20:8 x)
53+ (arm 21:7 (lit 21:7 ~) (lit 21:9 %add))
54+ (arm 22:7
55+ (cell 22:7 (lit 22:8 ~) (bind 22:10 text))
56+ (tuple 22:16 (lit 22:17 %note) (wing 22:23 text)))))))))
57+ (value 23:1 nested
58+ (gate 23:11
59+ (face 23:14 x (ref 23:16 maybe))
60+ (body 24:3
61+ (cast 24:3
62+ (ref 24:6 msg)
63+ (body 25:5
64+ (branch 25:5
65+ (wing 25:8 x)
66+ (arm 26:7
67+ (lit 26:7 ~)
68+ (body 27:9
69+ (branch 27:9
70+ (lit 27:12 %.y)
71+ (arm 28:11 (lit 28:11 %.y) (lit 28:15 %add))
72+ (arm 29:11
73+ (lit 29:11 %.n)
74+ (tuple 29:15 (lit 29:16 %note) (str 29:22 "hi"))))))
75+ (arm 30:7
76+ (cell 30:7 (lit 30:8 ~) (bind 30:10 text))
77+ (tuple 30:16 (lit 30:17 %note) (wing 30:23 text)))))))))
78+ (value 31:1 bad-empty
79+ (gate 31:14
80+ (face 31:17 x (ref 31:19 maybe))
81+ (body 32:3
82+ (cast 32:3
83+ (ref 32:6 msg)
84+ (body 33:5
85+ (branch 33:5
86+ (wing 33:8 x)
87+ (arm 34:7 (lit 34:7 ~) (lit 34:9 %missing))
88+ (arm 35:7
89+ (cell 35:7 (lit 35:8 ~) (bind 35:10 text))
90+ (tuple 35:16 (lit 35:17 %note) (wing 35:23 text)))))))))
91+ (value 36:1 bad-present
92+ (gate 36:16
93+ (face 36:19 x (ref 36:21 maybe))
94+ (body 37:3
95+ (cast 37:3
96+ (ref 37:6 msg)
97+ (body 38:5
98+ (branch 38:5
99+ (wing 38:8 x)
100+ (arm 39:7 (lit 39:7 ~) (lit 39:9 %add))
101+ (arm 40:7
102+ (cell 40:7 (lit 40:8 ~) (bind 40:10 text))
103+ (lit 40:16 %missing))))))))
104+ (value 41:1 unknown
105+ (gate 41:12
106+ (bind 41:15 x)
107+ (body 42:3
108+ (cast 42:3
109+ (ref 42:6 msg)
110+ (body 43:5
111+ (branch 43:5
112+ (wing 43:8 x)
113+ (arm 44:7 (lit 44:7 ~) (lit 44:9 %add))
114+ (arm 45:7
115+ (cell 45:7 (lit 45:8 ~) (bind 45:10 text))
116+ (tuple 45:16 (lit 45:17 %note) (wing 45:23 text)))))))))
117+ (value 46:1 shadow
118+ (gate 46:11
119+ (face 46:14 x (ref 46:16 maybe))
120+ (body 47:3
121+ (cast 47:3
122+ (ref 47:6 msg)
123+ (body 48:5
124+ (branch 48:5
125+ (wing 48:8 x)
126+ (arm 49:7 (lit 49:7 ~) (lit 49:9 %add))
127+ (arm 50:7
128+ (cell 50:7 (lit 50:8 ~) (bind 50:10 x))
129+ (tuple 50:13 (lit 50:14 %note) (wing 50:20 x)))))))))
130+ (value 51:1 pending
131+ (gate 51:12
132+ (face 51:15 x (ref 51:17 maybe))
133+ (body 52:3
134+ (trace 52:3
135+ (lit 52:6 %unknown)
136+ (body 53:5
137+ (cast 53:5
138+ (ref 53:8 msg)
139+ (body 54:7
140+ (branch 54:7
141+ (wing 54:10 x)
142+ (arm 55:9 (lit 55:9 ~) (lit 55:11 %add))
143+ (arm 56:9
144+ (cell 56:9 (lit 56:10 ~) (bind 56:12 text))
145+ (tuple 56:18 (lit 56:19 %note) (wing 56:25 text)))))))))))
146+ (value 57:1 nested-unit
147+ (gate 57:16
148+ (face 57:19 x (ref 57:21 maybe))
149+ (body 58:3
150+ (cast 58:3
151+ (ref 58:6 msg)
152+ (body 59:5
153+ (branch 59:5
154+ (wing 59:8 x)
155+ (arm 60:7
156+ (lit 60:7 ~)
157+ (body 61:9
158+ (branch 61:9
159+ (wing 61:12 x)
160+ (arm 62:11 (lit 62:11 ~) (lit 62:13 %add))
161+ (arm 63:11
162+ (cell 63:11 (lit 63:12 ~) (bind 63:14 inner))
163+ (tuple 63:21 (lit 63:22 %note) (wing 63:28 inner))))))
164+ (arm 64:7
165+ (cell 64:7 (lit 64:8 ~) (bind 64:10 text))
166+ (tuple 64:16 (lit 64:17 %note) (wing 64:23 text)))))))))
167+ (value 65:1 pending-null
168+ (gate 65:17
169+ (face 65:20 x (ref 65:22 maybe))
170+ (body 66:3
171+ (trace 66:3
172+ (lit 66:6 ~)
173+ (body 67:5
174+ (cast 67:5
175+ (ref 67:8 msg)
176+ (body 68:7
177+ (branch 68:7
178+ (wing 68:10 x)
179+ (arm 69:9 (lit 69:9 ~) (lit 69:11 %add))
180+ (arm 70:9
181+ (cell 70:9 (lit 70:10 ~) (bind 70:12 text))
182+ (tuple 70:18 (lit 70:19 %note) (wing 70:25 text))))))))))))
tests/golden/types-unit-context/types.txtnew file+27
@@ -0,0 +1,27 @@
1+partial inference; module not checked
2++$ maybe: cases proven disjoint; mold not checked
3++$ msg: cases proven disjoint; mold not checked
4+++ cast: $-(maybe msg)
5+++ reversed: $-(maybe msg)
6+++ consume: $-(msg @t)
7+++ call: $-(maybe @t)
8+++ nested: $-(maybe msg)
9+++ bad-empty: branch arm does not fit its expected union
10+/tests/golden/types-unit-context/source.jibb:32:6: expected union
11+ ^- msg
12+ ^
13+/tests/golden/types-unit-context/source.jibb:34:9: branch arm
14+ ~ %missing
15+ ^
16+++ bad-present: branch arm does not fit its expected union
17+/tests/golden/types-unit-context/source.jibb:37:6: expected union
18+ ^- msg
19+ ^
20+/tests/golden/types-unit-context/source.jibb:40:16: branch arm
21+ [~ text] %missing
22+ ^
23+++ unknown: unit branch subject is not supported by partial inference
24+++ shadow: pattern binder shadows a name
25+++ pending: tag needs context in partial inference
26+++ nested-unit: $-(maybe msg)
27+++ pending-null: `~` needs context in partial inference
tests/lib/jibb.hoon+11−5
@@ -1722,10 +1722,14 @@
17221722/* tok-493 %txt /tests/golden/types-union-unresolved-flow/tokens/txt
17231723/* tre-493 %txt /tests/golden/types-union-unresolved-flow/tree/txt
17241724/* typ-493 %txt /tests/golden/types-union-unresolved-flow/types/txt
1725−/* src-494 %jibb /tests/golden/types-unit-patterns/source/jibb
1726−/* tok-494 %txt /tests/golden/types-unit-patterns/tokens/txt
1727−/* tre-494 %txt /tests/golden/types-unit-patterns/tree/txt
1728−/* typ-494 %txt /tests/golden/types-unit-patterns/types/txt
1725+/* src-494 %jibb /tests/golden/types-unit-context/source/jibb
1726+/* tok-494 %txt /tests/golden/types-unit-context/tokens/txt
1727+/* tre-494 %txt /tests/golden/types-unit-context/tree/txt
1728+/* typ-494 %txt /tests/golden/types-unit-context/types/txt
1729+/* src-495 %jibb /tests/golden/types-unit-patterns/source/jibb
1730+/* tok-495 %txt /tests/golden/types-unit-patterns/tokens/txt
1731+/* tre-495 %txt /tests/golden/types-unit-patterns/tree/txt
1732+/* typ-495 %txt /tests/golden/types-unit-patterns/types/txt
17291733|%
17301734:: one arm per case
17311735::
@@ -2715,8 +2719,10 @@
27152719 (weld (check ~.types-union-unresolved src-492 `tok-492 `tre-492) (check-types ~.types-union-unresolved ~[%tests %golden ~.types-union-unresolved %source %jibb] src-492 `typ-492))
27162720++ test-types-union-unresolved-flow
27172721 (weld (check ~.types-union-unresolved-flow src-493 `tok-493 `tre-493) (check-types ~.types-union-unresolved-flow ~[%tests %golden ~.types-union-unresolved-flow %source %jibb] src-493 `typ-493))
2722+++ test-types-unit-context
2723+ (weld (check ~.types-unit-context src-494 `tok-494 `tre-494) (check-types ~.types-unit-context ~[%tests %golden ~.types-unit-context %source %jibb] src-494 `typ-494))
27182724++ test-types-unit-patterns
2719− (weld (check ~.types-unit-patterns src-494 `tok-494 `tre-494) (check-types ~.types-unit-patterns ~[%tests %golden ~.types-unit-patterns %source %jibb] src-494 `typ-494))
2725+ (weld (check ~.types-unit-patterns src-495 `tok-495 `tre-495) (check-types ~.types-unit-patterns ~[%tests %golden ~.types-unit-patterns %source %jibb] src-495 `typ-495))
27202726::
27212727:: +check: run golden:jibb on a case and compare both outputs
27222728::