From b38c943086fd99d03ee33fcf3fac92f75dbb730d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Mar 2015 10:13:16 -0700
Subject: [PATCH] fix(library/tactic/class_instance_synth): discard partial
 solutions even when option class.unique_instances = true is used

---
 src/library/tactic/class_instance_synth.cpp | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp
index 5ba8d7fc4..4426df223 100644
--- a/src/library/tactic/class_instance_synth.cpp
+++ b/src/library/tactic/class_instance_synth.cpp
@@ -375,11 +375,18 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
         };
 
         unify_result_seq seq1    = unify(env, 1, &c, ngen, substitution(), new_cfg);
+        unify_result_seq seq2    = filter(seq1, [=](pair<substitution, constraints> const & p) {
+                substitution new_s = p.first;
+                expr result = new_s.instantiate(new_meta);
+                // We only keep complete solutions (modulo universe metavariables)
+                return !has_expr_metavar_relaxed(result);
+            });
+
         if (get_class_unique_class_instances(C->m_ios.get_options())) {
             optional<expr> solution;
             substitution subst;
             constraints  cnstrs;
-            for_each(seq1, [&](pair<substitution, constraints> const & p) {
+            for_each(seq2, [&](pair<substitution, constraints> const & p) {
                     subst  = p.first;
                     cnstrs = p.second;
                     expr next_solution = subst.instantiate(new_meta);
@@ -403,12 +410,6 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
                 return lazy_list<constraints>(to_cnstrs_fn(subst, cnstrs));
             }
         } else {
-            unify_result_seq seq2      = filter(seq1, [=](pair<substitution, constraints> const & p) {
-                    substitution new_s = p.first;
-                    expr result = new_s.instantiate(new_meta);
-                    // We only keep complete solutions (modulo universe metavariables)
-                    return !has_expr_metavar_relaxed(result);
-                });
             if (try_multiple_instances(env, *cls_name_it)) {
                 lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) {
                         return to_cnstrs_fn(p.first, p.second);