diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 90549c205..aa6ce89a4 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -1158,6 +1158,7 @@ class elaborator::imp {
                             push_front(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst));
                         return true;
                     } else {
+                        m_conflict = justification(new unification_failure_justification(c));
                         return false;
                     }
                 }