feat(library/type_inference): check types when assigning meta-variables

src/library/type_inference.cpp

@@ -49,6 +49,8 @@ type_inference::type_inference(environment const & env):
     m_ngen(*g_prefix),
     m_ext_ctx(new ext_ctx(*this)),
     m_proj_info(get_projection_info_map(env)) {
+    m_ignore_external_mvars = false;
+    m_check_types           = true;
 }
 
 type_inference::~type_inference() {
@@ -599,7 +601,7 @@ bool type_inference::is_def_eq_proof_irrel(expr const & e1, expr const & e2) {
 
 /** \brief Given \c ma of the form <tt>?m t_1 ... t_n</tt>, (try to) assign
     ?m to (an abstraction of) v. Return true if success and false otherwise. */
-bool type_inference::assign_mvar(expr const & ma, expr const & v) {
+bool type_inference::process_assignment(expr const & ma, expr const & v) {
     buffer<expr> args;
     expr const & m = get_app_args(ma, args);
     buffer<expr> locals;
@@ -617,6 +619,23 @@ bool type_inference::assign_mvar(expr const & ma, expr const & v) {
     if (!validate_assignment(m, locals, v))
         return false;
 
+    if (m_check_types) {
+        try {
+            scope s(*this);
+            expr t1 = infer(ma);
+            expr t2 = infer(v);
+            flet<bool> ignore_ext_mvar(m_ignore_external_mvars, true);
+            if (!is_def_eq_core(t1, t2))
+                return false;
+            s.commit();
+        } catch (exception &) {
+            // We may fail to infer the type of ma or v because the type may contain meta-variables.
+            // Example: ma may be of the form (?m a), and the type of ?m may be ?M where ?M is a
+            // (external) metavariable created by the unifier.
+            // We believe this only happens when we are interacting with the elaborator.
+        }
+    }
+
     if (args.empty()) {
         // easy case
         update_assignment(m, new_v);
@@ -655,7 +674,7 @@ lbool type_inference::quick_is_def_eq(expr const & e1, expr const & e2) {
         if (is_assigned(f1)) {
             return to_lbool(is_def_eq_core(subst_mvar(e1), e2));
         } else {
-            return to_lbool(assign_mvar(e1, e2));
+            return to_lbool(process_assignment(e1, e2));
         }
     }
 
@@ -664,10 +683,13 @@ lbool type_inference::quick_is_def_eq(expr const & e1, expr const & e2) {
         if (is_assigned(f2)) {
             return to_lbool(is_def_eq_core(e1, subst_mvar(e2)));
         } else {
-            return to_lbool(assign_mvar(e2, e1));
+            return to_lbool(process_assignment(e2, e1));
         }
     }
 
+    if (m_ignore_external_mvars && (is_meta(e1) || is_meta(e2)))
+        return l_true;
+
     if (e1.kind() == e2.kind()) {
         switch (e1.kind()) {
         case expr_kind::Lambda: case expr_kind::Pi:

src/library/type_inference.h

@@ -29,6 +29,44 @@ class type_inference {
     std::vector<pair<level, level>> m_postponed;
     name_map<projection_info>       m_proj_info;
 
+    // Internal (configuration) options for customers
+
+    /** If m_ignore_external_mvars is true, then we treat (external) expression meta-variables
+        as wildcards. That is, (?M t_1 ... t_n) matches any term T. We say a meta-variable is
+        external when is_mvar returns false for it, and this module can't assign it. */
+    bool                            m_ignore_external_mvars;
+
+    /** If m_check_types is true, then whenever we assign a meta-variable,
+        we check whether the type of the value matches the type of the meta-variable.
+        When this option is enabled, we turn on m_ignore_external_mvars while checking types.
+
+        At this point, this option is useful only for helping us solve universe unification constraints.
+        For example, consider the following unification problem
+        Given:
+             p   : Type.{l1}
+             q   : Type.{l2}
+             ?m1 : Type.{?u1}
+             ?m2 : Type.{?u2}
+
+             decidable.{max ?u1 u2} (?m1 -> ?m2)  =?=  decidable.{max l1 l2} (q -> p)
+
+        If m_check_types is turned off, the is_def_eq implemented here produces the incorrect solution
+
+             ?u1 := l1
+             ?u2 := l2
+             ?m1 := q
+             ?m2 := p
+
+        This solution is type incorrect.
+
+             ?m1 : Type.{l1}     q  : Type.{l2}
+             ?m2 : Type.{l2}     p  : Type.{l1}
+
+        TODO(Leo,Daniel): checking types is extra overhead, and it seems unnecessary most of the time.
+        We should investigate how often this kind of constraint occurs in blast.
+    */
+    bool                            m_check_types;
+
     bool is_opaque(declaration const & d) const;
     optional<expr> expand_macro(expr const & m);
     optional<expr> reduce_projection(expr const & e);
@@ -52,7 +90,7 @@ class type_inference {
     bool is_def_eq_proof_irrel(expr const & e1, expr const & e2);
 
     expr subst_mvar(expr const & e);
-    bool assign_mvar(expr const & ma, expr const & v);
+    bool process_assignment(expr const & ma, expr const & v);
     enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff };
     reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n);
     lbool lazy_delta_reduction(expr & t_n, expr & s_n);