diff --git a/tests/lean/eq_class_error.lean b/tests/lean/eq_class_error.lean
new file mode 100644
index 000000000..2c0cc5fd2
--- /dev/null
+++ b/tests/lean/eq_class_error.lean
@@ -0,0 +1,15 @@
+inductive foo :=
+| a | b
+
+open foo
+
+-- This test demonstrates we need to disable local instances.
+set_option elaborator.local_instances false
+
+definition decidable_eq_foo [instance] : ∀ f₁ f₂ : foo, decidable (f₁ = f₂)
+| a  a := by left; reflexivity
+| a  b := by right; contradiction
+| b  a := by right; contradiction
+-- If we don't disable the local_instances, then type class resolution synthesizes the term (decidable_eq_foo b b) which is not a
+-- valid "recursive application", and the recursive equation compiler fails with a cryptic message saying we should try to use well-founded recursion.
+| b  b := _
diff --git a/tests/lean/eq_class_error.lean.expected.out b/tests/lean/eq_class_error.lean.expected.out
new file mode 100644
index 000000000..28e650db7
--- /dev/null
+++ b/tests/lean/eq_class_error.lean.expected.out
@@ -0,0 +1,7 @@
+eq_class_error.lean:15:10: error: don't know how to synthesize placeholder
+decidable_eq_foo : Π (f₁ f₂ : foo), decidable (f₁ = f₂)
+⊢ decidable (b = b)
+eq_class_error.lean:9:11: error: failed to synthesize placeholder
+
+⊢ Π (f₁ f₂ : foo),
+    decidable (f₁ = f₂)