diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index d91d76efeb..3969c5e1c4 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1778,6 +1778,15 @@ bool type_context::process_assignment(expr const & m, expr const & v) {
     try {
         expr t1 = infer(mvar);
         expr t2 = infer(new_v);
+        /* TODO(Leo): check whether using transparency_mode::All hurts performance.
+           We use Semireducible to make sure we will not fail an unification step
+                   ?m := t
+           because we cannot establish that the types of ?m and t are definitionally equal
+           due to the current transparency setting.
+           This change is consistent with the general approach used in the rest of the code
+           base where spurious typing errors due reducibility are avoided by using
+           relaxed_is_def_eq. */
+        transparency_scope _(*this, transparency_mode::All);
         if (!is_def_eq_core(t1, t2)) {
             lean_trace(name({"type_context", "is_def_eq_detail"}),
                        scope_trace_env scope(env(), *this);