Add support for metavariables in the type checker.

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

src/kernel/metavar.cpp

@@ -67,6 +67,10 @@ void metavar_env::assign(unsigned midx, expr const & v) {
     m_env[midx] = data(v, p->m_type, p->m_ctx);
 }
 
+context const & metavar_env::get_context(unsigned midx) const {
+    return m_env[midx].m_ctx;
+}
+
 expr instantiate(expr const & s, meta_ctx const & ctx, metavar_env const & env) {
     if (ctx) {
         expr r = instantiate(s, tail(ctx), env);

src/kernel/metavar.h

@@ -110,6 +110,11 @@ public:
     */
     void assign(unsigned midx, expr const & t);
 
+    /**
+       \brief Return the context associated with a metavariable.
+    */
+    context const & get_context(unsigned midx) const;
+
     /**
        \brief Return true if this environment contains the given metavariable
 

src/kernel/normalizer.cpp

@@ -362,16 +362,22 @@ public:
         expr new_given    = given;
         expr new_expected = expected;
         if (has_metavar(new_given) || has_metavar(new_expected)) {
-            expr new_given    = instantiate_metavars(new_given, *menv);
-            expr new_expected = instantiate_metavars(new_expected, *menv);
+            if (!menv)
+                return false;
+            new_given    = instantiate_metavars(new_given, *menv);
+            new_expected = instantiate_metavars(new_expected, *menv);
             if (is_convertible_core(new_given, new_expected))
                 return true;
             if (has_metavar(new_given) || has_metavar(new_expected)) {
                 // Very conservative approach, just postpone the problem.
                 // We may also try to normalize new_given and new_expected even if
                 // they contain metavariables.
-                up->add_is_convertible(ctx, new_given, new_expected);
-                return true;
+                if (up) {
+                    up->add_is_convertible(ctx, new_given, new_expected);
+                    return true;
+                } else {
+                    return false;
+                }
             }
         }
         set_menv(menv);

src/kernel/replace.h

@@ -23,10 +23,10 @@ public:
    \brief Functional for applying <tt>F</tt> to the subexpressions of a given expression.
 
    The signature of \c F is
-   unsigned, expr -> expr
+   expr const &, unsigned -> expr
 
    F is invoked for each subexpression \c s of the input expression e.
-   In a call <tt>F(n, s)</tt>, n is the scope level, i.e., the number of
+   In a call <tt>F(s, n)</tt>, n is the scope level, i.e., the number of
    bindings operators that enclosing \c s.
 
    P is a "post-processing" functional object that is applied to each

src/kernel/type_checker.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/scoped_map.h"
+#include "util/flet.h"
 #include "kernel/type_checker.h"
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
@@ -12,16 +13,21 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/builtin.h"
 #include "kernel/free_vars.h"
+#include "kernel/metavar.h"
 
 namespace lean {
+static name g_x_name("x");
 /** \brief Auxiliary functional object used to implement infer_type. */
 class type_checker::imp {
     typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
 
-    environment const & m_env;
-    cache               m_cache;
-    normalizer          m_normalizer;
-    volatile bool       m_interrupted;
+    environment const &    m_env;
+    cache                  m_cache;
+    normalizer             m_normalizer;
+    metavar_env *          m_menv;
+    unsigned               m_menv_timestamp;
+    unification_problems * m_up;
+    volatile bool          m_interrupted;
 
     expr lookup(context const & c, unsigned i) {
         auto p = lookup_ext(c, i);
@@ -37,26 +43,48 @@ 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));
+            // 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_context(r)) {
+                // r contains lift/inst operations, so we put the constraint in m_up
+                m_up->add_eq(ctx, r, p);
+            } else {
+                m_menv->assign(r, p);
+            }
+            return p;
+        }
         throw function_expected_exception(m_env, ctx, s);
     }
 
-public:
-    imp(environment const & env):
-        m_env(env),
-        m_normalizer(env) {
-        m_interrupted = false;
-    }
-
-    level infer_universe(expr const & t, context const & ctx) {
-        expr u = m_normalizer(infer_type(t, ctx), ctx);
+    level infer_universe_core(expr const & t, context const & ctx) {
+        expr u = m_normalizer(infer_type_core(t, ctx), ctx);
         if (is_type(u))
             return ty_level(u);
         if (u == Bool)
             return level();
+        if (is_metavar(u) && m_up) {
+            lean_assert(!m_menv->is_assigned(u));
+            // 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_context(u))
+                m_up->add_eq(ctx, u, Type());
+            else
+                m_menv->assign(u, Type());
+            return level();
+        }
         throw type_expected_exception(m_env, ctx, t);
     }
 
-    expr infer_type(expr const & e, context const & ctx) {
+    expr infer_type_core(expr const & e, context const & ctx) {
         check_interrupted(m_interrupted);
         bool shared = false;
         if (is_shared(e)) {
@@ -69,10 +97,11 @@ public:
         expr r;
         switch (e.kind()) {
         case expr_kind::MetaVar:
-            // TODO(Leo) The following code should be unreachable in the current implementation.
-            // It will be needed when we implement the new elaborator.
-            lean_unreachable();
-            return e;
+            if (m_menv && m_up) {
+                return m_menv->get_type(e, *m_up);
+            } else {
+                throw kernel_exception(m_env, "unexpected metavariable occurrence");
+            }
         case expr_kind::Constant:
             r = m_env.get_object(const_name(e)).get_type();
             break;
@@ -87,14 +116,14 @@ public:
             lean_assert(num >= 2);
             buffer<expr> arg_types;
             for (unsigned i = 0; i < num; i++) {
-                arg_types.push_back(infer_type(arg(e, i), ctx));
+                arg_types.push_back(infer_type_core(arg(e, i), ctx));
             }
             expr f_t     = check_pi(arg_types[0], e, ctx);
             unsigned i   = 1;
             while (true) {
                 expr const & c   = arg(e, i);
                 expr const & c_t = arg_types[i];
-                if (!m_normalizer.is_convertible(c_t, abst_domain(f_t), ctx))
+                if (!is_convertible_core(c_t, abst_domain(f_t), ctx))
                     throw app_type_mismatch_exception(m_env, ctx, e, arg_types.size(), arg_types.data());
                 if (closed(abst_body(f_t)))
                     f_t = abst_body(f_t);
@@ -112,40 +141,40 @@ public:
             break;
         }
         case expr_kind::Eq:
-            infer_type(eq_lhs(e), ctx);
-            infer_type(eq_rhs(e), ctx);
+            infer_type_core(eq_lhs(e), ctx);
+            infer_type_core(eq_rhs(e), ctx);
             r = mk_bool_type();
             break;
         case expr_kind::Lambda: {
-            infer_universe(abst_domain(e), ctx);
+            infer_universe_core(abst_domain(e), ctx);
             expr t;
             {
                 cache::mk_scope sc(m_cache);
-                t = infer_type(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
+                t = infer_type_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
             }
             r = mk_pi(abst_name(e), abst_domain(e), t);
             break;
         }
         case expr_kind::Pi: {
-            level l1 = infer_universe(abst_domain(e), ctx);
+            level l1 = infer_universe_core(abst_domain(e), ctx);
             level l2;
             {
                 cache::mk_scope sc(m_cache);
-                l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
+                l2 = infer_universe_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
             }
             r = mk_type(max(l1, l2));
             break;
         }
         case expr_kind::Let: {
-            expr lt = infer_type(let_value(e), ctx);
+            expr lt = infer_type_core(let_value(e), ctx);
             if (let_type(e)) {
-                infer_universe(let_type(e), ctx); // check if it is really a type
-                if (!m_normalizer.is_convertible(lt, let_type(e), ctx))
+                infer_universe_core(let_type(e), ctx); // check if it is really a type
+                if (!is_convertible_core(lt, let_type(e), ctx))
                     throw def_type_mismatch_exception(m_env, ctx, let_name(e), let_type(e), let_value(e), lt);
             }
             {
                 cache::mk_scope sc(m_cache);
-                expr t = infer_type(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
+                expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
                 r = instantiate(t, let_value(e));
             }
             break;
@@ -169,8 +198,50 @@ public:
         return r;
     }
 
-    bool is_convertible(expr const & t1, expr const & t2, context const & ctx) {
-        return m_normalizer.is_convertible(t1, t2, ctx);
+    bool is_convertible_core(expr const & t1, expr const & t2, context const & ctx) {
+        return m_normalizer.is_convertible(t1, t2, ctx, m_menv, m_up);
+    }
+
+    void set_menv(metavar_env * menv) {
+        if (m_menv == menv) {
+            // Check whether m_menv has been updated since the last time the normalizer has been invoked
+            if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) {
+                clear();
+                m_menv_timestamp = m_menv->get_timestamp();
+            }
+        } else {
+            clear();
+            m_menv = menv;
+            m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0;
+        }
+    }
+
+public:
+    imp(environment const & env):
+        m_env(env),
+        m_normalizer(env) {
+        m_menv           = nullptr;
+        m_menv_timestamp = 0;
+        m_up             = nullptr;
+        m_interrupted    = false;
+    }
+
+    level infer_universe(expr const & t, context const & ctx, metavar_env * menv, unification_problems * up) {
+        set_menv(menv);
+        flet<unification_problems*> set(m_up, up);
+        return infer_universe_core(t, ctx);
+    }
+
+    expr infer_type(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) {
+        set_menv(menv);
+        flet<unification_problems*> set(m_up, up);
+        return infer_type_core(e, ctx);
+    }
+
+    bool is_convertible(expr const & t1, expr const & t2, context const & ctx, metavar_env * menv, unification_problems * up) {
+        set_menv(menv);
+        flet<unification_problems*> set(m_up, up);
+        return is_convertible_core(t1, t2, ctx);
     }
 
     void set_interrupt(bool flag) {
@@ -190,11 +261,17 @@ public:
 
 type_checker::type_checker(environment const & env):m_ptr(new imp(env)) {}
 type_checker::~type_checker() {}
-expr type_checker::infer_type(expr const & e, context const & ctx) { return m_ptr->infer_type(e, ctx); }
-level type_checker::infer_universe(expr const & e, context const & ctx) { return m_ptr->infer_universe(e, ctx); }
+expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) {
+    return m_ptr->infer_type(e, ctx, menv, up);
+}
+level type_checker::infer_universe(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) {
+    return m_ptr->infer_universe(e, ctx, menv, up);
+}
 void type_checker::clear() { m_ptr->clear(); }
 void type_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
-bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) { return m_ptr->is_convertible(t1, t2, ctx); }
+bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx, metavar_env * menv, unification_problems * up) {
+    return m_ptr->is_convertible(t1, t2, ctx, menv, up);
+}
 normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); }
 
 expr  infer_type(expr const & e, environment const & env, context const & ctx) {

src/kernel/type_checker.h

@@ -12,6 +12,8 @@ Author: Leonardo de Moura
 namespace lean {
 class environment;
 class normalizer;
+class metavar_env;
+class unification_problems;
 /**
    \brief Lean Type Checker. It can also be used to infer types, universes and check whether a
    type \c A is convertible to a type \c B.
@@ -23,10 +25,19 @@ public:
     type_checker(environment const & env);
     ~type_checker();
 
-    expr infer_type(expr const & e, context const & ctx = context());
-    level infer_universe(expr const & e, context const & ctx = context());
-    void check(expr const & e, context const & ctx = context()) { infer_type(e, ctx); }
-    bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context());
+    expr infer_type(expr const & e, context const & ctx = context(),
+                    metavar_env * menv = nullptr, unification_problems * up = nullptr);
+
+    level infer_universe(expr const & e, context const & ctx = context(),
+                         metavar_env * menv = nullptr, unification_problems * up = nullptr);
+
+    void check(expr const & e, context const & ctx = context(),
+               metavar_env * menv = nullptr, unification_problems * up = nullptr) {
+        infer_type(e, ctx, menv, up);
+    }
+
+    bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context(),
+                        metavar_env * menv = nullptr, unification_problems * up = nullptr);
 
     void clear();
 

src/library/placeholder.cpp

@@ -5,7 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/occurs.h"
+#include "kernel/metavar.h"
+#include "kernel/expr_maps.h"
+#include "kernel/replace.h"
 #include "library/placeholder.h"
+#include "library/replace_using_ctx.h"
 
 namespace lean {
 static name g_placeholder_name("_");
@@ -20,4 +24,19 @@ bool is_placeholder(expr const & e) {
 bool has_placeholder(expr const & e) {
     return occurs(mk_placholder(), e);
 }
+
+expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map<expr> * trace) {
+    auto f = [&](expr const & e, context const & ctx, unsigned offset) -> expr {
+        if (is_placeholder(e)) {
+            return menv.mk_metavar(ctx);
+        } else {
+            return e;
+        }
+    };
+    auto p = [&](expr const & s, expr const & t) {
+        if (trace)
+            (*trace)[t] = s;
+    };
+    return replace_using_ctx_fn<decltype(f), decltype(p)>(f, p)(e);
+}
 }

src/library/placeholder.h

@@ -6,8 +6,10 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/expr.h"
+#include "kernel/expr_maps.h"
 
 namespace lean {
+class metavar_env;
 /**
     \brief Return a new placeholder expression. To be able to track location,
     a new constant for each placeholder.
@@ -23,4 +25,11 @@ bool is_placeholder(expr const & e);
     \brief Return true iff the given expression contains placeholders.
 */
 bool has_placeholder(expr const & e);
+
+/**
+   \brief Replace the placeholders in \c e with fresh metavariables from menv.
+   if \c trace is not null, then for each new expression \c t created based on
+   \c s, we store <tt>(*trace)[t] = s</tt>. We say this is traceability information.
+*/
+expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map<expr> * trace = nullptr);
 }

src/library/replace_using_ctx.h

@@ -0,0 +1,99 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/scoped_map.h"
+#include "kernel/replace.h"
+
+namespace lean {
+/**
+   \brief Functional for applying <tt>F</tt> to the subexpressions of a given expression.
+
+   The signature of \c F is
+   expr const &, context const & ctx, unsigned n -> expr
+
+   F is invoked for each subexpression \c s of the input expression e.
+   In a call <tt>F(s, c, n)</tt>, \c c is the context where \c s occurs,
+   and \c n is the size of \c c.
+
+   P is a "post-processing" functional object that is applied to each
+   pair (old, new)
+*/
+template<typename F, typename P = default_replace_postprocessor>
+class replace_using_ctx_fn {
+    static_assert(std::is_same<typename std::result_of<F(expr const &, context const &, unsigned)>::type, expr>::value,
+                  "replace_using_ctx_fn: return type of F is not expr");
+    typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
+    cache                      m_cache;
+    F                          m_f;
+    P                          m_post;
+
+    expr apply(expr const & e, context const & ctx, unsigned offset) {
+        bool shared = false;
+        if (is_shared(e)) {
+            shared = true;
+            auto it = m_cache.find(e);
+            if (it != m_cache.end())
+                return it->second;
+        }
+
+        expr r = m_f(e, ctx, offset);
+        if (is_eqp(e, r)) {
+            switch (e.kind()) {
+            case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant:
+            case expr_kind::Var: case expr_kind::MetaVar:
+                break;
+            case expr_kind::App:
+                r = update_app(e, [=](expr const & c) { return apply(c, ctx, offset); });
+                break;
+            case expr_kind::Eq:
+                r = update_eq(e, [=](expr const & l, expr const & r) { return std::make_pair(apply(l, ctx, offset), apply(r, ctx, offset)); });
+                break;
+            case expr_kind::Lambda:
+            case expr_kind::Pi:
+                r = update_abst(e, [=](expr const & t, expr const & b) {
+                        expr new_t = apply(t, ctx, offset);
+                        expr new_b;
+                        {
+                            cache::mk_scope sc(m_cache);
+                            new_b = apply(b, extend(ctx, abst_name(e), new_t), offset + 1);
+                        }
+                        return std::make_pair(new_t, new_b);
+                    });
+                break;
+            case expr_kind::Let:
+                r = update_let(e, [=](expr const & t, expr const & v, expr const & b) {
+                        expr new_t = t ? apply(t, ctx, offset) : expr();
+                        expr new_v = apply(v, ctx, offset);
+                        expr new_b;
+                        {
+                            cache::mk_scope sc(m_cache);
+                            new_b  = apply(b, extend(ctx, abst_name(e), new_t, new_v), offset+1);
+                        }
+                        return std::make_tuple(new_t, new_v, new_b);
+                    });
+                break;
+            }
+        }
+
+        if (shared)
+            m_cache.insert(std::make_pair(e, r));
+
+        m_post(e, r);
+        return r;
+    }
+
+public:
+    replace_using_ctx_fn(F const & f, P const & p = P()):
+        m_f(f),
+        m_post(p) {
+    }
+
+    expr operator()(expr const & e, context const & ctx = context()) {
+        return apply(e, ctx, ctx.size());
+    }
+};
+}

src/tests/kernel/metavar.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <iostream>
 #include <algorithm>
 #include <vector>
 #include <utility>
@@ -14,22 +15,35 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/normalizer.h"
 #include "kernel/environment.h"
+#include "kernel/type_checker.h"
 #include "library/printer.h"
+#include "library/placeholder.h"
 using namespace lean;
 
 class unification_problems_dbg : public unification_problems {
-    std::vector<std::pair<expr, expr>> m_eqs;
-    std::vector<std::pair<expr, expr>> m_type_of_eqs;
-    std::vector<std::pair<expr, expr>> m_is_convertible_cnstrs;
+    typedef std::tuple<context, expr, expr> constraint;
+    typedef std::vector<constraint>         constraints;
+    constraints m_eqs;
+    constraints m_type_of_eqs;
+    constraints m_is_convertible_cnstrs;
 public:
     unification_problems_dbg() {}
     virtual ~unification_problems_dbg() {}
-    virtual void add_eq(context const &, expr const & lhs, expr const & rhs) { m_eqs.push_back(mk_pair(lhs, rhs)); }
-    virtual void add_type_of_eq(context const &, expr const & n, expr const & t) { m_type_of_eqs.push_back(mk_pair(n, t)); }
-    virtual void add_is_convertible(context const &, expr const & t1, expr const & t2) { m_is_convertible_cnstrs.push_back(mk_pair(t1, t2)); }
-    std::vector<std::pair<expr, expr>> const & eqs() const { return m_eqs; }
-    std::vector<std::pair<expr, expr>> const & type_of_eqs() const { return m_type_of_eqs; }
-    std::vector<std::pair<expr, expr>> const & is_convertible_cnstrs() const { return m_is_convertible_cnstrs; }
+    virtual void add_eq(context const & ctx, expr const & lhs, expr const & rhs) { m_eqs.push_back(constraint(ctx, lhs, rhs)); }
+    virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) { m_type_of_eqs.push_back(constraint(ctx, n, t)); }
+    virtual void add_is_convertible(context const & ctx, expr const & t1, expr const & t2) { m_is_convertible_cnstrs.push_back(constraint(ctx, t1, t2)); }
+    constraints const & eqs() const { return m_eqs; }
+    constraints const & type_of_eqs() const { return m_type_of_eqs; }
+    constraints const & is_convertible_cnstrs() const { return m_is_convertible_cnstrs; }
+    friend std::ostream & operator<<(std::ostream & out, unification_problems_dbg const & up) {
+        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";
+        for (auto c : up.m_is_convertible_cnstrs)
+            std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " --> " << std::get<2>(c) << "\n";
+        return out;
+    }
 };
 
 static void tst1() {
@@ -56,7 +70,7 @@ static void tst1() {
     lean_assert(u.eqs().empty());
     lean_assert(u.type_of_eqs().size() == 2);
     for (auto p : u.type_of_eqs()) {
-        std::cout << "typeof(" << p.first << ") == " << p.second << "\n";
+        std::cout << "typeof(" << std::get<1>(p) << ") == " << std::get<2>(p) << "\n";
     }
     expr f = Const("f");
     expr a = Const("a");
@@ -446,6 +460,43 @@ static void tst21() {
                 add_lift(m1, 1, 7));
 }
 
+#define _ mk_placholder()
+
+static void tst22() {
+    metavar_env menv;
+    expr f = Const("f");
+    expr x = Const("x");
+    expr N = Const("N");
+    expr F = f(Fun({x, N}, f(_, x)), _);
+    std::cout << F << "\n";
+    std::cout << replace_placeholders_with_metavars(F, menv) << "\n";
+    lean_assert(menv.contains(0));
+    lean_assert(menv.contains(1));
+    lean_assert(!menv.contains(2));
+    lean_assert(menv.get_context(0).size() == 1);
+    lean_assert(lookup(menv.get_context(0), 0).get_domain() == N);
+    lean_assert(menv.get_context(1).size() == 0);
+}
+
+static void tst23() {
+    environment env;
+    metavar_env menv;
+    unification_problems_dbg up;
+    type_checker checker(env);
+    expr N  = Const("N");
+    expr f  = Const("f");
+    expr a  = Const("a");
+    env.add_var("N", Type());
+    env.add_var("f", N >> (N >> N));
+    env.add_var("a", N);
+    expr x  = Const("x");
+    expr F0 = f(Fun({x, N}, f(_, x))(a), _);
+    expr F1 = replace_placeholders_with_metavars(F0, menv);
+    std::cout << F1 << "\n";
+    std::cout << checker.infer_type(F1, context(), &menv, &up) << "\n";
+    std::cout << up << "\n";
+}
+
 int main() {
     tst1();
     tst2();
@@ -468,5 +519,7 @@ int main() {
     tst19();
     tst20();
     tst21();
+    tst22();
+    tst23();
     return has_violations() ? 1 : 0;
 }