fix(library/tactic/rewrite_tactic): apply substitution before trying to rewrite

closes #487

src/library/tactic/rewrite_tactic.cpp

@@ -1341,6 +1341,7 @@ public:
         m_matcher_tc(mk_matcher_tc()),
         m_unifier_tc(mk_type_checker(m_env, m_ngen.mk_child(), ps.relax_main_opaque())),
         m_mplugin(m_ios, *m_matcher_tc) {
+        m_ps = apply_substitution(m_ps);
         goals const & gs = m_ps.get_goals();
         lean_assert(gs);
         update_goal(head(gs));

tests/lean/487.hlean

@@ -0,0 +1,19 @@
+open eq is_trunc
+
+structure is_retraction [class] {A B : Type} (f : A → B) :=
+  (sect : B → A)
+  (right_inverse : Π(b : B), f (sect b) = b)
+
+definition foo
+{A : Type}
+{B : Type}
+(f : A → B)
+(g : B → A)
+(ε : Πb, f (g b) = b)
+(b b' : B)
+  : is_retraction (λ (q : g b = g b'), (ε b) ⁻¹ ⬝ ap f q ⬝ ε b') :=
+begin
+  fapply is_retraction.mk,
+    {exact (@ap B A g b b') },
+    {intro p, cases p, esimp {eq.ap, eq.rec_on, eq.idp} }
+end

tests/lean/487.hlean.expected.out

@@ -0,0 +1,12 @@
+487.hlean:18:56: error: unsolved subgoals
+A : Type,
+B : Type,
+f : A → B,
+g : B → A,
+ε : Π (b : B), f (g b) = b,
+b b' : B
+⊢ (ε b) ⁻¹ ⬝ refl (f (g b)) ⬝ ε b = refl b
+487.hlean:19:0: error: failed to add declaration 'foo' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A : Type) (B : Type) (f : …) (g : …) (ε : …) (b b' : B),
+    is_retraction.mk … ?M_1