diff --git a/tests/lean/instance1.lean b/tests/lean/instance1.lean
new file mode 100644
index 0000000000..9db054baa8
--- /dev/null
+++ b/tests/lean/instance1.lean
@@ -0,0 +1,9 @@
+def Mine := Id
+
+class MyMonad (m) extends Monad m where
+  bind_eq_bind : @bind = @bind := by trivial
+
+instance : MyMonad Mine where
+  -- should show me all the fields I need to fill in
+  -- excluding default and auto-param fields
+  -- i.e., only `pure` and `bind`
diff --git a/tests/lean/instance1.lean.expected.out b/tests/lean/instance1.lean.expected.out
new file mode 100644
index 0000000000..f09ccac7f6
--- /dev/null
+++ b/tests/lean/instance1.lean.expected.out
@@ -0,0 +1 @@
+instance1.lean:6:24-6:29: error: fields missing: 'pure', 'bind'