diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp
index 138f651a51..a91941ab49 100644
--- a/src/library/compiler/compiler.cpp
+++ b/src/library/compiler/compiler.cpp
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/max_sharing.h"
 #include "library/trace.h"
-#include "library/module.h"
 #include "library/vm/vm.h"
 #include "library/compiler/util.h"
 #include "library/compiler/lcnf.h"
@@ -78,11 +77,7 @@ static environment cache_stage1(environment env, comp_decls const & ds) {
         name n = d.fst();
         expr v = d.snd();
         constant_info info = env.get(n);
-        /* This a temporary hack to store Stage1 intermediate result.
-           We should not store this information as a declaration. */
-        declaration aux_decl = mk_definition(mk_cstage1_name(n), info.get_lparams(), info.get_type(),
-                                             v, reducibility_hints::mk_opaque(), true);
-        env = module::add(env, aux_decl, false);
+        env = register_stage1_decl(env, n, info.get_lparams(), info.get_type(), v);
     }
     return env;
 }
@@ -93,11 +88,7 @@ static environment cache_stage2(environment env, comp_decls const & ds) {
         expr v = d.snd();
         expr t = ll_infer_type(env, v);
         lean_trace(name({"compiler", "stage2"}), tout() << n << " : " << t << "\n";);
-        /* This a temporary hack to store Stage2 intermediate result.
-           We should not store this information as a declaration. */
-        declaration aux_decl = mk_definition(mk_cstage2_name(n), names(), t,
-                                             v, reducibility_hints::mk_opaque(), true);
-        env = module::add(env, aux_decl, false);
+        env = register_stage2_decl(env, n, t, v);
     }
     return env;
 }
diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index 3b66385c6a..62fc58978b 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -124,7 +124,7 @@ bool is_llnf_unbox(expr const & e) { return e == *g_unbox; }
 
    Remark: we use the instruction `_box.0` to box unboxed values of type `usize` into a boxed value (type `_obj`).
    We use `0` because the number of bytes necessary to store a `usize` is different in 32 and 64 bit machines. */
-expr mk_llnf_box(unsigned n);
+expr mk_llnf_box(unsigned n) { return mk_constant(name(*g_box, n)); }
 bool is_llnf_box(expr const & e, unsigned & n) { return is_llnf_unary_primitive(e, *g_box, n); }
 
 bool is_llnf_op(expr const & e) {
@@ -184,8 +184,13 @@ struct cnstr_info {
     }
 };
 
+static expr * g_usize = nullptr;
 std::vector<pair<name, unsigned>> * g_builtin_scalar_size = nullptr;
 
+bool is_usize_type(expr const & e) {
+    return is_constant(e, get_usize_name());
+}
+
 optional<unsigned> is_builtin_scalar(expr const & type) {
     if (!is_constant(type)) return optional<unsigned>();
     for (pair<name, unsigned> const & p : *g_builtin_scalar_size) {
@@ -247,7 +252,7 @@ class to_llnf_fn {
             } else if (m_unboxed) {
                 type_checker tc(m_st, lctx);
                 ftype = tc.whnf(ftype);
-                if (is_constant(ftype, get_usize_name())) {
+                if (is_usize_type(ftype)) {
                     result.push_back(field_info::mk_usize(next_usize));
                     next_usize++;
                 } else if (optional<unsigned> sz = is_builtin_scalar(ftype)) {
@@ -912,18 +917,56 @@ static environment update(environment const & env, boxed_functions_ext const & e
 
 /* Insert explicit boxing/unboxing instructions. */
 class explicit_boxing_fn {
-    environment       m_env;
-    name_generator    m_ngen;
-    local_ctx         m_lctx;
-    buffer<expr>      m_fvars;
-    name              m_x;
-    unsigned          m_next_idx{1};
-    buffer<comp_decl> m_new_decls;
+    environment         m_env;
+    boxed_functions_ext m_ext;
+    name_generator      m_ngen;
+    local_ctx           m_lctx;
+    buffer<expr>        m_fvars;
+    name                m_x;
+    unsigned            m_next_idx{1};
+    buffer<comp_decl>   m_new_decls;
+    expr                m_result_type;
+    optional<unsigned>  m_result_type_size;
 
     environment const & env() const { return m_env; }
 
     name_generator & ngen() { return m_ngen; }
 
+    /* usize     => some 0
+       uint8     => some 1
+       uint16    => some 2
+       uint32    => some 4
+       uint64    => some 8
+       otherwise => none */
+    optional<unsigned> get_type_size(expr const & type) {
+        if (is_usize_type(type)) {
+            /* Recall that we use 0 to denote the size of type `usize`.
+               See comment at `mk_llnf_box` above. */
+            return optional<unsigned>(0);
+        } else if (optional<unsigned> r = is_builtin_scalar(type)) {
+            return r;
+        } else {
+            lean_assert(m_result_type == mk_enf_object_type() ||
+                        m_result_type == mk_enf_neutral_type());
+            return optional<unsigned>();
+        }
+    }
+
+    expr get_constant_type(name const & c) {
+        // TODO(Leo): add support for builtin. We need to add a builtin management module
+        return env().get(mk_cstage2_name(c)).get_type();
+    }
+
+    /* Initialize `m_result_type` and `m_result_type` */
+    void init_result_type(name const & d_name) {
+        expr type = get_constant_type(d_name);
+        while (is_pi(type))
+            type = binding_body(type);
+        lean_assert(is_constant(type));
+        m_result_type      = type;
+        m_result_type_size = get_type_size(type);
+    }
+
     name next_name() {
         name r = m_x.append_after(m_next_idx);
         m_next_idx++;
@@ -945,21 +988,35 @@ class explicit_boxing_fn {
         return r;
     }
 
+    expr infer_jp_type(expr v) {
+        if (is_lambda(v)) {
+            return mk_arrow(binding_domain(v), infer_jp_type(binding_body(v)));
+        } else {
+            return m_result_type;
+        }
+    }
+
     expr visit_let(expr e) {
         buffer<expr> fvars;
         while (is_let(e)) {
             lean_assert(!has_loose_bvars(let_type(e)));
-            expr new_val = visit(instantiate_rev(let_value(e), fvars.size(), fvars.data()));
+            expr type    = let_type(e);
+            expr val     = instantiate_rev(let_value(e), fvars.size(), fvars.data());
             name n       = let_name(e);
-            if (is_internal_name(n) && !is_join_point_name(n)) {
-                n = next_name();
+            if (is_internal_name(n)) {
+                if (is_join_point_name(n)) {
+                    type = infer_jp_type(type);
+                } else {
+                    n    = next_name();
+                }
             }
-            expr new_fvar = m_lctx.mk_local_decl(ngen(), n, let_type(e), new_val);
+            val = visit(val, type);
+            expr new_fvar = m_lctx.mk_local_decl(ngen(), n, type, val);
             fvars.push_back(new_fvar);
             m_fvars.push_back(new_fvar);
             e = let_body(e);
         }
-        return visit(instantiate_rev(e, fvars.size(), fvars.data()));
+        return visit(instantiate_rev(e, fvars.size(), fvars.data()), m_result_type);
     }
 
     expr visit_lambda(expr e) {
@@ -972,19 +1029,249 @@ class explicit_boxing_fn {
         }
         e = instantiate_rev(e, binding_fvars.size(), binding_fvars.data());
         unsigned saved_fvars_size = m_fvars.size();
-        expr r = mk_let(saved_fvars_size, visit(e));
+        expr r = mk_let(saved_fvars_size, visit(e, m_result_type));
         lean_assert(!is_lambda(r));
         return m_lctx.mk_lambda(binding_fvars, r);
     }
 
-    expr visit_app(expr const & e) {
-        // TODO(Leo):
-        return e;
+    expr get_arg_type(expr const & e) {
+        lean_assert(is_fvar(e));
+        return m_lctx.get_local_decl(e).get_type();
     }
 
-    expr visit(expr const & e) {
+    expr unbox_if_needed(expr const & e, unsigned n) {
+        lean_assert(!is_enf_neutral(e));
+        lean_assert(is_fvar(e));
+        expr type = get_arg_type(e);
+        if (is_enf_object_type(type)) {
+            return mk_let_decl(*to_uint_type(n), mk_app(mk_llnf_unbox(), e));
+        } else {
+            return e;
+        }
+    }
+
+    expr box_if_needed(expr const & e) {
+        if (is_enf_neutral(e)) {
+            return e;
+        } else {
+            lean_assert(is_fvar(e));
+            expr type = get_arg_type(e);
+            if (is_enf_object_type(type)) {
+                return e;
+            } else if (is_usize_type(type)) {
+                return mk_let_decl(mk_enf_object_type(), mk_app(mk_llnf_box(0), e));
+            } else {
+                optional<unsigned> r = is_builtin_scalar(type);
+                lean_assert(r);
+                return mk_let_decl(mk_enf_object_type(), mk_app(mk_llnf_box(*r), e));
+            }
+        }
+    }
+
+    expr visit_cases(expr const & fn, buffer<expr> & args) {
+        lean_assert(is_constant(fn));
+        name const & c = const_name(fn);
+        lean_assert(is_cases_on_recursor(env(), c));
+        name const & I = c.get_prefix();
+        optional<unsigned> r = is_enum_type(env(), I);
+        if (r) {
+            args[0] = unbox_if_needed(args[0], *r);
+        }
+        for (unsigned i = 1; i < args.size(); i++) {
+            unsigned saved_fvars_size = m_fvars.size();
+            args[i] = mk_let(saved_fvars_size, visit(args[i], m_result_type));
+        }
+        return mk_app(fn, args);
+    }
+
+    bool is_unboxed(expr const & type) {
+        return type != mk_enf_object_type() && type != mk_enf_neutral_type();
+    }
+
+    bool has_unboxed(expr const & type) {
+        if (is_pi(type)) {
+            return is_unboxed(binding_domain(type)) || has_unboxed(binding_body(type));
+        } else {
+            return is_unboxed(type);
+        }
+    }
+
+    expr mk_boxed_version(name const & fn) {
+        if (name const * boxed_fn = m_ext.m_boxed_map.find(fn)) {
+            return mk_constant(*boxed_fn);
+        }
+        expr fn_type = get_constant_type(fn);
+        if (!has_unboxed(fn_type)) {
+            m_ext.m_boxed_map.insert(fn, fn);
+            return mk_constant(fn);
+        }
+        local_ctx lctx;
+        buffer<expr> args;
+        buffer<expr> fvars;
+        name y("_y");
+        unsigned idx = 1;
+        while (is_pi(fn_type)) {
+            expr fvar = lctx.mk_local_decl(ngen(), y.append_after(idx), mk_enf_object_type());
+            idx++;
+            fvars.push_back(fvar);
+            args.push_back(cast_if_needed(fvar, mk_enf_object_type(), binding_domain(fn_type)));
+            fn_type = binding_body(fn_type);
+        }
+        name new_fn(fn, "_boxed");
+        expr new_val = mk_app(mk_constant(fn), args);
+        new_val = cast_if_needed(new_val, fn_type, mk_enf_object_type());
+        new_val = lctx.mk_lambda(fvars, new_val);
+        m_new_decls.push_back(comp_decl(new_fn, new_val));
+        expr new_type = lctx.mk_pi(fvars, mk_enf_object_type());
+        m_ext.m_boxed_map.insert(fn, new_fn);
+        m_env = register_stage2_decl(m_env, new_fn, new_type, new_val);
+        return mk_constant(new_fn);
+    }
+
+    expr visit_closure(expr const & fn, buffer<expr> & args) {
+        lean_assert(is_constant(args[0]));
+        args[0] = mk_boxed_version(const_name(args[0]));
+        for (unsigned i = 1; i < args.size(); i++) {
+            args[i] = box_if_needed(args[i]);
+        }
+        return mk_app(fn, args);
+    }
+
+    expr visit_apply(expr const & fn, buffer<expr> & args, expr const & expected_type) {
+        for (unsigned i = 1; i < args.size(); i++) {
+            args[i] = box_if_needed(args[i]);
+        }
+        expr r = mk_app(fn, args);
+        if (expected_type != mk_enf_object_type()) {
+            r = mk_let_decl(mk_enf_object_type(), r);
+            r = mk_let_decl(expected_type, mk_app(mk_llnf_unbox(), r));
+        }
+        return r;
+    }
+
+    void box_args_if_needed(buffer<expr> & args) {
+        for (expr & arg : args) {
+            arg = box_if_needed(arg);
+        }
+    }
+
+    expr visit_cnstr(expr const & fn, buffer<expr> & args, expr const & expected_type) {
+        if (args.size() == 0 && expected_type != mk_enf_object_type()) {
+            unsigned cidx = 0;
+            unsigned n1, n2;
+            is_llnf_cnstr(fn, cidx, n1, n2);
+            expr r = mk_let_decl(expected_type, mk_lit(literal(nat(cidx))));
+            return r;
+        } else {
+            box_args_if_needed(args);
+            return mk_app(fn, args);
+        }
+    }
+
+    expr visit_reuse(expr const & fn, buffer<expr> & args) {
+        box_args_if_needed(args);
+        return mk_app(fn, args);
+    }
+
+    expr cast_if_needed(expr e, expr const & e_type, expr const & expected_type) {
+        if (e_type == expected_type)
+            return e;
+        if (!is_fvar(e))
+            e = mk_let_decl(e_type, e);
+        if (expected_type == mk_enf_object_type()) {
+            return mk_let_decl(mk_enf_object_type(), mk_app(mk_llnf_box(*get_type_size(e_type)), e));
+        } else {
+            lean_assert(e_type == mk_enf_object_type());
+            return mk_let_decl(expected_type, mk_app(mk_llnf_unbox(), e));
+        }
+    }
+
+    expr visit_sset(expr const & fn, buffer<expr> & args) {
+        lean_assert(args.size() == 2);
+        unsigned sz = 0;
+        unsigned d1, d2;
+        is_llnf_sset(fn, sz, d1, d2);
+        args[1] = cast_if_needed(args[1], get_arg_type(args[1]), *to_uint_type(sz));
+        return mk_app(fn, args);
+    }
+
+    expr visit_uset(expr const & fn, buffer<expr> & args) {
+        lean_assert(args.size() == 2);
+        args[1] = cast_if_needed(args[1], get_arg_type(args[1]), *g_usize);
+        return mk_app(fn, args);
+    }
+
+    expr visit_jmp(expr const & fn, buffer<expr> & args) {
+        expr jp_type = get_arg_type(args[0]);
+        for (unsigned i = 1; i < args.size(); i++) {
+            lean_assert(is_fvar(args[i]));
+            lean_assert(is_pi(jp_type));
+            expr arg_expected_type = binding_domain(jp_type);
+            expr arg_type          = get_arg_type(args[i]);
+            args[i] = cast_if_needed(args[i], arg_type, arg_expected_type);
+            jp_type = binding_body(jp_type);
+        }
+        return mk_app(fn, args);
+    }
+
+    expr visit_app_default(expr const & fn, buffer<expr> & args, expr const & expected_type) {
+        expr type = get_constant_type(const_name(fn));
+        for (expr & arg : args) {
+            lean_assert(is_pi(type));
+            if (is_fvar(arg)) {
+                expr arg_expected_type = binding_domain(type);
+                expr arg_type          = get_arg_type(arg);
+                arg = cast_if_needed(arg, arg_type, arg_expected_type);
+            } else {
+                lean_assert(is_enf_neutral(arg));
+            }
+            type = binding_body(type);
+        }
+        lean_assert(!is_pi(type));
+        expr r = mk_app(fn, args);
+        return cast_if_needed(r, type, expected_type);
+    }
+
+    expr visit_app(expr const & e, expr const & expected_type) {
+        buffer<expr> args;
+        expr const & f = get_app_args(e, args);
+        lean_assert(is_constant(f));
+        name const & fn = const_name(f);
+        if (is_cases_on_recursor(env(), fn)) {
+            lean_assert(!is_let_val);
+            return visit_cases(f, args);
+        } else if (is_llnf_closure(f)) {
+            return visit_closure(f, args);
+        } else if (is_llnf_apply(f)) {
+            return visit_apply(f, args, expected_type);
+        } else if (is_llnf_cnstr(f)) {
+            return visit_cnstr(f, args, expected_type);
+        } else if (is_llnf_reuse(f)) {
+            return visit_reuse(f, args);
+        } else if (is_llnf_sset(f)) {
+            return visit_sset(f, args);
+        } else if (is_llnf_uset(f)) {
+            return visit_uset(f, args);
+        } else if (is_llnf_proj(f)) {
+            return e;
+        } else if (is_llnf_sproj(f)) {
+            return e;
+        } else if (is_llnf_uproj(f)) {
+            return e;
+        } else if (is_llnf_jmp(f)) {
+            return visit_jmp(f, args);
+        } else if (is_llnf_box(f)) {
+            lean_unreachable();
+        } else if (is_llnf_unbox(f)) {
+            lean_unreachable();
+        } else {
+            return visit_app_default(f, args, expected_type);
+        }
+    }
+
+    expr visit(expr const & e, expr const & expected_type) {
         switch (e.kind()) {
-        case expr_kind::App:    return visit_app(e);
+        case expr_kind::App:    return visit_app(e, expected_type);
         case expr_kind::Lambda: return visit_lambda(e);
         case expr_kind::Let:    return visit_let(e);
         default:                return e;
@@ -993,12 +1280,14 @@ class explicit_boxing_fn {
 
 public:
     explicit_boxing_fn(environment const & env):
-        m_env(env), m_x("_x") {}
+        m_env(env), m_ext(get_extension(env)), m_x("_x") {}
 
     pair<environment, comp_decls> operator()(comp_decl const & d) {
-        expr new_v = visit(d.snd());
+        init_result_type(d.fst());
+        expr new_v = visit(d.snd(), m_result_type);
         new_v = mk_let(0, new_v);
         comp_decls new_ds(comp_decl(d.fst(), new_v), comp_decls(m_new_decls));
+        m_env = update(m_env, m_ext);
         return mk_pair(m_env, new_ds);
     }
 };
@@ -1023,6 +1312,7 @@ pair<environment, comp_decls> to_llnf(environment const & env, comp_decls const
 }
 
 void initialize_llnf() {
+    g_usize     = new expr(mk_constant(get_usize_name()));
     g_apply     = new expr(mk_constant("_apply"));
     g_closure   = new expr(mk_constant("_closure"));
     g_cnstr     = new name("_cnstr");
@@ -1045,6 +1335,7 @@ void initialize_llnf() {
 }
 
 void finalize_llnf() {
+    delete g_usize;
     delete g_closure;
     delete g_apply;
     delete g_cnstr;
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 6b9d59dd02..4323569485 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "library/aux_recursors.h"
 #include "library/replace_visitor.h"
 #include "library/constants.h"
+#include "library/module.h"
 #include "library/compiler/util.h"
 
 namespace lean {
@@ -447,6 +448,17 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) {
     }
 }
 
+environment register_stage1_decl(environment const & env, name const & n, names const & ls, expr const & t, expr const & v) {
+    declaration aux_decl = mk_definition(mk_cstage1_name(n), ls, t, v, reducibility_hints::mk_opaque(), true);
+    return module::add(env, aux_decl, false);
+}
+
+environment register_stage2_decl(environment const & env, name const & n, expr const & t, expr const & v) {
+    declaration aux_decl = mk_definition(mk_cstage2_name(n), names(), t,
+                                         v, reducibility_hints::mk_opaque(), true);
+    return module::add(env, aux_decl, false);
+}
+
 void initialize_compiler_util() {
     g_neutral_expr     = new expr(mk_constant("_neutral"));
     g_unreachable_expr = new expr(mk_constant("_unreachable"));
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index 3187dd2db6..b16ca77cff 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -150,6 +150,9 @@ bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & t
 
 void collect_used(expr const & e, std::unordered_set<name, name_hash> & S);
 
+environment register_stage1_decl(environment const & env, name const & n, names const & ls, expr const & t, expr const & v);
+environment register_stage2_decl(environment const & env, name const & n, expr const & t, expr const & v);
+
 void initialize_compiler_util();
 void finalize_compiler_util();
 }