Incorrect names can be generated for generalised variables

[nad]

The following code should not be accepted:

open import Agda.Builtin.Equality

variable
  A : Set₁
  x : A

postulate
  f : (B : Set) → B ≡ B → Set

g : f _ x ≡ f _ x
g {B = B} = refl

Agda infers the following type for g:

{B : Set} {x : B ≡ B} → f B x ≡ f B x

The function g should not have an implicit argument called B.

[nad]

Here is another example:

variable
  A : Set
  x : A

postulate
  F : Set → Set
  P : {x : Set} → F x → Set
  p : P x

-- fails : (A : Set) (f : F A) → P f
-- fails A f = p {x = f}

works : (A : Set) (f : F A) → P f
works A f = p {x = _} {x = f}

Agda infers the following type for p:

{x : Set} {x = x₁ : F x} → P x₁

There should only be one implicit argument called x. With the current naming scheme I guess the first argument should be called x.x, or something like that.

[andreasabel]

We need to distinguish user-written from system-generated names more seriously. In the OP, the name B should be marked as system-generated so that it cannot be referred to in the input.

[UlfNorell]

Both names should be x.A.1. PR above fixes this and clarifies the naming scheme in the user manual.