diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 0954b669d9..cab34b53fd 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -43,18 +43,17 @@ class type_checker::imp {
         expr r = m_normalizer(e, ctx);
         if (is_pi(r))
             return r;
-        if (is_metavar(r) && m_menv && m_up) {
-            lean_assert(!m_menv->is_assigned(r));
+        if (has_metavar(r) && m_menv && m_up) {
             // Create two fresh variables A and B,
             // and assign r == (Pi(x : A), B x)
             expr A = m_menv->mk_metavar(ctx);
             expr B = m_menv->mk_metavar(ctx);
             expr p = mk_pi(g_x_name, A, B(Var(0)));
-            if (has_meta_context(r)) {
-                // r contains lift/inst operations, so we put the constraint in m_up
-                m_up->add_eq(ctx, r, p);
-            } else {
+            if (is_metavar(r) && !has_meta_context(r)) {
+                // cheap case
                 m_menv->assign(r, p);
+            } else {
+                m_up->add_eq(ctx, r, p);
             }
             return p;
         }
@@ -67,18 +66,19 @@ class type_checker::imp {
             return ty_level(u);
         if (u == Bool)
             return level();
-        if (is_metavar(u) && m_up) {
-            lean_assert(!m_menv->is_assigned(u));
+        if (has_metavar(u) && m_menv && m_up) {
             // Remark: in the current implementation we don't have level constraints and variables
             // in the unification problem set. So, we assume the metavariable is in level 0.
             // This is a crude approximation that works most of the time.
             // A better solution is consists in creating a fresh universe level k and
             // associate the constraint that u == Type k.
             // Later the constraint must be solved in the elaborator.
-            if (has_meta_context(u))
-                m_up->add_eq(ctx, u, Type());
-            else
+            if (is_metavar(u) && !has_meta_context(u)) {
+                // cheap case
                 m_menv->assign(u, Type());
+            } else {
+                m_up->add_eq(ctx, u, Type());
+            }
             return level();
         }
         throw type_expected_exception(m_env, ctx, t);
@@ -136,7 +136,7 @@ class type_checker::imp {
                     r = f_t;
                     break;
                 }
-                check_pi(f_t, e, ctx);
+                f_t = check_pi(f_t, e, ctx);
             }
             break;
         }
diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index bf1dba7dc3..b44d32b199 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -39,13 +39,24 @@ public:
         for (auto c : up.m_eqs)
             std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " == " << std::get<2>(c) << "\n";
         for (auto c : up.m_type_of_eqs)
-            std::cout << std::get<0>(c) << " |- typeof(" << std::get<1>(c) << ") == " << std::get<2>(c) << "\n";
+            std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " : " << std::get<2>(c) << "\n";
         for (auto c : up.m_is_convertible_cnstrs)
-            std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " --> " << std::get<2>(c) << "\n";
+            std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " == " << std::get<2>(c) << "\n";
         return out;
     }
 };
 
+std::ostream & operator<<(std::ostream & out, metavar_env const & env) {
+    bool first = true;
+    for (unsigned i = 0; i < env.size(); i++) {
+        if (env.is_assigned(i)) {
+            if (first) first = false; else out << "\n";
+            out << "?M" << i << " <- " << env.get_subst(i);
+        }
+    }
+    return out;
+}
+
 static void tst1() {
     unification_problems_dbg u;
     metavar_env          menv;
@@ -509,6 +520,24 @@ static void tst24() {
     std::cout << instantiate_metavars(f(m1), menv) << "\n";
 }
 
+static void tst25() {
+    environment env;
+    metavar_env menv;
+    unification_problems_dbg up;
+    type_checker checker(env);
+    expr N = Const("N");
+    expr a = Const("a");
+    expr b = Const("b");
+    env.add_var("N", Type());
+    env.add_var("a", N);
+    env.add_var("b", N);
+    expr m = menv.mk_metavar();
+    expr F = m(a, b);
+    std::cout << checker.infer_type(F, context(), &menv, &up) << "\n";
+    std::cout << menv << "\n";
+    std::cout << up << "\n";
+}
+
 int main() {
     tst1();
     tst2();
@@ -534,5 +563,6 @@ int main() {
     tst22();
     tst23();
     tst24();
+    tst25();
     return has_violations() ? 1 : 0;
 }