"${HOLE NAME} is already defined" in `with`

[gergoerdi]

data Name : Type where
     UN : String -> Name -- user written name
     MN : String -> Int -> Name -- machine generated name

data IsVar : Name -> Nat -> List Name -> Type where
     First : IsVar n Z (n :: ns)
     Later : IsVar n i ns -> IsVar n (S i) (m :: ns)

data Var : List Name -> Type where
     MkVar : {i : Nat} -> (0 p : IsVar n i vars) -> Var vars

insertName : {outer : List Name} -> Var (outer ++ inner) -> Var (outer ++ n :: inner)
insertName {outer = []} (MkVar p) = MkVar (Later p)
insertName {outer = (n::ns)} (MkVar First) = MkVar First
insertName {outer = (n::ns)} (MkVar (Later x)) with (insertName ?zz)
  insertName {  outer = (n::ns)} (MkVar (Later x)) | with_pat = ?q___rhs

Note that the hole name ?zz is unique. Still, trying to load this file, I get the following error message:

While processing right hand side of insertName at WarmupExercise/Ex2.idr:30:1--32:1: Main.zz is already defined

[gallais]

In #2546 I solved some similar issues with holes in record parameters. The problem is that elaboration duplicates the holes (I'm not sure where it's being duplicated in this case).