diff --git a/tests/lean/holes.lean b/tests/lean/holes.lean
index 5fe9a4e6be..ac72e420ad 100644
--- a/tests/lean/holes.lean
+++ b/tests/lean/holes.lean
@@ -20,3 +20,7 @@ f a
 
 partial def f7 (x : Nat) :=
 f7 x
+
+partial def f8 (x : Nat) :=
+let rec aux (y : Nat) := aux y;
+x + 1
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index 9b0cc34dfa..5239c0f0c0 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -49,3 +49,8 @@ holes.lean:21:25: error: don't know how to synthesize placeholder
 context:
 x : Nat
 ⊢ Sort ?
+holes.lean:25:8: error: don't know how to synthesize placeholder
+context:
+f8 : Nat → Nat
+x y : Nat
+⊢ Sort ?