From 7e2f0f9a3638ae3c1d7156251d2b348c57b4ce82 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Mar 2015 17:28:56 -0800 Subject: [PATCH] fix(library/unifier): in the context_check, we should not consider local constants that occur in the type of other constants This was a performance bug. We were missing higher-order pattern constraints due to this bug. --- src/library/unifier.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 434a72bcd..d5703f50d 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -118,9 +118,10 @@ bool context_check(expr const & e, buffer const & locals) { for_each(e, [&](expr const & e, unsigned) { if (failed) return false; - if (is_local(e) && !contains_local(e, locals)) { - failed = true; - return false; + if (is_local(e)) { + if (!contains_local(e, locals)) + failed = true; + return false; // do not visit type } if (is_metavar(e)) return false; // do not visit type