diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 7abe6d3e00..8a45495f4c 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2543,6 +2543,11 @@ expr type_context::elim_delayed_abstraction(expr const & e) {
     return r;
 }
 
+static bool mvar_has_user_facing_name(expr const & m) {
+    lean_assert(is_metavar(m));
+    return mlocal_name(m) != mlocal_pp_name(m);
+}
+
 lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
     if (e1 == e2)
         return l_true;
@@ -2572,24 +2577,38 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
             optional<metavar_decl> m2_decl = m_mctx.find_metavar_decl(f2);
             if (m1_decl && m2_decl) {
                 if (m2_decl->get_context().is_subset_of(m1_decl->get_context())) {
-                    if (!is_app(e1) || is_app(e2)) {
+                    /* Remark:
+                       It is easier to solve the assignment
+                          ?m2 := ?m1 a_1 ... a_n
+                       than
+                          ?m1 a_1 ... a_n := ?m2
+
+                       Reason: the first one is precise. For example,
+                       consider the following constraint:
+
+                          ?m1 ?m =?= ?m2
+                    */
+                    if (!is_app(e1) && is_app(e2)) {
+                        /* ?m1 := ?m2 a_1 ... a_n */
                         return to_lbool(process_assignment(e1, e2));
                     } else if (m1_decl->get_context().is_subset_of(m2_decl->get_context())) {
-                        lean_assert(is_app(e1) && !is_app(e2));
-                        /* It is easier to solve the assignment
-                                 ?m2 := ?m1 a_1 ... a_n
-                           than
-                                 ?m1 a_1 ... a_n := ?m2
-                           Reason: the first one is precise. For example,
-                           consider the following constraint:
-
-                                 ?m1 ?m =?= ?m2
-                        */
-                        return to_lbool(process_assignment(e2, e1));
+                        lean_assert(is_app(e1) || !is_app(e2));
+                        if ((is_app(e1) && !is_app(e2)) || /* ?m2 := ?m1 a_1 ... a_n */
+                            (!mvar_has_user_facing_name(f2) && mvar_has_user_facing_name(f1)) /* ?m2 does not have a user facing name, but ?m1 has */
+                            ) {
+                            /* Remark: the second case (?m2 has user facing name but ?m1 doesn't) is particularly for
+                               the equation preprocessor. See issue #1801. */
+                            return to_lbool(process_assignment(e2, e1));
+                        } else {
+                            return to_lbool(process_assignment(e1, e2));
+                        }
                     } else {
+                        lean_assert(m2_decl->get_context().is_subset_of(m1_decl->get_context()));
+                        lean_assert(!m1_decl->get_context().is_subset_of(m2_decl->get_context()));
                         return to_lbool(process_assignment(e1, e2));
                     }
                 } else {
+                    lean_assert(!m2_decl->get_context().is_subset_of(m1_decl->get_context()));
                     return to_lbool(process_assignment(e2, e1));
                 }
             } else {
diff --git a/tests/lean/def_inaccessible_issue.lean.expected.out b/tests/lean/def_inaccessible_issue.lean.expected.out
index 023f20bc55..5599ccc6b4 100644
--- a/tests/lean/def_inaccessible_issue.lean.expected.out
+++ b/tests/lean/def_inaccessible_issue.lean.expected.out
@@ -1,3 +1,3 @@
 map2.equations._eqn_2 :
-  ∀ (f : bool → bool → bool) (x : ℕ) (b1 : bool) (v1 : bv x) (b2 : bool) (v2 : bv x),
-    map2 f (cons x b1 v1) (cons x b2 v2) = cons x (f b1 b2) (map2 f v1 v2)
+  ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv n) (b2 : bool) (v2 : bv n),
+    map2 f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2 f v1 v2)
diff --git a/tests/lean/eqn_compiler_error_msg.lean.expected.out b/tests/lean/eqn_compiler_error_msg.lean.expected.out
index a6cc4fdedc..30f739b496 100644
--- a/tests/lean/eqn_compiler_error_msg.lean.expected.out
+++ b/tests/lean/eqn_compiler_error_msg.lean.expected.out
@@ -1,3 +1,3 @@
 eqn_compiler_error_msg.lean:5:28: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
-  .?m_1 + .?m_2
+  .p + .n
 eqn_compiler_error_msg.lean:4:6: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out
index 0756178ca1..a1e0214203 100644
--- a/tests/lean/inaccessible2.lean.expected.out
+++ b/tests/lean/inaccessible2.lean.expected.out
@@ -7,7 +7,7 @@ inaccessible2.lean:11:46: error: invalid expression
 inaccessible2.lean:11:4: error: invalid application, function expected
 inaccessible2.lean:11:46: error: ill-formed match/equation expression
 inaccessible2.lean:11:46: error: command expected
-inaccessible2.lean:14:27: error: don't know how to synthesize placeholder
+inaccessible2.lean:14:21: error: don't know how to synthesize placeholder
 context:
 A : Sort ?,
 symm : ∀ (a b : A), a = b → b = a
diff --git a/tests/lean/inject.lean.expected.out b/tests/lean/inject.lean.expected.out
index 004e5cb2ff..0972e3501c 100644
--- a/tests/lean/inject.lean.expected.out
+++ b/tests/lean/inject.lean.expected.out
@@ -3,12 +3,12 @@ lift.equations._eqn_2 : ∀ {m k : ℕ} (f : fi m → fi k) (n : ℕ), @lift m k
 lift.equations._eqn_3 :
   ∀ {m k : ℕ} (f : fi m → fi k) (n : ℕ) (i : fi (m + n)),
     @lift m k f (succ n) (@fs (m + n) i) = @fs (k + n) (@lift m k f n i)
-to_nat.equations._eqn_1 : ∀ (x : ℕ), @to_nat (succ x) (@f0 x) = 0
-to_nat.equations._eqn_2 : ∀ (x : ℕ) (i : fi x), @to_nat (succ x) (@fs x i) = succ (@to_nat x i)
-inject.equations._eqn_1 : ∀ (x : ℕ) (i : fi x), @inject (succ x) (@fs x i) (@f0 (@to_nat x i)) = @f0 x
+to_nat.equations._eqn_1 : ∀ (n : ℕ), @to_nat (succ n) (@f0 n) = 0
+to_nat.equations._eqn_2 : ∀ (n : ℕ) (i : fi n), @to_nat (succ n) (@fs n i) = succ (@to_nat n i)
+inject.equations._eqn_1 : ∀ (n : ℕ) (i : fi n), @inject (succ n) (@fs n i) (@f0 (@to_nat n i)) = @f0 n
 inject.equations._eqn_2 :
-  ∀ (x : ℕ) (i : fi x) (j : fi (@to_nat x i)),
-    @inject (succ x) (@fs x i) (@fs (@to_nat x i) j) = @fs x (@inject x i j)
+  ∀ (n : ℕ) (i : fi n) (j : fi (@to_nat n i)),
+    @inject (succ n) (@fs n i) (@fs (@to_nat n i) j) = @fs n (@inject n i j)
 inject'.equations._eqn_1 : ∀ (n : ℕ) (i : fi n), @inject' (succ n) (@fs n i) (@f0 (@to_nat n i)) = @f0 n
 inject'.equations._eqn_2 :
   ∀ (n : ℕ) (i : fi n) (j : fi (@to_nat n i)),
@@ -16,10 +16,10 @@ inject'.equations._eqn_2 :
 raise.equations._eqn_1 : ∀ {m : ℕ} (i : fi m), @raise m 0 i = i
 raise.equations._eqn_2 : ∀ {m : ℕ} (n : ℕ) (i : fi m), @raise m (succ n) i = @fs (m + n) (@raise m n i)
 deg.equations._eqn_1 : ∀ (n : ℕ) (j : fi (succ n)), @deg (succ n) (@f0 (succ n)) j = @fs (succ n) j
-deg.equations._eqn_2 : ∀ (x : ℕ) (i : fi (succ x)), @deg (succ x) (@fs (succ x) i) (@f0 x) = @f0 (succ x)
+deg.equations._eqn_2 : ∀ (n : ℕ) (i : fi (succ n)), @deg (succ n) (@fs (succ n) i) (@f0 n) = @f0 (succ n)
 deg.equations._eqn_3 :
-  ∀ (x : ℕ) (i : fi (succ x)) (j : fi x), @deg (succ x) (@fs (succ x) i) (@fs x j) = @fs (succ x) (@deg x i j)
+  ∀ (n : ℕ) (i : fi (succ n)) (j : fi n), @deg (succ n) (@fs (succ n) i) (@fs n j) = @fs (succ n) (@deg n i j)
 deg'.equations._eqn_1 : ∀ (n : ℕ) (j : fi (succ n)), @deg' (succ n) (@f0 (succ n)) j = @fs (succ n) j
-deg'.equations._eqn_2 : ∀ (x : ℕ) (i : fi (succ x)), @deg' (succ x) (@fs (succ x) i) (@f0 x) = @f0 (succ x)
+deg'.equations._eqn_2 : ∀ (n : ℕ) (i : fi (succ n)), @deg' (succ n) (@fs (succ n) i) (@f0 n) = @f0 (succ n)
 deg'.equations._eqn_3 :
-  ∀ (x : ℕ) (i : fi (succ x)) (j : fi x), @deg' (succ x) (@fs (succ x) i) (@fs x j) = @fs (succ x) (@deg' x i j)
+  ∀ (n : ℕ) (i : fi (succ n)) (j : fi n), @deg' (succ n) (@fs (succ n) i) (@fs n j) = @fs (succ n) (@deg' n i j)
diff --git a/tests/lean/offset_is_def_eq_trick.lean.expected.out b/tests/lean/offset_is_def_eq_trick.lean.expected.out
index 56296405a7..dda1efbaa4 100644
--- a/tests/lean/offset_is_def_eq_trick.lean.expected.out
+++ b/tests/lean/offset_is_def_eq_trick.lean.expected.out
@@ -1 +1 @@
-head.equations._eqn_1 : ∀ {α : Type u_1} (x : ℕ) (h : α) (t : Vec α x), head (Vec.cons h t) = h
+head.equations._eqn_1 : ∀ {α : Type u_1} (n : ℕ) (h : α) (t : Vec α n), head (Vec.cons h t) = h