diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 7eb9c0d512..d4573946bb 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -781,11 +781,13 @@ public:
             f_type = whnf(f_type, cs);
         if (!is_pi(f_type) && has_metavar(f_type)) {
             constraint_seq saved_cs = cs;
-            f_type = whnf(f_type, cs);
-            if (!is_pi(f_type) && is_meta(f_type)) {
+            expr new_f_type = whnf(f_type, cs);
+            if (!is_pi(new_f_type) && is_meta(new_f_type)) {
                 cs = saved_cs;
                 // let type checker add constraint
                 f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
+            } else {
+                f_type = new_f_type;
             }
         }
         if (!is_pi(f_type)) {