From affe3463ab33ae159654472355fb1c72c8414945 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 8 Feb 2018 14:05:43 +0100 Subject: [PATCH] fix(frontends/lean/elaborator): fix assertion error: accidental mutation of a variable --- src/frontends/lean/elaborator.cpp | 6 +++--- tests/lean/structure_notation_dep_mvars.lean | 1 + tests/lean/structure_notation_dep_mvars.lean.expected.out | 6 ++++++ 3 files changed, 10 insertions(+), 3 deletions(-) create mode 100644 tests/lean/structure_notation_dep_mvars.lean create mode 100644 tests/lean/structure_notation_dep_mvars.lean.expected.out 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