From 89bc55aece640f671a9013f50ac2ed86f422c6fa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 8 Sep 2016 19:20:08 -0700
Subject: [PATCH] feat(frontends/lean/elaborator): improve expected type for
 equation rhs

---
 src/frontends/lean/elaborator.cpp | 4 +++-
 tests/lean/run/new_elab1.lean     | 8 ++++++++
 tests/lean/run/rw_set1.lean       | 2 +-
 3 files changed, 12 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/new_elab1.lean

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index dd8adc843c..d1fe6f97c6 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1428,11 +1428,13 @@ expr elaborator::visit_equation(expr const & eq) {
         throw exception("ill-formed equation");
     expr new_lhs;
     {
+        list<expr> saved_instance_stack = m_instance_stack;
         flet<bool> set(m_in_pattern, true);
         new_lhs = visit(lhs, none_expr());
         check_inaccessible_annotations(new_lhs);
+        try_to_synthesize_type_class_instances(saved_instance_stack);
     }
-    expr new_lhs_type = infer_type(new_lhs);
+    expr new_lhs_type = instantiate_mvars(infer_type(new_lhs));
     expr new_rhs      = visit(rhs, some_expr(new_lhs_type));
     new_rhs = enforce_type(new_rhs, new_lhs_type, "equation type mismatch", eq);
     return copy_tag(eq, mk_equation(new_lhs, new_rhs));
diff --git a/tests/lean/run/new_elab1.lean b/tests/lean/run/new_elab1.lean
new file mode 100644
index 0000000000..8799fcd8ba
--- /dev/null
+++ b/tests/lean/run/new_elab1.lean
@@ -0,0 +1,8 @@
+open nat
+
+protected theorem my_add_comm : ∀ (n m : ℕ), n + m = m + n
+| n 0     := eq.symm (nat.zero_add n)
+| n (m+1) :=
+  suffices succ (n + m) = succ (m + n), from
+    eq.symm (succ_add m n) ▸ this,
+  congr_arg succ (my_add_comm n m)
diff --git a/tests/lean/run/rw_set1.lean b/tests/lean/run/rw_set1.lean
index a064a65181..a4e6a7d609 100644
--- a/tests/lean/run/rw_set1.lean
+++ b/tests/lean/run/rw_set1.lean
@@ -1,5 +1,5 @@
 constant nat.add_assoc (a b c : nat) : (a + b) + c = a + (b + c)
-constant nat.add_comm (a b : nat) : a + b = b + a
+
 
 namespace foo
   attribute nat.add_assoc [simp]