Say and N more when a typed-hole refinement list is cut

docs/src/learn/07-collections.md

@@ -115,7 +115,7 @@ note: hole `?` has type `int -> int -> int` — try: min, max, const — or: fli
 3 | let total = List.fold ? 0 ns
   |                       ^
 
-note: hole `?` has type `int` — try: total — or: List.sum ?, Seq.sum ?, String.len ?, round ?
+note: hole `?` has type `int` — try: total — or: List.sum ?, Seq.sum ?, String.len ?, round ?, and 13 more
  --> 4:32
   |
 4 | let atTen = Option.withDefault ? (List.get 10 ns)

docs/src/learn/09-typed-holes.md

@@ -18,7 +18,7 @@ names |> headline |> print
 Running `pyfun check` reports the gap rather than a failure:
 
 ```console
-note: hole `?upper` has type `'a -> string` — try: String.upper, input, String.trimStart, String.trimEnd, String.rev, String.ofList, and 9 more — or: String.repeat ?, String.concat ?, String.join ?, Option.withDefault ?
+note: hole `?upper` has type `'a -> string` — try: String.upper, input, String.trimStart, String.trimEnd, String.rev, String.ofList, and 9 more — or: String.repeat ?, String.concat ?, String.join ?, Option.withDefault ?, and 18 more
  --> 5:15
   |
 5 |   |> List.map ?upper
@@ -27,7 +27,7 @@ note: hole `?upper` has type `'a -> string` — try: String.upper, input, String
 
 The hole needs a function producing a string, and `String.upper` is first under `try:`. It comes first because of the hole's name: a fit whose name matches the hole's goes to the front of the list, so naming a hole after what you want is a way of asking for it. The `or:` list names functions that would also fit if you filled their own holes. Replace `?upper` with `String.upper` and the program compiles and prints `ADA, GRACE, ALAN`.
 
-The `try:` list shows six fits, and `and 9 more` says how many it left out. Hovering the module in your editor, or `:type` in the REPL, gives you the full surface.
+The `try:` list shows six fits and the `or:` list shows four. The `and 9 more` and `and 18 more` at their ends say how many each one left out. Hovering the module in your editor, or `:type` in the REPL, gives you the full surface.
 
 This is the workflow: sketch the whole pipeline with holes, let the compiler name each gap's type, and fill inward from the types and the suggested fits. You never have to guess a function's signature, because the hole reports it for you, and a hole blocks compilation by design, so nothing runs until every blank is filled.
 
@@ -36,7 +36,7 @@ This is the workflow: sketch the whole pipeline with holes, let the compiler nam
 Fill both holes. `report` looks a score up in a map, supplies a fallback when the name is absent, and turns the number into a string. `pyfun check` reports each hole with a `try:` value that fits. The first report is:
 
 ```console
-note: hole `?render` has type `int -> 'a` — try: List.range, Seq.range, String.get, String.repeat, String.fromInt, String.fromFloat, and 59 more — or: String.slice ?, List.replicate ?, List.updateAt ?, List.insertAt ?
+note: hole `?render` has type `int -> 'a` — try: List.range, Seq.range, String.get, String.repeat, String.fromInt, String.fromFloat, and 59 more — or: String.slice ?, List.replicate ?, List.updateAt ?, List.insertAt ?, and 16 more
 ```
 
 ```pyfun

docs/src/notebooks/07-collections.ipynb

@@ -165,7 +165,7 @@
     "3 | let total = List.fold ? 0 ns\n",
     "  |                       ^\n",
     "\n",
-    "note: hole `?` has type `int` — try: total — or: List.sum ?, Seq.sum ?, String.len ?, round ?\n",
+    "note: hole `?` has type `int` — try: total — or: List.sum ?, Seq.sum ?, String.len ?, round ?, and 13 more\n",
     " --> 4:32\n",
     "  |\n",
     "4 | let atTen = Option.withDefault ? (List.get 10 ns)\n",

docs/src/notebooks/09-typed-holes.ipynb

@@ -44,7 +44,7 @@
     "Running `pyfun check` reports the gap rather than a failure:\n",
     "\n",
     "```console\n",
-    "note: hole `?upper` has type `'a -> string` — try: String.upper, input, String.trimStart, String.trimEnd, String.rev, String.ofList, and 9 more — or: String.repeat ?, String.concat ?, String.join ?, Option.withDefault ?\n",
+    "note: hole `?upper` has type `'a -> string` — try: String.upper, input, String.trimStart, String.trimEnd, String.rev, String.ofList, and 9 more — or: String.repeat ?, String.concat ?, String.join ?, Option.withDefault ?, and 18 more\n",
     " --> 5:15\n",
     "  |\n",
     "5 |   |> List.map ?upper\n",
@@ -53,7 +53,7 @@
     "\n",
     "The hole needs a function producing a string, and `String.upper` is first under `try:`. It comes first because of the hole's name: a fit whose name matches the hole's goes to the front of the list, so naming a hole after what you want is a way of asking for it. The `or:` list names functions that would also fit if you filled their own holes. Replace `?upper` with `String.upper` and the program compiles and prints `ADA, GRACE, ALAN`.\n",
     "\n",
-    "The `try:` list shows six fits, and `and 9 more` says how many it left out. Hovering the module in your editor, or `:type` in the REPL, gives you the full surface.\n",
+    "The `try:` list shows six fits and the `or:` list shows four. The `and 9 more` and `and 18 more` at their ends say how many each one left out. Hovering the module in your editor, or `:type` in the REPL, gives you the full surface.\n",
     "\n",
     "This is the workflow: sketch the whole pipeline with holes, let the compiler name each gap's type, and fill inward from the types and the suggested fits. You never have to guess a function's signature, because the hole reports it for you, and a hole blocks compilation by design, so nothing runs until every blank is filled.\n",
     "\n",
@@ -62,7 +62,7 @@
     "Fill both holes. `report` looks a score up in a map, supplies a fallback when the name is absent, and turns the number into a string. `pyfun check` reports each hole with a `try:` value that fits. The first report is:\n",
     "\n",
     "```console\n",
-    "note: hole `?render` has type `int -> 'a` — try: List.range, Seq.range, String.get, String.repeat, String.fromInt, String.fromFloat, and 59 more — or: String.slice ?, List.replicate ?, List.updateAt ?, List.insertAt ?\n",
+    "note: hole `?render` has type `int -> 'a` — try: List.range, Seq.range, String.get, String.repeat, String.fromInt, String.fromFloat, and 59 more — or: String.slice ?, List.replicate ?, List.updateAt ?, List.insertAt ?, and 16 more\n",
     "```"
    ],
    "id": "09-003"

src/types/mod.rs

@@ -1752,6 +1752,8 @@ pub struct Hole {
     /// more arguments) unifies with the hole's type — shown applied to further holes
     /// (`String.upper ?`, `String.concat ? ?`). Fewest-holes-first, capped.
     pub refinements: Vec<String>,
+    /// How many further refinement fits the cap left out of `refinements`.
+    pub more_refinements: usize,
     pub span: Span,
 }
 
@@ -1771,7 +1773,11 @@ impl Hole {
             parts.push(format!("try: {}{more}", self.fits.join(", ")));
         }
         if !self.refinements.is_empty() {
-            parts.push(format!("or: {}", self.refinements.join(", ")));
+            let more = match self.more_refinements {
+                0 => String::new(),
+                n => format!(", and {n} more"),
+            };
+            parts.push(format!("or: {}{more}", self.refinements.join(", ")));
         }
         parts.join(" — ")
     }
@@ -2458,13 +2464,15 @@ fn run(module: &Module, record: bool, imports: &HashMap<String, ModuleExports>)
         .map(|(span, name, ty, env)| {
             let (fits, more_fits) = inf.hole_fits(&env, &ty, name.as_deref());
             let direct: std::collections::HashSet<String> = fits.iter().cloned().collect();
-            let refinements = inf.hole_refinements(&env, &ty, &direct, name.as_deref());
+            let (refinements, more_refinements) =
+                inf.hole_refinements(&env, &ty, &direct, name.as_deref());
             Hole {
                 name,
                 ty: show(&inf.apply(&ty)),
                 fits,
                 more_fits,
                 refinements,
+                more_refinements,
                 span,
             }
         })
@@ -9576,16 +9584,17 @@ impl Infer {
     /// keeps out trivially-general combinators (`id`, `const`) that would otherwise
     /// "refine" into every hole. `direct` is the set already reported as direct fits.
     /// Fewest-holes-first, then fewest generalized vars, then unqualified, then name.
+    /// Returns the shortlist and how many further refinements the cap left out.
     fn hole_refinements(
         &mut self,
         env: &Env,
         target: &Ty,
         direct: &std::collections::HashSet<String>,
         hole: Option<&str>,
-    ) -> Vec<String> {
+    ) -> (Vec<String>, usize) {
         let target = self.apply(target);
         if matches!(target, Ty::Var(_)) {
-            return Vec::new();
+            return (Vec::new(), 0);
         }
         let snap = self.subst_snapshot();
         let mut out: Vec<(u8, usize, usize, bool, usize, String)> = Vec::new();
@@ -9633,10 +9642,13 @@ impl Infer {
             }
         }
         out.sort();
-        out.into_iter()
+        let more = out.len().saturating_sub(REFINE_CAP);
+        let shown = out
+            .into_iter()
             .map(|(_, _, _, _, _, s)| s)
             .take(REFINE_CAP)
-            .collect()
+            .collect();
+        (shown, more)
     }
 
     fn instantiate(&mut self, scheme: &Scheme) -> Ty {

tests/typecheck.rs

@@ -3928,6 +3928,36 @@ fn a_truncated_fit_list_says_how_many_it_left_out() {
     );
 }
 
+#[test]
+fn a_truncated_refinement_list_says_how_many_it_left_out() {
+    // Same string->string hole as the truncated direct-fit case: many functions
+    // refine into it (String.lower ?, String.upper ?, …), so the refinement
+    // shortlist is capped and must say how many it left out.
+    let module =
+        pyfun::parse("let r = [\"a\"] |> List.map ?f |> String.join \",\"").expect("parse");
+    let (_e, _t, holes, _ordered, _codecs) = pyfun::types::check_collecting(&module);
+    let hole = &holes[0];
+    assert_eq!(hole.refinements.len(), 4);
+    assert!(hole.more_refinements > 0);
+    // The "and N more" for refinements sits on the `or:` clause; pin that the
+    // message reports the leftover count (the try: clause also has one for fits).
+    assert!(
+        hole.message()
+            .contains(&format!("or: {}", hole.refinements.join(", "))),
+        "{}",
+        hole.message()
+    );
+    assert!(
+        hole.message().contains(&format!(
+            "or: {}, and {} more",
+            hole.refinements.join(", "),
+            hole.more_refinements
+        )),
+        "{}",
+        hole.message()
+    );
+}
+
 #[test]
 fn an_unconstrained_hole_lists_no_fits() {
     // A bare, fully-polymorphic hole (`'a`) would match everything — unhelpful, so