diff --git a/src/library/fun_info_manager.cpp b/src/library/fun_info_manager.cpp
index 32f7605f54..474d180512 100644
--- a/src/library/fun_info_manager.cpp
+++ b/src/library/fun_info_manager.cpp
@@ -36,13 +36,13 @@ list<unsigned> fun_info_manager::collect_deps(expr const & type, buffer<expr> co
 auto fun_info_manager::get(expr const & e) -> fun_info {
     if (auto r = m_fun_info.find(e))
         return *r;
-    expr type = m_ctx.infer(e);
+    expr type = m_ctx.relaxed_try_to_pi(m_ctx.infer(e));
     buffer<param_info> info;
     buffer<expr> locals;
     while (is_pi(type)) {
         expr local      = m_ctx.mk_tmp_local_from_binding(type);
         expr local_type = m_ctx.infer(local);
-        expr new_type   = m_ctx.whnf(instantiate(binding_body(type), local));
+        expr new_type   = m_ctx.relaxed_try_to_pi(instantiate(binding_body(type), local));
         bool is_prop    = m_ctx.is_prop(local_type);
         bool is_sub     = is_prop;
         bool is_dep     = !closed(binding_body(type));
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 9396f55d5a..9e3b452443 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -310,11 +310,24 @@ expr type_context::whnf(expr const & e) {
     }
 }
 
+expr type_context::try_to_pi(expr const & e) {
+    expr new_e = whnf(e);
+    if (is_pi(new_e))
+        return new_e;
+    else
+        return e;
+}
+
 expr type_context::relaxed_whnf(expr const & e) {
     flet<bool> relax(m_relax_is_opaque, true);
     return whnf(e);
 }
 
+expr type_context::relaxed_try_to_pi(expr const & e) {
+    flet<bool> relax(m_relax_is_opaque, true);
+    return try_to_pi(e);
+}
+
 bool type_context::relaxed_assign(expr const & ma, expr const & v) {
     flet<bool> relax(m_relax_is_opaque, true);
     return assign(ma, v);
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 04d6948892..d3dfe02174 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -439,6 +439,11 @@ public:
     /** \brief Infer the type of \c e. */
     expr infer(expr const & e);
 
+    /** \brief Put \c e in whnf, it is a Pi, then return whnf, otherwise return e */
+    expr try_to_pi(expr const & e);
+    /** \brief Put \c e in relaxed_whnf, it is a Pi, then return whnf, otherwise return e */
+    expr relaxed_try_to_pi(expr const & e);
+
     /** \brief Return true if \c e1 and \c e2 are definitionally equal.
         When \c e1 and \c e2, this method is not as complete as the one in the kernel.
         That is, it may return false even when \c e1 and \c e2 may be definitionally equal.
diff --git a/tests/lean/run/blast_fun_info_bug.lean b/tests/lean/run/blast_fun_info_bug.lean
new file mode 100644
index 0000000000..40795297e1
--- /dev/null
+++ b/tests/lean/run/blast_fun_info_bug.lean
@@ -0,0 +1,4 @@
+definition set (A : Type) := A → Prop
+
+example {A : Type} (s : set A) (a b : A) : a = b → s a → s b :=
+by blast