diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 827d34473b..85d777c4ef 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -1008,7 +1008,8 @@ private def isPatternVar (stx : Syntax) : TermElabM Bool := do
     | Expr.const fName _ _ =>
       match (← getEnv).find? fName with
       | some (ConstantInfo.ctorInfo _) => return false
-      | _ => isAtomicIdent stx
+      | some _                         => return !hasMatchPatternAttribute (← getEnv) fName
+      | _                              => isAtomicIdent stx
     | _ => isAtomicIdent stx
 where
   isAtomicIdent (stx : Syntax) : Bool :=
diff --git a/tests/lean/run/matchVarIssue.lean b/tests/lean/run/matchVarIssue.lean
new file mode 100644
index 0000000000..5d5a2b6656
--- /dev/null
+++ b/tests/lean/run/matchVarIssue.lean
@@ -0,0 +1,2 @@
+theorem ex {c d : Char} : c = d → c.val = d.val
+  | rfl => rfl