Skip to content

Instantly share code, notes, and snippets.

@pauleveritt
Created June 30, 2026 16:17
Show Gist options
  • Select an option

  • Save pauleveritt/d61c042f259a3a2620f9be4c798ae3cb to your computer and use it in GitHub Desktop.

Select an option

Save pauleveritt/d61c042f259a3a2620f9be4c798ae3cb to your computer and use it in GitHub Desktop.
tdom handling in Pyrefly

Pyrefly Fork Changes (tainie-fork)

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.


TDOM Support

Type-check tdom HTML-component t-string syntax as ordinary Python keyword calls.

Goal

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`

tdom component-call semantics (from tdom processor.py::_invoke_component)

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=expr
    • attr="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 a children parameter 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.

Design: synthesize a call, don't rewrite source

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.

Parsing approach

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.

What works (28 tests in pyrefly/lib/test/tdom_components.rs)

  • 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-iddata_id).
  • Literal string attributes (kind="primary") and bare boolean flags (disabledTrue).
  • Dataclass components: <{Card} .../> checked as Card(...) 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 Template typing.

Children handling

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.

By-design divergences

  • Unknown attribute → error. tdom silently drops; we report unexpected-keyword.
  • Unquoted/literal attribute typed as str. count=3 is a string in HTML; use count={3} for a typed integer value.

Remaining gaps

  • 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 as Template.

Module isolation

All logic lives in pyrefly/lib/alt/tdom.rs. Net footprint against main:

  • pyrefly/lib/alt/tdom.rs — new file, ~290 lines
  • pyrefly/lib/alt/expr.rsExpr::TString arm calls self.check_tdom_components(...) (+12/−3 lines)
  • pyrefly/lib/alt/mod.rs — +1 pub mod tdom;
  • pyrefly/lib/test/mod.rs — +1 mod tdom_components;

How to reproduce

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

Overlay Check

In-memory multi-file diff-against-baseline type check for transactional edits.

Goal

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.

Problem

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.

Design

A new overlay-check subcommand accepts a JSON file mapping each path to its post-edit text. It:

  1. Converts listed files from filesystem handles to in-memory handles (so they pick up the set_memory invalidation).
  2. Captures a baseline of pre-edit diagnostics per file.
  3. Applies all overlays atomically via the existing set_memory path.
  4. Runs a full-project type check.
  5. Diffs post-edit diagnostics against the baseline per file.
  6. 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.

Files changed

  • pyrefly/lib/commands/overlay_check.rs — new subcommand entry point
  • pyrefly/lib/commands/check.rsOutputArgs and BehaviorArgs made pub(crate); overlay check logic
  • pyrefly/lib/commands/all.rsOverlayCheck variant wired into the command enum
  • pyrefly/lib/state/load.rs — overlay-aware load_from_path
  • pyrefly/lib/state/memory.rs — extended in-memory file management
  • pyrefly/lib/state/state.rs — multi-file overlay application

Known limitations (documented in args)

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

Glean Xrefs

Export call-site keyword-argument cross-references into Glean facts, enabling field/parameter discovery for rename and change-signature IDE actions.

Problem

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.

Solution: four new xref paths (all via XRefsViaNameByTarget.4)

All four paths emit xrefs into the existing XRefsViaNameByTarget fact that consumers already read; no new fact types, no consumer changes.

1. Keyword → constructor field (f792e360f)

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.

2. Keyword → function/method parameter (20052e360)

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

3. Keyword → TypedDict field (c97af46a5)

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.

4. Positional argument → parameter (0d5c1fa90)

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.

Fix: attribute path must not fire for function calls (ad50f00ff)

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.

5. Structural Protocol implementors (c785e241f)

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.

Files changed

  • pyrefly/lib/report/glean/convert.rskeyword_argument_xrefs, keyword_parameter_xrefs, keyword_typeddict_xrefs, positional_arg_xrefs, compute_structural_bases, fix for function-call guard
  • pyrefly/lib/report/glean/testdata/ — new fixtures + snapshots

Honest remainder

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

assert_never exhaustiveness check (feature/assert-never)

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 — added AssertNever error kind (defaults to Severity::Error).
  • crates/pyrefly_types/src/callable.rs — added FunctionKind::AssertNever variant with from_name, module_name, function_name, and class arms all mapped to typing::assert_never.
  • pyrefly/lib/alt/special_calls.rscall_assert_never(): infers the single arg, checks is_never(), emits ErrorKind::AssertNever if not Never, returns Type::never().
  • pyrefly/lib/alt/call.rs — dispatch arm CalleeKind::Function(FunctionKind::AssertNever)call_assert_never().
  • pyrefly/lib/test/narrow.rs — two new test cases: test_assert_never_non_exhaustive_match (expects error) and test_assert_never_exhaustive_match (expects clean).

Verified:

  • cargo build clean (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.pyERROR 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 basic preset silences AssertNever (as it does all non-allowlisted kinds) — to get the error in unconfigured projects, users must explicitly enable it or use --preset default. Consider adding AssertNever to the Basic preset's allowlist as a high-confidence diagnostic.
  • No snapshot-test update was needed; the testcase macro evaluated the # E: annotations correctly.

Refinement — ignore Any/Unknown residual (commit de508ce)

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

Verified capability summary

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.

Preset / severity gotcha

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

Config schema — promoting an error kind to error severity

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.


Maintenance posture

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 for overlay-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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment