Steven Troxler

Replace `Unique` with `QuantifiedIdentity` in `Quantified` (plumbing) Summary: `Quantified` previously used `Unique` (an allocation-order counter) as its identity. This is nondeterministic: the same type variable gets a different identity on every run, making union ordering, hashing, and caching nondeterministic across processes. This commit replaces `unique: Unique` with `identity: QuantifiedIdentity`, a struct of `(module: ModuleName, anchor: TextRange, slot: QuantifiedSlot, ordinal: u32)`. Identity is now fully deterministic and derived from source locations. `QuantifiedSlot` discriminates construction origin to prevent collisions between different kinds of quantifieds that happen to share an anchor range: `ScopedLegacy` (legacy TypeVar), `Pep695` (new-style `[T]` params), `SyntheticSelf` (`__new__` cls binder), and `SyntheticCallableResidual` (TypeVarTuple instantiation helpers). `TypeEqCtx` gains a `quantified_identity: SmallMap<QuantifiedIdentity, QuantifiedIdentity>` field for alpha-equivalence comparison of `Forall`-bound quantifieds, using the same first-pairing-wins pattern as the existing `Unique` map for `Var`. For PEP 695 type params, the parameter's own identifier range is the anchor (naturally unique per file). For legacy TypeVars (commit 2 will improve this), the TypeVar's qname range serves as a placeholder anchor with `ScopedLegacy` slot. Synthetic quantifieds use the owning class range or `TextRange::default()` with distinct ordinals. Reviewed By: rchen152 Differential Revision: D102088816 fbshipit-source-id: 5abcd1711f901e149adad19beca3fe03abc8f084

Plug user-reachable panics in the DSL evaluator Summary: Audit of most eval_dsl_expr / eval_dsl_body / eval_call / eval_binop for panic sites that can be triggered by user-authored shape_dsl_function definitions (as opposed to IR bugs or internal assertions), and fix each one. The idea here is to get reasonable behavior, not panics, when a DSL function is misused in a way that we somehow miss during the type checking phase. Ideally, this would never occur - we validate the DSL ahead of time, so only a bug in Pyrefly would actually make the code reachable (hence no unit tests), but sooner or later we probably will encounter a failure to validate the DSL (i.e. a soundness bug) at which point this change should make it easier to understand what went wrong. This is best-effort and a couple of panics remain where this is much more convenient, which is probably fine - again this is just to make debugging easier if we encounter problems in the future Reviewed By: rchen152 Differential Revision: D106003742 fbshipit-source-id: 1220f1322ee3663a76a0112791b5a834bb6df1bf

Gate residual reads by outermost expansion var Summary: **This stack** Adds a "callable residual" type that allows us to capture structure when a generic or overloaded callable is passed to a higher-order function. The residuals can later be "exploded" to recover generic and overload structure in outputs (either Callable outputs, or classes whose methods capture the callable structure of an argument - e.g. callback protocol classes). The full design details are [here](https://github.com/stroxler/pyrefly-docs/tree/main/callable-residuals) **This diff** Thread the outermost query var through expand-time recursion and only expose payloads when that query var is in ; non-target reads flatten residuals to their precomputed fallback. All reads of solver `variables` map go through this check - if two vars got unified via `union-find` but one of them isn't actually part of a comparsion that can produce residuals (like comparing a generic callable argument with a callable parameter in a higher-order function), then we will prevent the residual from appearing in the result and instead we will just flatten to a plain fallback type. The relevant read points are: - expand_var - record_recursive - is_subset_eq when we look up answers This allows us to cleanly enforce boundaries where residual types get flattened; without it, and expand call could potentially produce a residual somewhere where we aren't expecting it. This is only necessary becuase the current union-find algorithm conflates variables rather than setting bounds between them, and as a result the residuals can appear in places they don't belong; if we do a major refactor of the solver in the future this can go away. Reviewed By: rchen152 Differential Revision: D102011864 fbshipit-source-id: 68e1e4bbae4c39d1d7cb862bcd826bfb9f646b92

Serialize SCC member writes with write-lock ownership so only one thread will win Summary: We observed races where one thread could read partially-interleaved writes from another thread while SCC members were being committed, producing inconsistent answers. This change makes SCC commit use a consistent write-lock ownership phase so one thread owns all writable members before publishing results, preventing cross-thread interleaving between reads and writes. The locking happens in CalcId sort order, which will be the same across threads. As a result, it should be impossible for two threads computing the same Scc to interleave writes, since they will try to acquire locks in the same order. In theory, overlapping Sccs are possible because graphs are dynamic (edges depend on Answers) and discovery is entrypoint-dependent. If that occurs, the winning thread will own all of the bindings in *its* Scc, but anything in the other thread alone will get written after the locks are released. It is unknown whether this can occur in practice, we only know that the general properties of dynamic graph traversal cannot fully rule it out. Reviewed By: rchen152 Differential Revision: D95079384 fbshipit-source-id: 3874e3979178c893376e94a6ee759117c5940128

Type var resolution must be idempotent: add a unique cache to Quantified logic Summary: With iterative solving, we have a problem where as we iterate a fixpoint we'll evaluate the same binding multiple times. We need the result to be idempotent when there's no actual semantic change going on; for the most part this is true, `Type` is structurally equal when it is semantically equal. But legacy type var handling means there's a unique in `Quantified`, and that unique is part of structural equality. So to be idempotent, we need to make sure that the same binding, evaluated in an exactly equivalent semantic way, should produce a result with the same unique. We can do this by creating a cache of the uniques, keyed on information that is stable across threads and iterations. ------- Note: I originally thought that idempotence was only relevant when two different threads raced to spit out answers for the same Scc, which is already a problem and fixed more generally in the next diff D95079384. But after thinking this through with some agents' help I realized it's an issue for iterating even within a single Scc, because due to the use of previous-iteration values for recursion-breaking we could mix two different "generations" of the same `Quantified` in computations, and having non-idempotent `unique` values would cause problems. ------- Note: I also realized when cleaning up tech debt in the original agent implementation that there are additional places we create Quantified that aren't covered by this fix. They don't seem to *currently* come up prominently in determinism checks, but they probably present risk. I'll stack a diff later to cut them all over to also using a cache, because we really need *all* bindings to be idempotent. Basically, all the places where we are blindly passing a `fresh()` down are potentially non-idempotent. This is the only callsite that happened to come up in the mypy primer results I was looking at, and it's easier to fix the one relevant site first, but I'll patch the rest up later in the stack. Reviewed By: rchen152 Differential Revision: D94402210 fbshipit-source-id: a15997d03a21dcb8d0ce199be403039e552804cc

convert __static__ contextual-type tests to expect-test format Summary: Also delete test_literal_promoted_type: it is already covered by the existing test_fixture_literal_type fixture (x = 42 produces Literal[42] -> builtins.int in the readable output). Expect-style tests verify more about the output in a human-readable way, and this way of setting up tests is much better for quick TDD iteration on actual examples where cinderx/pyrefly integration hits bugs Reviewed By: DinoV Differential Revision: D97672079 fbshipit-source-id: 5037038fc7c794da8783ab27c846a09d5059f3cb

Add solver residual-answer plumbing scaffolding Summary: **This stack** Adds a "callable residual" type that allows us to capture structure when a generic or overloaded callable is passed to a higher-order function. The residuals can later be "exploded" to recover generic and overload structure in outputs (either Callable outputs, or classes whose methods capture the callable structure of an argument - e.g. callback protocol classes). The full design details are [here](https://github.com/stroxler/pyrefly-docs/tree/main/callable-residuals) **This diff** Why: Residual-aware solving needs explicit solver-side slots for residual metadata and visibility-gated answers, but we want to introduce that structure without changing solving behavior yet. What: Add Bounds residual metadata storage, ResidualIdentity scaffolding, and Variable::ResidualAnswer, while keeping all solver flows that read solved vars treating ResidualAnswer like Answer for now. Why it works: The solver can now carry residual-oriented state through existing pathways without behavioral shifts, preparing follow-up commits to add capture, gating, and flattening semantics incrementally. Reviewed By: rchen152 Differential Revision: D102011885 fbshipit-source-id: a1b9f57a46f44d8357d81c9de50c34b215f3f00a

switch pruning to call-context witness payloads Summary: Overload pruning at call finishing should use call-context witness payloads so pruning still works even when quantified vars are solved to concrete answers before finishing. This commit introduces call-context payload and deferred-var storage, threads that state through context-scoped solver mutations, records overload probe captures into payload storage, and updates call-boundary finishing to consume payloads as the authoritative pruning source while keeping non-call finishing on variable-backed residuals. It also preserves call-site contextual typing by routing call-argument expression checks through a hint-aware call-context expression path, and includes conformance expectation updates for resulting diagnostic location shifts. Reviewed By: rchen152 Differential Revision: D103290898 fbshipit-source-id: 021c4ae8f49756b4489e077e0f114ec693a37a6f

Add public shape-DSL wrapper API in pyrefly_types (#3480) Summary: Pull Request resolved: https://github.com/facebook/pyrefly/pull/3480 **This stack** Reworks tensor shape operations so that instead of being hardcoded in tensor_ops_registry.rs, only DSL primitives are directly hardcoded into Pyrefly; the actual operations and the association with "normal" (non DSL) stubs all lives in user-space stub files. This allows iterating on the ops without rebuilding Pryefly, and is 100% essential for actually building out full stubs for pytorch (and even more so if we want to extend to other libraries like numpy and jax). The DSL itself is unchanged but we will use a decorator to indicate when a stub function is a DSL function; we use a different decorator to actually register a DSL function as the "shape transform" associated with some normal function (e.g. to associate the DSL function `reshape_ir` with a `torch.reshape` function). Details of the plan are in https://github.com/stroxler/pyrefly-docs/blob/main/tensor-shapes-in-stubs/v2-doc.md **This commit** The next step of tensor-shapes-in-stubs migration. Adds a public surface to `pyrefly_types::meta_shape_dsl` that lets later phases (the binder and solver in `pyrefly/lib`) drive the DSL pipeline without exposing the grammar-aligned `DslFnDef` internals. The new surface: - `ShapeDslFunction` — an opaque, cheap (one `Arc`) handle to a single DSL function lowered from its Python AST. - `ShapeDslProgram` — a bundle of `ShapeDslFunction`s that has been validated together as a program. The only way to obtain one is via `build_shape_dsl_program`, which type-checks the bundle. - `convert_shape_dsl_function` — AST → `ShapeDslFunction`. - `build_shape_dsl_program` — `Iterator<ShapeDslFunction>` → `ShapeDslProgram`. Panics on type-check failure today, matching the existing `parse_dsl` semantics; Phase 7 of the migration will convert this to a `Result` and surface diagnostics. - `make_meta_shape_function` — `(&ShapeDslProgram, root_name)` → `Box<dyn MetaShapeFunction>`. Taking a `&ShapeDslProgram` (not raw pieces) enforces that callers cannot build a `MetaShapeFunction` from un-type-checked DSL. The internal helpers (`convert_fndef`, `type_check_program`, `bind_dsl_params`, `eval_dsl_body`) stay module-private; the wrappers live in the same module and call them directly. This keeps DSL internals fully opaque outside the module. No call sites change in this commit; the new API is exercised by the follow-up dogfood refactor of `tensor_ops_registry`. Reviewed By: yangdanny97 Differential Revision: D105720303 fbshipit-source-id: 63ce4fcb79abf1964b29f29d11e96ae0869b4837

Introduce new `range_with` method to `Keyed` Summary: I realized while working on iterative fixpoint that we have an rely on `Ranged` for `Key`, but in fact most of our `Key.*` types don't have a real range, they use dummy ranges. This is not type-safe - it's a lie to the rust type checker, and we are actively lying to our own codebase because if you actually use these ranges, you will always produce 100% unacceptable UX - error messages that have no trace of actual code locations, and on top of that can't be suppressed. It's a disaster waiting to happen. And implementing fixpoint means we can get convergence failures at any key/binding pair, so we're very much exposed to this. We have to fix it. The problem is that it's actually not very convenient or safe to actually make all `Key.*` types ranged, because we actually *want* non-range based behavior on `Eq` and `Hash` for various reasons, including the ability to do name-addressibility of the keys when looking up exports and class fields, etc. This means that we don't actually want to rely on `Ranged` at all, we want to use a more flexible API that allows us to only sometimes use the `Key` for the range; other times we can use the `Binding` or even look up some other `Key` / `Binding` pair in cases where the binding is really just a pointer (for example, `KeyExpect` is just pointing at a binding). This commit adds the hook to allow this; for now we still rely on the (often dummy) `Ranged` implementations to provide the range, but I'll stack changes to get real ranges. Reviewed By: grievejia Differential Revision: D95120700 fbshipit-source-id: 26da06d1df46e79839549a67b1929e860e99364e

Inline per-module report writes Summary: **About this perf change** Last week, the Pysa team re-wired the `--report-pysa` integration to happen "inline" during type checking in D97510488, which was a huge memory and performance win because then Pyrefly no longer has to store all the data in RAM between checking and post-processing. It's probably an even bigger win for `--report-cinderx` to adopt this, because I never even bothered parallelizing the post-processing (to be fair, it probably doesn't matter much if we're only compiling a few processes - but if we try to compile and entire application it might). This stack adopts the same strategy as D97510488 for `--report-cinderx` **About this diff** Move CinderX per-module type file generation into the main type-checking flow. A transaction-held reporter now writes each module's JSON (and optional readable text) as soon as Answers are available, while project-level files are still written at the end of the run. This keeps the new behavior narrowly scoped: it changes when per-module files are emitted, but does not yet change retention or the class metadata source. Reviewed By: yangdanny97 Differential Revision: D97762602 fbshipit-source-id: e9ca93de13a2ec6da0667adf6f73081fdd1ffdfd

Store compact class metadata in Solutions Summary: **About this perf change** Last week, the Pysa team re-wired the `--report-pysa` integration to happen "inline" during type checking in D97510488, which was a huge memory and performance win because then Pyrefly no longer has to store all the data in RAM between checking and post-processing. It's probably an even bigger win for `--report-cinderx` to adopt this, because I never even bothered parallelizing the post-processing (to be fair, it probably doesn't matter much if we're only compiling a few processes - but if we try to compile and entire application it might). This stack adopts the same strategy as D97510488 for `--report-cinderx` **About this diff** Add compact per-module CinderX summaries to Solutions and switch class_metadata.json generation to consume those summaries instead of reading full retained Solutions for every defining module. The summary only keeps the class qname, ancestor refs, and protocol bit that CinderX finalization needs. A fallback path still rebuilds the summary from retained answers for tests and non-reporter callers. Reviewed By: yangdanny97 Differential Revision: D97762603 fbshipit-source-id: 9d3151c428f9f2263745f19d0777e690f61a3029

Reconstruct overload residuals at callable boundaries Summary: **This stack** Adds a "callable residual" type that allows us to capture structure when a generic or overloaded callable is passed to a higher-order function. The residuals can later be "exploded" to recover generic and overload structure in outputs (either Callable outputs, or classes whose methods capture the callable structure of an argument - e.g. callback protocol classes). The full design details are [here](https://github.com/stroxler/pyrefly-docs/tree/main/callable-residuals) **This diff** This is the first commit where we can start to see end-to-end overload residual behavior, because a minimal capture/finishing/finalization cycle is now fully implemented Overload residual finishing now emits branch projections for each captured var, so callable-boundary finalization must apply those branch substitutions to the enclosing type rather than flattening to a single marker. This reconstructs overloads by identity: intersect viable branch indices across matching markers, substitute each branch into a cloned enclosing type, recursively finalize each branch, and combine callable-shaped results into `Type::Overload` so downstream call checks do real overload dispatch instead of noisy union checks. Expectation updates for callable_residuals are folded here so this commit is test-clean on its own. Invariants remain explicit: substitution must eliminate the active identity, and recursive identity cycles are unreachable. ---------- NOTE: I had originally intended `finalize_callable_residuals_mut` to handle both overload *and* generic residuals, but what wound up happening at this stage is that overload residuals get expanded first in a separate pass, and *then* we handle generic residuals in `finalize_callable_residuals_mut`. This is fine in that it all works and allows us to get end-to-end behavior in good shape, but I want to tighten things up at the end of the stack because in my opinion the code, while functional, is kind of sprawling now. I'll do that in a cleanup later, because it's easier to refactor with a test harness in place for behaviors we like. Reviewed By: rchen152 Differential Revision: D102216902 fbshipit-source-id: ed1ef60f5460c18dd1f8f746e992c913ecd9ed6b

Add type_to_structured conversion Summary: Converts pyrefly's internal Type enum into the flat StructuredType representation (class, callable, variable, literal) used by the CinderX report. Includes helpers for qname canonicalization, callables, quantified type variables, and a catch-all fallback to typing.Any for internal/uncommon type variants. Reviewed By: lolpack Differential Revision: D95859726 fbshipit-source-id: 412b4ab2a49071bfa42f2de0189032c812c9946c

make call-scope context a required solve boundary Summary: This is part of the solver-boundary plan: constraint solving is usually per-call, but we also rely on ad-hoc subset boundaries where call-like behavior can occur with residual tracking disabled, so we must make boundary ownership explicit and always drain call-scoped state before leaving the boundary. This change makes callable finishing consume the active call context, adds explicit boundary-consumption state with debug-time drop invariants, and tracks fresh quantified vars created during call-scoped solving so boundary finishing still sees them even when residual reachability is lost. NOTE: there's a lot of new code here and not much deltion, but a lot of the new logic is just the preparation / plumbing phase of a mini-stack that shifts responsibility for finishing around - there's offsetting deletion of a lot of legacy finishing code in D103337567 (which is the end goal - that commit fixes the `reduce` regression by storing all fresh vars in context and finishing them at the appropriate time). Reviewed By: rchen152 Differential Revision: D103328383 fbshipit-source-id: d5bf4bbff28154cb64f7365a9e64c66c78fe90fd

Route pruning through probe-backed finishing Summary: **This stack** Adds a "callable residual" type that allows us to capture structure when a generic or overloaded callable is passed to a higher-order function. The residuals can later be "exploded" to recover generic and overload structure in outputs (either Callable outputs, or classes whose methods capture the callable structure of an argument - e.g. callback protocol classes). The full design details are [here](https://github.com/stroxler/pyrefly-docs/tree/main/callable-residuals) **This diff** Here we finally wire up pruning end-to-end. Why: overload pruning viability was computed with an inert subset relation on several call-analysis finishing paths, so every branch looked compatible and pruning never took effect. What: add a type-order-aware finishing entrypoint that runs through Subset probe-backed subset checks, route call/callable finishing sites to it, and keep non-call definition-time finishing on the inert path. Also harden pruning probes by snapshotting/restoring the entire subset cache, and emit a specialization error when all branches for a witness are pruned. Why it works: pruning decisions now use real assignability checks under rollback semantics, so branch sets shrink correctly (including collapse-to-one and all-pruned). Updated overload-pruning tests now assert the actual pruned outcomes. Reviewed By: rchen152 Differential Revision: D102245364 fbshipit-source-id: cea699b4f5aa6e91a00fc7556eaa5b94e701c9da

Add a structured type representation Summary: Dump types in a json format that uses hashing to deduplicate types for a much more compact representation. Reviewed By: lolpack Differential Revision: D95856048 fbshipit-source-id: bf1a0678e6248200faef4f1b64b9d0974d13ee1d

Replace all-siblings fn_lookup with per-caller transitive-callee resolution (#3485) Summary: Pull Request resolved: https://github.com/facebook/pyrefly/pull/3485 **This stack** Reworks tensor shape operations so that instead of being hardcoded in tensor_ops_registry.rs, only DSL primitives are directly hardcoded into Pyrefly; the actual operations and the association with "normal" (non DSL) stubs all lives in user-space stub files. This allows iterating on the ops without rebuilding Pryefly, and is 100% essential for actually building out full stubs for pytorch (and even more so if we want to extend to other libraries like numpy and jax). The DSL itself is unchanged but we will use a decorator to indicate when a stub function is a DSL function; we use a different decorator to actually register a DSL function as the "shape transform" associated with some normal function (e.g. to associate the DSL function `reshape_ir` with a `torch.reshape` function). Details of the plan are in https://github.com/stroxler/pyrefly-docs/blob/main/tensor-shapes-in-stubs/v2-doc.md **This commit** Each `shape_dsl_function` now carries only its transitive callees instead of every DSL function in the module. A leaf function like `randn_ir` gets `helpers = [self]` (1 entry) instead of all 86 siblings. `reshape_ir` gets `[reshape_ir, normalize_dim]` (2 entries). `movedim_ir` gets its 6 transitive callees. Adds `ShapeDslFunction::call_targets()` which walks `DslBody`/`DslExpr` collecting `DslCallTarget::UserDefined` names, and `compute_transitive_helpers` which resolves those names against the per-module `BindingsMetadata` index and computes the fixed-point closure. Behaviorally identical — same shape inference results, same types. The change reduces per-function memory footprint and will enable finer cache invalidation once solver dependency edges are per-helper. Reviewed By: rchen152 Differential Revision: D105783601 fbshipit-source-id: 1dcab8c9da122bdfe8c427f8b87add81ba752cf9

Roll back keyless ExclusiveLock change to investigate primer timeouts Summary: Roll back 4c8b4f15e98d9bb48e629bcdcf7ada3b7b02d45f ("Replace ExclusiveLock keyed locking with keyless blocking lock"). Hypothesis: the keyless blocking lock can introduce lock-order deadlocks in demand() under concurrency. A thread may hold module A's compute lock while demanding module B, while another thread holds B and demands A, causing both threads to block. This would show up as nondeterministic mypy_primer timeouts depending on scheduling. The evidence for this is mostly empirical, I don't have a precise root cause: - Here are two sandcastle jobs kicked off from the commit *before* 4c8b4f15e98, both pass - https://www.internalfb.com/sandcastle/workflow/441352763496628319 - https://www.internalfb.com/sandcastle/workflow/4327959241917262804 - Here are two sandcastle jobs kicked off *against* 4c8b4f15e98 - https://www.internalfb.com/sandcastle/workflow/1292533093069624277 - https://www.internalfb.com/sandcastle/workflow/1373597886362130243 This change restores the prior keyed behavior to test whether the timeouts disappear in CI Reviewed By: yangdanny97 Differential Revision: D95256215 fbshipit-source-id: 31805e320c6e8311e3ef133a60a0c227a1e31585

Convert callable/bound-method tests to expect test format Summary: The readable output shows narrowed/unnarrowed types with mismatch markers, which is the key behavior these tests validate. This format tests more about the output in a human-verifiable way, and this way of setting up tests is much better for quick TDD iteration on actual examples where cinderx/pyrefly integration hits bugs Reviewed By: DinoV Differential Revision: D97672078 fbshipit-source-id: 776dfadbb466ee274d34a0cbe3f6208507326047