Incorrect handling of "shadowing" in LHS

[spcfox]

Steps to Reproduce

foo : (n : Nat) -> Vect n a -> ()
foo Z [] = ()
foo n@(.(S n)) (_ :: xs) = foo _ xs

The hole should resolve to the inner n, but it is erased, and the outer one appears in its place. This results in an incorrect clause:

foo n@(.(S _)) (_ :: xs) = foo n xs

Expected Behavior

Error: While processing left hand side of foo. Can't match on ?n [no locals in scope] (Non linear pattern variable).

or

Error: While processing right hand side of foo. n is not accessible in this context.

Observed Behavior

Main> baz 2 [1, 2]
baz 2 []

[spcfox]

The problem is not in solving the hole, but in unification. If we explicitly write n, we will get the same result.

foo : (n : Nat) -> Vect n a -> ()
foo Z [] = ()
foo n@(.(S n)) (_ :: xs) = foo n xs

[dunhamsteve]

At first I thought it was shadowing, but the two n are being treated as the same before it gets to the RHS.

foo : (n : Nat) -> Vect n a -> ()
foo Z [] = ()
foo n@(.(S n)) (_ :: xs) = ?hole

gives

> :ti hole
 0 a : Type
   n : Nat
   xs : Vect n a
------------------------------
hole : ()

[spcfox]

Yes, there is no shadowing of names in LHS because names have the form PV str functionId.

[spcfox]

This also works for conflicts with names in the other patterns

foo : Nat -> (n : Nat) -> Vect n a -> ()
foo _ Z [] = ()
foo n .(S n) (_ :: xs) = foo n n xs

Main> foo 42 2 [1, 2]
foo 42 42 []

[spcfox]

Such cases without a dot are discarded by adding dots to repeating names. https://github.com/idris-lang/Idris2/blob/c6788e5ce0f27436986f4a7bcb8845782ac11db5/src/TTImp/Elab/Ambiguity.idr#L37-L41

But we cannot use a dot inside a dotted pattern.