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<expr> 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