38c711c · jibb · git.iko.soy

docs/compiler.md+3−1

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

58

59The 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.

60

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+

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

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

62

64

63The 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.

65The 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

224

226

225In 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.

227In 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.

226

228

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.

228

230

229With 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.

231With 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.

230

232

docs/status.md+4−2

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

61

62Imported 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.

63

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+

64The 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.

66The 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.

65

67

66The 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.

68The 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:

117

119

118Besides the plan's list:

120Besides the plan's list:

119

121

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.

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.

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.

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.

122- `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.

124- `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.

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

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

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

126- 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 @@

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

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

5133 ~

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

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

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

5136 ~

5137::

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

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

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

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

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

5140:: variable-dependent face merges stay unresolved.

5214:: variable-dependent face merges stay unresolved.

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

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

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

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

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

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

8028 ?^ 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)

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

8030 ?~ 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)]

7958::

8032::

7959++ infer-unit-branch

8033++ infer-unit-branch

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

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

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

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

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

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

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

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

8072 ?^ 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)

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

8074 ?~ 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)]

8002::

8076::

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

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

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

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

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

8144 =/ remaining=(list itype) cases

8218 =/ remaining=(list itype) cases

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

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

8146 =/ st=istate state.p.subject

8220 =/ st=istate state.p.subject

8147− =/ answer=(unit itype) ~

8221+ =/ results=(list itype) ~

8148 |-

8222 |-

8149 ?~ arms

8223 ?~ arms

8150 ?^ remaining

8224 ?^ remaining

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

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

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

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

8153− `[%& u.answer st]

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

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

8154 =/ a=arm i.arms

8229 =/ a=arm i.arms

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

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

8156 ~

8231 ~

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

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

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

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

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

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

8243 =/ 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])

8172::

8245::

8173++ infer-known-union-context-whole

8246++ infer-known-union-context-whole

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

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

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

8231 =/ remaining=(list ifinite) cases

8304 =/ remaining=(list ifinite) cases

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

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

8233 =/ st=istate state.p.subject

8306 =/ st=istate state.p.subject

8234− =/ answer=(unit itype) ~

8307+ =/ results=(list itype) ~

8235 |-

8308 |-

8236 ?~ arms

8309 ?~ arms

8237 ?^ remaining

8310 ?^ remaining

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

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

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

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

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

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

8241− [%& 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)]

8242 =/ a=arm i.arms

8317 =/ a=arm i.arms

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

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

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

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

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

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

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

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

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

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

8343 [%| ["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])

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

8345 =/ 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])

8274::

8347::

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

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

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

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

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

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

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

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

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

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

8918 =/ 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)

8849 ?~ joined

8920 ?~ joined

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

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

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

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

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

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

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

8924 [%| ["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]

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

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

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

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

8858 ?: |((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))

8927 ?: |((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))

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

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

8860 [%| ["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)]]]]

8929 [%| ["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)]

8862 %cast

8931 %cast

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

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

8864 ?~ target

8933 ?~ target

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

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

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

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

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

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

15364 ?: ?=(%| -.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)]

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

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

15297 =/ st=istate state.p.right

15368 =/ st=istate state.p.right

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

15369 ?. (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

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

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

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

11++ 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 @@

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

3expect: parses

4expect-types: a partial inference report

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

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

9 ?- xs

10 [item rest] rest

11 ~ !!

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

13+ ?- xs

14+ ~ 0x1f

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

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

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

13 ^- msg

17 ^- msg

14 ?- xs

18 ?- xs

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

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

6012:1 DEDENT

6112:1 NEWLINE

6212:1 glyph ++

63−12:4 name with-context

63+12:4 name parent

64−12:17 glyph |=

64+12:11 glyph |=

65−12:20 name xs

65+12:14 name xs

66−12:22 tight glyph =

66+12:16 tight glyph =

67−12:23 tight glyph (

67+12:17 tight glyph (

68−12:24 tight name list

68+12:18 tight name list

69−12:29 aura @t

69+12:23 aura @t

70−12:31 tight glyph )

70+12:25 tight glyph )

7113:3 INDENT

72−13:3 glyph ^-

72+13:3 glyph ?-

73−13:6 name msg

73+13:6 name xs

7414:5 INDENT

75−14:5 glyph ?-

75+14:5 lit ~

76−14:8 name xs

77−15:7 INDENT

78−15:7 lit ~

76+14:7 lit 0x1f

79−15:9 lit %empty

80−16:7 NEWLINE

77+15:5 NEWLINE

81−16:7 glyph [

78+15:5 glyph [

82−16:8 tight name item

79+15:6 tight name item

83−16:13 name rest

80+15:11 name rest

84−16:17 tight glyph ]

81+15:15 tight glyph ]

85−16:19 glyph [

82+15:17 glyph ^-

86−16:20 tight lit %item

83+15:20 aura @u

87−16:26 name item

84+15:23 lit 0x1f

88−16:30 tight glyph ]

89−17:1 DEDENT

85+16:1 DEDENT

90−17:1 DEDENT

91−17:1 DEDENT

86+16:1 DEDENT

92−17:1 NEWLINE

87+16:1 NEWLINE

93−17:1 glyph ++

88+16:1 glyph ++

94−17:4 name shadow

89+16:4 name with-context

95−17:11 glyph |=

90+16:17 glyph |=

96−17:14 name xs

91+16:20 name xs

97−17:16 tight glyph =

92+16:22 tight glyph =

98−17:17 tight glyph (

93+16:23 tight glyph (

99−17:18 tight name list

94+16:24 tight name list

100−17:23 aura @t

95+16:29 aura @t

101−17:25 tight glyph )

96+16:31 tight glyph )

102−18:3 INDENT

97+17:3 INDENT

103−18:3 glyph ?-

98+17:3 glyph ^-

99+17:6 name msg

100+18:5 INDENT

101+18:5 glyph ?-

104−18:6 name xs

102+18:8 name xs

105−19:5 INDENT

103+19:7 INDENT

106−19:5 lit ~

104+19:7 lit ~

107−19:7 glyph !!

105+19:9 lit %empty

108−20:5 NEWLINE

106+20:7 NEWLINE

109−20:5 glyph [

107+20:7 glyph [

110−20:6 tight name xs

108+20:8 tight name item

111−20:9 name rest

109+20:13 name rest

112−20:13 tight glyph ]

110+20:17 tight glyph ]

113−20:15 name xs

111+20:19 glyph [

112+20:20 tight lit %item

113+20:26 name item

114+20:30 tight glyph ]

115+21:1 DEDENT

11421:1 DEDENT

11621:1 DEDENT

11521:1 DEDENT

11721:1 DEDENT

11621:1 NEWLINE

11821:1 NEWLINE

11721:1 glyph ++

11921:1 glyph ++

118−21:4 name duplicate

120+21:4 name shadow

119−21:14 glyph |=

121+21:11 glyph |=

120−21:17 name xs

122+21:14 name xs

121−21:19 tight glyph =

123+21:16 tight glyph =

122−21:20 tight glyph (

124+21:17 tight glyph (

123−21:21 tight name list

125+21:18 tight name list

124−21:26 aura @t

126+21:23 aura @t

125−21:28 tight glyph )

127+21:25 tight glyph )

12622:3 INDENT

12822:3 INDENT

12722:3 glyph ?-

12922:3 glyph ?-

12822:6 name xs

13022:6 name xs

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

13123:7 glyph !!

13323:7 glyph !!

13224:5 NEWLINE

13424:5 NEWLINE

13324:5 glyph [

13524:5 glyph [

134−24:6 tight name item

136+24:6 tight name xs

135−24:11 name item

137+24:9 name rest

136−24:15 tight glyph ]

138+24:13 tight glyph ]

137−24:17 name item

139+24:15 name xs

13825:1 DEDENT

14025:1 DEDENT

13925:1 DEDENT

14125:1 DEDENT

14025:1 NEWLINE

14225:1 NEWLINE

14125:1 glyph ++

14325:1 glyph ++

142−25:4 name unknown

144+25:4 name duplicate

143−25:12 glyph |=

145+25:14 glyph |=

144−25:15 name xs

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 )

14526:3 INDENT

15226:3 INDENT

14626:3 glyph ?-

15326:3 glyph ?-

14726:6 name xs

15426:6 name xs

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

15128:5 NEWLINE

15828:5 NEWLINE

15228:5 glyph [

15928:5 glyph [

15328:6 tight name item

16028:6 tight name item

154−28:11 name rest

161+28:11 name item

15528:15 tight glyph ]

16228:15 tight glyph ]

15628:17 name item

16328:17 name item

15729:1 DEDENT

16429:1 DEDENT

15829:1 DEDENT

16529:1 DEDENT

15929:1 NEWLINE

16629:1 NEWLINE

16029:1 glyph ++

16729:1 glyph ++

161−29:4 name not-list

168+29:4 name unknown

162−29:13 glyph |=

169+29:12 glyph |=

163−29:16 name xs

170+29:15 name xs

164−29:18 tight glyph =

165−29:19 tight aura @t

16630:3 INDENT

17130:3 INDENT

16730:3 glyph ?-

17230:3 glyph ?-

16830:6 name xs

17330:6 name xs

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

17933:1 DEDENT

18433:1 DEDENT

18033:1 NEWLINE

18533:1 NEWLINE

18133:1 glyph ++

18633:1 glyph ++

182−33:4 name missing

187+33:4 name not-list

183−33:12 glyph |=

188+33:13 glyph |=

184−33:15 name xs

189+33:16 name xs

185−33:17 tight glyph =

190+33:18 tight glyph =

186−33:18 tight glyph (

187−33:19 tight name list

191+33:19 tight aura @t

188−33:24 aura @t

189−33:26 tight glyph )

19034:3 INDENT

19234:3 INDENT

19134:3 glyph ?-

19334:3 glyph ?-

19234:6 name xs

19434:6 name xs

19335:5 INDENT

19535:5 INDENT

19435:5 lit ~

19635:5 lit ~

19535:7 glyph !!

19735:7 glyph !!

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

196−36:1 DEDENT

204+37:1 DEDENT

197−36:1 DEDENT

205+37:1 DEDENT

198−36:1 NEWLINE

206+37:1 NEWLINE

199−36:1 glyph ++

207+37:1 glyph ++

200−36:4 name invalid

208+37:4 name missing

201−36:12 glyph |=

209+37:12 glyph |=

202−36:15 name xs

210+37:15 name xs

203−36:17 tight glyph =

211+37:17 tight glyph =

204−36:18 tight glyph (

212+37:18 tight glyph (

205−36:19 tight name list

213+37:19 tight name list

206−36:24 aura @t

214+37:24 aura @t

207−36:26 tight glyph )

215+37:26 tight glyph )

208−37:3 INDENT

216+38:3 INDENT

209−37:3 glyph ?-

217+38:3 glyph ?-

210−37:6 name xs

218+38:6 name xs

211−38:5 INDENT

219+39:5 INDENT

212−38:5 lit ~

220+39:5 lit ~

213−38:7 glyph !!

221+39: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

22040:1 DEDENT

22240:1 DEDENT

22140:1 DEDENT

22340:1 DEDENT

22240:1 NEWLINE

22440:1 NEWLINE

22340:1 glyph ++

22540:1 glyph ++

224−40:4 name unresolved

226+40:4 name invalid

225−40:15 glyph |=

227+40:12 glyph |=

226−40:18 name xs

228+40:15 name xs

227−40:20 tight glyph =

229+40:17 tight glyph =

228−40:21 tight glyph (

230+40:18 tight glyph (

229−40:22 tight name list

231+40:19 tight name list

230−40:27 aura @t

232+40:24 aura @t

231−40:29 tight glyph )

233+40:26 tight glyph )

23241:3 INDENT

23441:3 INDENT

23341:3 glyph ?-

23541:3 glyph ?-

23441:6 name xs

23641:6 name xs

23542:5 INDENT

23742:5 INDENT

23642:5 lit ~

23842:5 lit ~

237−42:7 lit %empty

239+42:7 glyph !!

23843:5 NEWLINE

24043:5 NEWLINE

23943:5 glyph [

24143:5 glyph [

240−43:6 tight name item

242+43:6 tight lit %tag

24143:11 name rest

24343:11 name rest

24243:15 tight glyph ]

24443:15 tight glyph ]

243−43:17 lit %more

245+43:17 name rest

24444:1 DEDENT

24644:1 DEDENT

24544:1 DEDENT

24744:1 DEDENT

24644:1 NEWLINE

24844:1 NEWLINE

24744:1 glyph ++

24944:1 glyph ++

248−44:4 name duplicate-arm

250+44:4 name unresolved

249−44:18 glyph |=

251+44:15 glyph |=

250−44:21 name xs

252+44:18 name xs

251−44:23 tight glyph =

253+44:20 tight glyph =

252−44:24 tight glyph (

254+44:21 tight glyph (

253−44:25 tight name list

255+44:22 tight name list

254−44:30 aura @t

256+44:27 aura @t

255−44:32 tight glyph )

257+44:29 tight glyph )

25645:3 INDENT

25845:3 INDENT

25745:3 glyph ?-

25945:3 glyph ?-

25845:6 name xs

26045:6 name xs

25946:5 INDENT

26146:5 INDENT

26046:5 lit ~

26246:5 lit ~

261−46:7 glyph !!

263+46:7 lit %empty

26247:5 NEWLINE

26447:5 NEWLINE

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

263−47:5 lit ~

286+50:5 lit ~

264−47:7 glyph !!

287+50:7 glyph !!

265−48:5 NEWLINE

288+51:5 NEWLINE

289+51:5 lit ~

266−48:5 glyph [

290+51:7 glyph !!

291+52:5 NEWLINE

292+52:5 glyph [

267−48:6 tight name item

293+52:6 tight name item

268−48:11 name rest

294+52:11 name rest

269−48:15 tight glyph ]

295+52:15 tight glyph ]

270−48:17 name item

296+52:17 name item

271−49:1 DEDENT

297+53:1 DEDENT

272−49:1 DEDENT

298+53:1 DEDENT

273−49:1 NEWLINE

299+53:1 NEWLINE

274−49:1 glyph ++

300+53:1 glyph ++

275−49:4 name unrelated

301+53:4 name unrelated

276−49:14 glyph |=

302+53:14 glyph |=

277−49:17 name xs

303+53:17 name xs

278−49:19 tight glyph =

304+53:19 tight glyph =

279−49:20 tight glyph (

305+53:20 tight glyph (

280−49:21 tight name list

306+53:21 tight name list

281−49:26 aura @t

307+53:26 aura @t

282−49:28 tight glyph )

308+53:28 tight glyph )

283−50:3 INDENT

309+54:3 INDENT

284−50:3 glyph ~&

310+54:3 glyph ~&

285−50:6 lit %pending

311+54:6 lit %pending

286−51:5 INDENT

312+55:5 INDENT

287−51:5 glyph ?-

313+55:5 glyph ?-

288−51:8 name xs

314+55:8 name xs

289−52:7 INDENT

315+56:7 INDENT

290−52:7 lit ~

316+56:7 lit ~

291−52:9 glyph !!

317+56:9 glyph !!

292−53:7 NEWLINE

318+57:7 NEWLINE

293−53:7 glyph [

319+57:7 glyph [

294−53:8 tight name item

320+57:8 tight name item

295−53:13 name rest

321+57:13 name rest

296−53:17 tight glyph ]

322+57:17 tight glyph ]

297−53:19 name item

323+57:19 name item

298−54:1 DEDENT

299−54:1 DEDENT

300−54:1 DEDENT

324+58: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

32358:1 DEDENT

32558:1 DEDENT

32458:1 DEDENT

32658:1 DEDENT

32558:1 NEWLINE

32758:1 NEWLINE

326−58:1 glyph +$

328+58:1 glyph ++

327−58:4 name maybe

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 )

32859:3 INDENT

33759:3 INDENT

338+59:3 glyph ?-

339+59:6 name xs

340+60:5 INDENT

329−59:3 lit ~

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 ~

330−60:3 NEWLINE

356+64:3 NEWLINE

331−60:3 glyph [

357+64:3 glyph [

332−60:4 tight lit ~

358+64:4 tight lit ~

333−60:6 name value

359+64:6 name value

334−60:11 tight glyph =

360+64:11 tight glyph =

335−60:12 tight aura @t

361+64:12 tight aura @t

336−60:14 tight glyph ]

362+64:14 tight glyph ]

337−61:1 DEDENT

363+65:1 DEDENT

338−61:1 NEWLINE

364+65:1 NEWLINE

339−61:1 glyph ++

365+65:1 glyph ++

340−61:4 name unit-shape

366+65:4 name unit-shape

341−61:15 glyph |=

367+65:15 glyph |=

342−61:18 name xs

368+65:18 name xs

343−61:20 tight glyph =

369+65:20 tight glyph =

344−61:21 tight name maybe

370+65:21 tight name maybe

345−62:3 INDENT

371+66:3 INDENT

346−62:3 glyph ?-

372+66:3 glyph ?-

347−62:6 name xs

373+66:6 name xs

348−63:5 INDENT

374+67:5 INDENT

349−63:5 lit ~

375+67:5 lit ~

350−63:7 glyph !!

376+67:7 glyph !!

351−64:5 NEWLINE

377+68:5 NEWLINE

352−64:5 glyph [

378+68:5 glyph [

353−64:6 tight name item

379+68:6 tight name item

354−64:11 name rest

380+68:11 name rest

355−64:15 tight glyph ]

381+68:15 tight glyph ]

356−64:17 name item

382+68:17 name item

357−64:21 DEDENT

383+68:21 DEDENT

358−64:21 DEDENT

384+68:21 DEDENT

359−64:21 NEWLINE

385+68:21 NEWLINE

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

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

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

28 (wing 10:17 rest))

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

30− (value 12:1 with-context

30+ (value 12:1 parent

31− (gate 12:17

31+ (gate 12:11

32− (face 12:20 xs

32+ (face 12:14 xs

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

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

34 (body 13:3

35− (cast 13:3

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

36− (ref 13:6 msg)

47+ (ref 17:6 msg)

37− (body 14:5

48+ (body 18:5

38− (branch 14:5

49+ (branch 18:5

39− (wing 14:8 xs)

50+ (wing 18:8 xs)

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

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

41− (arm 16:7

52+ (arm 20:7

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

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

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

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

44− (value 17:1 shadow

55+ (value 21:1 shadow

45− (gate 17:11

56+ (gate 21:11

46− (face 17:14 xs

57+ (face 21: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)))

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

59 (body 22:3

60 (branch 22:3

61 (wing 22:6 xs)

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

63 (arm 24:5

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

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

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

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

66− (value 25:1 unknown

66+ (value 25:1 duplicate

67− (gate 25:12

67+ (gate 25:14

68− (bind 25:15 xs)

68+ (face 25:17 xs

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

69 (body 26:3

70 (body 26:3

70 (branch 26:3

71 (branch 26:3

71 (wing 26:6 xs)

72 (wing 26:6 xs)

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

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

73 (arm 28:5

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

75 (wing 28:17 item))))))

76 (wing 28:17 item))))))

76− (value 29:1 not-list

77+ (value 29:1 unknown

77− (gate 29:13

78+ (gate 29:12

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

79+ (bind 29:15 xs)

79 (body 30:3

80 (body 30:3

80 (branch 30:3

81 (branch 30:3

81 (wing 30:6 xs)

82 (wing 30:6 xs)

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

83 (arm 32:5

84 (arm 32:5

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

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

85 (wing 32:17 item))))))

86 (wing 32:17 item))))))

86− (value 33:1 missing

87+ (value 33:1 not-list

87− (gate 33:12

88+ (gate 33:13

88− (face 33:15 xs

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

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

90 (body 34:3

91 (branch 34:3

92 (wing 34:6 xs)

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

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

94− (value 36:1 invalid

94+ (arm 36:5

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

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

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

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

105− (value 40:1 unresolved

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

106+ (gate 40:12

107− (face 40:18 xs

107+ (face 40:15 xs

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

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

109 (body 41:3

110 (branch 41:3

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

113 (arm 43:5

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

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

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

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

116− (value 44:1 duplicate-arm

116+ (value 44:1 unresolved

117− (gate 44:18

117+ (gate 44:15

118− (face 44:21 xs

118+ (face 44:18 xs

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

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

120 (body 45:3

121 (branch 45:3

122 (wing 45:6 xs)

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

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

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

124+ (arm 47:5

125− (arm 48: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

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

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

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

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

128− (value 49:1 unrelated

139+ (value 53:1 unrelated

129− (gate 49:14

140+ (gate 53:14

130− (face 49:17 xs

141+ (face 53:17 xs

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

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

132− (body 50:3

143+ (body 54:3

133− (trace 50:3

144+ (trace 54:3

134− (lit 50:6 %pending)

145+ (lit 54:6 %pending)

135− (body 51:5

146+ (body 55:5

136− (branch 51:5

147+ (branch 55:5

137− (wing 51:8 xs)

148+ (wing 55:8 xs)

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

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

139− (arm 53:7

150+ (arm 57:7

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

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

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

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

142− (value 54:1 empty-elements

153+ (value 58:1 empty-elements

143− (gate 54:19

154+ (gate 58:19

144− (face 54:22 xs

155+ (face 58:22 xs

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

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

146− (body 55:3

157+ (body 59:3

147− (branch 55:3

158+ (branch 59:3

148− (wing 55:6 xs)

159+ (wing 59:6 xs)

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

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

150− (arm 57:5

161+ (arm 61:5

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

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

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

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

153− (mold 58:1 maybe

164+ (mold 62:1 maybe

154− (union 59:3

165+ (union 63:3

155− (const 59:3 ~)

166+ (const 63:3 ~)

156− (cell 60:3

167+ (cell 64:3

157− (const 60:4 ~)

168+ (const 64:4 ~)

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

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

159− (value 61:1 unit-shape

170+ (value 65:1 unit-shape

160− (gate 61:15

171+ (gate 65:15

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

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

162− (body 62:3

173+ (body 66:3

163− (branch 62:3

174+ (branch 66:3

164− (wing 62:6 xs)

175+ (wing 66:6 xs)

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

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

166− (arm 64:5

177+ (arm 68:5

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

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

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

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

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

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

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

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

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

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

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

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

6++ shadow: pattern binder shadows a name

7++ shadow: pattern binder shadows a name

7++ duplicate: pattern binder shadows a name

8++ duplicate: pattern binder shadows a name

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

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

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

3expect: parses

4expect-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

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

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

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

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

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

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

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

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

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

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

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

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

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

21 ++ recur |= y (recur recur)

22 ^

23−++ captures: local definitions need unsupported inference

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

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

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

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

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

3expect: parses

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

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

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

10 ?- b

11 %.y ^- @ ~zod

12 %.n "hi"

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

14+ ?- b

15+ %.y ^- @ ~zod

16+ %.n 0

13++ unknown |= x

17++ unknown |= x

14 ?- %.y

18 ?- %.y

15 %.y x

19 %.y x

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

18 ?- b

22 ?- b

19 %.y ^- @ud 1

23 %.y ^- @ud 1

20 %.n 0x1f

24 %.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 @@

5913:1 DEDENT

6013:1 NEWLINE

6113:1 glyph ++

62−13:4 name unknown

62+13:4 name atom-decimal

63−13:12 glyph |=

63+13:17 glyph |=

64−13:15 name x

64+13:20 name b

65+13:21 tight glyph =

66+13:22 tight glyph ?

6514:3 INDENT

6714:3 INDENT

6614:3 glyph ?-

6814:3 glyph ?-

67−14:6 lit %.y

69+14:6 name b

6815:5 INDENT

7015:5 INDENT

6915:5 lit %.y

7115:5 lit %.y

70−15:9 name x

72+15:9 glyph ^-

73+15:12 aura @

74+15:14 lit ~zod

7116:5 NEWLINE

7516:5 NEWLINE

7216:5 lit %.n

7616:5 lit %.n

73−16:9 lit 0x1f

77+16:9 lit 0

7417:1 DEDENT

7817:1 DEDENT

7517:1 DEDENT

7917:1 DEDENT

7617:1 NEWLINE

8017:1 NEWLINE

7717:1 glyph ++

8117:1 glyph ++

78−17:4 name siblings

82+17:4 name unknown

79−17:13 glyph |=

83+17:12 glyph |=

80−17:16 name b

84+17:15 name x

81−17:17 tight glyph =

82−17:18 tight glyph ?

8318:3 INDENT

8518:3 INDENT

8418:3 glyph ?-

8618:3 glyph ?-

85−18:6 name b

87+18:6 lit %.y

8619:5 INDENT

8819:5 INDENT

8719:5 lit %.y

8919:5 lit %.y

88−19:9 glyph ^-

90+19:9 name x

89−19:12 aura @ud

90−19:16 lit 1

9120:5 NEWLINE

9220:5 lit %.n

9320:9 lit 0x1f

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 ]

94−20:13 DEDENT

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

95−20:13 DEDENT

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

96−20:13 NEWLINE

436+75:28 NEWLINE

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

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

29 (lit 11:5 %.y)

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

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

32− (value 13:1 unknown

32+ (value 13:1 atom-decimal

33− (gate 13:12

33+ (gate 13:17

34− (bind 13:15 x)

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

35 (body 14:3

36 (branch 14:3

37− (lit 14:6 %.y)

37+ (wing 14:6 b)

38+ (arm 15:5

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

39+ (lit 15:5 %.y)

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

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

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

40− (value 17:1 siblings

42+ (value 17:1 unknown

41− (gate 17:13

43+ (gate 17:12

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

44+ (bind 17:15 x)

43 (body 18:3

45 (body 18:3

44 (branch 18:3

46 (branch 18:3

45− (wing 18:6 b)

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)

46− (arm 19:5

56+ (arm 23:5

47− (lit 19:5 %.y)

57+ (lit 23:5 %.y)

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

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

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

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

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

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

4++ atom: $-(? @)

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

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

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

6++ siblings: branch arms have incompatible types

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

8 %.y ^- @ud 1

9 %.y ^- @ud 1

9 ^

10 ^

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

11 %.n 0x1f

12 %.n 0x1f

12 ^

13 ^

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

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

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

14 ^

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

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

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

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

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

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

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

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

3expect: parses

4expect-types: a partial inference report

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

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

1partial inference; module not checked

2−++ outer: local definitions need unsupported inference

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

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

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

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

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

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

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

10++ captured: $-(A A)

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

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

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

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

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

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

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

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

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

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

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

47 %.n (aura-conflict b)

48 ^

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

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

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

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

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

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

18++ occurs |= x (x x)

19 ^

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

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

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

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

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

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

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

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

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

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

3expect: parses

4expect-types: a partial inference report

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

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

1partial inference; module not checked

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

3++ 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+ ^

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

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

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

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

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

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

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

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

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

3expect: parses

4expect-types: a partial inference report

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

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

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

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

10 %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

11++ wildcard |= m=msg

18++ wildcard |= m=msg

12 ?- m

19 ?- m

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

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

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

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

5811:1 DEDENT

5911:1 NEWLINE

6011:1 glyph ++

61−11:4 name wildcard

61+11:4 name parent

62−11:13 glyph |=

62+11:11 glyph |=

63−11:16 name m

63+11:14 name m

64−11:17 tight glyph =

64+11:15 tight glyph =

65−11:18 tight name msg

65+11:16 tight name msg

6612:3 INDENT

6712:3 glyph ?-

6812:6 name m

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

7013:5 glyph [

7113:6 tight lit %p

7213:9 lit %.y

73−13:13 glyph *

73+13:13 lit %.y

74−13:14 tight glyph ]

74+13:16 tight glyph ]

75−13:16 str "a"

75+13:18 lit 0x1f

7614:5 NEWLINE

7714:5 glyph [

7814:6 tight lit %p

79−14:9 lit %.n

79+14:9 lit %.y

80−14:13 glyph *

80+14:13 lit %.n

81−14:14 tight glyph ]

81+14:16 tight glyph ]

82−14:16 str "b"

82+14:18 glyph ^-

83+14:21 aura @u

84+14:24 lit 0x1f

8315:5 NEWLINE

8515:5 NEWLINE

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

84−15:5 lit %other

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

85−15:12 str "e"

132+22:12 str "e"

86−16:1 DEDENT

133+23:1 DEDENT

87−16:1 DEDENT

134+23:1 DEDENT

88−16:1 NEWLINE

135+23:1 NEWLINE

89−16:1 glyph ++

136+23:1 glyph ++

90−16:4 name covered

137+23:4 name covered

91−16:12 glyph |=

138+23:12 glyph |=

92−16:15 name m

139+23:15 name m

93−16:16 tight glyph =

140+23:16 tight glyph =

94−16:17 tight name msg

141+23:17 tight name msg

95−17:3 INDENT

142+24:3 INDENT

96−17:3 glyph ?-

143+24:3 glyph ?-

97−17:6 name m

144+24:6 name m

98−18:5 INDENT

145+25:5 INDENT

99−18:5 glyph [

146+25:5 glyph [

100−18:6 tight lit %p

147+25:6 tight lit %p

101−18:9 lit %.y

148+25:9 lit %.y

102−18:13 glyph *

149+25:13 glyph *

103−18:14 tight glyph ]

150+25:14 tight glyph ]

104−18:16 str "a"

151+25:16 str "a"

105−19:5 NEWLINE

152+26:5 NEWLINE

106−19:5 glyph [

153+26:5 glyph [

107−19:6 tight lit %p

154+26:6 tight lit %p

108−19:9 lit %.y

155+26:9 lit %.y

109−19:13 lit %.n

156+26:13 lit %.n

110−19:16 tight glyph ]

157+26:16 tight glyph ]

111−19:18 str "b"

158+26:18 str "b"

112−20:5 NEWLINE

159+27:5 NEWLINE

113−20:5 glyph *

160+27:5 glyph *

114−20:7 str "e"

161+27: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"

14929:1 DEDENT

16229:1 DEDENT

15029:1 DEDENT

16329:1 DEDENT

15129:1 NEWLINE

16429:1 NEWLINE

152−29:1 glyph ++

165+29:1 glyph +$

153−29:4 name typed

166+29:4 name choice

154−29:10 glyph |=

155−29:13 name x

156−29:14 tight glyph =

157−29:15 tight name choice

15830:3 INDENT

16730:3 INDENT

159−30:3 glyph ?-

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

160−30:6 name x

207+37:6 name x

161−31:5 INDENT

208+38:5 INDENT

162−31:5 glyph [

209+38:5 glyph [

163−31:6 tight lit %a

210+38:6 tight lit %a

164−31:9 name value

211+38:9 name value

165−31:14 tight glyph ]

212+38:14 tight glyph ]

166−31:16 name value

213+38:16 name value

167−32:5 NEWLINE

214+39:5 NEWLINE

168−32:5 lit %other

215+39:5 lit %other

169−32:12 lit %.n

216+39:12 lit %.n

170−33:1 DEDENT

217+40:1 DEDENT

171−33:1 DEDENT

218+40:1 DEDENT

172−33:1 NEWLINE

219+40:1 NEWLINE

173−33:1 glyph ++

220+40:1 glyph ++

174−33:4 name duplicate

221+40:4 name duplicate

175−33:14 glyph |=

222+40:14 glyph |=

176−33:17 name x

223+40:17 name x

177−33:18 tight glyph =

224+40:18 tight glyph =

178−33:19 tight name choice

225+40:19 tight name choice

179−34:3 INDENT

226+41:3 INDENT

180−34:3 glyph ?-

227+41:3 glyph ?-

181−34:6 name x

228+41:6 name x

182−35:5 INDENT

229+42:5 INDENT

183−35:5 glyph [

230+42:5 glyph [

184−35:6 tight lit %a

231+42:6 tight lit %a

185−35:9 lit %.y

232+42:9 lit %.y

186−35:12 tight glyph ]

233+42:12 tight glyph ]

187−35:14 str "yes"

234+42:14 str "yes"

188−36:5 NEWLINE

235+43:5 NEWLINE

189−36:5 glyph [

236+43:5 glyph [

190−36:6 tight lit %a

237+43:6 tight lit %a

191−36:9 lit %$

238+43:9 lit %$

192−36:11 tight glyph ]

239+43:11 tight glyph ]

193−36:13 str "duplicate"

240+43:13 str "duplicate"

194−37:5 NEWLINE

241+44:5 NEWLINE

195−37:5 glyph *

242+44:5 glyph *

196−37:7 str "other"

243+44:7 str "other"

197−38:1 DEDENT

244+45:1 DEDENT

198−38:1 DEDENT

245+45:1 DEDENT

199−38:1 NEWLINE

246+45:1 NEWLINE

200−38:1 glyph ++

247+45:1 glyph ++

201−38:4 name shadow

248+45:4 name shadow

202−38:11 glyph |=

249+45:11 glyph |=

203−38:14 name x

250+45:14 name x

204−38:15 tight glyph =

251+45:15 tight glyph =

205−38:16 tight name choice

252+45:16 tight name choice

206−39:3 INDENT

253+46:3 INDENT

207−39:3 glyph ?-

254+46:3 glyph ?-

208−39:6 name x

255+46:6 name x

209−40:5 INDENT

256+47:5 INDENT

210−40:5 glyph [

257+47:5 glyph [

211−40:6 tight lit %a

258+47:6 tight lit %a

212−40:9 name missing

259+47:9 name missing

213−40:16 tight glyph ]

260+47:16 tight glyph ]

214−40:18 str "yes"

261+47:18 str "yes"

215−41:5 NEWLINE

262+48:5 NEWLINE

216−41:5 lit %other

263+48:5 lit %other

217−41:12 str "other"

264+48:12 str "other"

218−42:1 DEDENT

265+49:1 DEDENT

219−42:1 DEDENT

266+49:1 DEDENT

220−42:1 NEWLINE

267+49:1 NEWLINE

221−42:1 glyph ++

268+49:1 glyph ++

222−42:4 name many-bind

269+49:4 name many-bind

223−42:14 glyph |=

270+49:14 glyph |=

224−42:17 name x

271+49:17 name x

225−42:18 tight glyph =

272+49:18 tight glyph =

226−42:19 tight name choice

273+49:19 tight name choice

227−43:3 INDENT

274+50:3 INDENT

228−43:3 glyph ?-

275+50:3 glyph ?-

229−43:6 name x

276+50:6 name x

230−44:5 INDENT

277+51:5 INDENT

231−44:5 name value

278+51:5 name value

232−44:11 str "anything"

279+51:11 str "anything"

233−45:5 NEWLINE

280+52:5 NEWLINE

234−45:5 lit %other

281+52:5 lit %other

235−45:12 str "dead"

282+52:12 str "dead"

236−45:18 DEDENT

283+52:18 DEDENT

237−45:18 DEDENT

284+52:18 DEDENT

238−45:18 NEWLINE

285+52:18 NEWLINE

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

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

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

26 (str 9:18 "d"))

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

28− (value 11:1 wildcard

28+ (value 11:1 parent

29− (gate 11:13

29+ (gate 11:11

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

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

31 (body 12:3

32 (branch 12:3

33 (wing 12:6 m)

34 (arm 13:5

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

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

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

36+ (lit 13:18 0x1f))

37 (arm 14:5

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

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

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

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

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

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

41− (value 16:1 covered

62+ (value 23:1 covered

42− (gate 16:12

63+ (gate 23:12

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

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

44− (body 17:3

65+ (body 24:3

45− (branch 17:3

66+ (branch 24:3

46− (wing 17:6 m)

67+ (wing 24:6 m)

47− (arm 18:5

68+ (arm 25:5

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

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

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

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

50− (arm 19:5

71+ (arm 26:5

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

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

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

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

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

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

54− (mold 22:1 choice

75+ (mold 29:1 choice

55− (union 23:3

76+ (union 30:3

56− (cell 23:3

77+ (cell 30:3

57− (const 23:4 %a)

78+ (const 30:4 %a)

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

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

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

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

60− (value 25:1 missing

81+ (value 32:1 missing

61− (gate 25:12

82+ (gate 32:12

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

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

63− (body 26:3

84+ (body 33:3

64− (branch 26:3

85+ (branch 33:3

65− (wing 26:6 x)

86+ (wing 33:6 x)

66− (arm 27:5

87+ (arm 34:5

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

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

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

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

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

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

70− (value 29:1 typed

91+ (value 36:1 typed

71− (gate 29:10

92+ (gate 36:10

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

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

73− (body 30:3

94+ (body 37:3

74− (branch 30:3

95+ (branch 37:3

75− (wing 30:6 x)

96+ (wing 37:6 x)

76− (arm 31:5

97+ (arm 38:5

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

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

78− (wing 31:16 value))

99+ (wing 38:16 value))

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

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

80− (value 33:1 duplicate

101+ (value 40:1 duplicate

81− (gate 33:14

102+ (gate 40:14

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

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

83− (body 34:3

104+ (body 41:3

84− (branch 34:3

105+ (branch 41:3

85− (wing 34:6 x)

106+ (wing 41:6 x)

86− (arm 35:5

107+ (arm 42:5

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

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

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

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

89− (arm 36:5

110+ (arm 43:5

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

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

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

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

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

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

93− (value 38:1 shadow

114+ (value 45:1 shadow

94− (gate 38:11

115+ (gate 45:11

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

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

96− (body 39:3

117+ (body 46:3

97− (branch 39:3

118+ (branch 46:3

98− (wing 39:6 x)

119+ (wing 46:6 x)

99− (arm 40:5

120+ (arm 47:5

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

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

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

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

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

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

103− (value 42:1 many-bind

124+ (value 49:1 many-bind

104− (gate 42:14

125+ (gate 49:14

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

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

106− (body 43:3

127+ (body 50:3

107− (branch 43:3

128+ (branch 50:3

108− (wing 43:6 x)

129+ (wing 50:6 x)

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

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

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

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

1partial inference; module not checked

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

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

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

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

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

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

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

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

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

8 ^

9 ^

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

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

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

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

11++ typed: $-(choice ?)

12++ typed: $-(choice ?)

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

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

14 [%a %$] "duplicate"

15 [%a %$] "duplicate"

15 ^

16 ^

16++ shadow: pattern binder shadows a name

17++ shadow: pattern binder shadows a name

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

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

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

3expect: parses

4expect-types: a partial inference report

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

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

7 [%ok again] again

8 ^

9++ 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+ ^

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

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

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

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

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

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

tests/lib/jibb-deferred.hoon+10

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

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

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

49 ==

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

50++ case-negative

59++ case-negative

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

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

52 ^- (list @t)

61 ^- (list @t)

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

226 ^- @t

235 ^- @t

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

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

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

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

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

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

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

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

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

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

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

tests/type-deferred/expected.txt+1

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

4independent built result stays polymorphic

5text use inferred

6ship use inferred independently

7+deferred branch joins present parent

7missing constructor leaves no result

8missing constructor leaves no result

8conflicting context leaves no result

9conflicting context leaves no result

9duplicate source binding declined

10duplicate source binding declined