Should `.below` be marked as private/internal?

[kim-em]

See for example

#check List.Sublist.below.cons
List.Sublist.below.cons.{u_1} {α : Type u_1} :
  ∀ {motive : (a a_1 : List α) → a.Sublist a_1 → Prop} {l₁ l₂ : List α} (a : α) {a_1 : l₁.Sublist l₂},
    a_1.below → motive l₁ l₂ a_1 → ⋯.below

In tests/lean/run/constructor_as_variable.lean we now see the error:

error: invalid pattern, constructor or constant marked with '[match_pattern]' expected

Suggestions: 'List.Sublist.below.cons', 'List.Sublist.cons', 'List.cons'

on the test

def ctorSuggestion2 (list : List α) : Nat :=
  match list with
  | nil => 0
  | cons x xs => 1 + ctorSuggestion2 xs

These .below auxiliary functions are rarely (never?) meant to be used by users, and perhaps should be marked as private or internal in some way, so they would not be displayed here.

There is already a check for isPrivateName when generating this message.

[kim-em]

Pinging @arthur-adjedj for an opinion?

[arthur-adjedj]

When having Batteries imported, the number of suggestions grows a lot, and not many of them seem to stem from below, it might be useful to restrict these suggestions to names of functions whose final codomains are that of the expected type being matched on (i.e List here):

invalid pattern, constructor or constant marked with '[match_pattern]' expected

Suggestions:
  'Batteries.AssocList.cons',
  'Batteries.BinomialHeap.Imp.Heap.cons',
  'Batteries.RBNode.Stream.cons',
  'IO.AsyncList.cons',
  'LazyList.cons',
  'Lean.AssocList.cons',
  'List.Chain.below.cons',
  'List.Chain.cons',
  'List.Forall₂.below.cons',
  'List.Forall₂.cons',
   (or 7 others)

I don't think there are many cases in which proving a .below property would be useful for the user, so I would be inclined to mark them as private/internal. If .belows were to be marked as private, shouldn't .brecOn also be marked as such ? AFAIK, they're mostly unusable unless one one can provide a proof of .below. Pinging @nomeata for a second opinion.

[nomeata]

I agree that it should not be suggested like this. I wouldn't hide it completely, it's useful for learning and for advanced uses, but not a good suggestion.

[nomeata]

JFTR: I anticipate that at some point we’ll have to get more clarity on the different notions of internal/private/etc that we have floating around, and their relevance for documentation listing/loogle/tactics/error message suggestions. When that comes up hopefully it’ll be clearer what to do here.