feat(library/compiler): simplify cheap beta reduction

The LCNF format contained may `let`-declarations of the form
```
x : (fun y, c) a := t
```
where `c` does not depend on `y`.
We reduce them to
```
x : c := t
```

src/library/compiler/csimp.cpp

@@ -63,7 +63,7 @@ class csimp_fn {
         if (is_atom(e)) {
             return e;
         } else {
-            expr type = infer_type(e);
+            expr type = head_beta_const_fn(infer_type(e));
             expr fvar = m_lctx.mk_local_decl(ngen(), next_name(), type, e);
             m_fvars.push_back(fvar);
             return fvar;

src/library/compiler/lcnf.cpp

@@ -48,7 +48,7 @@ public:
     }
 
     expr mk_let_decl(expr const & e) {
-        expr type = infer_type(e);
+        expr type = head_beta_const_fn(infer_type(e));
         /* Remark: we use `m_x.append_after(m_next_idx)` instead of `name(m_x, m_next_idx)`
            because the resulting name is confusing during debugging: it looks like a projection application.
            We should replace it with `name(m_x, m_next_idx)` when the compiler code gets more stable. */

src/library/compiler/util.cpp

@@ -9,6 +9,24 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 
 namespace lean {
+expr head_beta_const_fn(expr const & e) {
+    if (!is_app(e)) return e;
+    expr fn = get_app_fn(e);
+    if (!is_lambda(fn)) return e;
+    buffer<expr> args;
+    get_app_args(e, args);
+    unsigned i = 0;
+    while (is_lambda(fn) && i < args.size()) {
+        expr const & body = binding_body(fn);
+        if (has_loose_bvars(body))
+            break;
+        i++;
+        fn = body;
+    }
+    if (i == 0) return e;
+    return mk_app(fn, args.size() - i, args.data() + i);
+}
+
 bool is_cases_on_recursor(environment const & env, name const & n) {
     return ::lean::is_aux_recursor(env, n) && n.get_string() == "cases_on";
 }

src/library/compiler/util.h

@@ -11,6 +11,10 @@ Author: Leonardo de Moura
 #include "library/util.h"
 
 namespace lean {
+/* If `e` is of the form `(fun x, t) a` return `head_beta_const_fn(t)` if `t` does not depend on `x`,
+   and `e` otherwise. */
+expr head_beta_const_fn(expr const & e);
+
 /* Return true if the given argument is mdata relevant to the compiler
 
    Remark: we currently don't keep any metadata in the compiler. */