feat(frontends/lean/elaborator): improve expected type for equation rhs

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

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)

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]