f5939a4..master · jibb

git.iko.soy/jibb

20 files changed+1255−60

unifiedsplit

docs/README.md+3

@@ -14,11 +14,14 @@ The current full-module checker also has a narrow static/data-page slice, docume

1414| [prelude-inventory.md](prelude-inventory.md) | Working source audit for the prelude's exported inventory |

1515| [prompts/milestone-2.md](prompts/milestone-2.md) | A brief for the developer who builds milestone 2, types and prelude |

1616| [prompts/drop-union-rune.md](prompts/drop-union-rune.md) | The completed brief for dropping `$?`, as decided on 2026-10-30, before milestone 2 |

17+| [prompts/syntax-review-follow-up.md](prompts/syntax-review-follow-up.md) | A brief for finishing the syntax changes Montelot decided on 2026-11-03: open gaps, unfinished reviews, work that waits on the checker core, and questions to ask |

1718| [reviews/2026-11-02-repo-review.md](reviews/2026-11-02-repo-review.md) | A review of the whole repository on 2026-11-02: bugs, gaps and simplifications, each checked by a second reviewer |

1819| [reviews/2026-11-02-questions.md](reviews/2026-11-02-questions.md) | The 45 decisions that review raises, with options and recommendations |

1920| [reviews/2026-11-02-syntax-review.md](reviews/2026-11-02-syntax-review.md) | A review of Jibb's syntax on 2026-11-02: 15 verified proposals with before and after examples, what to keep, and questions for @iko |

2021| [reviews/2026-11-03-milestone-2-review.md](reviews/2026-11-03-milestone-2-review.md) | A review of milestone 2 against the plan on 2026-11-03: the done-criteria, the errors the spec describes, findings M1 to M17, with its [probes](reviews/2026-11-03-milestone-2-probes/) |

2122| [prompts/milestone-2-finish.md](prompts/milestone-2-finish.md) | A brief for finishing milestone 2: the general checker core, diagnostics, patterns, kinds, imports, tests and docs that the milestone 2 review found missing |

23+| [prompts/repo-review-finish.md](prompts/repo-review-finish.md) | A brief for finishing the 2026-11-02 repository review: the open findings no other brief covers, the rulings waiting for @iko, and the review's advice for the checker core |

24+| [reviews/2026-11-03-checker-map.md](reviews/2026-11-03-checker-map.md) | A map of the type checker on 2026-11-03 for whoever builds the general core: its families, recovery slices, hazards, and what the core replaces and keeps |

2225

2326## The spec

2427

docs/development.md+2

@@ -88,6 +88,8 @@ Each file in `tests/lib` is a suite: a core of `test-` arms, with the libraries

8888

8989A golden-report suite has a `report` arm and a golden file bound to the face `expected`; its test arm compares the report with that file, and `tools/test-arms --list` marks it `, report`. `tools/test-arms --report <suite>` prints the report, and `tools/test-arms --update <suite>` writes it to the file; with no suite named, `--update` writes every golden-report suite's. When such a suite's arm fails, `tools/test-arms` prints a unified diff between the file and the report. `jibb-buttons` and `jibb-deferred-prepared` have golden files too, but compare them inside helpers over several cases and have no `report` arm. Every golden file, a `/*` `%txt` file bound to a face containing `expected`, must end in exactly one newline (a suite compares `wain`s, which can't show a missing one) and hold no line that starts `BAD ` or ends `: BAD`; `tools/test-arms` checks that before any eval, and `--update` won't write a report that breaks it.

9090

91+`tools/doc-fragments` guards the examples checked in a larger context: the Core language's `update` must match the todo island's definition, and the valid buttons fixture must match the Grammar's buttons block with `add-button` removed. It runs as part of `tools/check` alongside `tools/doc-blocks`.

92+

9193The `jibb-dev` desk holds `my-app`'s `ui/`, `sur/` and `mar/` under `/my-app` (review question 31), so the suites that check `my-app` files bind them there, as `/* sur %txt /my-app/sur/todo/hoon`, and keep no copies. A mark's `/-` line is Ford's, which `ride` can't parse, so the suites that ride a mark drop it with their `+mark-text` arm. Where the table below calls a `my-app` file byte-identical or unchanged, the suite reads that file itself. Files that only the importer's tests need are kept off `my-app` (review question 34): the Clay fixtures' `/sur` with a Ford import, their mark and the real Tlon notes `/sur` are in `tests/clay-fixtures/desk/`, which the `jibb-fixtures` desk adds to `my-app` and the `jibb-dev` desk leaves out, and the golden cases and `tests/type-poke/mark.txt` that use the mark link to `tests/clay-fixtures/desk/mar/label.hoon`.

9294

9395| Suite | What it checks | Golden files |

docs/open-questions.md+2−2

@@ -50,14 +50,14 @@ In milestone 1 the parser met about thirty places where the doc could be read mo

5050| 1 | `knot` may be empty, so the EBNF admits `//`, `/a//b` and a trailing `/`. Which are paths? | A segment has at least one character, as in Hoon. `/` alone is the empty path, in expressions and molds; `%/` alone is the root application path. `//` fails at the second `/`, and a trailing `/` just past it. `inline-mold-paths` has `/` alone as a mold |

5151| 2 | Is `/` alone a valid path for a `/=` import? | No: `/=` names a module's file, so its path has a segment. `/= card /` fails just past the `/` (`inline-import-root-bad`) |

5252| 3 | The EBNF's `line = [ name "=" ] expr` lets every open bracket's lines take `name=`. What would it mean on a line of an open `(` or `~[`? | An error: `name=` lines belong to tuples and changes. "expected a space between items, found `=`; `name=value` goes in a cell, as [a=1], or a change, as m(a=1)" |

53−| 4 | Does "items named" make every item of a change need `name=`? | Yes: `m(x)` fails just past `x`, "a change's items are named, as in m(done=%.y)" (`lex-tight-change-bad-3` to `-7`; `-8` and `-9` test what follows a name there). The parser still accepts `m()`, though question 6 settled it as an error |

53+| 4 | Does "items named" make every item of a change need `name=`? | Settled on 2026-11-03 (syntax review S6): yes, `name=value` or `wing=value`, as `m(open.cart=x)`. `m(x)` still fails just past `x`, "a change's items are named, as in m(done=%.y)" (`lex-tight-change-bad-3` to `-7`, where `-5` is a wing with no `=`; `-8` and `-9` test what follows a name there) |

5555| 6 | What does an indented first line mean? | An error: "the first line is indented: top-level lines start at column 1" (`lex-indent-bad-3`) |

5656| 7 | With levels open at columns 1 and 5, what does a line at column 3 mean? | An error naming the open columns: "this line's indentation matches no enclosing line: indent it to column 1 or 5". `lex-indent-bad-2`, with levels at 1, 5 and 7, gives "column 1, 5 or 7" |

5757| 8 | Tabs, carriage returns, other control characters, and non-ASCII text outside strings and comments? | Errors everywhere, strings and comments included, except that UTF-8 is allowed in strings and comments; a tab in a string is written `\09`. `lex-indent-bad-1` and `lex-spacing-bad-2` test tabs |

5858| 9 | Must a file be valid UTF-8? | Not checked yet: any byte from 128 up passes in strings and comments, and columns assume UTF-8. The proposed reading makes a byte that can't continue a UTF-8 sequence an error. An escape such as `\ff` still writes any byte, as in Hoon |

5959| 10 | Inside `{…}`, may `::` start a comment, which would swallow the `}` and the `"`? Is a lone `}` in a string text? May a comment follow code with no space, as in `5::note`? | A `:` inside `{…}` is "a comment can't start inside `{…}`". A lone `}` is text, as in Hoon. `5::note` is `5` and a comment |

60−| 11 | Is a type variable exactly one capital letter, as `typevar = upper` says? | Yes: `Msg` is "a type variable is one capital letter" |

60+| 11 | Is a type variable exactly one capital letter, as `typevar = upper` says? | Settled on 2026-11-03 (syntax review S7): no, a capital then lowercase letters and digits, as `Msg`; `AB` is an error |

6161| 12 | Hoon has more runes of the left-out kinds than the list names: `?~ ?= ?. ?@ ?^`, `:- :+ :^ :_`, `%- %+ %^ %~`, `=+ =? =.`, `;:` and `~&(…)`. Are they all left out? | Yes, with the list's reasons, as "`:-` is left out: indentation covers it; write a cell as [a b]". Naming them in the doc, or saying "Hoon's other runes", would make the messages the doc's words (`inline-leftout-*`) |

6262| 13 | `@s…` and `@r…` auras are "errors wherever used". Is that the parser's error in Jibb source, or the checker's? | An error before the checker. Where a mold goes, the layout pass's, at the `s` or `r`: "signed and floating-point auras are left out of Jibb". Where an expression goes, the parser's, at the `@`: "expected an expression, found `@`; signed and floating-point auras are left out of Jibb". Imported ones are milestone 2's importer's. The case `inline-leftout-signed-float-auras` still says "expect: unclear" |

6363

docs/prompts/milestone-2-finish.md+3−2

@@ -13,7 +13,7 @@ You are finishing milestone 2 of Jibb, a UI language for Urbit: a Hoon dialect w

13133. [docs/spec/implementation-plan.md](../spec/implementation-plan.md), milestone 2, and the spec tabs it points at, closely Grammar's Tag resolution, Literals by context, Patterns, Modules and Imports.

14144. [docs/reviews/2026-11-02-questions.md](../reviews/2026-11-02-questions.md): the owner's answers, marked *(chosen)*. Q5 and Q6 set the direction below. Q16 to Q28 are proposals waiting for @iko, not spec.

15155. [docs/development.md](../development.md): setting up (`nix develop`), the tools, the test suites, and the checks before pushing (`tools/check` or `nix flake check`).

16−6. `git log origin/master`: @iko works in `jibb.hoon` in parallel, and another thread is implementing syntax-review proposals S1, S2, S4 to S7, S11 to S13 and S15 ([syntax review](../reviews/2026-11-02-syntax-review.md)). Rebase often and keep your changes out of theirs where you can.

16+6. `git log origin/master`: @iko works in `jibb.hoon` in parallel, and another thread is implementing syntax-review proposals S1, S2, S4 to S7, S11 to S13 and S15 ([syntax review](../reviews/2026-11-02-syntax-review.md)). Rebase often and keep your changes out of theirs where you can. The thread that fixes the 2026-11-02 review's findings planned this same core on 2026-11-03, in stages that keep every check green; ask in the project chat who is building it before you start step 2.

1717

1818## Ground rules

1919

@@ -32,12 +32,13 @@ The full checker, `infer-jibb-file-detailed`, drops every per-definition reason

3232

3333### 2. The general checker core (Q5)

3434

35−The owner chose this on 2026-11-02: union-find bindings with levels, a queue of deferred constraints, and a usefulness check for matches, built before more recovery paths. It is a long piece of work, so first write its design as a new section of the library's design notes, and share it in the project chat for @iko before replacing code.

35+The owner chose this on 2026-11-02: union-find bindings with levels, a queue of deferred constraints, and a usefulness check for matches, built before more recovery paths. It is a long piece of work, so first write its design as a new section of the library's design notes, and share it in the project chat for @iko before replacing code. Start from [the checker map](../reviews/2026-11-03-checker-map.md), which says what each part of today's checker does, which tests pin it, what the core replaces and keeps, and the hazards; [repo-review-finish.md](repo-review-finish.md) step 6 has the review's advice for staging it.

3636

3737- **Unification**: union-find over type variables, with levels for generalization instead of environment scans; an occurs check; aura variables and the "is an atom" and "contains no gates" constraints carried on the variable, as `0858191` already does for gate-freedom.

3838- **Deferred constraints**: tags, `~`, numbers and cells, wing access, changes and `?-` on a type not yet known each wait in one queue, retried as variables are bound, as the Grammar's Tag resolution says. A tag-constrained variable does not generalize and stays open until something in the module fixes it. At the end of the module, each still-open constraint is an error at its source: "nothing fixes the union of %add; add a `^-`".

3939- **Order**: infer `++`s by the strongly connected components `839f6b0` already computes, a group of mutually recursive gates together; reject a non-gate value that depends on itself, naming the cycle.

4040- **Kinds by type**: check `main` as an ordinary expression. `(program init update view subs)`, `(page load view)` and `(store init update)` are calls whose unification fixes their components' types, messages included, so a tag in `view` is resolved by `main`. Then read the kind from `main`'s type, as the Grammar says, and run each kind's own checks after inference: gate-free island data and models, naming the field; for islands, a walk of the `(list (sub M))` that asks for a watchability proof only for `%watch`; for pages, a load that is any gate to `(ask D)`, `pure` and typed paths included.

41+- **Rulings it must build in**, chosen by Montelot on 2026-11-03 from the syntax review: a capital that meets a faced position binds only the type under the face, never the face, so `[A A]` fits `[x=@ y=@]`, `(hunt lt-a `1 `2)` checks, and `(roll ~[1 2] 0 add-f)` checks with `++ add-f |= [a=@ud b=@ud] (add a b)`; a join keeps a face once a position takes one, so reordering a list's items never changes whether it checks; and, as the syntax thread lands them, the explicit `unface` (S1), bare decimals fitting only `@ud`, `@u`, `@` and `*` (S4), and a bare-name pattern that spells a union tag being an error (S5). Take their final wording from `decisions.md`, and add each ruling's examples as golden cases in the stage that builds it.

4142- **Then delete** the program, page and store recovery chain, the deferred transactions, the prepared-tuple route and the other example-shaped slices as the core covers their tests (the earlier review counts about 1,180 lines of program recovery alone).

4243

4344When this is done, M2 to M5 are gone: every valid variant in the review's [probe corpus](../reviews/2026-11-03-milestone-2-probes/) checks, and each error in an island is reported where it is, as `button "Add" %submitt` giving "msg has no case `%submitt`" at the tag, with the union's site.

docs/prompts/repo-review-finish.mdnew file+149

@@ -0,0 +1,149 @@

1+# Finishing the 2026-11-02 repository review

3+A brief for the developer who finishes what the [2026-11-02 repository review](../reviews/2026-11-02-repo-review.md) started. Paste it as the first message of a session, or hand it to a person; it assumes the repo `iko-soy/jibb`. Written 2026-11-03, at commit `e208bcb`, by the thread that fixed the review's findings, from a check of every question and finding against `master` that day.

5+---

7+You are finishing the follow-up to a review of the whole Jibb repository. Jibb is a UI language for Urbit, a Hoon dialect with an indentation layout; its compiler is a Hoon library, `jibb-dev/lib/jibb.hoon`, with a Hoon type importer in `jibb-dev/lib/jibb-import.hoon`. The review, at commit `4bf477e`, found 137 problems (A1 to A137) and raised 45 questions, which Montelot, the project's owner, answered: each answer is marked *(chosen)* in [the questions](../reviews/2026-11-02-questions.md). Most answers have landed. What is left is small fixes, simplifications and docs that no other brief covers, twelve language rulings and one more question (A62) that wait for @iko, and the review's advice for the checker core, which milestone-2-finish.md builds.

9+Three briefs share the remaining work. Don't do one brief's work under another:

10+

11+- **[milestone-2-finish.md](milestone-2-finish.md)** owns the general checker core (review question 5), the diagnostics the full checker still drops (its step 1), the usefulness check for `?-`, one types pipeline (question 6), kinds, APIs, the import table, tests and speed. Its import table step lists two known gaps from this review, A14 and A50; they are fixed here, in step 1 and under question 26.

12+- **[syntax-review-follow-up.md](syntax-review-follow-up.md)** owns the syntax changes S1 to S15, including `unface` and the gaps in S2, S4 to S7.

13+- **This brief** owns the rest of the repository review: the open findings below, the rulings for @iko, and the review's input to the core.

14+

15+## What landed

16+

17+| Questions | What | Commits |

18+| --- | --- | --- |

19+| 1 to 4 | The review on `master`, fixes as commits straight to `master`, a fake ship in cloud containers | `c7cd17d`, `f583172` |

20+| 7 to 15 and the eight "fix first" bugs | Ordinary inference before recovery, the narrow initializer recovery deleted, imported `(unit T)` as the prelude's unit, `ask` and `qath` printed without `.internal`, one branch-join rule, dependency-order resolution, kept diagnostics, no 26-variable gate, a fresh-ID high-water mark, lexer, `tools/ship` and `tools/golden` fixes | `a211c34`, `38c711c` and `ec7c6d4` (@iko), `93d6b23`, `839f6b0`, `f0411ad`, `ce69a3b`, `447a592`, `2b9666c`, `96d1784`, `c0a0b85`, `941c486`, `452f64c`, `68d9b76` |

21+| 25 | `eq` and the gate-free constraint | `0858191` (@iko) |

22+| 29 to 35 | `tools/test-arms` instead of 52 scripts, `tools/check`, `my-app` read on the test desk, the generated `tests/lib/jibb.hoon` no longer committed, importer fixtures in their suite, a `jibb-fixtures` desk, span and Hoon-reference checks as test arms | `d74b5e2`, `0a86d7c`, `8125287`, `ba67080`, `933bc83`, `d43c99b`, `32f4b78` |

23+| 30 (CI) | A GitHub Actions job ran the eval checks; Montelot had it removed on 2026-11-03. There is no CI; don't add one back without asking | `84b8527`, `f84a29e` |

24+| 36, 37, 39, 43 | Decided to keep things as they are | `bf65f8f` |

25+| 40 to 42, 44, 45 | `tools/hoon --no-debug`, `status.md` as a capability table, the repository spec wins until synced, `open-questions.md` only open questions, the MIT licence | `cdf53c8`, `e97aebe`, `7bc7d54`, `116178b` |

26+

27+## Read first

28+

29+1. [The review](../reviews/2026-11-02-repo-review.md): its summary, and the appendix rows for the findings below. Its line numbers are pinned to `4bf477e` and have drifted; find code by arm name.

30+2. [The questions](../reviews/2026-11-02-questions.md), and in [open-questions.md](../open-questions.md) the section "Review rulings waiting for @iko".

31+3. The two other briefs, so you know what they own.

32+4. [The checker map](../reviews/2026-11-03-checker-map.md), before you touch the type checker: what each family of arms does, which tests pin it, the 22 recovery slices, the five copies of definition finalization, and 22 hazards for anyone changing the checker.

33+5. [development.md](../development.md): setting up (`nix develop`), the tools, the test suites, and the checks to run before pushing (`tools/check`, or `nix flake check`).

34+6. `git log origin/master`. @iko and other threads work in `jibb.hoon` in parallel; rebase often.

35+

36+Then run `tools/check`. Every check should pass before you change anything.

37+

38+## Ground rules

39+

40+- **Push straight to `master`**, rebased on `origin/master`, in commits that each leave every check passing, the ship group included. Never force-push. Before a change to `tools/ship`, the desks or the `%jibb` mark, run the ship checks on a fake ship.

41+- **Every fix is a golden case or a test arm.** A finding that changes behaviour gets a case that fails before the fix.

42+- **Don't decide the language.** Questions 16 to 24 and 26 to 28 are Montelot's proposals, and each waits for @iko to confirm it before it goes in `decisions.md` and the code changes. Ask @iko in the project chat; don't build them on the proposal alone.

43+- **Don't patch what the core replaces.** The findings listed at the end of step 6 are fixed by building the core, not by repairing the old code. Before you change `+itype-unify`, `+itype-fit`, branch joins, `?-` coverage, the program, page and store recovery, or the `dg-*` transaction, ask in the project chat who is building the core and what has landed.

44+- **Keep docs current.** `status.md` is a table of capabilities: change the row a fix affects, don't add history. `compiler.md` follows the code.

45+

46+## Step 1: fixes that don't wait for anything

47+

48+A19 and the inhabitation half of A13 touch `+itype-fit-inner` and `+itype-inhabited-proof`, which the core replaces, so follow the ground rule: ask in the project chat first, and leave them to the core if it has replaced that code. A13's `+gate-free-type` half and A14's bridge are code the core keeps (the checker map, 4.2), so they don't wait.

49+

50+Checker and importer:

51+

52+- **A19.** `+width-scan` counts each faced entry on a spine, so a flat faced tuple has more entries than a record whose last field is a faced nested record. The flat tuple is then refused, as unknown by the `too-wide` guard in `+itype-fit-inner`, and as "record width constraint needs unsupported inference" by `+width-shape` in the cast and call checks. When the target's last field is a faced cell, match the source against it structurally instead of by count, and check the `lth` guards in `+width-proj-shape` and `+width-infer-literal` with the same case.

53+- **A13.** `+itype-inhabited-proof` and `+gate-free-type` know only the list and unit collections. Treat set, map, qeu, mop, jar and jug as inhabited by `~`, and check gate-freedom over all their arguments. Add a union match on a case that holds an imported map.

54+- **A14.** One whitelist of auras, `?(%u %ud %ux %uv %t %ta %tas %p %da %dr)`, is copied in `+rec-pattern`, `+import-to-itype-standard` and the API parameter check, and rejects bare `@` and other unsigned auras. Write one predicate for `@` and every unsigned, non-float aura and use it at all three; teach `+rec-pattern` `*` and `?` fields. Add bridge cases. Milestone-2-finish step 7 lists this gap for its import test; fix it here, and that test then covers it.

55+- **A56.** The importer's `+overlap-source-witness` proves a definite overlap only for a top-level `$?` of tagged cells. Accept `$%` bodies and `?(...)` leaves, so duplicate `$%` tags and `?(%a %a)` give the definite overlap, with cases in `tests/importer/tree.txt`.

56+- **A43.** Without a prelude the partial report says a bare "module has a reserved proj or unface name", with no "partial inference; module not checked" header, while the prepared path says "module has conflicting names". Give both paths one message under the header: the prepared path's, or, if milestone-2-finish step 1 has given `proj` its own wording by then, that wording. `inline-unface-reserved-no-prelude` already covers the no-prelude branch for a mold named `unface`; add a case for `++ proj 1`, and update that case's output.

57+- **A22.** The comment on the noun fit says a bare tag is "fixed as a constant", but the code binds it to the expected type. Fix the comment.

58+

59+Lexer and parser:

60+

61+- **A4.** `+read-string` calls `+doomed` for "the `}` of an interpolation", a case that never happens. Delete the call, fall through to `+bad`, and drop the clause from the notes and `+doomed`'s comment.

62+- **A5.** In the lexer's glyph dispatch, the second-character messages ("`|` begins `|=`…", "`^` begins `^-`") win over the 2.2 character errors, so a tab or control character after a glyph gets the wrong message, and only some left-out runes get the doc's reason. Run `+bad-char` first and give every left-out rune of the doc's kinds its reason. The syntax review's S9 (undecided) would rewrite nearby messages; keep to the review's fix.

63+- **A3, what is left.** About a dozen lexer hints have no golden case, among them "this `}` closes no `{`", "`|` begins …", "`^` begins `^-`", a comment inside `{…}`, interpolation outside a string, a wing's `.`, the `@u` and `@t` literal errors, the date bounds, "Jibb writes no such literal" and "Jibb can't read this literal". Several parser hints have none either, as "`+` begins `++` or `+$`", "patterns take no units: write [~ x]", "`?` alone is the loobean mold" and "the wide gate's body is one operand". Add a `lex-*-bad-*` case for each lexical one and an `inline-*` case for each parser one.

64+

65+## Step 2: tools and tests

66+

67+- **A68.** `tools/golden` splices `jibb-import.hoon` into the "(harness)" segment, so its compile errors and crash frames are blamed on the harness. Add the reader as its own segment, so spots map to `jibb-import.hoon` lines.

68+- **A69.** `tools/ship test`, `sync` and `gen-tests` accept a `--golden` folder that doesn't exist and pass with no tests. Fail when the folder is missing or a named folder has no cases, as `tools/golden` does.

69+- **A70, A84.** `tools/testdata/ship-selftest` hard-codes 45 `tests/lib` names, which miss 14 of the 58 suites, and dozens of fixture names in the checks after them. Replace them with one check: every file under `tests/` except `golden/` and `clay-fixtures/desk/` is in `assemble('jibb-dev')`, and so is the generated `tests/lib/jibb.hoon`. Keep the `--lib` and `--golden` isolation checks. That list is the last place a new suite must be registered by hand, so this also closes A84.

70+- **A74.** An `about.txt` that isn't UTF-8 crashes `tools/golden` and `tools/ship gen-tests` with a traceback, because `wants_types` in `tools/golden_case.py` is called outside the `except ValueError` handlers. Have it raise a `ValueError` that names the file, as `source_path` does, and move its calls inside the handlers: in `Case.__init__` in `tools/golden`, and in `generate_tests`' per-case loop and types-helper test in `tools/ship`. Both then exit 2 with a report.

71+- **A75.** `tools/golden` fills the harness's `{…}` placeholders after splicing in the cases' sources, the reader and the preludes, so any of them that contains a placeholder is rewritten. Substitute every placeholder in one pass.

72+- **A76.** The ship's plain `+check-types` isn't under `mule`, unlike `+check-import-types` and its other siblings, so a crash in it shows only as CRASHED, without the case's tokens and tree results or the label its siblings give. Wrap it. The eval and ship runners also keep separate copies of their Hoon helpers and their walk over a case's metadata; share them.

73+- **A72, A77, A73, A79.** Smaller tool copies: `tools/golden` renders the two preludes twice and repeats its read-to-`rap` code three times; `tools/ship` keeps its own `KNOT`/`TERM`, noun decoding and cord escaping beside `golden_case.py`, `noun.py` and `urbit_eval.py`; `delete_batches` keeps an empty-list case only a selftest uses; `tools/ship`'s `find_urbit` ignores `$URBIT`.

74+- **A71.** `check_fixture_crash_isolated` in `tools/testdata/selftest` runs the real compiler and pins checker output, though the file says the selftest runs against the stub. Give it a stub fixture, or say so.

75+- **Test-only code in the shipped library (A93, A127).** Move `+itype-unify-test` and `+check-spans-test` from `jibb.hoon` into the `jibb-typecheck` and `jibb-check-spans` suites, and have `test-unification` return the unifier's failures as its tang, so the one-line `tests/checker/unification.txt` can go (A85).

76+- **A86.** 38 suites repeat a lines-to-cord helper. Put one in a shared test library bound with `/+`.

77+- **A87, A88.** `development.md`'s golden naming table lists only `lex-`, `inline-` and `doc-`; add `types-`, `module-`, `prelude-`, `parser-` and `fixture-`, fix the ten `about.txt` files that lack a required line, and have `tools/golden` or the selftest reject them. Say in the suites section which `tests/type-*` folder belongs to which suite, or rename the folders after their suites.

78+- **A89.** The importer's fixtures are bound one by one in `tests/lib/jibb-import.hoon`; bind them as one list and derive the report and the missing-file checks from it. `tools/clay-fixtures` prints hand-written counts, "7 passed" and "4 projections passed"; compute them from the expected files.

79+- **A90, A102.** Nothing tests the claims that 100,000 nested brackets and a 20,000-line module parse. Add a suite or selftest step that generates them; milestone-2-finish step 9 then records the timings. Then re-measure design note 3's figures with `tools/hoon --no-debug` and say which mode they use: its "8 s" for starting urbit and building the library is now about 27 s.

80+- **A114.** The Clay fixture `tests/clay-fixtures/desk/sur/import-fixture.hoon` writes `$^(@ud [a=@ud b=@t])`, which accepts only atom-headed cells. Write the intended `$@(@ud [a=@ud b=@t])` and update the `ford-nested-union` expected files.

81+- **A111, A117.** `tools/ship`'s `DESKS` skips a `jibb-dev/tests` folder that doesn't exist, for `my-app` and `jibb-fixtures`; drop the skip and the README's "without tests/", and make the README's desk table match `DESKS`: add the `jibb-fixtures` row, and on `jibb-dev` name `my-app` under `/my-app` and the skipped `tests/clay-fixtures/desk`. Make `tools/ship assemble` fail when `my-app/sys.kelvin` and `jibb/sys.kelvin` differ.

82+- **A118.** `vendor/SOURCES.txt` records the machine-local path `/root/src/urbit` it was copied from, and credits the docket files to urbit/urbit's legacy `pkg/landscape`. Drop the local path, and say where the docket files are maintained now.

83+- **A110.** The Clay fixtures build `my-app`'s marks only as Hoon cores. Add a `%cb` build and a `vale` of one sample noun for each, with milestone-2-finish step 8's `my-app` ship check if that lands first.

84+

85+## Step 3: simplifications in code the core keeps

86+

87+Most are in the parser, the importer, and the module and API code, which the core keeps. A few are dead lines in checker arms that the core replaces, as the fuel of `+itype-closed-sample-match` and the last unify of `+itype-closed-gates-match`; deleting them changes nothing, so they don't wait for the core. Each must leave every golden output unchanged.

88+

89+- **Dead code (A26, A31, A42, A44, A130, A18, part of A45).** Delete `+width-has-projections`, `+infer-width-elaboration` and its type `+$ iwidth-elaboration`, `+direct-find-gate`, `+resolve-supported-defs`, the newly dead `+import-to-itypes`, `+one-request-interface-source` and `+golden-types-with-modules` (and its sentence in `compiler.md`), and the orphan comments above unrelated arms. Drop the narrow API branch, `+one-request-interface-graph`, so every API with `+$ paths` goes through `+multi-request-interface-graph`, after checking that `blog.jibb`'s interface and the `type-api` outputs don't change. Remove the never-decremented fuel of `+itype-closed-sample-match`, the always-true unify at the end of `+itype-closed-gates-match`, `+width-scan`'s unused `sub`, and two dead lines in `+find-imported-mold-prelude`. Of A45, fix only what is outside the recovery and `dg-*` arms: the double negation and the `?~ index` branch in the module driver, and the fake `ifile`s in the store code.

90+- **The `?(` check (A7).** `+hoon-union` walks back over tokens at twelve call sites to report a tight `?(`. Have the lexer's `?` branch report it, with the same column and message, and delete `+hoon-union`.

91+- **Names that shadow the standard library (A8).** Rename `+in`, move the `+fail*` helpers into `+parser` so `file` is in scope, and delete the `file` forwarders and the sixteen `in:..zuse` workarounds. Then drop the Code conventions bullet in `development.md` that says `+in` and `+fail` shadow the standard library, and move the `+fail*` helpers from the `%parser-helpers` row of `compiler.md`'s chapter table to the `%parser` row.

92+- **Copies in the parser (A9).** The path-segment loops of `+read-pathlit`, `+read-qath` and `+read-pathmold`, the open-mold-line loops, and the item and line name branches are near copies. Merge them where the result is clearly simpler; the review found some merges are not.

93+- **`%gate` and `%gate-wide` (A34, A123).** The two nodes carry the same fields, and 39 lines in the checker chapters test both or repeat an identical body for each (A34). Make one `%gate` node with a `wide=?` flag that only the printers read. That merges the checker's copies too and changes note 3's tree forms, but no golden output. Ask first if the core is being built; if its builder wants the old node kept for now, use `?(%gate %gate-wide)` in the parser, the printers and the syntax walkers only, and leave A34 to the core.

94+- **Syntax walkers (A32, A129).** The `scope-*`, `dependency-*`, `duplicate-*`, `*-has-hole` and reserved-name walker families each repeat the per-node dispatch. Add one enumeration of an expression's children and a fold, and rewrite these families on it. The type walkers (A21, A35) wait for the core.

95+- **API and module copies (A27, A29, A31).** `+request-graph-merge` should reuse `+request-graph-inputs-match` and `+request-graph-bounded`, drop its fuel arguments, and make the bound agree with its comment. `+prepare-prelude` and `+prepare-prelude-with-internal`, and `+module-mold-types` and its `-detail` form, should each share one core. `+api-path-evidence-source` and `+api-support-analysis-source` should call their `-graph` forms.

96+- **Importer copies (A57, A58, A59).** A provenance-error helper for the repeated preamble, `+local-arm-source` in `+tagged-union-fallback`, one list of standard collections, one unwrap gate parameterised by the wrapper's tag, one case lister for `$%` and `$?` with the budget as a parameter. A59, a reader that walks once for both the plain and diagnostic results, is low priority.

97+- **Budgets (A124).** The checker's literal budgets (256, 64, 4,096 and others) are scattered. Name the ones in code the core keeps in one arm; the `dg-*` ones go with the core.

98+

99+## Step 4: docs

100+

101+- **The library's header and `compiler.md` (A2, A60, A101, A131).** `jibb.hoon`'s first line says milestone 1, and its API list lacks `infer-jibb-file`, `infer-jibb-file-detailed` and the `golden-types-with-*` entry points. Its API list also lacks `+layout-error`, `+golden-types-imports`, `+prepare-prelude` and `+prepare-prelude-with-internal`, which hosts and `tools/golden` call. Add them all, make `compiler.md`'s API table list the same arms, fix its `%api` row, and add `%union-analysis` to its chapter table with an accurate `%type-inference` row; that chapter also holds the module checker, the API code and the recovery, so say so or split it. The header also still says the doc wins, where question 42 made the copy in `docs/spec/` win, and its Status paragraph calls the checker a partial inference fragment; fix both, as `development.md` words the first, and fix `compiler.md`'s first paragraph, which says "as milestone 1 left it". Milestone-2-finish step 10 rewrites these again for the core; this fix is for the code as it is now.

102+- **Design notes 2.6, 3 and 4.2 (A2).** They don't mention the `_` type hole (its token, where a mold may be `_`, its tree form) or the `?(` hint ("a union is a `+$` with its cases below"). Add them, writing the hint where A7 leaves the check: once the lexer reports it, in note 2.6's table of left-out forms, beside `$?` and `$%`.

103+- **The recovery chain (A41).** Neither `compiler.md` nor `status.md` mentions the plain-view recovery, `+program-plain-view-context`, which runs only when the keyed-view proof declines. Add it to `compiler.md`'s recovery paragraph and to `status.md`'s component-local recovery row, or leave it if the core has deleted it by then.

104+- **The importer's header (A53).** It opens with `+read-mold`, which only tests use; the callers use `+read-named` and `+read-mark` and their `-diagnostic` forms. Rewrite the header's API paragraph around them, and fix the two `jibb.hoon` comments that name `+read-mold`.

105+- **The prelude docs (A54, A105, A63, A99).** `prelude-inventory.md` lists the nine 3g shapes as future work though all exist, and its 2a rows contradict the paragraph above them. `decisions.md`'s Core language row still says three rules in its tab are proposed, but `core-language.md` marks none, and the review found each decided in its own row; drop the clause and set the row's Synced column to No, and ask @iko only about a rule that has no decided row. `internal.jibb` should say in a comment that the compiler adds the public prelude's validated list and unit to `core`, to avoid an import cycle, and `tuba-text` should take `values=(list @tD)`.

106+- **Question 38 (A112).** Montelot chose to keep `my-app`'s deliberately failing buttons example and the theme's static font, and to list them as a milestone 4 question. Add it to `open-questions.md` under "Questions milestone 2 raises", or in the plan's table with "review question 38" in the row, so the table doesn't credit the plan with it.

107+- **A106.** A paragraph about the tools sits under `development.md`'s ground rules, and `docs/README.md` carries status prose. Move the first into "The test suites". Delete the second, after adding to a `status.md` row anything it says that no row does.

108+- **A103, what is left.** `open-questions.md` still lists grammar questions 4 and 11, which the syntax review settled (S6, S7). `decisions.md`'s Syntax and Type variables rows already record the answers, so delete the two rows, keep the other rows' numbers, and update the page's "as of" date.

109+- **A115, A116.** `my-app/mar/todo-action.hoon` says it is "not supplied by the design doc", but it is the overview's `todo-action` block; fix the line. Say in the README's desk table that `my-app`'s `desk.bill` is `~` until fixture agents arrive. List the missing `%todo` and `%blog` fixture agents, and a page that embeds the basket, as gaps in `status.md` for milestones 5 and 6, and ask @iko before adding them to `implementation-plan.md`, which is @iko's tab.

110+

111+## Step 5: the rulings, when @iko confirms them

112+

113+Ask @iko about each in the project chat, with the proposal from `open-questions.md`. When one is confirmed, record it in `decisions.md`, move it out of `open-questions.md`, then change the code with golden cases. Until then, change nothing.

114+

115+| Question | Proposal | Then |

116+| --- | --- | --- |

117+| 16, 17 (A20) | A term literal fits its own aura family, `%1.000` a `@ud` and `%&` a `?`; a name term also fits `@t` | Change the two term-literal branches of `+itype-fit-inner`, the `%atom` row of `+tag-presence`, and the sentence in `grammar.md`'s Tag resolution that lists `@tas`, `@ta`, `@` and `*`; the syntax review's S4 already did this for bare decimals |

118+| 18 (A23) | A gate may fit `*` | No code change; say in `core-language.md` that `*` may hold gates |

119+| 19 (A6, A100) | `[]` and `m()` are rejected in the parser, at the closer | Parser errors at the closer, with golden cases; make the EBNF's `tuple` rule take at least one item; delete the three "empty cell is not supported by partial inference" strings, and the checker's "a change takes at least one field" once the parser reports `m()` |

120+| 20 (A30) | `[a=@ud [a=@t b=?]]` is one record, so the duplicate `a` is an error | `+duplicate-fields` carries seen fields through unfaced tails; fix the comment above `+$ written-fields` in `jibb.hoon`, which says each written record has its own scope |

121+| 21 (A25) | `/% %foo` and `++ foo 1` may share a name | `+module-scope-valid` checks marks only against marks and molds, as the API scope check has done since `ce69a3b`; add golden cases for `/% %foo` beside `++ foo 1` and beside a prelude value in an ordinary module. Tell @iko that API modules already allow it |

122+| 22 (A15) | A `?-` arm that matches no remaining case is a definite error, "arm matches no case" | The core's usefulness check gives it; until then it reads "union pattern is not supported" |

123+| 23 (A55), 24 (A64), 27 (A61) | Match Hoon: no comparator in `(mop K V)`; keep both `each`s; the mark keeps dropping the final newline | No code change; record each in `decisions.md` |

125+| 28 (A136) | The printer flattens `[a [b c]]` and prints named molds by name | `+show-itype`, and the missing-tag message, which lists an imported union's cases (`union %no %yes has no case %other` in `types-missing-tag-imported`) instead of naming it, `choice.fixture`; many `types.txt` change, so do it with or after the core's one pipeline |

126+

127+One more was never asked: **A62**, whether the prelude's `+$ attr` should spell `pad` and `gap` with a `+$ space %s0 %s1 %s2 %s3` instead of eight constant cases. It adds a public prelude name, which is @iko's call. Ask with the others.

128+

129+Milestone-2-finish step 7 lists the same import gaps (A50, and A14 from step 1). Build A50 here once @iko confirms question 26, and say in the project chat when it lands, so that brief's builder doesn't build it again.

130+

131+## Step 6: the checker core

132+

133+[milestone-2-finish.md](milestone-2-finish.md), steps 2 to 4, describes the core and owns it. Whoever builds it should start from [the checker map](../reviews/2026-11-03-checker-map.md). The review's own advice for staging it:

134+

135+- Give `istate` a constructor first (A28, A125): it has 27 positional fields, built as literals at 10 places in `jibb.hoon`, so every field the core adds touches all of them. The 13 suites that use it bunt `*istate:jibb` and set fields by name, so they don't need to change.

136+- The partial report re-infers each definition on its own, so a new core can sit behind the report one definition at a time, before the full check changes (map, section 4.4).

137+- The program, page and store recovery arms run only for definitions still missing after ordinary resolution, so when the core resolves one ordinarily, its recovery arm stops firing and can be deleted with its tests kept.

138+- Keep `+itype-fit`'s three answers while old callers remain: `%unknown` should still mean "would need a deferred constraint".

139+- Budget the golden changes: question 6 moves every `types.txt` once, 347 on `master` today (283 when the review counted). Do that in one commit, with every changed output read.

140+

141+These findings close when the core lands, and nobody should patch them before: A11 (same-origin unions compared by their raw cases), A15 with question 22, A16 (variable kinds kept by self-bindings in six copied `+itype-walk` arms), A17 (three union-coverage loops), A21 and A35 (the type walkers and variable-kind disjunctions), A33 (`+infer-recursive-gate` retried after every failure), A36 (the call-argument copies in the check-mode dispatcher), A46 (the report's own resolver), A47 (the `dg-*` transaction), A48 (the program recovery arms), A49 (the generic tree proof), A132 (the prelude parsed again for each direct gate-layout proof), the rest of A42 and A130 (the report's entry chain, which parses and duplicate-checks the source again in `+golden-types-in-context` and repeats its eligibility guards, and the ten `+golden-types*` wrappers, which the one pipeline should reduce to the entry points hosts need), the rest of A45, and A121 and A122, the review's direction items on example-fitted slices and two pipelines.

142+

143+## When you're done

144+

145+- Every finding in steps 1 to 4 is fixed, each with its case, or written up in `open-questions.md` with the reason it was left.

146+- Every ruling @iko has confirmed is in `decisions.md` and built; the rest are still listed as waiting.

147+- Every check passes, under eval and on the ship.

148+- `status.md`, `compiler.md` and `open-questions.md` describe the code as it is.

149+- Everything is pushed to `master`, and a few lines go to Montelot in the project chat: what landed, what was left and why, and what waits on @iko or the core.

docs/prompts/syntax-review-follow-up.mdnew file+80

@@ -0,0 +1,80 @@

1+# Finish the 2026-11-02 syntax review's changes

3+A brief for the developer who finishes what the [2026-11-02 syntax review](../reviews/2026-11-02-syntax-review.md) started. Paste it as the first message of a session, or hand it to a person; it assumes a fresh start in the repo `iko-soy/jibb`. Written 2026-11-03, when S1, S2, S4 to S7, S11 to S13 and S15 landed on `master`.

5+---

7+You are finishing a set of syntax changes to Jibb, a UI language for Urbit: a Hoon dialect with an indentation layout. Its spec is in `docs/spec/`; the parser, checker and printer are `jibb-dev/lib/jibb.hoon`; the prelude is `jibb-dev/lib/jibb/prelude.jibb`. On 2026-11-03 Montelot decided ten of the review's fifteen proposals, and they were built the same day, each on its own branch with its own golden cases, then merged. What is left is the gaps those builds reported, four adversarial reviews that didn't finish, and work that waits on the new checker core.

9+## What landed

10+

11+Each proposal is a section of the review, numbered S1 to S15, and a row of `docs/spec/decisions.md` dated 2026-11-03.

12+

13+| # | What it does now | Where to look |

14+| --- | --- | --- |

15+| S1 | `(unface e)` removes every face from `e`'s type, through cells, a gate's sample and product, containers' arguments and the unit's payload; unions and recursive molds go by name and are kept whole. It is reserved with `proj`, is not a value, and `++ f (unface \|= …)` is still a gate | grammar.md "Unface", `+itype-unface`, `+reserved-name`, `inline-unface-*` |

16+| S1 step 1 | Decided, not built: a capital that meets a faced position binds only the type under the face | decisions.md Inference row, `inline-unface-labelled-slot` |

17+| S2 | A body's final line hands the lines after it at its depth to a tall `\|=`, `^-` or `~&` that ends it; a `?-` that begins a body's final line may take its arms at its own depth | grammar.md "The rest of a body", `lex-body-rest-*` |

18+| S4 | A bare decimal is a `@ud`: it fits `@u`, `@` and `*`, and no other aura, unless its `++` is generic over its aura | grammar.md Literals, `inline-decimal-*` |

19+| S5 | A bare pattern name is an error where a case the pattern can match has a tag there that the name spells | grammar.md Patterns, `inline-pattern-tag-name-*` |

20+| S6 | A change's item may name a wing through record fields, `m(open.cart=x)`; overlapping items are an error | grammar.md Expressions, `inline-change-wing`, `types-change-*` |

22+| S11, S12, S15 | Spec wording for deeper lines and nested patterns; the examples build their models with faced cells | grammar.md Lexical rules and Patterns |

23+| S13 | A cast whose expression takes the deeper lines ends its owner line; the prelude, my-app and the spec's examples use the canonical layout, with flat `?-` arms | grammar.md Spacing, prelude.jibb |

24+

25+## Read first

26+

27+1. `docs/README.md` and `docs/development.md`: the ground rules, the checks, and how golden cases work.

28+2. The review's sections for S1, S2, S4, S5, S6, S7 and S12, and decisions.md's rows dated 2026-11-03.

29+3. `docs/status.md`, the rows that name S1 to S7: each says what is partial.

30+

31+Then run `tools/check`. Everything should pass before you change anything.

32+

33+## Ground rules

34+

35+- **The spec wins**, and a language question is Montelot's to decide, as the 2026-11-03 rows were. Where this brief would decide more of the language, it says so, and you ask instead.

36+- **Another thread is building the checker core** that review question 5 asks for: union-find with levels, deferred constraints and a usefulness check for `?-`. It will replace `+itype-unify`, branch joins, `?-` exhaustiveness and pattern binding. Don't patch those for S1 step 1 or face joins; that thread owns them. Ask in the project chat what has landed before you touch the checker.

37+- **Every change is a golden case or a test arm**, and every check passes, the ship group included (`nix flake check` runs it on a fresh fake ship, or see `docs/development.md`).

38+- **Push straight to `master`**, rebased, in commits that each leave every check passing.

39+- **Keep docs current**: the status.md row for each capability, decisions.md when something is settled.

40+

41+## Step 1: finish the adversarial reviews

42+

43+The reviews of S2, S4, S6 and S7 didn't finish before the merge. For each, try to break it: probe edge cases the golden cases don't cover, check that the spec says exactly what the code does, and check every golden output the change touched. Fix what you find, with a golden case for each fix. The probe recipe is at the end of the review.

44+

45+Known already:

46+

47+- **S2.** A body of 40,000 same-depth `~& x` lines runs out of memory under eval, where 40,000 nested parentheses don't: each rest is a level of recursion in the parser. Make the rest loop iterative, if that stays small. Some new ok cases have no `types.txt` because the partial checker can't type them (`lex-body-rest-ok-3`, `-5` and `-6`).

48+- **S4.** Number patterns are checked against the subject only on known-union and atom subjects. The unit, list, loobean, single-case and deferred `?-` paths don't check them, so `[~ 0]` against a `(unit @dr)` falls through to older messages. A constructor applied directly, `(|=%wait 30)`, and a call whose head is still a variable keep the generic "call's sample and argument types do not unify".

49+- **S6.** A wing through a union field's site note reads just "field `data`", with no type. The inference-level "repeated change fields" check is now unreachable from the module entry points, because the duplicate pass reports overlaps first; keep it as a safety net or remove it.

50+- **S7.** A few messages still say "capital", as "use the same capital for a shared type". Names live in the bits of a variable's ID (`+named-var`, `+var-name`), so any test that compares a prelude scheme's IDs exactly must use the named IDs.

51+

52+## Step 2: close S1's and S5's gaps

53+

54+- `unface` on an argument whose type isn't known yet, as `|= f (unface f)` or `|=(g (unface g))` passed where the call fixes `g`, says "not supported by partial inference". The spec says it waits, as wing access does. Make it wait when the deferred path can, and fail closed otherwise. The check also looks only at the top of the type: a faced variable passes and a bare one is refused.

55+- Islands, pages and stores that find `init`, `update`, `load` or `view` by a literal `|=` (around the program, page and store recognisers) don't see through `unface`. `++ update (unface |= …)` should be a gate there, as it is for recursion (`+unfaced-gate`).

56+- Golden cases for `unface` over a set, a map and a jug, which the code handles but no case shows. `inline-unface-unknown`'s about.txt cites the wrong spec sentence. `(unface)` gets a different error in a `++` body and as a call argument; make it one.

57+- S5's exemption for a union's generic arguments works by type equality, so a concretely typed position whose type happens to equal an argument is skipped. Make it follow where the mold puts the type variable. The full module check reports an S5 error only as "module definitions need unsupported inference"; give it the partial report's message and sites.

58+

59+## Step 3: after the checker core lands

60+

61+These wait on the core from review question 5. Coordinate with that thread first.

62+

63+1. **S1 step 1** is the core's job, with a golden case each for `(hunt lt-a `1 `2)`, `(roll ~[1 2] 0 add-f)` and `[A A]` against `[x=@ y=@]`. The same thread makes joins keep a face once a position has taken one, so `~[lt-u lt-a lt-c]` and `~[lt-a lt-u lt-c]` are errors alike (today the first checks and the second doesn't). Update `inline-unface-labelled-slot` and `inline-unface-lambda` when it lands.

64+2. **The prelude's `args=` gates.** Thirty prelude gates take an unfaced `args=[…]` and open a one-arm `?-` to name its parts, only so that they fit slots with any labels. With step 1, write them with labelled samples, `++ weld |= [xs=(list A) ys=(list A)] ^- (list A)`. Use `(unface |=(…))` only for small gates mostly passed as values, as `lth`, `gte` and `lte`. Each rewrite must keep the gate's type report.

65+3. **S12, later part.** Flatten the eight prelude gates that nest a `?-` inside another's arm to look at two values (`both`, `clap`, `hunt`, `mate`, `clef`, `join`, `snip`, `rear`) into nested cell patterns, as the review shows for `hunt`. The partial checker says "branch is not supported" for those today, so wait until the core types nested patterns.

66+

67+## Step 4: lowering, at milestone 3

68+

69+When the lowering to the core language is built, `(unface e)` lowers to `e`, a `++` whose body is `(unface |= …)` joins its group's `rec` as a gate, and a wing item in a change lowers to an edit at the wing's axis (core-language.md says how).

70+

71+## Questions to ask, not decide

72+

73+Put these to Montelot in the project chat, each with a recommendation, and record the answers in decisions.md:

74+

75+1. **What faces does a cast's result keep?** `^- $-([@ud @ud] ?) lt-a` drops the gate's labels today (the fall-through at the end of `+itype-merge-faces`), while `^- [@t @ud] r` keeps a record's. The critique recommends that a cast never removes faces, so `unface` is the one place labels go.

76+2. **May a flat arm's bare-name pattern hide a prelude name?** With flat arms, Hoon's habit of writing `?:`'s else branch back at the rune's column, as `dec a`, parses as a catch-all arm binding `dec`. Today "pattern binder shadows a name" catches it. If S3 ever lands, it wouldn't.

77+3. **Is a `|=` or `~&` that ends a body's final line written flat or with a deeper body by the formatter?** The prelude keeps deeper bodies for `flit` and `bond`.

78+4. **When named type variables merge, which name prints?** Today a capital written in the `++` wins, otherwise the one made first, so `(cork fk fv)` prints `cork`'s `A`, not `fk`'s `Key`.

79+

80+The review's other proposals (S3, S8, S9, S10 and S14) weren't decided. Leave them unless Montelot asks.

docs/reviews/2026-11-02-syntax-review.md+14

@@ -6,6 +6,20 @@ How it was done: five reviewers each read the spec, the prelude, the example des

77This review does not restate the language rulings that [the repository review](2026-11-02-questions.md) raised (questions 16 to 28, now listed in [open-questions.md](../open-questions.md) under "Review rulings waiting for @iko"). Where a proposal extends one of them, it says so. Proposals here are numbered S1 to S15 so they don't collide with those numbers. "Review question N" means a question in that file, and "open question N" means item N of [open-questions.md](../open-questions.md).

9+## Outcome, 2026-11-03

10+

11+Montelot decided ten of the proposals on 2026-11-03, and they were built the same day. [decisions.md](../spec/decisions.md) has a row for each, dated 2026-11-03, and [prompts/syntax-review-follow-up.md](../prompts/syntax-review-follow-up.md) lists what is left.

12+

13+| # | Decision | Built |

14+| --- | --- | --- |

15+| S1 | Not as proposed: an explicit `unface` that strips every face from a type, reserved like `proj`, instead of ignoring sample names when gates unify. Step 1 too: a capital binds only the type under a face | `unface` yes; step 1 waits for the checker core of review question 5 |

16+| S2 | Yes, and a `?-` that begins a body's final line may also take its arms at its own depth, without indenting them | Yes |

17+| S4, S5, S6, S7 | Yes | Yes, with gaps listed in the follow-up prompt |

18+| S11, S12, S13, S15 | Yes; S12's prelude rewrite waits for a checker that types nested patterns | Yes |

19+| S3, S8, S9, S10, S14 | Not decided | No |

20+

21+The sections below are the review as written on 2026-11-02, before these decisions.

22+

923## Summary

1024

1125- **The syntax is in good shape.** Open brackets without closers, tightness as the one disambiguator, one exhaustive `?-`, named unions, `|=%tag` constructors and named changes all read well, and nearly every slip the reviewers tried gets an error at the right character. The [keep list](#what-to-keep) says what not to change.

docs/reviews/2026-11-03-checker-map.mdnew file+587

@@ -0,0 +1,587 @@

1+# The checker on 2026-11-03, and what a general core replaces

3+A map of the type checker in `jibb-dev/lib/jibb.hoon`, written for whoever builds the general checker core that [review question 5](2026-11-02-questions.md) chose. It was written by the thread that fixed the [2026-11-02 review](2026-11-02-repo-review.md)'s findings, by reading the code; nothing in it was run. Claims about which tests would fail come from the tests' fixtures, their direct `name:jibb` references, and the code paths.

5+Line numbers without a file are `jibb-dev/lib/jibb.hoon` at commit [`f84a29e`](https://github.com/iko-soy/jibb/blob/f84a29e/jibb-dev/lib/jibb.hoon) (15,838 lines). The syntax changes of 2026-11-03 (`d4aed71` to `706e9ca`: `unface`, S2, S4 to S7) moved them by up to about 800 lines. They added `+itype-unface`, `+infer-unface`, `+unfaced-gate`, the `+decimal-*` arms, `+tag-name-pattern`, `+change-wing-field`, `+wing-overlap` and named type variables kept in the bits of a variable's ID (`+named-var`, `+var-name`, `+show-var`), and renamed `+module-has-reserved-proj` and `+reserved-proj-*` to `+module-has-reserved` and `+reserved-*`. This map doesn't cover them, and its rows in 6.2 for S1, S4, S5, S7 and S12 predate Montelot's decisions of that day; read `decisions.md`'s rows dated 2026-11-03 instead. Find an arm by its name, not its number. Review finding numbers (A1 to A137) come from [the review](2026-11-02-repo-review.md), whose own line numbers are pinned to `4bf477e`.

7+Review Q5 (`docs/reviews/2026-11-02-questions.md:43-49`) was answered (a): *"Build the general core

8+first: union-find bindings with levels, a deferred-constraint queue and Maranget's usefulness check,

9+with `main = (program …)` checked as an ordinary application."* Q6 (l.51-56, one golden pipeline),

10+Q11 (l.88, one branch-join rule) and Q12 (l.95, dependency-order pass) were also chosen.

11+

12+## 0. Numbers

13+

14+| Thing | Value |

15+| --- | --- |

16+| `%type-inference` chapter | 4601-10901 (325 arms) |

17+| `%union-analysis` chapter | 10902-15838 (224 arms). Despite its name it holds union analysis (10902-11302), the module checker, API derivation, program/store recovery, the report and the dg-* transaction (A131) |

18+| Arms and types from 4601 on | 549 `++` arms, 91 `+$` types |

19+| `itype` | 22 cases (4663-4686), six of them variable kinds plus `%tag` |

20+| `istate` | 27 positional fields (5996); built as a positional literal at 10 sites (10699, 10752, 11986, 12001, 12057, 12735, 12769, 14759, 14924, 15107) and bunted at 5 (14497, 14550, 14566, 15610, 15652) |

21+| Program/store/page/static recovery and kind code | 13146-14648 (1,503 lines) |

22+| dg-* deferred transaction | 15147-15719 (573 lines) |

23+| Direct gate-layout evidence | 9002-9228 (227 lines) |

24+| Lines saying "unsupported" or "not supported" | 283 |

25+| Golden cases | 690 in `tests/golden`; 304 have `types.txt`, every one of which starts `partial inference; module not checked`; 177 of those also have `modules.txt` (module-check mode, prepared prelude); 127 of the 304 contain an "unsupported"/"not supported" line |

26+| Suites | 58 files in `tests/lib` (the 57 checker-related suites of the brief plus `jibb-check-spans`/`jibb-hoon-reference`, which are not checker tests); they reference 125 distinct `jibb.hoon` arms and 55 types by `name:jibb` |

27+| Call sites | `itype-fit` 59 (22 in 13311-14648), `itype-unify` 43, `itype-normalize` 95 (20 in program/store, 7 in dg), `instantiate-scheme` 17 (12 in program/store), `itype-merge-faces` 13 (12 in program/store), `direct-invariant` 19 (16 in program/store), `template-apply` 22 (15 in program/store), `add-supported-result` 7 (6 in program/store) |

28+

29+## 1. The checker as it is

30+

31+### 1.1 Data types

32+

34+| --- | --- | --- | --- |

35+| `itype` | 4663 | `%var %fvar %avar %rvar %nvar %rnvar` (one id space), `%atom aura`, `%any-atom` (bare `@`), `%flag`, `%noun`, `%empty`, `%tag [id literal constructor=?]`, `%const literal`, `%collection [name args]`, `%recursive [module name label]`, `%jrec [at name label head aura tail]`, `%grec [at name label proof=shape args]`, `%union [cases origin label args]`, `%face [name body]`, `%fn [sample product]`, `%cell [hed tal]` | The whole type language. `%var` unconstrained; `%fvar` gate-free; `%avar` any atom incl. `?` and `@`; `%rvar` atom other than `?` (arithmetic); `%nvar` decimal literal, defaults to `@ud`; `%rnvar` both. `%tag` is a pending literal resolved by binding its id. Faces and display labels live inside the type, so relabelling changes equality (A11). `%collection` is opaque except list/unit (A13). Three recursive representations (`%recursive` imported, `%jrec` qath-shaped, `%grec` test tree) |

36+| `ibinding`, `isub` | 4687-4688 | `(list [id val])` | Substitution as an association list; first entry wins; entries only prepended; no path compression. Kind refinement is encoded as a self-binding (`[n -> %fvar n]`, `[n -> %rvar n]`, `[n -> %rnvar n]`) |

40+| `ischeme`, `ienv`, `imold-types` | 5804-5806 | `[typ vars=(list @ud)]`; `(list [name scheme])`; `(list [name template])` | Schemes with raw (not canonical) quantified ids; environment is newest-first, linear `ienv-lookup` (6001) |

41+| `iderived`, `iwidth-definition`, `iwidth-dependency` | 5807-5809 | | Derived poke constructors; `proj` elaboration evidence (carries the raw `sub`, 10687) |

42+| `irequest-evidence`, `istore-request-evidence`, `irequest-graph` | 5812, 5816, 5820 | | Source-bound API/store request certificates and the trusted closure inputs |

44+| `ijimports`, `icap(s)`, `iparams`, `imolds`, `iexternals`, `imark-externals`, `ihole` | 5823-5834 | | Imports in scope; written capitals with their var ids; generic params; local mold shapes; raw importer nouns; type holes (created 7103) |

45+| `iwfield(s)`, `iwstep`, `iwidth-result`, `iwprojection` | 5839-5843 | | Record-spine scan and `proj` plan |

48+| `dgo` | 5995 | `[left right at context]` | Deferred fit obligation (dg-* only) |

49+| `istate` | 5996 | `next sub caps binders molds globals externals surs mark-externals marks jimports reserved-molds params active tags in-mold at top-molds prelude holes jrec-fuel projections gate-defs head-evidence grec-index defer obligations` | Threaded functional state. `next` restarts at 0 per top-level definition. Recovery-only fields: `jrec-fuel`, `gate-defs`, `head-evidence`, `grec-index`, `defer`, `obligations` |

56+| `iwidth-elaboration` | 8994 | | Dead (only the dead `infer-width-elaboration`) |

57+| `igate-entry`, `igate-seeds` | 10433-10434 | | Recursive-group seeds |

59+| `iadj ivisited iwork iwresult icresult icomponents` | 10553-10558 | | Kosaraju state |

61+| `icyclesite`, `icycle` | 10788-10789 | | Value-cycle proof |

62+| `upat`, `urelation`, `upair` | 10909, 10919, 10920 | `%unknown %all %empty [%atom (unit @)] %flag [%cell] [%or]`; `?(%disjoint %overlap %unknown)`; `[first second relation]` | Noun-shape projection for disjointness/overlap (also used by the importer at 6463, 6645) |

63+| `uow-case` | 11191 | | Source overlap witness case |

64+| `jsource jbundle jcache jfile-result jfile-overlap jfile-failure jfile-detailed-result jimports(-detailed)-result` | 11507-11518 | | Module sources, per-invocation cache, results with structured overlap evidence |

68+| `iapi-*` | 12328-12706 | | API path/request/support evidence |

69+| `ione-request-interface`, `imulti-request-gates` | 12780, 13043 | | API constructors |

72+| `igate-free-mold` | 14885 | | `gate-free-mold-source` result |

73+| `dgscan`, `dgcommit`, `dg-step`, `dgparse` | 15149, 15243, 15444, 15581 | | dg-* transaction |

75+

76+### 1.2 Pipelines

77+

78+#### (a) The partial golden-types report (all 304 typed goldens)

79+

80+Entry chain:

81+- No prelude (127 typed goldens): `golden-types` 11486 → `golden-types-imports` 11497 → `golden-types-with-marks` 15016 → `golden-types-in-context` 15021 → `golden-types-in-context-core` 15025. `tools/golden:248-253` picks the arm by whether the case has `/sur` or mark fixtures.

82+- Module-check mode (177 typed goldens with `modules.txt`): `tools/golden:254-260` calls `golden-types-with-prepared-prelude` 14975 with a prelude prepared once under `mule` by `prepare-prelude-with-internal` 12103 (`tools/golden:291`), falling back to `golden-types-with-prelude-and-internal` 14969. 14975 parses, runs `duplicate-defs`, `module-scope-valid` 14986, and **resolves Jibb imports with the full checker** (`resolve-jibb-imports` 14989 → `infer-jibb-file-detailed` per imported module), then calls the core.

83+

84+`golden-types-in-context-core` 15025-15146:

85+1. Parse (15029), `duplicate-defs` 15031 (→ `duplicate-fields-report`), reserved `proj` 15033 (bare `'module has reserved proj name'`, no header, A43).

86+2. `resolve-groups` 15040: the same resolver as the full check (10662 → `resolve-groups-core` 10736) but **with no grec index**, so `%grec` never arises here; no program/store recovery, no kind checks.

87+3. `definite-value-cycles` 15041.

88+4. dg-* transaction if eligible (15044-15075): import-free, not API/store, no `main`, incomplete, ≤65,536 bytes, ≤64 defs, and either no prelude + `dg-source-candidate`, or the exact prepared prelude + `dg-prepared-candidate`. Names it adds are "recovered" only if the transaction env is complete and `dg-interface-safe`.

89+5. Per definition in source order (15079-15146): molds → `show-partial-mold` 11431 (never infers the mold; hole report, union disjointness verdict or `not checked`); duplicate name → `name already in scope`; cycle → `non-gate value depends on itself through a cycle`; recovered/grouped → print the scheme from env; otherwise **re-infer the definition afresh** (state literal 15107, `gate-defs`/`head-evidence` 15108-15109, `reserve-def-caps` 15110; gates through `infer-recursive-gate` 15113, others `infer-fragment` 15114) and finalize with its own copy of the finalization (15117-15143, table in 2.8), then `canonical-itype` 15144 + `show-itype` + `show-atom-constraint`.

90+

91+So a report line is not the scheme the resolver published; it is a second inference against the resolved env. The report never runs recovery, kind checks or grec; its messages are the raw per-definition failures.

92+

93+#### (b) The full module check

94+

95+`infer-jibb-file` 14650 (text adapter) → `infer-jibb-file-detailed` 14658-14879:

96+1. Parse 14661 (`module source does not parse: /p`), `duplicate-defs` 14664, API module with `main` rejected 14666.

97+2. `/ui/api/...` branch 14668-14725: `api-poke-interface-result` 12979 first; else `api-derived-clash` 14678, scope with mark rules 14684-14698, prelude required 14699, `resolve-jibb-imports-detailed` 14705, `+$ paths` required 14708, then the "narrow" `one-request-interface-graph` 14711-14721 or `multi-request-interface-graph` 14722-14725. No value inference beyond `api-support-analysis-*` (12708, 12742), which calls `resolve-groups`.

98+3. Other modules: `program-main-def` 14726 and the syntactic recognisers `program-main-parts` 14728, `page-main-parts` 14730, `store-main-parts` 14732; `store-declaration` 14734 (definite clash 14736; `module kind or scope needs unsupported inference` 14740); a `/ui/stores` main that is not a store is rejected 14741.

99+4. `module-scope-valid` 14745, `resolve-jibb-imports-detailed` 14748 (mutual recursion with this arm; cycle check before cache, cache reuse rules 12275).

100+5. Molds: `grec-collect-molds` 15825 only for import-free modules (14750-14752); istate literal 14759; grec index only for import-free prelude-backed modules whose prelude list is exactly `[[%collection %list ~[[%var 0]]] ~[0]]` and that have no local `list` (14762-14772); `module-mold-types-detail` 11799 (first failure aborts; overlap evidence rendered 14774-14780).

101+6. Values: `resolve-groups` or, with an index, `resolve-groups-core` (14781-14784). `resolve-groups-core` 10736-10756: compute names, graph, Kosaraju components, `direct-prelude-evidence` (prelude re-parse) and `dependency-order` 10768 once, then loop: `add-supported-defs-core` 10690 over the ordered defs (fresh positional state per def with `next=0`, `jrec-fuel=256`, `gate-defs` = `direct-checked-gates` of the current env, `head-evidence`; `reserve-def-caps`; `infer-fragment`, then `infer-recursive-gate` if that failed; `add-supported-result` 10670, which **silently drops** any failure or pending tag), then `add-groups` 10645 (cyclic components through `infer-gate-group` 10509), until env stops changing.

102+7. Program recovery chain 14786-14804, only for a direct `(program i u v s)` main: `program-update-context` 13346 → `program-subs-context` 13508 → `program-view-context` 13938 (keyed) → `program-plain-view-context` 13858 (only if keyed declined) → `program-plain-init-context` 14238 → `program-main-context` 14472. Single pass, fixed order, each arm a no-op unless its component (and `main`) is still missing.

103+8. dg fallback 14807-14816: only if incomplete, not a store, no imports **and no prelude** (14809), so it can never affect a prelude-backed check (A47).

104+9. Completeness 14817-14832 (store modules exclude `main`): `module-pending-tag` 10715 (re-infers ≤64 missing defs to find `nothing fixes the union of %x`), then `module-sample-shadow` 12171, then `module definitions need unsupported inference: /p[: ++ name]` with `module-missing-value` 12132 choosing the name.

105+10. `request-graph-merge` 14834; static main swap 14836-14843 (`static-main-specialized` 14487); store main swap 14844-14849 (`store-main-closed` 14599); kind boundary 14850-14857 (`program-main-closed` 14555, `page-main-closed` 14540, store/static results) → `module kind needs unsupported inference: /p`; store-derived exports 14858-14875; `request-graph-bounded` 14876; `ifile` 14878.

106+

107+#### Where the two pipelines differ (A46, A122)

108+

109+| | Report (a) | Full check (b) |

110+| --- | --- | --- |

111+| Resolver | `resolve-groups`, grec index `~` | `resolve-groups-core` with index when import-free |

112+| After resolving | re-infers each definition and prints its own failure | keeps resolver env; failures are silent |

113+| Recovery | none | program chain, static/store main swaps |

114+| Kind checks | none | `program-main-closed`, `page-main-closed`, store, static |

115+| dg-* | eligible with or without prepared prelude (15053-15061) | only without prelude (14809) |

116+| Finalization | 15117-15143 (adds `pending-null`, hidden recursive/generic, merged-capitals messages) | `add-supported-result` 10675-10689 (no `pending-null`, no hidden-name check, merged capitals caught only as `constrained-capitals`) |

117+| Mold check | `show-partial-mold` (projection only) | `module-mold-types-detail` (real templates) |

118+

119+### 1.3 Families, by layer

120+

121+"Category": G general inference, U union analysis, M module and imports, A API and paths, R recovery slice, P reporting/printing, O other. "Tests" lists suites (without the `jibb-` prefix) and goldens; `[call]` marks suites that name the family's arms directly.

122+

123+#### A. Substrate (4601-6400)

124+

126+| --- | --- | --- | --- | --- |

127+| Chapter contract, `itype`, `isub` | 4601-4689 | G | Contract comment 4603-4661 (assoc-list sub, occurs check, per-definition generalization, monomorphic binders, capitals shared per definition, `@` one-way, unions keep origin/args; `proj` limits 1,024/4,096; "The unchanged todo API fits this fragment" 4643-4644; closed gate sample may omit one outer face 4653-4655) | every `types-*`; 32 suites build `itype:jibb` |

128+| Lookup, walk, occurs, normalize | 4691-4732, 4817-4843, 6012-6026 | G | Linear `itype-lookup`; `itype-walk` follows chains for the six var kinds and `%tag`, stopping only at a self-binding to `%fvar`/`%rvar`/`%rnvar` (six copied arms, A16); `itype-occurs` (opaque `%recursive`/`%jrec`; same-id `%tag` counts); `itype-normalize` full zonk, leaves `%tag`/`%recursive`/`%jrec` | typecheck, hole-guards [call], arithmetic-guards [call], deferred [call], generic-construction [call]; `types-partial-occurs`, `types-partial-dependency-chain`, `types-partial-shared-tvar` |

129+| Emptiness and inhabitation | 4734-4815 | U | Budgeted; `itype-empty-proof` proves only emptiness; `itype-inhabited-proof` three-valued (`%var` yes only via written capital; only list/unit collections decided, A13; `%grec` via `grec-tree-proof` 4801); `itype-live-cases` drops proven-empty cases, any unknown → `~` | empty [call]; `types-list-patterns`, `types-partial-union-edges`, `types-union-finite-limit`, `types-tuple-context` |

130+| Unification | 4851-4940, 5005-5012 | G | `(unit isub)`, no reason. Walk both, equal → ok; grec by at+name then args; jrec by 5 fields; recursive by module+name; union by origin, then raw `cases` equality when argless (A11) else args; collection by name then args; `%var` binds anything after occurs; `%fvar` via `itype-bind-gate-free`; atom-kind lattice 4884-4925 (nvar~rvar → rnvar with self-binding 4887-4889); const by value; atoms of different aura fail (no widening); face~face same name; fn/cell pointwise | typecheck, arithmetic-guards, gate-free-guards, generic-recursion [call]; `types-arithmetic-*`, `types-partial-atom-*`, `types-union-phantom-generic` |

131+| Gate-free propagation | 4942-5003, 6320-6343 | G | `itype-gate-free-form` (budget; unbound `%var` → self-binding to `%fvar`; fails on fn/noun/tag/recursive/grec); `itype-bind-gate-free` 256 (exhaustion reads as mismatch); `itype-collection-keys` for set/map/mop/jar/jug keys; `itype-var-is-gate-free-fuel` fails open at fuel 0 | gate-free-guards [call], gate-free-source; `types-prelude-unit-helpers` |

132+| Directional fit | 5014-5019, 5451-5711 | G | `itype-fit` = `itype-fit-inner` + empty-source rescue (256). About 45 ordered guards: width (spine ≥1,024 or wider source → unknown); empty/flag-vs-`@f`; `*` accepts anything incl. gates (A23) and binds bare tags to `*` (A22); actual `*` only to a var; grec/jrec/recursive by identity; unions by origin; known union to var by unify; non-var vs union → `itype-fit-cases` (unique %ok wins, two → unknown); tags: ctor only vs fn via `itype-fit-ctor-cases`, term vs `@tas`/`@ta` with no aura check (A20), vs `?` if 0/1, vs `@`; zero vs list → unknown; var vs face unifies with the body (5652); `@` turns a var into a fresh `%avar` (only allocation, 5666); atom by `aura-prefix`; cells head then tail; faces same name; closed gates by `itype-closed-gates-match`; last resort unify, with failures turned to `%unknown` when unions, recursion or related auras are involved. **Gates (fn vs fn) only unify: no variance** | closed-gate-guards, constructor-fit-guards, empty, qath-fuel, generic-construction, arithmetic-guards, generic-recursion, deferred [call]; 32 golden lines `call constraint…`, 37 `cast constraint…` |

133+| Aura families | 5049-5092 | G | `aura-prefix` textual prefix (`@` above all); `itype-family-related` only to turn failures into unknown | `types-partial-aura*`, `types-partial-atom-widening`, `types-partial-branch-widening` |

134+| Branch joins | 5094-5097, 5125-5210 | G | Unify, else `itype-concrete-join` (prefix parent or `@`, never touches sub); n-ary: unify all, else first `@` or common prefix parent present among arms | `types-partial-branch-widening`, `types-list-branch`, `types-union-branch-*`, `types-recursive-branch`, cell-branch, deferred |

135+| Face guards | 5212-5227, 5265-5349 | G | `itype-face-asym` (face on one side vs non-var); `itype-merge-faces` (cast result, 1 + 12 recovery calls); positional rules `itype-positional-face-asym`/`-slot-face-asym` (added with `like`, 640a442); `itype-output-may-be-cell` | positional-face-guards [call], direct-gate-guards [call], deferred [call]; `types-positional-faces`, `types-prelude-like`, `types-generic-face-inference`; 4 golden lines `call result face propagation` |

136+| Closed gate sample matching | 5229-5263 | R | See 3, R12 | closed-gate-guards (via `itype-fit`), todo-api |

137+| Fail-closed structure guards | 5020-5046, 5098-5123, 5372-5449 | G | `itype-has-any-atom/-tag/-union/-recursive/-hidden-generic/-hidden-recursive`; `itype-has-fixed-atom` (5098) is dead | `types-union-unresolved*`, `types-generic-union-escaping`, `types-qath-module-identity` |

138+| Pending tags | 5351-5370 | G | `pending-tags`, `pending-null`, `pending-tag-diagnostic` (`nothing fixes the union of ` + `show-lit`, 5363); checked only at definition end | buttons (`tests/type-buttons/error.txt`), program-init, program-update, deferred [call]; 80 golden lines `tag needs context`, 24 `` `~` needs context `` |

139+| Self-test | 5713-5798 | O | `itype-unify-test`, compared by `jibb-typecheck` with `tests/checker/unification.txt` (the old `tools/hoon` check is gone) | typecheck [call] |

140+| State, env, results | 5800-5806, 5824-5827, 5832-5834, 5995-6006 | G | see 1.1 | 13 suites build `istate:jibb` |

141+| Interface/evidence types | 5807-5823, 5828-5831 | M | see 1.1 | module-*, api-evidence, store, program-watch |

142+| Record width and `proj` | 5835-5923 | O | `width-scan` (closed uniquely faced spine), `width-known-shape`, `width-shape` (wider source → `record width constraint needs unsupported inference`), `width-proj-shape`/`width-project` (source-order planner, 4,096) | proj-guards; `types-proj-*`, `types-partial-projection` |

143+| Gate-free proof with witness | 5925-5992 | O | `gate-free-type` on normalized types; budgeted; list/unit only (A13) | gate-free-guards, gate-free-source, empty, generic-recursion [call]; program-main |

144+| Defaulting, promotion, holes | 6028-6181 | G | `promote-restricted-numbers` (only with written caps), `default-hole-numbers` (only when the type has no gate), `unresolved-hole`, `default-decimals` (`itype-has-gate` treats `%grec` as gate-bearing, ignores union args), `uncertain-hole-msg` | hole-guards [call], generic-recursion [call]; `types-hole-*`, `types-partial-decimal-default` |

145+| Vars, rename, canonical, instantiate | 6183-6318, 6345-6368 | G | `itype-vars` order (fn sample before product, head before tail, union args before cases); `unique-type-vars` O(n²); `itype-rename` single pass, no sub; `canonical-itype` kind precedence rvar > avar (nvar/rnvar → avar) > fvar > var; `instantiate-scheme` pushes fresh fvar/avar/rvar ids onto `binders` | gate-free-guards [call]; `types-partial-generalization`, `types-partial-atom-alias`, `types-many-variables`, `module-import-atom-scheme` |

146+| Local capital and mold lookup | 6370-6395 | M | `icap-lookup`, `find-simple-mold` (unique only), `collect-simple-molds` | 5 suites [call] |

147+

148+#### B. Import bridge and mold elaboration (6397-7253)

149+

151+| --- | --- | --- | --- | --- |

152+| Imported Hoon validation and bridge | 6397-6728 | M | `jibb-face-name`, `rec-pattern(s)` (self-recursive disjoint fork → opaque `%recursive`), `imported-faces-valid` (repeated face on a spine fails), `import-to-itype(-standard)` (aura whitelist u ud ux uv t ta tas p da dr tD, duplicated at 6432, 6557, 12666, A14; `%f` pair → `?`; `%unit` → prelude unit union only with the standard template, A10; other forks → originless `%union` after pairwise `union-relate`), `find-imported-mold(-prelude)`, `find-imported-mark(-prelude)`, `collect-sur-imports`, `collect-mark-imports`. 6682-6683 dead (A18). All failures `~` | bridge, api-evidence [call], import*, mark-bridge, tlon-bridge, poke-bridge; `types-import-*`, `module-import-api-*` |

153+| Interface lookup and relabelling | 6730-6841 | M | `find-jibb-interface`, `find-jibb-mold` (~40 callers), `itype-in-import` relabels unions/jrec/grec (display only), `prelude-union-alias`, `identity-union-parameters` | generic-alias, ask-guards, store, page-main, program-watch, todo-full, theme [call]; `module-import-*`, `types-union-print-*` |

154+| Mold elaboration and templates | 6843-6919, 6970-7000, 7099-7253 | G | `infer-simple-shape` (shape→itype; holes allocate a var + `ihole`; unions need `union-pairs` without overlap, else the source slice; local mold expansion guarded by `active`; generic local mold re-elaborated with params bound; generic local unions refused 7216-7217); `template-apply(-sub)` renames scheme vars to args (`template-apply` drops the sub); `infer-mold-template` builds +$ schemes, generalizing exactly the params; `label-direct-union` gives a top-level union its origin | union-source [call], gate-free-guards [call]; `types-generic-*`, `types-hole-*`, `types-union-alias` |

155+| Source-recursive recognisers | 6921-6967 | R | `simple-source-recursive` (`%jrec`), `simple-source-generic-recursive` (`%grec`). See R17, R18 | qath-*, generic-recursion [call] |

156+| Import-invalid replay | 7002-7097 | M | Replays a failed shape to recover the importer's `[%invalid …]` message with site note `invalid imported mold` | import, import-diagnostic, import-overlap, import-structural |

157+| Gate samples | 7255-7300 | G | `infer-sample`: binders fresh `%var`, monomorphic, pushed onto `binders`; shadow → tape `sample shadows a name` | `types-partial-shadow-global`, `module-import-*-shadow` |

158+| Local definitions | 7302-7373, 7514-7702 | G | See 2.7; generalization subtracts `free-env-vars` and `free-cap-vars`; order-independence machinery `shared-types`/`shared-moved`/`closed-local` | `types-local-*`, `types-partial-locals`, `types-local-scc*` |

159+| Capital scope walker | 7375-7512 | G | `scope-*` syntactic walk; `reserve-def-caps` allocates one `%var` per written capital per `++` | `types-local-capitals`, `types-capital-distinct` |

160+| Record field access | 7704-7747 | G | `record-fields-named` on a known faced spine; no deferred has-field constraint | program-init/main/update/watch [call]; `types-record-faces` |

161+

162+#### C. Expression checker (7749-10032)

163+

165+| --- | --- | --- | --- | --- |

166+| Contextual branches and list literals | 7749-7921 | G | `infer-union-context` (two loobean arms or unit arms with the same expected type, no join), `infer-list-context` (exact prelude list scheme; cons only under list context), `infer-open-list-items`/`infer-list-items` (drifted copies, A17), each with the `element` fallback hook (R7) | `types-list-*`, `types-flag-branch-context`, `types-union-branch-context`, deferred-context, todo-partial |

167+| Unit and list two-arm branches | 7923-8075 | U | Hand-coded two-arm exhaustiveness (`~` + `[~ x]`, `~` + `[h t]`); unit recognised structurally (no origin check); inhabitation 256 | empty [call]; `types-unit-patterns`, `types-list-patterns` |

168+| String interpolation | 8077-8101 | G | Accepts atoms, `@`, leftover decimals, `(list @tD)`; generic atom from a capital → `a generic atom in interpolation needs an aura`; cell → `a cell in interpolation needs a printer` | `types-string-interpolation` |

169+| Union coverage, three copies | 8103-8390 | U | `union-pattern` %full/%none/%unknown; `infer-known-union-whole` 8208, `-context-whole` 8246, `-finite` 8292 (loobean expansion ≤64 rows); `single-structured-pattern`/`infer-single-case-branch` 8351-8390 | generic-pattern, cell-branch, nested-union-guards, empty; `types-union-patterns*`, `types-union-finite*`, `types-single-case-pattern` |

170+| jrec/grec match views | 8392-8475 | R | R17, R18 | qath-fuel, generic-pattern [call] |

171+| Branch routing | 8477-8549 + 8878-8930 | G | Order in `infer-fragment %branch`: dg → one arm (empty-list, empty-union, grec, structured, cell) → ≥3 arms known-union → two arms: speculative `known-union-subject`, unit, non-literal → known-union, loobeans (unify subject with `?`, infer arms, `itype-branch-join`, failure classified 8921-8929) | `types-union-*`, `types-loobean-*`, `doc-grammar-04-step` |

172+| Empty list / empty union | 8555-8608 | U | `empty-list-null-branch` (exact prelude list; element proven empty), `known-empty-union-wing` | empty [call] |

173+| Record change | 8612-8656 | G | `infer-change-edits` on a known faced spine; `standard-unit-template` 8646 | `types-record-change*` |

174+| Missing-tag diagnostics | 8658-8744 | P | `missing-union-tag` (`{label} has no case %x`), `nested-missing-tag` replay | `types-missing-tag-*`, `types-nested-missing-tag` |

175+| `infer-fragment` | 8749-8980 | G | Synthesis by node kind (literals: `%ud` → `%nvar`, `%loobean` → `%flag`, term/null → `%tag` + `ipending`; ctor → `%tag … &`; `%unit`/`%list`/`%qath` require the exact prelude templates; `%wing` instantiates; `%cast` = shape + check-mode + width check + fit + merge faces; `%gate` monomorphic sample; `%call` → `infer-call-with-head`) | every typed golden; cell-branch, deferred, generic-pattern, qath-source [call] |

176+| Dead code | 8988-9000, 9058-9063, 10780-10783 | O | `width-has-projections`, `infer-width-elaboration`, `direct-find-gate`, `resolve-supported-defs` | none |

177+| Direct gate-layout evidence | 9002-9228 | R | R11 | direct-gate-guards [call] |

178+| Call checking | 9230-9294, 9296-9314 | G | Head first; known `%fn`: context args, width, fit (`itype-fit-inner … skip-width` for multi-arg), else `direct-gate-call-fit`; `%unknown` → `call constraint…` (or a `dgo` in defer mode); `%bad` → missing tag → nested tag → `call's sample and argument types do not unify` (`call-error-site` blame); face-propagation guard 9283-9288. Unknown head: unify with `[%fn arg fresh]` | 116 golden lines `call's sample…` in 53 goldens; positional-face-guards |

179+| Contextual call and singleton/unit/tagged-case | 9316-9562 | R/G | `infer-unit-context` 9321, `infer-contextual-call` 9355 (pre-unify product with expected; `element` exception), `explicit-singleton-in-union` 9480, `contextual-*` 9501-9562 (R15), `grec-direct-context` 9527 | nested-union-guards, constructor-fit-guards [call]; `types-nested-union-context`, `types-unit-context` |

180+| `proj` intrinsic | 9396-9475 | O | `explicit-proj-call`, `infer-proj-context` (check mode only), literal fields by name | proj-guards; `types-proj-*` |

181+| Closed-cell branch retry | 9564-9662 | R | R14 | cell-branch [call]; `types-cell-branch-context` |

182+| Check-mode dispatcher | 9664-9783 | G | `infer-call-context-arg`, ~19 ordered steps (9667-9783): defer → unwrap pair/group/body/trace → peel faces → `proj` → grec ctor → jrec `~`/tuple → call → empty list → structured/cell patterns → loobean singleton → known-union branch → unit → closed-cell → flag/union/list branch → list literal → tagged case → cell tuple → synth. Reads the raw `expected` at 9732, 9743, 9756 to keep provenance (A36). Callers do the final fit | generic-construction, qath-fuel [call] |

183+| Positional items, cell binders | 9785-9928 | G | `infer-call-context-items/-args`, `projection-field-target` (peels one slot face), `infer-simple-items`, `infer-cell-branch` | `types-cell-pattern-*`, `types-multi-call` |

184+| Printers | 9930-10032 | P | `show-itype` (A-Z then T26…; six identical variable arms 9936-9951, A35), `show-itype-cases`, `site-type-note` (bare label for vars, nvar, tags, unions, hidden recursion) | every typed golden; 11 suites [call] |

185+

186+#### D. Definition boundary and module resolver (10034-10900)

187+

189+| --- | --- | --- | --- | --- |

190+| Capital and atom-var guards | 10034-10169 | G | `merged-capitals` 10072, `constrained-capitals` 10089 (capital bound to non-var or shared → "explicit capital constraints are not supported"), `atom-var-from-cap`, `atom-var-from-binder`, `unsupported-atom-vars` 10159 (atom vars generalize only from caps or `binders`) | deferred [call]; `types-capital-distinct`, `types-partial-explicit-capital`, `types-partial-aura-*` |

191+| Constraint printing | 10171-10191 | P | `show-atom-constraint`: ` where A is an atom other than ?` / ` is an atom` / ` contains no gates` | all typed goldens with constrained vars |

192+| Names, dependencies | 10193-10214, 10327-10428 | M | `global-value-names`, `unique-value-name`, `dependency-expr` (syntactic, ignores binders, errs closed) | `types-partial-forward`, `types-scope-*` |

193+| Single recursion | 10216-10325 | G | `infer-recursive-gate` 10285: monomorphic `[%fn sam seed-or-fresh]`, body, unify product; `recursive-branch-seed` 10254 (closed base arm of a one-self-call loobean branch); refuses in defer mode; clears `gate-defs` | `types-recursive-*`, `types-local-recursive` |

194+| Mutual recursion groups | 10430-10533 | G | `seed-gate-group`, `infer-gate-group-bodies`, `group-schemes` (short merged-capital text 10495), `infer-gate-group` 10509 (rejects projections, holes, pending tags) | `types-recursion-scc-*`, `types-local-scc*` |

195+| Projection finalization | 10535-10549 | O | `width-finalize` | `types-proj-*` |

196+| Kosaraju SCC | 10552-10643 | M | Work-list DFS; components dependencies-first; duplicates → no components | `types-recursion-scc-order`, `types-value-cycles` |

197+| Resolver fixpoint and finalization | 10645-10778 | M | `add-groups`, `resolve-groups`, `add-supported-result`, `add-supported-defs-core`, `resolve-groups-core`, `dependency-order` (see 1.2(b) step 6, 2.7, 2.8) | all full-check suites; `module-import-*` |

198+| Failure diagnostics, value cycles | 10711-10734, 10785-10900 | P | `module-pending-tag` 10715; `definite-value-cycles` 10885 (report only) | buttons, program-init, program-update; `types-value-cycle*` |

199+

200+#### E. Union analysis and module checker (10902-12600)

201+

203+| --- | --- | --- | --- | --- |

204+| Union projection and relation | 10904-11022, 11275-11286 | U | `project-union-mold` (local refs only, `seen` list), `union-relate` (`?` = {0,1}), `union-pairs` O(n²) in (i, j) order | full-overlap-*, import-overlap; 73 goldens print `cases proven disjoint`, 12 `overlapping cases` |

205+| Source disjointness slice + state screen | 11024-11187 | R | R19 | union-source [call] |

206+| Overlap witness | 11189-11273, 11288-11302 | U | `mold-overlap-witness` 11296: first projected overlap, else (only if some pair unknown) `union-source-overlap` 256 | union-alias-overlap, full-overlap-basic [call] |

207+| Hole detection | 11304-11430 | G | `simple-mold-hole` (unit unit span), syntactic `*-has-hole` | hole-guards [call]; `types-hole-*` |

208+| Report printers and entry wrappers | 11431-11500 | P | `show-partial-mold`, `show-inference-diagnostic`, `show-duplicate-fields`, `duplicate-fields-report`, `golden-types`, `golden-types-imports` | all typed goldens |

209+| Duplicate fields | 11520-11693 | O | Pre-inference syntax pass; nested cell opens a new scope (A30); message `record field `x` is repeated` | `types-record-field-*` |

210+| Scope validity, reserved `proj` | 11694-11773 | M | `import-binding-names` (includes `/%` marks, A25), `reserved-proj-*`, `module-scope-valid` | proj-guards, deferred-resolver [call]; `types-proj-reserved-*` |

211+| Module mold elaboration | 11775-11824 | G | `module-mold-types(-detail)`: each mold from the same base state (ids may repeat across templates); first failure aborts; overlap evidence for a union | full-overlap-basic [call]; `module-cache-incomplete` |

212+| Prelude bootstrap | 11826-12024 | R | R21 | `prelude-*`, `types-prelude-*` |

213+| Partial prelude interface | 11913-11926, 12026-12112 | M | `partial-prelude-molds` drops failing molds silently; `prepare-prelude(-with-internal)` re-parse | 33 suites call `prepare-prelude-with-internal`; `tools/golden:291` |

214+| Completeness and failure naming | 12114-12188 | P | `module-values-complete`, `module-missing-value`, `module-sample-shadow` | `module-missing-value-*` |

215+| Import resolver and cache | 12190-12200, 12219-12228, 12275-12324 | M | Cycle check before cache; legacy entries rebuilt; reuse needs identical inputs | `module-import-*`, `module-cache-*`; full-overlap-graph, request-guards |

216+| Request-graph merge | 12202-12218, 12229-12274 | A | Set union of paths; dedup requests/stores; 256/256 bound (A27) | store [call], request-guards |

217+| API path extraction, derived names, typing | 12326-12615 | A | `+$ paths`/`+$ poke` declarations, `api-derived-clash`, `api-path-analysis(-source)`, `api-path-evidence-source` | api-paths, api-evidence, hole-guards, proj-guards [call]; `module-import-api-*` |

218+

219+#### F. API interfaces (12596-13144)

220+

222+| --- | --- | --- | --- | --- |

223+| Path evidence | 12596-12652 | A | `api-path-evidence-source/-graph` (copies, A31), `api-path-watchability` | api-evidence [call] |

224+| Request components | 12654-12698 | A | `api-request-parameter-types`, `api-request-fold-type`, `api-request-parts` (argument order not fixed) | api-evidence [call], todo-api |

225+| Supporting definitions | 12700-12774 | A | `api-support-analysis-source/-graph` (copies): ordinary `resolve-groups` with a positional state | api-evidence [call] |

226+| Prelude shape certificates | 12776-12845 | A | `compatible-raw-poke`, `request-compatible-ask`: structural `=` on hard-coded itype nouns | store [call], ask-guards, sub-guards |

227+| Request interface constructors | 12847-12956, 13020-13075, 13099-13144 | A | `one-request-interface-source` (dead) and `-graph` (narrow branch, A44), `api-sur-covered`, `api-request-gates` (fuel 256), `multi-request-interface-graph`; hand-built `∀0` schemes | request-guards, todo-api, page-main, todo-full; `types-request-normal`, `module-import-api-request-reason` |

228+| Poke-only interface | 12958-13018, 13077-13097 | A | `api-poke-interface(-result)`, `api-poke-from-checked`, `api-mark-exports` | hole-guards, api-paths, proj-guards [call]; `module-import-api-poke-*` |

229+

230+#### G. Kind recognition and program/store recovery (13146-14648)

231+

233+| --- | --- | --- | --- | --- |

234+| Main-call recognisers | 13146-13240 | M | `program-main-def`, `program-main-wing`, `program-main-args/-parts`, `page-main-parts`, `store-main-parts`: syntax, heads matched by name (four copies of one walk, A48) | program-main, program-watch, store, page-main [call] |

235+| Store declaration, derived-name clash | 13242-13309 | M/P | `store-declaration`, `derived-name-clash` (precedence: definition, import face, another derived name, prelude name) | store; `module-import-store-*`, `module-import-api-*-clash` |

236+| Transparency helpers | 13311-13340 | R | `program-empty-null`, `program-subs-empty`, `program-transparent` | program-main, page-main |

237+| Update, subs recovery | 13342-13606 | R | R1, R2 | via `infer-jibb-file(-detailed)` |

238+| Slot and relation helpers | 13452-13503 | R | `program-inferred-slot`, `program-two-slot-names`, `program-update-relation` | via recovery |

239+| Keyed view-site walker | 13608-13749 | R | R3 | todo-full |

240+| Element message fits | 13751-13853 | R | R7 | todo-full, store, buttons; `types-prelude-ui` |

241+| View recovery | 13855-14155 | R | R3, R4 | todo-full, store |

242+| Initializer | 14157-14312 | R | R5 | program-init |

243+| Derived request/store evidence | 14314-14470 | A | `derived-poke-command-scheme`, `store-derived-schemes`, `program-subs-watch` 14367, `derived-request-member` 14405-14441, `derived-store-request-member` 14443-14470: provenance certificates compared by `=` | store [call], program-watch, page-main |

244+| Program main completion, kind boundary | 14472-14582 | R/M | `program-main-context` (R6), `static-main-specialized` (R9), `page-load-derived`, `page-main-closed` (R10), `program-main-closed` (R6) | program-main, program-watch, store, page-main [call] |

245+| Store kind | 14584-14648 | R | R8 | store |

246+

247+#### H. Driver, report, dg, fresh ids, grec (14650-15838)

248+

250+| --- | --- | --- | --- | --- |

251+| Module driver | 14650-14879 | M | 1.2(b) | 23 suites call `infer-jibb-file`, 12 `infer-jibb-file-detailed` |

252+| Mold analysis entry | 14881-14933 | O | `gate-free-mold-source` | gate-free-source [call] |

253+| Report adapters | 14935-15024 | P | `golden-types-with-modules` (dead, A42), `-with-prelude`, `-with-prelude-and-internal`, `-with-prepared-prelude`, `reader-result-for-checker`, `-with-reader-diagnostics`, `-with-marks`, `-in-context` | tools/golden, tools/ship; 24 suites |

254+| Report core | 15025-15146 | P | 1.2(a) | all 304 typed goldens; deferred-prepared [call] |

255+| dg-* | 15147-15656, 15704-15719 | R/G | R20 | deferred, deferred-context, deferred-prepared, deferred-resolver [call] |

256+| Fresh ids | 15658-15702 | G | `ienv-fresh-id` = one above the max id in env (declines on a pending `%tag`); stands in for a global fresh supply | deferred [call]; program recovery suites |

257+| grec trees | 15721-15835 | R | R18 | generic-*, union-source [call] |

258+

259+## 2. Inference today

260+

261+### 2.1 Unification and type comparison: one unifier, one fit, many special comparators

262+

264+| --- | --- | --- | --- | --- |

265+| 1 | `itype-unify` | 4851-4940 | symmetric | The only structural unifier. Returns `(unit isub)` with no reason. Nominal rules: grec/jrec/recursive identity; union by origin then (argless) raw case equality or args; face names must match. Atom-kind lattice by pairwise cases 4884-4925. Never widens |

266+| 2 | `itype-fit` / `itype-fit-inner` | 5516-5711 | actual → expected | Widening (aura prefix, `@`, `*`, empty source), tag binding, ctor case selection; three-valued; calls unify for vars and as last resort. Gate types are compared by unify (invariant) except `itype-closed-gates-match` |

267+| 3 | `itype-fit-cases`, `itype-fit-ctor-cases` | 5451-5514 | actual → union cases | Each case tried from the original sub; unique `%ok` wins, two → `%unknown` |

268+| 4 | `itype-closed-gates-match` | 5229-5263 | symmetric, closed only | Gate equality modulo one omitted outer sample-slot face; all unifies from empty sub |

269+| 5 | `direct-invariant` | 9097 | both ways | Fit forward and backward plus a face-asymmetry test; 19 call sites, 16 in program/store recovery |

270+| 6 | `direct-function-fit`, `direct-positional-fit` | 9107, 9142 | both ways per slot | Two-slot gate samples matched with binder-face stripping, then replay must leave `sub`/`next` unchanged |

271+| 7 | `program-union-tag-case`, `program-single-case-fit`, `program-single-generic-fit`, `program-keyed-product-fit` | 13751-13853 | element messages | Select the one literal-tagged case, fit head and tail; element covariance only for a single case |

272+| 8 | `contextual-tagged-case` | 9545 | expected union | Unique const-headed case by head noun |

273+| 9 | Structural `=` on itype | 12782, 12805, 14314-14349, 14408-14470, 14599-14648; `infer-closed-cell-branch` 9616; `dg-stable-fit` 15427; `dg-stage-one` 22-field state equality 15458-15479; `program-init-model` replay 14163-14213 | exact | Prelude certificates and "stability" checks substitute for constraint solving |

274+| 10 | `union-relate` | 10994 | pattern overlap | Not a type relation; noun-shape projection used for disjointness |

275+

276+### 2.2 Substitution

277+

278+- Representation: `isub` assoc list (4688), prepended, never compressed; `itype-lookup` 4691 linear.

279+- Head walk: `itype-walk` 4698-4732, six identical arms (`%var|%fvar`, `%avar`, `%rvar`, `%nvar`, `%rnvar`, `%tag`) that stop at a self-binding to `%fvar`/`%rvar`/`%rnvar` (A16). Self-bindings are created at 4887-4889 (nvar~rvar), 4962 (gate-free form) and in `promote-restricted-numbers` (6119-6131). Any other self-binding loops forever (no fuel).

280+- Second walker: `dg-scan` 15150-15178 follows the sub with fuel; recognises only `%rvar`/`%rnvar` self-bindings, so an `%fvar` self-binding burns fuel and declines.

281+- Full application: `itype-normalize` 6012 (95 call sites); leaves `%tag`, `%recursive`, `%jrec` unexpanded.

282+- Whole-sub scans used as provenance screens: `contextual-simple-sub` 9519 (unbounded), `closed-cell-sub-safe` 9592 (512), `grec-direct-context` 9527 (4,096), `union-state-sub-budget` 11147 (256). Each declines if *any* entry binds a structural type, so behaviour depends on inference order.

283+- Mold-level substitutions (not the type substitution): `bind-params` 6873 (param name → arg type, by re-elaboration), `template-apply-sub` 6882 (rename scheme vars to args), `union-overlap-case` 11206 (tvar → arg pattern).

284+- Rollback is implicit: speculative attempts drop their returned state (`known-union-subject` 8541, closed-cell retry, tagged-case retry 9768-9774, direct-gate replay, `infer-recursive-gate` retry, failed locals).

285+

286+### 2.3 Generalization: six sites, four rules

287+

288+| Site | Lines | Rule |

289+| --- | --- | --- |

290+| Top level (`add-supported-result`) | 10682 | Quantify **every** variable of the normalized type. Sound only because each definition starts at `next=0` (10699) and the env holds closed schemes |

291+| Report (`golden-types-in-context-core`) | 15141 | Same, copied |

292+| Locals (`infer-local-defs`) | 7677-7681 | Type vars minus `free-env-vars(env)` (7307: normalizes every non-quantified var of every env scheme) minus `free-cap-vars(enclosing caps)` (7320) |

293+| Groups (`group-schemes`) | 10502-10504 | Same rule with the outer state's caps |

294+| dg (`dg-generalize`) | 15222 (called 15482) | Vars of the normalized type minus "blocked" = env-free (`dg-env` 15187, whole env scan) + obligation vars + tag-reachable vars (`dg-tags` 15209) + captured; bounded scan 32,768; ≤64 edges |

295+| Molds (`infer-mold-template`) | 6970-7000 | Exactly the fresh param ids; a nongeneric mold must be closed |

296+| Hand-built schemes | 12889, 12943, 13068, 14349, `store-derived-schemes` 14351 | `[… ~[0]]` literals |

297+| Recovery publication | via `add-supported-result` in 13444, 13600, 13927, 14107, 14149, 14306 | Then require `vars ~` and no `itype-vars` (closed-only) |

298+

299+Instantiation is one arm, `instantiate-scheme` 6355 (fresh ids from `next`, kind precedence, fresh atom/gate-free ids pushed onto `binders`, which is what lets `types-partial-atom-alias` re-generalize), plus `template-apply(-sub)` for molds and `itype-rename` 6219. Fresh ids for env-mixing code come from `ienv-fresh-id` 15666 (program recovery 13381, 13543, 13894, 14008, 14271; dg roots 15607, 15649).

300+

301+### 2.4 Branch joins: one join, several non-joins

302+

303+- Join rule (Q11, A133 fixed in 38c711c): `itype-branch-join` 5138 (two arms) and `itype-branch-join-list` 5202 (n arms), falling back to `itype-concrete-join` 5125. Callers: 8029 (list), 8073 (unit), 8226 and 8314 (union folds), 8919 (loobean; failures classified into five messages 8921-8929), 15333 (dg boolean).

304+- Checking-mode branches do not join; each arm is fitted to the expected type and the result is `expected`: `infer-union-context` 7763, `infer-known-union-context-whole` 8246, `infer-known-union-finite` with expected 8292, `infer-single-case-branch` 8361, `infer-cell-branch` 9894, `infer-unit-branch`/`infer-list-branch` with expected (A133 note).

305+- Other "joins": open list literal items are fitted to one element var (`infer-open-list-items` 7879, messages `list item widening is not supported` / `list items do not have compatible types`); `infer-closed-cell-branch` 9616 requires the two arm results to be equal and closed; `dg-boolean-branch` 15316 falls back to a fresh result var with two `dgo` edges.

306+

307+### 2.5 Pending constraints (no queue)

308+

310+| --- | --- | --- | --- | --- |

311+| Tag/`~` literal, ctor | `istate.tags` (`ipending`) + `%tag` pseudo-var | 8780, 8781, 8848 | end of each definition: `pending-tags`/`pending-null` 5351-5370 | locals wait (7673); top level dropped (10680); report prints `tag needs context` / `` `~` needs context `` (15131-15134); groups fail (10529); dg fails (15503); full check explains with `module-pending-tag` 10715 |

319+

320+Nothing carries a constraint from one definition to the next except the dg transaction. A later definition (e.g. `main`) can never fix an earlier definition's tag; that is why the program recovery arms exist.

321+

322+### 2.6 Order of solving

323+

324+Synthesis is left-to-right and eager: every fit is decided when it is met, with `%unknown` meaning "give up". Expected types flow only through `infer-call-context-arg` 9664 and its ~19-step ladder; casts and known call samples are the only sources of context.

325+

326+### 2.7 Fixpoints and retries

327+

329+| --- | --- | --- | --- |

339+

340+### 2.8 Definition finalization: five copies

341+

343+| --- | --- | --- | --- | --- | --- |

344+| obligations unchanged |: |: | 7661 | refuses defer 10512 | collects them |

345+| `promote-restricted-numbers` | 10675 | 15117 | 7662 |: |: |

346+| `default-hole-numbers` | 10676 | 15118 | 7663 | holes must not change 10527 | holes unchanged 15477 |

347+| `unresolved-hole` | 10677 drop | 15119 message | 7664 fail |: |: |

349+| `constrained-capitals` | 10678 | 15128 | 7670 | 10496 |: |

350+| `default-decimals` | 10679 | 15130 | **none** | nvar → fail 10499 | nvar → decline 15481 |

351+| `pending-null` |: | 15131 |: |: |: |

352+| pending tags / tag in type | 10680 drop | 15133 | 7673 wait | 10529, 10500 | blocks generalization; 15503 at close |

353+| hidden recursive/generic name |: | 15135-15138 |: | 10500 | `dg-interface-safe` 15573 at publish |

354+| `unsupported-atom-vars` | 10681 drop | 15139 | 7675 wait | 10500 | 15480 |

356+| `width-finalize` | 10683 | 15142 | (left to the enclosing definition) | projections must not change 10525 | projections unchanged 15479 |

357+

358+## 3. Recovery slices

359+

360+"Would fail if removed today": `[call]` suites name the slice's arms and stop compiling if the arms go; `[out]` suites or goldens whose expected output depends on the path (from fixtures; not executed). **No typed golden reaches R1-R10, R18 or the full-check side of R20**, because the report (15025) runs no recovery, no kind check and no grec index, and the only goldens whose case-local modules have a `main` (`module-import-api-import-error`, `module-import-store-derived-clash`, `module-import-store-face-clash`, all importing a cart store) stop at the derived-name clash before inference. Those slices are pinned only by `tests/lib`.

361+

362+### 3.1 Example-fitted slices

363+

365+| --- | --- | --- | --- | --- | --- |

366+| R1 | Update recovery `program-update-context` | 13342-13450 | Todo island `update` (`my-app/ui/todo-list.jibb:16-25`) and basket `update`: bodies end in `[m ~]` and `\|=%acked`, whose tags have no context inside the definition, so `add-supported-result` drops them (10680) | Reads message/model from the written two-slot sample (binder faces stripped), builds `[model (list (cmd message))]` from prelude templates, proves it against program's instantiated slot with `direct-invariant`, checks the body in context, casts, merges faces, publishes only a closed scheme | [out] program-update (all `tests/type-program-update/*`), todo-full, store (basket), page-main (`index.jibb` imports `todo-list`), program-init (needs the update relation) |

367+| R2 | Subs recovery `program-subs-context` | 13505-13606 | Todo `subs ~[[%watch (todos.todo \|=%got)]]`, basket `(state.cart \|=%got)` | Same pattern with `(list (sub message))` and program slot 4 | [out] todo-full, store, page-main, program-init (`initializer-subs`) |

368+| R3 | Keyed view recovery `program-view-context` + view-site walker | 13608-13749, 13938-14155 | Todo `view` with exactly one `each (turn todos.m row-of)` and the mapper `row-of` | Finds the site syntactically, instantiates `each`/`turn`, infers the mapper and the view against hand-built `element message` types, publishes both mapper and view | [out] todo-full (`expected`, `alias`, `ambiguous-mapper`, `open-key`, `non-gate-view`, `wrong-*`), page-main, program-init (`initializer-open-view`) |

369+| R4 | Plain view `program-plain-view-context` | 13855-13936 | Basket `view` (no keyed site, 4bf477e) | Checks the body against `(element message)`; does not check program slot 3 (A48 drift) | [out] store (basket) |

370+| R5 | Initializer `program-init-model`, `program-init-ordinary`, `program-plain-init-context` | 14157-14312 | Todo `init \|= ts=(list item.todo) [ts "" ~]` (`~` needs context), basket `init \|= ~` | Model from the update relation or from a tentative positional fit of main's args (`direct-positional-fit` + replay stability), then context check of the body; ordinary fallback in a separate state | [out] program-init (17 `initializer*` fixtures), todo-full (`cast-init` guards ordering), store, page-main |

371+| R6 | Main completion and program kind check `program-main-context`, `program-main-closed`, `program-subs-watch`, `program-subs-empty` | 13311-13340, 14367-14403, 14472-14482, 14555-14582 | Any direct `(program i u v s)` main | Re-infers `main` after recovery (only agreement check); kind check instantiates program from `*istate`, requires closed invariant main, gate-free init data and model (256 shared budget), and one syntactic watch shape | [call] program-main, program-watch, store (`program-main-closed`); [out] program-main, program-watch, todo-full, store, page-main, program-update/init |

372+| R7 | Element message fits and the list-item hook | 7887-7891, 7909-7913, 9355-9394 (element exception in `infer-contextual-call`), 13751-13853 | Todo union controls (`button "Add" %submit`, `field … \|=%typed`), raw constructors (docs/compiler.md:153) | When an ordinary list-item fit to a prelude `element` union fails, prove the message argument invariantly or pick the single literal case; pre-unify recursive `element` results | [out] todo-full, store, buttons; goldens `types-prelude-ui` (`bad-child` and element lines), probably `doc-grammar-02-buttons` (`labelled`) |

373+| R8 | Store kind and main recovery `store-update-unfaced`, `store-main-closed` | 14584-14648, swap 14844-14849, completeness exception 14817-14819 | Cart store `my-app/ui/stores/cart.jibb` ("The builder erases the action from main", 14597) | Checks prelude `store` value and mold by `=`, checks init/update against local `state`/`poke` invariantly, publishes `[canonical ~]` as `main` even if `main` never inferred | [out] store (cart, basket); compiler.md:143 |

375+| R10 | Page kind `page-load-derived`, `page-main-closed` | 14510-14553 | `index.jibb`, `blog/index.jibb` | One syntactic load shape `case.face reply`, provenance via `derived-request-member` | [call] page-main |

376+| R11 | Direct gate-layout evidence `direct-*`, `istate.gate-defs/head-evidence` | 9002-9228; set at 10701-10702, 15108-15109, recovery arms | `(program init update view subs)` with a faced `update \|= [=msg m=model]` against prelude `update=$-([M X] …)` (`prelude.jibb:534`) | After an ordinary call fit is not `%ok`, re-parse the prelude (A132), match written gate samples slot by slot, both ways, then replay | [call] direct-gate-guards; [out] direct-gate-source (`tests/type-direct-gate`), program-main, program-update, todo-full; golden probably `types-prelude-ui` `++ concrete-program` (line 72 of its source) since the report sets `gate-defs` |

378+| R13 | Positional face rule | 5313-5349, 9285 | `like` result mapping (640a442) | Ignore one sample-slot face per written argument | [call] positional-face-guards, direct-gate-guards; goldens `types-positional-faces`, `types-prelude-like` |

379+| R14 | Closed-cell branch retry | 9564-9662, dispatch 9743 | Todo `update` inner `?- (gth …)` returning `[m(...) ~]` (22f3788) | Re-check a two-loobean branch against a cell target from the original state; results must be equal, closed, tag-free; replay | [call] cell-branch; golden `types-cell-branch-context`; [out] todo-full |

380+| R15 | Contextual tagged case | 9477-9562 (`contextual-tagged-case` 9545), dispatch 9753-9780 | Todo `subs` body `~[[%watch (todos.todo \|=%got)]]` (72acdb3) | Try ordinary inference; else select the union case by literal head and check the payload in context | [call] nested-union-guards; goldens `types-nested-union-context`, `types-nested-shallow-preserve`; [out] todo-full |

382+| R17 | `%jrec` / qath | 4680, 6925-6952, 8392-8420, 8757-8763, 8807-8821, 9699-9714 | Internal prelude `qath` (`internal.jibb:15-17`, 0ea700d); theme `font=` qath literal; `image`/`link` | Recognise `~ / [h=@aura t=self]`, unfold one layer per fuel (256 per definition) for matching, construction and static path literals | [call] qath-fuel; qath-source, theme; goldens `types-qath-*`, `types-arithmetic-proj-qath`, `types-prelude-ui` (`image-scheme`, `link-scheme` print `qath`) |

383+| R18 | `%grec` generic tree | 4681, 6954-6968, 8422-8475, 9527-9539, 9684-9698, 15721-15835, 4801 | Test-only node tree (`tests/type-generic-recursion`, c96597d) | Fixed two-case shape proof; one-layer view for patterns/construction; index only for import-free prelude-backed modules (14762-14772) | [call] generic-recursion, generic-construction, generic-pattern, union-source; golden `types-generic-recursive-union` only as an unsupported control |

384+| R19 | Union source disjointness, state screen, source overlap witness | 11024-11187, 11189-11273 | One-hop local generic alias with a literal head (b93a94b) | Bounded syntactic proof of distinct heads / positive overlap when projection is unknown | [call] union-source, union-alias-overlap, full-overlap-basic; goldens `types-union-source-alias`, `types-prelude-succ` |

385+| R20 | dg-* deferred transaction | 15147-15656, 15704-15719; hooks 8854, 8879, 8951, 9261-9265, 9281, 9667-9669, 10288, 10512 | Import-free modules without a prelude (full check, 14807-14816); prepared-prelude reports whose fixture is the todo initializer `[xs "" ~]` closed by a later cast (`tests/type-deferred-prepared/good.txt`) | Re-infer definitions with obligation edges for literal branch arms, tuple items and ctor args, retry to a fixpoint, replay edges twice | [call] deferred, deferred-context, deferred-prepared, deferred-resolver; goldens `types-constructor-context`, `types-union-singleton` reach the screens but the transaction declines (report unchanged) |

387+| R22 | API narrow branch `one-request-interface-graph` | 12904-12956, 14711-14721 | Blog API (one mark import, non-union paths) | Hand-built one-request interface; redundant with multi-request (A44); `one-request-interface-source` 12850 is dead | [out] page-main (blog API), request-guards |

388+

389+### 3.2 Ad hoc slices of general inference (not fitted to one example, but replaced by the core)

390+

391+| Slice | Lines | Replaced by |

392+| --- | --- | --- |

393+| Two-arm unit/list branches | 7923-8075 | usefulness over `~`/cell constructors |

394+| Three coverage loops + 64-row loobean expansion | 8103-8350 | usefulness |

395+| One-arm structured / cell-binder / empty-list / empty-union | 8351-8390, 8555-8608, 9852-9928 | one-row usefulness, empty types have no constructors |

396+| Speculative subject screens | 8477-8549 | infer subject once |

397+| `recursive-branch-seed`, blanket `infer-recursive-gate` retry | 10216-10325, 10705, 10729, 7646 | SCC let-rec with levels |

398+| `known-union-subject` double inference | 8541 |: |

399+| Loobean join failure classification | 8920-8929 | one join + deferred widen |

400+| Import-invalid replay | 7002-7097 | elaboration returning reasons |

401+| `module-pending-tag`, `module-missing-value`, `module-sample-shadow` | 10715, 12132, 12171 | per-definition errors from the core |

402+| Order-independence rules for locals | 7521-7584, 7633-7637 | SCC order + deferral |

403+

404+## 4. What the core replaces, what it must keep, and the hazards

405+

406+### 4.1 Replaced

407+

408+| Core piece | Replaces |

409+| --- | --- |

410+| Union-find store over a map, path compression, one global fresh counter | `isub`/`ibinding` 4687-4688, `itype-lookup` 4691, `itype-walk` 4698-4732, `dg-scan` 15150, `ienv-fresh-id` 15666-15702, per-definition `next=0` (10699, 10752, 14759, 15107) |

411+| Kind on the root (any ⊐ gate-free ⊐ atom ⊐ atom-other-than-? / defaultable number) | `%fvar %avar %rvar %nvar %rnvar` (4666-4670), the pairwise lattice 4884-4925, self-binding refinement (4887-4889, 4962, 6119-6131), `itype-bind-gate-free` 4998 and its 256 budget, `itype-var-is-*` 6267-6343, `binders` bookkeeping for `unsupported-atom-vars` 10159 |

412+| Levels | `free-env-vars` 7307, `free-cap-vars` 7320, `shared-types`/`shared-moved`/`closed-local` 7534-7584, `dg-env` 15187, `dg-generalize` 15222, all-var quantification 10682/15141 |

413+| Deferred-constraint queue (woken on binding, reported at module end) | `%tag` + `ipending` + `pending-tags`/`pending-null` 5351-5370 + drop at 10680 + `module-pending-tag` 10715; holes 6133-6181 (as level-exit obligations); decimal defaulting 6062 and promotion 6119 (as level-exit defaulting); fit `%unknown` (5527-5711) as "enqueue"; `itype-fit-ctor-cases` 5474; field access 7720, change 8622, interpolation 8081, `proj` 9461, cell/cons literals 7834; the whole dg-* transaction 15147-15719 and its hooks |

414+| Bidirectional check mode (synthesize then unify/subsume with expected; push expected into arms and items) | most of `infer-call-context-arg` 9664-9783: contextual branches 7749-7921, unit context 9321, singleton 9480, tagged case 9477-9562, closed-cell retry 9564-9662, `infer-contextual-call` pre-unify 9355 |

415+| Maranget usefulness over a constructor signature taken from the subject type | 7923-8075, 8103-8390, 8395, 8425-8475, 8477-8608, 9852-9928, `dg-boolean-patterns` 15292; branch routing 8878-8930 |

416+| One nominal recursive mold `(module, name, args)` unfolded on demand | `%recursive`/`%jrec`/`%grec` 4679-4681, `simple-source-recursive` 6925, `simple-source-generic-recursive` 6954, `jrec-match-view`, `qath-static-fuel`, grec 15721-15835, `jrec-fuel` |

417+| SCC driver, one pass, scheme-or-error per definition | `resolve-groups-core` fixpoint 10736-10756, `add-supported-defs-core` retries, `add-groups`, locals' pass loop 7611-7681, `try-local-group` 7686, `dg-stage` 15487 |

418+| `main` as an ordinary application, sample-slot faces as labels | program chain 13342-14482, `direct-*` 9002-9228, `itype-closed-gates-match` 5229-5263, positional face rules 5313-5349, element fits 13751-13853 and hooks 7887-7891/7909-7913, `static-main-specialized` 14487, store component recovery 14599-14648 |

419+| One pipeline (Q6) | report re-inference 15079-15146; its separate finalization 15117-15143 |

420+| Five finalization copies (2.8) | one generalization step at level exit |

421+

422+### 4.2 Kept (retargeted to the new representation, behaviour preserved)

423+

424+- **Printers**: `show-itype` 9930-9995 (A-Z then T26…, `(label args)`, space-separated unnamed unions, parenthesised in context), `site-type-note` 10024, `show-atom-constraint` 10171, `canonical-itype` 6345 with `itype-vars` order 6183 (fn sample before product, head before tail, union args before cases) and kind precedence rvar > avar > fvar > var, `show-partial-mold` 11431 (until Q6 changes the report), `show-inference-diagnostic` 11458, `show-duplicate-fields` 11470, `prelude-label*` 11870-11911, `itype-in-import` labels 6806 (display separate from identity).

425+- **Error wording and site notes** (golden-pinned; full list in 4.3).

426+- **API path analysis and derived interfaces**: 12326-13144 and 14314-14470, `derived-name-clash` 13289, request-graph 12202-12274, watchability; they synthesize schemes into interfaces before consumers are checked. The hand-built schemes should become instantiations of declared templates.

427+- **Hoon importer bridge**: 6397-6728 plus `jibb-dev/lib/jibb-import.hoon`; the import-invalid wording (`invalid imported mold` + importer message).

428+- **Overlap witness and disjointness**: `upat`/`union-relate`/`union-pairs` 10904-11022/11275, `mold-overlap-witness` 11296, `module-mold-overlap` 11786, `jfile-overlap` 11513 evidence. `union-relate` is also the importer's disjointness relation (6477, 6665), so either keep `upat` as the importer projection or give itype a pattern view.

429+- **Pre-inference passes**: duplicate fields 11520-11693, scope and reserved `proj` 11694-11773, dependency extraction 10327-10428, Kosaraju 10552-10643, value-cycle diagnosis 10785-10900 (wording), module graph and cache 12190-12324.

430+- **Elaboration**: `infer-simple-shape` 7099 / `infer-mold-template` 6970 / `label-direct-union` 6843 (mold → type, origin assignment), `proj` planning 5835-5923, 9396-9475, `width-finalize` 10535 (artifacts), `gate-free-type` 5925-5992 as a post-solve check with witness path.

431+- **Kind boundary** as post-solve matching of `main`'s closed type against prelude molds; watch/load provenance checks; store-derived exports.

432+

433+### 4.3 Hazards

434+

435+1. **Golden output moves.** All 304 `types.txt` come from the report path. Pinned fail-closed lines: 80 `tag needs context in partial inference`, 24 `` `~` needs context ``, 32 `call constraint is not supported…`, 37 `cast constraint…`, 5 `record width constraint…`, 5 `proj constraint…`, 6 `type hole needs unsupported inference`, 6 `unresolved aura-variable inference`, 4 `call result face propagation`, 31 `local definitions need unsupported inference`, 47 `name is not available to partial inference`; 127 goldens contain some unsupported text. Mold lines: 171 `+$ X: not checked`, 171 `cases proven disjoint; mold not checked`, 6 `case disjointness unresolved`, 22 `overlapping cases`. A stronger core changes these; each stage must either keep the exact `%unknown` sites or budget a deliberate golden update (Q6 predicts ~283 outputs change once).

436+2. **Definite wording to keep byte-exact**: `call's sample and argument types do not unify` + `called gate`/`argument` (116 golden lines, 53 goldens); `branch arms have incompatible types` + `first arm`/`second arm`; `cast mold and expression type do not unify` + `cast mold`/`expression`; `{label} has no case `%x`` + `expected union`/`tag` (8706); `record has no field `x`` + `unknown field`; `change field and replacement do not unify`; `a change takes at least one field` + `empty change`; `missing union case X` (no sites, first remaining case); `branch arm is covered by earlier arms` + `covered arm`; `branch does not cover both loobeans`; `nothing fixes the union of %x` (5363; `tests/type-buttons/error.txt`, program-init, program-update; not in any golden); `non-gate value depends on itself through a cycle` + `value in cycle`/`dependency in cycle`; the long capitals message (7669, 15126) vs the short one (10495); `type hole needs a determined type` + `unresolved type hole`; `a generic atom in interpolation needs an aura`, `a cell in interpolation needs a printer`; `record field `x` is repeated` + `first field`/`repeated field`; derived-name clash texts; module/API texts in 1.2(b).

437+3. **Sites decide definiteness.** `definite-diag` 7521 treats site-less diags as retryable; several definite-sounding errors have no sites (`missing union case`, `pattern binder shadows a name`, `unit present pattern is unreachable`, `sample shadows a name`). Adding sites changes local-definition outcomes (they stop ending as `local definitions need unsupported inference`).

438+4. **Message precedence is order-dependent**: report checks 15117-15143 in fixed order; loobean join classification 8921-8929; missing tag → nested tag → generic after every `%bad`; union coverage checks `%unknown` before coverage and `covered` before `not supported` (A15); locals report the earliest failing local (`rear sure`, 7636); finite expansion prints `%.n` rows before `%.y`; the full check reports pending tag, then shadowing sample, then missing value (14821-14832); API precedence poke-only → clash → scope → import error → constructor reason.

439+5. **Unification semantics goldens rely on**: unequal atoms never unify; argful named unions unify by args only, argless by raw case equality (A11); `%var` binds faces, unions, tags; a `%tag` vs non-var fails in unify; faces must match by name; fit is invariant for gates; `*` accepts gates (A23, pending Q18) and binds bare tags (A22); term literal fits `@tas`/`@ta` with no aura check (A20); `?` vs `@f` is unknown; zero vs list unknown; only `@` allocates in fit.

440+6. **Self-binding invariant**: any self-binding other than `%fvar`/`%rvar`/`%rnvar` loops `itype-walk`. A staged migration that keeps `isub` alongside a union-find store must keep this invariant or convert at the boundary.

441+7. **Ids**: ids restart at 0 per top-level definition, `itype-rename` is single-pass, so scheme ids may coincide with fresh ids by design (6008-6010); `module-mold-types` reuses one base state per mold, so template ids repeat. A union-find store must never assume scheme ids are globally unique; instantiate always.

442+8. **Rollback**: speculative attempts drop state; tests assert that failed retries return the original result and replays leave `sub`/`next` byte-identical (cell-branch, direct-gate-guards, deferred). A mutable store needs a trail/snapshot or a persistent map.

443+9. **Provenance screens**: grec, tagged-case and closed-cell screens decline if any substitution entry is structural; `infer-call-context-arg` reads raw `expected` at 9732, 9743, 9756. Behaviour of these slices depends on inference order; a new store changes when they fire.

444+10. **Budgets pinned by tests**: `jrec-fuel` 256 (qath-fuel uses 0/1/2); grec arms 128; closed-cell screens 512 (cell-branch tests the limits); `union-source-distinct-tags` 18 ok / 17 declines; `union-source-overlap` 20/19; `module-mold-params-valid` 256/257; `union-source-state-safe` 256/257 caps; `dg-direct-source` 63/64 wrappers, `dg-source-candidate` 64/65 defs; `ienv-fresh-id` results `2.000.002`, `1`, `10`; `dg-generalize` results `~[43]`, `~[81]`, `~[722]`, `~[713]`. Other literals: empty proof 256 in fit, live cases 4,096, inhabitation 256, finite 64, width 1,024/4,096, gate-free 256, obligations 62/63/64, `module-pending-tag` 64, request graph 256/256, `api-request-gates` 256.

445+11. **`istate` shape**: 27 positional fields at 10 literal sites, 5 bunts, `dg-stage-one` compares 22 fields (15458-15479), 13 suites use `istate:jibb`, all by bunting `*istate:jibb` and setting fields by name. Adding union-find, level or queue fields touches the 10 literal sites; a constructor arm (A28/A125) should come first.

446+12. **Interfaces are hashed nouns**: `iwidth-definition` carries the raw `sub` (10687) into `ifile.elaborations`; cache reuse compares inputs by equality (12219, 12275). Changing the representation changes interface nouns, cache keys and anything comparing `ifile`s (`request-graph-merge` dedup, `derived-request-member` evidence equality).

447+13. **Structural `=` certificates**: `compatible-raw-poke`, `request-compatible-ask`, `derived-poke-command-scheme` (five `cmd` cases in order `poke go wait now who`, label `raw-poke`), `store-main-closed`, `derived-request-member` (`∀m. $-($-(full m) (ask m))`), `derived-store-request-member`. A new var representation must keep these equal or replace them with template comparisons; any edit to `prelude.jibb`/`internal.jibb` silently disables them.

448+14. **Printer stability**: variable letters depend on `itype-vars` order and kind precedence; `site-type-note` suppression rules; nvar/rnvar print as atom constraints; `(unit qath)` and other public labels rely on `prelude-label-nested` (A134; jibb-theme).

449+15. **Prelude identity checks**: exact list scheme compared at 7844, 7996, 8572, 8800, 14767 (and built at 11920, 11979, 12013, 12064); unit via `standard-unit-template` 8646; `element` by origin `[at.prelude %element]`; qath must be `%jrec` at `/lib/jibb/internal/jibb` (8816). The core must expose the same identities or these paths all fail closed.

450+16. **Two pipelines**: changing the resolver or finalization in one pipeline without the other moves goldens or suites (A46, A122). The golden report also runs the full check on imported case-local modules (14989), so module-check goldens see both.

451+17. **Recovery adapters**: until R1-R10 are retired, they call `itype-fit` (22×), `itype-merge-faces` (12×), `instantiate-scheme` (12×), `direct-invariant` (16×), `template-apply` (15×), `infer-sample`, `reserve-def-caps`, `record-fields-named`, `itype-in-import`, `add-supported-result` (6×), `infer-call-context-arg` (6×), `ienv-fresh-id`; and they mix substitutions on purpose (body inferred from the sample's own sub with the gate-fit's `next`, 13418-13421; mapper from `initial`). A core that threads one store changes their edge behaviour.

452+18. **Negative fixtures that encode recovery limits, not spec errors**: `tests/type-todo-full/ambiguous-mapper.txt`, `alias.txt`, probably `open-key.txt`; generic strings `module definitions need unsupported inference: /p: ++ name` and `module kind needs unsupported inference: /p` asserted by program-update/init/main. An ordinary-application core will accept or reject these differently; decide per fixture.

453+19. **`program-single-generic-fit` is in ordinary inference** (7890, 7912) for any prelude `element` target, so removing the program recovery does not remove it; `types-prelude-ui` and `doc-grammar-02-buttons` depend on the path that reaches it.

454+20. **Performance**: assoc-list lookups and 95 `itype-normalize` calls; `unique-type-vars` O(n²); `free-env-vars`/`dg-env` rescans per generalization; `itype-fit-cases` re-fits every case; subjects inferred twice; whole-to-finite re-inference; prelude re-parsed per `direct-prelude-evidence` call (A132); report re-infers every definition; compiler.md:67-69 reports 38-72 s CPU for 2,000 gates. Brief l.141 asks for seconds.

455+21. **Deviations from the spec the core should not copy unknowingly**: gates fit `*` (Q18 pending), tag fits `@tas`/`@ta` without aura check (Q16/Q17), faces handled by asymmetric guards instead of "unnamed acquires the face" (S1 pending), argless union identity by raw cases (A11), only list/unit in inhabitation/gate-free (A13), arms matching no case reported as unsupported (Q22), decimal defaulting skipped in locals and gate types (compiler.md:59 notes defaulting in gate types is incomplete).

456+22. **Dead code not to port**: `itype-has-fixed-atom` 5098, `width-has-projections` 8988, `infer-width-elaboration` 8995 and `iwidth-elaboration` 8994, `direct-find-gate` 9058, `resolve-supported-defs` 10780, `golden-types-with-modules` 14939, `one-request-interface-source` 12850, unreachable `!!` at 14258 and 14525, the last `[%& …]` of `dg-boolean-branch` (15351), the always-`~` `captured` argument of `dg-generalize`, misplaced headers (5014-5018, 6008-6010, 6320-6321, 6397-6403, 5835-5837), the stale comment at 11502-11505.

457+

458+### 4.4 Seams a staged plan can use (observations, not a plan)

459+

460+- `golden-types-in-context-core` re-infers each definition independently (15107-15114), so a new core can be swapped in per definition behind the same printer and finalization, leaving `resolve-groups` in place, before the full check changes.

461+- The full check's recovery chain only runs for components still missing after `resolve-groups-core` (`?^ (ienv-lookup …) ~` at the top of each arm). A core that resolves a component ordinarily turns its recovery arm into a no-op without deleting it; the `cast-init` regression already guards that ordering.

462+- `itype-fit`'s three-valued API can be preserved over a new store as long as `%unknown` stays the answer for "would need a queued constraint" in the old callers; R1-R10 are its heaviest users.

463+- The dg-* transaction is reachable from the full check only without a prelude (14809) and from the report only on eligible sources; its tests are self-contained (four suites), so it can be retired as a unit once the queue exists.

464+

465+## 5. Entry points that must stay stable during a staged migration

466+

467+### 5.1 Tools (signatures are checked)

468+

469+| Arm | Line | Caller |

470+| --- | --- | --- |

471+| `golden` | (%api chapter) | `tools/golden` (parser outputs), module trees |

472+| `golden-types` `[file=path src=@t] -> @t` | 11486 | `tools/golden:251-253` (signature enforced at `tools/golden:407-408`), `tools/ship:1234` |

473+| `golden-types-imports` | 11497 | `tools/golden:252`, `tools/ship:1257` |

474+| `golden-types-with-marks` | 15016 | `tools/golden:248`, `tools/ship:1288` |

475+| `golden-types-with-prelude-and-internal` | 14969 | `tools/golden:259`, `tools/ship:1345` |

476+| `golden-types-with-prepared-prelude` | 14975 | `tools/golden:260`, `tools/ship:1346` |

477+| `prepare-prelude-with-internal` | 12103 | `tools/golden:291` (under `mule`), `tools/ship:1222` |

478+

479+### 5.2 Module-check API (suites, and itself recursively)

480+

481+`infer-jibb-file` 14650 (23 suites; also builds the internal prelude, 11956), `infer-jibb-file-detailed` 14658 (12 suites; `resolve-jibb-imports-detailed` 12316/12320), `resolve-jibb-imports` 12286 (deferred-resolver, generic-recursion), `prepare-prelude` 12092 (api-evidence, poke-bridge), `prepare-prelude-with-internal` (33 suites), `golden-types-with-prelude` 14955 (bridge, list-alias-guards, module-scope), `golden-types-with-reader-diagnostics` 15007 (bridge, import-*), `golden-types-in-context` 15021 (empty, union-alias-overlap, union-source), `golden-types-in-context-core` 15025 (deferred-prepared), `gate-free-mold-source` 14887, the API evidence arms (`api-path-analysis(-source)`, `api-path-evidence-source`, `api-path-parameters`, `api-path-watchability`, `api-request-parts`, `api-support-analysis-source`, `api-poke-interface`), `find-jibb-cache`, `request-graph-bounded`, `request-graph-reusable`, `module-scope-valid`, `module-mold-params-valid`, `program-main-def`, `program-main-parts`, `page-main-parts`, `parse`, `show-error`, `show-itype` (11 suites), `canonical-itype` (buttons, deferred-resolver, doc-examples), `record-fields-named` (program-init/main/update/watch), `itype-in-import` (5 suites), `itype-vars` (page-main, program-watch, store, theme), `ienv-lookup` (17 suites), `find-jibb-mold` (13 suites), `find-jibb-interface`, `find-simple-mold`, `collect-simple-molds`, `find-imported-mold`, `find-imported-mark`, `import-to-itype`, `template-apply`, `identity-union-parameters`, `prelude-union-alias`, `compatible-raw-poke`, `request-compatible-ask`, `derived-poke-command-scheme`.

482+

483+### 5.3 Substrate arms called by suites (keep or migrate the suites in the same stage)

484+

485+`itype-fit` (8 suites: arithmetic-guards, closed-gate-guards, constructor-fit-guards, deferred, empty, generic-construction, generic-recursion, qath-fuel), `itype-unify` (arithmetic-guards, gate-free-guards, generic-recursion), `itype-unify-test` (typecheck), `itype-walk` (arithmetic-guards, deferred), `itype-lookup` (hole-guards), `itype-normalize` (deferred, generic-construction), `itype-empty-proof`/`itype-inhabited-proof`/`itype-live-cases`/`empty-list-null-branch` (empty), `itype-gate-free-form`/`itype-collection-keys`/`itype-var-is-gate-free`/`instantiate-scheme`/`template-apply-sub` (gate-free-guards), `gate-free-type` (empty, gate-free-guards, generic-recursion), `itype-has-face` (deferred, empty), `itype-face-asym`/`itype-output-may-be-cell`/`pending-tags`/`unsupported-atom-vars` (deferred), `itype-positional-face-asym` (positional-face-guards), `itype-positional-slot-face-asym` (direct-gate-guards), `itype-fit-ctor-cases` (constructor-fit-guards), `itype-has-gate`/`default-decimals` (generic-recursion), `default-hole-numbers`/`simple-mold-hole` (hole-guards), `infer-fragment` (cell-branch, deferred, generic-pattern, qath-source), `infer-call-context-arg` (generic-construction, qath-fuel), `infer-simple-shape` (union-source).

486+

487+### 5.4 Recovery and dg arms called by suites (retire with their suites)

488+

489+direct-gate-guards: `direct-checked-gates`, `direct-gate-call-fit`, `direct-gate-sample`, `direct-positional-fit`, `direct-prelude-evidence`. cell-branch: `closed-cell-branch-eligible`, `closed-cell-retry-safe`, `closed-cell-sub-safe`, `infer-closed-cell-branch`. nested-union-guards: `contextual-direct-union`, `contextual-simple-sub`, `contextual-tagged-case`. constructor-fit-guards: `explicit-singleton-in-union`. qath-fuel: `jrec-match-view`, `qath-static-fuel`. generic-*: `simple-source-generic-recursive`, `grec-direct-context`, `grec-match-view`, `grec-patterns-eligible`, `grec-single-wing-subject`, `grec-unfold-view`. union-source: `grec-collect-molds`, `union-source-distinct-tags`, `union-source-state-safe`. union-alias-overlap and full-overlap-basic: `union-source-overlap`. program-main/-watch/store: `program-main-closed`; page-main: `page-main-closed`. deferred*: `dg-close-env`, `dg-direct-source`, `dg-generalize`, `dg-obligations`, `dg-replay-edges`, `dg-root-detail`, `dg-root-prepared`, `dg-root-source`, `dg-scan`, `dg-source-candidate`, `dg-stable-call-fit`, `dg-stage`, `ienv-fresh-id`.

490+

491+### 5.5 Types constructed by suites

492+

493+`itype` (32 suites), `iprelude` (32), `ifile` (25), `ischeme` (24), `istate` (13: cell-branch, deferred-context, deferred, direct-gate-guards, empty, gate-free-guards, generic-construction, generic-pattern, generic-recursion, hole-guards, qath-fuel, qath-source, union-source), `ienv` (11), `isub` (10), `iresult` (6), `ifit` (6), `upair` (3), `irequest-graph`/`irequest-evidence` (3), `dgo`/`ipending`/`igate-free`/`iwprojection`/`iwidth-definition` (2), `istore-request-evidence`, `igate-prelude-evidence`, `igf-form`, `igf-segment`, `ibinding`, `dgscan`, `dgparse`, `dgcommit`, `grec-collected` (1 each). Q37 decided tests keep calling internal arms (A126) until the core lands; a facade or same-stage suite edits are required for every renamed arm or reshaped type.

494+

495+## 6. Spec rules the core must meet, and open rulings

496+

497+Repository spec wins over the design doc (review Q42); several type-system rows in `decisions.md` are still marked unsynced.

498+

499+### 6.1 Rules

500+

502+| --- | --- | --- | --- | --- |

503+| Inference basis | HM with aura variables; principal types; no general subtyping except listed one-way widenings and explicit `proj` | grammar.md l.121; decisions.md l.35; implementation-plan.md l.15; milestone-2.md l.39, l.62, l.141 | Union-find + levels; widening as directional constraints outside unify | assoc list, env scans, fit mixes widening and unification |

504+| Atoms and auras | `@` any atom per occurrence; specific auras distinct; aura fits `@` and Hoon-family ancestor; reverse needs a check | grammar.md l.124; decisions.md l.59, l.35, Q15 l.134, Q19 l.142 | `fit(actual, expected)` constraint that waits while actual is unbound; unify never widens | `aura-prefix` 5052, fit 5663-5680, `itype-concrete-join` 5125 |

506+| Empty and crash | `!!` expression has any type; mold `!!` empty; empty-position cells empty, disjoint from all | grammar.md l.62, l.127, l.132; decisions.md l.48, Q17 l.138 | crash = fresh var; usefulness drops uninhabited constructors | `%empty`, 4744, 5521-5525 |

507+| Loobeans | `?` = {0,1}; disjoint from cells, overlaps 0 and 1; arithmetic rejects, comparison accepts | grammar.md l.124, l.127, l.59; decisions.md l.52, l.60, Q16, Q28 | finite constructor set; "atom other than ?" kind | `?` vs `@f` unresolved (5546-5548) |

509+| Literals | decimal `@ud` or any aura by context; prefixed numbers, ships, dates, knots, cords; `` `x ``, `~[…]`, `a+b`, paths, qath read as Hoon | grammar.md l.19-39; decisions.md l.14, l.58 | literal → type or var + literal constraint; prelude unit/list/path/qath templates available | 8770-8821 |

510+| Faces | faces are part of types; unnamed position unifies with faced and takes its face; different faces don't unify; duplicate fields error (also imported); `[a]` is `a`; `[]` error; theme `dark=[tones=…]` must check | grammar.md l.126, l.33; decisions.md l.15, l.42, l.35, Q5, Q8, Q21, Q27 | label slot that may be unknown, bound by unification | `%face` wrapper + asymmetry guards 5212-5349 |

511+| `proj` | explicit, type-directed; expected type selects fields; evaluated once; never inserted implicitly; reserved name | grammar.md l.126; decisions.md l.43; core-language.md l.85; Q32 | deferred `proj(S) : T` with recorded axes | 5835-5923, 9461, 10535, 11706-11760 |

512+| Capitals | generalized per `++`; local `++` shares an enclosing capital it also uses; cannot force two capitals equal; cannot become more specific | grammar.md l.129; decisions.md l.50, Q4, Q23; milestone-2.md l.66 | rigid (skolem) vars scoped before inference; violations name both sites | `merged-capitals` 10072; forcing concrete is "unsupported" (10089) |

513+| Atom/arith constraints | atom constraint and "atom other than ?" retained through generalization and instantiation; printed as where-clauses separated by commas | grammar.md l.124, l.137; decisions.md l.31, l.60, Q28, Q29 | kind lattice on roots | six var kinds, A16 |

514+| Gate-free | `eq` args and map/set keys contain no gates; inferred and generalized; printed `where A contains no gates` | grammar.md l.137; decisions.md l.33, l.106; core-language.md l.39 | gate-free kind, structural propagation, binding a gate fails with sites | `%fvar`, 4998, 5951 |

515+| Holes | `_` wherever a mold may; resolves to a concrete type or written capital; unconstrained is an error; a definition determines its own holes | grammar.md l.123, l.130; decisions.md l.51, Q30, Q31 | hole var with span checked at its level exit | 6133-6181 |

516+| Order, recursion, value cycles | any order; gates self/mutually recursive; non-gate value depending on itself is an error; infer in dependency order, groups together | grammar.md l.56, l.101; decisions.md l.23; core-language.md l.145; milestone-2.md l.66, l.141 | one SCC pass; value cycles reported from the graph | fixpoint fallback 10749-10756; cycle proof needs a cast |

520+| Tag resolution | tag/`~` = fresh var + pending constraint; non-union = one-case union; checked by shape and shared tag positions, field positions against fields; `@tas`/`@ta`/`@`/`*` make it that constant; no match → `msg has no case %submitt` | grammar.md l.141-143; decisions.md l.29; milestone-2.md l.77 | the deferred queue, woken on binding | `%tag` 4676, 5451, 8693, 8711 |

521+| Non-generalization, module end | tag-constrained vars (and what they mention) do not generalize; an island's `main` fixes its messages; open at module end → error asking for `^-`, never guess | grammar.md l.145-146, l.150-158; milestone-2.md l.79 | keep such vars at module level; module-end pass reports `nothing fixes the union of %add` | dropped at 10680; recovery R1-R5; `module-pending-tag` |

522+| `\|=%tag` | case constructor typed by the expected gate; any case whose head noun equals the tag; no such case is an error | grammar.md l.48, l.141, l.144; decisions.md l.47, Q34; milestone-2.md l.78, l.124 | deferred ctor constraint on the product's root | 5474 |

523+| Numbers by context | wait for context; default `@ud` at the `++` only if unfixed and not generic over it | grammar.md l.162-167; decisions.md l.35; milestone-2.md l.81 | defaultable kind, defaulted at level exit unless linked to a quantified/rigid var | 6062, 6119; incomplete in gate types (compiler.md:59) |

530+| Disjointness | cases must differ as nouns (for all generic args); `*`, vars and `(list A)` overlap; `!!` disjoint; imported `$% $? $^` too; unverifiable imports fail closed; error suggests leaving `[` open | grammar.md l.127, l.94; decisions.md l.29, l.41, Q16, Q17, Q22; overview.md l.66-68; milestone-2.md l.86, l.125; jibb.hoon 4620 | noun-shape signature shared with usefulness; overlap witness naming both sites | 10909-11302 |

534+| `?-` | exhaustive, ordered; missing case error naming it; covered arm error; nested patterns allowed; last position binds the rest | grammar.md l.59, l.184-219, l.276-277; decisions.md l.32, l.57; milestone-2.md l.89-92, l.142 | Maranget usefulness with witnesses; one matrix also for milestone-3 lowering | three loops + slices; nested mostly unsupported |

537+| Interpolation | atoms print by aura (`@` as `@ud`); text auras and tapes splice; other cells error; generic aura error here and in qath segments; `~&` printer from type | grammar.md l.49, l.170-171; decisions.md l.58; core-language.md l.79, l.95; milestone-2.md l.82 | deferred printable constraint decided at level exit; record the printer | 8081 rejects late-known types |

539+| Imports, module values | `/-`, `/%` (no face), `/=` under a face; records read with `.`; module as a value is a cell of definitions in name order; APIs re-export `/%` types; import cycles are errors | grammar.md l.86-94, l.104, l.47; core-language.md l.146; overview.md l.305; milestone-2.md l.98-99 | interface noun; faces as record access with per-use instantiation | `ifile`, 12293, cycle 12304 |

540+| Hoon import table | `$% $? $^` unions if disjoint; `$@`; `$~` dropped; containers by name; tags `%0 %& %\|`; recursive by name; errors where used for duplicates, cores, gates, vases, signed/float auras | overview.md l.60-77; grammar.md l.94; decisions.md l.41, Q21, Q22; milestone-2.md l.102-104, l.134-140, l.153 | imported molds become the same core types; unsupported molds poisoned at use | 6527-6728; whitelist triplicated (A14) |

541+| Module kinds | main's type decides: `(element !!)` page, `(page R D)`, `(program D X M)`, `(store S)`, none = library; built by builders; stages never inferred | grammar.md l.103, l.107-117; overview.md l.106-115; decisions.md l.55, l.66, Q11; milestone-2.md l.100, l.107 | post-solve match of main's closed type; main ordinary (Q5) | syntactic recognisers 13146-13240 |

542+| Islands | `main` record of exactly init/update/view/subs; `island` checks data against init's sample; update/subs/init types from the prelude | overview.md l.112, l.115-121, l.155, l.166; grammar.md l.293-343; decisions.md l.70-71 | follows from prelude types once tags defer across `++` | R1-R6 |

543+| Gate-free island data/model | no gates in data and models; name the field | overview.md l.121; decisions.md l.73; core-language.md l.39; milestone-2.md l.109, l.124 | post-solve gate-free check with witness path | `program-main-closed` 14555 + 5951 (256) |

545+| Stores | `state`, local `+$ poke`, `++ main (store init update)`; builder `\|= [init=S update=$-([A S] S)] ^- (store S)`; kind check verifies A against poke; derived poke helper and state request; one store per page | overview.md l.168-169; grammar.md l.105, l.293-306, l.343; decisions.md l.77-78, Q11 | record A's instantiation at main's application, or check update against `$-([poke state] state)` | R8 |

546+| APIs | `/ui/api/<agent>.jibb` declares `+$ poke` and `+$ paths` (declarations); `(facts full diff …)` with fold `$-([[%mark diff] full] full)`; optional `scry=`; derived poke helper and one request per case; clashes are errors | overview.md l.283-307, l.157-158; grammar.md l.105, l.134; decisions.md l.38-40; milestone-2.md l.111-114 | declaration elaboration into interface schemes | 12329-13148 |

547+| Watchability | islands read agents only by watching; first fact full state; a `scry=` case cannot be watched; unproven watchability is a type error; store state is watchable | overview.md l.159; grammar.md l.105; decisions.md l.38, l.79, Q33 | type-level marker or provenance analysis over the elaborated tree | one syntactic watch shape (14367) |

548+| Pages with data | `load` maps route parameters to one `ask`/`pure`; `view` takes D, returns `(element !!)` | overview.md l.125-130, l.334; grammar.md l.103; decisions.md l.67; milestone-2.md l.161 | ordinary application of `page` | one load shape (14512) |

551+| Prelude | Hoon stdlib regrouped in Jibb with a complete inventory; private internal module | overview.md l.81-102; decisions.md l.87-88; open-questions Q3; milestone-2.md l.116-121 | prelude checked by the same core and exported as an interface | partial interface (compiler.md:159) |

552+| No built-ins | type-directed rules only if listed in the Grammar; special cases for one gate are language changes | decisions.md l.34; milestone-2.md l.28 | `program`, `page`, `store`, `each`, `turn`, `element` as ordinary gates | R3, R7 are gate-specific |

553+| Printing | Jibb mold syntax; unnamed unions as space-separated cases; where-clauses; no private names | grammar.md l.137; overview.md l.77; decisions.md l.30-31; milestone-2.md l.143, l.148 | keep origin/name through solving; canonical names past 26 | 9930, 6345, 10171 |

554+| Errors | each error names both sites with excerpts; messages are golden tests; catalogue (aura mismatch, faces, missing case, open constraint, ctor, overlap, missing `?-` case, covered arm, self-dependent value, shadowing, interpolation, capitals, `~[text "hi"]`, clashing derived names, import cycle, `(facts …)` misuse, gate in island data, repeated attribute) | implementation-plan.md Risks; milestone-2.md l.48, l.123-127 | every constraint carries spans; union-find keeps a reason per binding | `idiag` 5997; 283 unsupported lines |

555+| Elaborated output | types/faces/casts leave nothing; lowering needs field axes, edits, decision tree, `proj` plans, printers, path validators | core-language.md l.74-98, l.33-41 | apply the final substitution to a typed tree | only width artifacts (5808) |

556+| Checker as function | caller passes Clay inputs; interface is its own noun; cache with interface and body hashed separately; modules one at a time in dependency order | milestone-2.md l.133; implementation-plan.md (pipeline, cache row); compiler.md:19 | interfaces store generalized schemes with constraints and mold templates | `ifile`, `prepare-prelude` |

559+

560+### 6.2 Open rulings that affect the core

561+

562+| Ruling | State | Effect on the core |

563+| --- | --- | --- |

564+| open-questions.md Q3 (prelude inventory and signatures) | open | Fixes the environment the core checks against; the prepared prelude is partial today |

565+| open-questions.md Q32 (`proj` reordering) | partly settled | How `proj` constraints discharge (jibb.hoon 4625 treats reordering as a doc question) |

566+| Review Q16 (A20): follow Hoon, `%1.000` is `@ud`, `%&` is `?` | proposed, awaiting @iko | How tag constraints discharge against atoms (today 5617-5626, 5636-5648) |

567+| Review Q17 (A20): a name term fits `@t` | proposed | Same discharge rule |

568+| Review Q18 (A23): `*` may hold gates | proposed "yes" | Fit to `*`, gate-free proofs, element's child erasure to `*` (prelude.jibb l.447-466), core-language.md l.33 |

569+| Review Q19 (A6, A100): reject `[]` and `m()` in the parser | proposed | Otherwise the core must reject them |

570+| Review Q20 (A30): `[a=@ud [a=@t b=?]]` is one record, duplicate `a` is an error | proposed | Record and field-access semantics (today nested tails get their own scope, 11556) |

571+| Review Q21 (A25): `/% %foo` beside `++ foo` | proposed | Scope check (11760) |

572+| Review Q22 (A15): an arm matching no remaining case is definite (`arm matches no case`) | proposed | Usefulness reports a useless row; today `union pattern is not supported` (8236, 8273, 8324) |

573+| Review Q23 (A55): `(mop K V)` without comparator | proposed | No comparator in the type |

574+| Review Q24 (A64): Hoon's `each` mold beside the `each` gate | proposed | Relies on separate namespaces |

576+| Review Q28 (A136): printer flattens `[a [b c]]`, prints named molds by name | proposed | Core must keep mold names through solving |

577+| Review Q6 (A122): render the report from the full checker | decided, not done | ~283 `types.txt` change once |

578+| Review Q37 (A126): tests keep calling ~137 internal arms | decided; revisit after the core | Keep arms or move suites behind a facade per stage |

579+| Syntax review S1: capitals bind only the type under a face; gate sample names ignored when gate types unify | question for @iko | Decides the face rules; reopens decisions.md l.33 and settled Q8; directly decides whether R11-R13 become unnecessary |

580+| Syntax review S3: samples/binders/locals may reuse prelude value names | question for @iko | Shadowing pass; todo-list's `[%typed text]` fails today |

581+| Syntax review S4: bare decimal fits only `@ud @u @ *` | question for @iko | Number-literal constraint (grammar.md l.21 says any aura) |

582+| Syntax review S5: a pattern name spelling a case tag at a union position is an error | question for @iko | Usefulness-time check |

583+| Syntax review S7: multi-letter type variables | question for @iko | Printer and capital scoping |

584+| Syntax review S12: nested cell patterns shown in the spec | question for @iko | The EBNF allows them; the prelude uses nested `?-` because the checker lacks them, so the core must handle nesting |

585+| Derived request argument order | unresolved in code (`api-request-parts` 12683) | Overview's `(post.api slug same)` suggests segments first |

586+| Application paths vs routes | milestone 4 | Core types `%/…` as qath with printable segments only |

587+| Spec sync | repository copy wins (Q42) | Unsynced decisions.md rows (Unions, Printed type constraints, Partial type annotations, Record fields, Record projection, Store builder, Agent APIs, Effects) may still differ from the design doc |

docs/spec/decisions.md+11−8

@@ -8,10 +8,12 @@ The choices behind the Language tab, made on 2026-10-23; a later date marks a re

99Until the Claude doc is synced with this copy, this copy is the spec (review question 42). Synced says whether the doc's Decisions tab has the row as written here. A row decided by 2026-10-29 or undated was in the doc when `spec/` was copied from it on 2026-10-30, and is unchanged. A row decided on or after 2026-10-31 is only here. A row of 2026-10-30 says Check: the copy had that day's answers to the 12 grammar questions, but other rows of that day were added or edited here afterwards ([docs/README.md](../README.md#the-spec)), and nobody has compared them with the doc yet.

1010

11+Rows dated 2026-11-03 are Montelot's decisions on the [syntax review](../reviews/2026-11-02-syntax-review.md): S1 with its step 1, S2, S4 to S7, S11 to S13 and S15. S1 step 1 is decided but not built yet; the checker core that review question 5 asks for will build it.

12+

1214| --- | --- | --- | --- |

13−| Syntax | Hoon's runes as keywords, and its literals; wide forms only for `\|=` and `$-`; changes take one or more record items, as `m(draft="x")`, so `m()` is an error; `.` reads fields, imports and prelude groups; no name may shadow another | Decided 2026-10-30 | Check |

14−| Literals | Exactly Hoon's, including `%$` as a term literal and pattern: `1000` is an error, `~2026.2.31` is `~2026.3.3`, and years BC and sub-second groups are dates; `print-date`'s minute form is not a literal | Decided 2026-10-30 | Check |

15+| Syntax | Hoon's runes as keywords, and its literals; wide forms only for `\|=` and `$-`; changes take one or more record items, as `m(draft="x")`, so `m()` is an error; an item may name a wing through record fields, as `m(open.cart=x)`, every value is computed from the original record, and two items that name the same field, or one inside the other, are an error; `.` reads fields, imports and prelude groups; no name may shadow another | Decided 2026-11-03 | No |

16+| Literals | Exactly Hoon's, including `%$` as a term literal and pattern: a bare decimal is a `@ud`, so `^- @dr 30` is an error and a duration is written `~s30`; `1000` is an error, `~2026.2.31` is `~2026.3.3`, and years BC and sub-second groups are dates; `print-date`'s minute form is not a literal | Decided 2026-11-03 | No |

1719| Strings | Hoon's escapes: `\\`, `\"`, `\{`, and `\` with two lowercase hex digits; a string and each `{…}` close on the line they open; `::` in a string is text | Decided 2026-10-30 | Check |

@@ -32,7 +34,7 @@ Until the Claude doc is synced with this copy, this copy is the spec (review que

3335| Equality and negation | The gates `eq` and `not`, with Hoon's bitwise `not` exposed as `not.bit`; `eq`'s arguments and map and set keys contain no gates, even nested; the checker infers and generalizes that constraint; union matching never inspects a gate to distinguish cases | Decided 2026-10-30 | Check |

35−| Inference | Hindley–Milner with aura variables; `@` is any atom, a specific atom fits `@` and a more specific aura fits an ancestor in its Hoon aura family, but each reverse needs a check, and repeated atom-constrained capitals give the same type; a number takes `@ud` only where its `++` isn't generic over its aura; distinct specific auras remain distinct; faces are part of record types, and an unnamed position can take a face but two different faces don't unify; principal types | Decided 2026-10-30 | Check |

37+| Inference | Hindley–Milner with aura variables; `@` is any atom, a specific atom fits `@` and a more specific aura fits an ancestor in its Hoon aura family, but each reverse needs a check, and repeated atom-constrained capitals give the same type; a decimal is a `@ud`, which fits `@u`, `@` and `*` but no other aura, except where its `++` is generic over its aura; distinct specific auras remain distinct; faces are part of record types, and an unnamed position can take a face but two different faces don't unify; a capital that meets a faced position binds only the type under the face, so `$-([A A] ?)` takes a gate with named parameters (not built yet); principal types | Decided 2026-11-03 | No |

3638| Effects | The library unions `cmd` and `sub`; `raw-poke`, `ask` and `qath` are transparent types defined in the internal prelude and re-exported normally; derived gates and `pure` also construct requests; islands read agents only by watching; replies get full state, and diffs take a fold; timers carry the time; `%who` gives the owner's `@p`; nacks reach replies as text | Decided 2026-11-01 | No |

3739| Poke representation | The source-backed private internal prelude module defines `raw-poke`, and the public prelude re-exports it as an ordinary transparent type. A store's local `poke` action remains an ordinary mold; derived helpers produce the runtime envelope | Decided 2026-11-01 | No |

3840| Agent APIs | `/ui/api/<agent>.jibb` with `+$ poke` and `+$ paths`, over the agent's mark types; a case is a name, a path and a type, with `(facts full diff …)` for diffs, told apart by mark; an optional scry path, for pages; an island may watch a request only when the checker proves it is watchable, so a separate scry path or unknown watchability is an error; typed segments by aura | Decided 2026-10-31 | No |

@@ -40,21 +42,22 @@ Until the Claude doc is synced with this copy, this copy is the spec (review que

4042| Derived gates | API files and stores give a generic `poke` command helper taking an action and reply, and a checked request per path or store state; clashing names are errors, including a derived name that clashes with an import face | Decided 2026-11-01 | No |

4143| Hoon types | A fixed translation table; `map`, `set`, `qeu`, `jar`, `jug` by name; `mop` as `(mop K V)`, read with `on`; imported `$%`, `$?` and `$^` cases must differ as nouns, and records with duplicate field names are errors where used; unused molds skipped | Decided 2026-10-30 | Check |

45+| Unface | The explicit type-directed operation `unface` removes every face from its argument's type, through cells, a gate's sample and product, and containers' arguments; unions and recursive molds go by name and are kept whole; like `proj`, it is reserved and not a value; it leaves nothing behind at run time | Decided 2026-11-03 | No |

4346| Record projection | The explicit type-directed operation `proj` takes a record and uses its expected result type to select its fields; no projection is inserted automatically. `proj` is reserved and cannot be defined or imported under that name. The result has exactly the fields declared by its type | Decided 2026-10-31 | No |

47+| Layout | Indentation; juxtaposed calls; a bracket open at line end takes one item per line, with no closer; a block of deeper lines belongs to the line above, so a call never continues onto a deeper line; a body's final line may hand the rest of the body, at its depth, to a tall `\|=`, `^-` or `~&` that ends it, and a `?-` that begins it may take its arms at its depth | Decided 2026-11-03 | No |

4548| Elements | Ordinary gates; containers take attribute lists; `stack` switches at `wide`; `el` adds attributes and wins; headings 1 to 6; `form` sends on Enter, the innermost when nested; `image` from an application path, sized from the file, or a sized URL; no focus control for now | Decided 2026-10-29 | Yes |

50−| Type variables | Capitals, generalized per `++`; a capital in a local `++` shares the enclosing `++`'s variable of that name if the enclosing `++` also uses it; otherwise it is introduced and generalized locally; a different type takes a different capital; a body cannot force distinct capitals to be equal, so a shared type uses the same capital; one used where an atom is required gains an inferred atom constraint, and cannot be fixed to a more specific type in its body | Decided 2026-10-30 | Check |

53+| Type variables | A capital, then lowercase letters and digits, as `A` or `Msg`, printed by the name they were written with; generalized per `++`; a capital in a local `++` shares the enclosing `++`'s variable of that name if the enclosing `++` also uses it; otherwise it is introduced and generalized locally; a different type takes a different capital; a body cannot force distinct capitals to be equal, so a shared type uses the same capital; one used where an atom is required gains an inferred atom constraint, and cannot be fixed to a more specific type in its body | Decided 2026-11-03 | No |

5154| Partial type annotations | `_` may appear wherever a mold may appear and marks that part of the type for inference; a hole inferred as a named type variable is resolved; an unconstrained hole is an error, and a named mold or value definition must determine its own holes without constraints from later uses | Decided 2026-10-31 | No |

60+| Binding patterns | In `?-` arms; the last position binds the rest; cells of patterns nest; a bare name is an error where a case the pattern can match has there a tag the name spells, as `stop` for `%stop` | Decided 2026-11-03 | No |

5861| Text | Strings are written only as `"…"` and are always cords; tapes come from `trip`; `{…}` prints by aura, a bare `@` as `@ud`, and an atom whose aura its `++` is generic over is an error; `print-date` prints Urbit-style to the minute in the theme's zone, from jibb-dev's zone table; numbers keep Hoon's form | Decided 2026-10-30 | Check |

5962| Auras | Specific auras stay distinct; `@` is any atom, a more specific aura fits an ancestor in its Hoon aura family one way, with the reverse requiring a check, and shared atom-constrained type variables preserve the same aura | Decided 2026-10-30 | Check |

@@ -96,7 +99,7 @@ Until the Claude doc is synced with this copy, this copy is the spec (review que

102+| Formatter | One canonical layout: a cast whose expression takes the deeper lines ends the line it belongs to; every `?-` begins its own line, with its arms at its depth where the rest of a body allows that | Decided 2026-11-03 | No |

101104

102105## Settled milestone 2 questions

docs/status.md+10−2

@@ -36,6 +36,8 @@ These rows cover milestone 1. The plan's three done-when criteria are the rows o

3636| Layout pass: `+layout` (library section 2) emits INDENT, DEDENT and NEWLINE | Done | `lex-layout-*`, `lex-indent-*`, `lex-rune-layout-*` |

3737| Lexical rules: for each rule, inputs that break it, with the error's expected place, and inputs that keep it | Done: 148 `-bad-` and 57 `-ok-` cases; the left-out closers, blob and `@c` literals have only `-bad-` cases, and so does `lex-char` | `lex-*` |

3838| Parser: `+parse` and `+parse-tokens` (library section 3) turn the Grammar tab's EBNF into a syntax tree | Done | every golden `tree.txt` |

39+| The rest of a body (syntax review S2): a body's final line hands the lines after it at its depth to a tall `\|=`, `^-` or `~&` that ends it, and a `?-` that begins it may take its arms at its depth; arm, bracket, top-level and definition lines keep deeper bodies | Done: a body of 40,000 same-depth rest lines runs out of memory under eval, where 20,000 parse | `lex-body-rest-*`, [lex-rune-layout-ok-3](../tests/golden/lex-rune-layout-ok-3/) |

40+| Type variables longer than one letter (S7): a capital, then lowercase letters and digits; `AB`, `MSG` and `Msg_x` are errors | Done | `lex-typevar-*` |

3941| Unions without `$?`: a `+$` takes its cases on the lines below, and `$?` is an error | Done | [inline-union-wide](../tests/golden/inline-union-wide/), [inline-union-one-case](../tests/golden/inline-union-one-case/), `inline-hoon-union-*` |

4042| Spans: every node keeps its start and end, and `+golden` appends `SPAN ERROR` when `+check-spans` fails | Done | [jibb-check-spans](../tests/lib/jibb-check-spans.hoon), `tools/golden` |

4143| Parse errors: file, line, column, message, excerpt and caret (`+show-error`), at the first character where the text stops being the start of any valid module (library section 2.0) | Done: each failing case's `about.txt` states the position, except the unclear case below | `lex-*-bad-*`, `inline-*-bad` |

@@ -109,6 +111,7 @@ Two independent audits came before 7c739b7: one compared the library with a refe

109111| Unification: the library's own `+itype-unify-test` cases | Done | [jibb-typecheck](../tests/lib/jibb-typecheck.hoon) |

110112| Atoms: `@`, one-way widening to aura-family parents, branch widening to a present parent, atom constraints from capitals or bare binders | Partial: generic joins needing a common-type rule are unsupported | [types-partial-atom-widening](../tests/golden/types-partial-atom-widening/), [types-partial-aura-family](../tests/golden/types-partial-aura-family/), [types-partial-branch-widening](../tests/golden/types-partial-branch-widening/), [types-partial-bare-atom](../tests/golden/types-partial-bare-atom/), [types-partial-many-atom-constraints](../tests/golden/types-partial-many-atom-constraints/) |

111113| Decimal defaulting: unfixed decimals become `@ud` in gate-free types, including tuples and polymorphic calls | Partial: gate types still report "unresolved aura-variable inference" | [types-partial-decimal-default](../tests/golden/types-partial-decimal-default/) |

114+| Bare decimals fit only `@ud`, `@u`, `@` and `*` (S4), in casts, calls, fields, lists, branch joins and number patterns, with a hint for the aura's own literal | Partial: number patterns are checked only on known-union and atom subjects; a constructor applied directly, `(\|=%wait 30)`, keeps the generic message | `inline-decimal-*` |

112115| Literal heads: `%$` matches null-, loobean-zero- and term-zero-headed cases, and equal heads with disjoint payloads select a unique case | Partial: overlapping same-noun cases decline | [types-literal-constructor-nouns](../tests/golden/types-literal-constructor-nouns/), [types-equal-head-disjoint](../tests/golden/types-equal-head-disjoint/), [types-loobean-singleton-source](../tests/golden/types-loobean-singleton-source/) |

113116| String interpolation: known auras, `@`, tapes and isolated decimals; a known cell asks for a printer, a generic atom for an aura | Partial: a gate or non-tape list, which the Grammar makes a printer error, pending tags, generic or unknown types and a type fixed only later are unsupported | [types-string-interpolation](../tests/golden/types-string-interpolation/) |

114117| Annotation holes: each value or local definition resolves its own `_` before generalization, and later uses cannot repair it | Done: independent decimal holes default to `@ud`, captured and written-capital variables don't, and structural named molds report the hole's site | `types-hole-*`, [jibb-hole-guards](../tests/lib/jibb-hole-guards.hoon) |

@@ -123,10 +126,11 @@ Two independent audits came before 7c739b7: one compared the library with a refe

123126| --- | --- | --- |

124127| Duplicate field names in a written record, including nested records, samples and expressions | Done: both sites are shown | [types-record-field-nested-mold](../tests/golden/types-record-field-nested-mold/), [types-record-field-expr-duplicate](../tests/golden/types-record-field-expr-duplicate/), [types-record-field-sample-duplicate](../tests/golden/types-record-field-sample-duplicate/) |

125128| Acyclic local definitions with captures, simple and nonrecursive generic mold aliases, faced record casts and field reads | Partial: selected shapes only | `types-local-*`, `types-generic-*`, `types-record-*` |

126−| Record changes: uniquely named fields, nested wings, field context for replacements | Done: unknown or partly unfaced spines are unsupported, and mismatches point at the edit, not the field's declaration | [types-record-change](../tests/golden/types-record-change/) |

129+| Record changes: uniquely named fields, wing items through record fields (S6), with same-field and nested overlaps rejected, nested wings, field context for replacements | Done: unknown or partly unfaced spines are unsupported, and mismatches point at the edit, not the field's declaration | [types-record-change](../tests/golden/types-record-change/) |

127130| Record initializers under a known record cast, including nested list and union fields | Partial: mismatches point at the cast mold | [types-record-cast-context](../tests/golden/types-record-cast-context/) |

128131| A value of type variable `A` in a field typed `A`, including union payloads and nested or repeated fields | Partial: faces of differing variables don't merge | [types-generic-face-inference](../tests/golden/types-generic-face-inference/) |

129132| `proj`: explicit `(proj record)` with a known closed record type, keeping field-axis evidence for lowering; `proj` is reserved in definitions, samples, patterns and imports | Partial: same-order fields only; no context, a bare or aliased `proj` and the wrong arity fail closed | [jibb-proj-guards](../tests/lib/jibb-proj-guards.hoon), `types-proj-*` |

133+| `unface` (S1): removes every face from its argument's type, through cells, gate samples and products, containers' arguments and the unit's payload, keeping unions and recursive molds whole; reserved with `proj`; `++ f (unface \|= …)` is a gate for recursion | Partial: an argument of unknown type is unsupported; islands, pages and stores don't see a gate through `unface`; lowering waits for milestone 3 | `inline-unface-*` |

130134| `proj` with reordered fields or in nested unit, list or call contexts; `proj` lowering and execution | Missing: field order is open (question 32 in [open-questions.md](open-questions.md)) | [types-proj-explicit-context](../tests/golden/types-proj-explicit-context/), [types-proj-nested-no-implicit](../tests/golden/types-proj-nested-no-implicit/) |

131135| List literals without context, empty and nested, generalized independently | Partial: unresolved item tags and uncertain widening fail closed | [types-list-open](../tests/golden/types-list-open/), [types-list-open-constraints](../tests/golden/types-list-open-constraints/) |

132136| List literals with the validated prelude list and a known cast or sample: empty, nonempty, nested and cons, contextual tags, imported-list contexts | Done: a bad element, head or tail names both sites | [types-list-context](../tests/golden/types-list-context/), [types-list-cons](../tests/golden/types-list-cons/), [types-list-imported](../tests/golden/types-list-imported/), [types-list-zero-fit](../tests/golden/types-list-zero-fit/) |

@@ -150,6 +154,7 @@ Two independent audits came before 7c739b7: one compared the library with a refe

150154| Generic aliases may reorder, repeat or omit parameters, keeping a union's origin through scopes and library interfaces | Done: generic unions declared in a body and constraints on differing variables' faces are unsupported | [types-generic-union-alias](../tests/golden/types-generic-union-alias/), [types-generic-union-transitive](../tests/golden/types-generic-union-transitive/), [jibb-generic-alias](../tests/lib/jibb-generic-alias.hoon) |

151155| Nested unions compare by runtime noun; an empty field empties a cell, and unknown inhabitation stays unresolved | Done | [types-partial-union-nested-nouns](../tests/golden/types-partial-union-nested-nouns/) |

152156| Union patterns: whole-case arms, payload binders, imported and generic cases and binder-free catch-alls; missing cases and covered arms are reported | Done | [types-union-patterns](../tests/golden/types-union-patterns/), [types-union-patterns-generic](../tests/golden/types-union-patterns-generic/), [types-union-patterns-import](../tests/golden/types-union-patterns-import/) |

157+| A bare pattern name that spells a tag a matching case has at that position is an error (S5), on every checker path that types `?-` | Done: the full module check reports it only as "needs unsupported inference" | `inline-pattern-tag-name-*` |

153158| Partial boolean patterns: `?` positions split into at most 64 alternatives across the union | Done: past the limit the report says "union pattern expansion needs unsupported inference" | [types-union-finite](../tests/golden/types-union-finite/), [types-union-finite-limit](../tests/golden/types-union-finite-limit/), [types-union-finite-generic](../tests/golden/types-union-finite-generic/) |

154159| Other partial patterns, binders spanning cases, some complex two-arm subjects | Missing: fail closed | [types-union-finite-limit](../tests/golden/types-union-finite-limit/), [types-union-patterns-generic](../tests/golden/types-union-patterns-generic/) |

155160| Union pattern result context from a cast or call sample, for a union reached by a wing, grouped wing or shallow call | Partial: other subject forms are unsupported | [types-union-pattern-result-context](../tests/golden/types-union-pattern-result-context/), [types-union-pattern-result-controls](../tests/golden/types-union-pattern-result-controls/), [types-union-finite-context](../tests/golden/types-union-finite-context/) |

@@ -165,6 +170,8 @@ Two independent audits came before 7c739b7: one compared the library with a refe

165170| --- | --- | --- |

166171| Multi-argument calls: a right-nested sample keeping faces and shared variables, giving context to list and union arguments | Done: unknown-callee contexts and pending tags are unsupported | [types-multi-call](../tests/golden/types-multi-call/) |

167172| Positional calls unify a variable argument with a faced sample slot without passing the face on | Done: `labelled` checks as `$-([label=@t msg=A] (element A))` | [jibb-buttons](../tests/lib/jibb-buttons.hoon), [jibb-positional-face-guards](../tests/lib/jibb-positional-face-guards.hoon), [jibb-closed-gate-guards](../tests/lib/jibb-closed-gate-guards.hoon), [types-positional-faces](../tests/golden/types-positional-faces/) |

173+| A capital that meets a faced position binds only the type under the face (S1 step 1, decided 2026-11-03) | Missing: `(hunt lt-a `1 `2)` still fails; the checker core of review question 5 builds it | [inline-unface-labelled-slot](../tests/golden/inline-unface-labelled-slot/) |

174+| Printed type variables keep their written names (S7), as `(program Data Model Msg)`; a variable with no name prints as an unused letter | Done: when named variables merge, a capital written in the `++` names the result, otherwise the earliest-made one | [types-typevar-names](../tests/golden/types-typevar-names/), [types-typevar-print](../tests/golden/types-typevar-print/) |

168175| Named unions through unconstrained polymorphic gates, keeping origin, arguments and faces | Partial: different origins, explicit-capital forcing and pending tags are unsupported | [types-union-polymorphic-identity](../tests/golden/types-union-polymorphic-identity/) |

169176| Direct gate sample fit: a directly named, checked root gate against a generic gate sample in a direct prelude call | Partial: other cases fall back to ordinary inference, and it proves no island or watchability | [jibb-direct-gate-guards](../tests/lib/jibb-direct-gate-guards.hoon), [jibb-direct-gate-source](../tests/lib/jibb-direct-gate-source.hoon) |

170177| Single self-recursive gates, top-level and local: a monomorphic self reference, then generalization; bad recursive arguments name both sites | Done: polymorphic recursion, explicit-capital forcing and local name collisions are unsupported | [types-recursive-sample](../tests/golden/types-recursive-sample/), [types-recursive-gate](../tests/golden/types-recursive-gate/), [types-local-recursive](../tests/golden/types-local-recursive/) |

@@ -202,7 +209,8 @@ Two independent audits came before 7c739b7: one compared the library with a refe

202209| The validated `list` template for the prelude's own gates and mold aliases; an altered, omitted, duplicate or malformed `list` doesn't leak through aliases | Done | [jibb-list-alias-guards](../tests/lib/jibb-list-alias-guards.hoon), [types-prelude-list-alias](../tests/golden/types-prelude-list-alias/), [types-prelude-list-functions](../tests/golden/types-prelude-list-functions/) |

203210| The prelude `list` and imported Hoon lists unify both ways | Partial: other Jibb-written collection molds and most collection operations are unsupported | [types-list-imported](../tests/golden/types-list-imported/), [types-list-pattern-imported](../tests/golden/types-list-pattern-imported/), [jibb-bridge](../tests/lib/jibb-bridge.hoon) |

204211| With `list` or `unit` missing or altered, independent private molds (`qath`) stay available and dependent ones (`ask`) don't | Done | [jibb-qath-source](../tests/lib/jibb-qath-source.hoon), [jibb-ask-guards](../tests/lib/jibb-ask-guards.hoon) |

205−| Module scope: the prepared and source-taking prelude paths compared against the real prelude | Partial: does not establish complete shadowing coverage | [jibb-module-scope](../tests/lib/jibb-module-scope.hoon), [types-prelude-interface](../tests/golden/types-prelude-interface/) |

212+| Module scope: the prepared and source-taking prelude paths compared against the real prelude | Partial: full checks name top-level conflicts and show both sites when sources are available; nested reserved names and API mark conflicts can still be generic | [jibb-full-scope](../tests/lib/jibb-full-scope.hoon), [jibb-module-scope](../tests/lib/jibb-module-scope.hoon), [types-prelude-interface](../tests/golden/types-prelude-interface/) |

213+| Full-check definition diagnostics | Partial: definite inference failures on unresolved definitions retain their sites; mold, kind and context-dependent failures remain incomplete | [jibb-full-diagnostics](../tests/lib/jibb-full-diagnostics.hoon) |

206214| `fall` and `need` | Done | [prelude-list-unit](../tests/golden/prelude-list-unit/), [types-prelude-direct](../tests/golden/types-prelude-direct/) |

207215| `drop`, `skim`, `skip`, `murn`, `join`, `snip`, `rear` and a shared-type `clap` | Partial: no test calls `rear` | [types-prelude-list-helpers](../tests/golden/types-prelude-list-helpers/), [types-prelude-unit-helpers](../tests/golden/types-prelude-unit-helpers/) |

208216| `bond`, `levy`, `lien`, and gate composition and currying | Partial: currying a faced sample is unsupported | [types-prelude-bond](../tests/golden/types-prelude-bond/), [types-prelude-predicates](../tests/golden/types-prelude-predicates/), [types-prelude-functional](../tests/golden/types-prelude-functional/) |

jibb-dev/lib/jibb.hoon+228−41

@@ -849,6 +849,90 @@

849849:: %submitt [m(note="") ~]

850850:: ^

851851::

852+:: ===================================================================

853+:: 5. General checker core (design; not implemented yet)

854+:: ===================================================================

855+::

856+:: The existing inference and recovery paths are described in

857+:: docs/compiler.md. This section is a plan for replacing them, not a

858+:: claim that the current checker implements these rules. The Grammar and

859+:: Decisions are authoritative if this design needs adjustment.

860+::

861+:: 5.1 State and unification. Give each inference variable an identity and

862+:: a union-find entry: parent or binding, rank, level, source, rigidity,

863+:: and the atom, arithmetic-atom and gate-free obligations it carries.

864+:: Hoon's immutable maps hold the entries; operations return the updated

865+:: state. Find compresses paths in that returned state. Bind only after an

866+:: occurs check, merge obligations at roots, and lower levels throughout

867+:: the bound type to the root's level. A rigid written capital may acquire

868+:: allowed constraints but cannot be forced to a concrete type or a

869+:: different written capital. Keep origins for both sides of each fit so

870+:: a failure can show both excerpts. Recursive named molds retain their

871+:: identity; the occurs check is for inference variables, not a ban on

872+:: declared recursion.

873+::

874+:: A scheme quantifies eligible variables above the enclosing level;

875+:: instantiate with fresh variables and copy their obligations. Written

876+:: capitals respect their lexical scope, including sharing with a local

877+:: definition when the enclosing definition uses the same name. Retain

878+:: aura variables and directional aura fits, rather than turning every

879+:: fit into symmetric equality. At a faced position a capital binds the

880+:: type under the face; joining an unnamed position with a faced one keeps

881+:: the face, independently of the order of the inputs. Different explicit

882+:: faces conflict. No gate may hide inside a gate-free type, including in

883+:: a container; propagate the obligation through its arguments.

884+::

885+:: 5.2 Work queue. A constraint owns its source span, the types and

886+:: expression shape it depends on, and the information needed to report

887+:: failure. Tags and constructors, null, decimal and cell literals,

888+:: wings, changes, unface and unknown match subjects enter the same queue.

889+:: Index waiting constraints by the roots they read. Binding or merging a

890+:: root wakes its dependants; a retry either solves, fails with its sites,

891+:: or registers the roots still needed. Run to a fixed point, without

892+:: losing constraints when a root is redirected. Check patterns once the

893+:: subject is known. Contextual tags inspect case shapes and noun-equal

894+:: heads, retaining the named union and its site in diagnostics.

895+::

896+:: Variables reachable from an open tag constraint remain monomorphic

897+:: across definitions, so a later use, including main, can fix them.

898+:: Other eligible variables can generalize, with their atom and gate-free

899+:: obligations intact. At each definition boundary resolve its holes and

900+:: apply the specified decimal and cell defaults, without defaulting a

901+:: decimal whose definition is generic over its aura. A decimal fits @ud,

902+:: @u, @ and *; other concrete auras need their own literal. At module

903+:: completion retry the queue and report each still-open constraint at its

904+:: source; an unresolved tag asks for a ^-, never a guessed union.

905+::

906+:: 5.3 Definition order and kinds. Use the existing dependency graph's

907+:: strongly connected components in dependency order. Give a recursive

908+:: group of gates monomorphic placeholders, infer all members in one state,

909+:: solve what can be solved, then generalize together. Reject a cycle

910+:: involving a non-gate value, including one through a gate, and show the

911+:: cycle. Check a named definition's holes before later uses can fix them.

912+:: Infer main as an ordinary expression against ordinary prelude schemes;

913+:: only its resulting type determines library, page, island or store.

914+:: Afterwards check kind-specific invariants: recursively find the field

915+:: containing a gate in island data or a model, and inspect subscriptions

916+:: for watchability only at %watch. A page load may be any gate to ask,

917+:: including pure and typed paths. Preserve request provenance needed for

918+:: a watchability proof through ordinary calls and aliases.

919+::

920+:: 5.4 Matches and migration. A reusable usefulness matrix over noun

921+:: constructors, constants, cells and wildcards checks nested patterns;

922+:: loobeans, lists and units expand to their cases. Test an arm against

923+:: previous rows for usefulness, then test a wildcard for exhaustiveness;

924+:: keep a witness for a missing case and the covering arm's site for a

925+:: dead one. Recursive types require memoized specialization and a

926+:: terminating treatment of recursive states. The same matrix can later

927+:: drive lowering. The bare-name/tag spelling rule is checked against the

928+:: subject and the cases the rest of the pattern can match.

929+::

930+:: Migrate in small stages with eval and ship goldens for every change.

931+:: Keep diagnostics and source sites in the single full result; types.txt

932+:: is a rendering of that result. As general inference covers an existing

933+:: recovery or source-proven slice, remove that slice and retain its tests.

934+:: An unsupported construct fails closed at its own site until then.

935+::

852936|%

853937+| %positions

854938::

@@ -11307,7 +11391,7 @@

1130711391 `[entry u.rest]

1130811392::

1130911393

11310−+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]

11394++$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]

1131111395+$ iadj (map term (list term))

1131211396+$ ivisited (map term ?)

1131311397+$ iwork (list [name=term done=?])

@@ -11403,7 +11487,7 @@

1140311487++ add-groups

1140411488 |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]

1140511489 ^- iresolved

11406− ?~ components [env grouped artifacts]

11490+ ?~ components [env grouped artifacts ~]

1140711491 =/ component=(list term) i.components

1140811492 ?. (graph-cycle component graph) $(components t.components)

1140911493 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)

@@ -11447,8 +11531,10 @@

1144711531 `[[[name.d (cap-names typ vars caps.state.p.result sub.state.p.result)] env] checked artifacts]

1144811532++ add-supported-defs-core

1144911533 |= [ds=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]

11450− ^- [env=ienv artifacts=(list iwidth-definition)]

11451− ?~ ds [env artifacts]

11534+ ^- [env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]

11535+ =/ failures=(list [name=term diag=idiag]) ~

11536+ |-

11537+ ?~ ds [env artifacts (flop failures)]

1145211538 =/ d=def i.ds

1145311539 ?: ?=(%mold -.d) $(ds t.ds)

1145411540 ?. (unique-value-name name.d globals) $(ds t.ds)

@@ -11459,37 +11545,34 @@

1145911545 =. gate-defs.initial checked

1146011546 =. head-evidence.initial heads

1146111547 =. initial (reserve-def-caps val.d initial)

11462− =/ result=iresult (infer-fragment val.d env initial)

11548+ =/ plain=iresult (infer-fragment val.d env initial)

11549+ =/ result=iresult plain

1146311550 =? result ?=(%| -.result) (infer-recursive-gate d env initial)

11551+ ?: ?=(%| -.result)

11552+ =/ failure=idiag

11553+ ?: (definite-diag p.result) p.result

11554+ ?: ?=(%| -.plain) p.plain

11555+ p.result

11556+ =? failures (definite-diag failure) [[name.d failure] failures]

11557+ $(ds t.ds)

1146411558 =/ added=(unit iadded-definition)

1146511559 (add-supported-result d result initial env checked artifacts)

1146611560 ?~ added $(ds t.ds)

1146711561 $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)

1146811562::

11469−:: Full checking discards unsupported definitions. On that failure path only,

11470−:: retry a bounded number of missing definitions to explain a pending tag

11471−:: from the same ordinary inference state instead of hiding it behind the

11472−:: generic completeness error. No successful definition takes this path.

11473−++ module-pending-tag

11474− |= [ds=(list def) env=ienv base=istate fuel=@ud]

11563+:: Retry one unresolved definition to explain a pending tag. The gate

11564+:: evidence is built from the whole module, not only this definition.

11565+++ module-pending-tag-one

11566+ |= [d=def env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence)]

1147511567 ^- (unit [at=span msg=tape])

11476− =/ checked=(map term def) (direct-checked-gates ds env)

11477− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.base)

11478− |-

11479− ?~ ds ~

11480− ?: =(0 fuel) ~

11481− =/ d=def i.ds

11482− ?: ?=(%mold -.d) $(ds t.ds, fuel (dec fuel))

11483− ?^ (ienv-lookup name.d env) $(ds t.ds, fuel (dec fuel))

11568+ ?. ?=(%value -.d) ~

11569+ ?^ (ienv-lookup name.d env) ~

1148411570 =/ initial=istate base(gate-defs checked, head-evidence heads)

1148511571 =. initial (reserve-def-caps val.d initial)

1148611572 =/ result=iresult (infer-fragment val.d env initial)

1148711573 =? result ?=(%| -.result) (infer-recursive-gate d env initial)

11488− ?: ?=(%| -.result) $(ds t.ds, fuel (dec fuel))

11489− =/ pending=(unit [at=span msg=tape])

11490− (pending-tag-diagnostic tags.state.p.result sub.state.p.result)

11491− ?^ pending pending

11492− $(ds t.ds, fuel (dec fuel))

11574+ ?: ?=(%| -.result) ~

11575+ (pending-tag-diagnostic tags.state.p.result sub.state.p.result)

1149311576::

1149411577++ resolve-groups-core

1149511578 |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]

@@ -11505,12 +11588,12 @@

1150511588 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)

1150611589 =/ ordered=(list def) (dependency-order ds components)

1150711590 |-

11508− =/ next=[env=ienv artifacts=(list iwidth-definition)]

11591+ =/ next=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]

1150911592 (add-supported-defs-core ordered (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts index)

1151011593 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]

1151111594 =. grec-index.initial index

1151211595 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)

11513− ?: =(env env.out) out

11596+ ?: =(env env.out) out(failures failures.next)

1151411597 $(env env.out, grouped grouped.out, artifacts artifacts.out)

1151511598::

1151611599:: +dependency-order: the value definitions, dependencies first

@@ -12540,6 +12623,80 @@

1254012623 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))

1254112624 |((lien (weld imported (weld vals mold-names)) reserved-name) (lien defs.mod reserved-def))

1254212625::

12626+:: A scope collision retains source sites. Prelude declarations may be in

12627+:: another source, so their name and namespace are retained separately.

12628++$ iscope-diagnostic

12629+ [issue=idiag prelude=(unit [name=term kind=?(%value %mold %any)])]

12630+++ scope-import-diagnostic

12631+ |= [imports=(list import) prelude-values=(list term) prelude-molds=(list term) seen=written-fields]

12632+ ^- (each written-fields iscope-diagnostic)

12633+ ?~ imports [%& seen]

12634+ =/ imp=import i.imports

12635+ =/ n=term

12636+ ?- -.imp

12637+ %jibb face.imp

12638+ %sur name.imp

12639+ %mark mark.imp

12640+ ==

12641+ ?: (reserved-name n)

12642+ [%| [["`{(trip n)}` is reserved and cannot be bound" ~[[at.imp "reserved name"]]] ~]]

12643+ =/ earlier=(unit span) (~(get by seen) n)

12644+ ?^ earlier

12645+ [%| [["import `{(trip n)}` shadows an earlier import" ~[[u.earlier "earlier import"] [at.imp "conflicting import"]]] ~]]

12646+ ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x))))

12647+ [%| [["import `{(trip n)}` shadows a prelude name" ~[[at.imp "conflicting import"]]] `[n %any]]]

12648+ $(imports t.imports, seen (~(put by seen) n at.imp))

12649+++ scope-def-diagnostic

12650+ |= [defs=(list def) imports=written-fields prelude-values=(list term) prelude-molds=(list term) values=written-fields molds=written-fields]

12651+ ^- (unit iscope-diagnostic)

12652+ ?~ defs ~

12653+ =/ d=def i.defs

12654+ =/ n=term name.d

12655+ ?: (reserved-name n)

12656+ `[["`{(trip n)}` is reserved and cannot be bound" ~[[at.d "reserved name"]]] ~]

12657+ =/ imported=(unit span) (~(get by imports) n)

12658+ ?^ imported

12659+ `[["definition `{(trip n)}` shadows an import" ~[[u.imported "import"] [at.d "conflicting definition"]]] ~]

12660+ =/ seen=written-fields ?:(?=(%value -.d) values molds)

12661+ =/ earlier=(unit span) (~(get by seen) n)

12662+ ?^ earlier

12663+ `[["definition `{(trip n)}` shadows an earlier definition" ~[[u.earlier "earlier definition"] [at.d "conflicting definition"]]] ~]

12664+ =/ prelude-names=(list term) ?:(?=(%value -.d) prelude-values prelude-molds)

12665+ ?: (lien prelude-names |=(x=term =(n x)))

12666+ `[["definition `{(trip n)}` shadows a prelude name" ~[[at.d "conflicting definition"]]] `[n ?:(?=(%value -.d) %value %mold)]]

12667+ ?: ?=(%value -.d)

12668+ $(defs t.defs, values (~(put by values) n at.d))

12669+ $(defs t.defs, molds (~(put by molds) n at.d))

12670+++ module-scope-diagnostic

12671+ |= [mod=module prelude-values=(list term) prelude-molds=(list term)]

12672+ ^- (unit iscope-diagnostic)

12673+ =/ imports=(each written-fields iscope-diagnostic)

12674+ (scope-import-diagnostic imports.mod prelude-values prelude-molds ~)

12675+ ?: ?=(%| -.imports) `p.imports

12676+ (scope-def-diagnostic defs.mod p.imports prelude-values prelude-molds ~ ~)

12677+++ show-scope-diagnostic

12678+ |= [file=path src=@t diagnostic=iscope-diagnostic prelude=(unit ifile)]

12679+ ^- @t

12680+ =/ excerpts=(list @t)

12681+ %+ turn sites.issue.diagnostic

12682+ |= site=[at=span note=tape]

12683+ (show-error src [file line.beg.at.site col.beg.at.site note.site])

12684+ =/ previous=(list @t)

12685+ ?~ prelude.diagnostic ~

12686+ ?~ prelude ~

12687+ ?~ source.u.prelude ~

12688+ =/ parsed (parse at.u.prelude u.source.u.prelude)

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

12690+ =/ matching=(list def)

12691+ %+ skim defs.p.parsed

12692+ |= d=def

12693+ ?& =(name.d name.u.prelude.diagnostic)

12694+ |(=(%any kind.u.prelude.diagnostic) =(-.d kind.u.prelude.diagnostic))

12695+ ==

12696+ ?~ matching ~

12697+ ~[(show-error u.source.u.prelude [at.u.prelude line.beg.at.i.matching col.beg.at.i.matching "prelude declaration"])]

12698+ (of-wain:format [(crip msg.issue.diagnostic) (weld excerpts previous)])

12699+::

1254312700++ module-scope-valid

1254412701 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]

1254512702 ^- ?

@@ -12970,6 +13127,31 @@

1297013127 ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)

1297113128 `[u.name at.s]

1297213129::

13130+:: Select the first available reason in dependency order, rather than

13131+:: preferring one class of diagnostic across the whole module. Only the

13132+:: first 64 definitions are retried for pending tags, as before.

13133+++ module-unresolved-diagnostic

13134+ |= [ds=(list def) env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence) failures=(list [name=term diag=idiag]) values=(list term) file=path src=@t fuel=@ud]

13135+ ^- (unit @t)

13136+ ?~ ds ~

13137+ =/ d=def i.ds

13138+ =/ remaining=@ud ?:(=(0 fuel) 0 (dec fuel))

13139+ ?: ?=(%mold -.d) $(ds t.ds, fuel remaining)

13140+ ?^ (ienv-lookup name.d env) $(ds t.ds, fuel remaining)

13141+ =/ found=(list [name=term diag=idiag])

13142+ (skim failures |=(failure=[name=term diag=idiag] =(name.failure name.d)))

13143+ ?^ found `(show-inference-diagnostic file src name.d diag.i.found)

13144+ =/ pending=(unit [at=span msg=tape])

13145+ ?: =(0 fuel) ~

13146+ (module-pending-tag-one d env base checked heads)

13147+ ?^ pending

13148+ `(show-error src [file line.beg.at.u.pending col.beg.at.u.pending msg.u.pending])

13149+ =/ shadow=(unit [name=term at=span]) (module-sample-shadow ~[d] env values)

13150+ ?^ shadow

13151+ =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"

13152+ `(show-error src [file line.beg.at.u.shadow col.beg.at.u.shadow msg])

13153+ $(ds t.ds, fuel remaining)

13154+::

1297313155:: Cache only completed interfaces for this invocation. The source bundle,

1297413156:: imported Hoon types and prelude are fixed for the whole graph. Check the

1297513157:: active path and duplicate sources before consulting it, so a cache hit

@@ -14230,7 +14412,7 @@

1423014412 ?~ recovered ~

1423114413 ?. ?=(~ vars.u.recovered) ~

1423214414 ?. ?=(~ (itype-vars typ.u.recovered)) ~

14233− `[env.u.added grouped.resolution artifacts.u.added]

14415+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]

1423414416::

1423514417++ program-inferred-slot

1423614418 |= [typ=itype name=(unit term)]

@@ -14386,7 +14568,7 @@

1438614568 ?~ recovered ~

1438714569 ?. ?=(~ vars.u.recovered) ~

1438814570 ?. ?=(~ (itype-vars typ.u.recovered)) ~

14389− `[env.u.added grouped.resolution artifacts.u.added]

14571+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]

1439014572::

1439114573+$ iview-site [xs=expr mapper=term]

1439214574++ program-view-site

@@ -14713,7 +14895,7 @@

1471314895 ?~ recovered ~

1471414896 ?. ?=(~ vars.u.recovered) ~

1471514897 ?. ?=(~ (itype-vars typ.u.recovered)) ~

14716− `[env.u.added grouped.resolution artifacts.u.added]

14898+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]

1471714899::

1471814900:: Recover exactly one direct keyed each/turn row mapper, then its view.

1471914901:: The prelude's own each and turn schemes determine the mapper gate: the

@@ -14935,7 +15117,7 @@

1493515117 ?~ recovered ~

1493615118 ?. ?=(~ vars.u.recovered) ~

1493715119 ?. ?=(~ (itype-vars typ.u.recovered)) ~

14938− `[env.u.added grouped.resolution artifacts.u.added]

15120+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]

1493915121::

1494015122:: The model a direct program's initializer must produce. Update's written

1494115123:: two-item sample gives it when it can be read. Otherwise main's own program

@@ -15092,7 +15274,7 @@

1509215274 ?~ recovered ~

1509315275 ?. ?=(~ vars.u.recovered) ~

1509415276 ?. ?=(~ (itype-vars typ.u.recovered)) ~

15095− `[env.u.added grouped.resolution artifacts.u.added]

15277+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]

1509615278::

1509715279++ derived-poke-command-scheme

1509815280 |= [prelude=ifile action=itype]

@@ -15260,9 +15442,9 @@

1526015442 (direct-prelude-evidence ds prelude.initial)

1526115443 ?~ heads resolution

1526215444 =/ checked=(map term def) (direct-checked-gates ds env.resolution)

15263− =/ completed=[env=ienv artifacts=(list iwidth-definition)]

15445+ =/ completed=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]

1526415446 (add-supported-defs-core ~[main] checked heads env.resolution molds.initial globals.initial externals.initial surs.initial mark-externals.initial marks.initial jimports.initial reserved-molds.initial at.initial prelude.initial artifacts.resolution grec-index.initial)

15265− [env.completed grouped.resolution artifacts.completed]

15447+ [env.completed grouped.resolution artifacts.completed failures.resolution]

1526615448::

1526715449:: A static main may retain a generic element message in its ordinary

1526815450:: scheme. Instantiate that scheme, specialize it to canonical element !!,

@@ -15478,6 +15660,9 @@

1547815660 !(lien prelude-molds |=(m=term =(m n)))

1547915661 ==

1548015662 ==

15663+ =/ scope=(unit iscope-diagnostic)

15664+ (module-scope-diagnostic mod(defs ordinary, imports faces) prelude-values prelude-molds)

15665+ ?^ scope [%| [(show-scope-diagnostic at src u.scope prelude) ~]]

1548115666 [%| [(crip "module has conflicting names: {(spud at)}") ~]]

1548215667 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]

1548315668 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]

@@ -15526,6 +15711,9 @@

1552615711 =/ ds=(list def) ?~(declared defs.mod defs.u.declared)

1552715712 =/ checking=module mod(defs ds)

1552815713 ?. (module-scope-valid checking prelude-values prelude-molds)

15714+ =/ scope=(unit iscope-diagnostic)

15715+ (module-scope-diagnostic checking prelude-values prelude-molds)

15716+ ?^ scope [%| [(show-scope-diagnostic at src u.scope prelude) ~]]

1552915717 [%| [(crip "module has conflicting names: {(spud at)}") ~]]

1553015718 =/ vals=(list term) (global-value-names ds)

1553115719 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)

@@ -15601,15 +15789,14 @@

1560115789 ?~ store-parts ds

1560215790 (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))

1560315791 ?. (module-values-complete required env)

15604− =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)

15605− ?^ pending

15606− [%| [(show-error src [at line.beg.at.u.pending col.beg.at.u.pending msg.u.pending]) ~]]

15607− :: A shadowing sample is an error, so it comes before any named value.

15792+ =/ components=icomponents (graph-components required (global-value-names required))

15793+ =/ ordered=(list def) (dependency-order required components)

1560815794 =/ values=(list term) (weld prelude-values (weld (api-import-faces imports.mod) vals))

15609− =/ shadow=(unit [name=term at=span]) (module-sample-shadow required env values)

15610− ?^ shadow

15611− =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"

15612− [%| [(show-error src [at line.beg.at.u.shadow col.beg.at.u.shadow msg]) ~]]

15795+ =/ checked=(map term def) (direct-checked-gates required env)

15796+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence required prelude.state)

15797+ =/ diagnostic=(unit @t)

15798+ (module-unresolved-diagnostic ordered env state checked heads failures.resolution values at src 64)

15799+ ?^ diagnostic [%| [u.diagnostic ~]]

1561315800 =/ missing=(unit term) (module-missing-value required env)

1561415801 =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")

1561515802 [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]

tests/golden/module-import-api-scope-conflict/types.txt+7−1

@@ -1,2 +1,8 @@

11partial inference; module not checked

2−module has conflicting names: /ui/api/demo/jibb

2+import `same` shadows a prelude name

3+/ui/api/demo.jibb:2:1: conflicting import

4+/= same /ui/lib

5+^

6+/lib/jibb/prelude.jibb:7:1: prelude declaration

7+++ same |= x=A x

8+^

tests/golden/module-import-prelude-value-shadow/types.txt+7−1

@@ -1,2 +1,8 @@

11partial inference; module not checked

2−module has conflicting names: /ui/lib/jibb

2+definition `same` shadows a prelude name

3+/ui/lib.jibb:1:1: conflicting definition

4+++ same |=(x x)

5+^

6+/lib/jibb/prelude.jibb:7:1: prelude declaration

7+++ same |= x=A x

8+^

tests/golden/types-proj-reserved-imported-definition/types.txt+4−1

@@ -1,2 +1,5 @@

11partial inference; module not checked

2−module has conflicting names: /ui/lib/jibb

2+`proj` is reserved and cannot be bound

3+/ui/lib.jibb:1:1: reserved name

4+++ proj |= x=@t x

5+^

tests/lib/jibb-full-diagnostics.hoonnew file+45

@@ -0,0 +1,45 @@

1+:: Full-module diagnostics retain their inference sites.

2+/+ jibb

3+|%

4+++ test-full-diagnostics

5+ ^- tang

6+ =/ file=path /ui/probe/jibb

7+ =/ source=@t (of-wain:format ~['++ inc |= n=@ud n' '++ top (inc %.y)'])

8+ =/ result (infer-jibb-file-detailed:jibb file source ~ ~ ~ ~[file] ~ ~ ~ ~)

9+ ?: ?=(%& -.result) ~[leaf+"wrong argument was accepted"]

10+ =/ expected=@t

11+ (of-wain:format ~['++ top: call\'s sample and argument types do not unify' '/ui/probe.jibb:2:9: called gate has type $-(@ud @ud)' '++ top (inc %.y)' ' ^' '/ui/probe.jibb:2:13: argument has type ?' '++ top (inc %.y)' ' ^'])

12+ ?. =(expected message.p.result) ~[leaf+"full checker lost the argument diagnostic"]

13+ =/ forward=@t (of-wain:format ~['++ top (inc 5)' '++ inc |= n=@ud n'])

14+ =/ ok (infer-jibb-file-detailed:jibb file forward ~ ~ ~ ~[file] ~ ~ ~ ~)

15+ ?: ?=(%| -.ok) ~[leaf+"forward definition did not resolve"]

16+ :: An earlier open tag and an earlier shadow must not be hidden by a

17+ :: definite call mismatch in another unresolved definition.

18+ =/ pending-source=@t (of-wain:format ~['++ x %add' '++ inc |= n=@ud n' '++ bad (inc %.y)'])

19+ =/ pending-result (infer-jibb-file-detailed:jibb file pending-source ~ ~ ~ ~[file] ~ ~ ~ ~)

20+ ?: ?=(%& -.pending-result) ~[leaf+"open tag was accepted"]

21+ =/ pending-expected=@t

22+ (of-wain:format ~['/ui/probe.jibb:1:6: nothing fixes the union of %add' '++ x %add' ' ^'])

23+ ?. =(pending-expected message.p.pending-result) ~[leaf+"earlier pending tag was masked"]

24+ :: A forward dependency precedes its user even when its source line is

25+ :: after a separate mismatch.

26+ =/ dependency-source=@t (of-wain:format ~['++ wrapper x' '++ inc |= n=@ud n' '++ bad (inc %.y)' '++ x %add'])

27+ =/ dependency-result (infer-jibb-file-detailed:jibb file dependency-source ~ ~ ~ ~[file] ~ ~ ~ ~)

28+ ?: ?=(%& -.dependency-result) ~[leaf+"forward open tag was accepted"]

29+ =/ dependency-expected=@t

30+ (of-wain:format ~['/ui/probe.jibb:4:6: nothing fixes the union of %add' '++ x %add' ' ^'])

31+ ?. =(dependency-expected message.p.dependency-result) ~[leaf+"dependency diagnostic order differs"]

32+ =/ shadow-source=@t (of-wain:format ~['++ inc |= n=@ud n' '++ before |= inc 0' '++ bad (inc %.y)'])

33+ =/ shadow-result (infer-jibb-file-detailed:jibb file shadow-source ~ ~ ~ ~[file] ~ ~ ~ ~)

34+ ?: ?=(%& -.shadow-result) ~[leaf+"shadowing sample was accepted"]

35+ =/ shadow-expected=@t

36+ (of-wain:format ~['/ui/probe.jibb:2:14: sample `inc` shadows a name already in scope' '++ before |= inc 0' ' ^'])

37+ ?. =(shadow-expected message.p.shadow-result) ~[leaf+"earlier sample shadow was masked"]

38+ =/ reversed-source=@t (of-wain:format ~['++ inc |= n=@ud n' '++ bad (inc %.y)' '++ x %add'])

39+ =/ reversed-result (infer-jibb-file-detailed:jibb file reversed-source ~ ~ ~ ~[file] ~ ~ ~ ~)

40+ ?: ?=(%& -.reversed-result) ~[leaf+"call mismatch was accepted"]

41+ =/ reversed-expected=@t

42+ (of-wain:format ~['++ bad: call\'s sample and argument types do not unify' '/ui/probe.jibb:2:9: called gate has type $-(@ud @ud)' '++ bad (inc %.y)' ' ^' '/ui/probe.jibb:2:13: argument has type ?' '++ bad (inc %.y)' ' ^'])

43+ ?. =(reversed-expected message.p.reversed-result) ~[leaf+"earlier mismatch was masked"]

44+ ~

45+--

tests/lib/jibb-full-scope.hoonnew file+37

@@ -0,0 +1,37 @@

1+:: The full checker reports the names and sites of module scope conflicts.

2+/+ jibb

3+|%

4+++ test-full-scope

5+ ^- tang

6+ =/ file=path /ui/probe/jibb

7+ =/ dup=@t (of-wain:format ~['++ foo 1' '++ foo 2'])

8+ =/ dup-result (infer-jibb-file-detailed:jibb file dup ~ ~ ~ ~[file] ~ ~ ~ ~)

9+ ?: ?=(%& -.dup-result) ~[leaf+"duplicate definition was accepted"]

10+ =/ dup-expected=@t

11+ (of-wain:format ~['definition `foo` shadows an earlier definition' '/ui/probe.jibb:1:1: earlier definition' '++ foo 1' '^' '/ui/probe.jibb:2:1: conflicting definition' '++ foo 2' '^'])

12+ ?. =(dup-expected message.p.dup-result) ~[leaf+"duplicate definition diagnostic differs"]

13+ =/ reserved=@t '++ proj 1'

14+ =/ reserved-result (infer-jibb-file-detailed:jibb file reserved ~ ~ ~ ~[file] ~ ~ ~ ~)

15+ ?: ?=(%& -.reserved-result) ~[leaf+"reserved definition was accepted"]

16+ =/ reserved-expected=@t

17+ (of-wain:format ~['`proj` is reserved and cannot be bound' '/ui/probe.jibb:1:1: reserved name' '++ proj 1' '^'])

18+ ?. =(reserved-expected message.p.reserved-result) ~[leaf+"reserved definition diagnostic differs"]

19+ =/ collision=@t (of-wain:format ~['/= foo /ui/other' '++ foo 1'])

20+ =/ collision-result (infer-jibb-file-detailed:jibb file collision ~ ~ ~ ~[file] ~ ~ ~ ~)

21+ ?: ?=(%& -.collision-result) ~[leaf+"definition shadowing import was accepted"]

22+ =/ collision-expected=@t

23+ (of-wain:format ~['definition `foo` shadows an import' '/ui/probe.jibb:1:1: import' '/= foo /ui/other' '^' '/ui/probe.jibb:2:1: conflicting definition' '++ foo 1' '^'])

24+ ?. =(collision-expected message.p.collision-result) ~[leaf+"import conflict diagnostic differs"]

25+ =/ prelude-source=@t '++ add |= n n'

26+ =/ iface=ifile:jibb [~ ~ /lib/jibb/prelude/jibb ~ ~ ~ `prelude-source ~]

27+ =/ shadows=@t '++ add 1'

28+ =/ shadow-result (infer-jibb-file-detailed:jibb file shadows ~ ~ ~ ~[file] ~[%add] ~ ~ `iface)

29+ ?: ?=(%& -.shadow-result) ~[leaf+"prelude shadow was accepted"]

30+ =/ shadow-expected=@t

31+ (of-wain:format ~['definition `add` shadows a prelude name' '/ui/probe.jibb:1:1: conflicting definition' '++ add 1' '^' '/lib/jibb/prelude.jibb:1:1: prelude declaration' '++ add |= n n' '^'])

32+ ?. =(shadow-expected message.p.shadow-result) ~[leaf+"prelude shadow diagnostic differs"]

33+ =/ nested=@t '++ test |=(proj proj)'

34+ =/ nested-result (infer-jibb-file-detailed:jibb file nested ~ ~ ~ ~[file] ~ ~ ~ ~)

35+ ?: ?=(%& -.nested-result) ~[leaf+"reserved sample was accepted"]

36+ ~

37+--

tests/lib/jibb-page-main.hoon+2

@@ -158,6 +158,8 @@

158158::

159159++ test-page-main

160160 ^- tang

161+ =/ hand-parsed (parse:jibb /ui/index/jibb (text hand-built-load))

162+ ?: ?=(%| -.hand-parsed) ~[leaf+"hand-built load fixture does not parse"]

161163 =/ negatives=(list [label=@t src=@t])

162164 :~ ['wrong static message' (text wrong-static)]

163165 ['arbitrary main' (text arbitrary-main)]

tests/type-page-main/hand-built-load.txt+2−2

@@ -2,9 +2,9 @@

22/= todo-list /ui/todo-list

44++ main (page load view)

5−++ load |=(~

5+++ load |= ~

66 ^- (ask (list item.todo))

7− [%agent api="/ui/api/todo" case=%todos agent=%todo path=~[%todos] scry=~ receive=receive])

7+ [%agent api="/ui/api/todo" case=%todos agent=%todo path=~[%todos] scry=~ receive=receive]

88++ receive |= input=[mark=@tas state=(unit *) fact=*]

99 ^- [state=* message=(list item.todo)] [state=0 message=~]

1010

tools/check+1

@@ -80,6 +80,7 @@ CHECKS = [

8080 for i in range(1, ARM_SHARDS + 1)

8181] + [

8282 Check('doc-blocks', 'eval', ['tools/doc-blocks', 'docs/spec']),

83+ tool('doc-fragments'),

8384 # The ship group. ship-selftest leaves its fixture files on the

8485 # jibb-dev desk, and ship-test, which syncs the desk to the repo

8586 # first, puts the real ones back, so it must come after.

tools/doc-fragmentsnew file+61

@@ -0,0 +1,61 @@

1+#!/usr/bin/env python3

2+"""Check that the fragments tested in module context match the doc cases."""

4+from pathlib import Path

5+import difflib

6+import sys

8+ROOT = Path(__file__).resolve().parent.parent

10+

11+def definitions(text):

12+ """Return top-level ++ definitions, including their indented bodies."""

13+ lines = text.splitlines(keepends=True)

14+ starts = [i for i, line in enumerate(lines) if line.startswith('++ ')]

15+ result = {}

16+ for i, start in enumerate(starts):

17+ end = starts[i + 1] if i + 1 < len(starts) else len(lines)

18+ name = lines[start].split()[1]

19+ if name in result:

20+ raise ValueError('duplicate definition: ' + name)

21+ result[name] = ''.join(lines[start:end]).rstrip('\n') + '\n'

22+ return result

23+

24+

25+def read(path):

26+ return (ROOT / path).read_text(encoding='utf-8')

27+

28+

29+def compare(label, expected, actual):

30+ if expected == actual:

31+ print('ok ' + label)

32+ return True

33+ print('FAIL ' + label)

34+ sys.stdout.writelines(difflib.unified_diff(

35+ expected.splitlines(keepends=True), actual.splitlines(keepends=True),

36+ fromfile='documented fragment', tofile='tested fragment'))

37+ return False

38+

39+

40+def main():

41+ try:

42+ core = read('tests/golden/doc-core-02-update/source.jibb')

43+ todo = definitions(read('my-app/ui/todo-list.jibb'))

44+ buttons = definitions(read('tests/golden/doc-grammar-02-buttons/source.jibb'))

45+ valid = read('tests/type-buttons/valid.txt')

46+ checks = [

47+ compare('Core update in todo-list', core, todo['update']),

48+ compare('valid buttons without add-button',

49+ ''.join(body for name, body in buttons.items()

50+ if name != 'add-button'), valid),

51+ ]

52+ if 'add-button' not in buttons:

53+ raise ValueError('documented buttons have no add-button definition')

54+ return 0 if all(checks) else 1

55+ except (OSError, UnicodeError, KeyError, ValueError) as e:

56+ print('doc-fragments: %s' % e, file=sys.stderr)

57+ return 2

58+

59+

60+if __name__ == '__main__':

61+ sys.exit(main())