Automatically quantified variables are either inaccessible, or misprinted

[MiddleAdjunction]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [X] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

Consider the following code:

def foo : Fin.rev a = a := sorry

#check foo -- foo : ∀ {n : Nat} {a : Fin n}, a.rev = a
#check foo (n := 0) -- <-- error [HERE]

Here both a : Fin n of foo and its index n : Nat are automatically quantified. The command #check foo displays type of foo as expected: ∀ {n : Nat} {a : Fin n}, a.rev = a. However, when one tries to access this variable such as in foo (n := 0), it leads to the following error:

invalid argument name 'n' for function 'foo'

If the "generated names" like n are meant to be inaccessible then probably use of daggers or similar naming conventions would help resolve the confusion caused by the pretty printer. But, the ideal scenario is for foo (n := 0) to just work.

Context

I raised this issue on a Discord server (Lean 4 anarchy); the description above summarises the issue fairly well.

Steps to Reproduce

To reproduce the issue, run the code above.

Expected behavior: either the assignment like foo (n := 0) works, or pretty printer displays something like ∀ {n✝ : Nat} {a : Fin n}, a.rev = a.

Actual behavior: assigning not mentioned but automatically quantified (by dependency) names leads to error such the one above.

Versions

[4.12.0-nightly-2024-10-22]

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.