max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/elaborator): fix assertion error: accidental mutation of a variable

Browse source
This commit is contained in:
Sebastian Ullrich 2018-02-08 14:05:43 +01:00
parent 5736fda1ee
commit affe3463ab
3 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/elaborator.cpp
View file

@ -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)

1
tests/lean/structure_notation_dep_mvars.lean Normal file
View file

@ -0,0 +1 @@
instance : monad list := { .. }

6
tests/lean/structure_notation_dep_mvars.lean.expected.out Normal file
View file

@ -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