Add basic support for metavariables at is_convertible. Swap is_convertible arguments to make it more intuitive.

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

src/frontends/lean/elaborator.cpp

@@ -283,7 +283,7 @@ class elaborator::imp {
                     expr expected = abst_domain(f_t);
                     expr given    = types[i];
                     if (!has_metavar(expected) && !has_metavar(given)) {
-                        if (is_convertible(expected, given, ctx)) {
+                        if (is_convertible(given, expected, ctx)) {
                             // compatible
                         } else if (m_frontend.get_coercion(given, expected, ctx)) {
                             // compatible if using coercion
@@ -403,7 +403,7 @@ class elaborator::imp {
                         info_ref r = mk_app_mismatch_info(e, ctx, args.size(), args.data(), types.data());
                         m_constraints.push_back(constraint(expected, given, ctx, r));
                     } else {
-                        if (!is_convertible(expected, given, ctx)) {
+                        if (!is_convertible(given, expected, ctx)) {
                             expr coercion = m_frontend.get_coercion(given, expected, ctx);
                             if (coercion) {
                                 modified = true;
@@ -459,7 +459,7 @@ class elaborator::imp {
                     info_ref r = mk_expected_type_info(let_value(e), v_p.first, expected, given, ctx);
                     m_constraints.push_back(constraint(expected, given, ctx, r));
                 } else {
-                    if (!is_convertible(expected, given, ctx)) {
+                    if (!is_convertible(given, expected, ctx)) {
                         expr coercion = m_frontend.get_coercion(given, expected, ctx);
                         if (coercion) {
                             v_p.first = mk_app(coercion, v_p.first);

src/kernel/environment.cpp

@@ -224,7 +224,7 @@ struct environment::imp {
     void check_type(name const & n, expr const & t, expr const & v, environment const & env) {
         m_type_checker.infer_universe(t);
         expr v_t = m_type_checker.infer_type(v);
-        if (!m_type_checker.is_convertible(t, v_t))
+        if (!m_type_checker.is_convertible(v_t, t))
             throw def_type_mismatch_exception(env, n, t, v, v_t);
     }
 

src/kernel/metavar.cpp

@@ -107,6 +107,9 @@ void metavar_env::assign(expr const & m, expr const & t) {
 }
 
 expr instantiate_metavars(expr const & e, metavar_env const & env) {
+    if (!has_metavar(e)) {
+        return e;
+    } else {
         auto f = [=](expr const & m, unsigned offset) -> expr {
             if (is_metavar(m) && env.contains(m)) {
                 expr s = env.get_subst(m);
@@ -116,6 +119,7 @@ expr instantiate_metavars(expr const & e, metavar_env const & env) {
             }
         };
         return replace_fn<decltype(f)>(f)(e);
+    }
 }
 
 meta_ctx add_lift(meta_ctx const & ctx, unsigned s, unsigned n) {

src/kernel/metavar.h

@@ -16,6 +16,7 @@ namespace lean {
    It store two kinds of problems:
    1. <tt>ctx |- lhs == rhs</tt>
    2. <tt>ctx |- typeof(n) == t</tt>
+   3. <tt>ctx |- t1 is_convertible_to t2</tt>
 */
 class unification_problems {
 public:
@@ -28,6 +29,12 @@ public:
        \brief Add a new unification problem of the form <tt>ctx |- typeof(n) == t</tt>
     */
     virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) = 0;
+    /**
+       \brief Add a new problem of the form <tt>ctx |- t1 is_convertible_to t2</tt>
+
+       \remark <tt>ctx |- t1 == t2</tt> implies <tt>ctx |- t1 is_convertible_to t2</tt>
+    */
+    virtual void add_is_convertible(context const & ctx, expr const & t1, expr const & t2) = 0;
 };
 
 /**

src/kernel/normalizer.cpp

@@ -292,12 +292,12 @@ class normalizer::imp {
         return r;
     }
 
-    bool is_convertible_core(expr const & expected, expr const & given) {
+    bool is_convertible_core(expr const & given, expr const & expected) {
-        if (expected == given) {
+        if (given == expected) {
             return true;
         } else {
-            expr const * e = &expected;
             expr const * g = &given;
+            expr const * e = &expected;
             while (true) {
                 if (is_type(*e) && is_type(*g)) {
                     if (m_env.is_ge(ty_level(*e), ty_level(*g)))
@@ -308,8 +308,8 @@ class normalizer::imp {
                     return true;
 
                 if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) {
-                    e = &abst_body(*e);
                     g = &abst_body(*g);
+                    e = &abst_body(*e);
                 } else {
                     return false;
                 }
@@ -355,14 +355,31 @@ public:
         return reify(normalize(e, value_stack(), k), k);
     }
 
-    bool is_convertible(expr const & expected, expr const & given, context const & ctx) {
+    bool is_convertible(expr const & given, expr const & expected, context const & ctx,
-        if (is_convertible_core(expected, given))
+                        metavar_env * menv, unification_problems * up) {
+        if (is_convertible_core(given, expected))
             return true;
+        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 (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;
+            }
+        }
+        set_menv(menv);
         set_ctx(ctx);
         unsigned k   = m_ctx.size();
-        expr e_n = reify(normalize(expected, value_stack(), k), k);
+        new_given    = reify(normalize(new_given, value_stack(), k), k);
-        expr g_n = reify(normalize(given, value_stack(), k), k);
+        new_expected = reify(normalize(new_expected, value_stack(), k), k);
-        return is_convertible_core(e_n, g_n);
+        return is_convertible_core(new_given, new_expected);
     }
 
     void clear() { m_ctx = context(); m_cache.clear(); m_menv = nullptr; m_menv_timestamp = 0; }
@@ -374,15 +391,19 @@ normalizer::normalizer(environment const & env):normalizer(env, std::numeric_lim
 normalizer::normalizer(environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {}
 normalizer::~normalizer() {}
 expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const * menv) { return (*m_ptr)(e, ctx, menv); }
-bool normalizer::is_convertible(expr const & t1, expr const & t2, context const & ctx) { return m_ptr->is_convertible(t1, t2, ctx); }
+bool normalizer::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);
+}
 void normalizer::clear() { m_ptr->clear(); }
 void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
 
 expr normalize(expr const & e, environment const & env, context const & ctx, metavar_env const * menv) {
     return normalizer(env)(e, ctx, menv);
 }
-bool is_convertible(expr const & expected, expr const & given, environment const & env, context const & ctx) {
+bool is_convertible(expr const & given, expr const & expected, environment const & env, context const & ctx,
-    return normalizer(env).is_convertible(expected, given, ctx);
+                    metavar_env * menv, unification_problems * up) {
+    return normalizer(env).is_convertible(given, expected, ctx, menv, up);
 }
 }
 

src/kernel/normalizer.h

@@ -14,6 +14,7 @@ namespace lean {
 class environment;
 class options;
 class metavar_env;
+class unification_problems;
 /** \brief Functional object for normalizing expressions */
 class normalizer {
     class imp;
@@ -25,7 +26,8 @@ public:
     ~normalizer();
 
     expr operator()(expr const & e, context const & ctx = context(), metavar_env const * menv = nullptr);
-    bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context());
+    bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context(),
+                        metavar_env * menv = nullptr, unification_problems * up = nullptr);
 
     void clear();
 
@@ -35,5 +37,6 @@ public:
 };
 /** \brief Normalize \c e using the environment \c env and context \c ctx */
 expr normalize(expr const & e, environment const & env, context const & ctx = context(), metavar_env const * menv = nullptr);
-bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context());
+bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context(),
+                    metavar_env * menv = nullptr, unification_problems * up = nullptr);
 }

src/kernel/type_checker.cpp

@@ -94,7 +94,7 @@ public:
             while (true) {
                 expr const & c   = arg(e, i);
                 expr const & c_t = arg_types[i];
-                if (!m_normalizer.is_convertible(abst_domain(f_t), c_t, ctx))
+                if (!m_normalizer.is_convertible(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);
@@ -140,7 +140,7 @@ public:
             expr lt = infer_type(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(let_type(e), lt, ctx))
+                if (!m_normalizer.is_convertible(lt, let_type(e), ctx))
                     throw def_type_mismatch_exception(m_env, ctx, let_name(e), let_type(e), let_value(e), lt);
             }
             {

src/tests/kernel/metavar.cpp

@@ -20,13 +20,16 @@ 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;
 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; }
 };
 
 static void tst1() {