From 20d7727a9c91f75e70d2dfdbc5b13cb5a30648b2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Dec 2015 19:38:24 -0800
Subject: [PATCH] fix(library/blast/forward/pattern): pattern inference bug

---
 src/library/blast/forward/pattern.cpp     | 2 +-
 tests/lean/pattern_bug1.lean              | 3 +++
 tests/lean/pattern_bug1.lean.expected.out | 4 ++++
 3 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/pattern_bug1.lean
 create mode 100644 tests/lean/pattern_bug1.lean.expected.out

diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp
index c4d13e6fc..299b04755 100644
--- a/src/library/blast/forward/pattern.cpp
+++ b/src/library/blast/forward/pattern.cpp
@@ -550,9 +550,9 @@ struct mk_hi_lemma_fn {
         lean_assert(m_mvars.size() == inst_implicit_flags.size());
         buffer<expr> subst;
         buffer<expr> residue_locals;
+        candidate_set hints = collect_pattern_hints(m_mvars, B);
         expr proof  = mk_proof(residue_locals, subst);
         B           = replace_mvars(B, subst);
-        candidate_set hints = collect_pattern_hints(m_mvars, B);
         list<multi_pattern> mps;
         if (!hints.empty()) {
             mps = mk_multi_patterns_using(hints, false);
diff --git a/tests/lean/pattern_bug1.lean b/tests/lean/pattern_bug1.lean
new file mode 100644
index 000000000..dd64d91c1
--- /dev/null
+++ b/tests/lean/pattern_bug1.lean
@@ -0,0 +1,3 @@
+constants {A : Type} (P : A → Prop) (R : A → A → Prop)
+definition H [forward] : ∀ a, (: P a :) → ∃ b, R a b := sorry
+print H
diff --git a/tests/lean/pattern_bug1.lean.expected.out b/tests/lean/pattern_bug1.lean.expected.out
new file mode 100644
index 000000000..1964b92f5
--- /dev/null
+++ b/tests/lean/pattern_bug1.lean.expected.out
@@ -0,0 +1,4 @@
+definition H [forward] : ∀ (a : A), (:P a:) → Exists (R a) :=
+sorry
+(multi-)patterns:
+{P ?M_1}