From cf3b0e108764f2a72e93ba462ff79d563ba79d3f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 23 Nov 2014 16:11:50 -0800
Subject: [PATCH] feat(frontends/lean/placeholder_elaborator): apply
 substitution before collecting local instances, closes #333

---
 src/frontends/lean/local_context.cpp          | 9 +++++++++
 src/frontends/lean/local_context.h            | 3 +++
 src/frontends/lean/placeholder_elaborator.cpp | 4 ++--
 tests/lean/run/inst_bug.lean                  | 5 +++++
 4 files changed, 19 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/inst_bug.lean

diff --git a/src/frontends/lean/local_context.cpp b/src/frontends/lean/local_context.cpp
index 5cc636f88..f16f404b0 100644
--- a/src/frontends/lean/local_context.cpp
+++ b/src/frontends/lean/local_context.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/abstract.h"
 #include "kernel/replace_fn.h"
+#include "kernel/metavar.h"
 #include "frontends/lean/local_context.h"
 
 namespace lean {
@@ -107,4 +108,12 @@ void local_context::add_local(expr const & l) {
 list<expr> const & local_context::get_data() const {
     return m_ctx;
 }
+
+static list<expr> instantiate_locals(list<expr> const & ls, substitution & s) {
+    return map(ls, [&](expr const & l) { return update_mlocal(l, s.instantiate(mlocal_type(l))); });
+}
+
+local_context local_context::instantiate(substitution s) const {
+    return local_context(instantiate_locals(m_ctx, s));
+}
 }
diff --git a/src/frontends/lean/local_context.h b/src/frontends/lean/local_context.h
index ffd912c9b..56d4289df 100644
--- a/src/frontends/lean/local_context.h
+++ b/src/frontends/lean/local_context.h
@@ -84,5 +84,8 @@ public:
     list<expr> const & get_data() const;
 
     void add_local(expr const & l);
+
+    /** \brief Instantiate metavariables occurring this local context using \c s, and return updated local_context */
+    local_context instantiate(substitution s) const;
 };
 }
diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp
index 52bf16ed4..32052bd46 100644
--- a/src/frontends/lean/placeholder_elaborator.cpp
+++ b/src/frontends/lean/placeholder_elaborator.cpp
@@ -264,7 +264,6 @@ struct placeholder_elaborator : public choice_iterator {
     }
 };
 
-
 constraint mk_placeholder_cnstr(std::shared_ptr<placeholder_context> const & C, local_context const & ctx, expr const & m, unsigned depth) {
     environment const & env = C->env();
     justification j         = mk_failed_to_synthesize_jst(env, m);
@@ -318,7 +317,7 @@ static bool has_expr_metavar_relaxed(expr const & e) {
     return found;
 }
 
-constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const & C, local_context const & ctx,
+constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const & C, local_context const & _ctx,
                                      expr const & m, bool is_strict, unifier_config const & cfg, delay_factor const & factor) {
     environment const & env = C->env();
     justification j         = mk_failed_to_synthesize_jst(env, m);
@@ -329,6 +328,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
             // do nothing, since type is not a class.
             return lazy_list<constraints>(constraints());
         }
+        local_context ctx        = _ctx.instantiate(substitution(s));
         pair<expr, justification> mj = update_meta(meta, s);
         expr new_meta            = mj.first;
         justification new_j      = mj.second;
diff --git a/tests/lean/run/inst_bug.lean b/tests/lean/run/inst_bug.lean
new file mode 100644
index 000000000..49d20c188
--- /dev/null
+++ b/tests/lean/run/inst_bug.lean
@@ -0,0 +1,5 @@
+inductive is_equiv [class] (A B : Type) (f : A → B) : Type
+definition inverse (A B : Type) (f : A → B) [H : is_equiv A B f] := Type
+definition foo (A : Type) (B : A → Type) (h : A → A) (g : Π(a : A), B a → B a)
+               [H : Π(a : A), is_equiv _ _ (g a)] (x : A) : Type :=
+inverse (B (h x)) (B (h x)) (g (h x))