fix: simple match case

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 :=

tests/lean/run/matchVarIssue.lean

@@ -0,0 +1,2 @@
+theorem ex {c d : Char} : c = d → c.val = d.val
+  | rfl => rfl