From faee08591f011500d3d5e6472aceb0b5d6ff06c3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Jul 2014 12:01:06 -0700
Subject: [PATCH] fix(*): make sure elaborator and type_checker use the same
 "rules" for treating opaque definitions

This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_cmds.cpp      |   4 +-
 src/frontends/lean/decl_cmds.cpp         |   4 +-
 src/frontends/lean/elaborator.cpp        |  91 +++++----
 src/frontends/lean/elaborator.h          |   6 +-
 src/frontends/lean/inductive_cmd.cpp     |   4 +-
 src/frontends/lean/parser.cpp            |  20 +-
 src/frontends/lean/parser.h              |   5 +-
 src/frontends/lean/theorem_queue.cpp     |   3 +-
 src/kernel/constraint.cpp                |  26 +--
 src/kernel/constraint.h                  |  15 +-
 src/kernel/converter.cpp                 |   9 +
 src/kernel/converter.h                   |   1 +
 src/kernel/type_checker.cpp              |   4 +
 src/kernel/type_checker.h                |   1 +
 src/library/inductive_unifier_plugin.cpp |  15 +-
 src/library/kernel_bindings.cpp          |  16 +-
 src/library/opaque_hints.cpp             |  10 +-
 src/library/opaque_hints.h               |  11 +-
 src/library/tactic/apply_tactic.cpp      |  14 +-
 src/library/tactic/apply_tactic.h        |   4 +-
 src/library/unifier.cpp                  | 226 +++++++++++++----------
 src/library/unifier.h                    |   6 +-
 src/tests/library/unifier.cpp            |   2 +-
 tests/lean/run/class4.lean               |   1 +
 tests/lean/run/uni.lean                  |   2 +-
 tests/lean/run/uni2.lean                 |   2 +-
 tests/lean/run/univ2.lean                |  11 ++
 tests/lua/unify2.lua                     |   2 +-
 tests/lua/unify4.lua                     |   2 +-
 29 files changed, 303 insertions(+), 214 deletions(-)
 create mode 100644 tests/lean/run/univ2.lean

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index ea678aeb2..54a5c5ccf 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -86,7 +86,7 @@ environment check_cmd(parser & p) {
     level_param_names ls = to_level_param_names(collect_univ_params(e));
     level_param_names new_ls;
     std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);
-    auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen());
+    auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen(), true);
     expr type = tc->check(e, append(ls, new_ls));
     auto reg              = p.regular_stream();
     formatter const & fmt = reg.get_formatter();
@@ -270,7 +270,7 @@ environment opaque_hint_cmd(parser & p) {
             if (p.curr_is_token(g_module)) {
                 found = true;
                 p.next();
-                env = set_main_module_opaque_defs(env, hiding);
+                env = set_hide_main_opaque(env, hiding);
             } else {
                 name c  = p.check_constant_next("invalid 'opaque_hint', constant expected");
                 found   = true;
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 09daad7a5..a5f464a63 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -271,11 +271,11 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
             std::tie(type, new_ls) = p.elaborate_type(type);
             env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type)));
         } else {
-            std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
+            std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque);
             env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value)));
         }
     } else {
-        std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
+        std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque);
         env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque)));
     }
     if (real_n != n)
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 9314f7066..2a626a776 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -131,7 +131,7 @@ class elaborator {
     local_decls<level>  m_lls;
     io_state            m_ios;
     name_generator      m_ngen;
-    type_checker_ptr    m_tc;
+    type_checker_ptr    m_tc[2];
     substitution        m_subst;
     expr_map<expr>      m_cache; // (pointer equality) cache for Type and Constants (this is a trick to make sure we get the
                                  // same universe metavariable for different occurrences of the same Type/Constant
@@ -148,6 +148,7 @@ class elaborator {
     name_set            m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned
     bool                m_check_unassigned; // if true if display error messages if elaborated term still contains metavariables
     bool                m_use_local_instances; // if true class-instance resolution will use the local context
+    bool                m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent
 
     // Set m_ctx to ctx, and make sure m_ctx_buffer and m_ctx_domain_buffer reflect the contents of the new ctx
     void set_ctx(context const & ctx) {
@@ -173,12 +174,14 @@ class elaborator {
             lean_assert(m_main.m_accumulated.is_none());
             m_old_ctx    = m_main.m_ctx;
             m_main.set_ctx(ctx);
-            m_main.m_tc->push();
+            m_main.m_tc[0]->push();
+            m_main.m_tc[1]->push();
             m_main.m_subst = s;
         }
         ~scope() {
             m_main.set_ctx(m_old_ctx);
-            m_main.m_tc->pop();
+            m_main.m_tc[0]->pop();
+            m_main.m_tc[1]->pop();
             m_main.m_constraints.clear();
             m_main.m_accumulated = justification();
             m_main.m_subst = substitution();
@@ -189,8 +192,9 @@ class elaborator {
 
     /* \brief Move all constraints generated by the type checker to the buffer m_constraints. */
     void consume_tc_cnstrs() {
-        while (auto c = m_tc->next_cnstr())
-            m_constraints.push_back(*c);
+        for (unsigned i = 0; i < 2; i++)
+            while (auto c = m_tc[i]->next_cnstr())
+                m_constraints.push_back(*c);
     }
 
     struct choice_elaborator {
@@ -212,8 +216,9 @@ class elaborator {
         context      m_ctx;
         substitution m_subst;
         unsigned     m_idx;
-        choice_expr_elaborator(elaborator & elab, expr const & mvar, expr const & c, context const & ctx, substitution const & s):
-            m_elab(elab), m_mvar(mvar), m_choice(c), m_ctx(ctx), m_subst(s), m_idx(0) {
+        bool         m_relax_main_opaque;
+        choice_expr_elaborator(elaborator & elab, expr const & mvar, expr const & c, context const & ctx, substitution const & s, bool relax):
+            m_elab(elab), m_mvar(mvar), m_choice(c), m_ctx(ctx), m_subst(s), m_idx(0), m_relax_main_opaque(relax) {
         }
 
         virtual optional<constraints> next() {
@@ -226,7 +231,7 @@ class elaborator {
                     justification j = m_elab.m_accumulated;
                     m_elab.consume_tc_cnstrs();
                     list<constraint> cs = to_list(m_elab.m_constraints.begin(), m_elab.m_constraints.end());
-                    cs = cons(mk_eq_cnstr(m_mvar, r, j), cs);
+                    cs = cons(mk_eq_cnstr(m_mvar, r, j, m_relax_main_opaque), cs);
                     return optional<constraints>(cs);
                 } catch (exception &) {}
             }
@@ -263,13 +268,14 @@ class elaborator {
         context                 m_ctx; // local context for m_meta
         substitution            m_subst;
         justification           m_jst;
+        bool                    m_relax_main_opaque;
 
         placeholder_elaborator(elaborator & elab, expr const & meta, expr const & meta_type,
                                list<expr> const & local_insts, list<name> const & instances, list<tactic_hint_entry> const & tacs,
-                               context const & ctx, substitution const & s, justification const & j, bool ignore_failure):
+                               context const & ctx, substitution const & s, justification const & j, bool ignore_failure, bool relax):
             choice_elaborator(ignore_failure),
             m_elab(elab), m_meta(meta), m_meta_type(meta_type), m_local_instances(local_insts), m_instances(instances),
-            m_tactics(tacs), m_ctx(ctx), m_subst(s), m_jst(j) {
+            m_tactics(tacs), m_ctx(ctx), m_subst(s), m_jst(j), m_relax_main_opaque(relax) {
             collect_metavars(meta_type, m_mvars_in_meta_type);
         }
 
@@ -292,7 +298,7 @@ class elaborator {
                 for (auto & c : m_elab.m_constraints)
                     c = update_justification(c, mk_composite1(m_jst, c.get_justification()));
                 list<constraint> cs = to_list(m_elab.m_constraints.begin(), m_elab.m_constraints.end());
-                cs = cons(mk_eq_cnstr(m_meta, r, mk_composite1(m_jst, j)), cs);
+                cs = cons(mk_eq_cnstr(m_meta, r, mk_composite1(m_jst, j), m_relax_main_opaque), cs);
                 return optional<constraints>(cs);
             } catch (exception &) {
                 return optional<constraints>();
@@ -307,9 +313,9 @@ class elaborator {
                 substitution subst = next->first.get_subst();
                 buffer<constraint> cs;
                 expr const & mvar = get_app_fn(m_meta);
-                cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst));
+                cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, m_relax_main_opaque));
                 for (auto const & mvar : m_mvars_in_meta_type)
-                    cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst));
+                    cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, m_relax_main_opaque));
                 return optional<constraints>(to_list(cs.begin(), cs.end()));
             }
             return optional<constraints>();
@@ -319,7 +325,7 @@ class elaborator {
             while (!empty(m_local_instances)) {
                 expr inst         = head(m_local_instances);
                 m_local_instances = tail(m_local_instances);
-                constraints cs(mk_eq_cnstr(m_meta, inst, m_jst));
+                constraints cs(mk_eq_cnstr(m_meta, inst, m_jst, m_relax_main_opaque));
                 return optional<constraints>(cs);
             }
             while (!empty(m_instances)) {
@@ -362,8 +368,11 @@ public:
     elaborator(environment const & env, local_decls<level> const & lls, list<expr> const & ctx, io_state const & ios, name_generator const & ngen,
                pos_info_provider * pp, bool check_unassigned):
         m_env(env), m_lls(lls), m_ios(ios),
-        m_ngen(ngen), m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child())),
+        m_ngen(ngen),
         m_pos_provider(pp) {
+        m_relax_main_opaque = false;
+        m_tc[0] = mk_type_checker_with_hints(env, m_ngen.mk_child(), false);
+        m_tc[1] = mk_type_checker_with_hints(env, m_ngen.mk_child(), true);
         m_check_unassigned = check_unassigned;
         m_use_local_instances = get_elaborator_local_instances(ios.get_options());
         set_ctx(ctx);
@@ -375,10 +384,11 @@ public:
 
     expr infer_type(expr const & e) {
         lean_assert(closed(e));
-        return m_tc->infer(e); }
+        return m_tc[m_relax_main_opaque]->infer(e);
+    }
 
     expr whnf(expr const & e) {
-        return m_tc->whnf(e);
+        return m_tc[m_relax_main_opaque]->whnf(e);
     }
 
     /** \brief Clear constraint buffer \c m_constraints, and associated datastructures
@@ -593,7 +603,7 @@ public:
                     return lazy_list<constraints>(); // nothing to be done
                 bool ignore_failure = false; // we are always strict with placeholders associated with classes
                 return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, local_insts, insts, tacs, ctx, s, j,
-                                                                       ignore_failure));
+                                                                       ignore_failure, m_relax_main_opaque));
             } else if (s.is_assigned(mvar)) {
                 // if the metavariable is assigned and it is not a class, then we just ignore it, and return
                 // the an empty set of constraints.
@@ -602,10 +612,10 @@ public:
                 list<tactic_hint_entry> tacs = get_tactic_hints(m_env);
                 bool ignore_failure = !is_strict;
                 return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, list<expr>(), list<name>(), tacs, ctx, s, j,
-                                                                       ignore_failure));
+                                                                       ignore_failure, m_relax_main_opaque));
             }
         };
-        add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j));
+        add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j, m_relax_main_opaque));
         return m;
     }
 
@@ -642,11 +652,12 @@ public:
         // Possible optimization: try to lookahead and discard some of the alternatives.
         expr m      = mk_meta(t, e.get_tag());
         context ctx = m_ctx;
+        bool relax = m_relax_main_opaque;
         auto fn = [=](expr const & mvar, expr const & /* type */, substitution const & s, name_generator const & /* ngen */) {
-            return choose(std::make_shared<choice_expr_elaborator>(*this, mvar, e, ctx, s));
+            return choose(std::make_shared<choice_expr_elaborator>(*this, mvar, e, ctx, s, relax));
         };
         justification j = mk_justification("none of the overloads is applicable", some_expr(e));
-        add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), j));
+        add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), j, m_relax_main_opaque));
         return m;
     }
 
@@ -670,7 +681,7 @@ public:
             f_type = whnf(instantiate_metavars(f_type));
             if (!is_pi(f_type) && is_meta(f_type)) {
                 // let type checker add constraint
-                f_type = m_tc->ensure_pi(f_type, f);
+                f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f);
             }
         }
         if (!is_pi(f_type)) {
@@ -710,6 +721,7 @@ public:
     }
 
     constraint mk_delayed_coercion_cnstr(expr const & m, expr const & a, expr const & a_type, justification const & j, unsigned delay_factor) {
+        bool relax = m_relax_main_opaque;
         auto choice_fn = [=](expr const & mvar, expr const & new_d_type, substitution const & /* s */, name_generator const & /* ngen */) {
             // Remark: we want the coercions solved before we start discarding FlexFlex constraints. So, we use PreFlexFlex as a max cap
             // for delaying coercions.
@@ -718,10 +730,10 @@ public:
                 return lazy_list<constraints>(constraints(mk_delayed_coercion_cnstr(m, a, a_type, justification(), delay_factor+1)));
             } else {
                 expr r = apply_coercion(a, a_type, new_d_type);
-                return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, r, justification())));
+                return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, r, justification(), relax)));
             }
         };
-        return mk_choice_cnstr(m, choice_fn, delay_factor, j);
+        return mk_choice_cnstr(m, choice_fn, delay_factor, j, m_relax_main_opaque);
     }
 
     /** \brief Given an application \c e, where the expected type is d_type, and the argument type is a_type,
@@ -792,19 +804,19 @@ public:
             return mk_delayed_coercion(r, d_type, a_type);
         } else {
             app_delayed_justification j(r, f_type, a_type);
-            if (!m_tc->is_def_eq(a_type, d_type, j)) {
+            if (!m_tc[m_relax_main_opaque]->is_def_eq(a_type, d_type, j)) {
                 expr new_a = apply_coercion(a, a_type, d_type);
                 bool coercion_worked = false;
                 if (!is_eqp(a, new_a)) {
                     expr new_a_type = instantiate_metavars(infer_type(new_a));
-                    coercion_worked = m_tc->is_def_eq(new_a_type, d_type, j);
+                    coercion_worked = m_tc[m_relax_main_opaque]->is_def_eq(new_a_type, d_type, j);
                 }
                 if (coercion_worked) {
                     r = update_app(r, f, new_a);
                 } else {
                     if (has_metavar(a_type) || has_metavar(d_type)) {
                         // rely on unification hints to solve this constraint
-                        add_cnstr(mk_eq_cnstr(a_type, d_type, j.get()));
+                        add_cnstr(mk_eq_cnstr(a_type, d_type, j.get(), m_relax_main_opaque));
                     } else {
                         throw_kernel_exception(m_env, r, [=](formatter const & fmt) { return pp_app_type_mismatch(fmt, e, d_type, a_type); });
                     }
@@ -888,7 +900,7 @@ public:
                 return e;
             if (is_meta(t)) {
                 // let type checker add constraint
-                m_tc->ensure_sort(t, e);
+                m_tc[m_relax_main_opaque]->ensure_sort(t, e);
                 return e;
             }
         }
@@ -1112,7 +1124,7 @@ public:
             if (!meta)
                 return;
             meta = instantiate_meta(*meta, subst);
-            expr type = m_tc->infer(*meta);
+            expr type = m_tc[m_relax_main_opaque]->infer(*meta);
             // first solve unassigned metavariables in type
             type = solve_unassigned_mvars(subst, type, visited);
             proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child());
@@ -1173,7 +1185,8 @@ public:
         return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
     }
 
-    std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type) {
+    std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) {
+        flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque && !get_hide_main_opaque(m_env));
         expr r  = visit(e);
         if (_ensure_type)
             r = ensure_type(r);
@@ -1183,16 +1196,18 @@ public:
         return apply(s, r);
     }
 
-    std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n) {
+    std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque) {
         lean_assert(!has_local(t)); lean_assert(!has_local(v));
         expr r_t      = ensure_type(visit(t));
+        // Opaque definitions in the main module may treat other opaque definitions (in the main module) as transparent.
+        flet<bool> set_relax(m_relax_main_opaque, is_opaque && !get_hide_main_opaque(m_env));
         expr r_v      = visit(v);
         expr r_v_type = infer_type(r_v);
         justification j = mk_justification(v, [=](formatter const & fmt, substitution const & subst) {
                 substitution s(subst);
                 return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type));
             });
-        if (!m_tc->is_def_eq(r_v_type, r_t, j)) {
+        if (!m_tc[is_opaque]->is_def_eq(r_v_type, r_t, j)) {
             throw_kernel_exception(m_env, v, [=](formatter const & fmt) { return pp_def_type_mismatch(fmt, n, r_t, r_v_type); });
         }
         auto p  = solve().pull();
@@ -1209,13 +1224,13 @@ public:
 static name g_tmp_prefix = name::mk_internal_unique_name();
 
 std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, list<expr> const & ctx,
-                                              io_state const & ios, expr const & e, pos_info_provider * pp, bool check_unassigned,
-                                              bool ensure_type) {
-    return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type);
+                                              io_state const & ios, expr const & e, bool relax_main_opaque,
+                                              pos_info_provider * pp, bool check_unassigned, bool ensure_type) {
+    return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type, relax_main_opaque);
 }
 
 std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
-                                                    name const & n, expr const & t, expr const & v, pos_info_provider * pp) {
-    return elaborator(env, lls, list<expr>(), ios, name_generator(g_tmp_prefix), pp, true)(t, v, n);
+                                                    name const & n, expr const & t, expr const & v, bool is_opaque, pos_info_provider * pp) {
+    return elaborator(env, lls, list<expr>(), ios, name_generator(g_tmp_prefix), pp, true)(t, v, n, is_opaque);
 }
 }
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 5cd9155fa..128853e3b 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -14,9 +14,9 @@ Author: Leonardo de Moura
 
 namespace lean {
 std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, list<expr> const & ctx,
-                                              io_state const & ios, expr const & e, pos_info_provider * pp = nullptr,
-                                              bool check_unassigned = true, bool ensure_type = false);
+                                              io_state const & ios, expr const & e, bool relax_main_opaque,
+                                              pos_info_provider * pp = nullptr, bool check_unassigned = true, bool ensure_type = false);
 std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls,
                                                     io_state const & ios, name const & n, expr const & t, expr const & v,
-                                                    pos_info_provider * pp = nullptr);
+                                                    bool is_opaque, pos_info_provider * pp = nullptr);
 }
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index 955bbbf9c..80e9d67b6 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -90,7 +90,7 @@ struct inductive_cmd_fn {
         m_u = mk_global_univ(u_name);
         m_infer_result_universe = false;
         m_namespace = get_namespace(m_env);
-        m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen());
+        m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen(), false);
     }
 
     [[ noreturn ]] void throw_error(char const * error_msg) { throw parser_error(error_msg, m_pos); }
@@ -402,7 +402,7 @@ struct inductive_cmd_fn {
             std::tie(d_name, d_type, std::ignore) = d;
             m_env = m_env.add(check(m_env, mk_var_decl(d_name, ls, d_type)));
         }
-        m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen());
+        m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen(), false);
     }
 
     /** \brief Traverse the introduction rule type and collect the universes where non-parameters reside in \c r_lvls.
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index b2bb1341f..211ca5abc 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -485,28 +485,34 @@ level parser::parse_level(unsigned rbp) {
 
 std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, list<expr> const & ctx) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, &pp, false);
+    bool relax            = true;
+    bool check_unassigned = false;
+    return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned);
 }
 
 std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, &pp, true, true);
+    bool relax            = false;
+    bool ensure_type      = true;
+    bool check_unassigned = true;
+    return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type);
 }
 
 std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env, expr const & e) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(env, m_local_level_decls, list<expr>(), m_ios, e, &pp);
+    bool relax            = false;
+    return ::lean::elaborate(env, m_local_level_decls, list<expr>(), m_ios, e, relax, &pp);
 }
 
-std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v) {
+std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, &pp);
+    return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, is_opaque, &pp);
 }
 
 std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, local_level_decls const & lls,
-                                                                          name const & n, expr const & t, expr const & v) {
+                                                                          name const & n, expr const & t, expr const & v, bool is_opaque) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(env, lls, m_ios, n, t, v, &pp);
+    return ::lean::elaborate(env, lls, m_ios, n, t, v, is_opaque, &pp);
 }
 
 [[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) {
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 861aacc00..d7ab996db 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -262,9 +262,10 @@ public:
     /** \brief Elaborate \c e (making sure the result does not have metavariables). */
     std::tuple<expr, level_param_names> elaborate(expr const & e) { return elaborate_at(m_env, e); }
     /** \brief Elaborate the definition n : t := v */
-    std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v);
+    std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque);
     /** \brief Elaborate the definition n : t := v in the given environment*/
-    std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, local_level_decls const & lls, name const & n, expr const & t, expr const & v);
+    std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, local_level_decls const & lls,
+                                                                      name const & n, expr const & t, expr const & v, bool is_opaque);
 
     parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); }
 
diff --git a/src/frontends/lean/theorem_queue.cpp b/src/frontends/lean/theorem_queue.cpp
index b0e0e37e7..08c3fff91 100644
--- a/src/frontends/lean/theorem_queue.cpp
+++ b/src/frontends/lean/theorem_queue.cpp
@@ -16,7 +16,8 @@ void theorem_queue::add(environment const & env, name const & n, level_param_nam
     m_queue.add([=]() {
             level_param_names new_ls;
             expr type, value;
-            std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v);
+            bool is_opaque = true; // theorems are always opaque
+            std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v, is_opaque);
             return check(env, mk_theorem(n, append(ls, new_ls), type, value));
         });
 }
diff --git a/src/kernel/constraint.cpp b/src/kernel/constraint.cpp
index 840f8ac8c..d02fbf025 100644
--- a/src/kernel/constraint.cpp
+++ b/src/kernel/constraint.cpp
@@ -12,28 +12,29 @@ struct constraint_cell {
     MK_LEAN_RC()
     constraint_kind m_kind;
     justification   m_jst;
-    constraint_cell(constraint_kind k, justification const & j):m_rc(1), m_kind(k), m_jst(j) {}
+    bool            m_relax_main_opaque;
+    constraint_cell(constraint_kind k, justification const & j, bool relax):m_rc(1), m_kind(k), m_jst(j), m_relax_main_opaque(relax) {}
 };
 struct eq_constraint_cell : public constraint_cell {
     expr m_lhs;
     expr m_rhs;
-    eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j):
-        constraint_cell(constraint_kind::Eq, j),
+    eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j, bool relax):
+        constraint_cell(constraint_kind::Eq, j, relax),
         m_lhs(lhs), m_rhs(rhs) {}
 };
 struct level_constraint_cell : public constraint_cell {
     level m_lhs;
     level m_rhs;
     level_constraint_cell(level const & lhs, level const & rhs, justification const & j):
-        constraint_cell(constraint_kind::LevelEq, j),
+        constraint_cell(constraint_kind::LevelEq, j, false),
         m_lhs(lhs), m_rhs(rhs) {}
 };
 struct choice_constraint_cell : public constraint_cell {
     expr      m_expr;
     choice_fn m_fn;
     unsigned  m_delay_factor;
-    choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, justification const & j):
-        constraint_cell(constraint_kind::Choice, j),
+    choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax):
+        constraint_cell(constraint_kind::Choice, j, relax),
         m_expr(e), m_fn(fn), m_delay_factor(delay_factor) {}
 };
 
@@ -57,19 +58,20 @@ constraint & constraint::operator=(constraint && c) { LEAN_MOVE_REF(c); }
 constraint_kind constraint::kind() const { lean_assert(m_ptr); return m_ptr->m_kind; }
 justification const & constraint::get_justification() const { lean_assert(m_ptr); return m_ptr->m_jst; }
 
-constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
-    return constraint(new eq_constraint_cell(lhs, rhs, j));
+constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque) {
+    return constraint(new eq_constraint_cell(lhs, rhs, j, relax_main_opaque));
 }
 constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j) {
     return constraint(new level_constraint_cell(lhs, rhs, j));
 }
-constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j) {
+constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax_main_opaque) {
     lean_assert(is_meta(m));
-    return constraint(new choice_constraint_cell(m, fn, delay_factor, j));
+    return constraint(new choice_constraint_cell(m, fn, delay_factor, j, relax_main_opaque));
 }
 
 expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast<eq_constraint_cell*>(c.raw())->m_lhs; }
 expr const & cnstr_rhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast<eq_constraint_cell*>(c.raw())->m_rhs; }
+bool relax_main_opaque(constraint const & c) { return c.raw()->m_relax_main_opaque; }
 level const & cnstr_lhs_level(constraint const & c) {
     lean_assert(is_level_eq_cnstr(c));
     return static_cast<level_constraint_cell*>(c.raw())->m_lhs;
@@ -89,11 +91,11 @@ unsigned cnstr_delay_factor(constraint const & c) {
 constraint update_justification(constraint const & c, justification const & j) {
     switch (c.kind()) {
     case constraint_kind::Eq:
-        return mk_eq_cnstr(cnstr_lhs_expr(c), cnstr_rhs_expr(c), j);
+        return mk_eq_cnstr(cnstr_lhs_expr(c), cnstr_rhs_expr(c), j, relax_main_opaque(c));
     case constraint_kind::LevelEq:
         return mk_level_eq_cnstr(cnstr_lhs_level(c), cnstr_rhs_level(c), j);
     case constraint_kind::Choice:
-        return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), j);
+        return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), j, relax_main_opaque(c));
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h
index 7adc7ff12..7cbfb6701 100644
--- a/src/kernel/constraint.h
+++ b/src/kernel/constraint.h
@@ -65,9 +65,10 @@ public:
     friend bool is_eqp(constraint const & c1, constraint const & c2) { return c1.m_ptr == c2.m_ptr; }
     friend void swap(constraint & l1, constraint & l2) { std::swap(l1, l2); }
 
-    friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+    friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
     friend constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
-    friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j);
+    friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j,
+                                      bool relax_main_opaque);
 
     constraint_cell * raw() const { return m_ptr; }
 };
@@ -75,9 +76,13 @@ public:
 inline bool operator==(constraint const & c1, constraint const & c2) { return c1.raw() == c2.raw(); }
 inline bool operator!=(constraint const & c1, constraint const & c2) { return !(c1 == c2); }
 
-constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+/**
+   \brief Create a unification constraint lhs =?= rhs
+   If \c relax_main_opaque is true, then opaque definitions from the main module are treated as transparent.
+*/
+constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
 constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
-constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j);
+constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax_main_opaque);
 
 inline bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; }
 inline bool is_level_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::LevelEq; }
@@ -89,6 +94,8 @@ constraint update_justification(constraint const & c, justification const & j);
 expr const & cnstr_lhs_expr(constraint const & c);
 /** \brief Return the rhs of an equality constraint. */
 expr const & cnstr_rhs_expr(constraint const & c);
+/** \brief Return true iff opaque definitions from the main module should be treated as transparent. */
+bool relax_main_opaque(constraint const & c);
 /** \brief Return the lhs of an level constraint. */
 level const & cnstr_lhs_level(constraint const & c);
 /** \brief Return the rhs of an level constraint. */
diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index 044559731..3fcf0f63a 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -74,6 +74,7 @@ bool converter::is_def_eq(expr const & t, expr const & s, type_checker & c) {
 struct dummy_converter : public converter {
     virtual expr whnf(expr const & e, type_checker &) { return e; }
     virtual bool is_def_eq(expr const &, expr const &, type_checker &, delayed_justification &) { return true; }
+    virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
 };
 
 std::unique_ptr<converter> mk_dummy_converter() {
@@ -98,6 +99,10 @@ struct default_converter : public converter {
         m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_opaque(extra_opaque) {
     }
 
+    constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
+        return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx));
+    }
+
     optional<expr> expand_macro(expr const & m, type_checker & c) {
         lean_assert(is_macro(m));
         return macro_def(m).expand(m, get_extension(c));
@@ -552,6 +557,10 @@ struct default_converter : public converter {
     bool is_prop(expr const & e, type_checker & c) {
         return whnf(infer_type(c, e), c) == Prop;
     }
+
+    virtual optional<module_idx> get_module_idx() const {
+        return m_module_idx;
+    }
 };
 
 std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx,
diff --git a/src/kernel/converter.h b/src/kernel/converter.h
index e2728d814..1ebd8b42a 100644
--- a/src/kernel/converter.h
+++ b/src/kernel/converter.h
@@ -20,6 +20,7 @@ public:
     virtual ~converter() {}
     virtual expr whnf(expr const & e, type_checker & c) = 0;
     virtual bool is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;
+    virtual optional<module_idx> get_module_idx() const = 0;
     bool is_def_eq(expr const & t, expr const & s, type_checker & c);
 };
 
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index dcafd9bfc..44780c6f4 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -105,6 +105,10 @@ void type_checker::add_cnstr(constraint const & c) {
     m_cs.push_back(c);
 }
 
+constraint type_checker::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
+    return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_conv->get_module_idx()));
+}
+
 optional<constraint> type_checker::next_cnstr() {
     if (m_cs_qhead < m_cs.size()) {
         constraint c = m_cs[m_cs_qhead];
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index a6c0e308f..de1a2a0de 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -105,6 +105,7 @@ class type_checker {
     expr infer_type(expr const & e);
     void copy_constraints(unsigned qhead, buffer<constraint> & new_cnstrs);
     extension_context & get_extension() { return m_tc_ctx; }
+    constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
 public:
     /**
        \brief Create a type checker for the given environment. The auxiliary names created by this
diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp
index f2796fec5..f0411f06b 100644
--- a/src/library/inductive_unifier_plugin.cpp
+++ b/src/library/inductive_unifier_plugin.cpp
@@ -45,7 +45,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
     */
     lazy_list<constraints> add_elim_meta_cnstrs(type_checker & tc, name_generator ngen, inductive::inductive_decl const & decl,
                                                 expr const & elim, buffer<expr> & args, expr const & t, justification const & j,
-                                                buffer<constraint> & tc_cnstr_buffer) const {
+                                                buffer<constraint> & tc_cnstr_buffer, bool relax) const {
         lean_assert(is_constant(elim));
         environment const & env = tc.env();
         levels elim_lvls       = const_levels(elim);
@@ -78,12 +78,12 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
                 intro_type = tc.whnf(binding_body(intro_type), tc_cnstr_buffer);
                 lean_assert(!tc.next_cnstr());
             }
-            constraint c1      = mk_eq_cnstr(meta, hint, j);
+            constraint c1      = mk_eq_cnstr(meta, hint, j, relax);
             args[major_idx]    = hint;
             lean_assert(!tc.next_cnstr());
             expr reduce_elim   = tc.whnf(mk_app(elim, args), tc_cnstr_buffer);
             lean_assert(!tc.next_cnstr());
-            constraint c2      = mk_eq_cnstr(reduce_elim, t, j);
+            constraint c2      = mk_eq_cnstr(reduce_elim, t, j, relax);
             list<constraint> tc_cnstrs = to_list(tc_cnstr_buffer.begin(), tc_cnstr_buffer.end());
             alts.push_back(cons(c1, cons(c2, tc_cnstrs)));
         }
@@ -92,7 +92,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
     }
 
     lazy_list<constraints> process_elim_meta_core(type_checker & tc, name_generator const & ngen,
-                                                  expr const & lhs, expr const & rhs, justification const & j) const {
+                                                  expr const & lhs, expr const & rhs, justification const & j, bool relax) const {
         lean_assert(inductive::is_elim_meta_app(tc, lhs));
         buffer<constraint> tc_cnstr_buffer;
         lean_assert(!tc.next_cnstr());
@@ -106,7 +106,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
         auto decls   = *inductive::is_inductive_decl(env, it_name);
         for (auto const & d : std::get<2>(decls)) {
             if (inductive::inductive_decl_name(d) == it_name)
-                return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, tc_cnstr_buffer);
+                return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, tc_cnstr_buffer, relax);
         }
         lean_unreachable(); // LCOV_EXCL_LINE
     }
@@ -122,10 +122,11 @@ public:
         expr const & lhs        = cnstr_lhs_expr(c);
         expr const & rhs        = cnstr_rhs_expr(c);
         justification const & j = c.get_justification();
+        bool relax = relax_main_opaque(c);
         if (inductive::is_elim_meta_app(tc, lhs))
-            return process_elim_meta_core(tc, ngen, lhs, rhs, j);
+            return process_elim_meta_core(tc, ngen, lhs, rhs, j, relax);
         else if (inductive::is_elim_meta_app(tc, rhs))
-            return process_elim_meta_core(tc, ngen, rhs, lhs, j);
+            return process_elim_meta_core(tc, ngen, rhs, lhs, j, relax);
         else
             return lazy_list<constraints>();
     }
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 66e12f0f9..571a1a1df 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -1478,7 +1478,9 @@ static int constraint_tostring(lua_State * L) {
 }
 static int mk_eq_cnstr(lua_State * L) {
     int nargs = lua_gettop(L);
-    return push_constraint(L, mk_eq_cnstr(to_expr(L, 1), to_expr(L, 2), nargs == 3 ? to_justification(L, 3) : justification()));
+    return push_constraint(L, mk_eq_cnstr(to_expr(L, 1), to_expr(L, 2),
+                                          nargs >= 3 ? to_justification(L, 3) : justification(),
+                                          nargs >= 4 && lua_toboolean(L, 4)));
 }
 static int mk_level_eq_cnstr(lua_State * L) {
     int nargs = lua_gettop(L);
@@ -1508,7 +1510,7 @@ static choice_fn to_choice_fn(lua_State * L, int idx) {
                     if (is_constraint(L, -1))
                         r.push_back(constraints(to_constraint(L, -1)));
                     else if (is_expr(L, -1))
-                        r.push_back(constraints(mk_eq_cnstr(mvar, to_expr(L, -1), justification())));
+                        r.push_back(constraints(mk_eq_cnstr(mvar, to_expr(L, -1), justification(), false)));
                     else
                         r.push_back(to_list_constraint_ext(L, -1));
                     lua_pop(L, 1);
@@ -1526,13 +1528,15 @@ static int mk_choice_cnstr(lua_State * L) {
     expr m           = to_expr(L, 1);
     choice_fn fn     = to_choice_fn(L, 2);
     if (nargs == 2)
-        return push_constraint(L, mk_choice_cnstr(m, fn, 0, justification()));
+        return push_constraint(L, mk_choice_cnstr(m, fn, 0, justification(), false));
     else if (nargs == 3 && is_justification(L, 3))
-        return push_constraint(L, mk_choice_cnstr(m, fn, 0, to_justification(L, 3)));
+        return push_constraint(L, mk_choice_cnstr(m, fn, 0, to_justification(L, 3), false));
     else if (nargs == 3)
-        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), justification()));
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), justification(), false));
+    else if (nargs == 4)
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4), false));
     else
-        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4)));
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4), lua_toboolean(L, 5)));
 }
 
 static int constraint_expr(lua_State * L) {
diff --git a/src/library/opaque_hints.cpp b/src/library/opaque_hints.cpp
index efb6824a2..cf24341ef 100644
--- a/src/library/opaque_hints.cpp
+++ b/src/library/opaque_hints.cpp
@@ -45,15 +45,17 @@ environment expose_definition(environment const & env, name const & n) {
     ext.m_extra_opaque.erase(n);
     return update(env, ext);
 }
-environment set_main_module_opaque_defs(environment const & env, bool f) {
+environment set_hide_main_opaque(environment const & env, bool f) {
     auto ext = get_extension(env);
     ext.m_hide_module = f;
     return update(env, ext);
 }
-std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen) {
+bool get_hide_main_opaque(environment const & env) {
+    return get_extension(env).m_hide_module;
+}
+std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen, bool relax_main_opaque) {
     auto const & ext = get_extension(env);
-    return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, !ext.m_hide_module,
+    return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, !ext.m_hide_module && relax_main_opaque,
                                                                                           true, ext.m_extra_opaque)));
 }
 }
-
diff --git a/src/library/opaque_hints.h b/src/library/opaque_hints.h
index 1d7720068..b72002b97 100644
--- a/src/library/opaque_hints.h
+++ b/src/library/opaque_hints.h
@@ -22,12 +22,11 @@ namespace lean {
 environment hide_definition(environment const & env, name const & n);
 /** \brief Undo the modification made with \c hide_definition. */
 environment expose_definition(environment const & env, name const & n);
-/**
-    \brief By default, the elaborator/unifier will treat the opaque
-    definitions of the current/main module as transparent. We can
-    change this behavior using this function.
+/** \brief By default, the elaborator/unifier will treat the opaque definitions of the current/main
+    module as transparent (when allowed). We can change this behavior using this function.
 */
-environment set_main_module_opaque_defs(environment const & env, bool f);
+environment set_hide_main_opaque(environment const & env, bool f);
+bool get_hide_main_opaque(environment const & env);
 /** \brief Create a type checker that takes the hints into account. */
-std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen);
+std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen, bool relax_main_opaque);
 }
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index ce299e4dc..fd6e7317e 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -92,7 +92,7 @@ static void remove_redundant_metas(buffer<expr> & metas) {
 }
 
 proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e,
-                                  bool add_meta, bool add_subgoals) {
+                                  bool add_meta, bool add_subgoals, bool relax_main_opaque) {
     goals const & gs = s.get_goals();
     if (empty(gs))
         return proof_state_seq();
@@ -119,7 +119,7 @@ proof_state_seq apply_tactic_core(environment const & env, io_state const & ios,
         }
     }
     list<expr> meta_lst = to_list(metas.begin(), metas.end());
-    lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), ios.get_options());
+    lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), relax_main_opaque, s.get_subst(), ios.get_options());
     return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state {
             name_generator new_ngen(ngen);
             type_checker tc(env, new_ngen.mk_child());
@@ -182,21 +182,21 @@ expr refresh_univ_metavars(expr const & e, name_generator & ngen) {
     }
 }
 
-tactic apply_tactic(expr const & e, bool refresh_univ_mvars) {
+tactic apply_tactic(expr const & e, bool relax_main_opaque, bool refresh_univ_mvars) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             if (refresh_univ_mvars) {
                 name_generator ngen    = s.get_ngen();
                 substitution new_subst = s.get_subst();
                 expr new_e = refresh_univ_metavars(new_subst.instantiate_all(e), ngen);
                 proof_state new_s(s.get_goals(), new_subst, ngen);
-                return apply_tactic_core(env, ios, new_s, new_e, true, true);
+                return apply_tactic_core(env, ios, new_s, new_e, true, true, relax_main_opaque);
             } else {
-                return apply_tactic_core(env, ios, s, e, true, true);
+                return apply_tactic_core(env, ios, s, e, true, true, relax_main_opaque);
             }
         });
 }
 
-tactic eassumption_tactic() {
+tactic eassumption_tactic(bool relax_main_opaque) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
             if (empty(gs))
@@ -206,7 +206,7 @@ tactic eassumption_tactic() {
             buffer<expr> hs;
             get_app_args(g.get_meta(), hs);
             for (expr const & h : hs) {
-                r = append(r, apply_tactic_core(env, ios, s, h, false, false));
+                r = append(r, apply_tactic_core(env, ios, s, h, false, false, relax_main_opaque));
             }
             return r;
         });
diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h
index be1116183..64015b858 100644
--- a/src/library/tactic/apply_tactic.h
+++ b/src/library/tactic/apply_tactic.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 #include "library/tactic/tactic.h"
 namespace lean {
-tactic apply_tactic(expr const & e, bool refresh_univ_mvars = true);
-tactic eassumption_tactic();
+tactic apply_tactic(expr const & e, bool relax_main_opaque = true, bool refresh_univ_mvars = true);
+tactic eassumption_tactic(bool relax_main_opaque = true);
 void open_apply_tactic(lua_State * L);
 }
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 7b857932d..50f3e465c 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -209,7 +209,7 @@ unify_status unify_simple(substitution & s, constraint const & c) {
         return unify_status::Unsupported;
 }
 
-static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification());
+static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification(), false);
 static unsigned g_group_size = 1u << 29;
 static unsigned g_cnstr_group_first_index[6] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size};
 static unsigned get_group_first_index(cnstr_group g) {
@@ -241,7 +241,7 @@ struct unifier_fn {
     name_generator   m_ngen;
     substitution     m_subst;
     unifier_plugin   m_plugin;
-    type_checker_ptr m_tc;
+    type_checker_ptr m_tc[2];
     bool             m_use_exception; //!< True if we should throw an exception when there are no more solutions.
     unsigned         m_max_steps;
     unsigned         m_num_steps;
@@ -292,14 +292,17 @@ struct unifier_fn {
             m_assumption_idx(u.m_next_assumption_idx), m_jst(j), m_subst(u.m_subst), m_cnstrs(u.m_cnstrs),
             m_mvar_occs(u.m_mvar_occs) {
             u.m_next_assumption_idx++;
-            u.m_tc->push();
+            u.m_tc[0]->push();
+            u.m_tc[1]->push();
         }
 
         /** \brief Restore unifier's state with saved values, and update m_assumption_idx and m_failed_justifications. */
         void restore_state(unifier_fn & u) {
             lean_assert(u.in_conflict());
-            u.m_tc->pop();   // restore type checker state
-            u.m_tc->push();
+            u.m_tc[0]->pop();   // restore type checker state
+            u.m_tc[1]->pop();   // restore type checker state
+            u.m_tc[0]->push();
+            u.m_tc[1]->push();
             u.m_subst     = m_subst;
             u.m_cnstrs    = m_cnstrs;
             u.m_mvar_occs = m_mvar_occs;
@@ -333,8 +336,9 @@ struct unifier_fn {
                name_generator const & ngen, substitution const & s,
                bool use_exception, unsigned max_steps):
         m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)),
-        m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child())),
         m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0) {
+        m_tc[0] = mk_type_checker_with_hints(env, m_ngen.mk_child(), false);
+        m_tc[1] = mk_type_checker_with_hints(env, m_ngen.mk_child(), true);
         m_next_assumption_idx = 0;
         m_next_cidx = 0;
         m_first     = true;
@@ -403,9 +407,12 @@ struct unifier_fn {
         return cidx;
     }
 
-    /** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j */
-    bool is_def_eq(expr const & t1, expr const & t2, justification const & j) {
-        if (m_tc->is_def_eq(t1, t2, j)) {
+    /** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j
+
+        \remark If relax is true then opaque definitions from the main module are treated as transparent.
+    */
+    bool is_def_eq(expr const & t1, expr const & t2, justification const & j, bool relax) {
+        if (m_tc[relax]->is_def_eq(t1, t2, j)) {
             return true;
         } else {
             set_conflict(j);
@@ -417,21 +424,23 @@ struct unifier_fn {
        \brief Assign \c v to metavariable \c m with justification \c j.
        The type of v and m are inferred, and is_def_eq is invoked.
        Any constraint that contains \c m is revisited.
+
+       \remark If relax is true then opaque definitions from the main module are treated as transparent.
     */
-    bool assign(expr const & m, expr const & v, justification const & j) {
+    bool assign(expr const & m, expr const & v, justification const & j, bool relax) {
         lean_assert(is_metavar(m));
         m_subst.assign(m, v, j);
         expr m_type = mlocal_type(m);
         expr v_type;
         try {
-            v_type = m_tc->infer(v);
+            v_type = m_tc[relax]->infer(v);
         } catch (kernel_exception & e) {
             set_conflict(j);
             return false;
         }
         if (in_conflict())
             return false;
-        if (!is_def_eq(m_type, v_type, j))
+        if (!is_def_eq(m_type, v_type, j, relax))
             return false;
         auto it = m_mvar_occs.find(mlocal_name(m));
         if (it) {
@@ -463,7 +472,7 @@ struct unifier_fn {
        The method returns \c Failed if \c rhs contains <tt>?m</tt>, or it contains a local constant not in <tt>{l_1, ..., l_n}</tt>.
        Otherwise, it returns \c Continue.
     */
-    status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j) {
+    status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j, bool relax) {
         if (!is_meta(lhs))
             return Continue;
         buffer<expr> locals;
@@ -478,7 +487,7 @@ struct unifier_fn {
             return Continue;
         case l_true:
             lean_assert(!m_subst.is_assigned(*m));
-            if (assign(*m, lambda_abstract_locals(rhs, locals), j)) {
+            if (assign(*m, lambda_abstract_locals(rhs, locals), j, relax)) {
                 return Solved;
             } else {
                 return Failed;
@@ -509,7 +518,8 @@ struct unifier_fn {
             expr rhs = rhs_jst.first;
             if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) {
                 return mk_pair(mk_eq_cnstr(lhs, rhs,
-                                           mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second)),
+                                           mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second),
+                                           relax_main_opaque(c)),
                                true);
             }
         } else if (is_level_eq_cnstr(c)) {
@@ -530,19 +540,20 @@ struct unifier_fn {
         expr const & lhs = cnstr_lhs_expr(c);
         expr const & rhs = cnstr_rhs_expr(c);
         justification const & jst = c.get_justification();
+        bool relax = relax_main_opaque(c);
 
         if (lhs == rhs)
             return Solved; // trivial constraint
 
         // Update justification using the justification of the instantiated metavariables
         if (!has_metavar(lhs) && !has_metavar(rhs)) {
-            return is_def_eq(lhs, rhs, jst) ? Solved : Failed;
+            return is_def_eq(lhs, rhs, jst, relax) ? Solved : Failed;
         }
 
         // Handle higher-order pattern matching.
-        status st = process_metavar_eq(lhs, rhs, jst);
+        status st = process_metavar_eq(lhs, rhs, jst, relax);
         if (st != Continue) return st;
-        st = process_metavar_eq(rhs, lhs, jst);
+        st = process_metavar_eq(rhs, lhs, jst, relax);
         if (st != Continue) return st;
 
         return Continue;
@@ -589,11 +600,11 @@ struct unifier_fn {
         expr lhs = instantiate_meta(cnstr_lhs_expr(c), j);
         expr rhs = instantiate_meta(cnstr_rhs_expr(c), j);
         if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c))
-            return is_def_eq(lhs, rhs, j) ? Solved : Failed;
+            return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
         lhs = instantiate_meta_args(lhs, j);
         rhs = instantiate_meta_args(rhs, j);
         if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c))
-            return is_def_eq(lhs, rhs, j) ? Solved : Failed;
+            return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
         return Continue;
     }
 
@@ -608,6 +619,7 @@ struct unifier_fn {
 
         expr const & lhs = cnstr_lhs_expr(c);
         expr const & rhs = cnstr_rhs_expr(c);
+        bool relax = relax_main_opaque(c);
 
         if (is_eq_deltas(lhs, rhs)) {
             // we need to create a backtracking point for this one
@@ -617,7 +629,7 @@ struct unifier_fn {
             unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
             add_meta_occ(lhs, cidx);
             add_meta_occ(rhs, cidx);
-        } else if (m_plugin->delay_constraint(*m_tc, c)) {
+        } else if (m_plugin->delay_constraint(*m_tc[relax], c)) {
             unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
             add_meta_occs(lhs, cidx);
             add_meta_occs(rhs, cidx);
@@ -749,7 +761,8 @@ struct unifier_fn {
     }
 
     void pop_case_split() {
-        m_tc->pop();
+        m_tc[0]->pop();
+        m_tc[1]->pop();
         m_case_splits.pop_back();
     }
 
@@ -835,26 +848,28 @@ struct unifier_fn {
             return lazy_list<constraints>();
         justification const & j = c.get_justification();
         buffer<constraint> cs;
-        lean_assert(!m_tc->next_cnstr());
-        if (!m_tc->is_def_eq(f_lhs, f_rhs, j, cs))
+        bool relax = relax_main_opaque(c);
+        lean_assert(!m_tc[relax]->next_cnstr());
+        if (!m_tc[relax]->is_def_eq(f_lhs, f_rhs, j, cs))
             return lazy_list<constraints>();
         buffer<expr> args_lhs, args_rhs;
         get_app_args(lhs, args_lhs);
         get_app_args(rhs, args_rhs);
         if (args_lhs.size() != args_rhs.size())
             return lazy_list<constraints>();
-        lean_assert(!m_tc->next_cnstr());
+        lean_assert(!m_tc[relax]->next_cnstr());
         for (unsigned i = 0; i < args_lhs.size(); i++)
-            if (!m_tc->is_def_eq(args_lhs[i], args_rhs[i], j, cs))
+            if (!m_tc[relax]->is_def_eq(args_lhs[i], args_rhs[i], j, cs))
                 return lazy_list<constraints>();
         return lazy_list<constraints>(to_list(cs.begin(), cs.end()));
     }
 
     bool process_plugin_constraint(constraint const & c) {
+        bool relax = relax_main_opaque(c);
         lean_assert(!is_choice_cnstr(c));
-        lean_assert(!m_tc->next_cnstr());
-        lazy_list<constraints> alts = m_plugin->solve(*m_tc, c, m_ngen.mk_child());
-        lean_assert(!m_tc->next_cnstr());
+        lean_assert(!m_tc[relax]->next_cnstr());
+        lazy_list<constraints> alts = m_plugin->solve(*m_tc[relax], c, m_ngen.mk_child());
+        lean_assert(!m_tc[relax]->next_cnstr());
         alts = append(alts, process_const_const_cnstr(c));
         return process_lazy_constraints(alts, c.get_justification());
     }
@@ -864,8 +879,9 @@ struct unifier_fn {
         expr const &   m            = cnstr_expr(c);
         choice_fn const & fn        = cnstr_choice_fn(c);
         expr m_type;
+        bool relax = relax_main_opaque(c);
         try {
-            m_type                  = m_tc->infer(m);
+            m_type                  = m_tc[relax]->infer(m);
         } catch (kernel_exception &) {
             set_conflict(c.get_justification());
             return false;
@@ -920,8 +936,9 @@ struct unifier_fn {
         expr rhs_fn_val = instantiate_univ_params(d.get_value(), d.get_univ_params(), const_levels(rhs_fn));
         expr t = apply_beta(lhs_fn_val, lhs_args.size(), lhs_args.data());
         expr s = apply_beta(rhs_fn_val, rhs_args.size(), rhs_args.data());
+        bool relax = relax_main_opaque(c);
         buffer<constraint> cs2;
-        if (m_tc->is_def_eq(t, s, j, cs2)) {
+        if (m_tc[relax]->is_def_eq(t, s, j, cs2)) {
             // create a case split
             a = mk_assumption_justification(m_next_assumption_idx);
             add_case_split(std::unique_ptr<case_split>(new simple_case_split(*this, j, to_list(cs2.begin(), cs2.end()))));
@@ -941,7 +958,7 @@ struct unifier_fn {
         unsigned i = lhs_args.size();
         while (i > 0) {
             --i;
-            if (!is_def_eq(lhs_args[i], rhs_args[i], new_j))
+            if (!is_def_eq(lhs_args[i], rhs_args[i], new_j, relax))
                 return false;
         }
         return true;
@@ -979,19 +996,19 @@ struct unifier_fn {
     }
 
     /** \see ensure_sufficient_args */
-    optional<expr> ensure_sufficient_args_core(expr mtype, unsigned i, buffer<expr> const & margs) {
+    optional<expr> ensure_sufficient_args_core(expr mtype, unsigned i, buffer<expr> const & margs, bool relax) {
         if (i == margs.size())
             return some_expr(mtype);
-        mtype = m_tc->ensure_pi(mtype);
+        mtype = m_tc[relax]->ensure_pi(mtype);
         try {
-            if (!m_tc->is_def_eq(binding_domain(mtype), m_tc->infer(margs[i])))
+            if (!m_tc[relax]->is_def_eq(binding_domain(mtype), m_tc[relax]->infer(margs[i])))
                 return none_expr();
         } catch (kernel_exception &) {
             return none_expr();
         }
         expr local = mk_local_for(mtype);
         expr body  = instantiate(binding_body(mtype), local);
-        auto new_body = ensure_sufficient_args_core(body, i+1, margs);
+        auto new_body = ensure_sufficient_args_core(body, i+1, margs, relax);
         if (!new_body)
             return none_expr();
         return some_expr(Pi(local, *new_body));
@@ -1001,7 +1018,8 @@ struct unifier_fn {
        \brief Make sure mtype is a Pi of size at least margs.size().
        If it is not, we use ensure_pi and (potentially) add new constaints to enforce it.
     */
-    optional<expr> ensure_sufficient_args(expr const & mtype, buffer<expr> const & margs, buffer<constraint> & cs, justification const & j) {
+    optional<expr> ensure_sufficient_args(expr const & mtype, buffer<expr> const & margs, buffer<constraint> & cs, justification const & j,
+                                          bool relax) {
         expr t = mtype;
         unsigned num = 0;
         while (is_pi(t)) {
@@ -1010,13 +1028,13 @@ struct unifier_fn {
         }
         if (num == margs.size())
             return some_expr(mtype);;
-        lean_assert(!m_tc->next_cnstr()); // make sure there are no pending constraints
+        lean_assert(!m_tc[relax]->next_cnstr()); // make sure there are no pending constraints
         // We must create a scope to make sure no constraints "leak" into the current state.
-        type_checker::scope scope(*m_tc);
-        auto new_mtype = ensure_sufficient_args_core(mtype, 0, margs);
+        type_checker::scope scope(*m_tc[relax]);
+        auto new_mtype = ensure_sufficient_args_core(mtype, 0, margs, relax);
         if (!new_mtype)
             return none_expr();
-        while (auto c = m_tc->next_cnstr())
+        while (auto c = m_tc[relax]->next_cnstr())
             cs.push_back(update_justification(*c, mk_composite1(c->get_justification(), j)));
         return new_mtype;
     }
@@ -1073,13 +1091,13 @@ struct unifier_fn {
                   - variable (if g is a local constant equal to a_i)
     */
     void mk_flex_rigid_app_cnstrs(expr const & m, buffer<expr> const & margs, expr const & f, expr const & rhs, justification const & j,
-                                  buffer<constraints> & alts) {
+                                  buffer<constraints> & alts, bool relax) {
         lean_assert(is_metavar(m));
         lean_assert(is_app(rhs));
         lean_assert(is_constant(f) || is_var(f));
         buffer<constraint> cs;
         expr mtype = mlocal_type(m);
-        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j);
+        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
         if (!new_mtype) return;
         mtype = *new_mtype;
         buffer<expr> rargs;
@@ -1090,13 +1108,13 @@ struct unifier_fn {
                 sargs.push_back(*v);
             } else {
                 expr maux = mk_aux_metavar_for(m_ngen, mtype);
-                cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j));
+                cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j, relax));
                 sargs.push_back(mk_app_vars(maux, margs.size()));
             }
         }
         expr v = mk_app(f, sargs);
         v = mk_lambda_for(mtype, v);
-        cs.push_back(mk_eq_cnstr(m, v, j));
+        cs.push_back(mk_eq_cnstr(m, v, j, relax));
         alts.push_back(to_list(cs.begin(), cs.end()));
     }
 
@@ -1112,25 +1130,25 @@ struct unifier_fn {
        where l is a fresh local constant.
     */
     void mk_bindings_imitation(expr const & m, buffer<expr> const & margs, expr const & rhs, justification const & j,
-                               buffer<constraints> & alts) {
+                               buffer<constraints> & alts, bool relax) {
         lean_assert(is_metavar(m));
         lean_assert(is_binding(rhs));
         buffer<constraint> cs;
         expr mtype = mlocal_type(m);
-        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j);
+        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
         if (!new_mtype) return;
         mtype = *new_mtype;
         expr maux1  = mk_aux_metavar_for(m_ngen, mtype);
-        cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j));
+        cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j, relax));
         expr dontcare;
         expr tmp_pi = mk_pi(binding_name(rhs), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context
         expr mtype2 = replace_range(mtype, tmp_pi); // trick for "extending" the context
         expr maux2  = mk_aux_metavar_for(m_ngen, mtype2);
         expr new_local = mk_local_for(rhs);
-        cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j));
+        cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j, relax));
         expr v = update_binding(rhs, mk_app_vars(maux1, margs.size()), mk_app_vars(maux2, margs.size() + 1));
         v = mk_lambda_for(mtype, v);
-        cs.push_back(mk_eq_cnstr(m, v, j));
+        cs.push_back(mk_eq_cnstr(m, v, j, relax));
         alts.push_back(to_list(cs.begin(), cs.end()));
     }
 
@@ -1141,12 +1159,12 @@ struct unifier_fn {
         Then solve (?m a_1 ... a_k) =?= rhs, by returning the constraint
                  ?m  =?= fun (x1 ... x_k), rhs
     */
-    void mk_simple_imitation(expr const & m, expr const & rhs, justification const & j, buffer<constraints> & alts) {
+    void mk_simple_imitation(expr const & m, expr const & rhs, justification const & j, buffer<constraints> & alts, bool relax) {
         lean_assert(is_metavar(m));
         lean_assert(is_sort(rhs) || is_constant(rhs));
         expr const & mtype = mlocal_type(m);
         buffer<constraint> cs;
-        cs.push_back(mk_eq_cnstr(m, mk_lambda_for(mtype, rhs), j));
+        cs.push_back(mk_eq_cnstr(m, mk_lambda_for(mtype, rhs), j, relax));
         alts.push_back(to_list(cs.begin(), cs.end()));
     }
 
@@ -1162,24 +1180,24 @@ struct unifier_fn {
                ?m  =?= fun (x_1 ... x_k), M((?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k))
     */
     void mk_macro_imitation(expr const & m, buffer<expr> const & margs, expr const & rhs, justification const & j,
-                            buffer<constraints> & alts) {
+                            buffer<constraints> & alts, bool relax) {
         lean_assert(is_metavar(m));
         lean_assert(is_macro(rhs));
         buffer<constraint> cs;
         expr mtype = mlocal_type(m);
-        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j);
+        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
         if (!new_mtype) return;
         mtype = *new_mtype;
         // create an auxiliary metavariable for each macro argument
         buffer<expr> sargs;
         for (unsigned i = 0; i < macro_num_args(rhs); i++) {
             expr maux = mk_aux_metavar_for(m_ngen, mtype);
-            cs.push_back(mk_eq_cnstr(mk_app(maux, margs), macro_arg(rhs, i), j));
+            cs.push_back(mk_eq_cnstr(mk_app(maux, margs), macro_arg(rhs, i), j, relax));
             sargs.push_back(mk_app_vars(maux, margs.size()));
         }
         expr v = mk_macro(macro_def(rhs), sargs.size(), sargs.data());
         v = mk_lambda_for(mtype, v);
-        cs.push_back(mk_eq_cnstr(m, v, j));
+        cs.push_back(mk_eq_cnstr(m, v, j, relax));
         alts.push_back(to_list(cs.begin(), cs.end()));
     }
 
@@ -1198,17 +1216,17 @@ struct unifier_fn {
        to alts as a possible solution.
     */
     void mk_simple_nonlocal_projection(expr const & m, buffer<expr> const & margs, unsigned i, expr const & rhs, justification const & j,
-                              buffer<constraints> & alts) {
+                                       buffer<constraints> & alts, bool relax) {
         expr const & mtype = mlocal_type(m);
         unsigned vidx = margs.size() - i - 1;
         expr const & marg = margs[i];
         buffer<constraint> cs;
-        if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j)) {
+        if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax)) {
             // Remark: we should not use mk_eq_cnstr(marg, rhs, j) since is_def_eq may be able to reduce them.
             // The unifier assumes the eq constraints are reduced.
-            if (m_tc->is_def_eq(marg, rhs, j, cs)) {
+            if (m_tc[relax]->is_def_eq(marg, rhs, j, cs)) {
                 expr v = mk_lambda_for(*new_mtype, mk_var(vidx));
-                cs.push_back(mk_eq_cnstr(m, v, j));
+                cs.push_back(mk_eq_cnstr(m, v, j, relax));
                 alts.push_back(to_list(cs.begin(), cs.end()));
             }
         }
@@ -1232,7 +1250,7 @@ struct unifier_fn {
 
     */
     void mk_simple_projections(expr const & m, buffer<expr> const & margs, expr const & rhs, justification const & j,
-                                buffer<constraints> & alts) {
+                               buffer<constraints> & alts, bool relax) {
         lean_assert(is_metavar(m));
         lean_assert(!is_meta(rhs));
         expr const & mtype = mlocal_type(m);
@@ -1243,13 +1261,13 @@ struct unifier_fn {
             expr const & marg = margs[i];
             if ((!is_local(marg) && !is_local(rhs)) || (is_meta(marg) && is_local(rhs))) {
                 // if rhs is not local, then we only add projections for the nonlocal arguments of lhs
-                mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts);
+                mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts, relax);
             } else if (is_local(marg) && is_local(rhs) && mlocal_name(marg) == mlocal_name(rhs)) {
                 // if the argument is local, and rhs is equal to it, then we also add a projection
                 buffer<constraint> cs;
-                if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j)) {
+                if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax)) {
                     expr v = mk_lambda_for(*new_mtype, mk_var(vidx));
-                    cs.push_back(mk_eq_cnstr(m, v, j));
+                    cs.push_back(mk_eq_cnstr(m, v, j, relax));
                     alts.push_back(to_list(cs.begin(), cs.end()));
                 }
             }
@@ -1257,7 +1275,7 @@ struct unifier_fn {
     }
 
     /** \brief Process a flex rigid constraint */
-    bool process_flex_rigid(expr const & lhs, expr const & rhs, justification const & j) {
+    bool process_flex_rigid(expr const & lhs, expr const & rhs, justification const & j, bool relax) {
         lean_assert(is_meta(lhs));
         lean_assert(!is_meta(rhs));
         buffer<expr> margs;
@@ -1266,7 +1284,7 @@ struct unifier_fn {
             // Make sure that if marg is reducible to a local constant, then it is replaced with it.
             // We need that because of the optimization based on is_easy_flex_rigid_arg
             if (!is_local(marg)) {
-                expr new_marg = m_tc->whnf(marg);
+                expr new_marg = m_tc[relax]->whnf(marg);
                 if (is_local(new_marg))
                     marg = new_marg;
             }
@@ -1276,19 +1294,19 @@ struct unifier_fn {
         case expr_kind::Var: case expr_kind::Meta:
             lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::Local:
-            mk_simple_projections(m, margs, rhs, j, alts);
+            mk_simple_projections(m, margs, rhs, j, alts, relax);
             break;
         case expr_kind::Sort: case expr_kind::Constant:
-            mk_simple_projections(m, margs, rhs, j, alts);
-            mk_simple_imitation(m, rhs, j, alts);
+            mk_simple_projections(m, margs, rhs, j, alts, relax);
+            mk_simple_imitation(m, rhs, j, alts, relax);
             break;
         case expr_kind::Pi: case expr_kind::Lambda:
-            mk_simple_projections(m, margs, rhs, j, alts);
-            mk_bindings_imitation(m, margs, rhs, j, alts);
+            mk_simple_projections(m, margs, rhs, j, alts, relax);
+            mk_bindings_imitation(m, margs, rhs, j, alts, relax);
             break;
         case expr_kind::Macro:
-            mk_simple_projections(m, margs, rhs, j, alts);
-            mk_macro_imitation(m, margs, rhs, j, alts);
+            mk_simple_projections(m, margs, rhs, j, alts, relax);
+            mk_macro_imitation(m, margs, rhs, j, alts, relax);
             break;
         case expr_kind::App: {
             expr const & f = get_app_fn(rhs);
@@ -1299,17 +1317,17 @@ struct unifier_fn {
                     --i;
                     expr const & marg = margs[i];
                     if (is_local(marg) && mlocal_name(marg) == mlocal_name(f))
-                        mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j, alts);
+                        mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j, alts, relax);
                     else
-                        mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts);
+                        mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts, relax);
                 }
             } else if (is_constant(f)) {
-                mk_simple_projections(m, margs, rhs, j, alts);
-                mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j, alts);
+                mk_simple_projections(m, margs, rhs, j, alts, relax);
+                mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j, alts, relax);
             } else {
-                expr new_rhs = m_tc->whnf(rhs);
+                expr new_rhs = m_tc[relax]->whnf(rhs);
                 lean_assert(new_rhs != rhs);
-                return is_def_eq(lhs, new_rhs, j);
+                return is_def_eq(lhs, new_rhs, j, relax);
             }
             break;
         }}
@@ -1330,12 +1348,13 @@ struct unifier_fn {
     /** \brief Process a flex rigid constraint */
     bool process_flex_rigid(constraint const & c) {
         lean_assert(is_flex_rigid(c));
-        expr lhs = cnstr_lhs_expr(c);
-        expr rhs = cnstr_rhs_expr(c);
+        expr lhs   = cnstr_lhs_expr(c);
+        expr rhs   = cnstr_rhs_expr(c);
+        bool relax = relax_main_opaque(c);
         if (is_meta(lhs))
-            return process_flex_rigid(lhs, rhs, c.get_justification());
+            return process_flex_rigid(lhs, rhs, c.get_justification(), relax);
         else
-            return process_flex_rigid(rhs, lhs, c.get_justification());
+            return process_flex_rigid(rhs, lhs, c.get_justification(), relax);
     }
 
     bool process_flex_flex(constraint const & c) {
@@ -1358,18 +1377,20 @@ struct unifier_fn {
             if (mlocal_name(lhs_args[i]) != mlocal_name(rhs_args[i]))
                 break;
         if (i == lhs_args.size())
-            return assign(ml, mr, c.get_justification());
+            return assign(ml, mr, c.get_justification(), relax_main_opaque(c));
         return true;
     }
 
     void consume_tc_cnstrs() {
-        while (true) {
-            if (in_conflict())
-                return;
-            if (auto c = m_tc->next_cnstr()) {
-                process_constraint(*c);
-            } else {
-                break;
+        for (unsigned i = 0; i < 2; i++) {
+            while (true) {
+                if (in_conflict())
+                    return;
+                if (auto c = m_tc[i]->next_cnstr()) {
+                    process_constraint(*c);
+                } else {
+                    break;
+                }
             }
         }
     }
@@ -1417,7 +1438,8 @@ struct unifier_fn {
         } else {
             auto r = instantiate_metavars(c);
             c = r.first;
-            lean_assert(!m_tc->next_cnstr());
+            lean_assert(!m_tc[0]->next_cnstr());
+            lean_assert(!m_tc[1]->next_cnstr());
             bool modified = r.second;
             if (is_level_eq_cnstr(c)) {
                 if (modified)
@@ -1432,7 +1454,7 @@ struct unifier_fn {
                 if (is_delta_cnstr(c)) {
                     return process_delta(c);
                 } else if (modified) {
-                    return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification());
+                    return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification(), relax_main_opaque(c));
                 } else if (is_flex_rigid(c)) {
                     return process_flex_rigid(c);
                 } else if (is_flex_flex(c)) {
@@ -1510,21 +1532,21 @@ lazy_list<substitution> unify(environment const & env,  unsigned num_cs, constra
     return unify(env, num_cs, cs, ngen, use_exception, get_unifier_max_steps(o));
 }
 
-lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
-                              unsigned max_steps) {
+lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
+                              bool relax, substitution const & s, unsigned max_steps) {
     substitution new_s = s;
     expr _lhs = new_s.instantiate(lhs);
     expr _rhs = new_s.instantiate(rhs);
     auto u = std::make_shared<unifier_fn>(env, 0, nullptr, ngen, new_s, false, max_steps);
-    if (!u->m_tc->is_def_eq(_lhs, _rhs))
+    if (!u->m_tc[relax]->is_def_eq(_lhs, _rhs))
         return lazy_list<substitution>();
     else
         return unify(u);
 }
 
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
-                              substitution const & s, options const & o) {
-    return unify(env, lhs, rhs, ngen, s, get_unifier_max_steps(o));
+                              bool relax, substitution const & s, options const & o) {
+    return unify(env, lhs, rhs, ngen, relax, s, get_unifier_max_steps(o));
 }
 
 static int unify_simple(lua_State * L) {
@@ -1646,10 +1668,12 @@ static int unify(lua_State * L) {
     lazy_list<substitution> r;
     environment const & env = to_environment(L, 1);
     if (is_expr(L, 2)) {
-        if (nargs == 6)
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), to_options(L, 6));
+        if (nargs == 7)
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6), to_options(L, 7));
+        else if (nargs == 6)
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6), options());
         else
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), options());
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5));
     } else {
         buffer<constraint> cs;
         to_constraint_buffer(L, 2, cs);
diff --git a/src/library/unifier.h b/src/library/unifier.h
index 26e09f3e9..c64b4169c 100644
--- a/src/library/unifier.h
+++ b/src/library/unifier.h
@@ -40,10 +40,10 @@ lazy_list<substitution> unify(environment const & env, unsigned num_cs, constrai
                               bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
 lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
                               bool use_exception, options const & o);
-lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
+lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, bool relax_main_opaque,
                               substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
-lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
-                              options const & o);
+lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
+                              bool relax_main_opaque, substitution const & s, options const & o);
 
 /**
     The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, PluginDelayed, PreFlexFlex, FlexFlex, MaxDelayed
diff --git a/src/tests/library/unifier.cpp b/src/tests/library/unifier.cpp
index 0495475b5..0b46fb6a2 100644
--- a/src/tests/library/unifier.cpp
+++ b/src/tests/library/unifier.cpp
@@ -18,7 +18,7 @@ static void tst1() {
     expr m  = mk_metavar("m", A);
     expr t1 = f(m, m);
     expr t2 = f(a, b);
-    auto r = unify(env, t1, t2, ngen);
+    auto r = unify(env, t1, t2, ngen, false);
     lean_assert(!r.pull());
 }
 
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index d099faeaf..a08ef8b4a 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -69,6 +69,7 @@ variable div : Π (x y : nat) {H : not_zero y}, nat
 
 variables a b : nat
 
+set_option pp.implicit true
 opaque_hint (hiding [module])
 check div a (succ b)
 check (λ H : not_zero b, div a b)
diff --git a/tests/lean/run/uni.lean b/tests/lean/run/uni.lean
index f4fa23eae..5f6d9af1a 100644
--- a/tests/lean/run/uni.lean
+++ b/tests/lean/run/uni.lean
@@ -27,7 +27,7 @@ print(env:whnf(t(m)))
 
 function test_unify(env, lhs, rhs, num_s)
    print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
-   local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
+   local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
    local n  = 0
    for s in ss do
       print("solution: ")
diff --git a/tests/lean/run/uni2.lean b/tests/lean/run/uni2.lean
index 407b1a011..a557e7610 100644
--- a/tests/lean/run/uni2.lean
+++ b/tests/lean/run/uni2.lean
@@ -30,7 +30,7 @@ print(env:whnf(t(m)))
 
 function test_unify(env, lhs, rhs, num_s)
    print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
-   local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
+   local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
    local n  = 0
    for s in ss do
       print("solution: ")
diff --git a/tests/lean/run/univ2.lean b/tests/lean/run/univ2.lean
new file mode 100644
index 000000000..786d1a8c9
--- /dev/null
+++ b/tests/lean/run/univ2.lean
@@ -0,0 +1,11 @@
+import standard
+
+hypothesis I : Type
+definition F (X : Type) : Type := (X → Prop) → Prop
+hypothesis unfold : I → F I
+hypothesis fold   : F I → I
+hypothesis iso1 : ∀x, fold (unfold x) = x
+
+variable sorry {A : Type} : A
+theorem iso2 : ∀x, fold (unfold x) = x
+:= sorry
diff --git a/tests/lua/unify2.lua b/tests/lua/unify2.lua
index f1cf56e9b..a04282bea 100644
--- a/tests/lua/unify2.lua
+++ b/tests/lua/unify2.lua
@@ -1,6 +1,6 @@
 function test_unify(env, lhs, rhs, num_s)
    print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
-   local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
+   local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
    local n  = 0
    for s in ss do
       print("solution: ")
diff --git a/tests/lua/unify4.lua b/tests/lua/unify4.lua
index a94af1e47..f01b933f6 100644
--- a/tests/lua/unify4.lua
+++ b/tests/lua/unify4.lua
@@ -1,6 +1,6 @@
 function test_unify(env, m, lhs, rhs, num_s)
    print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
-   local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
+   local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
    local n  = 0
    for s in ss do
       print("solution: " .. tostring(s:instantiate(m)))