Explicit dependent argument is not shadowed correctly in `where`-block

[buzden]

Steps to Reproduce

Consider the following function:

genAtIndex : DecEq a => (n : Nat) -> (f : Fin n) -> (m : a) -> (v : Vect n a) -> Maybe $ AtIndex f v m
genAtIndex n f m v = genHere n f m v
  where
    genHere : (n : Nat) -> (f : Fin n) -> (m : a) -> (v : Vect n a) -> Maybe $ AtIndex f v m
    genHere (S n) FZ x (x0 :: xs) with (decEq x x0)
      genHere (S n) FZ x (x :: xs)  | Yes Refl = pure Here
      genHere (S n) FZ x (x0 :: xs) | No _ = empty
    genHere _ _ _ _ = empty

In the of the outer function body variable n appears several times, both on the LHS and RHS, and inside the inner function, in the signature, on the LHS and RHS of the inner function.

Expected Behavior

Code typecheks.

Observed Behavior

Error: While processing right hand side of genAtIndex. While processing right hand side of genAtIndex,genHere. When unifying:
    Vect n a
and:
    Vect n a
Mismatch between: n and n.

IncorrWhereShadowing:24:5--26:51
 24 |     genHere (S n) FZ x (x0 :: xs) with (decEq x x0)
 25 |       genHere (S n) FZ x (x :: xs)  | Yes Refl = pure Here
 26 |       genHere (S n) FZ x (x0 :: xs) | No _ = empty

Renaming n in usages of the outer function shows that somewhy in the body of the inner function the outer n is used instead of the inner one. For instance, if you replace

-genAtIndex n f m v = genHere n f m v
+genAtIndex n' f m v = genHere n' f m v

code starts to typecheck.

This issue may be related to #2521, but it behaves differently (there it's enough to simply match explicitly in the inner function, which is present here anyway), so I'm not sure this is the same bug.

[buzden]

Shrunk in dryer:

import Data.Vect

%default total

outer : (n : Nat) -> (v : Vect n a) -> Unit
outer n v = inner n v where
  inner : (n : Nat) -> (v : Vect n a) -> Unit
  inner n xs with (())
    inner n xs | () = ()

The problem is definitely with the with clause.