feat(library/type_context): improve type_context get_level_core, add virtual method for checking types whenever a metavariable is assigned

We add an example where app_builder fails without these new features.
That is, app_builder fails to solve the unification problem.

src/library/type_context.cpp

@@ -744,6 +744,10 @@ bool type_context::is_def_eq_proof_irrel(expr const & e1, expr const & e2) {
     return false;
 }
 
+bool type_context::validate_assignment_types(expr const & m, expr const & v) {
+    return is_def_eq_core(infer_metavar(m), infer(v));
+}
+
 /** \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_context::process_assignment_core(expr const & ma, expr const & v) {
@@ -789,11 +793,8 @@ bool type_context::process_assignment_core(expr const & ma, expr const & v) {
 
     if (args.empty()) {
         // easy case
-        update_assignment(m, new_v);
-        return true;
     } else if (args.size() == locals.size()) {
-        update_assignment(m, Fun(locals, new_v));
-        return true;
+        new_v = Fun(locals, new_v);
     } else {
         // This case is imprecise since it is not a higher order pattern.
         // That the term \c ma is of the form (?m t_1 ... t_n) and the t_i's are not pairwise
@@ -810,9 +811,10 @@ bool type_context::process_assignment_core(expr const & ma, expr const & v) {
             m_type = instantiate(binding_body(m_type), locals[i]);
         }
         lean_assert(locals.size() == args.size());
-        update_assignment(m, Fun(locals, new_v));
-        return true;
+        new_v = Fun(locals, new_v);
     }
+    update_assignment(m, new_v);
+    return validate_assignment_types(m, new_v);
 }
 
 bool type_context::process_assignment(expr const & ma, expr const & v) {
@@ -1106,17 +1108,29 @@ expr type_context::infer_lambda(expr e) {
 
 optional<level> type_context::get_level_core(expr const & A) {
     expr A_type = relaxed_whnf(infer(A));
-    if (is_sort(A_type))
-        return some_level(sort_level(A_type));
-    else
-        return none_level();
+    while (true) {
+        if (is_sort(A_type)) {
+            return some_level(sort_level(A_type));
+        } else if (is_mvar(A_type)) {
+            if (auto v = get_assignment(A_type)) {
+                A_type = *v;
+            } else {
+                level r = mk_uvar();
+                update_assignment(A_type, mk_sort(r));
+                return some_level(r);
+            }
+        } else {
+            return none_level();
+        }
+    }
 }
 
 level type_context::get_level(expr const & A) {
-    if (auto r = get_level_core(A))
+    if (auto r = get_level_core(A)) {
         return *r;
-    else
+    } else {
         throw exception("infer type failed, sort expected");
+    }
 }
 
 expr type_context::infer_pi(expr const & e0) {
@@ -1866,6 +1880,13 @@ bool default_type_context::ignore_universe_def_eq(level const & l1, level const
     }
 }
 
+bool default_type_context::validate_assignment_types(expr const &, expr const &) {
+    // We disable this check because the interface between type_context and the elaborator unifier
+    // is currently quite brittle.
+    // Recall that this class is used to implement the type class inference in the Lean frontend.
+    return true;
+}
+
 expr normalizer::normalize_binding(expr const & e) {
     expr d = normalize(binding_domain(e));
     expr l = m_ctx.mk_tmp_local(binding_name(e), d, binding_info(e));

src/library/type_context.h

@@ -406,6 +406,13 @@ public:
         whether all internal local constants in v occur in locals.
         The default implementation only checks that. */
     virtual bool validate_assignment(expr const & m, buffer<expr> const & locals, expr const & v);
+    /** \brief Given a metavariable and the value \c v that has already been abstracted.
+        Check if the types match.
+        \remark By checking the types we may be able to assign additional metavariables.
+        The default implementation is:
+
+        return is_def_eq_core(infer_metavar(m), infer(v)); */
+    virtual bool validate_assignment_types(expr const & m, expr const & v);
 
     /** \brief Return the type of a local constant (local or not).
         \remark This method allows the customer to store the type of local constants
@@ -596,6 +603,7 @@ public:
     virtual void pop() { lean_assert(!m_trail.empty()); m_assignment = m_trail.back(); m_trail.pop_back(); }
     virtual void commit() { lean_assert(!m_trail.empty()); m_trail.pop_back(); }
     virtual optional<expr> mk_subsingleton_instance(expr const & type);
+    virtual bool validate_assignment_types(expr const & m, expr const & v);
     // TODO(REMOVE)
     bool & get_ignore_if_zero() { return m_ignore_if_zero; }
 };

tests/lean/run/app_builder_issue1.lean

@@ -0,0 +1,4 @@
+constant f {A : Type} (a : A) {B : Type} (b : B) : nat
+
+example (a b c d : nat) : a = c → b = d → f a b = f c d :=
+by simp