refactor: no signature says Any, and a symbol table section that is not a mapping is refused

[FBumann]

Prompt: "How can we enforce this from pyrefly? So this doesnt occure again? (with opt outs possible)" — "Does it now disable any everywhere? It should! And fix all existing ines. possible taking things from 567"

Note

The following content was generated by AI.

explicit-any = "error" on src/math_spec, with nothing exempt. src/ says Any nowhere, and a signature that writes one fails the type check. The rewrite is #567's, ported onto main; the two sites it leaves are narrowed rather than excused.

What this changes

• The gate. explicit-any = "error" in [tool.pyrefly.errors], and no sub-config list. It is the one Any the table did not already reach: an unannotated parameter is implicit-any-parameter, which the strict preset refuses, and an unannotated return is inferred rather than widened. What was left is the Any a signature writes down — a parameter, a return, a variable, a type alias, or inside a generic such as dict[str, Any].
• The 73 sites, taken from refactor: no signature in the package says Any, and a symbol table section that is not a mapping is refused #567. The public doors take Mapping[str, object]; a raw value is object until pydantic has read it; the grammars hand back the node type their walk names; the exclusivity proof compares a cell with a literal of its own kind. _where_parser.py keeps main's grammar and takes only the fold's return type, since the rest of that file's change belongs to the arithmetic-where feature.
• Two sites refactor: no signature in the package says Any, and a symbol table section that is not a mapping is refused #567 leaves, narrowed here. ValidationInfo is Protocol[ContextT] and was left unparameterised, so its argument was Any; ValidationInfo[object] says what the validator accepts, which never reads .context. JsonSchemaValue is pydantic's alias for dict[str, Any], where those three signatures mean dict[str, object]. Neither wants a pragma.
• One refusal, which comes with the rewrite. A symbol table whose dimensions: or names: is a list or a string raised AttributeError. It now raises SchemaError: dimensions: must be a mapping of names to entries, got list.

Why

Any came back into a signature because nothing refused it. Now the type checker does, everywhere, with no file exempt and no pragma outstanding.

Gates

pixi.sh is refused by this environment's egress proxy, so the gates ran from a uv environment on Python 3.12.3 with pydantic 2.13.5 against the lock's 2.13.4, on the pinned pyrefly 1.2.0 and ruff 0.16.1. That is a departure from the "everything runs in a pixi environment" default.

gate	result
pyrefly check	0 errors, 8 suppressed — one pragma fewer than the base's 9
pytest -n auto	1301 passed, 6 skipped (base: 1299 passed, 6 skipped — the two new refusals)
ruff check, ruff format	clean
taplo format, typos	no change, clean
mkdocs build --strict	clean, with the docs.python.org inventory dropped for the run, which the proxy refuses with a 403
compile-tex	not run, for want of a TeX distribution
grep -rn '\bAny\b' src/	no match

The gate was checked in both directions, not only for staying green. Given def widened(x: Any) -> None in any file of the package, pyrefly check fails with Explicit Any is not allowed [explicit-any]; the same line with # pyrefly: ignore[explicit-any] passes, and the suppression count rises by one.

What the narrowing bought, and what it cost — five guards deleted in turn

Replacing Any with the type a line actually holds turns some checks the annotation used to make into checks the code has to make. Each one deleted, suite re-run, tree restored by git checkout --:

deleted	suite
_numbers' "a label or a date reached a magnitude" assert	1301 passed — unreached
_compare's "the two are of different kinds" AssertionError	1301 passed — unreached
_section's "is a mapping in a validated model" assert	1301 passed — unreached
_mask_dims' nominated branch, left reading the mask's dims	6 failed, 1295 passed
_section's setdefault, left indexing the raw dict	1 failed, 1300 passed

The last two are load-bearing and covered. The first three are guards no test reaches, so this PR owes each one a purpose-built probe before merge, per AGENTS. None of them wants Any back: each states an invariant the dtype rules or a validated model already guarantee, and the alternative is not Any but an unchecked cast. The cast count did not rise — src/ has one fewer than the base, exclusivity.py having lost cast('set[int]', values).

What this means for #567

This carries #567's src/ diff, so that PR is left with the parser work and nothing else to say about typing. The port was a three-way apply of 5e37736..d080058 limited to src/ and tests/, and only _where_parser.py conflicted — that file's change is mostly the arithmetic-where feature's _nested, which does not exist on main, so main keeps its grammar and takes the _folder return type alone. Everything else applied clean, which is why the counts above match what that PR measured.

Rebasing the stack on this should drop those twelve files from it. What is genuinely #567's and is not here: nothing — its tests/typesetting/test_symbols.py cases came along with the refusal.

Departed from, and deliberately not done

• This PR grew a src/ diff after it was opened, so it is no longer the one-line ci: change its first commit was. It is one topic — Any is refused and Any is gone — but it is two commits rather than one, and the first commit's message describes a backlog list that the second deletes. A squash merge reads correctly; the branch history does not, and I did not force-push to fix that.
• The refusal is a behaviour change inside a refactor:. It is in the title for that reason, rather than left for the body, because it is what a changelog reader can see. The alternative was to keep raw.get('names') or {} and its Any, which is the thing this PR exists to remove.
• Three guards still want a probe, as the table above says. They are named rather than written, because writing a test against an invariant is a decision about how far to reach around validation to reproduce it.
• No ratchet test and no second rule. With nothing exempt there is no list to ratchet. The implicit-any family and unannotated-* are already at zero, so promoting them would be a no-op; unknown-argument-type reports 44 and is a separate argument.
• _yaml.py keeps its one unknown-variable-type pragma on construct_document, whose stub returns Any. That is the third-party boundary the per-line opt-out exists for, and it is the only one left in the package.

🤖 Generated with Claude Code

https://claude.ai/code/session_015nY2qq2hQzyMFApWuD5zFW

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34652618 | 📁 Comparing fb723b6 against latest (3317ecf)

  🔍 Preview build  

5 files changed · ± 5 modified

± Modified

• reference/math_spec/advice/index.html
• reference/math_spec/lowering/index.html
• reference/math_spec/model/index.html
• reference/math_spec/validation/index.html
• reference/math_spec/typesetting/symbols/index.html