Expose tightening hints in JSON and fix prompt-mode staleness

Two review findings:

- :spec_wider_return entries were auto-triaged but only counted in
  stats, contradicting the comment that says tightening candidates
  remain discoverable. The JSON output now carries them in a
  tightening_hints section with full entry detail (not gated).

- Prompt mode omitted untranslatable entries and still instructed
  reviewers to judge spec_wider_return, which no longer appears in its
  data. It now includes untranslatables and the instructions match the
  actual verdict set, including the dynamic_args probe.

Also drops the Code.fetch_docs/1 exclusion: :erl_anno's nominal types
resolve now that Code.Typespec.fetch_types/1 returns them (elixir-lang#15562),
and the tool reported the entry as stale -- zero untranslatable specs
remain.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: lukaszsamson

lib/elixir/scripts/compare_specs_and_signatures.exs

@@ -766,11 +766,13 @@ defmodule Main do
       stale: stale
     }
 
+    hints = Enum.filter(all, &(&1.verdict == :spec_wider_return))
+
     out =
       case opts[:format] do
         "report" -> render_report(stats, residue, untranslatable, all, gate)
-        "json" -> JSON.encode_to_iodata!(render_json(stats, residue, untranslatable))
-        "prompt" -> render_prompt(stats, residue)
+        "json" -> JSON.encode_to_iodata!(render_json(stats, residue, untranslatable, hints))
+        "prompt" -> render_prompt(stats, residue, untranslatable)
       end
 
     case opts[:output] do
@@ -825,13 +827,18 @@ defmodule Main do
     %{mfa: mfa_string(e), why: e[:why]}
   end
 
-  defp render_json(stats, residue, untranslatable) do
+  # tightening_hints carries the auto-triaged :spec_wider_return entries:
+  # inference proved the return strictly narrower than an exactly-translated
+  # spec. Not gated (specs are deliberately wide contracts), but listed so
+  # documentation-tightening candidates remain identifiable.
+  defp render_json(stats, residue, untranslatable, hints) do
     %{
       elixir: System.version(),
       format_version: 3,
       stats: stats,
       residue: Enum.map(residue, &entry_json/1),
-      untranslatable: Enum.map(untranslatable, &untranslatable_json/1)
+      untranslatable: Enum.map(untranslatable, &untranslatable_json/1),
+      tightening_hints: Enum.map(hints, &entry_json/1)
     }
   end
 
@@ -931,29 +938,33 @@ defmodule Main do
   defp percent(_n, 0), do: "n/a"
   defp percent(n, total), do: "#{Float.round(n * 100 / total, 1)}%"
 
-  defp render_prompt(stats, residue) do
-    json = JSON.encode_to_iodata!(render_json(stats, residue, []))
+  defp render_prompt(stats, residue, untranslatable) do
+    json = JSON.encode_to_iodata!(render_json(stats, residue, untranslatable, []))
 
     [
       """
       You are reviewing the RESIDUE of a mechanical comparison between Elixir
       @spec declarations and compiler-inferred type signatures. Everything
       mechanically decidable has already been decided:
 
-      - functions where spec and inference agree, or where inference is merely
-        wider (expected conservatism), are NOT included;
-      - "verdict" was computed with semantic subtyping in the checker's own
-        type lattice, slice-wise per spec clause;
+      - functions where spec and inference agree, where inference is merely
+        wider (expected conservatism), or where inference is strictly inside
+        the spec (specs are deliberately wide public contracts) are NOT
+        included;
+      - "verdict" was computed by applying the inferred signature with the
+        checker's own application rule, slice-wise per spec clause, using
+        semantic subtyping in the checker's type lattice;
       - "translation_exact" flags where the spec had to be approximated
         (e.g. non_neg_integer() -> integer()); do not draw conclusions that
-        depend on precision the translation lost.
+        depend on precision the translation lost;
+      - "dynamic_args" is the checker's return prediction for a call with
+        fully-unknown arguments and its relation to the spec return.
 
       For each entry, judge:
       1. contradiction: which side is wrong, and what should change?
-      2. spec_wider_return: is tightening the spec desirable documentation-wise
-         (e.g. a function that never returns [] declared as returning keyword())
-         or is the wider spec intentional API contract?
-      3. mixed: characterize the difference and whether it is actionable.
+      2. mixed: characterize the difference and whether it is actionable.
+      3. untranslatable: which typespec construct is unsupported and whether
+         a sound over-approximation could be added to the translator.
 
       Be concise; order by severity; reference module.function/arity.
 

lib/elixir/scripts/compare_specs_exclusions.txt

@@ -33,7 +33,6 @@ Calendar.ISO.parse_utc_datetime/1          # mixed
 Calendar.ISO.parse_utc_datetime/2          # mixed
 Calendar.ISO.time_to_iodata/5              # mixed
 Code.Typespec.spec_to_quoted/2             # mixed
-Code.fetch_docs/1                          # untranslatable ({:missing_type, :erl_anno, :location, 0}) -- OTP 28 nominal type; resolves once Code.Typespec returns nominal types
 Config.__env__!/0                          # mixed
 Config.__target__!/0                       # mixed
 Date.from_erl/2                            # mixed