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

pyproject.toml

@@ -154,13 +154,18 @@ strict-callable-subtyping = true
 # Where a rule is genuinely wrong about one line, suppress that line with
 # `# pyrefly: ignore[rule-name]` and a reason -- do not turn the rule off here.
 #
+# `explicit-any` is the one `Any` the rest of this table does not reach. An
+# *unannotated* parameter is `implicit-any-parameter`, which the preset already
+# refuses; what was left is the `Any` a signature writes down.
+#
 # `implicit-any-lambda` is left on and suppressed per line in the two grammars.
 # A lambda takes no annotation, and giving the parse action a typed callback
 # only moves the error: pyparsing returns `ParseResults`, whose `__getitem__`
 # is a union, so the body fails where the parameter used to. Kept on rather
 # than switched off so a lambda outside those grammars still has to say what
 # it takes.
 [tool.pyrefly.errors]
+explicit-any = "error"
 implicit-import = "error"
 missing-import = "error"
 no-any-return-explicit = "error"

src/math_spec/_expression_parser.py

@@ -12,7 +12,7 @@
 
 from dataclasses import dataclass, field
 from functools import lru_cache
-from typing import TYPE_CHECKING, Any, Literal, assert_never, cast, get_args
+from typing import TYPE_CHECKING, Literal, assert_never, cast, get_args
 
 import pyparsing as pp
 
@@ -410,16 +410,17 @@ def _make_func_call(tokens: pp.ParseResults) -> FunctionCallNode:
     return FunctionCallNode(name=name, args=tuple(args), kwargs=kwargs)
 
 
-def _make_left_assoc(tokens: pp.ParseResults) -> Any:
+def _make_left_assoc(tokens: pp.ParseResults) -> ArithmeticNode:
+    result: ArithmeticNode
     result, *rest = tokens
     for op, right in zip(rest[::2], rest[1::2], strict=True):
         result = BinaryOperatorNode(op, result, right)
     return result
 
 
-def _make_power(tokens: pp.ParseResults) -> Any:
+def _make_power(tokens: pp.ParseResults) -> ArithmeticNode:
     """A base and at most one exponent — right-associative, since the exponent is itself a ``unary``."""
-    items = list(tokens)
+    items: list[ArithmeticNode] = list(tokens)
     return items[0] if len(items) == 1 else BinaryOperatorNode('**', items[0], items[2])
 
 
@@ -457,20 +458,22 @@ def _too_deep(what: str, text: str, found: int | None, rewrite: str) -> str:
     return f'The {what} {measured}, past the {MAX_DEPTH} levels the language admits: {shown!r}\n{rewrite}'
 
 
-def parse_text(
+def parse_text[T](
     grammar: pp.ParserElement,
     text: str,
     what: str,
     rewrite: Callable[[str, int], str | None],
-    child_of: Callable[[Any], tuple[Any, ...]],
+    child_of: Callable[[T], tuple[T, ...]],
     deep_rewrite: str,
-) -> Any:
+) -> T:
     """Parse the whole of *text* with *grammar*, or raise :class:`SchemaError` naming *what* failed to parse.
 
     *rewrite* is asked for the predictable mistake at the failure position; its
     sentence, if any, precedes the grammar's own complaint. A tree nesting past
     :data:`MAX_DEPTH`, measured through *child_of*, is refused with
-    *deep_rewrite* — and so is one the parser itself ran out of stack on.
+    *deep_rewrite* — and so is one the parser itself ran out of stack on. The
+    node comes back as the type *child_of* walks, which is the grammar's word
+    for what it builds.
     """
     try:
         result = grammar.parse_string(text, parse_all=True)
@@ -480,7 +483,7 @@ def parse_text(
         raise SchemaError(msg) from e
     except RecursionError:
         raise SchemaError(_too_deep(what, text, None, deep_rewrite)) from None
-    node = result[0]
+    node = cast('T', result[0])
     found = depth(node, child_of)
     if found > MAX_DEPTH:
         raise SchemaError(_too_deep(what, text, found, deep_rewrite))
@@ -534,4 +537,4 @@ def parse_expression(text: str) -> ParsedNode:
             lone ``=``, ``^`` for power — is named with its rewrite before the
             grammar's own complaint.
     """
-    return cast('ParsedNode', parse_text(_GRAMMAR, text, 'expression', _named_rewrite, children, _DEEP_REWRITE))
+    return parse_text(_GRAMMAR, text, 'expression', _named_rewrite, children, _DEEP_REWRITE)

src/math_spec/_where_parser.py

@@ -11,7 +11,7 @@
 
 from dataclasses import dataclass
 from functools import lru_cache
-from typing import TYPE_CHECKING, Any, cast, get_args
+from typing import TYPE_CHECKING, cast, get_args
 
 import pyparsing as pp
 
@@ -156,14 +156,14 @@ def _build_where_grammar() -> pp.ParserElement:
     return where_expr
 
 
-def _folder(node_type: type[AndNode] | type[OrNode]) -> Callable[[pp.ParseResults], Any]:
+def _folder(node_type: type[AndNode] | type[OrNode]) -> Callable[[pp.ParseResults], WhereNode | UnresolvedWhereNode]:
     """A parse action left-folding a flat operator chain into *node_type*."""
 
-    def fold(tokens: pp.ParseResults) -> Any:
-        items = list(tokens)
-        result: WhereNode | UnresolvedWhereNode = items[0]
+    def fold(tokens: pp.ParseResults) -> WhereNode | UnresolvedWhereNode:
+        items: list[WhereNode | UnresolvedWhereNode] = list(tokens)
+        result = items[0]
         for item in items[1:]:
-            result = node_type(cast('WhereNode', result), item)
+            result = node_type(cast('WhereNode', result), cast('WhereNode', item))
         return result
 
     return fold

src/math_spec/_yaml.py

@@ -22,7 +22,7 @@
 
 import re
 from pathlib import Path
-from typing import TYPE_CHECKING, Any
+from typing import TYPE_CHECKING
 
 import yaml
 
@@ -64,7 +64,7 @@ def _check_duplicate_keys(node: yaml.Node, origin: str) -> None:
     two merge keys are two merges, which PyYAML accumulates.
     """
     if isinstance(node, yaml.MappingNode):
-        seen: dict[Any, int] = {}
+        seen: dict[str, int] = {}
         pairs: list[tuple[yaml.Node, yaml.Node]] = node.value
         for key_node, value_node in pairs:
             line = key_node.start_mark.line + 1
@@ -89,12 +89,12 @@ def _check_duplicate_keys(node: yaml.Node, origin: str) -> None:
             _check_duplicate_keys(item, origin)
 
 
-def read_yaml(path: Path | str) -> dict[str, Any]:
+def read_yaml(path: Path | str) -> dict[str, object]:
     """Read *path* off disk and parse it, in YAML 1.2's reading of scalars."""
     return parse_yaml(Path(path).read_text(encoding='utf-8'), str(path))
 
 
-def read_model(model: str | Path) -> dict[str, Any]:
+def read_model(model: str | Path) -> dict[str, object]:
     """A model from a file or from its text — a newline decides which a ``str`` is.
 
     A :class:`~pathlib.Path` names a file, and so does a ``str`` with no
@@ -117,7 +117,7 @@ def read_model(model: str | Path) -> dict[str, Any]:
     return parse_yaml(model, 'YAML text')
 
 
-def parse_yaml(text: str, origin: str = '<string>') -> dict[str, Any]:
+def parse_yaml(text: str, origin: str = '<string>') -> dict[str, object]:
     """Parse YAML *text* as a mapping of sections.
 
     Args:

src/math_spec/advice.py

@@ -17,14 +17,14 @@
 from math_spec.program import At, GroupSum, walk
 
 if TYPE_CHECKING:
+    from collections.abc import Mapping
     from pathlib import Path
-    from typing import Any
 
     from math_spec.model import Spec
     from math_spec.program import Program
 
 
-def advice(model: str | Path | dict[str, Any] | Spec | Program) -> tuple[Advice, ...]:
+def advice(model: str | Path | Mapping[str, object] | Spec | Program) -> tuple[Advice, ...]:
     """Everything the language advises about *model* — never an error, decidable without data.
 
     Args: