fix(library/fun_info_manager): reducibility issue

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));

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);

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.

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