fix(types): make strict mypy clean and run it in CI

.github/workflows/ci.yml

@@ -21,6 +21,7 @@ jobs:
       - run: uv sync --extra dev
       - run: uv run ruff check
       - run: uv run ruff format --check
+      - run: uv run mypy
 
   test:
     # The tool promises identical behaviour on all three platforms, so all three

src/proofpath/config.py

@@ -152,10 +152,10 @@ def _coerce(section: str, key: str, value: Any, expected: Any, path: Path) -> An
             return value
         raise ConfigError(f"{path}: {where} must be a string, got {value!r}")
     if get_origin(expected) is Literal:
-        choices = get_args(expected)
-        if isinstance(value, str) and value in choices:
+        options = get_args(expected)
+        if isinstance(value, str) and value in options:
             return value
-        raise ConfigError(f"{path}: {where} must be one of {', '.join(choices)}, got {value!r}")
+        raise ConfigError(f"{path}: {where} must be one of {', '.join(options)}, got {value!r}")
     if expected is int:
         # ``bool`` is an ``int`` to Python and a different answer to a reader.
         if isinstance(value, int) and not isinstance(value, bool) and value >= 1:

src/proofpath/judge.py

@@ -1484,8 +1484,8 @@ def _queries_from(text: str, count: int) -> dict[int, JudgedClaim]:
             if not isinstance(entry, dict):
                 continue
             try:
-                ident = int(entry.get("id"))
-            except (TypeError, ValueError):
+                ident = int(entry["id"])
+            except (KeyError, TypeError, ValueError):
                 continue
             if not 0 <= ident < count:
                 continue

src/proofpath/tui/app.py

@@ -426,7 +426,9 @@ def ask(host: str, status: int | None) -> Answer:
                 return "no"  # asked while the app was already leaving
             answer: Future[Answer] = Future()
             try:
-                self.call_from_thread(self._open_prompt, owner, host, status, answer)
+                # Textual types the callback as ``Callable[..., T | Awaitable[T]]``, and
+                # mypy solves ``T`` for a coroutine function as ``Never``: a stub limit.
+                self.call_from_thread(self._open_prompt, owner, host, status, answer)  # type: ignore[arg-type]
             except Exception:
                 return "no"
             return answer.result()
@@ -592,7 +594,7 @@ def on_key(self, event: tevents.Key) -> None:
     def on_resize(self, event: tevents.Resize) -> None:
         # The event's size, not ``self.size``: the app's own is a step behind here.
         self._fit_bottom(event.size.width)
-        if self.query_one(Suggestions).visible:
+        if self.query_one(Suggestions).showing:
             self._refresh_suggestions(event.size)
 
     def _fit_bottom(self, width: int | None = None) -> None:

src/proofpath/tui/widgets/suggestions.py

@@ -8,6 +8,7 @@
 from rich.text import Text
 from textual.content import Content
 from textual.style import Style
+from textual.widget import Widget
 from textual.widgets import Static
 
 from proofpath.tui.commands import DESCRIPTIONS, NEEDS_ARGUMENT
@@ -82,7 +83,10 @@ def __init__(self, *, theme: Theme, coloured: bool) -> None:
         self._indicators: tuple[bool, bool] = (False, False)
 
     @property
-    def visible(self) -> bool:
+    def showing(self) -> bool:
+        """Whether the list is displayed. Not ``visible``: Textual's own property of
+        that name reads the ``visibility`` rule and is settable, and shadowing it with
+        a read-only ``display`` reading would change what Textual itself sees."""
         return self.display
 
     @property
@@ -247,7 +251,7 @@ def _width(self) -> int:
         # widget is still ``display: none``) the container's, less this widget's own
         # gutter, which is what the layout is about to give it.
         width = self.size.width
-        if not width and self.parent is not None:
+        if not width and isinstance(self.parent, Widget):
             width = self.parent.size.width - self.styles.gutter.width
         return width or DEFAULT_WIDTH
 

src/proofpath/tui/wordmark.py

@@ -69,7 +69,9 @@
 class ThemeLike(Protocol):
     """What :func:`render` needs of a theme: its name."""
 
-    name: str
+    # Read-only, so a frozen ``Theme`` with a ``Literal`` name satisfies it.
+    @property
+    def name(self) -> str: ...
 
 
 #: The three things :func:`rows` can decide: no mark at all (``narrow``), the texts

src/proofpath/verify.py

@@ -518,7 +518,7 @@ def target_document(
     address = _bare_address(target)
     if address is not None:
         return _address_document(address, client, fetcher, network_allowed=network_allowed)[0]
-    if _is_file(target):
+    if isinstance(target, Path) or _is_file(target):
         return ingest.load(Path(target))
     return _pasted(target, name or "pasted text")
 
@@ -812,13 +812,13 @@ def closed(stage: str, by: str, summary: str, began: float) -> None:
     # and some text to search. The three branches below all start from this same
     # question, so it is asked once instead of being spelled out three times.
     searchable = not document.references and unmarked and bool(document.paragraphs)
-    chosen: claims_mod.Checkworthy | None = None
+    worthy: claims_mod.Checkworthy | None = None
     if searchable and allowed and engine.search and engine.searcher is not None:
-        chosen = claims_mod.checkworthy(document, limit=engine.config.search.max_claims)
+        worthy = claims_mod.checkworthy(document, limit=engine.config.search.max_claims)
     # A text with no sentence to search ("???", a row of emoji) is not searched: a
     # Searching stage over nothing would end the run with no finding at all, which
     # reads as clean (product rule 6). It keeps the parse error below instead.
-    will_search = chosen is not None and bool(chosen.claims)
+    will_search = worthy is not None and bool(worthy.claims)
     if sourceless and not will_search:
         if searchable and engine.search and engine.search_problem and allowed:
             # A provider was configured and cannot run. The fix is one setting, so
@@ -931,18 +931,18 @@ def closed(stage: str, by: str, summary: str, began: float) -> None:
     # found (``origin="search"``). From here on every stage runs exactly as it does
     # for a cited source.
     search: SearchSummary | None = None
-    if will_search and chosen is not None:
-        found = _search(
+    if will_search and worthy is not None:
+        searched = _search(
             document,
-            chosen,
+            worthy,
             engine,
             add=add,
             emit=emit,
             check=check,
             opened=opened,
             closed=closed,
         )
-        document, claims, search = found.document, found.claims, found.summary
+        document, claims, search = searched.document, searched.claims, searched.summary
 
     # --- 3. resolving -------------------------------------------------------
     began = opened(RESOLVING, RESOLVERS_BY)

tests/test_tui_app.py

@@ -2069,7 +2069,7 @@ async def test_a_slash_lists_every_verb_in_order_with_the_first_selected() -> No
         await type_into(pilot, "/")
         prompt = app.query_one(Prompt)
         suggestions = app.query_one(Suggestions)
-        assert suggestions.visible
+        assert suggestions.showing
         assert prompt.value == "/"
         assert prompt.candidates == tuple(_completion(verb) for verb in commands.VERBS)
         assert prompt.selected == 0
@@ -2095,26 +2095,26 @@ async def test_the_list_narrows_per_keystroke_and_goes_when_nothing_matches() ->
     async with app.run_test(size=SIZE) as pilot:
         suggestions = app.query_one(Suggestions)
         await type_into(pilot, "/h")
-        assert suggestions.visible
+        assert suggestions.showing
         assert [row[2:].split("  ")[0] for row in suggestions.held] == ["/help"]
         await type_into(pilot, "e")
-        assert suggestions.visible
+        assert suggestions.showing
         assert app.query_one(Prompt).candidates == ("/help",)
         await pilot.press("backspace", "backspace")
         await type_into(pilot, "x")
         assert app.query_one(Prompt).value == "/x"
-        assert suggestions.visible is False
+        assert suggestions.showing is False
 
 
 async def test_a_verb_with_its_space_suggests_nothing_but_allow_and_cancel_do() -> None:
     app, schedulers = build_app()
     async with app.run_test(size=SIZE) as pilot:
         suggestions = app.query_one(Suggestions)
         await type_into(pilot, "/check ")
-        assert suggestions.visible is False
+        assert suggestions.showing is False
         await pilot.press(*(["backspace"] * len("/check ")))
         await type_into(pilot, "/allow ")
-        assert suggestions.visible
+        assert suggestions.showing
         assert [row[2:].split("  ")[0] for row in suggestions.held] == [
             f"/allow {answer}" for answer in commands.ALLOW_ANSWERS
         ]
@@ -2125,7 +2125,7 @@ async def test_a_verb_with_its_space_suggests_nothing_but_allow_and_cancel_do()
         await submit(pilot, "/check one.pdf")
         assert schedulers[0].runs[0].state == "queued"
         await type_into(pilot, "/cancel ")
-        assert suggestions.visible
+        assert suggestions.showing
         assert [row[2:].split("  ")[0] for row in suggestions.held] == ["/cancel #1"]
 
 
@@ -2149,7 +2149,7 @@ async def test_arrows_move_the_selection_and_tab_takes_the_selected_row() -> Non
         await pilot.press("tab")
         assert prompt.value == chosen
         # The cycle stays on show, with its siblings, so a further ``tab`` steps on.
-        assert suggestions.visible
+        assert suggestions.showing
         assert prompt.selected == 2 and suggestions.held[2].startswith("> ")
         await pilot.press("tab")
         assert prompt.value == _completion("config")
@@ -2165,12 +2165,12 @@ async def test_enter_runs_what_is_in_the_bar_and_the_list_goes() -> None:
     async with app.run_test(size=SIZE) as pilot:
         suggestions = app.query_one(Suggestions)
         await type_into(pilot, "/help")
-        assert suggestions.visible
+        assert suggestions.showing
         await pilot.press("enter")
         await pilot.pause()
         assert f"/check {commands.NEEDS_ARGUMENT['check']}" in _notes(app)
         assert app.query_one(Prompt).value == ""
-        assert suggestions.visible is False
+        assert suggestions.showing is False
 
 
 async def test_the_selection_never_walks_the_history_and_a_recalled_line_shows_no_list() -> None:
@@ -2186,12 +2186,12 @@ async def test_the_selection_never_walks_the_history_and_a_recalled_line_shows_n
         await pilot.press("up")
         assert prompt.value == "/"
         await pilot.press("backspace")
-        assert suggestions.visible is False
+        assert suggestions.showing is False
         # With the list hidden the keys are the walk again, and a recalled line does
         # not open the list over itself: the next ``up`` walks on.
         await pilot.press("up")
         assert prompt.value == "/cache"
-        assert suggestions.visible is False
+        assert suggestions.showing is False
         await pilot.press("up")
         assert prompt.value == "/help"
         await pilot.press("down", "down")
@@ -2200,10 +2200,10 @@ async def test_the_selection_never_walks_the_history_and_a_recalled_line_shows_n
         await pilot.press("up")
         await type_into(pilot, "x")
         assert prompt.value == "/cachex"
-        assert suggestions.visible is False
+        assert suggestions.showing is False
         await pilot.press("backspace", "backspace", "backspace")
         assert prompt.value == "/cac"
-        assert suggestions.visible
+        assert suggestions.showing
 
 
 async def test_tab_on_a_recalled_slash_line_brings_the_list_back() -> None:
@@ -2214,11 +2214,11 @@ async def test_tab_on_a_recalled_slash_line_brings_the_list_back() -> None:
         suggestions = app.query_one(Suggestions)
         await pilot.press("up")
         assert prompt.value == "/con"
-        assert suggestions.visible is False  # a recalled line shows no list over itself
+        assert suggestions.showing is False  # a recalled line shows no list over itself
         await pilot.press("tab")
         # "con" completes to one candidate; ``tab`` both takes it and reopens the list.
         assert prompt.value == "/config"
-        assert suggestions.visible
+        assert suggestions.showing
         assert prompt.candidates == ("/config",)
         assert prompt.selected == 0
         assert suggestions.held[0].endswith(commands.DESCRIPTIONS["config"])
@@ -2237,7 +2237,7 @@ async def test_the_list_never_covers_the_log_and_the_bottom_grows_by_its_rows()
         log_height = log.region.height
         await type_into(pilot, "/c")
         await pilot.pause()
-        assert suggestions.visible
+        assert suggestions.showing
         assert len(suggestions.held) == 4
         assert suggestions.drawn == suggestions.held  # four candidates, nothing capped
         assert bottom.region.height == 4 + len(suggestions.drawn)
@@ -2271,7 +2271,7 @@ async def test_the_list_never_covers_the_log_and_the_bottom_grows_by_its_rows()
         await pilot.pause()
         limit = 20 - banner - footer.rows - frame.rows - 1
         assert 0 < limit < len(commands.VERBS)
-        assert suggestions.visible
+        assert suggestions.showing
         first, last = suggestions.window
         assert (first, last) != (0, len(commands.VERBS))
         assert first == 0  # the selection (row 0) is still at the top
@@ -2311,7 +2311,7 @@ async def test_the_list_never_covers_the_log_and_the_bottom_grows_by_its_rows()
 
         await pilot.press("backspace")
         await pilot.pause()
-        assert suggestions.visible is False
+        assert suggestions.showing is False
         assert bottom.region.height == 4
         assert log.region.height == log_height
 
@@ -2417,7 +2417,7 @@ async def test_a_held_paste_never_opens_the_list() -> None:
         assert prompt.held == "/help\n/config"
         assert prompt.value.startswith("pasted")
         assert HELD_SUMMARY.startswith("pasted")
-        assert app.query_one(Suggestions).visible is False
+        assert app.query_one(Suggestions).showing is False
 
 
 # --- the log from the keyboard ------------------------------------------------------
@@ -2604,7 +2604,7 @@ async def test_a_slash_after_clicking_a_finding_brings_the_list_up() -> None:
         prompt = app.query_one(Prompt)
         assert app.focused is prompt
         assert prompt.value == "/"
-        assert app.query_one(Suggestions).visible
+        assert app.query_one(Suggestions).showing
         assert len(app.query_one(Suggestions).held) == len(commands.VERBS)