Branch: tainie-fork
Implementation-level notes for the four fork areas: tdom t-string checking,
overlay-check, Glean xrefs, and the assert_never exhaustiveness gate. The
narrative why / how / what (and the asks to the Pyrefly and Mellum teams) lives
in tainie's docs/pyrefly.md; this file is the file-level manifest.
Type-check tdom HTML-component t-string syntax as ordinary Python keyword calls.
Make Pyrefly type-check the tdom HTML-component calling syntax embedded in a Python 3.14 t-string as if it were an ordinary Python keyword call.
def Heading(*, name: str, children: tuple = ()) -> Element: ...
name = "world"
html(t'<{Heading} name={name}>The children</>') # -> check as Heading(name=name, children=...)
html(t'<{Heading} name={123}>x</>') # -> error: int not assignable to str
html(t'<{Heading}>x</>') # -> error: missing required arg `name`For t'<{Comp} attr1={v1} attr2="lit" flag>children</>':
- The first interpolation in tag position (
<{Comp}) is the callable. - HTML attributes become keyword-only arguments:
attr={expr}->attr=exprattr="lit"->attr="lit"(string literal)- bare
flag->flag=True {...spread}->**spread
- Attribute names are kebab-case -> snake_case (
data-foo->data_foo). - Children (content between open/close tags) are passed as
children=tuple(...)only if the callable declares achildrenparameter or**kwargs. - All arguments are passed keyword-only; components may not require positional
args. Unknown attributes are silently dropped unless the callable has
**kwargs; missing required params raise at runtime. - Self-closing
<{Comp} .../>passes no children. - Close tag may be
</{Comp}>or shorthand</>.
Note: tdom's runtime silently drops unknown attrs (no **kwargs). The checker
instead reports unexpected-keyword (JSX/TS excess-property style) — stricter on
purpose, but a genuine behavioral divergence.
This mirrors how the TypeScript compiler checks JSX (checkJsxOpeningLikeElement):
it never emits/rewrites JSX before checking — it derives a call signature and
checks attributes against it with the normal assignability engine.
Key insight: the interpolation expressions inside a t-string are already real
ruff_python_ast::Expr nodes with real source spans. We construct a synthetic
ExprCall reusing those nodes and feed it to the existing expr_call_infer. Every
argument type error lands on exactly the right source span for free. Zero new
type-system code.
A t-string arrives pre-split into static string parts interleaved with interpolation holes. We walk the static parts as a minimal HTML tokenizer; at each hole the current state classifies it:
- right after
<→ hole is the component callable - in attribute-value position → hole is a kwarg value
- text/child position → child (inferred but not passed to the call)
Attribute names come from the literal text. Tag detection follows the HTML5
tokenizer rule: < is a tag opener only if immediately followed (no whitespace)
by {Hole}, /, ASCII alpha, or !. A bare < (as in a < b) is NOT a tag
opener, preventing text comparisons from swallowing sibling components.
- Attribute interpolations checked as kwargs:
name={123}→ wrong-type error. - Missing required attribute →
Missing argument. - Unknown attribute →
Unexpected keyword argument. - kebab-case → snake_case (
data-id→data_id). - Literal string attributes (
kind="primary") and bare boolean flags (disabled→True). - Dataclass components:
<{Card} .../>checked asCard(...)constructor call. - Sibling and nested components all type-checked in a single pass.
- Error spans point at the offending interpolation, not the t-string start.
- Non-component t-strings keep
Templatetyping.
tdom's _invoke_component passes children=tuple(...) whenever the callable
declares a children parameter or has **kwargs. The checker mirrors this:
accepts_children inspects the resolved callee signature (classes lowered to their
constructor via constructor_to_callable, so dataclass components work) and checks
for a keyword-passable children parameter or **kwargs. When present, a synthetic
children=() keyword is appended to the call before expr_call_infer.
children=() (empty tuple) is assignable to every realistic variadic children
annotation (tuple[Node, ...], Sequence[Node], …) without needing to model
tdom's Node type. The synthetic ExprTuple uses TextRange::empty(TextSize::new(0))
as its range to avoid clobbering the callable's LSP type-trace entry.
- Unknown attribute → error. tdom silently drops; we report
unexpected-keyword. - Unquoted/literal attribute typed as
str.count=3is a string in HTML; usecount={3}for a typed integer value.
- Spreads (
{**attrs}): the tokenizer stops at a hole in attribute-name position; the spread is neither expanded nor checked. - Child content types: child interpolations and nested components are inferred
on their own; their types are not validated against the
children=annotation. - Intrinsic (lowercase) tags (
<div>): kept asTemplate.
All logic lives in pyrefly/lib/alt/tdom.rs. Net footprint against main:
pyrefly/lib/alt/tdom.rs— new file, ~290 linespyrefly/lib/alt/expr.rs—Expr::TStringarm callsself.check_tdom_components(...)(+12/−3 lines)pyrefly/lib/alt/mod.rs— +1pub mod tdom;pyrefly/lib/test/mod.rs— +1mod tdom_components;
cargo test -p pyrefly tdom_components
cargo build -p pyrefly --bin pyrefly
./target/debug/pyrefly check --preset all --python-version 3.14.0 <file>.py
In-memory multi-file diff-against-baseline type check for transactional edits.
Enable an agent (tainie or similar) to declare a multi-file edit set, verify that the whole set type-checks as a unit, and get a pass/fail verdict — without touching the working tree.
A refactor that spans multiple files cannot be validated file-by-file: intermediate states (after editing file A but before editing file B) are type-incorrect by design. The check needs to see all files in their post-edit state simultaneously.
A new overlay-check subcommand accepts a JSON file mapping each path to its
post-edit text. It:
- Converts listed files from filesystem handles to in-memory handles (so they
pick up the
set_memoryinvalidation). - Captures a baseline of pre-edit diagnostics per file.
- Applies all overlays atomically via the existing
set_memorypath. - Runs a full-project type check.
- Diffs post-edit diagnostics against the baseline per file.
- Returns a single pass/fail verdict: pass iff no new errors appear in any file.
Files reached transitively via import still use filesystem handles; the overlay
flag tells load_from_path to consult the overlay for those transitive imports.
pyrefly/lib/commands/overlay_check.rs— new subcommand entry pointpyrefly/lib/commands/check.rs—OutputArgsandBehaviorArgsmadepub(crate); overlay check logicpyrefly/lib/commands/all.rs—OverlayCheckvariant wired into the command enumpyrefly/lib/state/load.rs— overlay-awareload_from_pathpyrefly/lib/state/memory.rs— extended in-memory file managementpyrefly/lib/state/state.rs— multi-file overlay application
- New files not on disk are not added to the check set (project discovery runs against on-disk files).
- Config file changes in the overlay are ignored (config loading runs against on-disk config).
Export call-site keyword-argument cross-references into Glean facts, enabling field/parameter discovery for rename and change-signature IDE actions.
A call like Complaint(agent_name="bob") has no value-position read of
agent_name (it's a string literal keyword), so it produced zero Glean evidence.
Similarly, render_report(verbose=True) gave no xref from verbose to the
parameter declaration. Field and parameter renames could silently miss these
sites.
All four paths emit xrefs into the existing XRefsViaNameByTarget fact that
consumers already read; no new fact types, no consumer changes.
For Complaint(agent_name=...), the type trace at the call range is
type[Complaint]. Each keyword name is resolved as an attribute of the
constructed instance via find_definition_for_typed_attribute. The xref source
span is the keyword identifier — the rename edit site that was previously
invisible. Covers @dataclass fields and plain __init__ attributes.
For render_report(verbose=True), the callee is resolved to its function type via
normalize_singleton_function_type_into_params. Each keyword matching a
keyword-passable parameter (Pos | KwOnly) emits an xref to
<callee>.<locals>.<param> — byte-identical to the parameter declaration's own
FQN, so a tainie query keyed on a parameter now returns both in-body references
and keyword call sites. Class constructors no-op here (handled by path 1).
TypedDict construction Config(port=...) is not to_callable, so it falls
through both prior paths. Fix: when the call-result type is a named TypedDict,
read the field set from typed_dict_fields, resolve the callee FQN, and emit
{callee_fqn}.{field} — the same FQN a field declaration carries.
positional_arg_xrefs complements the keyword path: for each non-keyword,
non-starred argument at position i, resolve the callee's parameter list and emit
an xref from the argument span to <callee>.<locals>.<param>. A starred (*rest)
arg stops position mapping (subsequent positions are statically unknowable).
Combined with path 2, tainie now discovers all call sites for a named parameter
regardless of argument style.
When a free function's return type happens to have an attribute matching the
keyword name — e.g. add_complaint(agent_name=...) -> Complaint where
Complaint.agent_name exists — the attribute lookup (path 1) would falsely link
the keyword to the field instead of the parameter. Fix: path 1 gates on the callee
NOT introspecting as a function (normalize_singleton_function_type_into_params
returning None), matching the existing constructor/function split.
Top-level classes in a module are checked against all top-level Protocols in the
same file using the existing is_subset_eq subtype oracle (via ad_hoc_solve).
Structural conformances are merged into the class's ClassDefinition.bases list —
the same field nominal subclasses already populate — so protocol implementors
surface through the existing inheritance query with no new fact type and no
consumer change. Bounded to same-module to keep the check cheap.
pyrefly/lib/report/glean/convert.rs—keyword_argument_xrefs,keyword_parameter_xrefs,keyword_typeddict_xrefs,positional_arg_xrefs,compute_structural_bases, fix for function-call guardpyrefly/lib/report/glean/testdata/— new fixtures + snapshots
- TypedDict subscript access
cfg["port"]is not covered (string literal in subscript, not a keyword; needs a separate path). - Cross-module structural Protocol implementors are not found (per-module bound).
- Generic and overloaded callees no-op for the parameter paths.
Motivation: pyrefly did not flag assert_never(x) when x was not Never, so
case _: assert_never(x) in a non-exhaustive match passed silently. This is the
static guarantee behind Principle 18 in tainie's PRINCIPLES.md.
Implementation: Five-file change (~87 lines net).
crates/pyrefly_config/src/error_kind.rs— addedAssertNevererror kind (defaults toSeverity::Error).crates/pyrefly_types/src/callable.rs— addedFunctionKind::AssertNevervariant withfrom_name,module_name,function_name, andclassarms all mapped totyping::assert_never.pyrefly/lib/alt/special_calls.rs—call_assert_never(): infers the single arg, checksis_never(), emitsErrorKind::AssertNeverif not Never, returnsType::never().pyrefly/lib/alt/call.rs— dispatch armCalleeKind::Function(FunctionKind::AssertNever)→call_assert_never().pyrefly/lib/test/narrow.rs— two new test cases:test_assert_never_non_exhaustive_match(expects error) andtest_assert_never_exhaustive_match(expects clean).
Verified:
cargo buildclean (316 crates compiled).cargo test assert_never→ 4 passed (2 new + 2 pre-existing enum cases).- Smoke test non-exhaustive:
pyrefly check --preset default /tmp/test_assert_never_match.py→ERROR assert_never(str) failed: argument is not \Never` [assert-never]at theassert_never(x)` call site. - Smoke test exhaustive: both arms covered → 0 errors.
- Smoke test direct:
x: str = "hello"; assert_never(x)→ same error fires.
Open:
- The
basicpreset silencesAssertNever(as it does all non-allowlisted kinds) — to get the error in unconfigured projects, users must explicitly enable it or use--preset default. Consider addingAssertNeverto the Basic preset's allowlist as a high-confidence diagnostic. - No snapshot-test update was needed; the testcase macro evaluated the
# E:annotations correctly.
Problem: When the residual type inside the case _: arm degrades to Any/Unknown
(e.g. a union member from an unresolved import), is_never() is false, so assert_never
fired — a false positive coupled to import resolvability. The typing convention
(mypy/pyright) is that Any is gradually consistent with Never, so assert_never(Any)
must NOT error.
Fix: call_assert_never() now emits only when !arg_ty.is_never() && !arg_ty.is_any().
Type::is_any() matches Type::Any(_) (all AnyStyle variants, incl. the Error/Unknown
style from unresolved imports). This mirrors narrow.rs check_match_exhaustiveness
(line ~2180: remaining_ty.is_never() || remaining_ty.is_any()), keeping the two
exhaustiveness paths consistent.
Verified: new test test_assert_never_any_residual_no_error (int | Any subject,
wildcard arm, expects clean) + cargo test assert_never → 5 passed. Smoke under
--preset default: int | UnresolvedThing match → ONLY [missing-import], NO
[assert-never]; genuine non-exhaustive int | str → STILL fires [assert-never]
(no over-suppression).
assert_never (this fork) catches non-exhaustive matches on richer subjects than stock
non-exhaustive-match:
- frozen-dataclass discriminated unions — single- and multi-variant residuals.
- pydantic discriminated unions — single- and multi-variant residuals.
Stock non-exhaustive-match only covers enum / Literal subjects; it does not flag
incomplete matches over dataclass/pydantic class unions. So the case _: assert_never(x)
pattern is the only static guard for those subjects.
| Error kind | Default severity | Visible under --preset default? |
Under basic / no config? |
|---|---|---|---|
assert-never (this fork) |
error | yes (ERROR) | silenced (allowlist) |
non-exhaustive-match (stock) |
warn | hidden (N warning not shown) |
silenced |
To surface non-exhaustive-match / unreachable-match-case reliably, promote them to
error severity in pyrefly.toml (see config schema below).
ConfigBase.errors is Option<ErrorDisplayConfig>, where ErrorDisplayConfig wraps
HashMap<ErrorKind, Severity>. TOML table name is [errors] (field is literally errors;
no rename). Keys are the kebab-case error-kind names (ErrorKind is
#[serde(rename_all = "kebab-case")], exposed via to_name()). Values are either a
lowercase severity string (Severity is #[serde(rename_all = "lowercase")]:
"error", "warn", "info", "ignore") or a bool (true = enable, false = ignore).
# pyrefly.toml
[errors]
non-exhaustive-match = "error"
unreachable-match-case = "error"Equivalent under pyproject.toml:
[tool.pyrefly.errors]
non-exhaustive-match = "error"
unreachable-match-case = "error"Verified against the built binary: with the [errors] stanza above, an enum match missing
a variant surfaces as ERROR ... [non-exhaustive-match] instead of the default hidden warning.
This is a one-way snapshot fork, not a tracked rebase. As of 2026-06-29:
merge-base 99c080bec, 15 commits ahead / 134 behind facebook/pyrefly
origin/main. Posture: accept divergence; rebase only when upstreaming a
specific piece.
Permanent divergent carry (the pieces least likely to upstream as-is):
pyrefly/lib/alt/tdom.rs(~372 lines) — tdom-specific, the largest area.pyrefly/lib/state/{load,memory,state}.rs— overlay plumbing foroverlay-check; load-bearing and entangled with mainline state handling.
Upstreaming candidates (cleaner to land): overlay-check
(pyrefly/lib/commands/check.rs + overlay_check.rs) and the
positional-argument xref export (pyrefly/lib/report/glean/convert.rs). See
tainie's docs/pyrefly.md "Next" for the framed upstream asks.
overlay-check now canonicalizes overlay input paths (ask #7) and bails on
orphaned overlay entries (ask #8); see pyrefly/tests/overlay_check.rs for the
fork-side coverage.