feat(frontends/lean/placeholder_elaborator): apply substitution before collecting local instances, closes #333

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

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

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;

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