feat(frontends/lean): remove unnecessary instantiate_all's that were messing with error localization

src/frontends/lean/elaborator.cpp

@@ -1586,7 +1586,7 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
                 return false;
             ps = proof_state(ps, tail(gs), subst, ngen);
         } else {
-            expr new_ptac = subst.instantiate_all(ptac);
+            expr new_ptac = ptac;
             if (auto tac = pre_tactic_to_tactic(new_ptac)) {
                 try {
                     proof_state_seq seq = (*tac)(env(), ios(), ps);
@@ -1648,7 +1648,7 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
             return;
         }
 
-        if (auto tac = pre_tactic_to_tactic(subst.instantiate_all(*pre_tac))) {
+        if (auto tac = pre_tactic_to_tactic(*pre_tac)) {
             bool show_failure = true;
             try_using(subst, mvar, ps, *pre_tac, *tac, show_failure);
             return;

src/library/tactic/elaborate.cpp

@@ -38,7 +38,7 @@ optional<expr> elaborate_with_respect_to(environment const & env, io_state const
     goals const & gs    = s.get_goals();
     if (empty(gs))
         return none_expr();
-    auto ecs = elab(head(gs), ngen.mk_child(), e, report_unassigned);
+    auto ecs   = elab(head(gs), ngen.mk_child(), e, report_unassigned);
     expr new_e = ecs.first;
     buffer<constraint> cs;
     to_buffer(ecs.second, cs);

tests/lean/change_tac_fail.lean

@@ -0,0 +1,12 @@
+import data.list
+open list
+
+variable {T : Type}
+
+theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u)
+| append.assoc nil t u      := by esimp
+| append.assoc (a :: l) t u :=
+  begin
+    change a :: (l ++ t ++ u) = (a :: l) ++ (t ++ a),
+    rewrite append.assoc
+  end

tests/lean/change_tac_fail.lean.expected.out

@@ -0,0 +1,8 @@
+change_tac_fail.lean:10:47: error: type mismatch at application
+  t ++ a
+term
+  a
+has type
+  T
+but is expected to have type
+  list T