38c711c · jibb · git.iko.soy

git.iko.soy/jibb

Unify branch result joining

Use unification followed by explicitly present atom widening for every uncontextual branch kind. Make multi-arm joins independent of arm order, preserve deferred pending-literal fallback, and cover variable substitutions, singleton atoms, and restricted decimals.

commit38c711cca1adae8cfdb084441dd63eb3f789222e authoriko <mail@iko.soy> dateMon 2 Nov 2026, 21:32 (9 hours ago) parent84b8527

33 files changed+1428−654

compare with master

unifiedsplit

docs/compiler.md+3−1

@@ -58,6 +58,8 @@ The core is split into chapters, `+| %name`, in this order:

5858

5959The inference fragment supports fixed auras, unrestricted `@`, one-way widening into it and toward aura-family ancestors, generic variables and gates, faced and unfaced cells, cell sample binders, known record field reads, a cell pattern of two or more binders, a complete two-arm loobean branch, a complete two-arm unit-shaped branch, closed local mold aliases and acyclic forward value references. For a supported single syntactic top-level recursive gate, the checker infers the sample first and uses that exact sample, including its field faces, in a monomorphic self placeholder. The completed body must unify with the placeholder before the gate is generalized; incompatible recursive arguments can report the call and argument sites. Uses of generalized top-level definitions instantiate their schemes independently. For a complete loobean branch with one direct self-call arm, the checker can infer the other arm independently and use its closed, fully resolved type to seed the recursive result; it then checks the whole body. Open or pending base types do not seed the result, and other branch shapes still depend on the existing partial inference. A supported single local recursive gate also uses a monomorphic self reference while its body is checked, then generalizes variables free of its enclosing environment; captured variables remain shared. Acyclic local value definitions can refer forward. When the remaining local definitions stop making progress and no cyclic group applies, the earliest of them whose definite error no order of the siblings could change reports it; otherwise the generic message remains. A definite error names sites, except an uncertain type hole, which names its site but is unsupported. A sibling can change another's result through a type variable the locals share, such as one in an untyped sample of the enclosing gate: a sibling's cast of the sample to `!!` makes every cast of it fit. So the error of a local that names no sibling and nothing whose type has a shared variable always counts. Another local's error counts only if no sibling had bound or refined a shared variable when it was tried and every other waiting definition also failed with sites, since one that waits without them, on a checker limit, a pending tag or its own nested stall, might in another order constrain the shared variable. In that case every definition is inferred against the same state in every order. A definition that infers but is then rejected as unsupported, such as for an uncertain type hole or a capital forced to a concrete type, reports its own message. Errors found while a cyclic group is inferred together are dropped, so a mutual group whose error comes after the call to its partner keeps the generic message. The checker collects written capitals per `++` before inference, excluding nested definitions: a capital used in an enclosing definition is shared with its locals, even when written later, while a capital introduced only in a local definition is generalized there. Sibling locals can introduce independent capitals with the same spelling; generic mold parameters keep their own scope. Top-level groups of syntactic gates are inferred together with monomorphic placeholders and shared substitutions, then generalized only after the whole group checks; downstream uses and library interfaces instantiate those schemes independently. A dependency graph identifies groups with two iterative depth-first passes; its conservative local-reference edges can reject otherwise valid programs. Supported local mutually recursive gate groups also use shared monomorphic placeholders and generalize only after the group checks, preserving captured outer variables. Some proven non-gate value cycles are diagnosed; other mixed gate/value cycles, polymorphic recursion, unresolved literal constraints and unresolved branch joins remain unsupported. Acyclic simple local mold aliases can also refer forward, and are scoped to the body, not its gate's sample. Nonrecursive generic aliases of supported molds can be applied at exact arity, including locally and through library interfaces; their parameters are lexical. Closed, provably disjoint nonrecursive unions and tagged single-case molds support contextual term values, `~` and `|=%tag` constructors. Literal heads compare by their runtime noun, so `|=%$` can construct an explicit null-, loobean-zero- or term-zero-headed case. Equal heads with distinct payloads can be selected when exactly one payload fit is proven; unknown or ambiguous alternatives remain unsupported. Unresolved tags and nulls remain pending, with distinct partial-inference diagnostics. Nonrecursive top-level generic union molds with provably disjoint cases also support contextual tags and constructors at exact arity; their arguments are retained through generalization and supported library interfaces. Nonrecursive generic aliases can reorder, repeat or omit parameters while preserving a supported union’s origin, including through local scopes and library interfaces. Generic unions declared directly inside a body and recursive molds outside the source-proven slices described below remain unsupported. A directly known named union can instantiate an unconstrained generic gate sample while retaining its origin, generic arguments and faces. Unnamed, pending-tag, recursive, unknown-atom and variable-bound union origins remain unsupported. 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. A differing-variable face constraint remains unsupported. When inference forces two distinct explicitly written capitals equal, it reports both source sites; forcing a capital to a concrete type remains unsupported in this fragment. It can infer and generalize atom constraints arising from explicit capitals or bare sample binders, preserve those constraints through aliases, instantiate them independently, and print multiple constraints. Unresolved decimal variables default to `@ud` for inferred types without gates; defaulting inside gate types and other constraint cases remain incomplete. It does not yet check a module, complete imports, general patterns, general deferred constraints, recursive molds, dependency cycles or most errors with both conflicting excerpts. Definite cast and call mismatches, incompatible branches and overlapping union cases report both sites and excerpts. Concrete branch results can join at an explicitly present parent aura or `@`. Some known tuple and record positions acquire matching faces; other variable-dependent face merges, general branch tag context and ambiguous call-result propagation remain unsupported; function compatibility involving nested `@` and variable-dependent joins remain unsupported except for equal types and the source-bound gate-sample proof below. For a single recursive gate outside a group, the reporting path repeats inference rather than instantiating its generalized interface inside its own body; a group report uses its stored schemes. This adds work, and the current dependency pass can take quadratic time on long forward chains; the milestone's speed target remains unverified. A separate conservative pass reports unions whose cases are provably disjoint or overlapping and leaves other cases unresolved; it does not claim the mold is checked. Unsupported forms are reported as such, and the partial output says the module has not been checked.

6060

61+Uncontextual `?-` branches share one result join across loobean, unit, list and known-union folds. They first unify the arm types and retain the resulting substitution, including gate-free constraints. If unification fails, they widen only to an explicitly present parent aura or unrestricted `@`; sibling auras do not acquire a guessed common parent. Multi-arm union folds first unify as a group; if that fails, they select an explicitly present atom parent independently of arm order and bind variables to that final parent. Explicit `@` accepts atom singletons and restricted atom variables. Deferred boolean branches try the same join before their pending-literal fallback.

62+

6163A direct unshadowed prelude call can use checked source layouts when a positional argument is a directly named, already inferred root gate. For two-slot function samples, the checker can match a named update against an unnamed generic gate sample without confusing a binder face with a nested record face. Both explicitly named slots must agree; source boundaries are evidence for this fit, not a call-arity rule. The source gate and prelude annotation must be available from their checked bindings. Local or dynamic gates, aliases without direct evidence, recursive or SCC placeholder bodies, other sample shapes and unresolved call-sample variables remain unsupported by this proof. Ordinary inference remains the fallback.

6264

6365The checker retains a per-analysis index of finalized root gates and a prelude source table bound to the entire trusted prepared interface. A dependency screen avoids building the table when the root cannot use it; changing the interface invalidates it. The host remains responsible for supplying a prepared interface paired with its source. The matcher checks each slot and product in both directions with a shared substitution. Before returning its tentative proof it requires both complete call samples to normalize to closed, tag-free types, then repeats every slot check and requires the substitution and fresh-ID counter to remain unchanged. This keeps later argument or enclosing constraints from invalidating an earlier face check, and preserves pending constraints, capital checks and projection evidence. These scans and the bounded second proof add work; they do not establish a global linear-time bound.

@@ -224,7 +226,7 @@ An expected cell type can supply context to both arms of a loobean branch. This

224226

225227In an isolated diagnostic with the real todo API and reader inputs, this cell context allowed the original update body to infer when its result type was written explicitly and experimental source-defined text helpers were supplied. The unchanged island still needs those text helpers, an actual source-backed `program` and UI interface, context propagation across definitions, island-kind checking and watchability proof. This branch change itself provides no runtime implementation or watchability evidence.

226228

227−A deferred boolean branch must use both distinct literal loobean patterns. Its subject is unified with `?`; the arms are inferred in source order without contextual retry. Equal normalized arm types are retained directly. When both written arms are direct literals that each created their own unbound pending tag, the checker can instead retain two source-owned fit obligations to a shared, monomorphic result variable. A later definition may close that variable; replay uses the ordinary literal fit, requires a closed atomic target or a union of direct constant/cell cases, and rejects faced targets and faced union cases. It replays all edges under the final substitution without adding bindings or fresh IDs. This does not support deferred list literals, union-pattern reachability, arbitrary branch expressions or prepared-prelude/imported modules. It does not establish request watchability.

229+A deferred boolean branch must use both distinct literal loobean patterns. Its subject is unified with `?`; the arms are inferred in source order without contextual retry. The shared unification-first result join applies before the pending-literal fallback. When both written arms are direct literals that each created their own unbound pending tag, the checker can instead retain two source-owned fit obligations to a shared, monomorphic result variable. A later definition may close that variable; replay uses the ordinary literal fit, requires a closed atomic target or a union of direct constant/cell cases, and rejects faced targets and faced union cases. It replays all edges under the final substitution without adding bindings or fresh IDs. This does not support deferred list literals, union-pattern reachability, arbitrary branch expressions or prepared-prelude/imported modules. It does not establish request watchability.

228230

229231With the caller's unchanged prepared prelude, the partial report can also recover a narrow import-free, non-main ordinary library initializer. A direct tuple literal may retain one source-owned fit obligation for each newly created pending literal until a later exact result cast closes them. A separate bounded candidate screen admits a direct tuple even without a constructor call. The prepared transaction requires exact agreement among the supplied interface, value inventory and reserved molds, and retains the API, store, import and `main` exclusions. It only adds recovered entries to the partial report: the ordinary full-module resolver does not publish them. Wrong unit or draft fields, unrelated pending tags and mold-name collisions fail closed; without the later final cast, the initializer remains not checked. This does not add list-literal deferral or import-aware recovery.

230232

docs/status.md+4−2

@@ -61,6 +61,8 @@ Keyed programs no longer skip ordinary component inference: an annotated initial

6161

6262Imported Hoon `(unit T)` now converts to the validated canonical prelude `unit` when that template is supplied, instead of remaining an incompatible collection. Conversion recurses through imported unions and collections, and API path/diff/poke analysis uses the same prepared reader. The fixtures prove identity, `fall`, `need`, `(unit @t)` casts, union- and list-nested matching, canonical unit-typed API full/diff marks and a canonical direct-poke export while preserving the no-prelude compatibility report and wrong-collection rejection. Nested public re-export labels also remain `ask`, `qath` and `raw-poke` instead of leaking their private `.internal` suffixes into printed types.

6363

64+Uncontextual `?-` result joining now uses one rule for loobean, unit, list and known-union branches: unify and retain substitutions first, then widen only to an explicitly present parent aura or `@`. Multi-arm folds select an explicitly present parent independently of arm order and bind variables to that final parent; deferred boolean branches retain their pending-literal fallback, and sibling auras remain distinct without a present common parent. Valid recursive local branches that were rejected by the old per-kind screens now infer, while pending tags and distinct type variables retain definite diagnostics.

65+

6466The component-local program recovery now covers update, subscriptions, one direct keyed `each`/`turn` mapper and its view, then the existing initializer and ordinary `main` path. Each recovered scheme is closed and freshly allocated; non-gate views decline safely. Canonical `element` recursion and exact singleton-case list fits are narrowly guarded, with successful ordinary fits taking precedence. The byte-identical unchanged todo now passes both detailed and legacy full-module checks with an exact closed `main` type and structural downstream import. Wrong models, messages, results, mappers, keys, aliases, non-gate views and watches fail closed. This is static checking only: no Jibb execution or runtime watching is claimed.

6567

6668The API path analyzer can retain its source, complete prepared prelude, reader results and resolved dependencies as evidence, and classify a unique declaration as watchable, not watchable or unknown. This remains declaration evidence rather than proof about an arbitrary request value. The narrow direct-program check above composes it with final value syntax, resolved imports and merged evidence for one plain request. Prepared artifacts and reader results remain trusted host inputs.

@@ -117,8 +119,8 @@ What the plan asks for, and where it is:

117119

118120Besides the plan's list:

119121

120−- 660 golden cases: 440 that parse and 220 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.

121−- The 660-case corpus passed under `urbit eval` in 108.0 s while other checks were running. The fake ship passed all 717 tests, including the source-overlap, structural-overlap, generic-union source and alias-overlap, full-module overlap, deferred-context, generic-recursion, generic-construction, generic-pattern, deferred-inference, empty-mold and cell-branch fixtures, importer, importer/checker and mark/checker bridges, module scope, unification, hole, qath, ask, default-wrapper importer, projection, arithmetic, generic-alias, positional-face, API-evidence, request, closed-gate, todo API, constructor, sub, nested-union, gate-free and direct-gate guards and the unchanged todo report. Desk sync took 111.2 s and the ship's `-test` run took 316.7 s. The importer golden compares 221 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.

122+- 689 golden cases: 460 that parse and 229 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.

123+- The 689-case corpus passed under `urbit eval` in 107.0 s while other checks were running. The fake ship passed all 746 tests, including the source-overlap, structural-overlap, generic-union source and alias-overlap, full-module overlap, deferred-context, generic-recursion, generic-construction, generic-pattern, deferred-inference, empty-mold and cell-branch fixtures, importer, importer/checker and mark/checker bridges, module scope, unification, hole, qath, ask, default-wrapper importer, projection, arithmetic, generic-alias, positional-face, API-evidence, request, closed-gate, todo API, constructor, sub, nested-union, gate-free and direct-gate guards and the unchanged todo report. Desk sync took 111.2 s and the ship's `-test` run took 316.7 s. The importer golden compares 221 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.

122124- `tools/testdata/selftest` (22 checks), `tools/testdata/ship-selftest` and `tools/testdata/clay-fixtures-selftest` test the tools themselves; the last checks temporary Clay fixture cleanup and signal handling without a ship.

123125- 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.

124126- Speed: starting `urbit eval` and building the library takes about 27 s with the dev tools' `!:`, and 24 s without it (`tools/hoon --no-debug`). 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).

jibb-dev/lib/jibb.hoon+97−26

@@ -5131,10 +5131,84 @@

51315131 ?: (aura-prefix aura.a aura.b) `a

51325132 ?: (aura-prefix aura.b aura.a) `b

51335133 ~

5134− ?: &(?=(%any-atom -.a) |(?=(%atom -.b) ?=(%flag -.b))) `a

5135− ?: &(?=(%any-atom -.b) |(?=(%atom -.a) ?=(%flag -.a))) `b

5134+ ?: &(?=(%any-atom -.a) |(?=(%atom -.b) ?=(%flag -.b) ?=(%const -.b) ?=(%avar -.b) ?=(%rvar -.b) ?=(%nvar -.b) ?=(%rnvar -.b))) `a

5135+ ?: &(?=(%any-atom -.b) |(?=(%atom -.a) ?=(%flag -.a) ?=(%const -.a) ?=(%avar -.a) ?=(%rvar -.a) ?=(%nvar -.a) ?=(%rnvar -.a))) `b

51365136 ~

51375137::

5138+++ itype-branch-join

5139+ |= [a=itype b=itype sub=isub]

5140+ ^- (unit [typ=itype sub=isub])

5141+ =/ unified=(unit isub) (itype-unify a b sub)

5142+ ?^ unified `[(itype-normalize a u.unified) u.unified]

5143+ =/ common=(unit itype) (itype-concrete-join a b sub)

5144+ ?~ common ~

5145+ `[u.common sub]

5146+::

5147+++ itype-branch-join-with

5148+ |= [candidate=itype types=(list itype) sub=isub]

5149+ ^- (unit [typ=itype sub=isub])

5150+ ?~ types `[(itype-normalize candidate sub) sub]

5151+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join candidate i.types sub)

5152+ ?~ joined ~

5153+ $(candidate typ.u.joined, types t.types, sub sub.u.joined)

5154+::

5155+++ itype-branch-unify-list

5156+ |= [types=(list itype) sub=isub]

5157+ ^- (unit [typ=itype sub=isub])

5158+ ?~ types ~

5159+ =/ candidate=itype i.types

5160+ =/ rest=(list itype) t.types

5161+ |-

5162+ ?~ rest `[(itype-normalize candidate sub) sub]

5163+ =/ unified=(unit isub) (itype-unify candidate i.rest sub)

5164+ ?~ unified ~

5165+ $(candidate (itype-normalize candidate u.unified), rest t.rest, sub u.unified)

5166+::

5167+++ itype-branch-any-atom

5168+ |= [types=(list itype) sub=isub]

5169+ ^- (unit itype)

5170+ ?~ types ~

5171+ =/ typ=itype (itype-walk i.types sub)

5172+ ?: ?=(%any-atom -.typ) `typ

5173+ $(types t.types)

5174+::

5175+++ itype-branch-atom-parent

5176+ |= [candidate=itype types=(list itype) sub=isub]

5177+ ^- (unit itype)

5178+ ?~ types `candidate

5179+ =/ typ=itype (itype-walk i.types sub)

5180+ ?. ?=(%atom -.typ) $(types t.types)

5181+ =/ joined=(unit itype) (itype-concrete-join candidate typ sub)

5182+ ?~ joined ~

5183+ $(candidate u.joined, types t.types)

5184+::

5185+++ itype-branch-atom-candidates

5186+ |= [candidates=(list itype) types=(list itype) sub=isub]

5187+ ^- (unit itype)

5188+ ?~ candidates ~

5189+ =/ candidate=itype (itype-walk i.candidates sub)

5190+ ?. ?=(%atom -.candidate) $(candidates t.candidates)

5191+ =/ parent=(unit itype) (itype-branch-atom-parent candidate types sub)

5192+ ?^ parent parent

5193+ $(candidates t.candidates)

5194+::

5195+++ itype-branch-parent

5196+ |= [types=(list itype) sub=isub]

5197+ ^- (unit itype)

5198+ =/ unrestricted=(unit itype) (itype-branch-any-atom types sub)

5199+ ?^ unrestricted unrestricted

5200+ (itype-branch-atom-candidates types types sub)

5201+::

5202+++ itype-branch-join-list

5203+ |= [types=(list itype) sub=isub]

5204+ ^- (unit [typ=itype sub=isub])

5205+ ?~ types ~

5206+ =/ unified=(unit [typ=itype sub=isub]) (itype-branch-unify-list types sub)

5207+ ?^ unified unified

5208+ =/ parent=(unit itype) (itype-branch-parent types sub)

5209+ ?~ parent ~

5210+ (itype-branch-join-with u.parent types sub)

5211+::

51385212:: Unifying an already-bound tuple with a faced position would need to

51395213:: update the bound type. Until substitutions can retain that information,

51405214:: variable-dependent face merges stay unresolved.

@@ -7952,9 +8026,9 @@

79528026 (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)

79538027 ?: ?=(%| -.right) right

79548028 ?^ expected [%& typ.u.expected state.p.right]

7955− =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)

8029+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join typ.p.left typ.p.right sub.state.p.right)

79568030 ?~ joined [%| ["list branch results need unsupported inference" ~]]

7957− [%& typ.p.left state.p.right(sub u.joined)]

8031+ [%& typ.u.joined state.p.right(sub sub.u.joined)]

79588032::

79598033++ infer-unit-branch

79608034 |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]

@@ -7996,9 +8070,9 @@

79968070 (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)

79978071 ?: ?=(%| -.right) right

79988072 ?^ expected [%& typ.u.expected state.p.right]

7999− =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)

8073+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join typ.p.left typ.p.right sub.state.p.right)

80008074 ?~ joined [%| ["unit branch results need unsupported inference" ~]]

8001− [%& typ.p.left state.p.right(sub u.joined)]

8075+ [%& typ.u.joined state.p.right(sub sub.u.joined)]

80028076::

80038077:: Infer pieces in order, retaining their substitutions and pending tags.

80048078:: A bare decimal literal has no outside type constraint, so it takes its

@@ -8144,13 +8218,14 @@

81448218 =/ remaining=(list itype) cases

81458219 =/ arms=(list arm) arms.e

81468220 =/ st=istate state.p.subject

8147− =/ answer=(unit itype) ~

8221+ =/ results=(list itype) ~

81488222 |-

81498223 ?~ arms

81508224 ?^ remaining

81518225 `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]

8152− ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]

8153− `[%& u.answer st]

8226+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join-list (flop results) sub.st)

8227+ ?~ joined `[%| ["union branch result matching needs unsupported inference" ~]]

8228+ `[%& typ.u.joined st(sub sub.u.joined)]

81548229 =/ a=arm i.arms

81558230 ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))

81568231 ~

@@ -8166,9 +8241,7 @@

81668241 =/ body=iresult (infer-fragment val.a u.bound st)

81678242 ?: ?=(%| -.body) `body

81688243 =/ result=itype (itype-normalize typ.p.body sub.state.p.body)

8169− =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))

8170− ?: mismatch `[%| ["union branch result matching needs unsupported inference" ~]]

8171− $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, answer `result)

8244+ $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, results [result results])

81728245::

81738246++ infer-known-union-context-whole

81748247 |= [e=expr expected=itype env=ienv subject=iresult context=span]

@@ -8231,14 +8304,16 @@

82318304 =/ remaining=(list ifinite) cases

82328305 =/ arms=(list arm) arms.e

82338306 =/ st=istate state.p.subject

8234− =/ answer=(unit itype) ~

8307+ =/ results=(list itype) ~

82358308 |-

82368309 ?~ arms

82378310 ?^ remaining

82388311 [%| ["missing union case {(show-itype part.i.remaining sub.st)}" ~]]

8239− ?~ answer [%| ["empty union branch is not supported by partial inference" ~]]

8240− ?~ expected [%& u.answer st]

8241− [%& typ.u.expected st]

8312+ ?~ results [%| ["empty union branch is not supported by partial inference" ~]]

8313+ ?^ expected [%& typ.u.expected st]

8314+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join-list (flop results) sub.st)

8315+ ?~ joined [%| ["union branch result matching needs unsupported inference" ~]]

8316+ [%& typ.u.joined st(sub sub.u.joined)]

82428317 =/ a=arm i.arms

82438318 ?: (lien remaining |=(c=ifinite =(%unknown (union-pattern pat.a part.c))))

82448319 [%| ["partial union pattern is not supported by partial inference" ~]]

@@ -8266,11 +8341,9 @@

82668341 [%| ["union branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.a) "branch arm"]]]]

82678342 ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))

82688343 [%| ["union branch result needs context in partial inference" ~]]

8269− $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body(sub sub.fit, next next.fit), answer `typ.u.expected)

8344+ $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body(sub sub.fit, next next.fit), results [typ.p.body results])

82708345 =/ result=itype (itype-normalize typ.p.body sub.state.p.body)

8271− =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))

8272− ?: mismatch [%| ["union branch result matching needs unsupported inference" ~]]

8273− $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body, answer `result)

8346+ $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body, results [result results])

82748347::

82758348:: Prove a one-arm record pattern covers a known, non-union subject.

82768349:: Variable or partial matches stay unsupported; binding uses the same

@@ -8843,22 +8916,18 @@

88438916 ?: ?=(%| -.right) right

88448917 =/ ltype=itype (itype-normalize typ.p.left sub.state.p.right)

88458918 =/ rtype=itype (itype-normalize typ.p.right sub.state.p.right)

8846− ?: &(!=(ltype rtype) |(?=(^ (itype-vars ltype)) ?=(^ (itype-vars rtype))) |((itype-has-fixed-atom ltype) (itype-has-fixed-atom rtype)))

8847− [%| ["branch widening is not supported by partial inference" ~]]

8848− =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)

8919+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join typ.p.left typ.p.right sub.state.p.right)

88498920 ?~ joined

88508921 ?: |((itype-has-recursive ltype) (itype-has-recursive rtype))

88518922 [%| ["recursive branch matching is not supported by partial inference" ~]]

88528923 ?: |((itype-has-tag ltype) (itype-has-tag rtype) (itype-has-union ltype) (itype-has-union rtype))

88538924 [%| ["branch tag or union context is not supported by partial inference" ~]]

8854− =/ common=(unit itype) (itype-concrete-join typ.p.left typ.p.right sub.state.p.right)

8855− ?^ common [%& u.common state.p.right]

88568925 ?: |((itype-has-face typ.p.left sub.state.p.right) (itype-has-face typ.p.right sub.state.p.right))

88578926 [%| ["record branch matching is not supported by partial inference" ~]]

88588927 ?: |((itype-has-any-atom typ.p.left sub.state.p.right) (itype-has-any-atom typ.p.right sub.state.p.right) (itype-family-related typ.p.left typ.p.right sub.state.p.right))

88598928 [%| ["branch widening is not supported by partial inference" ~]]

88608929 [%| ["branch arms have incompatible types" ~[[(span-of val.x) (site-type-note "first arm" typ.p.left sub.state.p.right)] [(span-of val.y) (site-type-note "second arm" typ.p.right sub.state.p.right)]]]]

8861− [%& typ.p.left state.p.right(sub u.joined)]

8930+ [%& typ.u.joined state.p.right(sub sub.u.joined)]

88628931 %cast

88638932 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)

88648933 ?~ target

@@ -15293,6 +15362,8 @@

1529315362 ?: ?=(%| -.left) left

1529415363 =/ right=iresult (infer-fragment val.y env state.p.left)

1529515364 ?: ?=(%| -.right) right

15365+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join typ.p.left typ.p.right sub.state.p.right)

15366+ ?^ joined [%& typ.u.joined state.p.right(sub sub.u.joined)]

1529615367 ?. (dg-stable-fit typ.p.left typ.p.right sub.state.p.right)

1529715368 =/ st=istate state.p.right

1529815369 ?. (dg-owned-arm-literal val.x typ.p.left tags.st sub.st next.state)

tests/golden/types-cell-branch-context/types.txt+1−1

@@ -7,5 +7,5 @@ partial inference; module not checked

77++ named: $-(? [name=@t place=(unit @t)])

88++ wrong: branch tag or union context is not supported by partial inference

99++ different: branch tag or union context is not supported by partial inference

10−++ open: branch widening is not supported by partial inference

10+++ open: branch tag or union context is not supported by partial inference

1111++ waiting: branch tag or union context is not supported by partial inference

tests/golden/types-list-patterns/about.txt+1−1

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

11source: Grammar, Patterns: "Every case needs an arm or a catch-all"; "A name in a pattern always binds anew". Modules: no name may shadow an in-scope name.

2−tests: Both orders of an exhaustive list branch bind the head and tail with their respective types; unsupported subjects or patterns, conflicting binders, and unrelated unresolved tags fail closed; a nonempty arm of `(list !!)` is unreachable.

2+tests: Both orders of an exhaustive list branch bind the head and tail with their respective types; uncontextual results unify and then widen to an explicitly present parent aura; unsupported subjects or patterns, conflicting binders, and unrelated unresolved tags fail closed; a nonempty arm of `(list !!)` is unreachable.

33expect: parses

44expect-types: a partial inference report

tests/golden/types-list-patterns/source.jibb+4

@@ -9,6 +9,10 @@

99 ?- xs

1010 [item rest] rest

1111 ~ !!

12+++ parent |= xs=(list @t)

13+ ?- xs

14+ ~ 0x1f

15+ [item rest] ^- @u 0x1f

1216++ with-context |= xs=(list @t)

1317 ^- msg

1418 ?- xs

tests/golden/types-list-patterns/tokens.txt+241−215

@@ -60,69 +60,71 @@

606012:1 DEDENT

616112:1 NEWLINE

626212:1 glyph ++

63−12:4 name with-context

64−12:17 glyph |=

65−12:20 name xs

66−12:22 tight glyph =

67−12:23 tight glyph (

68−12:24 tight name list

69−12:29 aura @t

70−12:31 tight glyph )

63+12:4 name parent

64+12:11 glyph |=

65+12:14 name xs

66+12:16 tight glyph =

67+12:17 tight glyph (

68+12:18 tight name list

69+12:23 aura @t

70+12:25 tight glyph )

717113:3 INDENT

72−13:3 glyph ^-

73−13:6 name msg

72+13:3 glyph ?-

73+13:6 name xs

747414:5 INDENT

75−14:5 glyph ?-

76−14:8 name xs

77−15:7 INDENT

78−15:7 lit ~

79−15:9 lit %empty

80−16:7 NEWLINE

81−16:7 glyph [

82−16:8 tight name item

83−16:13 name rest

84−16:17 tight glyph ]

85−16:19 glyph [

86−16:20 tight lit %item

87−16:26 name item

88−16:30 tight glyph ]

89−17:1 DEDENT

90−17:1 DEDENT

91−17:1 DEDENT

92−17:1 NEWLINE

93−17:1 glyph ++

94−17:4 name shadow

95−17:11 glyph |=

96−17:14 name xs

97−17:16 tight glyph =

98−17:17 tight glyph (

99−17:18 tight name list

100−17:23 aura @t

101−17:25 tight glyph )

102−18:3 INDENT

103−18:3 glyph ?-

104−18:6 name xs

105−19:5 INDENT

106−19:5 lit ~

107−19:7 glyph !!

108−20:5 NEWLINE

109−20:5 glyph [

110−20:6 tight name xs

111−20:9 name rest

112−20:13 tight glyph ]

113−20:15 name xs

75+14:5 lit ~

76+14:7 lit 0x1f

77+15:5 NEWLINE

78+15:5 glyph [

79+15:6 tight name item

80+15:11 name rest

81+15:15 tight glyph ]

82+15:17 glyph ^-

83+15:20 aura @u

84+15:23 lit 0x1f

85+16:1 DEDENT

86+16:1 DEDENT

87+16:1 NEWLINE

88+16:1 glyph ++

89+16:4 name with-context

90+16:17 glyph |=

91+16:20 name xs

92+16:22 tight glyph =

93+16:23 tight glyph (

94+16:24 tight name list

95+16:29 aura @t

96+16:31 tight glyph )

97+17:3 INDENT

98+17:3 glyph ^-

99+17:6 name msg

100+18:5 INDENT

101+18:5 glyph ?-

102+18:8 name xs

103+19:7 INDENT

104+19:7 lit ~

105+19:9 lit %empty

106+20:7 NEWLINE

107+20:7 glyph [

108+20:8 tight name item

109+20:13 name rest

110+20:17 tight glyph ]

111+20:19 glyph [

112+20:20 tight lit %item

113+20:26 name item

114+20:30 tight glyph ]

115+21:1 DEDENT

11411621:1 DEDENT

11511721:1 DEDENT

11611821:1 NEWLINE

11711921:1 glyph ++

118−21:4 name duplicate

119−21:14 glyph |=

120−21:17 name xs

121−21:19 tight glyph =

122−21:20 tight glyph (

123−21:21 tight name list

124−21:26 aura @t

125−21:28 tight glyph )

120+21:4 name shadow

121+21:11 glyph |=

122+21:14 name xs

123+21:16 tight glyph =

124+21:17 tight glyph (

125+21:18 tight name list

126+21:23 aura @t

127+21:25 tight glyph )

12612822:3 INDENT

12712922:3 glyph ?-

12813022:6 name xs

@@ -131,17 +133,22 @@

13113323:7 glyph !!

13213424:5 NEWLINE

13313524:5 glyph [

134−24:6 tight name item

135−24:11 name item

136−24:15 tight glyph ]

137−24:17 name item

136+24:6 tight name xs

137+24:9 name rest

138+24:13 tight glyph ]

139+24:15 name xs

13814025:1 DEDENT

13914125:1 DEDENT

14014225:1 NEWLINE

14114325:1 glyph ++

142−25:4 name unknown

143−25:12 glyph |=

144−25:15 name xs

144+25:4 name duplicate

145+25:14 glyph |=

146+25:17 name xs

147+25:19 tight glyph =

148+25:20 tight glyph (

149+25:21 tight name list

150+25:26 aura @t

151+25:28 tight glyph )

14515226:3 INDENT

14615326:3 glyph ?-

14715426:6 name xs

@@ -151,18 +158,16 @@

15115828:5 NEWLINE

15215928:5 glyph [

15316028:6 tight name item

154−28:11 name rest

161+28:11 name item

15516228:15 tight glyph ]

15616328:17 name item

15716429:1 DEDENT

15816529:1 DEDENT

15916629:1 NEWLINE

16016729:1 glyph ++

161−29:4 name not-list

162−29:13 glyph |=

163−29:16 name xs

164−29:18 tight glyph =

165−29:19 tight aura @t

168+29:4 name unknown

169+29:12 glyph |=

170+29:15 name xs

16617130:3 INDENT

16717230:3 glyph ?-

16817330:6 name xs

@@ -179,181 +184,202 @@

17918433:1 DEDENT

18018533:1 NEWLINE

18118633:1 glyph ++

182−33:4 name missing

183−33:12 glyph |=

184−33:15 name xs

185−33:17 tight glyph =

186−33:18 tight glyph (

187−33:19 tight name list

188−33:24 aura @t

189−33:26 tight glyph )

187+33:4 name not-list

188+33:13 glyph |=

189+33:16 name xs

190+33:18 tight glyph =

191+33:19 tight aura @t

19019234:3 INDENT

19119334:3 glyph ?-

19219434:6 name xs

19319535:5 INDENT

19419635:5 lit ~

19519735:7 glyph !!

196−36:1 DEDENT

197−36:1 DEDENT

198−36:1 NEWLINE

199−36:1 glyph ++

200−36:4 name invalid

201−36:12 glyph |=

202−36:15 name xs

203−36:17 tight glyph =

204−36:18 tight glyph (

205−36:19 tight name list

206−36:24 aura @t

207−36:26 tight glyph )

208−37:3 INDENT

209−37:3 glyph ?-

210−37:6 name xs

211−38:5 INDENT

212−38:5 lit ~

213−38:7 glyph !!

214−39:5 NEWLINE

215−39:5 glyph [

216−39:6 tight lit %tag

217−39:11 name rest

218−39:15 tight glyph ]

219−39:17 name rest

198+36:5 NEWLINE

199+36:5 glyph [

200+36:6 tight name item

201+36:11 name rest

202+36:15 tight glyph ]

203+36:17 name item

204+37:1 DEDENT

205+37:1 DEDENT

206+37:1 NEWLINE

207+37:1 glyph ++

208+37:4 name missing

209+37:12 glyph |=

210+37:15 name xs

211+37:17 tight glyph =

212+37:18 tight glyph (

213+37:19 tight name list

214+37:24 aura @t

215+37:26 tight glyph )

216+38:3 INDENT

217+38:3 glyph ?-

218+38:6 name xs

219+39:5 INDENT

220+39:5 lit ~

221+39:7 glyph !!

22022240:1 DEDENT

22122340:1 DEDENT

22222440:1 NEWLINE

22322540:1 glyph ++

224−40:4 name unresolved

225−40:15 glyph |=

226−40:18 name xs

227−40:20 tight glyph =

228−40:21 tight glyph (

229−40:22 tight name list

230−40:27 aura @t

231−40:29 tight glyph )

226+40:4 name invalid

227+40:12 glyph |=

228+40:15 name xs

229+40:17 tight glyph =

230+40:18 tight glyph (

231+40:19 tight name list

232+40:24 aura @t

233+40:26 tight glyph )

23223441:3 INDENT

23323541:3 glyph ?-

23423641:6 name xs

23523742:5 INDENT

23623842:5 lit ~

237−42:7 lit %empty

239+42:7 glyph !!

23824043:5 NEWLINE

23924143:5 glyph [

240−43:6 tight name item

242+43:6 tight lit %tag

24124343:11 name rest

24224443:15 tight glyph ]

243−43:17 lit %more

245+43:17 name rest

24424644:1 DEDENT

24524744:1 DEDENT

24624844:1 NEWLINE

24724944:1 glyph ++

248−44:4 name duplicate-arm

249−44:18 glyph |=

250−44:21 name xs

251−44:23 tight glyph =

252−44:24 tight glyph (

253−44:25 tight name list

254−44:30 aura @t

255−44:32 tight glyph )

250+44:4 name unresolved

251+44:15 glyph |=

252+44:18 name xs

253+44:20 tight glyph =

254+44:21 tight glyph (

255+44:22 tight name list

256+44:27 aura @t

257+44:29 tight glyph )

25625845:3 INDENT

25725945:3 glyph ?-

25826045:6 name xs

25926146:5 INDENT

26026246:5 lit ~

261−46:7 glyph !!

263+46:7 lit %empty

26226447:5 NEWLINE

263−47:5 lit ~

264−47:7 glyph !!

265−48:5 NEWLINE

266−48:5 glyph [

267−48:6 tight name item

268−48:11 name rest

269−48:15 tight glyph ]

270−48:17 name item

271−49:1 DEDENT

272−49:1 DEDENT

273−49:1 NEWLINE

274−49:1 glyph ++

275−49:4 name unrelated

276−49:14 glyph |=

277−49:17 name xs

278−49:19 tight glyph =

279−49:20 tight glyph (

280−49:21 tight name list

281−49:26 aura @t

282−49:28 tight glyph )

283−50:3 INDENT

284−50:3 glyph ~&

285−50:6 lit %pending

286−51:5 INDENT

287−51:5 glyph ?-

288−51:8 name xs

289−52:7 INDENT

290−52:7 lit ~

291−52:9 glyph !!

292−53:7 NEWLINE

293−53:7 glyph [

294−53:8 tight name item

295−53:13 name rest

296−53:17 tight glyph ]

297−53:19 name item

298−54:1 DEDENT

299−54:1 DEDENT

300−54:1 DEDENT

301−54:1 NEWLINE

302−54:1 glyph ++

303−54:4 name empty-elements

304−54:19 glyph |=

305−54:22 name xs

306−54:24 tight glyph =

307−54:25 tight glyph (

308−54:26 tight name list

309−54:31 glyph !!

310−54:33 tight glyph )

311−55:3 INDENT

312−55:3 glyph ?-

313−55:6 name xs

314−56:5 INDENT

315−56:5 lit ~

316−56:7 glyph !!

317−57:5 NEWLINE

318−57:5 glyph [

319−57:6 tight name item

320−57:11 name rest

321−57:15 tight glyph ]

322−57:17 name item

265+47:5 glyph [

266+47:6 tight name item

267+47:11 name rest

268+47:15 tight glyph ]

269+47:17 lit %more

270+48:1 DEDENT

271+48:1 DEDENT

272+48:1 NEWLINE

273+48:1 glyph ++

274+48:4 name duplicate-arm

275+48:18 glyph |=

276+48:21 name xs

277+48:23 tight glyph =

278+48:24 tight glyph (

279+48:25 tight name list

280+48:30 aura @t

281+48:32 tight glyph )

282+49:3 INDENT

283+49:3 glyph ?-

284+49:6 name xs

285+50:5 INDENT

286+50:5 lit ~

287+50:7 glyph !!

288+51:5 NEWLINE

289+51:5 lit ~

290+51:7 glyph !!

291+52:5 NEWLINE

292+52:5 glyph [

293+52:6 tight name item

294+52:11 name rest

295+52:15 tight glyph ]

296+52:17 name item

297+53:1 DEDENT

298+53:1 DEDENT

299+53:1 NEWLINE

300+53:1 glyph ++

301+53:4 name unrelated

302+53:14 glyph |=

303+53:17 name xs

304+53:19 tight glyph =

305+53:20 tight glyph (

306+53:21 tight name list

307+53:26 aura @t

308+53:28 tight glyph )

309+54:3 INDENT

310+54:3 glyph ~&

311+54:6 lit %pending

312+55:5 INDENT

313+55:5 glyph ?-

314+55:8 name xs

315+56:7 INDENT

316+56:7 lit ~

317+56:9 glyph !!

318+57:7 NEWLINE

319+57:7 glyph [

320+57:8 tight name item

321+57:13 name rest

322+57:17 tight glyph ]

323+57:19 name item

324+58:1 DEDENT

32332558:1 DEDENT

32432658:1 DEDENT

32532758:1 NEWLINE

326−58:1 glyph +$

327−58:4 name maybe

328+58:1 glyph ++

329+58:4 name empty-elements

330+58:19 glyph |=

331+58:22 name xs

332+58:24 tight glyph =

333+58:25 tight glyph (

334+58:26 tight name list

335+58:31 glyph !!

336+58:33 tight glyph )

32833759:3 INDENT

329−59:3 lit ~

330−60:3 NEWLINE

331−60:3 glyph [

332−60:4 tight lit ~

333−60:6 name value

334−60:11 tight glyph =

335−60:12 tight aura @t

336−60:14 tight glyph ]

337−61:1 DEDENT

338−61:1 NEWLINE

339−61:1 glyph ++

340−61:4 name unit-shape

341−61:15 glyph |=

342−61:18 name xs

343−61:20 tight glyph =

344−61:21 tight name maybe

345−62:3 INDENT

346−62:3 glyph ?-

347−62:6 name xs

348−63:5 INDENT

349−63:5 lit ~

350−63:7 glyph !!

351−64:5 NEWLINE

352−64:5 glyph [

353−64:6 tight name item

354−64:11 name rest

355−64:15 tight glyph ]

356−64:17 name item

357−64:21 DEDENT

358−64:21 DEDENT

359−64:21 NEWLINE

338+59:3 glyph ?-

339+59:6 name xs

340+60:5 INDENT

341+60:5 lit ~

342+60:7 glyph !!

343+61:5 NEWLINE

344+61:5 glyph [

345+61:6 tight name item

346+61:11 name rest

347+61:15 tight glyph ]

348+61:17 name item

349+62:1 DEDENT

350+62:1 DEDENT

351+62:1 NEWLINE

352+62:1 glyph +$

353+62:4 name maybe

354+63:3 INDENT

355+63:3 lit ~

356+64:3 NEWLINE

357+64:3 glyph [

358+64:4 tight lit ~

359+64:6 name value

360+64:11 tight glyph =

361+64:12 tight aura @t

362+64:14 tight glyph ]

363+65:1 DEDENT

364+65:1 NEWLINE

365+65:1 glyph ++

366+65:4 name unit-shape

367+65:15 glyph |=

368+65:18 name xs

369+65:20 tight glyph =

370+65:21 tight name maybe

371+66:3 INDENT

372+66:3 glyph ?-

373+66:6 name xs

374+67:5 INDENT

375+67:5 lit ~

376+67:7 glyph !!

377+68:5 NEWLINE

378+68:5 glyph [

379+68:6 tight name item

380+68:11 name rest

381+68:15 tight glyph ]

382+68:17 name item

383+68:21 DEDENT

384+68:21 DEDENT

385+68:21 NEWLINE

tests/golden/types-list-patterns/tree.txt+121−110

@@ -27,55 +27,56 @@

2727 (cell 10:5 (bind 10:6 item) (bind 10:11 rest))

2828 (wing 10:17 rest))

2929 (arm 11:5 (lit 11:5 ~) (crash 11:7))))))

30− (value 12:1 with-context

31− (gate 12:17

32− (face 12:20 xs

33− (apply 12:23 list (aura 12:29 @t)))

30+ (value 12:1 parent

31+ (gate 12:11

32+ (face 12:14 xs

33+ (apply 12:17 list (aura 12:23 @t)))

3434 (body 13:3

35− (cast 13:3

36− (ref 13:6 msg)

37− (body 14:5

38− (branch 14:5

39− (wing 14:8 xs)

40− (arm 15:7 (lit 15:7 ~) (lit 15:9 %empty))

41− (arm 16:7

42− (cell 16:7 (bind 16:8 item) (bind 16:13 rest))

43− (tuple 16:19 (lit 16:20 %item) (wing 16:26 item)))))))))

44− (value 17:1 shadow

45− (gate 17:11

46− (face 17:14 xs

47− (apply 17:17 list (aura 17:23 @t)))

48− (body 18:3

49− (branch 18:3

50− (wing 18:6 xs)

51− (arm 19:5 (lit 19:5 ~) (crash 19:7))

52− (arm 20:5

53− (cell 20:5 (bind 20:6 xs) (bind 20:9 rest))

54− (wing 20:15 xs))))))

55− (value 21:1 duplicate

56− (gate 21:14

57− (face 21:17 xs

58− (apply 21:20 list (aura 21:26 @t)))

35+ (branch 13:3

36+ (wing 13:6 xs)

37+ (arm 14:5 (lit 14:5 ~) (lit 14:7 0x1f))

38+ (arm 15:5

39+ (cell 15:5 (bind 15:6 item) (bind 15:11 rest))

40+ (cast 15:17 (aura 15:20 @u) (lit 15:23 0x1f)))))))

41+ (value 16:1 with-context

42+ (gate 16:17

43+ (face 16:20 xs

44+ (apply 16:23 list (aura 16:29 @t)))

45+ (body 17:3

46+ (cast 17:3

47+ (ref 17:6 msg)

48+ (body 18:5

49+ (branch 18:5

50+ (wing 18:8 xs)

51+ (arm 19:7 (lit 19:7 ~) (lit 19:9 %empty))

52+ (arm 20:7

53+ (cell 20:7 (bind 20:8 item) (bind 20:13 rest))

54+ (tuple 20:19 (lit 20:20 %item) (wing 20:26 item)))))))))

55+ (value 21:1 shadow

56+ (gate 21:11

57+ (face 21:14 xs

58+ (apply 21:17 list (aura 21:23 @t)))

5959 (body 22:3

6060 (branch 22:3

6161 (wing 22:6 xs)

6262 (arm 23:5 (lit 23:5 ~) (crash 23:7))

6363 (arm 24:5

64− (cell 24:5 (bind 24:6 item) (bind 24:11 item))

65− (wing 24:17 item))))))

66− (value 25:1 unknown

67− (gate 25:12

68− (bind 25:15 xs)

64+ (cell 24:5 (bind 24:6 xs) (bind 24:9 rest))

65+ (wing 24:15 xs))))))

66+ (value 25:1 duplicate

67+ (gate 25:14

68+ (face 25:17 xs

69+ (apply 25:20 list (aura 25:26 @t)))

6970 (body 26:3

7071 (branch 26:3

7172 (wing 26:6 xs)

7273 (arm 27:5 (lit 27:5 ~) (crash 27:7))

7374 (arm 28:5

74− (cell 28:5 (bind 28:6 item) (bind 28:11 rest))

75+ (cell 28:5 (bind 28:6 item) (bind 28:11 item))

7576 (wing 28:17 item))))))

76− (value 29:1 not-list

77− (gate 29:13

78− (face 29:16 xs (aura 29:19 @t))

77+ (value 29:1 unknown

78+ (gate 29:12

79+ (bind 29:15 xs)

7980 (body 30:3

8081 (branch 30:3

8182 (wing 30:6 xs)

@@ -83,86 +84,96 @@

8384 (arm 32:5

8485 (cell 32:5 (bind 32:6 item) (bind 32:11 rest))

8586 (wing 32:17 item))))))

86− (value 33:1 missing

87− (gate 33:12

88− (face 33:15 xs

89− (apply 33:18 list (aura 33:24 @t)))

87+ (value 33:1 not-list

88+ (gate 33:13

89+ (face 33:16 xs (aura 33:19 @t))

9090 (body 34:3

9191 (branch 34:3

9292 (wing 34:6 xs)

93− (arm 35:5 (lit 35:5 ~) (crash 35:7))))))

94− (value 36:1 invalid

95− (gate 36:12

96− (face 36:15 xs

97− (apply 36:18 list (aura 36:24 @t)))

98− (body 37:3

99− (branch 37:3

100− (wing 37:6 xs)

101− (arm 38:5 (lit 38:5 ~) (crash 38:7))

102− (arm 39:5

103− (cell 39:5 (lit 39:6 %tag) (bind 39:11 rest))

104− (wing 39:17 rest))))))

105− (value 40:1 unresolved

106− (gate 40:15

107− (face 40:18 xs

108− (apply 40:21 list (aura 40:27 @t)))

93+ (arm 35:5 (lit 35:5 ~) (crash 35:7))

94+ (arm 36:5

95+ (cell 36:5 (bind 36:6 item) (bind 36:11 rest))

96+ (wing 36:17 item))))))

97+ (value 37:1 missing

98+ (gate 37:12

99+ (face 37:15 xs

100+ (apply 37:18 list (aura 37:24 @t)))

101+ (body 38:3

102+ (branch 38:3

103+ (wing 38:6 xs)

104+ (arm 39:5 (lit 39:5 ~) (crash 39:7))))))

105+ (value 40:1 invalid

106+ (gate 40:12

107+ (face 40:15 xs

108+ (apply 40:18 list (aura 40:24 @t)))

109109 (body 41:3

110110 (branch 41:3

111111 (wing 41:6 xs)

112− (arm 42:5 (lit 42:5 ~) (lit 42:7 %empty))

112+ (arm 42:5 (lit 42:5 ~) (crash 42:7))

113113 (arm 43:5

114− (cell 43:5 (bind 43:6 item) (bind 43:11 rest))

115− (lit 43:17 %more))))))

116− (value 44:1 duplicate-arm

117− (gate 44:18

118− (face 44:21 xs

119− (apply 44:24 list (aura 44:30 @t)))

114+ (cell 43:5 (lit 43:6 %tag) (bind 43:11 rest))

115+ (wing 43:17 rest))))))

116+ (value 44:1 unresolved

117+ (gate 44:15

118+ (face 44:18 xs

119+ (apply 44:21 list (aura 44:27 @t)))

120120 (body 45:3

121121 (branch 45:3

122122 (wing 45:6 xs)

123− (arm 46:5 (lit 46:5 ~) (crash 46:7))

124− (arm 47:5 (lit 47:5 ~) (crash 47:7))

125− (arm 48:5

126− (cell 48:5 (bind 48:6 item) (bind 48:11 rest))

127− (wing 48:17 item))))))

128− (value 49:1 unrelated

129− (gate 49:14

130− (face 49:17 xs

131− (apply 49:20 list (aura 49:26 @t)))

132− (body 50:3

133− (trace 50:3

134− (lit 50:6 %pending)

135− (body 51:5

136− (branch 51:5

137− (wing 51:8 xs)

138− (arm 52:7 (lit 52:7 ~) (crash 52:9))

139− (arm 53:7

140− (cell 53:7 (bind 53:8 item) (bind 53:13 rest))

141− (wing 53:19 item))))))))

142− (value 54:1 empty-elements

143− (gate 54:19

144− (face 54:22 xs

145− (apply 54:25 list (void 54:31)))

146− (body 55:3

147− (branch 55:3

148− (wing 55:6 xs)

149− (arm 56:5 (lit 56:5 ~) (crash 56:7))

150− (arm 57:5

151− (cell 57:5 (bind 57:6 item) (bind 57:11 rest))

152− (wing 57:17 item))))))

153− (mold 58:1 maybe

154− (union 59:3

155− (const 59:3 ~)

156− (cell 60:3

157− (const 60:4 ~)

158− (face 60:6 value (aura 60:12 @t)))))

159− (value 61:1 unit-shape

160− (gate 61:15

161− (face 61:18 xs (ref 61:21 maybe))

162− (body 62:3

163− (branch 62:3

164− (wing 62:6 xs)

165− (arm 63:5 (lit 63:5 ~) (crash 63:7))

166− (arm 64:5

167− (cell 64:5 (bind 64:6 item) (bind 64:11 rest))

168− (wing 64:17 item)))))))

123+ (arm 46:5 (lit 46:5 ~) (lit 46:7 %empty))

124+ (arm 47:5

125+ (cell 47:5 (bind 47:6 item) (bind 47:11 rest))

126+ (lit 47:17 %more))))))

127+ (value 48:1 duplicate-arm

128+ (gate 48:18

129+ (face 48:21 xs

130+ (apply 48:24 list (aura 48:30 @t)))

131+ (body 49:3

132+ (branch 49:3

133+ (wing 49:6 xs)

134+ (arm 50:5 (lit 50:5 ~) (crash 50:7))

135+ (arm 51:5 (lit 51:5 ~) (crash 51:7))

136+ (arm 52:5

137+ (cell 52:5 (bind 52:6 item) (bind 52:11 rest))

138+ (wing 52:17 item))))))

139+ (value 53:1 unrelated

140+ (gate 53:14

141+ (face 53:17 xs

142+ (apply 53:20 list (aura 53:26 @t)))

143+ (body 54:3

144+ (trace 54:3

145+ (lit 54:6 %pending)

146+ (body 55:5

147+ (branch 55:5

148+ (wing 55:8 xs)

149+ (arm 56:7 (lit 56:7 ~) (crash 56:9))

150+ (arm 57:7

151+ (cell 57:7 (bind 57:8 item) (bind 57:13 rest))

152+ (wing 57:19 item))))))))

153+ (value 58:1 empty-elements

154+ (gate 58:19

155+ (face 58:22 xs

156+ (apply 58:25 list (void 58:31)))

157+ (body 59:3

158+ (branch 59:3

159+ (wing 59:6 xs)

160+ (arm 60:5 (lit 60:5 ~) (crash 60:7))

161+ (arm 61:5

162+ (cell 61:5 (bind 61:6 item) (bind 61:11 rest))

163+ (wing 61:17 item))))))

164+ (mold 62:1 maybe

165+ (union 63:3

166+ (const 63:3 ~)

167+ (cell 64:3

168+ (const 64:4 ~)

169+ (face 64:6 value (aura 64:12 @t)))))

170+ (value 65:1 unit-shape

171+ (gate 65:15

172+ (face 65:18 xs (ref 65:21 maybe))

173+ (body 66:3

174+ (branch 66:3

175+ (wing 66:6 xs)

176+ (arm 67:5 (lit 67:5 ~) (crash 67:7))

177+ (arm 68:5

178+ (cell 68:5 (bind 68:6 item) (bind 68:11 rest))

179+ (wing 68:17 item)))))))

tests/golden/types-list-patterns/types.txt+1

@@ -2,6 +2,7 @@ partial inference; module not checked

22+$ msg: cases proven disjoint; mold not checked

33++ first-item: $-((list @t) @t)

44++ rest-items: $-((list @t) (list @t))

5+++ parent: $-((list @t) @u)

56++ with-context: $-((list @t) msg)

67++ shadow: pattern binder shadows a name

78++ duplicate: pattern binder shadows a name

tests/golden/types-local-error-order/about.txt+1−1

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

11source: Implementation plan, Risks: "Each error names both conflicting sites, with excerpts"; Grammar, Runes: "local names at the start of any body (a gate's, an arm's, a `^-`'s, a `~&`'s or a `++`'s), visible to each other and the final expression".

2−tests: a cast mismatch inside a local `++` is not reported as an error while a sibling that might fix the untyped sample's type waits without sites, since another order, or support for that sibling, could let the body pass. The sibling waits on a branch the checker does not support (`flat-mask`, and `outer-mask` one body further out), on its own nested stall (`nest-order`), or, in a local recursive gate, on the gate itself (`rec-order`, `rec-mask`, `rec-widen`). Each keeps the generic message; the `-ok`, `-g-first` and `-top` controls show the orders and forms the checker accepts or already leaves generic.

2+tests: a cast mismatch inside a local `++` is not reported as an error while a sibling that might fix the untyped sample's type waits without sites, since another order, or support for that sibling, could let the body pass. `flat-mask`, `outer-mask` and `rec-widen` now infer because their decimal and hexadecimal branch results unify at `@ux`. The remaining siblings wait on their own nested stall (`nest-order`) or, in a local recursive gate, on the gate itself (`rec-order`, `rec-mask`) and keep the generic message; the `-ok`, `-g-first` and `-top` controls show the orders and forms the checker accepts or already leaves generic.

33expect: parses

44expect-types: a partial inference report, not a checked module

tests/golden/types-local-error-order/types.txt+3−3

@@ -2,11 +2,11 @@ partial inference; module not checked

22++ rec-order: local definitions need unsupported inference

33++ rec-order-g-first: $-(@t @t)

44++ rec-order-top: local definitions need unsupported inference

5−++ flat-mask: local definitions need unsupported inference

5+++ flat-mask: $-(!! [@ux @t])

66++ flat-mask-ok: $-(!! [@ux @t])

7−++ outer-mask: local definitions need unsupported inference

7+++ outer-mask: $-(!! [@ux @t])

88++ nest-order: local definitions need unsupported inference

99++ nest-order-ok: $-(!! [@ux @t])

1010++ rec-mask: local definitions need unsupported inference

1111++ rec-ok: $-(@t @t)

12−++ rec-widen: local definitions need unsupported inference

12+++ rec-widen: $-(@t @t)

tests/golden/types-local-recursive/types.txt+1−1

@@ -20,5 +20,5 @@ partial inference; module not checked

2020/tests/golden/types-local-recursive/source.jibb:43:24: argument has type $-(A B)

2121 ++ recur |= y (recur recur)

2222 ^

23−++ captures: local definitions need unsupported inference

23+++ captures: explicit capital constraints are not supported by partial inference

2424++ via-gate: local definitions need unsupported inference

tests/golden/types-partial-branch-widening/about.txt+1−1

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

11source: a specific atom fits `@`, and a subaura fits its parent; different specific auras do not unify.

2−tests: a branch joins an already present parent aura or unrestricted atom in either order; unresolved variable-dependent joins stay unsupported, and sibling auras remain distinct.

2+tests: every uncontextual branch kind unifies first, then joins an already present parent aura or unrestricted atom; open variables retain unification substitutions, decimal results work with or without context, late union parents widen earlier results without order-dependent variable substitutions, singleton atoms and restricted decimals join explicit `@`, and sibling auras remain distinct without a common parent.

33expect: parses

44expect-types: a partial inference report, not a checked module

tests/golden/types-partial-branch-widening/source.jibb+55

@@ -10,6 +10,10 @@

1010 ?- b

1111 %.y ^- @ ~zod

1212 %.n "hi"

13+++ atom-decimal |= b=?

14+ ?- b

15+ %.y ^- @ ~zod

16+ %.n 0

1317++ unknown |= x

1418 ?- %.y

1519 %.y x

@@ -18,3 +22,54 @@

1822 ?- b

1923 %.y ^- @ud 1

2024 %.n 0x1f

25+++ decimal |= [b=? n=@ud]

26+ ?- b

27+ %.y n

28+ %.n 0

29+++ decimal-context |= [b=? n=@ud]

30+ ^- @ud ?- b

31+ %.y n

32+ %.n 0

33++$ maybe |$ [A]

34+ ~

35+ [~ value=A]

36+++ unit-parent |= x=(maybe @ud)

37+ ?- x

38+ ~ 0x1f

39+ [~ value] ^- @u 0x1f

40++$ number-choice

41+ [%hex @ux]

42+ [%parent @u]

43+ [%decimal @ud]

44+++ union-parent |= x=number-choice

45+ ?- x

46+ [%hex n] 0x1f

47+ [%parent n] ^- @u 0x1f

48+ [%decimal n] 0

49+++ union-parent-late |= x=number-choice

50+ ?- x

51+ [%hex n] 0x1f

52+ [%decimal n] ^- @ud 0

53+ [%parent n] ^- @u 0x1f

54+++ union-variable |= [x=number-choice value]

55+ ?- x

56+ [%hex n] value

57+ [%decimal n] 0x1f

58+ [%parent n] ^- @u 0x1f

59+++ union-variable-late |= [x=number-choice value]

60+ ?- x

61+ [%parent n] ^- @u 0x1f

62+ [%hex n] 0x1f

63+ [%decimal n] value

64+++ union-any-late |= x=number-choice

65+ ?- x

66+ [%hex n] 0x1f

67+ [%decimal n] ^- @ud 0

68+ [%parent n] ^- @ ~zod

69++$ singleton-choice

70+ [%nothing ~]

71+ [%anything @ud]

72+++ union-singleton |= x=singleton-choice

73+ ?- x

74+ [%nothing n] n

75+ [%anything n] ^- @ ~zod

tests/golden/types-partial-branch-widening/tokens.txt+358−18

@@ -59,38 +59,378 @@

595913:1 DEDENT

606013:1 NEWLINE

616113:1 glyph ++

62−13:4 name unknown

63−13:12 glyph |=

64−13:15 name x

62+13:4 name atom-decimal

63+13:17 glyph |=

64+13:20 name b

65+13:21 tight glyph =

66+13:22 tight glyph ?

656714:3 INDENT

666814:3 glyph ?-

67−14:6 lit %.y

69+14:6 name b

687015:5 INDENT

697115:5 lit %.y

70−15:9 name x

72+15:9 glyph ^-

73+15:12 aura @

74+15:14 lit ~zod

717516:5 NEWLINE

727616:5 lit %.n

73−16:9 lit 0x1f

77+16:9 lit 0

747817:1 DEDENT

757917:1 DEDENT

768017:1 NEWLINE

778117:1 glyph ++

78−17:4 name siblings

79−17:13 glyph |=

80−17:16 name b

81−17:17 tight glyph =

82−17:18 tight glyph ?

82+17:4 name unknown

83+17:12 glyph |=

84+17:15 name x

838518:3 INDENT

848618:3 glyph ?-

85−18:6 name b

87+18:6 lit %.y

868819:5 INDENT

878919:5 lit %.y

88−19:9 glyph ^-

89−19:12 aura @ud

90−19:16 lit 1

90+19:9 name x

919120:5 NEWLINE

929220:5 lit %.n

939320:9 lit 0x1f

94−20:13 DEDENT

95−20:13 DEDENT

96−20:13 NEWLINE

94+21:1 DEDENT

95+21:1 DEDENT

96+21:1 NEWLINE

97+21:1 glyph ++

98+21:4 name siblings

99+21:13 glyph |=

100+21:16 name b

101+21:17 tight glyph =

102+21:18 tight glyph ?

103+22:3 INDENT

104+22:3 glyph ?-

105+22:6 name b

106+23:5 INDENT

107+23:5 lit %.y

108+23:9 glyph ^-

109+23:12 aura @ud

110+23:16 lit 1

111+24:5 NEWLINE

112+24:5 lit %.n

113+24:9 lit 0x1f

114+25:1 DEDENT

115+25:1 DEDENT

116+25:1 NEWLINE

117+25:1 glyph ++

118+25:4 name decimal

119+25:12 glyph |=

120+25:15 glyph [

121+25:16 tight name b

122+25:17 tight glyph =

123+25:18 tight glyph ?

124+25:20 name n

125+25:21 tight glyph =

126+25:22 tight aura @ud

127+25:25 tight glyph ]

128+26:3 INDENT

129+26:3 glyph ?-

130+26:6 name b

131+27:5 INDENT

132+27:5 lit %.y

133+27:9 name n

134+28:5 NEWLINE

135+28:5 lit %.n

136+28:9 lit 0

137+29:1 DEDENT

138+29:1 DEDENT

139+29:1 NEWLINE

140+29:1 glyph ++

141+29:4 name decimal-context

142+29:20 glyph |=

143+29:23 glyph [

144+29:24 tight name b

145+29:25 tight glyph =

146+29:26 tight glyph ?

147+29:28 name n

148+29:29 tight glyph =

149+29:30 tight aura @ud

150+29:33 tight glyph ]

151+30:3 INDENT

152+30:3 glyph ^-

153+30:6 aura @ud

154+30:11 glyph ?-

155+30:14 name b

156+31:5 INDENT

157+31:5 lit %.y

158+31:9 name n

159+32:5 NEWLINE

160+32:5 lit %.n

161+32:9 lit 0

162+33:1 DEDENT

163+33:1 DEDENT

164+33:1 NEWLINE

165+33:1 glyph +$

166+33:4 name maybe

167+33:10 glyph |$

168+33:13 glyph [

169+33:14 tight tvar A

170+33:15 tight glyph ]

171+34:3 INDENT

172+34:3 lit ~

173+35:3 NEWLINE

174+35:3 glyph [

175+35:4 tight lit ~

176+35:6 name value

177+35:11 tight glyph =

178+35:12 tight tvar A

179+35:13 tight glyph ]

180+36:1 DEDENT

181+36:1 NEWLINE

182+36:1 glyph ++

183+36:4 name unit-parent

184+36:16 glyph |=

185+36:19 name x

186+36:20 tight glyph =

187+36:21 tight glyph (

188+36:22 tight name maybe

189+36:28 aura @ud

190+36:31 tight glyph )

191+37:3 INDENT

192+37:3 glyph ?-

193+37:6 name x

194+38:5 INDENT

195+38:5 lit ~

196+38:7 lit 0x1f

197+39:5 NEWLINE

198+39:5 glyph [

199+39:6 tight lit ~

200+39:8 name value

201+39:13 tight glyph ]

202+39:15 glyph ^-

203+39:18 aura @u

204+39:21 lit 0x1f

205+40:1 DEDENT

206+40:1 DEDENT

207+40:1 NEWLINE

208+40:1 glyph +$

209+40:4 name number-choice

210+41:3 INDENT

211+41:3 glyph [

212+41:4 tight lit %hex

213+41:9 aura @ux

214+41:12 tight glyph ]

215+42:3 NEWLINE

216+42:3 glyph [

217+42:4 tight lit %parent

218+42:12 aura @u

219+42:14 tight glyph ]

220+43:3 NEWLINE

221+43:3 glyph [

222+43:4 tight lit %decimal

223+43:13 aura @ud

224+43:16 tight glyph ]

225+44:1 DEDENT

226+44:1 NEWLINE

227+44:1 glyph ++

228+44:4 name union-parent

229+44:17 glyph |=

230+44:20 name x

231+44:21 tight glyph =

232+44:22 tight name number-choice

233+45:3 INDENT

234+45:3 glyph ?-

235+45:6 name x

236+46:5 INDENT

237+46:5 glyph [

238+46:6 tight lit %hex

239+46:11 name n

240+46:12 tight glyph ]

241+46:14 lit 0x1f

242+47:5 NEWLINE

243+47:5 glyph [

244+47:6 tight lit %parent

245+47:14 name n

246+47:15 tight glyph ]

247+47:17 glyph ^-

248+47:20 aura @u

249+47:23 lit 0x1f

250+48:5 NEWLINE

251+48:5 glyph [

252+48:6 tight lit %decimal

253+48:15 name n

254+48:16 tight glyph ]

255+48:18 lit 0

256+49:1 DEDENT

257+49:1 DEDENT

258+49:1 NEWLINE

259+49:1 glyph ++

260+49:4 name union-parent-late

261+49:22 glyph |=

262+49:25 name x

263+49:26 tight glyph =

264+49:27 tight name number-choice

265+50:3 INDENT

266+50:3 glyph ?-

267+50:6 name x

268+51:5 INDENT

269+51:5 glyph [

270+51:6 tight lit %hex

271+51:11 name n

272+51:12 tight glyph ]

273+51:14 lit 0x1f

274+52:5 NEWLINE

275+52:5 glyph [

276+52:6 tight lit %decimal

277+52:15 name n

278+52:16 tight glyph ]

279+52:18 glyph ^-

280+52:21 aura @ud

281+52:25 lit 0

282+53:5 NEWLINE

283+53:5 glyph [

284+53:6 tight lit %parent

285+53:14 name n

286+53:15 tight glyph ]

287+53:17 glyph ^-

288+53:20 aura @u

289+53:23 lit 0x1f

290+54:1 DEDENT

291+54:1 DEDENT

292+54:1 NEWLINE

293+54:1 glyph ++

294+54:4 name union-variable

295+54:19 glyph |=

296+54:22 glyph [

297+54:23 tight name x

298+54:24 tight glyph =

299+54:25 tight name number-choice

300+54:39 name value

301+54:44 tight glyph ]

302+55:3 INDENT

303+55:3 glyph ?-

304+55:6 name x

305+56:5 INDENT

306+56:5 glyph [

307+56:6 tight lit %hex

308+56:11 name n

309+56:12 tight glyph ]

310+56:14 name value

311+57:5 NEWLINE

312+57:5 glyph [

313+57:6 tight lit %decimal

314+57:15 name n

315+57:16 tight glyph ]

316+57:18 lit 0x1f

317+58:5 NEWLINE

318+58:5 glyph [

319+58:6 tight lit %parent

320+58:14 name n

321+58:15 tight glyph ]

322+58:17 glyph ^-

323+58:20 aura @u

324+58:23 lit 0x1f

325+59:1 DEDENT

326+59:1 DEDENT

327+59:1 NEWLINE

328+59:1 glyph ++

329+59:4 name union-variable-late

330+59:24 glyph |=

331+59:27 glyph [

332+59:28 tight name x

333+59:29 tight glyph =

334+59:30 tight name number-choice

335+59:44 name value

336+59:49 tight glyph ]

337+60:3 INDENT

338+60:3 glyph ?-

339+60:6 name x

340+61:5 INDENT

341+61:5 glyph [

342+61:6 tight lit %parent

343+61:14 name n

344+61:15 tight glyph ]

345+61:17 glyph ^-

346+61:20 aura @u

347+61:23 lit 0x1f

348+62:5 NEWLINE

349+62:5 glyph [

350+62:6 tight lit %hex

351+62:11 name n

352+62:12 tight glyph ]

353+62:14 lit 0x1f

354+63:5 NEWLINE

355+63:5 glyph [

356+63:6 tight lit %decimal

357+63:15 name n

358+63:16 tight glyph ]

359+63:18 name value

360+64:1 DEDENT

361+64:1 DEDENT

362+64:1 NEWLINE

363+64:1 glyph ++

364+64:4 name union-any-late

365+64:19 glyph |=

366+64:22 name x

367+64:23 tight glyph =

368+64:24 tight name number-choice

369+65:3 INDENT

370+65:3 glyph ?-

371+65:6 name x

372+66:5 INDENT

373+66:5 glyph [

374+66:6 tight lit %hex

375+66:11 name n

376+66:12 tight glyph ]

377+66:14 lit 0x1f

378+67:5 NEWLINE

379+67:5 glyph [

380+67:6 tight lit %decimal

381+67:15 name n

382+67:16 tight glyph ]

383+67:18 glyph ^-

384+67:21 aura @ud

385+67:25 lit 0

386+68:5 NEWLINE

387+68:5 glyph [

388+68:6 tight lit %parent

389+68:14 name n

390+68:15 tight glyph ]

391+68:17 glyph ^-

392+68:20 aura @

393+68:22 lit ~zod

394+69:1 DEDENT

395+69:1 DEDENT

396+69:1 NEWLINE

397+69:1 glyph +$

398+69:4 name singleton-choice

399+70:3 INDENT

400+70:3 glyph [

401+70:4 tight lit %nothing

402+70:13 lit ~

403+70:14 tight glyph ]

404+71:3 NEWLINE

405+71:3 glyph [

406+71:4 tight lit %anything

407+71:14 aura @ud

408+71:17 tight glyph ]

409+72:1 DEDENT

410+72:1 NEWLINE

411+72:1 glyph ++

412+72:4 name union-singleton

413+72:20 glyph |=

414+72:23 name x

415+72:24 tight glyph =

416+72:25 tight name singleton-choice

417+73:3 INDENT

418+73:3 glyph ?-

419+73:6 name x

420+74:5 INDENT

421+74:5 glyph [

422+74:6 tight lit %nothing

423+74:15 name n

424+74:16 tight glyph ]

425+74:18 name n

426+75:5 NEWLINE

427+75:5 glyph [

428+75:6 tight lit %anything

429+75:16 name n

430+75:17 tight glyph ]

431+75:19 glyph ^-

432+75:22 aura @

433+75:24 lit ~zod

434+75:28 DEDENT

435+75:28 DEDENT

436+75:28 NEWLINE

tests/golden/types-partial-branch-widening/tree.txt+164−14

@@ -29,21 +29,171 @@

2929 (lit 11:5 %.y)

3030 (cast 11:9 (aura 11:12 @) (lit 11:14 ~zod)))

3131 (arm 12:5 (lit 12:5 %.n) (str 12:9 "hi"))))))

32− (value 13:1 unknown

33− (gate 13:12

34− (bind 13:15 x)

32+ (value 13:1 atom-decimal

33+ (gate 13:17

34+ (face 13:20 b (flag 13:22))

3535 (body 14:3

3636 (branch 14:3

37− (lit 14:6 %.y)

38− (arm 15:5 (lit 15:5 %.y) (wing 15:9 x))

39− (arm 16:5 (lit 16:5 %.n) (lit 16:9 0x1f))))))

40− (value 17:1 siblings

41− (gate 17:13

42− (face 17:16 b (flag 17:18))

37+ (wing 14:6 b)

38+ (arm 15:5

39+ (lit 15:5 %.y)

40+ (cast 15:9 (aura 15:12 @) (lit 15:14 ~zod)))

41+ (arm 16:5 (lit 16:5 %.n) (lit 16:9 0))))))

42+ (value 17:1 unknown

43+ (gate 17:12

44+ (bind 17:15 x)

4345 (body 18:3

4446 (branch 18:3

45− (wing 18:6 b)

46− (arm 19:5

47− (lit 19:5 %.y)

48− (cast 19:9 (aura 19:12 @ud) (lit 19:16 1)))

49− (arm 20:5 (lit 20:5 %.n) (lit 20:9 0x1f)))))))

47+ (lit 18:6 %.y)

48+ (arm 19:5 (lit 19:5 %.y) (wing 19:9 x))

49+ (arm 20:5 (lit 20:5 %.n) (lit 20:9 0x1f))))))

50+ (value 21:1 siblings

51+ (gate 21:13

52+ (face 21:16 b (flag 21:18))

53+ (body 22:3

54+ (branch 22:3

55+ (wing 22:6 b)

56+ (arm 23:5

57+ (lit 23:5 %.y)

58+ (cast 23:9 (aura 23:12 @ud) (lit 23:16 1)))

59+ (arm 24:5 (lit 24:5 %.n) (lit 24:9 0x1f))))))

60+ (value 25:1 decimal

61+ (gate 25:12

62+ (cell 25:15

63+ (face 25:16 b (flag 25:18))

64+ (face 25:20 n (aura 25:22 @ud)))

65+ (body 26:3

66+ (branch 26:3

67+ (wing 26:6 b)

68+ (arm 27:5 (lit 27:5 %.y) (wing 27:9 n))

69+ (arm 28:5 (lit 28:5 %.n) (lit 28:9 0))))))

70+ (value 29:1 decimal-context

71+ (gate 29:20

72+ (cell 29:23

73+ (face 29:24 b (flag 29:26))

74+ (face 29:28 n (aura 29:30 @ud)))

75+ (body 30:3

76+ (cast 30:3

77+ (aura 30:6 @ud)

78+ (branch 30:11

79+ (wing 30:14 b)

80+ (arm 31:5 (lit 31:5 %.y) (wing 31:9 n))

81+ (arm 32:5 (lit 32:5 %.n) (lit 32:9 0)))))))

82+ (mold 33:1 maybe

83+ (generic 33:10 A

84+ (union 34:3

85+ (const 34:3 ~)

86+ (cell 35:3

87+ (const 35:4 ~)

88+ (face 35:6 value (tvar 35:12 A))))))

89+ (value 36:1 unit-parent

90+ (gate 36:16

91+ (face 36:19 x

92+ (apply 36:21 maybe (aura 36:28 @ud)))

93+ (body 37:3

94+ (branch 37:3

95+ (wing 37:6 x)

96+ (arm 38:5 (lit 38:5 ~) (lit 38:7 0x1f))

97+ (arm 39:5

98+ (cell 39:5 (lit 39:6 ~) (bind 39:8 value))

99+ (cast 39:15 (aura 39:18 @u) (lit 39:21 0x1f)))))))

100+ (mold 40:1 number-choice

101+ (union 41:3

102+ (cell 41:3 (const 41:4 %hex) (aura 41:9 @ux))

103+ (cell 42:3 (const 42:4 %parent) (aura 42:12 @u))

104+ (cell 43:3 (const 43:4 %decimal) (aura 43:13 @ud))))

105+ (value 44:1 union-parent

106+ (gate 44:17

107+ (face 44:20 x (ref 44:22 number-choice))

108+ (body 45:3

109+ (branch 45:3

110+ (wing 45:6 x)

111+ (arm 46:5

112+ (cell 46:5 (lit 46:6 %hex) (bind 46:11 n))

113+ (lit 46:14 0x1f))

114+ (arm 47:5

115+ (cell 47:5 (lit 47:6 %parent) (bind 47:14 n))

116+ (cast 47:17 (aura 47:20 @u) (lit 47:23 0x1f)))

117+ (arm 48:5

118+ (cell 48:5 (lit 48:6 %decimal) (bind 48:15 n))

119+ (lit 48:18 0))))))

120+ (value 49:1 union-parent-late

121+ (gate 49:22

122+ (face 49:25 x (ref 49:27 number-choice))

123+ (body 50:3

124+ (branch 50:3

125+ (wing 50:6 x)

126+ (arm 51:5

127+ (cell 51:5 (lit 51:6 %hex) (bind 51:11 n))

128+ (lit 51:14 0x1f))

129+ (arm 52:5

130+ (cell 52:5 (lit 52:6 %decimal) (bind 52:15 n))

131+ (cast 52:18 (aura 52:21 @ud) (lit 52:25 0)))

132+ (arm 53:5

133+ (cell 53:5 (lit 53:6 %parent) (bind 53:14 n))

134+ (cast 53:17 (aura 53:20 @u) (lit 53:23 0x1f)))))))

135+ (value 54:1 union-variable

136+ (gate 54:19

137+ (cell 54:22

138+ (face 54:23 x (ref 54:25 number-choice))

139+ (bind 54:39 value))

140+ (body 55:3

141+ (branch 55:3

142+ (wing 55:6 x)

143+ (arm 56:5

144+ (cell 56:5 (lit 56:6 %hex) (bind 56:11 n))

145+ (wing 56:14 value))

146+ (arm 57:5

147+ (cell 57:5 (lit 57:6 %decimal) (bind 57:15 n))

148+ (lit 57:18 0x1f))

149+ (arm 58:5

150+ (cell 58:5 (lit 58:6 %parent) (bind 58:14 n))

151+ (cast 58:17 (aura 58:20 @u) (lit 58:23 0x1f)))))))

152+ (value 59:1 union-variable-late

153+ (gate 59:24

154+ (cell 59:27

155+ (face 59:28 x (ref 59:30 number-choice))

156+ (bind 59:44 value))

157+ (body 60:3

158+ (branch 60:3

159+ (wing 60:6 x)

160+ (arm 61:5

161+ (cell 61:5 (lit 61:6 %parent) (bind 61:14 n))

162+ (cast 61:17 (aura 61:20 @u) (lit 61:23 0x1f)))

163+ (arm 62:5

164+ (cell 62:5 (lit 62:6 %hex) (bind 62:11 n))

165+ (lit 62:14 0x1f))

166+ (arm 63:5

167+ (cell 63:5 (lit 63:6 %decimal) (bind 63:15 n))

168+ (wing 63:18 value))))))

169+ (value 64:1 union-any-late

170+ (gate 64:19

171+ (face 64:22 x (ref 64:24 number-choice))

172+ (body 65:3

173+ (branch 65:3

174+ (wing 65:6 x)

175+ (arm 66:5

176+ (cell 66:5 (lit 66:6 %hex) (bind 66:11 n))

177+ (lit 66:14 0x1f))

178+ (arm 67:5

179+ (cell 67:5 (lit 67:6 %decimal) (bind 67:15 n))

180+ (cast 67:18 (aura 67:21 @ud) (lit 67:25 0)))

181+ (arm 68:5

182+ (cell 68:5 (lit 68:6 %parent) (bind 68:14 n))

183+ (cast 68:17 (aura 68:20 @) (lit 68:22 ~zod)))))))

184+ (mold 69:1 singleton-choice

185+ (union 70:3

186+ (cell 70:3 (const 70:4 %nothing) (const 70:13 ~))

187+ (cell 71:3 (const 71:4 %anything) (aura 71:14 @ud))))

188+ (value 72:1 union-singleton

189+ (gate 72:20

190+ (face 72:23 x (ref 72:25 singleton-choice))

191+ (body 73:3

192+ (branch 73:3

193+ (wing 73:6 x)

194+ (arm 74:5

195+ (cell 74:5 (lit 74:6 %nothing) (bind 74:15 n))

196+ (wing 74:18 n))

197+ (arm 75:5

198+ (cell 75:5 (lit 75:6 %anything) (bind 75:16 n))

199+ (cast 75:19 (aura 75:22 @) (lit 75:24 ~zod))))))))

tests/golden/types-partial-branch-widening/types.txt+16−3

@@ -2,11 +2,24 @@ partial inference; module not checked

22++ join: $-(? @u)

33++ reverse: $-(? @u)

44++ atom: $-(? @)

5−++ unknown: branch widening is not supported by partial inference

5+++ atom-decimal: $-(? @)

6+++ unknown: $-(@ux @ux)

67++ siblings: branch arms have incompatible types

7−/tests/golden/types-partial-branch-widening/source.jibb:19:9: first arm has type @ud

8+/tests/golden/types-partial-branch-widening/source.jibb:23:9: first arm has type @ud

89 %.y ^- @ud 1

910 ^

10−/tests/golden/types-partial-branch-widening/source.jibb:20:9: second arm has type @ux

11+/tests/golden/types-partial-branch-widening/source.jibb:24:9: second arm has type @ux

1112 %.n 0x1f

1213 ^

14+++ decimal: $-([b=? n=@ud] @ud)

15+++ decimal-context: $-([b=? n=@ud] @ud)

16++$ maybe: cases proven disjoint; mold not checked

17+++ unit-parent: $-((maybe @ud) @u)

18++$ number-choice: cases proven disjoint; mold not checked

19+++ union-parent: $-(number-choice @u)

20+++ union-parent-late: $-(number-choice @u)

21+++ union-variable: $-([x=number-choice value=@u] @u)

22+++ union-variable-late: $-([x=number-choice value=@u] @u)

23+++ union-any-late: $-(number-choice @)

24++$ singleton-choice: cases proven disjoint; mold not checked

25+++ union-singleton: $-(singleton-choice @)

tests/golden/types-prelude-sub/types.txt+1−1

@@ -12,7 +12,7 @@ partial inference; module not checked

1212/tests/golden/types-prelude-sub/source.jibb:9:28: expression

1313++ wrong-reply ^- (sub @t) [%every gap=~s1 reply=|=(date=@p "bad")]

1414 ^

15−++ incomplete: union branch result matching needs unsupported inference

15+++ incomplete: missing union case [%url reply=$-((list @ta) msg)]

1616++ complete: union branch result matching needs unsupported inference

1717+$ my-msg: cases proven disjoint; mold not checked

1818++ take-watch: $-((sub my-msg) (ask my-msg))

tests/golden/types-recursion-scc-local/about.txt+1−1

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

11source: Grammar, Runes: "Gates may call themselves and their siblings; other values can't depend on themselves, even through a gate"; Modules: "Names may refer to each other in any order, and no name may shadow one already in scope, imports and the prelude included."

2−tests: A mutually recursive local group remains unsupported. A top-level group can include an outer gate whose local helper refers to the other group member.

2+tests: A mutually recursive local group unifies its text base and recursive arm results. A top-level group can include an outer gate whose local helper refers to the other group member.

33expect: parses

44expect-types: a partial inference report

tests/golden/types-recursion-scc-local/types.txt+1−1

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

11partial inference; module not checked

2−++ outer: local definitions need unsupported inference

2+++ outer: $-(@t @t)

33++ global-a: $-(@t A)

44++ global-b: $-(@t A)

tests/golden/types-recursive-branch/types.txt+4−4

@@ -8,9 +8,9 @@ partial inference; module not checked

88++ input-base: $-(A A)

99++ inferred-base: $-(A A)

1010++ captured: $-(A A)

11−++ forced: branch widening is not supported by partial inference

12−++ pending: branch widening is not supported by partial inference

13−++ pending-null: branch widening is not supported by partial inference

11+++ forced: explicit capital constraints are not supported by partial inference

12+++ pending: tag needs context in partial inference

13+++ pending-null: `~` needs context in partial inference

1414++ dependent: $-(? @t)

1515++ nonself: $-(? @t)

1616++ polymorphic: call's sample and argument types do not unify

@@ -46,5 +46,5 @@ partial inference; module not checked

4646/tests/golden/types-recursive-branch/source.jibb:93:11: second arm has type @t

4747 %.n (aura-conflict b)

4848 ^

49−++ traced: branch widening is not supported by partial inference

49+++ traced: $-(? @t)

5050++ unresolved-number: unresolved aura-variable inference

tests/golden/types-recursive-gate/types.txt+2−2

@@ -17,8 +17,8 @@ partial inference; module not checked

1717/tests/golden/types-recursive-gate/source.jibb:12:19: argument

1818++ occurs |= x (x x)

1919 ^

20−++ forcing: branch widening is not supported by partial inference

21−++ pending: branch widening is not supported by partial inference

20+++ forcing: explicit capital constraints are not supported by partial inference

21+++ pending: tag needs context in partial inference

2222++ direct-value: name is not available to partial inference

2323++ gate-value: name is not available to partial inference

2424++ value-cycle: name is not available to partial inference

tests/golden/types-union-finite-generic/about.txt+1−1

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

11source: Grammar, Patterns: "Every case needs an arm or a catch-all"; Molds: "Type variables are capitals, generalized per `++`."

2−tests: Boolean refinements preserve generic payload and binder types; a shared payload variable infers, while distinct arm result variables, forcing an explicit capital, unresolved tags and partial string matches remain unsupported. An unavailable name in an earlier arm is not masked by pattern checking.

2+tests: Boolean refinements preserve generic payload and binder types; a shared payload variable infers, while distinct arm result variables are diagnosed rather than forced equal, and forcing an explicit capital, unresolved tags and partial string matches remain unsupported. An unavailable name in an earlier arm is not masked by pattern checking.

33expect: parses

44expect-types: a partial inference report

tests/golden/types-union-finite-generic/types.txt+7−1

@@ -1,7 +1,13 @@

11partial inference; module not checked

22+$ msg: cases proven disjoint; mold not checked

33++ shared: $-((msg A A) A)

4−++ different: union branch result matching needs unsupported inference

4+++ different: distinct type variables `A` and `B` must not be forced equal; use the same capital for a shared type

5+/tests/golden/types-union-finite-generic/source.jibb:10:24: first type variable

6+++ different |= m=(msg A B)

7+ ^

8+/tests/golden/types-union-finite-generic/source.jibb:10:26: second type variable

9+++ different |= m=(msg A B)

10+ ^

511++ forced: explicit capital constraints are not supported by partial inference

612++ earlier: name is not available to partial inference

713+$ choice: cases proven disjoint; mold not checked

tests/golden/types-union-finite/about.txt+1−1

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

11source: Grammar, Patterns: "Every case needs an arm or a catch-all"; "An arm that earlier arms cover ... is an error"; "A name in a pattern always binds anew".

2−tests: Two boolean fields are split into finite alternatives for complete tables and wildcard patterns. A missing alternative is named, a covered partial arm is rejected even when it uses a different spelling of zero, and a whole-case binder retains its original `?` type. Shadowing and a binder spanning different union cases fail closed.

2+tests: Finite boolean refinements share the unification-first, explicitly-present-parent result join, including multiple arm results. Two boolean fields are split into finite alternatives for complete tables and wildcard patterns. A missing alternative is named, a covered partial arm is rejected even when it uses a different spelling of zero, and a whole-case binder retains its original `?` type. Shadowing and a binder spanning different union cases fail closed.

33expect: parses

44expect-types: a partial inference report

tests/golden/types-union-finite/source.jibb+7

@@ -8,6 +8,13 @@

88 [%p %.n %.y] "c"

99 [%p %.n %.n] "d"

1010 %other "e"

11+++ parent |= m=msg

12+ ?- m

13+ [%p %.y %.y] 0x1f

14+ [%p %.y %.n] ^- @u 0x1f

15+ [%p %.n %.y] 0

16+ [%p %.n %.n] 0x2f

17+ %other ^- @u 0x1f

1118++ wildcard |= m=msg

1219 ?- m

1320 [%p %.y *] "a"

tests/golden/types-union-finite/tokens.txt+210−163

@@ -58,11 +58,11 @@

585811:1 DEDENT

595911:1 NEWLINE

606011:1 glyph ++

61−11:4 name wildcard

62−11:13 glyph |=

63−11:16 name m

64−11:17 tight glyph =

65−11:18 tight name msg

61+11:4 name parent

62+11:11 glyph |=

63+11:14 name m

64+11:15 tight glyph =

65+11:16 tight name msg

666612:3 INDENT

676712:3 glyph ?-

686812:6 name m

@@ -70,169 +70,216 @@

707013:5 glyph [

717113:6 tight lit %p

727213:9 lit %.y

73−13:13 glyph *

74−13:14 tight glyph ]

75−13:16 str "a"

73+13:13 lit %.y

74+13:16 tight glyph ]

75+13:18 lit 0x1f

767614:5 NEWLINE

777714:5 glyph [

787814:6 tight lit %p

79−14:9 lit %.n

80−14:13 glyph *

81−14:14 tight glyph ]

82−14:16 str "b"

79+14:9 lit %.y

80+14:13 lit %.n

81+14:16 tight glyph ]

82+14:18 glyph ^-

83+14:21 aura @u

84+14:24 lit 0x1f

838515:5 NEWLINE

84−15:5 lit %other

85−15:12 str "e"

86−16:1 DEDENT

87−16:1 DEDENT

88−16:1 NEWLINE

89−16:1 glyph ++

90−16:4 name covered

91−16:12 glyph |=

92−16:15 name m

93−16:16 tight glyph =

94−16:17 tight name msg

95−17:3 INDENT

96−17:3 glyph ?-

97−17:6 name m

98−18:5 INDENT

99−18:5 glyph [

100−18:6 tight lit %p

101−18:9 lit %.y

102−18:13 glyph *

103−18:14 tight glyph ]

104−18:16 str "a"

105−19:5 NEWLINE

106−19:5 glyph [

107−19:6 tight lit %p

108−19:9 lit %.y

109−19:13 lit %.n

110−19:16 tight glyph ]

111−19:18 str "b"

112−20:5 NEWLINE

113−20:5 glyph *

114−20:7 str "e"

115−22:1 DEDENT

116−22:1 DEDENT

117−22:1 NEWLINE

118−22:1 glyph +$

119−22:4 name choice

120−23:3 INDENT

121−23:3 glyph [

122−23:4 tight lit %a

123−23:7 name on

124−23:9 tight glyph =

125−23:10 tight glyph ?

126−23:11 tight glyph ]

127−24:3 NEWLINE

128−24:3 lit %other

129−25:1 DEDENT

130−25:1 NEWLINE

131−25:1 glyph ++

132−25:4 name missing

133−25:12 glyph |=

134−25:15 name x

135−25:16 tight glyph =

136−25:17 tight name choice

137−26:3 INDENT

138−26:3 glyph ?-

139−26:6 name x

140−27:5 INDENT

141−27:5 glyph [

142−27:6 tight lit %a

143−27:9 lit %.y

144−27:12 tight glyph ]

145−27:14 str "yes"

146−28:5 NEWLINE

147−28:5 lit %other

148−28:12 str "other"

86+15:5 glyph [

87+15:6 tight lit %p

88+15:9 lit %.n

89+15:13 lit %.y

90+15:16 tight glyph ]

91+15:18 lit 0

92+16:5 NEWLINE

93+16:5 glyph [

94+16:6 tight lit %p

95+16:9 lit %.n

96+16:13 lit %.n

97+16:16 tight glyph ]

98+16:18 lit 0x2f

99+17:5 NEWLINE

100+17:5 lit %other

101+17:12 glyph ^-

102+17:15 aura @u

103+17:18 lit 0x1f

104+18:1 DEDENT

105+18:1 DEDENT

106+18:1 NEWLINE

107+18:1 glyph ++

108+18:4 name wildcard

109+18:13 glyph |=

110+18:16 name m

111+18:17 tight glyph =

112+18:18 tight name msg

113+19:3 INDENT

114+19:3 glyph ?-

115+19:6 name m

116+20:5 INDENT

117+20:5 glyph [

118+20:6 tight lit %p

119+20:9 lit %.y

120+20:13 glyph *

121+20:14 tight glyph ]

122+20:16 str "a"

123+21:5 NEWLINE

124+21:5 glyph [

125+21:6 tight lit %p

126+21:9 lit %.n

127+21:13 glyph *

128+21:14 tight glyph ]

129+21:16 str "b"

130+22:5 NEWLINE

131+22:5 lit %other

132+22:12 str "e"

133+23:1 DEDENT

134+23:1 DEDENT

135+23:1 NEWLINE

136+23:1 glyph ++

137+23:4 name covered

138+23:12 glyph |=

139+23:15 name m

140+23:16 tight glyph =

141+23:17 tight name msg

142+24:3 INDENT

143+24:3 glyph ?-

144+24:6 name m

145+25:5 INDENT

146+25:5 glyph [

147+25:6 tight lit %p

148+25:9 lit %.y

149+25:13 glyph *

150+25:14 tight glyph ]

151+25:16 str "a"

152+26:5 NEWLINE

153+26:5 glyph [

154+26:6 tight lit %p

155+26:9 lit %.y

156+26:13 lit %.n

157+26:16 tight glyph ]

158+26:18 str "b"

159+27:5 NEWLINE

160+27:5 glyph *

161+27:7 str "e"

14916229:1 DEDENT

15016329:1 DEDENT

15116429:1 NEWLINE

152−29:1 glyph ++

153−29:4 name typed

154−29:10 glyph |=

155−29:13 name x

156−29:14 tight glyph =

157−29:15 tight name choice

165+29:1 glyph +$

166+29:4 name choice

15816730:3 INDENT

159−30:3 glyph ?-

160−30:6 name x

161−31:5 INDENT

162−31:5 glyph [

163−31:6 tight lit %a

164−31:9 name value

165−31:14 tight glyph ]

166−31:16 name value

167−32:5 NEWLINE

168−32:5 lit %other

169−32:12 lit %.n

170−33:1 DEDENT

171−33:1 DEDENT

172−33:1 NEWLINE

173−33:1 glyph ++

174−33:4 name duplicate

175−33:14 glyph |=

176−33:17 name x

177−33:18 tight glyph =

178−33:19 tight name choice

179−34:3 INDENT

180−34:3 glyph ?-

181−34:6 name x

182−35:5 INDENT

183−35:5 glyph [

184−35:6 tight lit %a

185−35:9 lit %.y

186−35:12 tight glyph ]

187−35:14 str "yes"

188−36:5 NEWLINE

189−36:5 glyph [

190−36:6 tight lit %a

191−36:9 lit %$

192−36:11 tight glyph ]

193−36:13 str "duplicate"

194−37:5 NEWLINE

195−37:5 glyph *

196−37:7 str "other"

197−38:1 DEDENT

198−38:1 DEDENT

199−38:1 NEWLINE

200−38:1 glyph ++

201−38:4 name shadow

202−38:11 glyph |=

203−38:14 name x

204−38:15 tight glyph =

205−38:16 tight name choice

206−39:3 INDENT

207−39:3 glyph ?-

208−39:6 name x

209−40:5 INDENT

210−40:5 glyph [

211−40:6 tight lit %a

212−40:9 name missing

213−40:16 tight glyph ]

214−40:18 str "yes"

215−41:5 NEWLINE

216−41:5 lit %other

217−41:12 str "other"

218−42:1 DEDENT

219−42:1 DEDENT

220−42:1 NEWLINE

221−42:1 glyph ++

222−42:4 name many-bind

223−42:14 glyph |=

224−42:17 name x

225−42:18 tight glyph =

226−42:19 tight name choice

227−43:3 INDENT

228−43:3 glyph ?-

229−43:6 name x

230−44:5 INDENT

231−44:5 name value

232−44:11 str "anything"

233−45:5 NEWLINE

234−45:5 lit %other

235−45:12 str "dead"

236−45:18 DEDENT

237−45:18 DEDENT

238−45:18 NEWLINE

168+30:3 glyph [

169+30:4 tight lit %a

170+30:7 name on

171+30:9 tight glyph =

172+30:10 tight glyph ?

173+30:11 tight glyph ]

174+31:3 NEWLINE

175+31:3 lit %other

176+32:1 DEDENT

177+32:1 NEWLINE

178+32:1 glyph ++

179+32:4 name missing

180+32:12 glyph |=

181+32:15 name x

182+32:16 tight glyph =

183+32:17 tight name choice

184+33:3 INDENT

185+33:3 glyph ?-

186+33:6 name x

187+34:5 INDENT

188+34:5 glyph [

189+34:6 tight lit %a

190+34:9 lit %.y

191+34:12 tight glyph ]

192+34:14 str "yes"

193+35:5 NEWLINE

194+35:5 lit %other

195+35:12 str "other"

196+36:1 DEDENT

197+36:1 DEDENT

198+36:1 NEWLINE

199+36:1 glyph ++

200+36:4 name typed

201+36:10 glyph |=

202+36:13 name x

203+36:14 tight glyph =

204+36:15 tight name choice

205+37:3 INDENT

206+37:3 glyph ?-

207+37:6 name x

208+38:5 INDENT

209+38:5 glyph [

210+38:6 tight lit %a

211+38:9 name value

212+38:14 tight glyph ]

213+38:16 name value

214+39:5 NEWLINE

215+39:5 lit %other

216+39:12 lit %.n

217+40:1 DEDENT

218+40:1 DEDENT

219+40:1 NEWLINE

220+40:1 glyph ++

221+40:4 name duplicate

222+40:14 glyph |=

223+40:17 name x

224+40:18 tight glyph =

225+40:19 tight name choice

226+41:3 INDENT

227+41:3 glyph ?-

228+41:6 name x

229+42:5 INDENT

230+42:5 glyph [

231+42:6 tight lit %a

232+42:9 lit %.y

233+42:12 tight glyph ]

234+42:14 str "yes"

235+43:5 NEWLINE

236+43:5 glyph [

237+43:6 tight lit %a

238+43:9 lit %$

239+43:11 tight glyph ]

240+43:13 str "duplicate"

241+44:5 NEWLINE

242+44:5 glyph *

243+44:7 str "other"

244+45:1 DEDENT

245+45:1 DEDENT

246+45:1 NEWLINE

247+45:1 glyph ++

248+45:4 name shadow

249+45:11 glyph |=

250+45:14 name x

251+45:15 tight glyph =

252+45:16 tight name choice

253+46:3 INDENT

254+46:3 glyph ?-

255+46:6 name x

256+47:5 INDENT

257+47:5 glyph [

258+47:6 tight lit %a

259+47:9 name missing

260+47:16 tight glyph ]

261+47:18 str "yes"

262+48:5 NEWLINE

263+48:5 lit %other

264+48:12 str "other"

265+49:1 DEDENT

266+49:1 DEDENT

267+49:1 NEWLINE

268+49:1 glyph ++

269+49:4 name many-bind

270+49:14 glyph |=

271+49:17 name x

272+49:18 tight glyph =

273+49:19 tight name choice

274+50:3 INDENT

275+50:3 glyph ?-

276+50:6 name x

277+51:5 INDENT

278+51:5 name value

279+51:11 str "anything"

280+52:5 NEWLINE

281+52:5 lit %other

282+52:12 str "dead"

283+52:18 DEDENT

284+52:18 DEDENT

285+52:18 NEWLINE

tests/golden/types-union-finite/tree.txt+99−78

@@ -25,86 +25,107 @@

2525 (cell 9:5 (lit 9:6 %p) (lit 9:9 %.n) (lit 9:13 %.n))

2626 (str 9:18 "d"))

2727 (arm 10:5 (lit 10:5 %other) (str 10:12 "e"))))))

28− (value 11:1 wildcard

29− (gate 11:13

30− (face 11:16 m (ref 11:18 msg))

28+ (value 11:1 parent

29+ (gate 11:11

30+ (face 11:14 m (ref 11:16 msg))

3131 (body 12:3

3232 (branch 12:3

3333 (wing 12:6 m)

3434 (arm 13:5

35− (cell 13:5 (lit 13:6 %p) (lit 13:9 %.y) (any 13:13))

36− (str 13:16 "a"))

35+ (cell 13:5 (lit 13:6 %p) (lit 13:9 %.y) (lit 13:13 %.y))

36+ (lit 13:18 0x1f))

3737 (arm 14:5

38− (cell 14:5 (lit 14:6 %p) (lit 14:9 %.n) (any 14:13))

39− (str 14:16 "b"))

40− (arm 15:5 (lit 15:5 %other) (str 15:12 "e"))))))

41− (value 16:1 covered

42− (gate 16:12

43− (face 16:15 m (ref 16:17 msg))

44− (body 17:3

45− (branch 17:3

46− (wing 17:6 m)

47− (arm 18:5

48− (cell 18:5 (lit 18:6 %p) (lit 18:9 %.y) (any 18:13))

49− (str 18:16 "a"))

50− (arm 19:5

51− (cell 19:5 (lit 19:6 %p) (lit 19:9 %.y) (lit 19:13 %.n))

52− (str 19:18 "b"))

53− (arm 20:5 (any 20:5) (str 20:7 "e"))))))

54− (mold 22:1 choice

55− (union 23:3

56− (cell 23:3

57− (const 23:4 %a)

58− (face 23:7 on (flag 23:10)))

59− (const 24:3 %other)))

60− (value 25:1 missing

61− (gate 25:12

62− (face 25:15 x (ref 25:17 choice))

63− (body 26:3

64− (branch 26:3

65− (wing 26:6 x)

66− (arm 27:5

67− (cell 27:5 (lit 27:6 %a) (lit 27:9 %.y))

68− (str 27:14 "yes"))

69− (arm 28:5 (lit 28:5 %other) (str 28:12 "other"))))))

70− (value 29:1 typed

71− (gate 29:10

72− (face 29:13 x (ref 29:15 choice))

73− (body 30:3

74− (branch 30:3

75− (wing 30:6 x)

76− (arm 31:5

77− (cell 31:5 (lit 31:6 %a) (bind 31:9 value))

78− (wing 31:16 value))

79− (arm 32:5 (lit 32:5 %other) (lit 32:12 %.n))))))

80− (value 33:1 duplicate

81− (gate 33:14

82− (face 33:17 x (ref 33:19 choice))

83− (body 34:3

84− (branch 34:3

85− (wing 34:6 x)

86− (arm 35:5

87− (cell 35:5 (lit 35:6 %a) (lit 35:9 %.y))

88− (str 35:14 "yes"))

89− (arm 36:5

90− (cell 36:5 (lit 36:6 %a) (lit 36:9 %$))

91− (str 36:13 "duplicate"))

92− (arm 37:5 (any 37:5) (str 37:7 "other"))))))

93− (value 38:1 shadow

94− (gate 38:11

95− (face 38:14 x (ref 38:16 choice))

96− (body 39:3

97− (branch 39:3

98− (wing 39:6 x)

99− (arm 40:5

100− (cell 40:5 (lit 40:6 %a) (bind 40:9 missing))

101− (str 40:18 "yes"))

102− (arm 41:5 (lit 41:5 %other) (str 41:12 "other"))))))

103− (value 42:1 many-bind

104− (gate 42:14

105− (face 42:17 x (ref 42:19 choice))

106− (body 43:3

107− (branch 43:3

108− (wing 43:6 x)

109− (arm 44:5 (bind 44:5 value) (str 44:11 "anything"))

110− (arm 45:5 (lit 45:5 %other) (str 45:12 "dead")))))))

38+ (cell 14:5 (lit 14:6 %p) (lit 14:9 %.y) (lit 14:13 %.n))

39+ (cast 14:18 (aura 14:21 @u) (lit 14:24 0x1f)))

40+ (arm 15:5

41+ (cell 15:5 (lit 15:6 %p) (lit 15:9 %.n) (lit 15:13 %.y))

42+ (lit 15:18 0))

43+ (arm 16:5

44+ (cell 16:5 (lit 16:6 %p) (lit 16:9 %.n) (lit 16:13 %.n))

45+ (lit 16:18 0x2f))

46+ (arm 17:5

47+ (lit 17:5 %other)

48+ (cast 17:12 (aura 17:15 @u) (lit 17:18 0x1f)))))))

49+ (value 18:1 wildcard

50+ (gate 18:13

51+ (face 18:16 m (ref 18:18 msg))

52+ (body 19:3

53+ (branch 19:3

54+ (wing 19:6 m)

55+ (arm 20:5

56+ (cell 20:5 (lit 20:6 %p) (lit 20:9 %.y) (any 20:13))

57+ (str 20:16 "a"))

58+ (arm 21:5

59+ (cell 21:5 (lit 21:6 %p) (lit 21:9 %.n) (any 21:13))

60+ (str 21:16 "b"))

61+ (arm 22:5 (lit 22:5 %other) (str 22:12 "e"))))))

62+ (value 23:1 covered

63+ (gate 23:12

64+ (face 23:15 m (ref 23:17 msg))

65+ (body 24:3

66+ (branch 24:3

67+ (wing 24:6 m)

68+ (arm 25:5

69+ (cell 25:5 (lit 25:6 %p) (lit 25:9 %.y) (any 25:13))

70+ (str 25:16 "a"))

71+ (arm 26:5

72+ (cell 26:5 (lit 26:6 %p) (lit 26:9 %.y) (lit 26:13 %.n))

73+ (str 26:18 "b"))

74+ (arm 27:5 (any 27:5) (str 27:7 "e"))))))

75+ (mold 29:1 choice

76+ (union 30:3

77+ (cell 30:3

78+ (const 30:4 %a)

79+ (face 30:7 on (flag 30:10)))

80+ (const 31:3 %other)))

81+ (value 32:1 missing

82+ (gate 32:12

83+ (face 32:15 x (ref 32:17 choice))

84+ (body 33:3

85+ (branch 33:3

86+ (wing 33:6 x)

87+ (arm 34:5

88+ (cell 34:5 (lit 34:6 %a) (lit 34:9 %.y))

89+ (str 34:14 "yes"))

90+ (arm 35:5 (lit 35:5 %other) (str 35:12 "other"))))))

91+ (value 36:1 typed

92+ (gate 36:10

93+ (face 36:13 x (ref 36:15 choice))

94+ (body 37:3

95+ (branch 37:3

96+ (wing 37:6 x)

97+ (arm 38:5

98+ (cell 38:5 (lit 38:6 %a) (bind 38:9 value))

99+ (wing 38:16 value))

100+ (arm 39:5 (lit 39:5 %other) (lit 39:12 %.n))))))

101+ (value 40:1 duplicate

102+ (gate 40:14

103+ (face 40:17 x (ref 40:19 choice))

104+ (body 41:3

105+ (branch 41:3

106+ (wing 41:6 x)

107+ (arm 42:5

108+ (cell 42:5 (lit 42:6 %a) (lit 42:9 %.y))

109+ (str 42:14 "yes"))

110+ (arm 43:5

111+ (cell 43:5 (lit 43:6 %a) (lit 43:9 %$))

112+ (str 43:13 "duplicate"))

113+ (arm 44:5 (any 44:5) (str 44:7 "other"))))))

114+ (value 45:1 shadow

115+ (gate 45:11

116+ (face 45:14 x (ref 45:16 choice))

117+ (body 46:3

118+ (branch 46:3

119+ (wing 46:6 x)

120+ (arm 47:5

121+ (cell 47:5 (lit 47:6 %a) (bind 47:9 missing))

122+ (str 47:18 "yes"))

123+ (arm 48:5 (lit 48:5 %other) (str 48:12 "other"))))))

124+ (value 49:1 many-bind

125+ (gate 49:14

126+ (face 49:17 x (ref 49:19 choice))

127+ (body 50:3

128+ (branch 50:3

129+ (wing 50:6 x)

130+ (arm 51:5 (bind 51:5 value) (str 51:11 "anything"))

131+ (arm 52:5 (lit 52:5 %other) (str 52:12 "dead")))))))

tests/golden/types-union-finite/types.txt+3−2

@@ -1,16 +1,17 @@

11partial inference; module not checked

22+$ msg: cases proven disjoint; mold not checked

33++ boolean-table: $-(msg @t)

4+++ parent: $-(msg @u)

45++ wildcard: $-(msg @t)

56++ covered: branch arm is covered by earlier arms

6−/tests/golden/types-union-finite/source.jibb:19:5: covered arm

7+/tests/golden/types-union-finite/source.jibb:26:5: covered arm

78 [%p %.y %.n] "b"

89 ^

910+$ choice: cases proven disjoint; mold not checked

1011++ missing: missing union case [%a on=%.n]

1112++ typed: $-(choice ?)

1213++ duplicate: branch arm is covered by earlier arms

13−/tests/golden/types-union-finite/source.jibb:36:5: covered arm

14+/tests/golden/types-union-finite/source.jibb:43:5: covered arm

1415 [%a %$] "duplicate"

1516 ^

1617++ shadow: pattern binder shadows a name

tests/golden/types-union-patterns-generic/about.txt+1−1

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

11source: Grammar, Patterns: "Every case needs an arm or a catch-all"; Molds: "Type variables are capitals, generalized per `++`."

2−tests: Matching generic union cases preserves shared payload variables and concrete payload types. Different result variables, partial patterns, unresolved result tags and an explicit capital forced concrete remain unsupported. The same binder name can be reused in separate arms, and a duplicate arm is dead.

2+tests: Matching generic union cases preserves shared payload variables and concrete payload types. Distinct result variables are diagnosed rather than forced equal; partial patterns, unresolved result tags and an explicit capital forced concrete remain unsupported. The same binder name can be reused in separate arms, and a duplicate arm is dead.

33expect: parses

44expect-types: a partial inference report

tests/golden/types-union-patterns-generic/types.txt+7−1

@@ -7,7 +7,13 @@ partial inference; module not checked

77 [%ok again] again

88 ^

99++ nested: partial union pattern is not supported by partial inference

10−++ different: union branch result matching needs unsupported inference

10+++ different: distinct type variables `A` and `B` must not be forced equal; use the same capital for a shared type

11+/tests/golden/types-union-patterns-generic/source.jibb:21:27: first type variable

12+++ different |= r=(result A B)

13+ ^

14+/tests/golden/types-union-patterns-generic/source.jibb:21:29: second type variable

15+++ different |= r=(result A B)

16+ ^

1117++ forced: explicit capital constraints are not supported by partial inference

1218++ reused: $-((result A A) A)

1319++ pending: union branch result matching needs unsupported inference

tests/lib/jibb-deferred.hoon+10

@@ -47,6 +47,15 @@

4747 ?:(?=([%atom %t] typ.u.text) 'text use inferred' 'BAD-text-type')

4848 ?:(?=([%atom %p] typ.u.ship) 'ship use inferred independently' 'BAD-ship-type')

4949 ==

50+++ case-branch

51+ ^- (list @t)

52+ =/ source=@t '++ choose |= b=?\0a ?- b\0a %.y 0x1f\0a %.n ^- @u 0x1f\0a'

53+ =/ result=(unit dgcommit:jibb) (checked-source /ui/branch/jibb source)

54+ ?~ result ~['BAD-deferred-branch']

55+ =/ choose=(unit ischeme:jibb) (ienv-lookup:jibb %choose env.u.result)

56+ ?~ choose ~['BAD-deferred-branch-export']

57+ :~ ?:(=(typ.u.choose [%fn [%flag ~] [%atom %u]]) 'deferred branch joins present parent' 'BAD-deferred-branch-type')

58+ ==

5059++ case-negative

5160 |= [missing=@t conflict=@t duplicate=@t hole=@t]

5261 ^- (list @t)

@@ -226,6 +235,7 @@

226235 ^- @t

227236 =/ lines=(list @t) (case-nested nested-src)

228237 =. lines (weld lines (case-principal principal-src))

238+ =. lines (weld lines case-branch)

229239 =. lines (weld lines (case-negative missing-src conflict-src duplicate-src hole-src))

230240 =. lines (weld lines (case-groups local-src mutual-src))

231241 =. lines (weld lines (case-mold-hole mold-hole-src))

tests/type-deferred/expected.txt+1

@@ -4,6 +4,7 @@ nested obligation discharged

44independent built result stays polymorphic

55text use inferred

66ship use inferred independently

7+deferred branch joins present parent

78missing constructor leaves no result

89conflicting context leaves no result

910duplicate source binding declined