From 3d0ea4c9d13b54b84b3d373cadab87e174a37fee Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 24 Jan 2016 13:39:25 -0800
Subject: [PATCH] feat(library/type_context): improve find_unsynth_metavar

---
 src/library/type_context.cpp             | 30 +++++++++++++++++++++++-
 src/library/type_context.h               |  1 +
 tests/lean/run/blast_real_sub_issue.lean |  5 ++++
 3 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/blast_real_sub_issue.lean

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index c9a10d9d4..8605a65da 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1325,6 +1325,8 @@ bool type_context::compatible_local_instances(list<expr> const & ctx) {
 
 // Helper function for find_unsynth_metavar
 static bool has_meta_arg(expr e) {
+    if (!has_expr_metavar(e))
+        return false;
     while (is_app(e)) {
         if (is_meta(app_arg(e)))
             return true;
@@ -1337,7 +1339,7 @@ static bool has_meta_arg(expr e) {
     metavariable whose type is a type class, and (?m t_1 ... t_n) must be synthesized
     by type class resolution, then we return ?m.
     Otherwise, we return none */
-optional<pair<expr, expr>> type_context::find_unsynth_metavar(expr const & e) {
+optional<pair<expr, expr>> type_context::find_unsynth_metavar_at_args(expr const & e) {
     if (!has_meta_arg(e))
         return optional<pair<expr, expr>>();
     buffer<expr> args;
@@ -1364,6 +1366,32 @@ optional<pair<expr, expr>> type_context::find_unsynth_metavar(expr const & e) {
     return optional<pair<expr, expr>>();
 }
 
+/** Search in \c e for an expression of the form (f ... (?m t_1 ... t_n) ...) where ?m is an unassigned
+    metavariable whose type is a type class, and (?m t_1 ... t_n) must be synthesized
+    by type class resolution, then we return ?m.
+    Otherwise, we return none.
+    This procedure goes inside lambdas. */
+optional<pair<expr, expr>> type_context::find_unsynth_metavar(expr const & e) {
+    if (!has_expr_metavar(e))
+        return optional<pair<expr, expr>>();
+    if (is_app(e)) {
+        if (auto r = find_unsynth_metavar_at_args(e))
+            return r;
+        expr it = e;
+        while (is_app(it)) {
+            if (auto r = find_unsynth_metavar(app_arg(it)))
+                return r;
+            it = app_fn(it);
+        }
+        return optional<pair<expr, expr>>();
+    } else if (is_lambda(e)) {
+        expr l = mk_tmp_local_from_binding(e);
+        return find_unsynth_metavar(instantiate(binding_body(e), l));
+    } else {
+        return optional<pair<expr, expr>>();
+    }
+}
+
 bool type_context::on_is_def_eq_failure(expr & e1, expr & e2) {
     if (is_app(e1)) {
         if (auto p1 = find_unsynth_metavar(e1)) {
diff --git a/src/library/type_context.h b/src/library/type_context.h
index e02dd3be8..a00a36511 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -292,6 +292,7 @@ class type_context {
     optional<name> is_full_class(expr type);
     lbool is_quick_class(expr const & type, name & result);
 
+    optional<pair<expr, expr>> find_unsynth_metavar_at_args(expr const & e);
     optional<pair<expr, expr>> find_unsynth_metavar(expr const & e);
 
     expr mk_internal_local(name const & n, expr const & type, binder_info const & bi = binder_info());
diff --git a/tests/lean/run/blast_real_sub_issue.lean b/tests/lean/run/blast_real_sub_issue.lean
new file mode 100644
index 000000000..ac7d8b706
--- /dev/null
+++ b/tests/lean/run/blast_real_sub_issue.lean
@@ -0,0 +1,5 @@
+import data.real
+open real
+
+example (x y : ℝ) : x - y = x + - y :=
+by inst_simp