Pyrefly fork for agents

pyrefly.md

Pyrefly: the deterministic side of tainie

Audience: the Pyrefly team, and anyone trying to understand why tainie forks Pyrefly. For the model side — evidence and asks for the Mellum team — see mellum.md.

---

Why — move reasoning out of the model, into the engine

A common agentic-coding task: "I renamed a parameter — now update every call site." Or: "We added a required field to a dataclass; fix every constructor." These are named-symbol fan-out edits: one structural change ripples across tens or hundreds of use-sites scattered through a codebase.

General-purpose coding agents handle this badly. They use grep, which finds too much (decoys, comments, unrelated names) and misses too much (type-resolved binding sites invisible to text search). They let the model decide scope, which is unreliable at scale. They verify with tests, which only catch value errors after the fact.

A small model makes this worse, not better. A 2.5B-active model is a strong local generator and a weak global reasoner. The more of the scope and correctness burden you put on it, the less reliable the whole loop becomes.

tainie's answer is a generate-and-verify split:

• Pyrefly finds the work and proves it correct. Discovery is type-resolved, not text-matched. Verification is type-checker gating, not tests.
• The model makes one bounded mechanical edit per site, never deciding scope.

Every fork change below obeys one principle: the verifier carries the correctness burden so the model doesn't have to. The smaller the model, the larger the win.

How — fork Pyrefly to fit the agent loop

From an orchestrator's perspective tainie is a three-parameter call — a workspace, a symbol, and an instruction. The orchestrator decides when tainie is the right tool; tainie handles everything in between, in one of two tiers:

• Deterministic tier (run_fanout, no model) — mechanical edits needing no judgment: field/parameter reference retargeting. Discovery → span-precise transform → forked pyrefly overlay-check of the whole candidate in memory → atomic commit. Nothing touches disk until the full candidate type-checks.
• Model tier (run_demo, Mellum per site) — uniform edits needing a little judgment: add a keyword argument. Discovery → one bounded edit per site → per-site type gate → commit.

Both tiers share one spine — Pyrefly finds, classifies, and proves; the model fills the hole:

1. Locate — Pyrefly's Glean exporter (pyrefly check --report-glean) emits XRefsViaNameByTarget facts: the exact type-resolved use-sites for the named symbol. No grep, no heuristics.
2. Edit — a deterministic span-precise transform, or a per-site Mellum micro-agent that sees one file, one line, and the instruction. It never sees the worklist or decides scope.
3. Verify — the deterministic tier assembles all edited files in memory and runs the forked pyrefly overlay-check in one transaction, writing only a fully-passing candidate. The model tier gates each site against a single-file pyrefly check.
4. Report — sites applied, skipped (with reasons), unreachable (unresolvable), and whether the gate passed.

The fork exists to make steps 1 and 3 possible: richer discovery facts and an atomic verification surface that stock Pyrefly does not expose.

What — the four fork areas

The fork (~/PycharmProjects/pyrefly, branch tainie-fork) adds four capabilities. The file-level manifest is the fork's TDOM.md; this section is the honest high-level surface (≈16 source files, not the "2 files" earlier drafts claimed).

1. overlay-check — atomic multi-file verification

A non-interactive batch surface for "check this candidate edit set without touching disk." Takes a JSON edit-set, swaps it in via Transaction::set_memory, runs a full-project check in memory, and returns the new diagnostics (optionally diffed against a --baseline). Lives in pyrefly/lib/commands/check.rs (~221 lines for run_with_overlay + OverlayCheckArgs) plus load-bearing overlay plumbing in pyrefly/lib/state/{load,memory,state}.rs — the most divergent, least-upstream-aligned part of the fork. It turns the gate from "is this one file still OK?" into "is this atomic edit set still OK?" and makes failed retries pure computation. (Fork-side coverage: pyrefly/tests/overlay_check.rs.)

2. Glean xref exports

Five new xref paths, all emitted into the existing XRefsViaNameByTarget fact (no new fact type, no consumer change), in pyrefly/lib/report/glean/convert.rs (+ mod.rs):

1. keyword → constructor field (Complaint(agent_name=...) → Complaint.agent_name)
2. keyword → function/method parameter (render(verbose=True) → render.<locals>.verbose)
3. keyword → TypedDict field
4. positional argument → parameter (render("x", True) → render.<locals>.verbose)
5. structural Protocol implementors (same-module, via the existing subtype oracle)

Together these make field rename, parameter rename, and change-signature into type-resolved worklists that grep cannot produce.

3. tdom t-string component type-checking

pyrefly/lib/alt/tdom.rs (~372 lines) — the largest area and the one least likely to upstream as-is, since it is tdom-specific. It type-checks PEP 750 HTML-component t-strings (html(t'<{Heading} name={x}>...')) as ordinary keyword calls by synthesizing a call from the interpolation expressions and feeding it to the existing inference engine, so every argument error lands on the right source span. Purely additive — standard t-strings are unaffected.

4. assert_never exhaustiveness gate

pyrefly/lib/alt/special_calls.rs + crates/pyrefly_{config,types} adds a distinct error kind assert-never (ErrorKind::AssertNever, default Severity::Error) that fires when an assert_never(x) arg is reachable (!is_never() && !is_any()). This catches non-exhaustive matches on frozen-dataclass and pydantic discriminated unions — richer subjects than the stock non-exhaustive-match (enum/Literal only, default Warn), which the fork does not change. See concepts/spm.md for the full capability map.

Maintenance posture

The fork is a one-way snapshot, not a tracked rebase: merge-base 99c080b, 15 commits ahead / 134 behind facebook/pyrefly (as of 2026-06-29). Permanent divergent carry is concentrated in alt/tdom.rs and the state/{load,memory,state}.rs overlay plumbing. Posture: accept divergence; rebase only when upstreaming a specific piece. The CWD-relative Glean path behavior is upstream-by-design; tainie resolves paths against the repo root to account for it (documented at the fork's file_fact).

Next — asks to the Pyrefly team

Ranked by leverage for SLM-driven agentic coding:

1. Upstream the overlay-check surface (highest leverage) — accept it as a first-class command. ~221 lines of adapter on machinery that already works in the LSP path; today it carries merge-conflict cost against check.rs + state/.
2. Reference-kind tags on xrefs — tag each xref def | import | call | attribute-read | keyword-arg | parameter | …. Lets tainie drop the O(refs) source re-read and route the correct transform per kind.
3. Upstream the positional argument-slot export — completes change-signature; reuses matching call.rs already computes; no new fact type.
4. Completeness certificate (prove-complete) — expose Pyrefly's implicit "did we find them all?" signal as a queryable proof.
5. Edit-invariant diagnostic identity — anchor diagnostics to a stable semantic id so edits don't shift (path, line, col) and overlay checks compose.
6. Untyped-reach / blind-spot signal — alongside resolved xrefs, emit a lexical-candidate set (name appears but is outside the type graph), clearly labeled, so a silent blind spot becomes a machine-readable hand-off list.
7. Canonicalize overlay input paths — ✅ fixed in fork (246f66c). On macOS a symlink-form overlay key (/tmp/…) missed the canonical handle (/private/tmp/…) and the file was silently checked against disk — an undetectable false-green. The fork now canonicalizes at the input boundary. Upstream ask: accept the fix.
8. Error on orphaned overlay entries — ✅ fixed in fork (80c92aa). An overlay entry matching no project handle was silently discarded (another false-green, with no client-side workaround). The fork now bail!s on existing-but-unmatched paths. Upstream ask: accept the fix.

Model-tier asks (Mellum team and Mellum 2.1 training properties) live in mellum.md.