diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index b573ab6180..ce9c663890 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -64,7 +64,7 @@ struct type_checker::imp {
     // Examples:
     // The type of (lambda x : A, t)   is (Pi x : A, typeof(t))
     // The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t))
-    expr_bi_struct_map<expr>   m_infer_type_cache;
+    expr_bi_struct_map<expr>   m_infer_type_cache[2];
     converter_context          m_conv_ctx;
     type_checker_context       m_tc_ctx;
     bool                       m_memoize;
@@ -280,8 +280,8 @@ struct type_checker::imp {
         check_system("type checker");
 
         if (m_memoize) {
-            auto it = m_infer_type_cache.find(e);
-            if (it != m_infer_type_cache.end())
+            auto it = m_infer_type_cache[infer_only].find(e);
+            if (it != m_infer_type_cache[infer_only].end())
                 return it->second;
         }
 
@@ -378,7 +378,7 @@ struct type_checker::imp {
         }
 
         if (m_memoize)
-            m_infer_type_cache.insert(mk_pair(e, r));
+            m_infer_type_cache[infer_only].insert(mk_pair(e, r));
 
         return r;
     }
diff --git a/tests/lua/tc4.lua b/tests/lua/tc4.lua
new file mode 100644
index 0000000000..cba4c235ef
--- /dev/null
+++ b/tests/lua/tc4.lua
@@ -0,0 +1,17 @@
+local env = empty_environment()
+env = add_decl(env, mk_var_decl("or", mk_arrow(Bool, Bool, Bool)))
+env = add_decl(env, mk_var_decl("A", Bool))
+local Or = Const("or")
+local A  = Const("A")
+local B  = Const("B")
+local tc = type_checker(env)
+local F = Or(A, B)
+assert(tc:infer(F) == Bool)
+assert(not pcall(function()
+                    -- The following test must fail since B is not
+                    -- declared in env.
+                    -- This test make sure that infer and check are
+                    -- not sharing the same cache.
+                    print(tc:check(F))
+                 end
+))