diff --git a/tests/lean/forErrors.lean b/tests/lean/forErrors.lean
new file mode 100644
index 0000000000..8d36e09410
--- /dev/null
+++ b/tests/lean/forErrors.lean
@@ -0,0 +1,6 @@
+def g (xs ys : List Nat) (a : α) : IO Nat := do
+  let mut sum := 0
+  for x in xs, y in ys, c in a, z in ys do
+    sum := x + sum
+    IO.println s!"x: {x}, y: {y}, a: {a}, c: {c}, sum: {sum}"
+  return sum
diff --git a/tests/lean/forErrors.lean.expected.out b/tests/lean/forErrors.lean.expected.out
new file mode 100644
index 0000000000..d815b27add
--- /dev/null
+++ b/tests/lean/forErrors.lean.expected.out
@@ -0,0 +1,4 @@
+forErrors.lean:3:29: error: failed to synthesize instance
+  ToStream α ?m
+forErrors.lean:5:15: error: failed to synthesize instance
+  ToString α