feat(library/unifier): add 'quick' failure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/unifier.cpp

@@ -1165,13 +1165,18 @@ unifier_plugin get_noop_unifier_plugin() {
 }
 
 lazy_list<substitution> unify(std::shared_ptr<unifier_fn> u) {
-    return mk_lazy_list<substitution>([=]() {
-            auto s = u->next();
-            if (s)
-                return some(mk_pair(*s, unify(u)));
-            else
-                return lazy_list<substitution>::maybe_pair();
-        });
+    if (u->in_conflict()) {
+        u->failure(); // make sure exception is thrown if u->m_use_exception is true
+        return lazy_list<substitution>();
+    } else {
+        return mk_lazy_list<substitution>([=]() {
+                auto s = u->next();
+                if (s)
+                    return some(mk_pair(*s, unify(u)));
+                else
+                    return lazy_list<substitution>::maybe_pair();
+            });
+    }
 }
 
 lazy_list<substitution> unify(environment const & env,  unsigned num_cs, constraint const * cs, name_generator const & ngen,

src/tests/library/CMakeLists.txt

@@ -7,3 +7,6 @@ add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy)
 add_executable(occurs occurs.cpp)
 target_link_libraries(occurs ${EXTRA_LIBS})
 add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
+add_executable(unifier unifier.cpp)
+target_link_libraries(unifier ${EXTRA_LIBS})
+add_test(unifier ${CMAKE_CURRENT_BINARY_DIR}/unifier)

src/tests/library/unifier.cpp

@@ -0,0 +1,29 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/test.h"
+#include "library/unifier.h"
+using namespace lean;
+
+static void tst1() {
+    environment env;
+    name_generator ngen("foo");
+    expr A  = Local("A", Type);
+    expr f  = Local("f", A >> (A >> A));
+    expr a  = Local("a", A);
+    expr b  = Local("b", A);
+    expr m  = mk_metavar("m", A);
+    expr t1 = f(m, m);
+    expr t2 = f(a, b);
+    auto r = unify(env, t1, t2, ngen);
+    lean_assert(r.is_nil());
+}
+
+int main() {
+    save_stack_info();
+    tst1();
+    return has_violations() ? 1 : 0;
+}