fix: don't treat non-atomic idents as pattern variables

src/Lean/Elab/Match.lean

@@ -1201,18 +1201,17 @@ private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermEla
   elabMatchAux gen? discrStxs altViews matchOptMotive expectedType
 
 private def isPatternVar (stx : Syntax) : TermElabM Bool := do
+  if !stx.isIdent || !stx.getId.eraseMacroScopes.isAtomic then
+    return false
   match (← resolveId? stx "pattern") with
-  | none   => return isAtomicIdent stx
+  | none   => return true
   | some f => match f with
     | Expr.const fName _ =>
       match (← getEnv).find? fName with
       | some (ConstantInfo.ctorInfo _) => return false
       | some _                         => return !hasMatchPatternAttribute (← getEnv) fName
-      | _                              => return isAtomicIdent stx
-    | _ => return isAtomicIdent stx
-where
-  isAtomicIdent (stx : Syntax) : Bool :=
-    stx.isIdent && stx.getId.eraseMacroScopes.isAtomic
+      | _                              => return true
+    | _ => return true
 
 @[builtin_term_elab «match»] def elabMatch : TermElab := fun stx expectedType? => do
   match stx with

tests/lean/6537.lean

@@ -0,0 +1,11 @@
+/-! Non-atomic pattern variables should give an error -/
+
+example : Nat → Nat | x.y => x.y
+
+def x.y := ()
+
+example : Nat → Nat | x.y => x.y
+
+attribute [match_pattern] x.y
+
+example : Nat → Nat | x.y => x.y

tests/lean/6537.lean.expected.out

@@ -0,0 +1,8 @@
+6537.lean:3:22-3:25: error: invalid pattern variable, must be atomic
+6537.lean:7:22-7:25: error: invalid pattern variable, must be atomic
+6537.lean:11:22-11:25: error: type mismatch
+  x.y
+has type
+  Unit : Type
+but is expected to have type
+  Nat : Type