diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index e1cabbb3b1ba..bf58d089ca52 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -368,7 +368,7 @@ for new reflexive relations.
 Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
 reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
+macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
 - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
 - The arguments of the relation are not equal.
 Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
diff --git a/tests/lean/run/issue4063.lean b/tests/lean/run/issue4063.lean
new file mode 100644
index 000000000000..9ee73f745243
--- /dev/null
+++ b/tests/lean/run/issue4063.lean
@@ -0,0 +1,5 @@
+/-- error: no goals to be solved -/
+#guard_msgs in
+example : 3 = 3 := by
+  rfl
+  rfl