diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index fa97cff4c7..874859d269 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3143,14 +3143,14 @@ class visit_structure_instance_fn {
                     name S_fname = m_mvar2field[mlocal_name(e)];
                     name full_S_fname = m_S_name + S_fname;
                     expr expected_type = m_elab.infer_type(e);
-                    expected_type = m_elab.instantiate_mvars(expected_type);
+                    expr reduced_expected_type = m_elab.instantiate_mvars(expected_type);
                     expr val;
 
                     try {
-                        reduce_and_check_deps(expected_type, full_S_fname);
+                        reduce_and_check_deps(reduced_expected_type, full_S_fname);
                         /* note: we pass the reduced, mvar-free expected type. Otherwise auto params may fail with
                          * "result contains meta-variables". */
-                        val = (*m_field2elab.find(S_fname))(expected_type);
+                        val = (*m_field2elab.find(S_fname))(reduced_expected_type);
                     } catch (field_not_ready_to_synthesize_exception const & e) {
                         done = false;
                         if (!last_progress)
diff --git a/tests/lean/structure_notation_dep_mvars.lean b/tests/lean/structure_notation_dep_mvars.lean
new file mode 100644
index 0000000000..0fe9fbc29a
--- /dev/null
+++ b/tests/lean/structure_notation_dep_mvars.lean
@@ -0,0 +1 @@
+instance : monad list := { .. }
diff --git a/tests/lean/structure_notation_dep_mvars.lean.expected.out b/tests/lean/structure_notation_dep_mvars.lean.expected.out
new file mode 100644
index 0000000000..44dcd2ad24
--- /dev/null
+++ b/tests/lean/structure_notation_dep_mvars.lean.expected.out
@@ -0,0 +1,6 @@
+structure_notation_dep_mvars.lean:1:25: error: type mismatch at field 'pure_bind'
+  ?m_1
+has type
+  ∀ {α β : Type ?} (x : α) (f : α → list β), ?m_1 (?m_2 x) f = f x
+but is expected to have type
+  ∀ {α β : Type ?} (x : α) (f : α → list β), has_pure.pure list x >>= f = f x