conv command enter miscounts function arguments

[javra]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

In the following code, the enter command should focus on f's second argument instead of failing:

example (α : Type) (β : α → Type) (f : (a : α) → β a → Nat) (a : α) (b b' : β a) :
  f a b = f a b' := by
  conv => 
    enter [1, 2]

This is because arguments with forward dependencies are skipped, but this is not obvious to the user.

[leodemoura]

I see two possible solutions.

1- We improve the current error message. The current error message is

error: invalid 'arg' conv tactic, application has only 1 (nondependent) argument(s)

It is indirectly saying that only independent arguments can be explored. Any suggestions on how to make it better?
We can also add doc-strings to many conv tactics such as enter, arg, etc.

BTW, enter and arg are currently not using user-defined [congr] theorems. We want to fix this in the future.

2- Allow enter and arg to go inside dependent arguments, but disable tactics that do not preserve definitional equality.

[javra]

It's not that I don't like the error message, it's more that the numbering is off, which option 1 doesn't fix. I'd rather we do count all explicit throw the error message at the (potentially) unsuccessful rewrite. I.e. your second option but without really disabling anything. rw outside of conv also sometimes produces motive not type correct messages, and I think that's okay within conv, too.

As for the user-defined [congr] theorems, will they have to be called explicitely? I see potential sources of confusion otherwise...

[javra]

I would propose changing enter and arg's syntax to have numbers refer to all explicit arguments and have something like @3 to count implicits, too.

[fpfu]

It also seems natural to use argument names in enter and arg

[leodemoura]

Closed by PR above.