diff --git a/tests/lean/run/matchMissingCase.lean b/tests/lean/run/matchMissingCase.lean
new file mode 100644
index 0000000000..36def2c81e
--- /dev/null
+++ b/tests/lean/run/matchMissingCase.lean
@@ -0,0 +1,24 @@
+inductive Enum where | a | b | c | d
+
+/--
+error: Missing cases:
+Enum.d
+Enum.c
+-/
+#guard_msgs in
+def test : Enum → Nat
+  | .a => 0
+  | .b => 0
+
+-- set_option trace.Meta.Match.match true
+
+/--
+error: Missing cases:
+Enum.d, false
+Enum.c, false
+-/
+#guard_msgs(pass trace, all) in
+def test2 : Enum → Bool → Nat
+  | .a, _ => 0
+  | .b, _ => 0
+  | _, true => 0