fix: inaccessible pattern vars reported as binders (#5337)

Fixes an unused variable false positive on some wildcard patterns

Fixes #1633, fixes #2830

src/Lean/Elab/Match.lean

@@ -643,7 +643,7 @@ where
     | .proj _ _ b       => return p.updateProj! (← go b)
     | .mdata k b        =>
       if inaccessible? p |>.isSome then
-        return mkMData k (← withReader (fun _ => false) (go b))
+        return mkMData k (← withReader (fun _ => true) (go b))
       else if let some (stx, p) := patternWithRef? p then
         Elab.withInfoContext' (go p) fun p => do
           /- If `p` is a free variable and we are not inside of an "inaccessible" pattern, this `p` is a binder. -/

tests/lean/linterUnusedVariables.lean

@@ -255,3 +255,10 @@ def ignoreEverything : Lean.Linter.IgnoreFunction :=
   fun _ _ _ => true
 
 def ignored (x : Nat) := 0
+
+/-!
+The wildcard pattern introduces a copy of `x` that should not be linted as it is in an
+inaccessible annotation.
+-/
+example : (x = y) → y = x
+  | .refl _ => .refl _