fix(frontends/lean/elaborator): incorrect error position in begin-end block, fixes #276

src/frontends/lean/elaborator.cpp

@@ -907,13 +907,9 @@ void elaborator::display_unsolved_proof_state(expr const & mvar, proof_state con
     display_unsolved_proof_state(mvar, ps, msg, mvar);
 }
 
-optional<expr> elaborator::get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited) {
+optional<expr> elaborator::get_pre_tactic_for(expr const & mvar) {
     if (auto it = m_local_tactic_hints.find(mlocal_name(mvar))) {
-        expr pre_tac = subst.instantiate(*it);
-        // TODO(Leo): after we move to new apply/exact, we will not need the following
-        // command anymore.
-        pre_tac      = solve_unassigned_mvars(subst, pre_tac, visited);
-        return some_expr(pre_tac);
+        return some_expr(*it);
     } else {
         return none_expr();
     }
@@ -941,14 +937,6 @@ optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
     }
 }
 
-optional<tactic> elaborator::get_local_tactic_hint(substitution & subst, expr const & mvar, name_set & visited) {
-    if (auto pre_tac = get_pre_tactic_for(subst, mvar, visited)) {
-        return pre_tactic_to_tactic(*pre_tac);
-    } else {
-        return optional<tactic>();
-    }
-}
-
 /** \brief Try to instantiate meta-variable \c mvar (modulo its state ps) using the given tactic.
     If it succeeds, then update subst with the solution.
     Return true iff the metavariable \c mvar has been assigned.
@@ -1053,7 +1041,7 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
     type = solve_unassigned_mvars(subst, type, visited);
     bool relax_main_opaque = m_relaxed_mvars.contains(mlocal_name(mvar));
     proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child(), relax_main_opaque);
-    if (auto pre_tac = get_pre_tactic_for(subst, mvar, visited)) {
+    if (auto pre_tac = get_pre_tactic_for(mvar)) {
         if (is_begin_end_annotation(*pre_tac)) {
             try_using_begin_end(subst, mvar, ps, *pre_tac);
             return;

src/frontends/lean/elaborator.h

@@ -126,9 +126,8 @@ class elaborator : public coercion_info_manager {
     unify_result_seq solve(constraint_seq const & cs);
     void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg, expr const & pos);
     void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg);
-    optional<expr> get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited);
+    optional<expr> get_pre_tactic_for(expr const & mvar);
     optional<tactic> pre_tactic_to_tactic(expr const & pre_tac);
-    optional<tactic> get_local_tactic_hint(substitution & subst, expr const & mvar, name_set & visited);
     bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, tactic const & tac,
                    bool show_failure);
     void try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac);

tests/lean/beginend_bug.lean

@@ -0,0 +1,9 @@
+import tools.tactic
+open tactic
+
+theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
+begin
+  apply eq.trans,
+  apply Hbc,
+  apply Hbc,
+end

tests/lean/beginend_bug.lean.expected.out

@@ -0,0 +1,19 @@
+beginend_bug.lean:7:2: error: tactic failed
+A : Type,
+a : A,
+b : A,
+c : A,
+Hab : a = b,
+Hbc : b = c
+⊢ a = ?M_1
+
+A : Type,
+a : A,
+b : A,
+c : A,
+Hab : a = b,
+Hbc : b = c
+⊢ ?M_1 = c
+beginend_bug.lean:9:0: error: failed to add declaration 'foo' to environment, value has metavariables
+  λ (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c),
+    ?M_1