feat(library/tactic/apply_tactic): perform class-instance resolution in the apply tactic

closes #360

src/library/tactic/apply_tactic.cpp

@@ -20,8 +20,10 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/metavar_closure.h"
 #include "library/type_util.h"
+#include "library/local_context.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/tactic/apply_tactic.h"
+#include "library/tactic/class_instance_synth.h"
 
 namespace lean {
 /**
@@ -61,15 +63,19 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
     if (empty(gs))
         return proof_state_seq();
     name_generator ngen = s.get_ngen();
-    std::shared_ptr<type_checker> tc(mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque()));
+    bool relax_opaque = s.relax_main_opaque();
-    goal  g          = head(gs);
+    std::shared_ptr<type_checker> tc(mk_type_checker(env, ngen.mk_child(), relax_opaque));
-    goals tail_gs    = tail(gs);
+    goal  g           = head(gs);
-    expr  t          = g.get_type();
+    goals tail_gs     = tail(gs);
-    expr  e          = _e;
+    expr  t           = g.get_type();
-    auto e_t_cs      = tc->infer(e);
+    expr  e           = _e;
+    auto e_t_cs       = tc->infer(e);
     e_t_cs.second.linearize(cs);
-    expr  e_t        = e_t_cs.first;
+    expr  e_t         = e_t_cs.first;
     buffer<expr> metas;
+    local_context ctx;
+    bool initialized_ctx = false;
+    unifier_config cfg(ios.get_options());
     if (add_meta) {
         // unsigned num_t   = get_expect_num_args(*tc, t);
         unsigned num_e_t = get_expect_num_args(*tc, e_t);
@@ -80,19 +86,34 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
             auto e_t_cs = tc->whnf(e_t);
             e_t_cs.second.linearize(cs);
             e_t        = e_t_cs.first;
-            expr meta  = g.mk_meta(ngen.next(), binding_domain(e_t));
+            expr meta;
+            if (binding_info(e_t).is_inst_implicit()) {
+                if (!initialized_ctx) {
+                    ctx = g.to_local_context();
+                    initialized_ctx = true;
+                }
+                bool use_local_insts = true;
+                bool is_strict       = false;
+                auto mc = mk_class_instance_elaborator(
+                    env, ios, ctx, ngen.next(), optional<name>(),
+                    relax_opaque, use_local_insts, is_strict,
+                    some_expr(binding_domain(e_t)), e.get_tag(), cfg, nullptr);
+                meta    = mc.first;
+                cs.push_back(mc.second);
+            } else {
+                meta  = g.mk_meta(ngen.next(), binding_domain(e_t));
+            }
             e          = mk_app(e, meta);
             e_t        = instantiate(binding_body(e_t), meta);
             metas.push_back(meta);
         }
     }
     metavar_closure cls(t);
-    cls.mk_constraints(s.get_subst(), justification(), s.relax_main_opaque());
+    cls.mk_constraints(s.get_subst(), justification(), relax_opaque);
     pair<bool, constraint_seq> dcs = tc->is_def_eq(t, e_t);
     if (!dcs.first)
         return proof_state_seq();
     dcs.second.linearize(cs);
-    unifier_config cfg(ios.get_options());
     unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), s.get_subst(), cfg);
     list<expr> meta_lst   = to_list(metas.begin(), metas.end());
     return map2<proof_state>(rseq, [=](pair<substitution, constraints> const & p) -> proof_state {

tests/lean/hott/360_2.hlean

@@ -0,0 +1,17 @@
+open truncation
+--structure is_contr [class] (A : Type) : Type
+
+context
+parameters {P : Π(A : Type), A → Type}
+
+definition my_contr {A : Type} [H : is_contr A] (a : A) : P A a := sorry
+
+definition foo2
+(A : Type)
+(B : A → Type)
+(a : A)
+(x : B a)
+(H : Π (a : A), is_contr (B a))  --(H : is_contr (B a))
+  : P (B a) x :=
+by apply my_contr
+end

tests/lean/run/360_1.lean

@@ -0,0 +1,10 @@
+structure is_tr [class] (A : Type) : Type :=
+(x : A)
+
+theorem foo (B : Type) [H : is_tr B] : B :=
+sorry
+
+theorem bar (A : Type) (H : is_tr A) : A :=
+begin
+  apply foo
+end