diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 4d957ac6d9..03ef0b7dc1 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -1205,7 +1205,15 @@ class elaborator::imp {
             return true;
         }
 
-        if (a.kind() != b.kind() && !has_metavar(a) && !has_metavar(b)) {
+        // If 'a' and 'b' have different kinds, and 'a' and 'b' are not metavariables,
+        // and 'a' and 'b' are not applications where the function contains metavariables,
+        // then it is not possible to unify 'a' and 'b'.
+        // We need the last condition because if 'a'/'b' are applications containing metavariables,
+        // then they can be reduced when the metavariable is assigned
+        // Here is an example:
+        //     |- (?m Type) << Type
+        // If ?m is assigned to the identity function (fun x, x), then the constraint can be solved.
+        if (a.kind() != b.kind() && !is_metavar(a) && !is_metavar(b) && !(is_app(a) && has_metavar(arg(a, 0))) && !(is_app(b) && has_metavar(arg(b, 0)))) {
             m_conflict = justification(new unification_failure_justification(c));
             return false;
         }
diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out
index 3da47b5760..070159bf34 100644
--- a/tests/lean/elab1.lean.expected.out
+++ b/tests/lean/elab1.lean.expected.out
@@ -135,7 +135,11 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
   Assumed: a
   Assumed: b
   Assumed: H
-Error (line: 20, pos: 59) failed to synthesize metavar, its type is not a proposition
+Failed to solve
+ ⊢ if ?M::0 ?M::1 ⊤ ≺ b
+    Normalize
+     ⊢ ?M::0 ⇒ ?M::1 ≺ b
+        (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
 Failed to solve
  ⊢ b ≈ a
     Substitution