From e925ec179567449132ceb72f34b497a7b15e3f0b Mon Sep 17 00:00:00 2001
From: Louis Gesbert <louis.gesbert@ocamlpro.com>
Date: Thu, 6 Oct 2022 19:13:45 +0200
Subject: [PATCH] Swap boxing and annotations in expressions

This was the only reasonable solution I found to the issue raised
[here](https://github.com/CatalaLang/catala/pull/334#discussion_r987175884).

This was a pretty tedious rewrite, but it should now ensure we are doing things
correctly. As a bonus, the "smart" expression constructors are now used
everywhere to build expressions (so another refactoring like this one should be
much easier) and this makes the code overall feel more
straightforward (`Bindlib.box_apply` or `let+` no longer need to be visible!)

---

Basically, we were using values of type `gexpr box = naked_gexpr marked box`
throughout when (re-)building expressions. This was done 99% of the time by
using `Bindlib.box_apply add_mark naked_e` right after building `naked_e`. In
lots of places, we needed to recover the annotation of this expression later on,
typically to build its parent term (to inherit the position, or build the type).

Since it wasn't always possible to wrap these uses within `box_apply` (esp. as
bindlib boxes aren't a monad), here and there we had to call `Bindlib.unbox`,
just to recover the position or type. This had the very unpleasant effect of
forcing the resolution of the whole box (including applying any stored closures)
to reach the top-level annotation which isn't even dependant on specific
variable bindings. Then, generally, throwing away the result.

Therefore, the change proposed here transforms
- `naked_gexpr marked Bindlib.box` into
- `naked_gexpr Bindlib.box marked` (aliased to `boxed_gexpr` or `gexpr boxed` for
convenience)

This means only
1. not fitting the mark into the box right away when building, and
2. accessing the top-level mark directly without unboxing

The functions for building terms from module `Shared_ast.Expr` could be changed
easily. But then they needed to be consistently used throughout, without
manually building terms through `Bindlib.apply_box` -- which covers most of the
changes in this patch.

`Expr.Box.inj` is provided to swap back to a box, before binding for example.

Additionally, this gives a 40% speedup on `make -C examples pass_all_tests`,
which hints at the amount of unnecessary work we were doing --'
---
 compiler/dcalc/interpreter.ml                |   4 +-
 compiler/desugared/ast.ml                    |  34 +-
 compiler/desugared/ast.mli                   |   6 +-
 compiler/desugared/desugared_to_scope.ml     | 248 ++++-----
 compiler/driver.ml                           |   7 +-
 compiler/lcalc/ast.ml                        |  37 +-
 compiler/lcalc/ast.mli                       |  17 +-
 compiler/lcalc/closure_conversion.ml         | 146 ++----
 compiler/lcalc/compile_with_exceptions.ml    |  34 +-
 compiler/lcalc/compile_without_exceptions.ml |  59 +--
 compiler/lcalc/optimizations.ml              | 139 ++----
 compiler/scopelang/ast.ml                    |   6 +-
 compiler/scopelang/ast.mli                   |  10 -
 compiler/scopelang/scope_to_dcalc.ml         | 170 +++----
 compiler/shared_ast/definitions.ml           |   8 +-
 compiler/shared_ast/expr.ml                  | 228 +++++----
 compiler/shared_ast/expr.mli                 | 236 ++++++---
 compiler/shared_ast/program.mli              |   6 +-
 compiler/shared_ast/scope.ml                 |  23 +-
 compiler/shared_ast/scope.mli                |  17 +-
 compiler/shared_ast/typing.ml                | 498 +++++++++----------
 compiler/shared_ast/typing.mli               |   2 +-
 compiler/surface/desugaring.ml               | 461 +++++++----------
 compiler/verification/conditions.ml          |   2 +-
 compiler/verification/z3backend.real.ml      |  56 +--
 25 files changed, 1111 insertions(+), 1343 deletions(-)

diff --git a/compiler/dcalc/interpreter.ml b/compiler/dcalc/interpreter.ml
index 17167c8f..1b164337 100644
--- a/compiler/dcalc/interpreter.ml
+++ b/compiler/dcalc/interpreter.ml
@@ -502,11 +502,11 @@ let interpret_program :
         taus
     in
     let to_interpret =
-      Expr.make_app (Bindlib.box e)
+      Expr.make_app (Expr.box e)
         [Expr.make_tuple application_term (Some s_in) mark_e]
         (Expr.pos e)
     in
-    match Marked.unmark (evaluate_expr ctx (Bindlib.unbox to_interpret)) with
+    match Marked.unmark (evaluate_expr ctx (Expr.unbox to_interpret)) with
     | ETuple (args, Some s_out) ->
       let s_out_fields =
         List.map
diff --git a/compiler/desugared/ast.ml b/compiler/desugared/ast.ml
index d5a1c8a7..a38a794e 100644
--- a/compiler/desugared/ast.ml
+++ b/compiler/desugared/ast.ml
@@ -112,8 +112,8 @@ type label_situation = ExplicitlyLabeled of LabelName.t Marked.pos | Unlabeled
 
 type rule = {
   rule_id : RuleName.t;
-  rule_just : expr Bindlib.box;
-  rule_cons : expr Bindlib.box;
+  rule_just : expr boxed;
+  rule_cons : expr boxed;
   rule_parameter : (expr Var.t * typ) option;
   rule_exception : exception_situation;
   rule_label : label_situation;
@@ -127,25 +127,25 @@ module Rule = struct
   let compare r1 r2 =
     match r1.rule_parameter, r2.rule_parameter with
     | None, None -> (
-      let j1 = Bindlib.unbox r1.rule_just in
-      let j2 = Bindlib.unbox r2.rule_just in
+      let j1 = Expr.unbox r1.rule_just in
+      let j2 = Expr.unbox r2.rule_just in
       match Expr.compare j1 j2 with
       | 0 ->
-        let c1 = Bindlib.unbox r1.rule_cons in
-        let c2 = Bindlib.unbox r2.rule_cons in
+        let c1 = Expr.unbox r1.rule_cons in
+        let c2 = Expr.unbox r2.rule_cons in
         Expr.compare c1 c2
       | n -> n)
     | Some (v1, t1), Some (v2, t2) -> (
       match Shared_ast.Expr.compare_typ t1 t2 with
       | 0 -> (
         let open Bindlib in
-        let b1 = unbox (bind_var v1 r1.rule_just) in
-        let b2 = unbox (bind_var v2 r2.rule_just) in
+        let b1 = unbox (bind_var v1 (Expr.Box.inj r1.rule_just)) in
+        let b2 = unbox (bind_var v2 (Expr.Box.inj r2.rule_just)) in
         let _, j1, j2 = unbind2 b1 b2 in
         match Expr.compare j1 j2 with
         | 0 ->
-          let b1 = unbox (bind_var v1 r1.rule_cons) in
-          let b2 = unbox (bind_var v2 r2.rule_cons) in
+          let b1 = unbox (bind_var v1 (Expr.Box.inj r1.rule_cons)) in
+          let b2 = unbox (bind_var v2 (Expr.Box.inj r2.rule_cons)) in
           let _, c1, c2 = unbind2 b1 b2 in
           Expr.compare c1 c2
         | n -> n)
@@ -156,8 +156,8 @@ end
 
 let empty_rule (pos : Pos.t) (have_parameter : typ option) : rule =
   {
-    rule_just = Bindlib.box (ELit (LBool false), Untyped { pos });
-    rule_cons = Bindlib.box (ELit LEmptyError, Untyped { pos });
+    rule_just = Expr.box (ELit (LBool false), Untyped { pos });
+    rule_cons = Expr.box (ELit LEmptyError, Untyped { pos });
     rule_parameter =
       (match have_parameter with
       | Some typ -> Some (Var.make "dummy", typ)
@@ -169,8 +169,8 @@ let empty_rule (pos : Pos.t) (have_parameter : typ option) : rule =
 
 let always_false_rule (pos : Pos.t) (have_parameter : typ option) : rule =
   {
-    rule_just = Bindlib.box (ELit (LBool true), Untyped { pos });
-    rule_cons = Bindlib.box (ELit (LBool false), Untyped { pos });
+    rule_just = Expr.box (ELit (LBool true), Untyped { pos });
+    rule_cons = Expr.box (ELit (LBool false), Untyped { pos });
     rule_parameter =
       (match have_parameter with
       | Some typ -> Some (Var.make "dummy", typ)
@@ -180,7 +180,7 @@ let always_false_rule (pos : Pos.t) (have_parameter : typ option) : rule =
     rule_label = Unlabeled;
   }
 
-type assertion = expr Bindlib.box
+type assertion = expr boxed
 type variation_typ = Increasing | Decreasing
 type reference_typ = Decree | Law
 
@@ -263,8 +263,8 @@ let free_variables (def : rule RuleMap.t) : Pos.t ScopeDefMap.t =
     (fun _ rule acc ->
       let locs =
         LocationSet.union
-          (locations_used (Bindlib.unbox rule.rule_just))
-          (locations_used (Bindlib.unbox rule.rule_cons))
+          (locations_used (Expr.unbox rule.rule_just))
+          (locations_used (Expr.unbox rule.rule_cons))
       in
       add_locs acc locs)
     def ScopeDefMap.empty
diff --git a/compiler/desugared/ast.mli b/compiler/desugared/ast.mli
index 77558ecc..713cff92 100644
--- a/compiler/desugared/ast.mli
+++ b/compiler/desugared/ast.mli
@@ -68,8 +68,8 @@ type label_situation = ExplicitlyLabeled of LabelName.t Marked.pos | Unlabeled
 
 type rule = {
   rule_id : RuleName.t;
-  rule_just : expr Bindlib.box;
-  rule_cons : expr Bindlib.box;
+  rule_just : expr boxed;
+  rule_cons : expr boxed;
   rule_parameter : (expr Var.t * typ) option;
   rule_exception : exception_situation;
   rule_label : label_situation;
@@ -80,7 +80,7 @@ module Rule : Set.OrderedType with type t = rule
 val empty_rule : Pos.t -> typ option -> rule
 val always_false_rule : Pos.t -> typ option -> rule
 
-type assertion = expr Bindlib.box
+type assertion = expr boxed
 type variation_typ = Increasing | Decreasing
 type reference_typ = Decree | Law
 
diff --git a/compiler/desugared/desugared_to_scope.ml b/compiler/desugared/desugared_to_scope.ml
index 655a878a..a2d65649 100644
--- a/compiler/desugared/desugared_to_scope.ml
+++ b/compiler/desugared/desugared_to_scope.ml
@@ -31,14 +31,16 @@ type ctx = {
 }
 
 let tag_with_log_entry
-    (e : untyped Scopelang.Ast.expr)
+    (e : untyped Scopelang.Ast.expr boxed)
     (l : log_entry)
-    (markings : Utils.Uid.MarkedString.info list) : untyped Scopelang.Ast.expr =
-  ( EApp ((EOp (Unop (Log (l, markings))), Marked.get_mark e), [e]),
-    Marked.get_mark e )
+    (markings : Utils.Uid.MarkedString.info list) :
+    untyped Scopelang.Ast.expr boxed =
+  Expr.eapp
+    (Expr.eop (Unop (Log (l, markings))) (Marked.get_mark e))
+    [e] (Marked.get_mark e)
 
 let rec translate_expr (ctx : ctx) (e : Ast.expr) :
-    untyped Scopelang.Ast.expr Bindlib.box =
+    untyped Scopelang.Ast.expr boxed =
   let m = Marked.get_mark e in
   match Marked.unmark e with
   | ELocation (SubScopeVar (s_name, ss_name, s_var)) ->
@@ -50,55 +52,40 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr) :
       | States states ->
         Marked.same_mark_as (snd (List.hd (List.rev states))) s_var
     in
-    Bindlib.box (ELocation (SubScopeVar (s_name, ss_name, new_s_var)), m)
+    Expr.elocation (SubScopeVar (s_name, ss_name, new_s_var)) m
   | ELocation (DesugaredScopeVar (s_var, None)) ->
-    Bindlib.box
-      ( ELocation
-          (ScopelangScopeVar
-             (match
-                ScopeVarMap.find (Marked.unmark s_var) ctx.scope_var_mapping
-              with
-             | WholeVar new_s_var -> Marked.same_mark_as new_s_var s_var
-             | States _ -> failwith "should not happen")),
-        m )
+    Expr.elocation
+      (ScopelangScopeVar
+         (match
+            ScopeVarMap.find (Marked.unmark s_var) ctx.scope_var_mapping
+          with
+         | WholeVar new_s_var -> Marked.same_mark_as new_s_var s_var
+         | States _ -> failwith "should not happen"))
+      m
   | ELocation (DesugaredScopeVar (s_var, Some state)) ->
-    Bindlib.box
-      ( ELocation
-          (ScopelangScopeVar
-             (match
-                ScopeVarMap.find (Marked.unmark s_var) ctx.scope_var_mapping
-              with
-             | WholeVar _ -> failwith "should not happen"
-             | States states ->
-               Marked.same_mark_as (List.assoc state states) s_var)),
-        m )
-  | EVar v ->
-    Bindlib.box_apply
-      (fun v -> Marked.same_mark_as v e)
-      (Bindlib.box_var (Var.Map.find v ctx.var_mapping))
+    Expr.elocation
+      (ScopelangScopeVar
+         (match
+            ScopeVarMap.find (Marked.unmark s_var) ctx.scope_var_mapping
+          with
+         | WholeVar _ -> failwith "should not happen"
+         | States states -> Marked.same_mark_as (List.assoc state states) s_var))
+      m
+  | EVar v -> Expr.evar (Var.Map.find v ctx.var_mapping) m
   | EStruct (s_name, fields) ->
-    Bindlib.box_apply
-      (fun new_fields -> EStruct (s_name, new_fields), m)
-      (Scopelang.Ast.StructFieldMapLift.lift_box
-         (StructFieldMap.map (translate_expr ctx) fields))
+    Expr.estruct s_name (StructFieldMap.map (translate_expr ctx) fields) m
   | EStructAccess (e1, s_name, f_name) ->
-    Bindlib.box_apply
-      (fun new_e1 -> EStructAccess (new_e1, s_name, f_name), m)
-      (translate_expr ctx e1)
+    Expr.estructaccess (translate_expr ctx e1) s_name f_name m
   | EEnumInj (e1, cons, e_name) ->
-    Bindlib.box_apply
-      (fun new_e1 -> EEnumInj (new_e1, cons, e_name), m)
-      (translate_expr ctx e1)
+    Expr.eenuminj (translate_expr ctx e1) cons e_name m
   | EMatchS (e1, e_name, arms) ->
-    Bindlib.box_apply2
-      (fun new_e1 new_arms -> EMatchS (new_e1, e_name, new_arms), m)
-      (translate_expr ctx e1)
-      (Scopelang.Ast.EnumConstructorMapLift.lift_box
-         (EnumConstructorMap.map (translate_expr ctx) arms))
+    Expr.ematchs (translate_expr ctx e1) e_name
+      (EnumConstructorMap.map (translate_expr ctx) arms)
+      m
   | ELit
       (( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
        | LDuration _ ) as l) ->
-    Bindlib.box (ELit l, m)
+    Expr.elit l m
   | EAbs (binder, typs) ->
     let vars, body = Bindlib.unmbind binder in
     let new_vars = Array.map (fun var -> Var.make (Bindlib.name_of var)) vars in
@@ -108,33 +95,19 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr) :
           { ctx with var_mapping = Var.Map.add var new_var ctx.var_mapping })
         ctx (Array.to_list vars) (Array.to_list new_vars)
     in
-    Bindlib.box_apply
-      (fun new_binder -> EAbs (new_binder, typs), m)
-      (Bindlib.bind_mvar new_vars (translate_expr ctx body))
+    Expr.eabs (Expr.bind new_vars (translate_expr ctx body)) typs m
   | EApp (e1, args) ->
-    Bindlib.box_apply2
-      (fun new_e1 new_args -> EApp (new_e1, new_args), m)
-      (translate_expr ctx e1)
-      (Bindlib.box_list (List.map (translate_expr ctx) args))
-  | EOp op -> Bindlib.box (EOp op, m)
+    Expr.eapp (translate_expr ctx e1) (List.map (translate_expr ctx) args) m
+  | EOp op -> Expr.eop op m
   | EDefault (excepts, just, cons) ->
-    Bindlib.box_apply3
-      (fun new_excepts new_just new_cons ->
-        Expr.make_default new_excepts new_just new_cons m)
-      (Bindlib.box_list (List.map (translate_expr ctx) excepts))
-      (translate_expr ctx just) (translate_expr ctx cons)
+    Expr.edefault
+      (List.map (translate_expr ctx) excepts)
+      (translate_expr ctx just) (translate_expr ctx cons) m
   | EIfThenElse (e1, e2, e3) ->
-    Bindlib.box_apply3
-      (fun new_e1 new_e2 new_e3 -> EIfThenElse (new_e1, new_e2, new_e3), m)
-      (translate_expr ctx e1) (translate_expr ctx e2) (translate_expr ctx e3)
-  | EArray args ->
-    Bindlib.box_apply
-      (fun new_args -> EArray new_args, m)
-      (Bindlib.box_list (List.map (translate_expr ctx) args))
-  | ErrorOnEmpty e1 ->
-    Bindlib.box_apply
-      (fun new_e1 -> ErrorOnEmpty new_e1, m)
-      (translate_expr ctx e1)
+    Expr.eifthenelse (translate_expr ctx e1) (translate_expr ctx e2)
+      (translate_expr ctx e3) m
+  | EArray args -> Expr.earray (List.map (translate_expr ctx) args) m
+  | ErrorOnEmpty e1 -> Expr.eerroronempty (translate_expr ctx e1) m
 
 (** {1 Rule tree construction} *)
 
@@ -186,7 +159,7 @@ let rec rule_tree_to_expr
     (ctx : ctx)
     (def_pos : Pos.t)
     (is_func : Ast.expr Var.t option)
-    (tree : rule_tree) : untyped Scopelang.Ast.expr Bindlib.box =
+    (tree : rule_tree) : untyped Scopelang.Ast.expr boxed =
   let emark = Untyped { pos = def_pos } in
   let exceptions, base_rules =
     match tree with Leaf r -> [], r | Node (exceptions, r) -> exceptions, r
@@ -194,15 +167,16 @@ let rec rule_tree_to_expr
   (* because each rule has its own variable parameter and we want to convert the
      whole rule tree into a function, we need to perform some alpha-renaming of
      all the expressions *)
-  let substitute_parameter (e : Ast.expr Bindlib.box) (rule : Ast.rule) :
-      Ast.expr Bindlib.box =
+  let substitute_parameter (e : Ast.expr boxed) (rule : Ast.rule) :
+      Ast.expr boxed =
     match is_func, rule.Ast.rule_parameter with
     | Some new_param, Some (old_param, _) ->
-      let binder = Bindlib.bind_var old_param e in
-      Bindlib.box_apply2
-        (fun binder new_param -> Bindlib.subst binder new_param)
-        binder
-        (Bindlib.box_var new_param)
+      let binder = Bindlib.bind_var old_param (Marked.unmark e) in
+      Marked.mark (Marked.get_mark e)
+      @@ Bindlib.box_apply2
+           (fun binder new_param -> Bindlib.subst binder new_param)
+           binder
+           (Bindlib.box_var new_param)
     | None, None -> e
     | _ -> assert false
     (* should not happen *)
@@ -235,45 +209,38 @@ let rec rule_tree_to_expr
       (fun rule -> substitute_parameter rule.Ast.rule_cons rule)
       base_rules
   in
-  let translate_and_unbox_list (list : Ast.expr Bindlib.box list) :
-      untyped Scopelang.Ast.expr Bindlib.box list =
+  let translate_and_unbox_list (list : Ast.expr boxed list) :
+      untyped Scopelang.Ast.expr boxed list =
     List.map
       (fun e ->
         (* There are two levels of boxing here, the outermost is introduced by
            the [translate_expr] function for which all of the bindings should
            have been closed by now, so we can safely unbox. *)
-        Bindlib.unbox (Bindlib.box_apply (translate_expr ctx) e))
+        translate_expr ctx (Expr.unbox e))
       list
   in
   let default_containing_base_cases =
-    Bindlib.box_apply2
-      (fun base_just_list base_cons_list ->
-        Expr.make_default
-          (List.map2
-             (fun base_just base_cons ->
-               Expr.make_default []
-                 (* Here we insert the logging command that records when a
-                    decision is taken for the value of a variable. *)
-                 (tag_with_log_entry base_just PosRecordIfTrueBool [])
-                 base_cons emark)
-             base_just_list base_cons_list)
-          (ELit (LBool false), emark)
-          (ELit LEmptyError, emark) emark)
-      (Bindlib.box_list (translate_and_unbox_list base_just_list))
-      (Bindlib.box_list (translate_and_unbox_list base_cons_list))
+    Expr.make_default
+      (List.map2
+         (fun base_just base_cons ->
+           Expr.make_default []
+             (* Here we insert the logging command that records when a decision
+                is taken for the value of a variable. *)
+             (tag_with_log_entry base_just PosRecordIfTrueBool [])
+             base_cons emark)
+         (translate_and_unbox_list base_just_list)
+         (translate_and_unbox_list base_cons_list))
+      (Expr.elit (LBool false) emark)
+      (Expr.elit LEmptyError emark)
+      emark
   in
   let exceptions =
-    Bindlib.box_list
-      (List.map
-         (rule_tree_to_expr ~toplevel:false ctx def_pos is_func)
-         exceptions)
+    List.map (rule_tree_to_expr ~toplevel:false ctx def_pos is_func) exceptions
   in
   let default =
-    Bindlib.box_apply2
-      (fun exceptions default_containing_base_cases ->
-        Expr.make_default exceptions (ELit (LBool true), emark)
-          default_containing_base_cases emark)
-      exceptions default_containing_base_cases
+    Expr.make_default exceptions
+      (Expr.elit (LBool true) emark)
+      default_containing_base_cases emark
   in
   match is_func, (List.hd base_rules).Ast.rule_parameter with
   | None, None -> default
@@ -281,12 +248,7 @@ let rec rule_tree_to_expr
     if toplevel then
       (* When we're creating a function from multiple defaults, we must check
          that the result returned by the function is not empty *)
-      let default =
-        Bindlib.box_apply
-          (fun (default : untyped Scopelang.Ast.expr) ->
-            ErrorOnEmpty default, emark)
-          default
-      in
+      let default = Expr.eerroronempty default emark in
       Expr.make_abs
         [| Var.Map.find new_param ctx.var_mapping |]
         default [typ] def_pos
@@ -304,7 +266,7 @@ let translate_def
     (typ : typ)
     (io : Scopelang.Ast.io)
     ~(is_cond : bool)
-    ~(is_subscope_var : bool) : untyped Scopelang.Ast.expr =
+    ~(is_subscope_var : bool) : untyped Scopelang.Ast.expr boxed =
   (* Here, we have to transform this list of rules into a default tree. *)
   let is_def_func =
     match Marked.unmark typ with TArrow (_, _) -> true | _ -> false
@@ -330,13 +292,12 @@ let translate_def
       let spans =
         List.map
           (fun (_, r) ->
-            ( Some "This definition is a function:",
-              Expr.pos (Bindlib.unbox r.Ast.rule_cons) ))
+            Some "This definition is a function:", Expr.pos r.Ast.rule_cons)
           (Ast.RuleMap.bindings (Ast.RuleMap.filter is_rule_func def))
         @ List.map
             (fun (_, r) ->
               ( Some "This definition is not a function:",
-                Expr.pos (Bindlib.unbox r.Ast.rule_cons) ))
+                Expr.pos r.Ast.rule_cons ))
             (Ast.RuleMap.bindings
                (Ast.RuleMap.filter (fun n r -> not (is_rule_func n r)) def))
       in
@@ -386,30 +347,30 @@ let translate_def
        defined as an OnlyInput to a subscope, since the [false] default value
        will not be provided by the calee scope, it has to be placed in the
        caller. *)
-  then ELit LEmptyError, Untyped { pos = Ast.ScopeDef.get_position def_info }
+  then
+    Expr.elit LEmptyError (Untyped { pos = Ast.ScopeDef.get_position def_info })
   else
-    Bindlib.unbox
-      (rule_tree_to_expr ~toplevel:true ctx
-         (Ast.ScopeDef.get_position def_info)
-         (Option.map (fun _ -> Var.make "param") is_def_func_param_typ)
-         (match top_list, top_value with
-         | [], None ->
-           (* In this case, there are no rules to define the expression and no
-              default value so we put an empty rule. *)
-           Leaf [Ast.empty_rule (Marked.get_mark typ) is_def_func_param_typ]
-         | [], Some top_value ->
-           (* In this case, there are no rules to define the expression but a
-              default value so we put it. *)
-           Leaf [top_value]
-         | _, Some top_value ->
-           (* When there are rules + a default value, we put the rules as
-              exceptions to the default value *)
-           Node (top_list, [top_value])
-         | [top_tree], None -> top_tree
-         | _, None ->
-           Node
-             ( top_list,
-               [Ast.empty_rule (Marked.get_mark typ) is_def_func_param_typ] )))
+    rule_tree_to_expr ~toplevel:true ctx
+      (Ast.ScopeDef.get_position def_info)
+      (Option.map (fun _ -> Var.make "param") is_def_func_param_typ)
+      (match top_list, top_value with
+      | [], None ->
+        (* In this case, there are no rules to define the expression and no
+           default value so we put an empty rule. *)
+        Leaf [Ast.empty_rule (Marked.get_mark typ) is_def_func_param_typ]
+      | [], Some top_value ->
+        (* In this case, there are no rules to define the expression but a
+           default value so we put it. *)
+        Leaf [top_value]
+      | _, Some top_value ->
+        (* When there are rules + a default value, we put the rules as
+           exceptions to the default value *)
+        Node (top_list, [top_value])
+      | [top_tree], None -> top_tree
+      | _, None ->
+        Node
+          ( top_list,
+            [Ast.empty_rule (Marked.get_mark typ) is_def_func_param_typ] ))
 
 (** Translates a scope *)
 let translate_scope (ctx : ctx) (scope : Ast.scope) :
@@ -471,7 +432,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) :
                        Marked.get_mark (ScopeVar.get_info scope_var) ),
                      var_typ,
                      scope_def.Ast.scope_def_io,
-                     expr_def );
+                     Expr.unbox expr_def );
                ])
            | Dependency.Vertex.SubScope sub_scope_index ->
              (* Before calling the sub_scope, we need to include all the
@@ -568,7 +529,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) :
                            var_pos ),
                          def_typ,
                          scope_def.Ast.scope_def_io,
-                         expr_def ))
+                         Expr.unbox expr_def ))
                  sub_scope_vars_redefs_candidates
              in
              let sub_scope_vars_redefs =
@@ -595,12 +556,9 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) :
     scope_decl_rules
     @ List.map
         (fun e ->
-          let scope_e = translate_expr ctx e in
-          Bindlib.unbox
-            (Bindlib.box_apply
-               (fun scope_e -> Scopelang.Ast.Assertion scope_e)
-               scope_e))
-        (Bindlib.unbox (Bindlib.box_list scope.Ast.scope_assertions))
+          let scope_e = translate_expr ctx (Expr.unbox e) in
+          Scopelang.Ast.Assertion (Expr.unbox scope_e))
+        scope.Ast.scope_assertions
   in
   let scope_sig =
     ScopeVarMap.fold
diff --git a/compiler/driver.ml b/compiler/driver.ml
index 43f119b1..f01f9e49 100644
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@@ -217,7 +217,7 @@ let driver source_file (options : Cli.options) : int =
                      prgm.scopes) )
           else
             let prgrm_dcalc_expr =
-              Bindlib.unbox (Shared_ast.Program.to_expr prgm scope_uid)
+              Shared_ast.Expr.unbox (Shared_ast.Program.to_expr prgm scope_uid)
             in
             Format.fprintf fmt "%a\n"
               (Shared_ast.Expr.format prgm.decl_ctx)
@@ -250,7 +250,7 @@ let driver source_file (options : Cli.options) : int =
           | `Interpret ->
             Cli.debug_print "Starting interpretation...";
             let prgrm_dcalc_expr =
-              Bindlib.unbox (Shared_ast.Program.to_expr prgm scope_uid)
+              Shared_ast.Expr.unbox (Shared_ast.Program.to_expr prgm scope_uid)
             in
             let results =
               Dcalc.Interpreter.interpret_program prgm.decl_ctx prgrm_dcalc_expr
@@ -322,7 +322,8 @@ let driver source_file (options : Cli.options) : int =
                          prgm.scopes) )
               else
                 let prgrm_lcalc_expr =
-                  Bindlib.unbox (Shared_ast.Program.to_expr prgm scope_uid)
+                  Shared_ast.Expr.unbox
+                    (Shared_ast.Program.to_expr prgm scope_uid)
                 in
                 Format.fprintf fmt "%a\n"
                   (Shared_ast.Expr.format prgm.decl_ctx)
diff --git a/compiler/lcalc/ast.ml b/compiler/lcalc/ast.ml
index cfd7ba57..feb12929 100644
--- a/compiler/lcalc/ast.ml
+++ b/compiler/lcalc/ast.ml
@@ -34,39 +34,25 @@ let option_enum_config : (EnumConstructor.t * typ) list =
 (* FIXME: proper typing in all the constructors below *)
 
 let make_none m =
-  let mark = Marked.mark m in
   let tunit = TLit TUnit, Expr.mark_pos m in
-  Bindlib.box
-  @@ mark
-  @@ EInj
-       ( Marked.mark (Expr.with_ty m tunit) (ELit LUnit),
-         0,
-         option_enum,
-         [TLit TUnit, Pos.no_pos; TAny, Pos.no_pos] )
+  Expr.einj
+    (Expr.elit LUnit (Expr.with_ty m tunit))
+    0 option_enum
+    [TLit TUnit, Pos.no_pos; TAny, Pos.no_pos]
+    m
 
 let make_some e =
-  let m = Marked.get_mark @@ Bindlib.unbox e in
-  let mark = Marked.mark m in
-  Bindlib.box_apply
-    (fun e ->
-      mark
-      @@ EInj
-           ( e,
-             1,
-             option_enum,
-             [TLit TUnit, Expr.mark_pos m; TAny, Expr.mark_pos m] ))
-    e
+  let m = Marked.get_mark e in
+  Expr.einj e 1 option_enum
+    [TLit TUnit, Expr.mark_pos m; TAny, Expr.mark_pos m]
+    m
 
 (** [make_matchopt_with_abs_arms arg e_none e_some] build an expression
     [match arg with |None -> e_none | Some -> e_some] and requires e_some and
     e_none to be in the form [EAbs ...].*)
 let make_matchopt_with_abs_arms arg e_none e_some =
-  let m = Marked.get_mark @@ Bindlib.unbox arg in
-  let mark = Marked.mark m in
-  Bindlib.box_apply3
-    (fun arg e_none e_some ->
-      mark @@ EMatch (arg, [e_none; e_some], option_enum))
-    arg e_none e_some
+  let m = Marked.get_mark arg in
+  Expr.ematch arg [e_none; e_some] option_enum m
 
 (** [make_matchopt pos v tau arg e_none e_some] builds an expression
     [match arg with | None () -> e_none | Some v -> e_some]. It binds v to
@@ -74,7 +60,6 @@ let make_matchopt_with_abs_arms arg e_none e_some =
     requirements on the form of both e_some and e_none. *)
 let make_matchopt pos v tau arg e_none e_some =
   let x = Var.make "_" in
-
   make_matchopt_with_abs_arms arg
     (Expr.make_abs [| x |] e_none [TLit TUnit, pos] pos)
     (Expr.make_abs [| v |] e_some [tau] pos)
diff --git a/compiler/lcalc/ast.mli b/compiler/lcalc/ast.mli
index dd4ac4c4..08e2ad60 100644
--- a/compiler/lcalc/ast.mli
+++ b/compiler/lcalc/ast.mli
@@ -33,23 +33,20 @@ val option_enum : EnumName.t
 val none_constr : EnumConstructor.t
 val some_constr : EnumConstructor.t
 val option_enum_config : (EnumConstructor.t * typ) list
-val make_none : 'm mark -> 'm expr Bindlib.box
-val make_some : 'm expr Bindlib.box -> 'm expr Bindlib.box
+val make_none : 'm mark -> 'm expr boxed
+val make_some : 'm expr boxed -> 'm expr boxed
 
 val make_matchopt_with_abs_arms :
-  'm expr Bindlib.box ->
-  'm expr Bindlib.box ->
-  'm expr Bindlib.box ->
-  'm expr Bindlib.box
+  'm expr boxed -> 'm expr boxed -> 'm expr boxed -> 'm expr boxed
 
 val make_matchopt :
   Utils.Pos.t ->
   'm expr Var.t ->
   typ ->
-  'm expr Bindlib.box ->
-  'm expr Bindlib.box ->
-  'm expr Bindlib.box ->
-  'm expr Bindlib.box
+  'm expr boxed ->
+  'm expr boxed ->
+  'm expr boxed ->
+  'm expr boxed
 (** [e' = make_matchopt'' pos v e e_none e_some] Builds the term corresponding
     to [match e with | None -> fun () -> e_none |Some -> fun v -> e_some]. *)
 
diff --git a/compiler/lcalc/closure_conversion.ml b/compiler/lcalc/closure_conversion.ml
index e1a9aacf..a17979f6 100644
--- a/compiler/lcalc/closure_conversion.ml
+++ b/compiler/lcalc/closure_conversion.ml
@@ -27,14 +27,12 @@ type 'm ctx = { name_context : string; globally_bound_vars : 'm expr Var.Set.t }
 (** Returns the expression with closed closures and the set of free variables
     inside this new expression. Implementation guided by
     http://gallium.inria.fr/~fpottier/mpri/cours04.pdf#page=9. *)
-let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
-    m expr Bindlib.box =
+let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) : m expr boxed =
   let rec aux e =
+    let m = Marked.get_mark e in
     match Marked.unmark e with
     | EVar v ->
-      ( Bindlib.box_apply
-          (fun new_v -> new_v, Marked.get_mark e)
-          (Bindlib.box_var v),
+      ( (Bindlib.box_var v, m),
         if Var.Set.mem v ctx.globally_bound_vars then Var.Set.empty
         else Var.Set.singleton v )
     | ETuple (args, s) ->
@@ -45,22 +43,13 @@ let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
             new_arg :: new_args, Var.Set.union new_free_vars free_vars)
           ([], Var.Set.empty) args
       in
-      ( Bindlib.box_apply
-          (fun new_args -> ETuple (List.rev new_args, s), Marked.get_mark e)
-          (Bindlib.box_list new_args),
-        free_vars )
+      Expr.etuple (List.rev new_args) s m, free_vars
     | ETupleAccess (e1, n, s, typs) ->
       let new_e1, free_vars = aux e1 in
-      ( Bindlib.box_apply
-          (fun new_e1 -> ETupleAccess (new_e1, n, s, typs), Marked.get_mark e)
-          new_e1,
-        free_vars )
+      Expr.etupleaccess new_e1 n s typs m, free_vars
     | EInj (e1, n, e_name, typs) ->
       let new_e1, free_vars = aux e1 in
-      ( Bindlib.box_apply
-          (fun new_e1 -> EInj (new_e1, n, e_name, typs), Marked.get_mark e)
-          new_e1,
-        free_vars )
+      Expr.einj new_e1 n e_name typs m, free_vars
     | EMatch (e1, arms, e_name) ->
       let new_e1, free_vars = aux e1 in
       (* We do not close the clotures inside the arms of the match expression,
@@ -72,22 +61,13 @@ let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
             | EAbs (binder, typs) ->
               let vars, body = Bindlib.unmbind binder in
               let new_body, new_free_vars = aux body in
-              let new_binder = Bindlib.bind_mvar vars new_body in
-              ( Bindlib.box_apply
-                  (fun new_binder ->
-                    EAbs (new_binder, typs), Marked.get_mark arm)
-                  new_binder
-                :: new_arms,
+              let new_binder = Expr.bind vars new_body in
+              ( Expr.eabs new_binder typs (Marked.get_mark arm) :: new_arms,
                 Var.Set.union free_vars new_free_vars )
             | _ -> failwith "should not happen")
           arms ([], free_vars)
       in
-      ( Bindlib.box_apply2
-          (fun new_e1 new_arms ->
-            EMatch (new_e1, new_arms, e_name), Marked.get_mark e)
-          new_e1
-          (Bindlib.box_list new_arms),
-        free_vars )
+      Expr.ematch new_e1 new_arms e_name m, free_vars
     | EArray args ->
       let new_args, free_vars =
         List.fold_right
@@ -96,16 +76,13 @@ let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
             new_arg :: new_args, Var.Set.union free_vars new_free_vars)
           args ([], Var.Set.empty)
       in
-      ( Bindlib.box_apply
-          (fun new_args -> EArray new_args, Marked.get_mark e)
-          (Bindlib.box_list new_args),
-        free_vars )
-    | ELit l -> Bindlib.box (ELit l, Marked.get_mark e), Var.Set.empty
+      Expr.earray new_args m, free_vars
+    | ELit l -> Expr.elit l m, Var.Set.empty
     | EApp ((EAbs (binder, typs_abs), e1_pos), args) ->
       (* let-binding, we should not close these *)
       let vars, body = Bindlib.unmbind binder in
       let new_body, free_vars = aux body in
-      let new_binder = Bindlib.bind_mvar vars new_body in
+      let new_binder = Expr.bind vars new_body in
       let new_args, free_vars =
         List.fold_right
           (fun arg (new_args, free_vars) ->
@@ -113,16 +90,10 @@ let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
             new_arg :: new_args, Var.Set.union free_vars new_free_vars)
           args ([], free_vars)
       in
-      ( Bindlib.box_apply2
-          (fun new_binder new_args ->
-            ( EApp ((EAbs (new_binder, typs_abs), e1_pos), new_args),
-              Marked.get_mark e ))
-          new_binder
-          (Bindlib.box_list new_args),
-        free_vars )
+      Expr.eapp (Expr.eabs new_binder typs_abs e1_pos) new_args m, free_vars
     | EAbs (binder, typs) ->
       (* λ x.t *)
-      let binder_mark = Marked.get_mark e in
+      let binder_mark = m in
       let binder_pos = Expr.mark_pos binder_mark in
       (* Converting the closure. *)
       let vars, body = Bindlib.unmbind binder in
@@ -144,15 +115,11 @@ let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
           (List.map (fun _ -> any_ty) extra_vars_list)
           (List.mapi
              (fun i _ ->
-               Bindlib.box_apply
-                 (fun inner_c_var ->
-                   ( ETupleAccess
-                       ( (inner_c_var, binder_mark),
-                         i + 1,
-                         None,
-                         List.map (fun _ -> any_ty) extra_vars_list ),
-                     binder_mark ))
-                 (Bindlib.box_var inner_c_var))
+               Expr.etupleaccess
+                 (Expr.evar inner_c_var binder_mark)
+                 (i + 1) None
+                 (List.map (fun _ -> any_ty) extra_vars_list)
+                 binder_mark)
              extra_vars_list)
           new_body
           (Expr.mark_pos binder_mark)
@@ -167,20 +134,12 @@ let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
       ( Expr.make_let_in code_var
           (TAny, Expr.pos e)
           new_closure
-          (Bindlib.box_apply2
-             (fun code_var extra_vars ->
-               ( ETuple
-                   ( (code_var, binder_mark)
-                     :: List.map
-                          (fun extra_var -> extra_var, binder_mark)
-                          extra_vars,
-                     None ),
-                 Marked.get_mark e ))
-             (Bindlib.box_var code_var)
-             (Bindlib.box_list
-                (List.map
-                   (fun extra_var -> Bindlib.box_var extra_var)
-                   extra_vars_list)))
+          (Expr.etuple
+             ((Bindlib.box_var code_var, binder_mark)
+             :: List.map
+                  (fun extra_var -> Bindlib.box_var extra_var, binder_mark)
+                  extra_vars_list)
+             None m)
           (Expr.pos e),
         extra_vars )
     | EApp ((EOp op, pos_op), args) ->
@@ -193,10 +152,7 @@ let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
             new_arg :: new_args, Var.Set.union free_vars new_free_vars)
           args ([], Var.Set.empty)
       in
-      ( Bindlib.box_apply
-          (fun new_e2 -> EApp ((EOp op, pos_op), new_e2), Marked.get_mark e)
-          (Bindlib.box_list new_args),
-        free_vars )
+      Expr.eapp (Expr.eop op pos_op) new_args m, free_vars
     | EApp ((EVar v, v_pos), args) when Var.Set.mem v ctx.globally_bound_vars ->
       (* This corresponds to a scope call, which we don't want to transform*)
       let new_args, free_vars =
@@ -206,11 +162,7 @@ let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
             new_arg :: new_args, Var.Set.union free_vars new_free_vars)
           args ([], Var.Set.empty)
       in
-      ( Bindlib.box_apply2
-          (fun new_v new_e2 -> EApp ((new_v, v_pos), new_e2), Marked.get_mark e)
-          (Bindlib.box_var v)
-          (Bindlib.box_list new_args),
-        free_vars )
+      Expr.eapp (Bindlib.box_var v, v_pos) new_args m, free_vars
     | EApp (e1, args) ->
       let new_e1, free_vars = aux e1 in
       let env_var = Var.make "env" in
@@ -223,52 +175,36 @@ let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
           args ([], free_vars)
       in
       let call_expr =
+        let m1 = Marked.get_mark e1 in
         Expr.make_let_in code_var
           (TAny, Expr.pos e)
-          (Bindlib.box_apply
-             (fun env_var ->
-               ( ETupleAccess
-                   ((env_var, Marked.get_mark e1), 0, None, [ (*TODO: fill?*) ]),
-                 Marked.get_mark e ))
-             (Bindlib.box_var env_var))
-          (Bindlib.box_apply3
-             (fun code_var env_var new_args ->
-               ( EApp
-                   ( (code_var, Marked.get_mark e1),
-                     (env_var, Marked.get_mark e1) :: new_args ),
-                 Marked.get_mark e ))
-             (Bindlib.box_var code_var) (Bindlib.box_var env_var)
-             (Bindlib.box_list new_args))
+          (Expr.etupleaccess
+             (Bindlib.box_var env_var, m1)
+             0 None [ (*TODO: fill?*) ]
+             m)
+          (Expr.eapp
+             (Bindlib.box_var code_var, m1)
+             ((Bindlib.box_var env_var, m1) :: new_args)
+             m)
           (Expr.pos e)
       in
       ( Expr.make_let_in env_var (TAny, Expr.pos e) new_e1 call_expr (Expr.pos e),
         free_vars )
     | EAssert e1 ->
       let new_e1, free_vars = aux e1 in
-      ( Bindlib.box_apply
-          (fun new_e1 -> EAssert new_e1, Marked.get_mark e)
-          new_e1,
-        free_vars )
-    | EOp op -> Bindlib.box (EOp op, Marked.get_mark e), Var.Set.empty
+      Expr.eassert new_e1 m, free_vars
+    | EOp op -> Expr.eop op m, Var.Set.empty
     | EIfThenElse (e1, e2, e3) ->
       let new_e1, free_vars1 = aux e1 in
       let new_e2, free_vars2 = aux e2 in
       let new_e3, free_vars3 = aux e3 in
-      ( Bindlib.box_apply3
-          (fun new_e1 new_e2 new_e3 ->
-            EIfThenElse (new_e1, new_e2, new_e3), Marked.get_mark e)
-          new_e1 new_e2 new_e3,
+      ( Expr.eifthenelse new_e1 new_e2 new_e3 m,
         Var.Set.union (Var.Set.union free_vars1 free_vars2) free_vars3 )
-    | ERaise except ->
-      Bindlib.box (ERaise except, Marked.get_mark e), Var.Set.empty
+    | ERaise except -> Expr.eraise except m, Var.Set.empty
     | ECatch (e1, except, e2) ->
       let new_e1, free_vars1 = aux e1 in
       let new_e2, free_vars2 = aux e2 in
-      ( Bindlib.box_apply2
-          (fun new_e1 new_e2 ->
-            ECatch (new_e1, except, new_e2), Marked.get_mark e)
-          new_e1 new_e2,
-        Var.Set.union free_vars1 free_vars2 )
+      Expr.ecatch new_e1 except new_e2 m, Var.Set.union free_vars1 free_vars2
   in
   let e', _vars = aux e in
   e'
diff --git a/compiler/lcalc/compile_with_exceptions.ml b/compiler/lcalc/compile_with_exceptions.ml
index 33ae49ca..27b5b050 100644
--- a/compiler/lcalc/compile_with_exceptions.ml
+++ b/compiler/lcalc/compile_with_exceptions.ml
@@ -23,9 +23,9 @@ type 'm ctx = ('m D.expr, 'm A.expr Var.t) Var.Map.t
 (** This environment contains a mapping between the variables in Dcalc and their
     correspondance in Lcalc. *)
 
-let thunk_expr (type m) (e : m A.expr Bindlib.box) : m A.expr Bindlib.box =
+let thunk_expr (type m) (e : m A.expr boxed) : m A.expr boxed =
   let dummy_var = Var.make "_" in
-  let pos = Expr.pos (Bindlib.unbox e) in
+  let pos = Expr.pos e in
   let arg_t = Marked.mark pos (TLit TUnit) in
   Expr.make_abs [| dummy_var |] e [arg_t] pos
 
@@ -34,7 +34,7 @@ let rec translate_default
     (exceptions : 'm D.expr list)
     (just : 'm D.expr)
     (cons : 'm D.expr)
-    (mark_default : 'm mark) : 'm A.expr Bindlib.box =
+    (mark_default : 'm mark) : 'm A.expr boxed =
   let exceptions =
     List.map (fun except -> thunk_expr (translate_expr ctx except)) exceptions
   in
@@ -42,8 +42,8 @@ let rec translate_default
   let exceptions =
     Expr.make_app
       (Expr.make_var
-         ( Var.translate A.handle_default,
-           Expr.with_ty mark_default (Utils.Marked.mark pos TAny) ))
+         (Var.translate A.handle_default)
+         (Expr.with_ty mark_default (Utils.Marked.mark pos TAny)))
       [
         Expr.earray exceptions mark_default;
         thunk_expr (translate_expr ctx just);
@@ -53,9 +53,9 @@ let rec translate_default
   in
   exceptions
 
-and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr Bindlib.box =
+and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr boxed =
   match Marked.unmark e with
-  | EVar v -> Expr.make_var (Var.Map.find v ctx, Marked.get_mark e)
+  | EVar v -> Expr.make_var (Var.Map.find v ctx) (Marked.get_mark e)
   | ETuple (args, s) ->
     Expr.etuple (List.map (translate_expr ctx) args) s (Marked.get_mark e)
   | ETupleAccess (e1, i, s, ts) ->
@@ -71,8 +71,8 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr Bindlib.box =
   | ELit
       ((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
       l) ->
-    Bindlib.box (Marked.same_mark_as (ELit l) e)
-  | ELit LEmptyError -> Bindlib.box (Marked.same_mark_as (ERaise EmptyError) e)
+    Expr.elit l (Marked.get_mark e)
+  | ELit LEmptyError -> Expr.eraise EmptyError (Marked.get_mark e)
   | EOp op -> Expr.eop op (Marked.get_mark e)
   | EIfThenElse (e1, e2, e3) ->
     Expr.eifthenelse (translate_expr ctx e1) (translate_expr ctx e2)
@@ -80,7 +80,7 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr Bindlib.box =
   | EAssert e1 -> Expr.eassert (translate_expr ctx e1) (Marked.get_mark e)
   | ErrorOnEmpty arg ->
     Expr.ecatch (translate_expr ctx arg) EmptyError
-      (Bindlib.box (Marked.same_mark_as (ERaise NoValueProvided) e))
+      (Expr.eraise NoValueProvided (Marked.get_mark e))
       (Marked.get_mark e)
   | EApp (e1, args) ->
     Expr.eapp (translate_expr ctx e1)
@@ -97,14 +97,12 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr Bindlib.box =
     in
     let lc_vars = Array.of_list lc_vars in
     let new_body = translate_expr ctx body in
-    let new_binder = Bindlib.bind_mvar lc_vars new_body in
-    Bindlib.box_apply
-      (fun new_binder -> Marked.same_mark_as (EAbs (new_binder, ts)) e)
-      new_binder
+    let new_binder = Expr.bind lc_vars new_body in
+    Expr.eabs new_binder ts (Marked.get_mark e)
   | EDefault ([exn], just, cons) when !Cli.optimize_flag ->
     Expr.ecatch (translate_expr ctx exn) EmptyError
       (Expr.eifthenelse (translate_expr ctx just) (translate_expr ctx cons)
-         (Bindlib.box (Marked.same_mark_as (ERaise EmptyError) e))
+         (Expr.eraise EmptyError (Marked.get_mark e))
          (Marked.get_mark e))
       (Marked.get_mark e)
   | EDefault (exceptions, just, cons) ->
@@ -116,7 +114,8 @@ let rec translate_scope_lets
     (scope_lets : 'm D.expr scope_body_expr) :
     'm A.expr scope_body_expr Bindlib.box =
   match scope_lets with
-  | Result e -> Bindlib.box_apply (fun e -> Result e) (translate_expr ctx e)
+  | Result e ->
+    Bindlib.box_apply (fun e -> Result e) (Expr.Box.inj (translate_expr ctx e))
   | ScopeLet scope_let ->
     let old_scope_let_var, scope_let_next =
       Bindlib.unbind scope_let.scope_let_next
@@ -136,7 +135,8 @@ let rec translate_scope_lets
             scope_let_next = new_scope_next;
             scope_let_expr = new_scope_let_expr;
           })
-      new_scope_next new_scope_let_expr
+      new_scope_next
+      (Expr.Box.inj new_scope_let_expr)
 
 let rec translate_scopes
     (decl_ctx : decl_ctx)
diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml
index 1e43a1fe..95982a1b 100644
--- a/compiler/lcalc/compile_without_exceptions.ml
+++ b/compiler/lcalc/compile_without_exceptions.ml
@@ -45,11 +45,7 @@ open Shared_ast
 type 'm hoists = ('m A.expr, 'm D.expr) Var.Map.t
 (** Hoists definition. It represent bindings between [A.Var.t] and [D.expr]. *)
 
-type 'm info = {
-  expr : 'm A.expr Bindlib.box;
-  var : 'm A.expr Var.t;
-  is_pure : bool;
-}
+type 'm info = { expr : 'm A.expr boxed; var : 'm A.expr Var.t; is_pure : bool }
 (** Information about each encontered Dcalc variable is stored inside a context
     : what is the corresponding LCalc variable; an expression corresponding to
     the variable build correctly using Bindlib, and a boolean `is_pure`
@@ -103,7 +99,7 @@ let add_var
     (is_pure : bool)
     (ctx : 'm ctx) : 'm ctx =
   let new_var = Var.make (Bindlib.name_of var) in
-  let expr = Expr.make_var (new_var, mark) in
+  let expr = Expr.make_var new_var mark in
 
   (* Cli.debug_print @@ Format.asprintf "D.%a |-> A.%a" Print.var var Print.var
      new_var; *)
@@ -156,7 +152,7 @@ let disjoint_union_maps (pos : Pos.t) (cs : ('e, 'a) Var.Map.t list) :
     equivalent in an environement where each variable v, where (v, e_v) is in
     hoists, has the non-empty value in e_v. *)
 let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
-    'm A.expr Bindlib.box * 'm hoists =
+    'm A.expr boxed * 'm hoists =
   let mark = Marked.get_mark e in
   let pos = Expr.mark_pos mark in
   match Marked.unmark e with
@@ -172,23 +168,23 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
       let v' = Var.make (Bindlib.name_of v) in
       (* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a,
          created a variable %a to replace it" Print.var v Print.var v'; *)
-      Expr.make_var (v', mark), Var.Map.singleton v' e
+      Expr.make_var v' mark, Var.Map.singleton v' e
     else (find ~info:"should never happen" v ctx).expr, Var.Map.empty
   | EApp ((EVar v, p), [(ELit LUnit, _)]) ->
     if not (find ~info:"search for a variable" v ctx).is_pure then
       let v' = Var.make (Bindlib.name_of v) in
       (* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a,
          created a variable %a to replace it" Print.var v Print.var v'; *)
-      Expr.make_var (v', mark), Var.Map.singleton v' (EVar v, p)
+      Expr.make_var v' mark, Var.Map.singleton v' (EVar v, p)
     else
       Errors.raise_spanned_error (Expr.pos e)
         "Internal error: an pure variable was found in an unpure environment."
   | EDefault (_exceptions, _just, _cons) ->
     let v' = Var.make "default_term" in
-    Expr.make_var (v', mark), Var.Map.singleton v' e
+    Expr.make_var v' mark, Var.Map.singleton v' e
   | ELit LEmptyError ->
     let v' = Var.make "empty_litteral" in
-    Expr.make_var (v', mark), Var.Map.singleton v' e
+    Expr.make_var v' mark, Var.Map.singleton v' e
   (* This one is a very special case. It transform an unpure expression
      environement to a pure expression. *)
   | ErrorOnEmpty arg ->
@@ -201,9 +197,9 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
 
     ( A.make_matchopt_with_abs_arms arg'
         (Expr.make_abs [| silent_var |]
-           (Bindlib.box (ERaise NoValueProvided, Expr.with_ty mark rty))
+           (Expr.eraise NoValueProvided (Expr.with_ty mark rty))
            [rty] pos)
-        (Expr.make_abs [| x |] (Expr.make_var (x, mark)) [rty] pos),
+        (Expr.make_abs [| x |] (Expr.make_var x mark) [rty] pos),
       Var.Map.empty )
   (* pure terms *)
   | ELit
@@ -244,12 +240,9 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
     (* here we take the guess that if we cannot build the closure because one of
        the variable is empty, then we cannot build the function. *)
     let new_body, hoists = translate_and_hoist ctx body in
-    let new_binder = Bindlib.bind_mvar lc_vars new_body in
+    let new_binder = Expr.bind lc_vars new_body in
 
-    ( Bindlib.box_apply
-        (fun new_binder -> EAbs (new_binder, List.map translate_typ ts), mark)
-        new_binder,
-      hoists )
+    Expr.eabs new_binder (List.map translate_typ ts) mark, hoists
   | EApp (e1, args) ->
     let e1', h1 = translate_and_hoist ctx e1 in
     let args', h_args =
@@ -287,10 +280,10 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
     let es', hoists = es |> List.map (translate_and_hoist ctx) |> List.split in
 
     Expr.earray es' mark, disjoint_union_maps (Expr.pos e) hoists
-  | EOp op -> Bindlib.box (EOp op, mark), Var.Map.empty
+  | EOp op -> Expr.eop op mark, Var.Map.empty
 
 and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
-    'm A.expr Bindlib.box =
+    'm A.expr boxed =
   let e', hoists = translate_and_hoist ctx e in
   let hoists = Var.Map.bindings hoists in
 
@@ -304,7 +297,7 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
     ~f:(fun acc (v, (hoist, mark_hoist)) ->
       (* Cli.debug_print @@ Format.asprintf "hoist using A.%a" Print.var v; *)
       let pos = Expr.mark_pos mark_hoist in
-      let c' : 'm A.expr Bindlib.box =
+      let c' : 'm A.expr boxed =
         match hoist with
         (* Here we have to handle only the cases appearing in hoists, as defined
            the [translate_and_hoist] function. *)
@@ -315,14 +308,8 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
           let cons' = translate_expr ctx cons in
           (* calls handle_option. *)
           Expr.make_app
-            (Expr.make_var (Var.translate A.handle_default_opt, mark_hoist))
-            [
-              Bindlib.box_apply
-                (fun excep' -> EArray excep', mark_hoist)
-                (Bindlib.box_list excep');
-              just';
-              cons';
-            ]
+            (Expr.make_var (Var.translate A.handle_default_opt) mark_hoist)
+            [Expr.earray excep' mark_hoist; just'; cons']
             pos
         | ELit LEmptyError -> A.make_none mark_hoist
         | EAssert arg ->
@@ -335,13 +322,11 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
 
           A.make_matchopt_with_abs_arms arg'
             (Expr.make_abs [| silent_var |]
-               (Bindlib.box (ERaise NoValueProvided, mark_hoist))
+               (Expr.eraise NoValueProvided mark_hoist)
                [TAny, Expr.mark_pos mark_hoist]
                pos)
             (Expr.make_abs [| x |]
-               (Bindlib.box_apply
-                  (fun arg -> EAssert arg, mark_hoist)
-                  (Expr.make_var (x, mark_hoist)))
+               (Expr.eassert (Expr.make_var x mark_hoist) mark_hoist)
                [TAny, Expr.mark_pos mark_hoist]
                pos)
         | _ ->
@@ -364,7 +349,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
   | Result e ->
     Bindlib.box_apply
       (fun e -> Result e)
-      (translate_expr ~append_esome:false ctx e)
+      (Expr.Box.inj (translate_expr ~append_esome:false ctx e))
   | ScopeLet
       {
         scope_let_kind = SubScopeVarDefinition;
@@ -394,7 +379,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
             scope_let_next = new_next;
             scope_let_pos = pos;
           })
-      (translate_expr ctx ~append_esome:false expr)
+      (Expr.Box.inj (translate_expr ctx ~append_esome:false expr))
       (Bindlib.bind_var new_var new_next)
   | ScopeLet
       {
@@ -421,7 +406,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
             scope_let_next = new_next;
             scope_let_pos = pos;
           })
-      (translate_expr ctx ~append_esome:false expr)
+      (Expr.Box.inj (translate_expr ctx ~append_esome:false expr))
       (Bindlib.bind_var new_var (translate_scope_let ctx' next))
   | ScopeLet
       {
@@ -472,7 +457,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
             scope_let_next = new_next;
             scope_let_pos = pos;
           })
-      (translate_expr ctx ~append_esome:false expr)
+      (Expr.Box.inj (translate_expr ctx ~append_esome:false expr))
       (Bindlib.bind_var new_var (translate_scope_let ctx' next))
 
 let translate_scope_body
diff --git a/compiler/lcalc/optimizations.ml b/compiler/lcalc/optimizations.ml
index 4a4bd779..11628f3b 100644
--- a/compiler/lcalc/optimizations.ml
+++ b/compiler/lcalc/optimizations.ml
@@ -18,64 +18,18 @@ open Shared_ast
 open Ast
 module D = Dcalc.Ast
 
-let ( let+ ) x f = Bindlib.box_apply f x
-let ( and+ ) x y = Bindlib.box_pair x y
+let visitor_map (t : 'a -> 'm expr -> 'm expr boxed) (ctx : 'a) (e : 'm expr) :
+    'm expr boxed =
+  Expr.map ctx ~f:t e
 
-let visitor_map
-    (t : 'a -> 'm expr -> 'm expr Bindlib.box)
-    (ctx : 'a)
-    (e : 'm expr) : 'm expr Bindlib.box =
-  (* calls [t ctx] on every direct childs of [e], then rebuild an abstract
-     syntax tree modified. Used in other transformations. *)
-  let default_mark e' = Marked.same_mark_as e' e in
-  match Marked.unmark e with
-  | EVar v ->
-    let+ v = Bindlib.box_var v in
-    default_mark @@ v
-  | ETuple (args, n) ->
-    let+ args = args |> List.map (t ctx) |> Bindlib.box_list in
-    default_mark @@ ETuple (args, n)
-  | ETupleAccess (e1, i, n, ts) ->
-    let+ e1 = t ctx e1 in
-    default_mark @@ ETupleAccess (e1, i, n, ts)
-  | EInj (e1, i, n, ts) ->
-    let+ e1 = t ctx e1 in
-    default_mark @@ EInj (e1, i, n, ts)
-  | EMatch (arg, cases, n) ->
-    let+ arg = t ctx arg
-    and+ cases = cases |> List.map (t ctx) |> Bindlib.box_list in
-    default_mark @@ EMatch (arg, cases, n)
-  | EArray args ->
-    let+ args = args |> List.map (t ctx) |> Bindlib.box_list in
-    default_mark @@ EArray args
-  | EAbs (binder, ts) ->
-    let vars, body = Bindlib.unmbind binder in
-    let body = t ctx body in
-    let+ binder = Bindlib.bind_mvar vars body in
-    default_mark @@ EAbs (binder, ts)
-  | EApp (e1, args) ->
-    let+ e1 = t ctx e1
-    and+ args = args |> List.map (t ctx) |> Bindlib.box_list in
-    default_mark @@ EApp (e1, args)
-  | EAssert e1 ->
-    let+ e1 = t ctx e1 in
-    default_mark @@ EAssert e1
-  | EIfThenElse (e1, e2, e3) ->
-    let+ e1 = t ctx e1 and+ e2 = t ctx e2 and+ e3 = t ctx e3 in
-    default_mark @@ EIfThenElse (e1, e2, e3)
-  | ECatch (e1, exn, e2) ->
-    let+ e1 = t ctx e1 and+ e2 = t ctx e2 in
-    default_mark @@ ECatch (e1, exn, e2)
-  | ERaise _ | ELit _ | EOp _ -> Bindlib.box e
-
-let rec iota_expr (_ : unit) (e : 'm expr) : 'm expr Bindlib.box =
-  let default_mark e' = Marked.mark (Marked.get_mark e) e' in
+let rec iota_expr (_ : unit) (e : 'm expr) : 'm expr boxed =
+  let m = Marked.get_mark e in
   match Marked.unmark e with
   | EMatch ((EInj (e1, i, n', _ts), _), cases, n) when EnumName.compare n n' = 0
     ->
-    let+ e1 = visitor_map iota_expr () e1
-    and+ case = visitor_map iota_expr () (List.nth cases i) in
-    default_mark @@ EApp (case, [e1])
+    let e1 = visitor_map iota_expr () e1 in
+    let case = visitor_map iota_expr () (List.nth cases i) in
+    Expr.eapp case [e1] m
   | EMatch (e', cases, n)
     when cases
          |> List.mapi (fun i (case, _pos) ->
@@ -87,17 +41,17 @@ let rec iota_expr (_ : unit) (e : 'm expr) : 'm expr Bindlib.box =
     visitor_map iota_expr () e'
   | _ -> visitor_map iota_expr () e
 
-let rec beta_expr (_ : unit) (e : 'm expr) : 'm expr Bindlib.box =
-  let default_mark e' = Marked.same_mark_as e' e in
+let rec beta_expr (e : 'm expr) : 'm expr boxed =
+  let m = Marked.get_mark e in
   match Marked.unmark e with
-  | EApp (e1, args) -> (
-    let+ e1 = beta_expr () e1
-    and+ args = List.map (beta_expr ()) args |> Bindlib.box_list in
-    match Marked.unmark e1 with
-    | EAbs (binder, _ts) ->
-      Bindlib.msubst binder (List.map fst args |> Array.of_list)
-    | _ -> default_mark @@ EApp (e1, args))
-  | _ -> visitor_map beta_expr () e
+  | EApp (e1, args) ->
+    Expr.Box.app1n (beta_expr e1) (List.map beta_expr args)
+      (fun e1 args ->
+        match Marked.unmark e1 with
+        | EAbs (binder, _) -> Marked.unmark (Expr.subst binder args)
+        | _ -> EApp (e1, args))
+      m
+  | _ -> visitor_map (fun () -> beta_expr) () e
 
 let iota_optimizations (p : 'm program) : 'm program =
   let new_scopes =
@@ -110,41 +64,40 @@ let iota_optimizations (p : 'm program) : 'm program =
    read, and can produce exponential blowup of the size of the generated
    program. *)
 let _beta_optimizations (p : 'm program) : 'm program =
-  let new_scopes =
-    Scope.map_exprs ~f:(beta_expr ()) ~varf:(fun v -> v) p.scopes
-  in
+  let new_scopes = Scope.map_exprs ~f:beta_expr ~varf:(fun v -> v) p.scopes in
   { p with scopes = Bindlib.unbox new_scopes }
 
-let rec peephole_expr (_ : unit) (e : 'm expr) : 'm expr Bindlib.box =
-  let default_mark e' = Marked.mark (Marked.get_mark e) e' in
-
+let rec peephole_expr (e : 'm expr) : 'm expr boxed =
+  let m = Marked.get_mark e in
   match Marked.unmark e with
-  | EIfThenElse (e1, e2, e3) -> (
-    let+ e1 = peephole_expr () e1
-    and+ e2 = peephole_expr () e2
-    and+ e3 = peephole_expr () e3 in
-    match Marked.unmark e1 with
-    | ELit (LBool true)
-    | EApp ((EOp (Unop (Log _)), _), [(ELit (LBool true), _)]) ->
-      e2
-    | ELit (LBool false)
-    | EApp ((EOp (Unop (Log _)), _), [(ELit (LBool false), _)]) ->
-      e3
-    | _ -> default_mark @@ EIfThenElse (e1, e2, e3))
-  | ECatch (e1, except, e2) -> (
-    let+ e1 = peephole_expr () e1 and+ e2 = peephole_expr () e2 in
-    match Marked.unmark e1, Marked.unmark e2 with
-    | ERaise except', ERaise except'' when except' = except && except = except''
-      ->
-      default_mark @@ ERaise except
-    | ERaise except', _ when except' = except -> e2
-    | _, ERaise except' when except' = except -> e1
-    | _ -> default_mark @@ ECatch (e1, except, e2))
-  | _ -> visitor_map peephole_expr () e
+  | EIfThenElse (e1, e2, e3) ->
+    Expr.Box.app3 (peephole_expr e1) (peephole_expr e2) (peephole_expr e3)
+      (fun e1 e2 e3 ->
+        match Marked.unmark e1 with
+        | ELit (LBool true)
+        | EApp ((EOp (Unop (Log _)), _), [(ELit (LBool true), _)]) ->
+          Marked.unmark e2
+        | ELit (LBool false)
+        | EApp ((EOp (Unop (Log _)), _), [(ELit (LBool false), _)]) ->
+          Marked.unmark e3
+        | _ -> EIfThenElse (e1, e2, e3))
+      m
+  | ECatch (e1, except, e2) ->
+    Expr.Box.app2 (peephole_expr e1) (peephole_expr e2)
+      (fun e1 e2 ->
+        match Marked.unmark e1, Marked.unmark e2 with
+        | ERaise except', ERaise except''
+          when except' = except && except = except'' ->
+          ERaise except
+        | ERaise except', _ when except' = except -> Marked.unmark e2
+        | _, ERaise except' when except' = except -> Marked.unmark e1
+        | _ -> ECatch (e1, except, e2))
+      m
+  | _ -> visitor_map (fun () -> peephole_expr) () e
 
 let peephole_optimizations (p : 'm program) : 'm program =
   let new_scopes =
-    Scope.map_exprs ~f:(peephole_expr ()) ~varf:(fun v -> v) p.scopes
+    Scope.map_exprs ~f:peephole_expr ~varf:(fun v -> v) p.scopes
   in
   { p with scopes = Bindlib.unbox new_scopes }
 
diff --git a/compiler/scopelang/ast.ml b/compiler/scopelang/ast.ml
index 74625c25..f660ba68 100644
--- a/compiler/scopelang/ast.ml
+++ b/compiler/scopelang/ast.ml
@@ -16,8 +16,6 @@
 
 open Utils
 open Shared_ast
-module StructFieldMapLift = Bindlib.Lift (StructFieldMap)
-module EnumConstructorMapLift = Bindlib.Lift (EnumConstructorMap)
 
 type location = scopelang glocation
 
@@ -88,11 +86,11 @@ type 'm program = {
 let type_rule decl_ctx env = function
   | Definition (loc, typ, io, expr) ->
     let expr' = Typing.expr decl_ctx ~env ~typ expr in
-    Definition (loc, typ, io, Bindlib.unbox expr')
+    Definition (loc, typ, io, Expr.unbox expr')
   | Assertion expr ->
     let typ = Marked.mark (Expr.pos expr) (TLit TBool) in
     let expr' = Typing.expr decl_ctx ~env ~typ expr in
-    Assertion (Bindlib.unbox expr')
+    Assertion (Expr.unbox expr')
   | Call (sc_name, ssc_name, m) ->
     let pos = Expr.mark_pos m in
     Call (sc_name, ssc_name, Typed { pos; ty = Marked.mark pos TAny })
diff --git a/compiler/scopelang/ast.mli b/compiler/scopelang/ast.mli
index b2b622e5..2586bedd 100644
--- a/compiler/scopelang/ast.mli
+++ b/compiler/scopelang/ast.mli
@@ -21,16 +21,6 @@ open Shared_ast
 
 (** {1 Identifiers} *)
 
-module StructFieldMapLift : sig
-  val lift_box :
-    'a Bindlib.box StructFieldMap.t -> 'a StructFieldMap.t Bindlib.box
-end
-
-module EnumConstructorMapLift : sig
-  val lift_box :
-    'a Bindlib.box EnumConstructorMap.t -> 'a EnumConstructorMap.t Bindlib.box
-end
-
 type location = scopelang glocation
 
 module LocationSet : Set.S with type elt = location Marked.pos
diff --git a/compiler/scopelang/scope_to_dcalc.ml b/compiler/scopelang/scope_to_dcalc.ml
index 7f880360..649c4f50 100644
--- a/compiler/scopelang/scope_to_dcalc.ml
+++ b/compiler/scopelang/scope_to_dcalc.ml
@@ -73,40 +73,30 @@ let pos_mark_mk (type a m) (e : (a, m mark) gexpr) :
   let pos_mark_as e = pos_mark (Marked.get_mark e) in
   pos_mark, pos_mark_as
 
-let merge_defaults
-    (caller : 'a Dcalc.Ast.expr Bindlib.box)
-    (callee : 'a Dcalc.Ast.expr Bindlib.box) : 'a Dcalc.Ast.expr Bindlib.box =
+let merge_defaults caller callee =
   let caller =
-    let m = Marked.get_mark (Bindlib.unbox caller) in
+    let m = Marked.get_mark caller in
     let pos = Expr.mark_pos m in
     Expr.make_app caller
-      [Bindlib.box (ELit LUnit, Expr.with_ty m (Marked.mark pos (TLit TUnit)))]
+      [Expr.elit LUnit (Expr.with_ty m (Marked.mark pos (TLit TUnit)))]
       pos
   in
   let body =
-    Bindlib.box_apply2
-      (fun caller callee ->
-        let m = Marked.get_mark callee in
-        let ltrue =
-          Marked.mark
-            (Expr.with_ty m (Marked.mark (Expr.mark_pos m) (TLit TBool)))
-            (ELit (LBool true))
-        in
-        Marked.mark m (EDefault ([caller], ltrue, callee)))
-      caller callee
+    let m = Marked.get_mark callee in
+    let ltrue =
+      Expr.elit (LBool true)
+        (Expr.with_ty m (Marked.mark (Expr.mark_pos m) (TLit TBool)))
+    in
+    Expr.edefault [caller] ltrue callee m
   in
   body
 
 let tag_with_log_entry
-    (e : 'm Dcalc.Ast.expr Bindlib.box)
+    (e : 'm Dcalc.Ast.expr boxed)
     (l : log_entry)
-    (markings : Utils.Uid.MarkedString.info list) :
-    'm Dcalc.Ast.expr Bindlib.box =
-  Bindlib.box_apply
-    (fun e ->
-      let m = mark_tany (Marked.get_mark e) (Expr.pos e) in
-      Marked.mark m (EApp (Marked.mark m (EOp (Unop (Log (l, markings)))), [e])))
-    e
+    (markings : Utils.Uid.MarkedString.info list) : 'm Dcalc.Ast.expr boxed =
+  let m = mark_tany (Marked.get_mark e) (Expr.pos e) in
+  Expr.eapp (Expr.eop (Unop (Log (l, markings))) m) [e] m
 
 (* In a list of exceptions, it is normally an error if more than a single one
    apply at the same time. This relaxes this constraint slightly, allowing a
@@ -153,15 +143,14 @@ let collapse_similar_outcomes (type m) (excepts : m Ast.expr list) :
   excepts
 
 let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
-    'm Dcalc.Ast.expr Bindlib.box =
-  Bindlib.box_apply (fun x -> Marked.same_mark_as x e)
-  @@
+    'm Dcalc.Ast.expr boxed =
+  let m = Marked.get_mark e in
   match Marked.unmark e with
-  | EVar v -> Bindlib.box_var (Var.Map.find v ctx.local_vars)
+  | EVar v -> Expr.evar (Var.Map.find v ctx.local_vars) m
   | ELit
       (( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
        | LDuration _ ) as l) ->
-    Bindlib.box (ELit l)
+    Expr.elit l m
   | EStruct (struct_name, e_fields) ->
     let struct_sig = StructMap.find struct_name ctx.structs in
     let d_fields, remaining_e_fields =
@@ -181,10 +170,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
            (fun fmt (field_name, _) ->
              Format.fprintf fmt "%a" StructFieldName.format_t field_name))
         (StructFieldMap.bindings remaining_e_fields)
-    else
-      Bindlib.box_apply
-        (fun d_fields -> ETuple (d_fields, Some struct_name))
-        (Bindlib.box_list d_fields)
+    else Expr.etuple d_fields (Some struct_name) m
   | EStructAccess (e1, field_name, struct_name) ->
     let struct_sig = StructMap.find struct_name ctx.structs in
     let _, field_index =
@@ -196,10 +182,8 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
           StructFieldName.format_t field_name StructName.format_t struct_name
     in
     let e1 = translate_expr ctx e1 in
-    Bindlib.box_apply
-      (fun e1 ->
-        ETupleAccess (e1, field_index, Some struct_name, List.map snd struct_sig))
-      e1
+    Expr.etupleaccess e1 field_index (Some struct_name)
+      (List.map snd struct_sig) m
   | EEnumInj (e1, constructor, enum_name) ->
     let enum_sig = EnumMap.find enum_name ctx.enums in
     let _, constructor_index =
@@ -211,9 +195,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
           EnumConstructor.format_t constructor EnumName.format_t enum_name
     in
     let e1 = translate_expr ctx e1 in
-    Bindlib.box_apply
-      (fun e1 -> EInj (e1, constructor_index, enum_name, List.map snd enum_sig))
-      e1
+    Expr.einj e1 constructor_index enum_name (List.map snd enum_sig) m
   | EMatchS (e1, enum_name, cases) ->
     let enum_sig = EnumMap.find enum_name ctx.enums in
     let d_cases, remaining_e_cases =
@@ -242,9 +224,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
         (EnumConstructorMap.bindings remaining_e_cases)
     else
       let e1 = translate_expr ctx e1 in
-      Bindlib.box_apply2
-        (fun d_fields e1 -> EMatch (e1, d_fields, enum_name))
-        (Bindlib.box_list d_cases) e1
+      Expr.ematch e1 d_cases enum_name m
   | EApp (e1, args) ->
     (* We insert various log calls to record arguments and outputs of
        user-defined functions belonging to scopes *)
@@ -292,12 +272,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
         ]
       | _ -> new_args
     in
-    let new_e =
-      Bindlib.box_apply2
-        (fun e' u -> Marked.same_mark_as (EApp (e', u)) e)
-        e1_func
-        (Bindlib.box_list new_args)
-    in
+    let new_e = Expr.eapp e1_func new_args m in
     let new_e =
       match Marked.unmark e1 with
       | ELocation l ->
@@ -307,7 +282,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
           EndCall (markings l)
       | _ -> new_e
     in
-    Bindlib.box_apply Marked.unmark new_e
+    new_e
   | EAbs (binder, typ) ->
     let xs, body = Bindlib.unmbind binder in
     let new_xs = Array.map (fun x -> Var.make (Bindlib.name_of x)) xs in
@@ -323,24 +298,23 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
         }
         body
     in
-    let binder = Bindlib.bind_mvar new_xs body in
-    Bindlib.box_apply (fun b -> EAbs (b, typ)) binder
+    let binder = Expr.bind new_xs body in
+    Expr.eabs binder typ m
   | EDefault (excepts, just, cons) ->
     let excepts = collapse_similar_outcomes excepts in
-    Bindlib.box_apply3
-      (fun e j c -> EDefault (e, j, c))
-      (Bindlib.box_list (List.map (translate_expr ctx) excepts))
-      (translate_expr ctx just) (translate_expr ctx cons)
+    Expr.edefault
+      (List.map (translate_expr ctx) excepts)
+      (translate_expr ctx just) (translate_expr ctx cons) m
   | ELocation (ScopelangScopeVar a) ->
     let v, _, _ = ScopeVarMap.find (Marked.unmark a) ctx.scope_vars in
-    Bindlib.box_var v
+    Expr.evar v m
   | ELocation (SubScopeVar (_, s, a)) -> (
     try
       let v, _, _ =
         ScopeVarMap.find (Marked.unmark a)
           (SubScopeMap.find (Marked.unmark s) ctx.subscope_vars)
       in
-      Bindlib.box_var v
+      Expr.evar v m
     with Not_found ->
       Errors.raise_multispanned_error
         [
@@ -355,16 +329,11 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
         SubScopeName.format_t (Marked.unmark s) ScopeVar.format_t
         (Marked.unmark a) SubScopeName.format_t (Marked.unmark s))
   | EIfThenElse (cond, et, ef) ->
-    Bindlib.box_apply3
-      (fun c t f -> EIfThenElse (c, t, f))
-      (translate_expr ctx cond) (translate_expr ctx et) (translate_expr ctx ef)
-  | EOp op -> Bindlib.box (EOp op)
-  | ErrorOnEmpty e' ->
-    Bindlib.box_apply (fun e' -> ErrorOnEmpty e') (translate_expr ctx e')
-  | EArray es ->
-    Bindlib.box_apply
-      (fun es -> EArray es)
-      (Bindlib.box_list (List.map (translate_expr ctx) es))
+    Expr.eifthenelse (translate_expr ctx cond) (translate_expr ctx et)
+      (translate_expr ctx ef) m
+  | EOp op -> Expr.eop op m
+  | ErrorOnEmpty e' -> Expr.eerroronempty (translate_expr ctx e') m
+  | EArray es -> Expr.earray (List.map (translate_expr ctx) es) m
 
 (** The result of a rule translation is a list of assignment, with variables and
     expressions. We also return the new translation context available after the
@@ -384,17 +353,16 @@ let translate_rule
     let a_name = ScopeVar.get_info (Marked.unmark a) in
     let a_var = Var.make (Marked.unmark a_name) in
     let new_e = translate_expr ctx e in
-    let a_expr = Expr.make_var (a_var, pos_mark var_def_pos) in
+    let a_expr = Expr.make_var a_var (pos_mark var_def_pos) in
     let merged_expr =
-      Bindlib.box_apply
-        (fun merged_expr -> ErrorOnEmpty merged_expr, pos_mark_as a_name)
+      Expr.eerroronempty
         (match Marked.unmark a_io.io_input with
-        | OnlyInput ->
-          failwith "should not happen"
-          (* scopelang should not contain any definitions of input only
-             variables *)
+        | OnlyInput -> failwith "should not happen"
+        (* scopelang should not contain any definitions of input only
+           variables *)
         | Reentrant -> merge_defaults a_expr new_e
         | NoInput -> new_e)
+        (pos_mark_as a_name)
     in
     let merged_expr =
       tag_with_log_entry merged_expr
@@ -413,7 +381,7 @@ let translate_rule
                 scope_let_pos = Marked.get_mark a;
               })
           (Bindlib.bind_var a_var next)
-          merged_expr),
+          (Expr.Box.inj merged_expr)),
       {
         ctx with
         scope_vars =
@@ -443,10 +411,7 @@ let translate_rule
     let thunked_or_nonempty_new_e =
       match Marked.unmark a_io.io_input with
       | NoInput -> failwith "should not happen"
-      | OnlyInput ->
-        Bindlib.box_apply
-          (fun new_e -> ErrorOnEmpty new_e, pos_mark_as subs_var)
-          new_e
+      | OnlyInput -> Expr.eerroronempty new_e (pos_mark_as subs_var)
       | Reentrant ->
         Expr.make_abs [| silent_var |] new_e
           [TLit TUnit, var_def_pos]
@@ -469,7 +434,7 @@ let translate_rule
                 scope_let_kind = SubScopeVarDefinition;
               })
           (Bindlib.bind_var a_var next)
-          thunked_or_nonempty_new_e),
+          (Expr.Box.inj thunked_or_nonempty_new_e)),
       {
         ctx with
         subscope_vars =
@@ -527,15 +492,12 @@ let translate_rule
             let a_var, _, _ =
               ScopeVarMap.find subvar.scope_var_name subscope_vars_defined
             in
-            Expr.make_var (a_var, mark_tany m pos_call))
+            Expr.make_var a_var (mark_tany m pos_call))
         all_subscope_input_vars
     in
     let subscope_struct_arg =
-      Bindlib.box_apply
-        (fun subscope_args ->
-          ( ETuple (subscope_args, Some called_scope_input_struct),
-            mark_tany m pos_call ))
-        (Bindlib.box_list subscope_args)
+      Expr.etuple subscope_args (Some called_scope_input_struct)
+        (mark_tany m pos_call)
     in
     let all_subscope_output_vars_dcalc =
       List.map
@@ -551,7 +513,7 @@ let translate_rule
     in
     let subscope_func =
       tag_with_log_entry
-        (Expr.make_var (scope_dcalc_var, mark_tany m pos_call))
+        (Expr.make_var scope_dcalc_var (mark_tany m pos_call))
         BeginCall
         [
           sigma_name, pos_sigma;
@@ -561,9 +523,7 @@ let translate_rule
     in
     let call_expr =
       tag_with_log_entry
-        (Bindlib.box_apply2
-           (fun e u -> EApp (e, [u]), mark_tany m pos_call)
-           subscope_func subscope_struct_arg)
+        (Expr.eapp subscope_func [subscope_struct_arg] (mark_tany m pos_call))
         EndCall
         [
           sigma_name, pos_sigma;
@@ -585,7 +545,7 @@ let translate_rule
               scope_let_expr = call_expr;
             })
         (Bindlib.bind_var result_tuple_var next)
-        call_expr
+        (Expr.Box.inj call_expr)
     in
     let result_bindings_lets next =
       List.fold_right
@@ -610,7 +570,8 @@ let translate_rule
                         mark_tany m pos_sigma );
                   })
               (Bindlib.bind_var v next)
-              (Expr.make_var (result_tuple_var, mark_tany m pos_sigma)),
+              (Expr.Box.inj
+                 (Expr.make_var result_tuple_var (mark_tany m pos_sigma))),
             i - 1 ))
         all_subscope_output_vars_dcalc
         (next, List.length all_subscope_output_vars_dcalc - 1)
@@ -649,7 +610,7 @@ let translate_rule
                 scope_let_kind = Assertion;
               })
           (Bindlib.bind_var (Var.make "_") next)
-          new_e),
+          (Expr.Box.inj new_e)),
       ctx )
 
 let translate_rules
@@ -676,17 +637,17 @@ let translate_rules
       scope_variables
   in
   let return_exp =
-    Bindlib.box_apply
-      (fun args ->
-        ETuple (args, Some sigma_return_struct_name), mark_tany mark pos_sigma)
-      (Bindlib.box_list
-         (List.map
-            (fun (_, (dcalc_var, _, _)) ->
-              Expr.make_var (dcalc_var, mark_tany mark pos_sigma))
-            scope_output_variables))
+    Expr.etuple
+      (List.map
+         (fun (_, (dcalc_var, _, _)) ->
+           Expr.make_var dcalc_var (mark_tany mark pos_sigma))
+         scope_output_variables)
+      (Some sigma_return_struct_name) (mark_tany mark pos_sigma)
   in
   ( scope_lets
-      (Bindlib.box_apply (fun return_exp -> Result return_exp) return_exp),
+      (Bindlib.box_apply
+         (fun return_exp -> Result return_exp)
+         (Expr.Box.inj return_exp)),
     new_ctx )
 
 let translate_scope_decl
@@ -783,8 +744,9 @@ let translate_scope_decl
                          mark_tany sigma.scope_mark pos_sigma );
                    })
                (Bindlib.bind_var v next)
-               (Expr.make_var
-                  (scope_input_var, mark_tany sigma.scope_mark pos_sigma)),
+               (Expr.Box.inj
+                  (Expr.make_var scope_input_var
+                     (mark_tany sigma.scope_mark pos_sigma))),
              i - 1 ))
          scope_input_variables
          (next, List.length scope_input_variables - 1))
diff --git a/compiler/shared_ast/definitions.ml b/compiler/shared_ast/definitions.ml
index 50900bd5..79bfb1bb 100644
--- a/compiler/shared_ast/definitions.ml
+++ b/compiler/shared_ast/definitions.ml
@@ -249,7 +249,13 @@ and ('a, 't) naked_gexpr =
       ('a, 't) gexpr * except * ('a, 't) gexpr
       -> ((lcalc as 'a), 't) naked_gexpr
 
-type 'a box = 'a Bindlib.box
+type ('a, 't) boxed_gexpr = (('a, 't) naked_gexpr Bindlib.box, 't) Marked.t
+(** The annotation is lifted outside of the box for expressions *)
+
+type 'e boxed = ('a, 't) boxed_gexpr constraint 'e = ('a, 't) gexpr
+(** [('a, 't) gexpr boxed] is [('a, 't) boxed_gexpr]. The difference with
+    [('a, 't) gexpr Bindlib.box] is that the annotations is outside of the box,
+    and can therefore be accessed without the need to resolve the box *)
 
 type ('e, 'b) binder = (('a, 't) naked_gexpr, 'b) Bindlib.binder
   constraint 'e = ('a, 't) gexpr
diff --git a/compiler/shared_ast/expr.ml b/compiler/shared_ast/expr.ml
index c180529f..861bd039 100644
--- a/compiler/shared_ast/expr.ml
+++ b/compiler/shared_ast/expr.ml
@@ -22,67 +22,99 @@ open Definitions
 
 (* Basic block constructors *)
 
-let evar v mark = Bindlib.box_apply (Marked.mark mark) (Bindlib.box_var v)
+module Box = struct
+  module B = Bindlib
 
-let etuple args s mark =
-  Bindlib.box_apply (fun args -> ETuple (args, s), mark) (Bindlib.box_list args)
+  let app0 x mark = B.box x, mark
+  let app1 (xb, m) f mark = B.box_apply (fun x -> f (x, m)) xb, mark
 
-let etupleaccess e1 i s typs mark =
-  Bindlib.box_apply (fun e1 -> ETupleAccess (e1, i, s, typs), mark) e1
+  let app2 (xb1, m1) (xb2, m2) f mark =
+    B.box_apply2 (fun x1 x2 -> f (x1, m1) (x2, m2)) xb1 xb2, mark
 
-let einj e1 i e_name typs mark =
-  Bindlib.box_apply (fun e1 -> EInj (e1, i, e_name, typs), mark) e1
+  let app3 (xb1, m1) (xb2, m2) (xb3, m3) f mark =
+    ( B.box_apply3 (fun x1 x2 x3 -> f (x1, m1) (x2, m2) (x3, m3)) xb1 xb2 xb3,
+      mark )
 
-let ematch arg arms e_name mark =
-  Bindlib.box_apply2
-    (fun arg arms -> EMatch (arg, arms, e_name), mark)
-    arg (Bindlib.box_list arms)
+  let appn xmbl f mark =
+    let xbl, ml = List.split xmbl in
+    B.box_apply (fun xl -> f (List.combine xl ml)) (B.box_list xbl), mark
 
-let earray args mark =
-  Bindlib.box_apply (fun args -> EArray args, mark) (Bindlib.box_list args)
+  let app1n (xb0, m0) xmbl f mark =
+    let xbl, ml = List.split xmbl in
+    ( B.box_apply2
+        (fun x0 xl -> f (x0, m0) (List.combine xl ml))
+        xb0 (B.box_list xbl),
+      mark )
 
-let elit l mark = Bindlib.box (ELit l, mark)
+  let app2n (xb0, m0) (xb1, m1) xmbl f mark =
+    let xbl, ml = List.split xmbl in
+    ( B.box_apply3
+        (fun x0 x1 xl -> f (x0, m0) (x1, m1) (List.combine xl ml))
+        xb0 xb1 (B.box_list xbl),
+      mark )
+
+  let inj : ('a, 't) boxed_gexpr -> ('a, 't) gexpr B.box =
+   fun em ->
+    B.box_apply (fun e -> Marked.mark (Marked.get_mark em) e) (Marked.unmark em)
+end
+
+let bind vars e = Bindlib.bind_mvar vars (Box.inj e)
+
+let subst binder vars =
+  Bindlib.msubst binder (Array.of_list (List.map Marked.unmark vars))
+
+let evar v mark = Marked.mark mark (Bindlib.box_var v)
+let etuple args s = Box.appn args @@ fun args -> ETuple (args, s)
+
+let etupleaccess e1 i s typs =
+  Box.app1 e1 @@ fun e1 -> ETupleAccess (e1, i, s, typs)
+
+let einj e1 i e_name typs = Box.app1 e1 @@ fun e1 -> EInj (e1, i, e_name, typs)
+
+let ematch arg arms e_name =
+  Box.app1n arg arms @@ fun arg arms -> EMatch (arg, arms, e_name)
+
+let earray args = Box.appn args @@ fun args -> EArray args
+let elit l mark = Marked.mark mark (Bindlib.box (ELit l))
 
 let eabs binder typs mark =
-  Bindlib.box_apply (fun binder -> EAbs (binder, typs), mark) binder
+  Bindlib.box_apply (fun binder -> EAbs (binder, typs)) binder, mark
 
-let eapp e1 args mark =
-  Bindlib.box_apply2
-    (fun e1 args -> EApp (e1, args), mark)
-    e1 (Bindlib.box_list args)
+let eapp e1 args = Box.app1n e1 args @@ fun e1 args -> EApp (e1, args)
+let eassert e1 = Box.app1 e1 @@ fun e1 -> EAssert e1
+let eop op = Box.app0 @@ EOp op
 
-let eassert e1 mark = Bindlib.box_apply (fun e1 -> EAssert e1, mark) e1
-let eop op mark = Bindlib.box (EOp op, mark)
+let edefault excepts just cons =
+  Box.app2n just cons excepts
+  @@ fun just cons excepts -> EDefault (excepts, just, cons)
 
-let edefault excepts just cons mark =
-  Bindlib.box_apply3
-    (fun excepts just cons -> EDefault (excepts, just, cons), mark)
-    (Bindlib.box_list excepts) just cons
+let eifthenelse e1 e2 e3 =
+  Box.app3 e1 e2 e3 @@ fun e1 e2 e3 -> EIfThenElse (e1, e2, e3)
 
-let eifthenelse e1 e2 e3 mark =
-  Bindlib.box_apply3 (fun e1 e2 e3 -> EIfThenElse (e1, e2, e3), mark) e1 e2 e3
+let eerroronempty e1 = Box.app1 e1 @@ fun e1 -> ErrorOnEmpty e1
+let eraise e1 = Box.app0 @@ ERaise e1
+let ecatch e1 exn e2 = Box.app2 e1 e2 @@ fun e1 e2 -> ECatch (e1, exn, e2)
+let elocation loc = Box.app0 @@ ELocation loc
 
-let eerroronempty e1 mark =
-  Bindlib.box_apply (fun e1 -> ErrorOnEmpty e1, mark) e1
+let estruct name (fields : ('a, 't) boxed_gexpr StructFieldMap.t) mark =
+  let module Lift = Bindlib.Lift (StructFieldMap) in
+  Marked.mark mark
+  @@ Bindlib.box_apply
+       (fun fields -> EStruct (name, fields))
+       (Lift.lift_box (StructFieldMap.map Box.inj fields))
 
-let eraise e1 mark = Bindlib.box (ERaise e1, mark)
+let estructaccess e1 field struc =
+  Box.app1 e1 @@ fun e1 -> EStructAccess (e1, field, struc)
 
-let ecatch e1 exn e2 mark =
-  Bindlib.box_apply2 (fun e1 e2 -> ECatch (e1, exn, e2), mark) e1 e2
-
-let elocation loc mark = Bindlib.box (ELocation loc, mark)
-
-let estruct name fields mark =
-  Bindlib.box_apply (fun es -> EStruct (name, es), mark) fields
-
-let estructaccess e1 field struc mark =
-  Bindlib.box_apply (fun e1 -> EStructAccess (e1, field, struc), mark) e1
-
-let eenuminj e1 cons enum mark =
-  Bindlib.box_apply (fun e1 -> EEnumInj (e1, cons, enum), mark) e1
+let eenuminj e1 cons enum = Box.app1 e1 @@ fun e1 -> EEnumInj (e1, cons, enum)
 
 let ematchs e1 enum cases mark =
-  Bindlib.box_apply2 (fun e1 cases -> EMatchS (e1, enum, cases), mark) e1 cases
+  let module Lift = Bindlib.Lift (EnumConstructorMap) in
+  Marked.mark mark
+  @@ Bindlib.box_apply2
+       (fun e1 cases -> EMatchS (e1, enum, cases))
+       (Box.inj e1)
+       (Lift.lift_box (EnumConstructorMap.map Box.inj cases))
 
 (* - Manipulation of marks - *)
 
@@ -156,18 +188,20 @@ let maybe_ty (type m) ?(typ = TAny) (m : m mark) : typ =
 let map
     (type a)
     (ctx : 'ctx)
-    ~(f : 'ctx -> (a, 'm1) gexpr -> (a, 'm2) gexpr box)
-    (e : ((a, 'm1) naked_gexpr, 'm2) Marked.t) : (a, 'm2) gexpr box =
+    ~(f : 'ctx -> (a, 'm1) gexpr -> (a, 'm2) boxed_gexpr)
+    (e : ((a, 'm1) naked_gexpr, 'm2) Marked.t) : (a, 'm2) boxed_gexpr =
   let m = Marked.get_mark e in
   match Marked.unmark e with
   | ELit l -> elit l m
   | EApp (e1, args) -> eapp (f ctx e1) (List.map (f ctx) args) m
-  | EOp op -> Bindlib.box (EOp op, m)
+  | EOp op -> eop op m
   | EArray args -> earray (List.map (f ctx) args) m
   | EVar v -> evar (Var.translate v) m
   | EAbs (binder, typs) ->
     let vars, body = Bindlib.unmbind binder in
-    eabs (Bindlib.bind_mvar (Array.map Var.translate vars) (f ctx body)) typs m
+    let body = f ctx body in
+    let binder = bind (Array.map Var.translate vars) body in
+    eabs binder typs m
   | EIfThenElse (e1, e2, e3) ->
     eifthenelse ((f ctx) e1) ((f ctx) e2) ((f ctx) e3) m
   | ETuple (args, s) -> etuple (List.map (f ctx) args) s m
@@ -184,23 +218,12 @@ let map
   | ERaise exn -> eraise exn m
   | ELocation loc -> elocation loc m
   | EStruct (name, fields) ->
-    let fields =
-      StructFieldMap.fold
-        (fun fld e -> Bindlib.box_apply2 (StructFieldMap.add fld) (f ctx e))
-        fields
-        (Bindlib.box StructFieldMap.empty)
-    in
+    let fields = StructFieldMap.map (f ctx) fields in
     estruct name fields m
   | EStructAccess (e1, field, struc) -> estructaccess (f ctx e1) field struc m
   | EEnumInj (e1, cons, enum) -> eenuminj (f ctx e1) cons enum m
   | EMatchS (e1, enum, cases) ->
-    let cases =
-      EnumConstructorMap.fold
-        (fun cstr e ->
-          Bindlib.box_apply2 (EnumConstructorMap.add cstr) (f ctx e))
-        cases
-        (Bindlib.box EnumConstructorMap.empty)
-    in
+    let cases = EnumConstructorMap.map (f ctx) cases in
     ematchs (f ctx e1) enum cases m
 
 let rec map_top_down ~f e = map () ~f:(fun () -> map_top_down ~f) (f e)
@@ -211,10 +234,12 @@ let map_marks ~f e =
 (* - *)
 
 (** See [Bindlib.box_term] documentation for why we are doing that. *)
-let box e =
+let rebox e =
   let rec id_t () e = map () ~f:id_t e in
   id_t () e
 
+let box e = Marked.same_mark_as (Bindlib.box (Marked.unmark e)) e
+let unbox (e, m) = Bindlib.unbox e, m
 let untype e = map_marks ~f:(fun m -> Untyped { pos = mark_pos m }) e
 
 (* Tests *)
@@ -721,8 +746,7 @@ let rec size : type a. (a, 't) gexpr -> int =
 
 (* - Expression building helpers - *)
 
-let make_var (x, mark) =
-  Bindlib.box_apply (fun x -> x, mark) (Bindlib.box_var x)
+let make_var v mark = evar v mark
 
 let make_abs xs e taus pos =
   let mark =
@@ -732,56 +756,46 @@ let make_abs xs e taus pos =
         List.fold_right
           (fun tx acc -> Marked.mark pos (TArrow (tx, acc)))
           taus ety)
-      (Marked.get_mark (Bindlib.unbox e))
+      (Marked.get_mark e)
   in
-  Bindlib.box_apply (fun b -> EAbs (b, taus), mark) (Bindlib.bind_mvar xs e)
+  eabs (bind xs e) taus mark
 
 let make_app e u pos =
-  Bindlib.box_apply2
-    (fun e u ->
-      let mark =
-        fold_marks
-          (fun _ -> pos)
-          (function
-            | [] -> assert false
-            | fty :: argtys ->
-              List.fold_left
-                (fun tf tx ->
-                  match Marked.unmark tf with
-                  | TArrow (tx', tr) ->
-                    assert (unifiable tx.ty tx');
-                    (* wrong arg type *)
-                    tr
-                  | TAny -> tf
-                  | _ ->
-                    Format.eprintf
-                      "Attempt to construct application of non-arrow type %a:@\n\
-                       %a"
-                      Print.typ_debug tf
-                      (Print.expr_debug ~debug:false)
-                      e;
-                    assert false)
-                fty.ty argtys)
-          (List.map Marked.get_mark (e :: u))
-      in
-      EApp (e, u), mark)
-    e (Bindlib.box_list u)
+  let mark =
+    fold_marks
+      (fun _ -> pos)
+      (function
+        | [] -> assert false
+        | fty :: argtys ->
+          List.fold_left
+            (fun tf tx ->
+              match Marked.unmark tf with
+              | TArrow (tx', tr) ->
+                assert (unifiable tx.ty tx');
+                (* wrong arg type *)
+                tr
+              | TAny -> tf
+              | _ -> assert false)
+            fty.ty argtys)
+      (List.map Marked.get_mark (e :: u))
+  in
+  eapp e u mark
 
 let empty_thunked_term mark =
   let silent = Var.make "_" in
   let pos = mark_pos mark in
   make_abs [| silent |]
-    (Bindlib.box (ELit LEmptyError, mark))
+    (Bindlib.box (ELit LEmptyError), mark)
     [TLit TUnit, pos]
     pos
 
 let make_let_in x tau e1 e2 mpos =
-  make_app (make_abs [| x |] e2 [tau] mpos) [e1] (pos (Bindlib.unbox e2))
+  make_app (make_abs [| x |] e2 [tau] mpos) [e1] (pos e2)
 
 let make_multiple_let_in xs taus e1s e2 mpos =
-  make_app (make_abs xs e2 taus mpos) e1s (pos (Bindlib.unbox e2))
+  make_app (make_abs xs e2 taus mpos) e1s (pos e2)
 
-let make_default exceptions just cons mark =
+let make_default_unboxed exceptions just cons =
   let rec bool_value = function
     | ELit (LBool b), _ -> Some b
     | EApp ((EOp (Unop (Log (l, _))), _), [e]), _
@@ -792,11 +806,15 @@ let make_default exceptions just cons mark =
     | _ -> None
   in
   match exceptions, bool_value just, cons with
-  | [], Some true, cons -> cons
-  | exceptions, Some true, (EDefault ([], just, cons), mark) ->
-    EDefault (exceptions, just, cons), mark
-  | [except], Some false, _ -> except
-  | exceptions, _, cons -> EDefault (exceptions, just, cons), mark
+  | [], Some true, cons -> Marked.unmark cons
+  | exceptions, Some true, (EDefault ([], just, cons), _) ->
+    EDefault (exceptions, just, cons)
+  | [except], Some false, _ -> Marked.unmark except
+  | exceptions, _, cons -> EDefault (exceptions, just, cons)
+
+let make_default exceptions just cons =
+  Box.app2n just cons exceptions
+  @@ fun just cons exceptions -> make_default_unboxed exceptions just cons
 
 let make_tuple el structname m0 =
   match el with
@@ -811,6 +829,6 @@ let make_tuple el structname m0 =
       fold_marks
         (fun posl -> List.hd posl)
         (fun ml -> TTuple (List.map (fun t -> t.ty) ml), (List.hd ml).pos)
-        (List.map (fun e -> Marked.get_mark (Bindlib.unbox e)) el)
+        (List.map (fun e -> Marked.get_mark e) el)
     in
     etuple el structname m
diff --git a/compiler/shared_ast/expr.mli b/compiler/shared_ast/expr.mli
index 1d6e28d2..3b97a966 100644
--- a/compiler/shared_ast/expr.mli
+++ b/compiler/shared_ast/expr.mli
@@ -22,82 +22,133 @@ open Definitions
 
 (** {2 Boxed constructors} *)
 
-val box : ('a, 't) gexpr -> ('a, 't) gexpr box
-val evar : ('a, 't) gexpr Var.t -> 't -> ('a, 't) gexpr box
+val box : ('a, 't) gexpr -> ('a, 't) boxed_gexpr
+(** Box the expression from the outside *)
+
+val unbox : ('a, 't) boxed_gexpr -> ('a, 't) gexpr
+(** For closed expressions, similar to [Bindlib.unbox] *)
+
+val rebox : ('a, 't) gexpr -> ('a, 't) boxed_gexpr
+(** Rebuild the whole term, re-binding all variables and exposing free variables *)
+
+val evar : ('a, 't) gexpr Var.t -> 't -> ('a, 't) boxed_gexpr
+
+val bind :
+  ('a, 't) gexpr Var.t array ->
+  ('a, 't) boxed_gexpr ->
+  (('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder Bindlib.box
+
+val subst :
+  (('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder ->
+  ('a, 't) gexpr list ->
+  ('a, 't) gexpr
 
 val etuple :
-  (([< dcalc | lcalc ] as 'a), 't) gexpr box list ->
+  (([< dcalc | lcalc ] as 'a), 't) boxed_gexpr list ->
   StructName.t option ->
   't ->
-  ('a, 't) gexpr box
+  ('a, 't) boxed_gexpr
 
 val etupleaccess :
-  (([< dcalc | lcalc ] as 'a), 't) gexpr box ->
+  (([< dcalc | lcalc ] as 'a), 't) boxed_gexpr ->
   int ->
   StructName.t option ->
   typ list ->
   't ->
-  ('a, 't) gexpr box
+  ('a, 't) boxed_gexpr
 
 val einj :
-  (([< dcalc | lcalc ] as 'a), 't) gexpr box ->
+  (([< dcalc | lcalc ] as 'a), 't) boxed_gexpr ->
   int ->
   EnumName.t ->
   typ list ->
   't ->
-  ('a, 't) gexpr box
+  ('a, 't) boxed_gexpr
 
 val ematch :
-  (([< dcalc | lcalc ] as 'a), 't) gexpr box ->
-  ('a, 't) gexpr box list ->
+  (([< dcalc | lcalc ] as 'a), 't) boxed_gexpr ->
+  ('a, 't) boxed_gexpr list ->
   EnumName.t ->
   't ->
-  ('a, 't) gexpr box
+  ('a, 't) boxed_gexpr
 
-val earray : ('a any, 't) gexpr box list -> 't -> ('a, 't) gexpr box
-val elit : 'a any glit -> 't -> ('a, 't) gexpr box
+val earray : ('a any, 't) boxed_gexpr list -> 't -> ('a, 't) boxed_gexpr
+val elit : 'a any glit -> 't -> ('a, 't) boxed_gexpr
 
 val eabs :
-  (('a any, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder box ->
+  (('a any, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder Bindlib.box ->
   typ list ->
   't ->
-  ('a, 't) gexpr box
+  ('a, 't) boxed_gexpr
 
 val eapp :
-  ('a any, 't) gexpr box -> ('a, 't) gexpr box list -> 't -> ('a, 't) gexpr box
+  ('a any, 't) boxed_gexpr ->
+  ('a, 't) boxed_gexpr list ->
+  't ->
+  ('a, 't) boxed_gexpr
 
 val eassert :
-  (([< dcalc | lcalc ] as 'a), 't) gexpr box -> 't -> ('a, 't) gexpr box
+  (([< dcalc | lcalc ] as 'a), 't) boxed_gexpr -> 't -> ('a, 't) boxed_gexpr
 
-val eop : operator -> 't -> (_ any, 't) gexpr box
+val eop : operator -> 't -> (_ any, 't) boxed_gexpr
 
 val edefault :
-  (([< desugared | scopelang | dcalc ] as 'a), 't) gexpr box list ->
-  ('a, 't) gexpr box ->
-  ('a, 't) gexpr box ->
+  (([< desugared | scopelang | dcalc ] as 'a), 't) boxed_gexpr list ->
+  ('a, 't) boxed_gexpr ->
+  ('a, 't) boxed_gexpr ->
   't ->
-  ('a, 't) gexpr box
+  ('a, 't) boxed_gexpr
 
 val eifthenelse :
-  ('a any, 't) gexpr box ->
-  ('a, 't) gexpr box ->
-  ('a, 't) gexpr box ->
+  ('a any, 't) boxed_gexpr ->
+  ('a, 't) boxed_gexpr ->
+  ('a, 't) boxed_gexpr ->
   't ->
-  ('a, 't) gexpr box
+  ('a, 't) boxed_gexpr
 
 val eerroronempty :
-  (([< desugared | scopelang | dcalc ] as 'a), 't) gexpr box ->
+  (([< desugared | scopelang | dcalc ] as 'a), 't) boxed_gexpr ->
   't ->
-  ('a, 't) gexpr box
+  ('a, 't) boxed_gexpr
 
 val ecatch :
-  (lcalc, 't) gexpr box ->
+  (lcalc, 't) boxed_gexpr ->
   except ->
-  (lcalc, 't) gexpr box ->
+  (lcalc, 't) boxed_gexpr ->
   't ->
-  (lcalc, 't) gexpr box
+  (lcalc, 't) boxed_gexpr
 
-val eraise : except -> 't -> (lcalc, 't) gexpr box
+val eraise : except -> 't -> (lcalc, 't) boxed_gexpr
+
+val elocation :
+  ([< desugared | scopelang ] as 'a) glocation -> 't -> ('a, 't) boxed_gexpr
+
+val estruct :
+  StructName.t ->
+  (([< desugared | scopelang ] as 'a), 't) boxed_gexpr StructFieldMap.t ->
+  't ->
+  ('a, 't) boxed_gexpr
+
+val estructaccess :
+  (([< desugared | scopelang ] as 'a), 't) boxed_gexpr ->
+  StructFieldName.t ->
+  StructName.t ->
+  't ->
+  ('a, 't) boxed_gexpr
+
+val eenuminj :
+  (([< desugared | scopelang ] as 'a), 't) boxed_gexpr ->
+  EnumConstructor.t ->
+  EnumName.t ->
+  't ->
+  ('a, 't) boxed_gexpr
+
+val ematchs :
+  (([< desugared | scopelang ] as 'a), 't) boxed_gexpr ->
+  EnumName.t ->
+  ('a, 't) boxed_gexpr EnumConstructorMap.t ->
+  't ->
+  ('a, 't) boxed_gexpr
 
 (** Manipulation of marks *)
 
@@ -129,18 +180,18 @@ val maybe_ty : ?typ:naked_typ -> 'm mark -> typ
 
 (** Manipulation of marked expressions *)
 
-val pos : ('e, 'm mark) gexpr -> Pos.t
+val pos : ('a, 'm mark) Marked.t -> Pos.t
 val ty : ('e, typed mark) Marked.t -> typ
 val set_ty : typ -> ('a, 'm mark) Marked.t -> ('a, typed mark) Marked.t
-val untype : ('a, 'm mark) gexpr -> ('a, untyped mark) gexpr box
+val untype : ('a, 'm mark) gexpr -> ('a, untyped mark) boxed_gexpr
 
 (** {2 Traversal functions} *)
 
 val map :
   'ctx ->
-  f:('ctx -> ('a, 't1) gexpr -> ('a, 't2) gexpr box) ->
+  f:('ctx -> ('a, 't1) gexpr -> ('a, 't2) boxed_gexpr) ->
   (('a, 't1) naked_gexpr, 't2) Marked.t ->
-  ('a, 't2) gexpr box
+  ('a, 't2) boxed_gexpr
 (** Flat (non-recursive) mapping on expressions.
 
     If you want to apply a map transform to an expression, you can save up
@@ -163,55 +214,55 @@ val map :
 val map_top_down :
   f:(('a, 't1) gexpr -> (('a, 't1) naked_gexpr, 't2) Marked.t) ->
   ('a, 't1) gexpr ->
-  ('a, 't2) gexpr box
+  ('a, 't2) boxed_gexpr
 (** Recursively applies [f] to the nodes of the expression tree. The type
     returned by [f] is hybrid since the mark at top-level has been rewritten,
     but not yet the marks in the subtrees. *)
 
-val map_marks : f:('t1 -> 't2) -> ('a, 't1) gexpr -> ('a, 't2) gexpr box
+val map_marks : f:('t1 -> 't2) -> ('a, 't1) gexpr -> ('a, 't2) boxed_gexpr
 
 (** {2 Expression building helpers} *)
 
-val make_var : ('a, 't) gexpr Var.t * 'b -> (('a, 't) naked_gexpr * 'b) box
+val make_var : ('a, 't) gexpr Var.t -> 't -> ('a, 't) boxed_gexpr
 
 val make_abs :
   ('a, 'm mark) gexpr Var.vars ->
-  ('a, 'm mark) gexpr box ->
+  ('a, 'm mark) boxed_gexpr ->
   typ list ->
   Pos.t ->
-  ('a, 'm mark) gexpr box
+  ('a, 'm mark) boxed_gexpr
 
 val make_app :
-  ('a any, 'm mark) gexpr box ->
-  ('a, 'm mark) gexpr box list ->
+  ('a any, 'm mark) boxed_gexpr ->
+  ('a, 'm mark) boxed_gexpr list ->
   Pos.t ->
-  ('a, 'm mark) gexpr box
+  ('a, 'm mark) boxed_gexpr
 
 val empty_thunked_term :
-  'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) gexpr box
+  'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) boxed_gexpr
 
 val make_let_in :
   ('a, 'm mark) gexpr Var.t ->
   typ ->
-  ('a, 'm mark) gexpr box ->
-  ('a, 'm mark) gexpr box ->
+  ('a, 'm mark) boxed_gexpr ->
+  ('a, 'm mark) boxed_gexpr ->
   Pos.t ->
-  ('a, 'm mark) gexpr box
+  ('a, 'm mark) boxed_gexpr
 
 val make_multiple_let_in :
   ('a, 'm mark) gexpr Var.vars ->
   typ list ->
-  ('a, 'm mark) gexpr box list ->
-  ('a, 'm mark) gexpr box ->
+  ('a, 'm mark) boxed_gexpr list ->
+  ('a, 'm mark) boxed_gexpr ->
   Pos.t ->
-  ('a, 'm mark) gexpr box
+  ('a, 'm mark) boxed_gexpr
 
 val make_default :
-  (([< desugared | scopelang | dcalc ] as 'a), 't) gexpr list ->
-  ('a, 't) gexpr ->
-  ('a, 't) gexpr ->
+  (([< desugared | scopelang | dcalc ] as 'a), 't) boxed_gexpr list ->
+  ('a, 't) boxed_gexpr ->
+  ('a, 't) boxed_gexpr ->
   't ->
-  ('a, 't) gexpr
+  ('a, 't) boxed_gexpr
 (** [make_default ?pos exceptions just cons] builds a term semantically
     equivalent to [<exceptions | just :- cons>] (the [EDefault] constructor)
     while avoiding redundant nested constructions. The position is extracted
@@ -226,16 +277,16 @@ val make_default :
     - [<ex | false :- _>], when [ex] is a single exception, is rewritten as [ex] *)
 
 val make_tuple :
-  (([< dcalc | lcalc ] as 'a), 'm mark) gexpr box list ->
+  (([< dcalc | lcalc ] as 'a), 'm mark) boxed_gexpr list ->
   StructName.t option ->
   'm mark ->
-  ('a, 'm mark) gexpr box
+  ('a, 'm mark) boxed_gexpr
 (** Builds a tuple; the mark argument is only used as witness and for position
     when building 0-uples *)
 
 (** {2 Transformations} *)
 
-val remove_logging_calls : ('a any, 't) gexpr -> ('a, 't) gexpr box
+val remove_logging_calls : ('a any, 't) gexpr -> ('a, 't) boxed_gexpr
 (** Removes all calls to [Log] unary operators in the AST, replacing them by
     their argument. *)
 
@@ -267,3 +318,72 @@ val free_vars : ('a any, 't) gexpr -> ('a, 't) gexpr Var.Set.t
 
 val size : ('a, 't) gexpr -> int
 (** Used by the optimizer to know when to stop *)
+
+(** {2 Low-level handling of boxed expressions} *)
+module Box : sig
+  (** This module contains helper functions for Bindlib, and wrappers to use
+      boxed expressions.
+
+      We use the [boxed_expr = naked_expr box marked] type throughout, rather
+      than the more straightforward [expr box = naked_expr marked box], because
+      the latter would force us to resolve the box every time we need to recover
+      the annotation, which happens often. It's more efficient and convenient to
+      add the annotation outside of the box, and delay its injection (using
+      [box_inj]) to when the parent term gets built. *)
+
+  val inj : ('a, 't) boxed_gexpr -> ('a, 't) gexpr Bindlib.box
+  (** Inject the annotation within the box, to use e.g. when a [gexpr box] is
+      required for building parent terms *)
+
+  val app0 : ('a, 't) naked_gexpr -> 't -> ('a, 't) boxed_gexpr
+  (** The [app*] functions allow building boxed expressions using
+      [Bindlib.apply_box] and its variants, while correctly handling the
+      expression annotations. Note that the function provided as argument should
+      return a [naked_gexpr] and the expression annotation (['t]) is provided as
+      a separate argument. *)
+
+  val app1 :
+    ('a, 't) boxed_gexpr ->
+    (('a, 't) gexpr -> ('a, 't) naked_gexpr) ->
+    't ->
+    ('a, 't) boxed_gexpr
+
+  val app2 :
+    ('a, 't) boxed_gexpr ->
+    ('a, 't) boxed_gexpr ->
+    (('a, 't) gexpr -> ('a, 't) gexpr -> ('a, 't) naked_gexpr) ->
+    't ->
+    ('a, 't) boxed_gexpr
+
+  val app3 :
+    ('a, 't) boxed_gexpr ->
+    ('a, 't) boxed_gexpr ->
+    ('a, 't) boxed_gexpr ->
+    (('a, 't) gexpr -> ('a, 't) gexpr -> ('a, 't) gexpr -> ('a, 't) naked_gexpr) ->
+    't ->
+    ('a, 't) boxed_gexpr
+
+  val appn :
+    ('a, 't) boxed_gexpr list ->
+    (('a, 't) gexpr list -> ('a, 't) naked_gexpr) ->
+    't ->
+    ('a, 't) boxed_gexpr
+
+  val app1n :
+    ('a, 't) boxed_gexpr ->
+    ('a, 't) boxed_gexpr list ->
+    (('a, 't) gexpr -> ('a, 't) gexpr list -> ('a, 't) naked_gexpr) ->
+    't ->
+    ('a, 't) boxed_gexpr
+
+  val app2n :
+    ('a, 't) boxed_gexpr ->
+    ('a, 't) boxed_gexpr ->
+    ('a, 't) boxed_gexpr list ->
+    (('a, 't) gexpr ->
+    ('a, 't) gexpr ->
+    ('a, 't) gexpr list ->
+    ('a, 't) naked_gexpr) ->
+    't ->
+    ('a, 't) boxed_gexpr
+end
diff --git a/compiler/shared_ast/program.mli b/compiler/shared_ast/program.mli
index 9e7246e7..58ea68b9 100644
--- a/compiler/shared_ast/program.mli
+++ b/compiler/shared_ast/program.mli
@@ -20,17 +20,17 @@ open Definitions
 (** {2 Transformations} *)
 
 val map_exprs :
-  f:('expr1 -> 'expr2 box) ->
+  f:('expr1 -> 'expr2 boxed) ->
   varf:('expr1 Var.t -> 'expr2 Var.t) ->
   'expr1 program ->
-  'expr2 program box
+  'expr2 program Bindlib.box
 
 val untype :
   (([< dcalc | lcalc ] as 'a), 'm mark) gexpr program ->
   ('a, untyped mark) gexpr program
 
 val to_expr :
-  (([< dcalc | lcalc ], _) gexpr as 'e) program -> ScopeName.t -> 'e box
+  (([< dcalc | lcalc ], _) gexpr as 'e) program -> ScopeName.t -> 'e boxed
 (** Usage: [build_whole_program_expr program main_scope] builds an expression
     corresponding to the main program and returning the main scope as a
     function. *)
diff --git a/compiler/shared_ast/scope.ml b/compiler/shared_ast/scope.ml
index 703f792d..a3c242f5 100644
--- a/compiler/shared_ast/scope.ml
+++ b/compiler/shared_ast/scope.ml
@@ -33,15 +33,21 @@ let rec fold_right_lets ~f ~init scope_body_expr =
     let next_result = fold_right_lets ~f ~init next in
     f scope_let var next_result
 
-let map_exprs_in_lets ~f ~varf scope_body_expr =
+let map_exprs_in_lets :
+    f:('expr1 -> 'expr2 boxed) ->
+    varf:('expr1 Var.t -> 'expr2 Var.t) ->
+    'expr1 scope_body_expr ->
+    'expr2 scope_body_expr Bindlib.box =
+ fun ~f ~varf scope_body_expr ->
   fold_right_lets
     ~f:(fun scope_let var_next acc ->
       Bindlib.box_apply2
         (fun scope_let_next scope_let_expr ->
           ScopeLet { scope_let with scope_let_next; scope_let_expr })
         (Bindlib.bind_var (varf var_next) acc)
-        (f scope_let.scope_let_expr))
-    ~init:(fun res -> Bindlib.box_apply (fun res -> Result res) (f res))
+        (Expr.Box.inj (f scope_let.scope_let_expr)))
+    ~init:(fun res ->
+      Bindlib.box_apply (fun res -> Result res) (Expr.Box.inj (f res)))
     scope_body_expr
 
 let rec fold_left ~f ~init scopes =
@@ -106,8 +112,7 @@ let get_body_mark scope_body =
   let _, e = Bindlib.unbind scope_body.scope_body_expr in
   get_body_expr_mark e
 
-let rec unfold_body_expr (ctx : decl_ctx) (scope_let : 'e scope_body_expr) :
-    'e box =
+let rec unfold_body_expr (ctx : decl_ctx) (scope_let : 'e scope_body_expr) =
   match scope_let with
   | Result e -> Expr.box e
   | ScopeLet
@@ -135,7 +140,7 @@ let build_typ_from_sig
 type 'e scope_name_or_var = ScopeName of ScopeName.t | ScopeVar of 'e Var.t
 
 let to_expr (ctx : decl_ctx) (body : 'e scope_body) (mark_scope : 'm mark) :
-    'e box =
+    'e boxed =
   let var, body_expr = Bindlib.unbind body.scope_body_expr in
   let body_expr = unfold_body_expr ctx body_expr in
   Expr.make_abs [| var |] body_expr
@@ -149,7 +154,7 @@ let format
     ((n, s) : ScopeName.t * 'm scope_body) =
   Format.fprintf fmt "@[<hov 2>%a %a =@ %a@]" Print.keyword "let"
     ScopeName.format_t n (Expr.format ctx ~debug)
-    (Bindlib.unbox
+    (Expr.unbox
        (to_expr ctx s
           (Expr.map_mark
              (fun _ -> Marked.get_mark (ScopeName.get_info n))
@@ -160,11 +165,11 @@ let rec unfold
     (ctx : decl_ctx)
     (s : 'e scopes)
     (mark : 'm mark)
-    (main_scope : 'expr scope_name_or_var) : 'e Bindlib.box =
+    (main_scope : 'expr scope_name_or_var) : 'e boxed =
   match s with
   | Nil -> (
     match main_scope with
-    | ScopeVar v -> Bindlib.box_apply (fun v -> v, mark) (Bindlib.box_var v)
+    | ScopeVar v -> Expr.make_var v mark
     | ScopeName _ -> failwith "should not happen")
   | ScopeDef { scope_name; scope_body; scope_next } ->
     let scope_var, scope_next = Bindlib.unbind scope_next in
diff --git a/compiler/shared_ast/scope.mli b/compiler/shared_ast/scope.mli
index 54e3e10f..6e18ee5e 100644
--- a/compiler/shared_ast/scope.mli
+++ b/compiler/shared_ast/scope.mli
@@ -43,10 +43,10 @@ val fold_right_lets :
     scope lets to be examined (which are before in the program order). *)
 
 val map_exprs_in_lets :
-  f:('expr1 -> 'expr2 box) ->
+  f:('expr1 -> 'expr2 boxed) ->
   varf:('expr1 Var.t -> 'expr2 Var.t) ->
   'expr1 scope_body_expr ->
-  'expr2 scope_body_expr box
+  'expr2 scope_body_expr Bindlib.box
 
 val fold_left :
   f:('a -> 'expr1 scope_def -> 'expr1 Var.t -> 'a) ->
@@ -67,13 +67,16 @@ val fold_right :
     where [scope_var] is the variable bound to the scope in the next scopes to
     be examined (which are before in the program order). *)
 
-val map : f:('e scope_def -> 'e scope_def box) -> 'e scopes -> 'e scopes box
+val map :
+  f:('e scope_def -> 'e scope_def Bindlib.box) ->
+  'e scopes ->
+  'e scopes Bindlib.box
 
 val map_exprs :
-  f:('expr1 -> 'expr2 box) ->
+  f:('expr1 -> 'expr2 boxed) ->
   varf:('expr1 Var.t -> 'expr2 Var.t) ->
   'expr1 scopes ->
-  'expr2 scopes box
+  'expr2 scopes Bindlib.box
 (** This is the main map visitor for all the expressions inside all the scopes
     of the program. *)
 
@@ -92,7 +95,7 @@ val to_expr :
   decl_ctx ->
   ('a any, 'm mark) gexpr scope_body ->
   'm mark ->
-  ('a, 'm mark) gexpr box
+  ('a, 'm mark) boxed_gexpr
 (** Usage: [to_expr ctx body scope_position] where [scope_position] corresponds
     to the line of the scope declaration for instance. *)
 
@@ -103,7 +106,7 @@ val unfold :
   ((_, 'm mark) gexpr as 'e) scopes ->
   'm mark ->
   'e scope_name_or_var ->
-  'e box
+  'e boxed
 
 val build_typ_from_sig :
   decl_ctx -> StructName.t -> StructName.t -> Pos.t -> typ
diff --git a/compiler/shared_ast/typing.ml b/compiler/shared_ast/typing.ml
index 596fb6a7..f7e2e0f2 100644
--- a/compiler/shared_ast/typing.ml
+++ b/compiler/shared_ast/typing.ml
@@ -309,28 +309,6 @@ end
 
 let add_pos e ty = Marked.mark (Expr.pos e) ty
 let ty (_, { uf; _ }) = uf
-let ( let+ ) x f = Bindlib.box_apply f x
-let ( and+ ) x1 x2 = Bindlib.box_pair x1 x2
-
-(* Maps a boxing function on a list, returning a boxed list *)
-let bmap (f : 'a -> 'b Bindlib.box) (es : 'a list) : 'b list Bindlib.box =
-  List.fold_right
-    (fun e acc ->
-      let+ e' = f e and+ acc in
-      e' :: acc)
-    es (Bindlib.box [])
-
-(* Likewise, but with a function of two arguments on two lists of identical
-   lengths *)
-let bmap2 (f : 'a -> 'b -> 'c Bindlib.box) (es : 'a list) (xs : 'b list) :
-    'c list Bindlib.box =
-  List.fold_right2
-    (fun e x acc ->
-      let+ e' = f e x and+ acc in
-      e' :: acc)
-    es xs (Bindlib.box [])
-
-let box_ty e = Bindlib.unbox (Bindlib.box_apply ty e)
 
 (** Infers the most permissive type from an expression *)
 let rec typecheck_expr_bottom_up :
@@ -338,122 +316,121 @@ let rec typecheck_expr_bottom_up :
     A.decl_ctx ->
     (a, m A.mark) A.gexpr Env.t ->
     (a, m A.mark) A.gexpr ->
-    (a, mark) A.gexpr A.box =
+    (a, mark) A.boxed_gexpr =
  fun ctx env e ->
   (* Cli.debug_format "Looking for type of %a" (Expr.format ~debug:true ctx)
      e; *)
   let pos_e = Expr.pos e in
-  let mark e1 uf =
+  let uf_mark uf =
     let () =
-      (* If the expression already has a type annotation, validate it before
-         rewrite *)
+      (* If the expression already has a type annotation, validate it *)
       match Marked.get_mark e with
       | A.Untyped _ | A.Typed { A.ty = A.TAny, _; _ } -> ()
       | A.Typed { A.ty; _ } -> unify ctx e uf (ast_to_typ ty)
     in
-    Marked.mark { uf; pos = pos_e } e1
+    { uf; pos = pos_e }
   in
-  let unionfind_make ?(pos = e) t = UnionFind.make (add_pos pos t) in
-  let mark_with_uf e1 ?pos ty = mark e1 (unionfind_make ?pos ty) in
+  let unionfind ?(pos = e) t = UnionFind.make (add_pos pos t) in
+  let ty_mark ?pos ty = uf_mark (unionfind ?pos ty) in
+  (* let mark_with_uf e1 ?pos ty = mark e1 (unionfind_make ?pos ty) in *)
   match Marked.unmark e with
-  | A.ELocation loc as e1 -> (
-    let ty =
+  | A.ELocation loc ->
+    let ty_opt =
       match loc with
       | DesugaredScopeVar (v, _) | ScopelangScopeVar v ->
         Env.get_scope_var env (Marked.unmark v)
       | SubScopeVar (scope_name, _, v) ->
         Env.get_subscope_var env scope_name (Marked.unmark v)
     in
-    match ty with
-    | Some ty -> Bindlib.box (mark e1 (ast_to_typ ty))
-    | None ->
-      Errors.raise_spanned_error pos_e "Reference to %a not found"
-        (Expr.format ctx) e)
+    let ty =
+      match ty_opt with
+      | Some ty -> ty
+      | None ->
+        Errors.raise_spanned_error pos_e "Reference to %a not found"
+          (Expr.format ctx) e
+    in
+    Expr.elocation loc (uf_mark (ast_to_typ ty))
   | A.EStruct (s_name, fmap) ->
-    let+ fmap' =
+    let str = A.StructMap.find s_name ctx.A.ctx_structs in
+    let fmap' =
       (* This assumes that the fields in fmap and the struct type are already
          ensured to be the same *)
-      List.fold_left
-        (fun fmap' (f_name, f_ty) ->
-          let f_e = A.StructFieldMap.find f_name fmap in
-          let+ fmap'
-          and+ f_e' = typecheck_expr_top_down ctx env (ast_to_typ f_ty) f_e in
-          A.StructFieldMap.add f_name f_e' fmap')
-        (Bindlib.box A.StructFieldMap.empty)
-        (A.StructMap.find s_name ctx.A.ctx_structs)
+      A.StructFieldMap.mapi
+        (fun f_name f_e ->
+          let f_ty = List.assoc f_name str in
+          typecheck_expr_top_down ctx env (ast_to_typ f_ty) f_e)
+        fmap
     in
-    mark_with_uf (A.EStruct (s_name, fmap')) (TStruct s_name)
+    Expr.estruct s_name fmap' (ty_mark (TStruct s_name))
   | A.EStructAccess (e_struct, f_name, s_name) ->
     let f_ty =
       ast_to_typ (List.assoc f_name (A.StructMap.find s_name ctx.A.ctx_structs))
     in
-    let+ e_struct' =
-      typecheck_expr_top_down ctx env (unionfind_make (TStruct s_name)) e_struct
+    let e_struct' =
+      typecheck_expr_top_down ctx env (unionfind (TStruct s_name)) e_struct
     in
-    mark (A.EStructAccess (e_struct', f_name, s_name)) f_ty
+    Expr.estructaccess e_struct' f_name s_name (uf_mark f_ty)
   | A.EEnumInj (e_enum, c_name, e_name) ->
     let c_ty =
       ast_to_typ (List.assoc c_name (A.EnumMap.find e_name ctx.A.ctx_enums))
     in
-    let+ e_enum' = typecheck_expr_top_down ctx env c_ty e_enum in
-    mark (A.EEnumInj (e_enum', c_name, e_name)) (unionfind_make (TEnum e_name))
+    let e_enum' = typecheck_expr_top_down ctx env c_ty e_enum in
+    Expr.eenuminj e_enum' c_name e_name (ty_mark (TEnum e_name))
   | A.EMatchS (e1, e_name, cases) ->
     let cases_ty = A.EnumMap.find e_name ctx.A.ctx_enums in
-    let t_ret = unionfind_make ~pos:e1 (TAny (Any.fresh ())) in
-    let+ e1' =
-      typecheck_expr_top_down ctx env (unionfind_make (TEnum e_name)) e1
-    and+ cases' =
-      A.EnumConstructorMap.fold
-        (fun c_name e cases' ->
+    let t_ret = unionfind ~pos:e1 (TAny (Any.fresh ())) in
+    let e1' = typecheck_expr_top_down ctx env (unionfind (TEnum e_name)) e1 in
+    let cases' =
+      A.EnumConstructorMap.mapi
+        (fun c_name e ->
           let c_ty = List.assoc c_name cases_ty in
-          let e_ty = unionfind_make ~pos:e (TArrow (ast_to_typ c_ty, t_ret)) in
-          let+ cases' and+ e' = typecheck_expr_top_down ctx env e_ty e in
-          A.EnumConstructorMap.add c_name e' cases')
+          let e_ty = unionfind ~pos:e (TArrow (ast_to_typ c_ty, t_ret)) in
+          typecheck_expr_top_down ctx env e_ty e)
         cases
-        (Bindlib.box A.EnumConstructorMap.empty)
     in
-    mark (A.EMatchS (e1', e_name, cases')) t_ret
-  | A.ERaise ex ->
-    Bindlib.box (mark_with_uf (A.ERaise ex) (TAny (Any.fresh ())))
+    Expr.ematchs e1' e_name cases' (uf_mark t_ret)
+  | A.ERaise ex -> Expr.eraise ex (ty_mark (TAny (Any.fresh ())))
   | A.ECatch (e1, ex, e2) ->
-    let+ e1' = typecheck_expr_bottom_up ctx env e1
-    and+ e2' = typecheck_expr_bottom_up ctx env e2 in
+    let e1' = typecheck_expr_bottom_up ctx env e1 in
+    let e2' = typecheck_expr_bottom_up ctx env e2 in
     let e_ty = ty e1' in
     unify ctx e e_ty (ty e2');
-    mark (A.ECatch (e1', ex, e2')) e_ty
-  | A.EVar v -> begin
-    match Env.get env v with
-    | Some t ->
-      let+ v' = Bindlib.box_var (Var.translate v) in
-      mark v' t
-    | None ->
-      Errors.raise_spanned_error (Expr.pos e)
-        "Variable %s not found in the current context." (Bindlib.name_of v)
-  end
-  | A.ELit lit as e1 -> Bindlib.box @@ mark_with_uf e1 (lit_type lit)
+    Expr.ecatch e1' ex e2' (uf_mark e_ty)
+  | A.EVar v ->
+    let ty =
+      match Env.get env v with
+      | Some t -> t
+      | None ->
+        Errors.raise_spanned_error (Expr.pos e)
+          "Variable %s not found in the current context." (Bindlib.name_of v)
+    in
+    Expr.evar (Var.translate v) (uf_mark ty)
+  | A.ELit lit -> Expr.elit lit (ty_mark (lit_type lit))
   | A.ETuple (es, None) ->
-    let+ es = bmap (typecheck_expr_bottom_up ctx env) es in
-    mark_with_uf (A.ETuple (es, None)) (TTuple (List.map ty es))
+    let es' = List.map (typecheck_expr_bottom_up ctx env) es in
+    Expr.etuple es' None (ty_mark (TTuple (List.map ty es')))
   | A.ETuple (es, Some s_name) ->
     let tys =
       List.map
         (fun (_, ty) -> ast_to_typ ty)
         (A.StructMap.find s_name ctx.A.ctx_structs)
     in
-    let+ es = bmap2 (typecheck_expr_top_down ctx env) tys es in
-    mark_with_uf (A.ETuple (es, Some s_name)) (TStruct s_name)
-  | A.ETupleAccess (e1, n, s, typs) -> begin
+    let es' = List.map2 (typecheck_expr_top_down ctx env) tys es in
+    Expr.etuple es' (Some s_name) (ty_mark (TStruct s_name))
+  | A.ETupleAccess (e1, n, s, typs) ->
     let utyps = List.map ast_to_typ typs in
     let tuple_ty = match s with None -> TTuple utyps | Some s -> TStruct s in
-    let+ e1 = typecheck_expr_top_down ctx env (unionfind_make tuple_ty) e1 in
-    match List.nth_opt utyps n with
-    | Some t' -> mark (A.ETupleAccess (e1, n, s, typs)) t'
-    | None ->
-      Errors.raise_spanned_error (Marked.get_mark e1).pos
-        "Expression should have a tuple type with at least %d elements but \
-         only has %d"
-        n (List.length typs)
-  end
+    let e1' = typecheck_expr_top_down ctx env (unionfind tuple_ty) e1 in
+    let ty =
+      match List.nth_opt utyps n with
+      | Some t' -> t'
+      | None ->
+        Errors.raise_spanned_error (Marked.get_mark e1').pos
+          "Expression should have a tuple type with at least %d elements but \
+           only has %d"
+          n (List.length typs)
+    in
+    Expr.etupleaccess e1' n s typs (uf_mark ty)
   | A.EInj (e1, n, e_name, ts) ->
     let ts' = List.map ast_to_typ ts in
     let ts_n =
@@ -465,24 +442,24 @@ let rec typecheck_expr_bottom_up :
            has %d"
           n (List.length ts')
     in
-    let+ e1' = typecheck_expr_top_down ctx env ts_n e1 in
-    mark_with_uf (A.EInj (e1', n, e_name, ts)) (TEnum e_name)
+    let e1' = typecheck_expr_top_down ctx env ts_n e1 in
+    Expr.einj e1' n e_name ts (ty_mark (TEnum e_name))
   | A.EMatch (e1, es, e_name) ->
     let enum_cases =
-      List.map (fun e' -> unionfind_make ~pos:e' (TAny (Any.fresh ()))) es
+      List.map (fun e' -> unionfind ~pos:e' (TAny (Any.fresh ()))) es
     in
-    let t_e1 = UnionFind.make (add_pos e1 (TEnum e_name)) in
-    let t_ret = unionfind_make ~pos:e (TAny (Any.fresh ())) in
-    let+ e1' = typecheck_expr_top_down ctx env t_e1 e1
-    and+ es' =
-      bmap2
+    let t_e1 = unionfind ~pos:e1 (TEnum e_name) in
+    let t_ret = unionfind ~pos:e (TAny (Any.fresh ())) in
+    let e1' = typecheck_expr_top_down ctx env t_e1 e1
+    and es' =
+      List.map2
         (fun es' enum_t ->
           typecheck_expr_top_down ctx env
-            (unionfind_make ~pos:es' (TArrow (enum_t, t_ret)))
+            (unionfind ~pos:es' (TArrow (enum_t, t_ret)))
             es')
         es enum_cases
     in
-    mark (A.EMatch (e1', es', e_name)) t_ret
+    Expr.ematch e1' es' e_name (uf_mark t_ret)
   | A.EAbs (binder, taus) ->
     if Bindlib.mbinder_arity binder <> List.length taus then
       Errors.raise_spanned_error (Expr.pos e)
@@ -499,67 +476,62 @@ let rec typecheck_expr_bottom_up :
       let body' = typecheck_expr_bottom_up ctx env body in
       let t_func =
         List.fold_right
-          (fun (_, t_arg) acc -> unionfind_make (TArrow (t_arg, acc)))
-          xstaus (box_ty body')
+          (fun (_, t_arg) acc -> unionfind (TArrow (t_arg, acc)))
+          xstaus (ty body')
       in
-      let+ binder' = Bindlib.bind_mvar xs' body' in
-      mark (A.EAbs (binder', taus)) t_func
+      let binder' = Bindlib.bind_mvar xs' (Expr.Box.inj body') in
+      Expr.eabs binder' taus (uf_mark t_func)
   | A.EApp (e1, args) ->
-    let args' = bmap (typecheck_expr_bottom_up ctx env) args in
-    let t_ret = unionfind_make (TAny (Any.fresh ())) in
+    let args' = List.map (typecheck_expr_bottom_up ctx env) args in
+    let t_ret = unionfind (TAny (Any.fresh ())) in
     let t_func =
       List.fold_right
-        (fun ty_arg acc -> unionfind_make (TArrow (ty_arg, acc)))
-        (Bindlib.unbox (Bindlib.box_apply (List.map ty) args'))
-        t_ret
+        (fun arg acc -> unionfind (TArrow (ty arg, acc)))
+        args' t_ret
     in
-    let+ e1' = typecheck_expr_bottom_up ctx env e1 and+ args' in
+    let e1' = typecheck_expr_bottom_up ctx env e1 in
     unify ctx e (ty e1') t_func;
-    mark (A.EApp (e1', args')) t_ret
-  | A.EOp op as e1 -> Bindlib.box @@ mark e1 (op_type (Marked.mark pos_e op))
+    Expr.eapp e1' args' (uf_mark t_ret)
+  | A.EOp op -> Expr.eop op (uf_mark (op_type (Marked.mark pos_e op)))
   | A.EDefault (excepts, just, cons) ->
     let just' =
-      typecheck_expr_top_down ctx env
-        (unionfind_make ~pos:just (TLit TBool))
-        just
+      typecheck_expr_top_down ctx env (unionfind ~pos:just (TLit TBool)) just
     in
     let cons' = typecheck_expr_bottom_up ctx env cons in
-    let tau = box_ty cons' in
-    let+ just'
-    and+ cons'
-    and+ excepts' =
-      bmap (fun except -> typecheck_expr_top_down ctx env tau except) excepts
+    let tau = ty cons' in
+    let excepts' =
+      List.map
+        (fun except -> typecheck_expr_top_down ctx env tau except)
+        excepts
     in
-    mark (A.EDefault (excepts', just', cons')) tau
+    Expr.edefault excepts' just' cons' (uf_mark tau)
   | A.EIfThenElse (cond, et, ef) ->
     let cond' =
-      typecheck_expr_top_down ctx env
-        (unionfind_make ~pos:cond (TLit TBool))
-        cond
+      typecheck_expr_top_down ctx env (unionfind ~pos:cond (TLit TBool)) cond
     in
     let et' = typecheck_expr_bottom_up ctx env et in
-    let tau = box_ty et' in
-    let+ cond' and+ et' and+ ef' = typecheck_expr_top_down ctx env tau ef in
-    mark (A.EIfThenElse (cond', et', ef')) tau
+    let tau = ty et' in
+    let ef' = typecheck_expr_top_down ctx env tau ef in
+    Expr.eifthenelse cond' et' ef' (uf_mark tau)
   | A.EAssert e1 ->
-    let+ e1' =
-      typecheck_expr_top_down ctx env (unionfind_make ~pos:e1 (TLit TBool)) e1
+    let e1' =
+      typecheck_expr_top_down ctx env (unionfind ~pos:e1 (TLit TBool)) e1
     in
-    mark_with_uf (A.EAssert e1') (TLit TUnit)
+    Expr.eassert e1' (ty_mark (TLit TUnit))
   | A.ErrorOnEmpty e1 ->
-    let+ e1' = typecheck_expr_bottom_up ctx env e1 in
-    mark (A.ErrorOnEmpty e1') (ty e1')
+    let e1' = typecheck_expr_bottom_up ctx env e1 in
+    Expr.eerroronempty e1' (uf_mark (ty e1'))
   | A.EArray es ->
-    let cell_type = unionfind_make (TAny (Any.fresh ())) in
-    let+ es' =
-      bmap
+    let cell_type = unionfind (TAny (Any.fresh ())) in
+    let es' =
+      List.map
         (fun e1 ->
           let e1' = typecheck_expr_bottom_up ctx env e1 in
-          unify ctx e1 cell_type (box_ty e1');
+          unify ctx e1 cell_type (ty e1');
           e1')
         es
     in
-    mark_with_uf (A.EArray es') (TArray cell_type)
+    Expr.earray es' (ty_mark (TArray cell_type))
 
 (** Checks whether the expression can be typed with the provided type *)
 and typecheck_expr_top_down :
@@ -568,7 +540,7 @@ and typecheck_expr_top_down :
     (a, m A.mark) A.gexpr Env.t ->
     unionfind_typ ->
     (a, m A.mark) A.gexpr ->
-    (a, mark) A.gexpr Bindlib.box =
+    (a, mark) A.boxed_gexpr =
  fun ctx env tau e ->
   (* Cli.debug_format "Propagating type %a for naked_expr %a" (format_typ ctx)
      tau (Expr.format ctx) e; *)
@@ -580,83 +552,81 @@ and typecheck_expr_top_down :
     | A.Untyped _ | A.Typed { A.ty = A.TAny, _; _ } -> ()
     | A.Typed { A.ty; _ } -> unify ctx e tau (ast_to_typ ty)
   in
-  let mark e = Marked.mark { uf = tau; pos = pos_e } e in
-  let unify_and_mark tau' f_e =
-    unify ctx e tau' tau;
-    Bindlib.box_apply (Marked.mark { uf = tau; pos = pos_e }) (f_e ())
+  let context_mark = { uf = tau; pos = pos_e } in
+  let uf_mark uf =
+    (* Unify with the supplied type first, and return the mark *)
+    unify ctx e uf tau;
+    { uf; pos = pos_e }
   in
-  let unionfind_make ?(pos = e) t = UnionFind.make (add_pos pos t) in
+  let unionfind ?(pos = e) t = UnionFind.make (add_pos pos t) in
+  let ty_mark ty = uf_mark (unionfind ty) in
   match Marked.unmark e with
-  | A.ELocation loc as e1 -> (
-    let ty =
+  | A.ELocation loc ->
+    let ty_opt =
       match loc with
       | DesugaredScopeVar (v, _) | ScopelangScopeVar v ->
         Env.get_scope_var env (Marked.unmark v)
       | SubScopeVar (scope, _, v) ->
         Env.get_subscope_var env scope (Marked.unmark v)
     in
-    match ty with
-    | Some ty -> unify_and_mark (ast_to_typ ty) (fun () -> Bindlib.box e1)
-    | None ->
-      Errors.raise_spanned_error pos_e "Reference to %a not found"
-        (Expr.format ctx) e)
+    let ty =
+      match ty_opt with
+      | Some ty -> ty
+      | None ->
+        Errors.raise_spanned_error pos_e "Reference to %a not found"
+          (Expr.format ctx) e
+    in
+    Expr.elocation loc (uf_mark (ast_to_typ ty))
   | A.EStruct (s_name, fmap) ->
-    unify_and_mark (unionfind_make (TStruct s_name))
-    @@ fun () ->
-    let+ fmap' =
+    let mark = ty_mark (TStruct s_name) in
+    let str = A.StructMap.find s_name ctx.A.ctx_structs in
+    let fmap' =
       (* This assumes that the fields in fmap and the struct type are already
          ensured to be the same *)
-      List.fold_left
-        (fun fmap' (f_name, f_ty) ->
-          let f_e = A.StructFieldMap.find f_name fmap in
-          let+ fmap'
-          and+ f_e' = typecheck_expr_top_down ctx env (ast_to_typ f_ty) f_e in
-          A.StructFieldMap.add f_name f_e' fmap')
-        (Bindlib.box A.StructFieldMap.empty)
-        (A.StructMap.find s_name ctx.A.ctx_structs)
+      A.StructFieldMap.mapi
+        (fun f_name f_e ->
+          let f_ty = List.assoc f_name str in
+          typecheck_expr_top_down ctx env (ast_to_typ f_ty) f_e)
+        fmap
     in
-    A.EStruct (s_name, fmap')
+    Expr.estruct s_name fmap' mark
   | A.EStructAccess (e_struct, f_name, s_name) ->
-    unify_and_mark
-      (ast_to_typ
-         (List.assoc f_name (A.StructMap.find s_name ctx.A.ctx_structs)))
-    @@ fun () ->
-    let+ e_struct' =
-      typecheck_expr_top_down ctx env (unionfind_make (TStruct s_name)) e_struct
+    let mark =
+      uf_mark
+        (ast_to_typ
+           (List.assoc f_name (A.StructMap.find s_name ctx.A.ctx_structs)))
     in
-    A.EStructAccess (e_struct', f_name, s_name)
+    let e_struct' =
+      typecheck_expr_top_down ctx env (unionfind (TStruct s_name)) e_struct
+    in
+    Expr.estructaccess e_struct' f_name s_name mark
   | A.EEnumInj (e_enum, c_name, e_name) ->
-    unify_and_mark (unionfind_make (TEnum e_name))
-    @@ fun () ->
-    let+ e_enum' =
+    let mark = uf_mark (unionfind (TEnum e_name)) in
+    let e_enum' =
       typecheck_expr_top_down ctx env
         (ast_to_typ (List.assoc c_name (A.EnumMap.find e_name ctx.A.ctx_enums)))
         e_enum
     in
-    A.EEnumInj (e_enum', c_name, e_name)
+    Expr.eenuminj e_enum' c_name e_name mark
   | A.EMatchS (e1, e_name, cases) ->
     let cases_ty = A.EnumMap.find e_name ctx.A.ctx_enums in
-    let t_ret = unionfind_make ~pos:e1 (TAny (Any.fresh ())) in
-    unify_and_mark t_ret
-    @@ fun () ->
-    let+ e1' =
-      typecheck_expr_top_down ctx env (unionfind_make (TEnum e_name)) e1
-    and+ cases' =
-      A.EnumConstructorMap.fold
-        (fun c_name e cases' ->
+    let t_ret = unionfind ~pos:e1 (TAny (Any.fresh ())) in
+    let mark = uf_mark t_ret in
+    let e1' = typecheck_expr_top_down ctx env (unionfind (TEnum e_name)) e1 in
+    let cases' =
+      A.EnumConstructorMap.mapi
+        (fun c_name e ->
           let c_ty = List.assoc c_name cases_ty in
-          let e_ty = unionfind_make ~pos:e (TArrow (ast_to_typ c_ty, t_ret)) in
-          let+ cases' and+ e' = typecheck_expr_top_down ctx env e_ty e in
-          A.EnumConstructorMap.add c_name e' cases')
+          let e_ty = unionfind ~pos:e (TArrow (ast_to_typ c_ty, t_ret)) in
+          typecheck_expr_top_down ctx env e_ty e)
         cases
-        (Bindlib.box A.EnumConstructorMap.empty)
     in
-    A.EMatchS (e1', e_name, cases')
-  | A.ERaise _ as e1 -> Bindlib.box (mark e1)
+    Expr.ematchs e1' e_name cases' mark
+  | A.ERaise ex -> Expr.eraise ex context_mark
   | A.ECatch (e1, ex, e2) ->
-    let+ e1' = typecheck_expr_top_down ctx env tau e1
-    and+ e2' = typecheck_expr_top_down ctx env tau e2 in
-    mark (A.ECatch (e1', ex, e2'))
+    let e1' = typecheck_expr_top_down ctx env tau e1 in
+    let e2' = typecheck_expr_top_down ctx env tau e2 in
+    Expr.ecatch e1' ex e2' context_mark
   | A.EVar v ->
     let tau' =
       match Env.get env v with
@@ -665,26 +635,22 @@ and typecheck_expr_top_down :
         Errors.raise_spanned_error pos_e
           "Variable %s not found in the current context" (Bindlib.name_of v)
     in
-    unify_and_mark tau' @@ fun () -> Bindlib.box_var (Var.translate v)
-  | A.ELit lit as e1 ->
-    unify_and_mark (unionfind_make (lit_type lit))
-    @@ fun () -> Bindlib.box @@ e1
+    Expr.evar (Var.translate v) (uf_mark tau')
+  | A.ELit lit -> Expr.elit lit (ty_mark (lit_type lit))
   | A.ETuple (es, None) ->
-    let tys = List.map (fun _ -> unionfind_make (TAny (Any.fresh ()))) es in
-    unify_and_mark (unionfind_make (TTuple tys))
-    @@ fun () ->
-    let+ es' = bmap2 (typecheck_expr_top_down ctx env) tys es in
-    A.ETuple (es', None)
+    let tys = List.map (fun _ -> unionfind (TAny (Any.fresh ()))) es in
+    let mark = uf_mark (unionfind (TTuple tys)) in
+    let es' = List.map2 (typecheck_expr_top_down ctx env) tys es in
+    Expr.etuple es' None mark
   | A.ETuple (es, Some s_name) ->
     let tys =
       List.map
         (fun (_, ty) -> ast_to_typ ty)
         (A.StructMap.find s_name ctx.A.ctx_structs)
     in
-    unify_and_mark (unionfind_make (TStruct s_name))
-    @@ fun () ->
-    let+ es' = bmap2 (typecheck_expr_top_down ctx env) tys es in
-    A.ETuple (es', Some s_name)
+    let mark = uf_mark (unionfind (TStruct s_name)) in
+    let es' = List.map2 (typecheck_expr_top_down ctx env) tys es in
+    Expr.etuple es' (Some s_name) mark
   | A.ETupleAccess (e1, n, s, typs) ->
     let typs' = List.map ast_to_typ typs in
     let tuple_ty = match s with None -> TTuple typs' | Some s -> TStruct s in
@@ -696,10 +662,9 @@ and typecheck_expr_top_down :
            only has %d"
           n (List.length typs)
     in
-    unify_and_mark t1n
-    @@ fun () ->
-    let+ e1' = typecheck_expr_top_down ctx env (unionfind_make tuple_ty) e1 in
-    A.ETupleAccess (e1', n, s, typs)
+    let mark = uf_mark t1n in
+    let e1' = typecheck_expr_top_down ctx env (unionfind tuple_ty) e1 in
+    Expr.etupleaccess e1' n s typs mark
   | A.EInj (e1, n, e_name, ts) ->
     let ts' = List.map ast_to_typ ts in
     let ts_n =
@@ -710,23 +675,23 @@ and typecheck_expr_top_down :
            has %d"
           n (List.length ts)
     in
-    unify_and_mark (unionfind_make (TEnum e_name))
-    @@ fun () ->
-    let+ e1' = typecheck_expr_top_down ctx env ts_n e1 in
-    A.EInj (e1', n, e_name, ts)
+    let mark = uf_mark (unionfind (TEnum e_name)) in
+    let e1' = typecheck_expr_top_down ctx env ts_n e1 in
+    Expr.einj e1' n e_name ts mark
   | A.EMatch (e1, es, e_name) ->
-    let+ es' =
-      bmap2
+    let es' =
+      List.map2
         (fun es' (_, c_ty) ->
           typecheck_expr_top_down ctx env
-            (unionfind_make ~pos:es' (TArrow (ast_to_typ c_ty, tau)))
+            (unionfind ~pos:es' (TArrow (ast_to_typ c_ty, tau)))
             es')
         es
         (A.EnumMap.find e_name ctx.ctx_enums)
-    and+ e1' =
-      typecheck_expr_top_down ctx env (unionfind_make ~pos:e1 (TEnum e_name)) e1
     in
-    mark (A.EMatch (e1', es', e_name))
+    let e1' =
+      typecheck_expr_top_down ctx env (unionfind ~pos:e1 (TEnum e_name)) e1
+    in
+    Expr.ematch e1' es' e_name context_mark
   | A.EAbs (binder, t_args) ->
     if Bindlib.mbinder_arity binder <> List.length t_args then
       Errors.raise_spanned_error (Expr.pos e)
@@ -735,14 +700,13 @@ and typecheck_expr_top_down :
         (List.length t_args)
     else
       let tau_args = List.map ast_to_typ t_args in
-      let t_ret = unionfind_make (TAny (Any.fresh ())) in
+      let t_ret = unionfind (TAny (Any.fresh ())) in
       let t_func =
         List.fold_right
-          (fun t_arg acc -> unionfind_make (TArrow (t_arg, acc)))
+          (fun t_arg acc -> unionfind (TArrow (t_arg, acc)))
           tau_args t_ret
       in
-      unify_and_mark t_func
-      @@ fun () ->
+      let mark = uf_mark t_func in
       let xs, body = Bindlib.unmbind binder in
       let xs' = Array.map Var.translate xs in
       let env =
@@ -751,66 +715,60 @@ and typecheck_expr_top_down :
           env (Array.to_list xs) tau_args
       in
       let body' = typecheck_expr_top_down ctx env t_ret body in
-      let+ binder' = Bindlib.bind_mvar xs' body' in
-      A.EAbs (binder', t_args)
+      let binder' = Bindlib.bind_mvar xs' (Expr.Box.inj body') in
+      Expr.eabs binder' t_args mark
   | A.EApp (e1, args) ->
-    let t_args =
-      List.map (fun _ -> unionfind_make (TAny (Any.fresh ()))) args
-    in
+    let t_args = List.map (fun _ -> unionfind (TAny (Any.fresh ()))) args in
     let t_func =
       List.fold_right
-        (fun t_arg acc -> unionfind_make (TArrow (t_arg, acc)))
+        (fun t_arg acc -> unionfind (TArrow (t_arg, acc)))
         t_args tau
     in
-    let+ e1' = typecheck_expr_top_down ctx env t_func e1
-    and+ args' = bmap2 (typecheck_expr_top_down ctx env) t_args args in
-    mark (A.EApp (e1', args'))
-  | A.EOp op as e1 ->
-    unify_and_mark (op_type (add_pos e op)) @@ fun () -> Bindlib.box e1
+    let e1' = typecheck_expr_top_down ctx env t_func e1 in
+    let args' = List.map2 (typecheck_expr_top_down ctx env) t_args args in
+    Expr.eapp e1' args' context_mark
+  | A.EOp op -> Expr.eop op (uf_mark (op_type (Marked.mark pos_e op)))
   | A.EDefault (excepts, just, cons) ->
-    let+ cons' = typecheck_expr_top_down ctx env tau cons
-    and+ just' =
-      typecheck_expr_top_down ctx env
-        (unionfind_make ~pos:just (TLit TBool))
-        just
-    and+ excepts' = bmap (typecheck_expr_top_down ctx env tau) excepts in
-    mark (A.EDefault (excepts', just', cons'))
+    let cons' = typecheck_expr_top_down ctx env tau cons in
+    let just' =
+      typecheck_expr_top_down ctx env (unionfind ~pos:just (TLit TBool)) just
+    in
+    let excepts' = List.map (typecheck_expr_top_down ctx env tau) excepts in
+    Expr.edefault excepts' just' cons' context_mark
   | A.EIfThenElse (cond, et, ef) ->
-    let+ et' = typecheck_expr_top_down ctx env tau et
-    and+ ef' = typecheck_expr_top_down ctx env tau ef
-    and+ cond' =
-      typecheck_expr_top_down ctx env
-        (unionfind_make ~pos:cond (TLit TBool))
-        cond
+    let et' = typecheck_expr_top_down ctx env tau et in
+    let ef' = typecheck_expr_top_down ctx env tau ef in
+    let cond' =
+      typecheck_expr_top_down ctx env (unionfind ~pos:cond (TLit TBool)) cond
     in
-    mark (A.EIfThenElse (cond', et', ef'))
+    Expr.eifthenelse cond' et' ef' context_mark
   | A.EAssert e1 ->
-    unify_and_mark (unionfind_make (TLit TUnit))
-    @@ fun () ->
-    let+ e1' =
-      typecheck_expr_top_down ctx env (unionfind_make ~pos:e1 (TLit TBool)) e1
+    let mark = uf_mark (unionfind (TLit TUnit)) in
+    let e1' =
+      typecheck_expr_top_down ctx env (unionfind ~pos:e1 (TLit TBool)) e1
     in
-    A.EAssert e1'
+    Expr.eassert e1' mark
   | A.ErrorOnEmpty e1 ->
-    let+ e1' = typecheck_expr_top_down ctx env tau e1 in
-    mark (A.ErrorOnEmpty e1')
+    let e1' = typecheck_expr_top_down ctx env tau e1 in
+    Expr.eerroronempty e1' context_mark
   | A.EArray es ->
-    let cell_type = unionfind_make (TAny (Any.fresh ())) in
-    unify_and_mark (unionfind_make (TArray cell_type))
-    @@ fun () ->
-    let+ es' = bmap (typecheck_expr_top_down ctx env cell_type) es in
-    A.EArray es'
+    let cell_type = unionfind (TAny (Any.fresh ())) in
+    let mark = uf_mark (unionfind (TArray cell_type)) in
+    let es' = List.map (typecheck_expr_top_down ctx env cell_type) es in
+    Expr.earray es' mark
 
 let wrap ctx f e =
-  try
-    Bindlib.unbox (f e)
-    (* We need to unbox here, because the typing may otherwise be stored in
-       Bindlib closures and not yet applied, and would escape the `try..with` *)
+  try f e
   with Type_error (e, ty1, ty2) -> (
     let bt = Printexc.get_raw_backtrace () in
     try handle_type_error ctx e ty1 ty2
     with e -> Printexc.raise_with_backtrace e bt)
 
+let wrap_expr ctx f e =
+  (* We need to unbox here, because the typing may otherwise be stored in
+     Bindlib closures and not yet applied, and would escape the `try..with` *)
+  wrap ctx (fun e -> Expr.unbox (f e)) e
+
 (** {1 API} *)
 
 let get_ty_mark { uf; pos } = A.Typed { ty = typ_to_ast uf; pos }
@@ -821,20 +779,20 @@ let expr
     (ctx : A.decl_ctx)
     ?(env = Env.empty)
     ?(typ : A.typ option)
-    (e : (a, 'm) A.gexpr) : (a, A.typed A.mark) A.gexpr A.box =
+    (e : (a, 'm) A.gexpr) : (a, A.typed A.mark) A.boxed_gexpr =
   let fty =
     match typ with
     | None -> typecheck_expr_bottom_up ctx env
     | Some typ -> typecheck_expr_top_down ctx env (ast_to_typ typ)
   in
-  Expr.map_marks ~f:get_ty_mark (wrap ctx fty e)
+  Expr.map_marks ~f:get_ty_mark (wrap_expr ctx fty e)
 
 let rec scope_body_expr ctx env ty_out body_expr =
   match body_expr with
   | A.Result e ->
-    let e' = wrap ctx (typecheck_expr_top_down ctx env ty_out) e in
+    let e' = wrap_expr ctx (typecheck_expr_top_down ctx env ty_out) e in
     let e' = Expr.map_marks ~f:get_ty_mark e' in
-    Bindlib.box_apply (fun e -> A.Result e) e'
+    Bindlib.box_apply (fun e -> A.Result e) (Expr.Box.inj e')
   | A.ScopeLet
       {
         scope_let_kind;
@@ -844,8 +802,8 @@ let rec scope_body_expr ctx env ty_out body_expr =
         scope_let_pos;
       } ->
     let ty_e = ast_to_typ scope_let_typ in
-    let e = wrap ctx (typecheck_expr_bottom_up ctx env) e0 in
-    wrap ctx (fun t -> Bindlib.box (unify ctx e0 (ty e) t)) ty_e;
+    let e = wrap_expr ctx (typecheck_expr_bottom_up ctx env) e0 in
+    wrap ctx (fun t -> unify ctx e0 (ty e) t) ty_e;
     (* We could use [typecheck_expr_top_down] rather than this manual
        unification, but we get better messages with this order of the [unify]
        parameters, which keeps location of the type as defined instead of as
@@ -864,7 +822,7 @@ let rec scope_body_expr ctx env ty_out body_expr =
             scope_let_next;
             scope_let_pos;
           })
-      (Expr.map_marks ~f:get_ty_mark e)
+      (Expr.Box.inj (Expr.map_marks ~f:get_ty_mark e))
       scope_let_next
 
 let scope_body ctx env body =
diff --git a/compiler/shared_ast/typing.mli b/compiler/shared_ast/typing.mli
index d1ac76c9..ccead1fd 100644
--- a/compiler/shared_ast/typing.mli
+++ b/compiler/shared_ast/typing.mli
@@ -33,7 +33,7 @@ val expr :
   ?env:'e Env.t ->
   ?typ:typ ->
   (('a, 'm mark) gexpr as 'e) ->
-  ('a, typed mark) gexpr box
+  ('a, typed mark) boxed_gexpr
 (** Infers and marks the types for the given expression. If [typ] is provided,
     it is assumed to be the outer type and used for inference top-down.
 
diff --git a/compiler/surface/desugaring.ml b/compiler/surface/desugaring.ml
index b7b89bc3..eae0a1ff 100644
--- a/compiler/surface/desugaring.ml
+++ b/compiler/surface/desugaring.ml
@@ -124,7 +124,7 @@ let rec translate_expr
     (scope : ScopeName.t)
     (inside_definition_of : Desugared.Ast.ScopeDef.t Marked.pos option)
     (ctxt : Name_resolution.context)
-    (expr : Ast.expression Marked.pos) : Desugared.Ast.expr Bindlib.box =
+    (expr : Ast.expression Marked.pos) : Desugared.Ast.expr boxed =
   let scope_ctxt = ScopeMap.find scope ctxt.scopes in
   let rec_helper = translate_expr scope inside_definition_of ctxt in
   let pos = Marked.get_mark expr in
@@ -145,64 +145,53 @@ let rec translate_expr
         (fun c_uid' tau ->
           if EnumConstructor.compare c_uid c_uid' <> 0 then
             let nop_var = Var.make "_" in
-            Bindlib.unbox
-              (Expr.make_abs [| nop_var |]
-                 (Bindlib.box (ELit (LBool false), emark))
-                 [tau] pos)
+            Expr.make_abs [| nop_var |]
+              (Expr.elit (LBool false) emark)
+              [tau] pos
           else
             let ctxt, binding_var =
               Name_resolution.add_def_local_var ctxt (Marked.unmark binding)
             in
             let e2 = translate_expr scope inside_definition_of ctxt e2 in
-            Bindlib.unbox (Expr.make_abs [| binding_var |] e2 [tau] pos))
+            Expr.make_abs [| binding_var |] e2 [tau] pos)
         (EnumMap.find enum_uid ctxt.enums)
     in
-    Bindlib.box_apply
-      (fun e1_sub -> EMatchS (e1_sub, enum_uid, cases), emark)
+    Expr.ematchs
       (translate_expr scope inside_definition_of ctxt e1_sub)
+      enum_uid cases emark
   | IfThenElse (e_if, e_then, e_else) ->
-    Bindlib.box_apply3
-      (fun e_if e_then e_else -> EIfThenElse (e_if, e_then, e_else), emark)
-      (rec_helper e_if) (rec_helper e_then) (rec_helper e_else)
+    Expr.eifthenelse (rec_helper e_if) (rec_helper e_then) (rec_helper e_else)
+      emark
   | Binop ((op, pos), e1, e2) ->
-    let op_term =
-      Marked.mark (Untyped { pos }) (EOp (Binop (translate_binop op)))
-    in
-    Bindlib.box_apply2
-      (fun e1 e2 -> EApp (op_term, [e1; e2]), emark)
-      (rec_helper e1) (rec_helper e2)
+    let op_term = Expr.eop (Binop (translate_binop op)) (Untyped { pos }) in
+    Expr.eapp op_term [rec_helper e1; rec_helper e2] emark
   | Unop ((op, pos), e) ->
-    let op_term =
-      Marked.mark (Untyped { pos }) (EOp (Unop (translate_unop op)))
-    in
-    Bindlib.box_apply (fun e -> EApp (op_term, [e]), emark) (rec_helper e)
+    let op_term = Expr.eop (Unop (translate_unop op)) (Untyped { pos }) in
+    Expr.eapp op_term [rec_helper e] emark
   | Literal l ->
-    let untyped_term =
+    let lit =
       match l with
-      | LNumber ((Int i, _), None) -> ELit (LInt (Runtime.integer_of_string i))
+      | LNumber ((Int i, _), None) -> LInt (Runtime.integer_of_string i)
       | LNumber ((Int i, _), Some (Percent, _)) ->
-        ELit (LRat Runtime.(decimal_of_string i /& decimal_of_string "100"))
+        LRat Runtime.(decimal_of_string i /& decimal_of_string "100")
       | LNumber ((Dec (i, f), _), None) ->
-        ELit (LRat Runtime.(decimal_of_string (i ^ "." ^ f)))
+        LRat Runtime.(decimal_of_string (i ^ "." ^ f))
       | LNumber ((Dec (i, f), _), Some (Percent, _)) ->
-        ELit
-          (LRat
-             Runtime.(
-               decimal_of_string (i ^ "." ^ f) /& decimal_of_string "100"))
-      | LBool b -> ELit (LBool b)
+        LRat
+          Runtime.(decimal_of_string (i ^ "." ^ f) /& decimal_of_string "100")
+      | LBool b -> LBool b
       | LMoneyAmount i ->
-        ELit
-          (LMoney
-             Runtime.(
-               money_of_cents_integer
-                 ((integer_of_string i.money_amount_units *! integer_of_int 100)
-                 +! integer_of_string i.money_amount_cents)))
+        LMoney
+          Runtime.(
+            money_of_cents_integer
+              ((integer_of_string i.money_amount_units *! integer_of_int 100)
+              +! integer_of_string i.money_amount_cents))
       | LNumber ((Int i, _), Some (Year, _)) ->
-        ELit (LDuration (Runtime.duration_of_numbers (int_of_string i) 0 0))
+        LDuration (Runtime.duration_of_numbers (int_of_string i) 0 0)
       | LNumber ((Int i, _), Some (Month, _)) ->
-        ELit (LDuration (Runtime.duration_of_numbers 0 (int_of_string i) 0))
+        LDuration (Runtime.duration_of_numbers 0 (int_of_string i) 0)
       | LNumber ((Int i, _), Some (Day, _)) ->
-        ELit (LDuration (Runtime.duration_of_numbers 0 0 (int_of_string i)))
+        LDuration (Runtime.duration_of_numbers 0 0 (int_of_string i))
       | LNumber ((Dec (_, _), _), Some ((Year | Month | Day), _)) ->
         Errors.raise_spanned_error pos
           "Impossible to specify decimal amounts of days, months or years"
@@ -213,17 +202,16 @@ let rec translate_expr
         if date.literal_date_day > 31 then
           Errors.raise_spanned_error pos
             "There is an error in this date: the day number is bigger than 31";
-        ELit
-          (LDate
-             (try
-                Runtime.date_of_numbers date.literal_date_year
-                  date.literal_date_month date.literal_date_day
-              with Runtime.ImpossibleDate ->
-                Errors.raise_spanned_error pos
-                  "There is an error in this date, it does not correspond to a \
-                   correct calendar day"))
+        LDate
+          (try
+             Runtime.date_of_numbers date.literal_date_year
+               date.literal_date_month date.literal_date_day
+           with Runtime.ImpossibleDate ->
+             Errors.raise_spanned_error pos
+               "There is an error in this date, it does not correspond to a \
+                correct calendar day")
     in
-    Bindlib.box (untyped_term, emark)
+    Expr.elit lit emark
   | Ident x -> (
     (* first we check whether this is a local var, then we resort to scope-wide
        variables *)
@@ -269,12 +257,12 @@ let rec translate_expr
               (* we take the last state in the chain *)
               Some (List.hd (List.rev states)))
         in
-        Bindlib.box (ELocation (DesugaredScopeVar ((uid, pos), x_state)), emark)
+        Expr.elocation (DesugaredScopeVar ((uid, pos), x_state)) emark
       | None ->
         Name_resolution.raise_unknown_identifier
           "for a local or scope-wide variable" (x, pos))
     | Some uid ->
-      Expr.make_var (uid, emark)
+      Expr.make_var uid emark
       (* the whole box thing is to accomodate for this case *))
   | Dotted (e, c, x) -> (
     match Marked.unmark e with
@@ -289,11 +277,10 @@ let rec translate_expr
       let subscope_var_uid =
         Name_resolution.get_var_uid subscope_real_uid ctxt x
       in
-      Bindlib.box
-        ( ELocation
-            (SubScopeVar
-               (subscope_real_uid, (subscope_uid, pos), (subscope_var_uid, pos))),
-          emark )
+      Expr.elocation
+        (SubScopeVar
+           (subscope_real_uid, (subscope_uid, pos), (subscope_var_uid, pos)))
+        emark
     | _ -> (
       (* In this case e.x is the struct field x access of expression e *)
       let e = translate_expr scope inside_definition_of ctxt e in
@@ -317,7 +304,7 @@ let rec translate_expr
             (StructMap.bindings x_possible_structs)
         else
           let s_uid, f_uid = StructMap.choose x_possible_structs in
-          Bindlib.box_apply (fun e -> EStructAccess (e, f_uid, s_uid), emark) e
+          Expr.estructaccess e f_uid s_uid emark
       | Some c_name -> (
         try
           let c_uid =
@@ -325,19 +312,14 @@ let rec translate_expr
           in
           try
             let f_uid = StructMap.find c_uid x_possible_structs in
-            Bindlib.box_apply
-              (fun e -> EStructAccess (e, f_uid, c_uid), emark)
-              e
+            Expr.estructaccess e f_uid c_uid emark
           with Not_found ->
             Errors.raise_spanned_error pos "Struct %s does not contain field %s"
               (Marked.unmark c_name) (Marked.unmark x)
         with Not_found ->
           Errors.raise_spanned_error (Marked.get_mark c_name)
             "Struct %s has not been defined before" (Marked.unmark c_name))))
-  | FunCall (f, arg) ->
-    Bindlib.box_apply2
-      (fun f arg -> EApp (f, [arg]), emark)
-      (rec_helper f) (rec_helper arg)
+  | FunCall (f, arg) -> Expr.eapp (rec_helper f) [rec_helper arg] emark
   | LetIn (x, e1, e2) ->
     let ctxt, v = Name_resolution.add_def_local_var ctxt (Marked.unmark x) in
     let tau = TAny, Marked.get_mark x in
@@ -346,9 +328,7 @@ let rec translate_expr
         (translate_expr scope inside_definition_of ctxt e2)
         [tau] pos
     in
-    Bindlib.box_apply2
-      (fun fn arg -> EApp (fn, [arg]), emark)
-      fn (rec_helper e1)
+    Expr.eapp fn [rec_helper e1] emark
   | StructLit (s_name, fields) ->
     let s_uid =
       try Desugared.Ast.IdentMap.find (Marked.unmark s_name) ctxt.struct_idmap
@@ -374,9 +354,7 @@ let rec translate_expr
           | None -> ()
           | Some e_field ->
             Errors.raise_multispanned_error
-              [
-                None, Marked.get_mark f_e; None, Expr.pos (Bindlib.unbox e_field);
-              ]
+              [None, Marked.get_mark f_e; None, Expr.pos e_field]
               "The field %a has been defined twice:" StructFieldName.format_t
               f_uid);
           let f_e = translate_expr scope inside_definition_of ctxt f_e in
@@ -392,9 +370,7 @@ let rec translate_expr
             StructFieldName.format_t expected_f)
       expected_s_fields;
 
-    Bindlib.box_apply
-      (fun s_fields -> EStruct (s_uid, s_fields), emark)
-      (LiftStructFieldMap.lift_box s_fields)
+    Expr.estruct s_uid s_fields emark
   | EnumInject (enum, (constructor, pos_constructor), payload) -> (
     let possible_c_uids =
       try Desugared.Ast.IdentMap.find constructor ctxt.constructor_idmap
@@ -424,16 +400,11 @@ let rec translate_expr
         let payload =
           Option.map (translate_expr scope inside_definition_of ctxt) payload
         in
-        Bindlib.box_apply
-          (fun payload ->
-            ( EEnumInj
-                ( (match payload with
-                  | Some e' -> e'
-                  | None -> ELit LUnit, mark_constructor),
-                  c_uid,
-                  e_uid ),
-              emark ))
-          (Bindlib.box_opt payload)
+        Expr.eenuminj
+          (match payload with
+          | Some e' -> e'
+          | None -> Expr.elit LUnit mark_constructor)
+          c_uid e_uid emark
     | Some enum -> (
       try
         (* The path has been fully qualified *)
@@ -445,16 +416,11 @@ let rec translate_expr
           let payload =
             Option.map (translate_expr scope inside_definition_of ctxt) payload
           in
-          Bindlib.box_apply
-            (fun payload ->
-              ( EEnumInj
-                  ( (match payload with
-                    | Some e' -> e'
-                    | None -> ELit LUnit, mark_constructor),
-                    c_uid,
-                    e_uid ),
-                emark ))
-            (Bindlib.box_opt payload)
+          Expr.eenuminj
+            (match payload with
+            | Some e' -> e'
+            | None -> Expr.elit LUnit mark_constructor)
+            c_uid e_uid emark
         with Not_found ->
           Errors.raise_spanned_error pos "Enum %s does not contain case %s"
             (Marked.unmark enum) constructor
@@ -467,10 +433,7 @@ let rec translate_expr
       disambiguate_match_and_build_expression scope inside_definition_of ctxt
         cases
     in
-    Bindlib.box_apply2
-      (fun e1 cases_d -> EMatchS (e1, e_uid, cases_d), emark)
-      e1
-      (LiftEnumConstructorMap.lift_box cases_d)
+    Expr.ematchs e1 e_uid cases_d emark
   | TestMatchCase (e1, pattern) ->
     (match snd (Marked.unmark pattern) with
     | None -> ()
@@ -486,21 +449,15 @@ let rec translate_expr
       EnumConstructorMap.mapi
         (fun c_uid' tau ->
           let nop_var = Var.make "_" in
-          Bindlib.unbox
-            (Expr.make_abs [| nop_var |]
-               (Bindlib.box
-                  ( ELit (LBool (EnumConstructor.compare c_uid c_uid' = 0)),
-                    emark ))
-               [tau] pos))
+          Expr.make_abs [| nop_var |]
+            (Expr.elit (LBool (EnumConstructor.compare c_uid c_uid' = 0)) emark)
+            [tau] pos)
         (EnumMap.find enum_uid ctxt.enums)
     in
-    Bindlib.box_apply
-      (fun e -> EMatchS (e, enum_uid, cases), emark)
+    Expr.ematchs
       (translate_expr scope inside_definition_of ctxt e1)
-  | ArrayLit es ->
-    Bindlib.box_apply
-      (fun es -> EArray es, emark)
-      (Bindlib.box_list (List.map rec_helper es))
+      enum_uid cases emark
+  | ArrayLit es -> Expr.earray (List.map rec_helper es) emark
   | CollectionOp
       ( (((Ast.Filter | Ast.Map) as op'), _pos_op'),
         param',
@@ -516,18 +473,14 @@ let rec translate_expr
         [TAny, pos]
         pos
     in
-    Bindlib.box_apply2
-      (fun f_pred collection ->
-        ( EApp
-            ( ( EOp
-                  (match op' with
-                  | Ast.Map -> Binop Map
-                  | Ast.Filter -> Binop Filter
-                  | _ -> assert false (* should not happen *)),
-                emark ),
-              [f_pred; collection] ),
-          emark ))
-      f_pred collection
+    Expr.eapp
+      (Expr.eop
+         (match op' with
+         | Ast.Map -> Binop Map
+         | Ast.Filter -> Binop Filter
+         | _ -> assert false (* should not happen *))
+         emark)
+      [f_pred; collection] emark
   | CollectionOp
       ( ( Ast.Aggregate (Ast.AggregateArgExtremum (max_or_min, pred_typ, init)),
           pos_op' ),
@@ -561,38 +514,28 @@ let rec translate_expr
     in
     let f_pred_var = Var.make "predicate" in
     let f_pred_var_e =
-      Expr.make_var (f_pred_var, Untyped { pos = Marked.get_mark predicate })
+      Expr.make_var f_pred_var (Untyped { pos = Marked.get_mark predicate })
     in
     let acc_var = Var.make "acc" in
-    let acc_var_e = Expr.make_var (acc_var, emark) in
+    let acc_var_e = Expr.make_var acc_var emark in
     let item_var = Var.make "item" in
-    let item_var_e =
-      Expr.make_var (item_var, Marked.get_mark (Bindlib.unbox collection))
-    in
+    let item_var_e = Expr.make_var item_var (Marked.get_mark collection) in
     let fold_body =
-      Bindlib.box_apply3
-        (fun acc_var_e item_var_e f_pred_var_e ->
-          ( EIfThenElse
-              ( ( EApp
-                    ( (EOp (Binop cmp_op), Untyped { pos = pos_op' }),
-                      [
-                        EApp (f_pred_var_e, [acc_var_e]), emark;
-                        EApp (f_pred_var_e, [item_var_e]), emark;
-                      ] ),
-                  emark ),
-                acc_var_e,
-                item_var_e ),
-            emark ))
-        acc_var_e item_var_e f_pred_var_e
+      Expr.eifthenelse
+        (Expr.eapp
+           (Expr.eop (Binop cmp_op) (Untyped { pos = pos_op' }))
+           [
+             Expr.eapp f_pred_var_e [acc_var_e] emark;
+             Expr.eapp f_pred_var_e [item_var_e] emark;
+           ]
+           emark)
+        acc_var_e item_var_e emark
     in
     let fold_f =
       Expr.make_abs [| acc_var; item_var |] fold_body [TAny, pos; TAny, pos] pos
     in
     let fold =
-      Bindlib.box_apply3
-        (fun fold_f collection init ->
-          EApp ((EOp (Ternop Fold), emark), [fold_f; init; collection]), emark)
-        fold_f collection init
+      Expr.eapp (Expr.eop (Ternop Fold) emark) [fold_f; init; collection] emark
     in
     Expr.make_let_in f_pred_var (TAny, pos) f_pred fold pos
   | CollectionOp (op', param', collection, predicate) ->
@@ -605,55 +548,46 @@ let rec translate_expr
       match Marked.unmark op' with
       | Ast.Map | Ast.Filter | Ast.Aggregate (Ast.AggregateArgExtremum _) ->
         assert false (* should not happen *)
-      | Ast.Exists -> Bindlib.box (ELit (LBool false), mark)
-      | Ast.Forall -> Bindlib.box (ELit (LBool true), mark)
+      | Ast.Exists -> Expr.elit (LBool false) mark
+      | Ast.Forall -> Expr.elit (LBool true) mark
       | Ast.Aggregate (Ast.AggregateSum Ast.Integer) ->
-        Bindlib.box (ELit (LInt (Runtime.integer_of_int 0)), mark)
+        Expr.elit (LInt (Runtime.integer_of_int 0)) mark
       | Ast.Aggregate (Ast.AggregateSum Ast.Decimal) ->
-        Bindlib.box (ELit (LRat (Runtime.decimal_of_string "0")), mark)
+        Expr.elit (LRat (Runtime.decimal_of_string "0")) mark
       | Ast.Aggregate (Ast.AggregateSum Ast.Money) ->
-        Bindlib.box
-          ( ELit
-              (LMoney
-                 (Runtime.money_of_cents_integer (Runtime.integer_of_int 0))),
-            mark )
+        Expr.elit
+          (LMoney (Runtime.money_of_cents_integer (Runtime.integer_of_int 0)))
+          mark
       | Ast.Aggregate (Ast.AggregateSum Ast.Duration) ->
-        Bindlib.box (ELit (LDuration (Runtime.duration_of_numbers 0 0 0)), mark)
+        Expr.elit (LDuration (Runtime.duration_of_numbers 0 0 0)) mark
       | Ast.Aggregate (Ast.AggregateSum t) ->
         Errors.raise_spanned_error pos
           "It is impossible to sum two values of type %a together"
           SurfacePrint.format_primitive_typ t
       | Ast.Aggregate (Ast.AggregateExtremum (_, _, init)) -> rec_helper init
       | Ast.Aggregate Ast.AggregateCount ->
-        Bindlib.box (ELit (LInt (Runtime.integer_of_int 0)), mark)
+        Expr.elit (LInt (Runtime.integer_of_int 0)) mark
     in
     let acc_var = Var.make "acc" in
     let acc =
-      Expr.make_var (acc_var, Untyped { pos = Marked.get_mark param' })
+      Expr.make_var acc_var (Untyped { pos = Marked.get_mark param' })
     in
     let f_body =
       let make_body (op : binop) =
-        Bindlib.box_apply2
-          (fun predicate acc ->
-            EApp ((EOp (Binop op), mark), [acc; predicate]), emark)
-          (translate_expr scope inside_definition_of ctxt predicate)
-          acc
+        Expr.eapp (Expr.eop (Binop op) mark)
+          [acc; translate_expr scope inside_definition_of ctxt predicate]
+          emark
       in
       let make_extr_body (cmp_op : binop) (t : typ) =
         let tmp_var = Var.make "tmp" in
         let tmp =
-          Expr.make_var (tmp_var, Untyped { pos = Marked.get_mark param' })
+          Expr.make_var tmp_var (Untyped { pos = Marked.get_mark param' })
         in
         Expr.make_let_in tmp_var t
           (translate_expr scope inside_definition_of ctxt predicate)
-          (Bindlib.box_apply2
-             (fun acc tmp ->
-               ( EIfThenElse
-                   ( (EApp ((EOp (Binop cmp_op), mark), [acc; tmp]), emark),
-                     acc,
-                     tmp ),
-                 emark ))
-             acc tmp)
+          (Expr.eifthenelse
+             (Expr.eapp (Expr.eop (Binop cmp_op) mark) [acc; tmp] emark)
+             acc tmp emark)
           pos
       in
       match Marked.unmark op' with
@@ -685,38 +619,33 @@ let rec translate_expr
         let cmp_op = if max_or_min then Gt op_kind else Lt op_kind in
         make_extr_body cmp_op typ
       | Ast.Aggregate Ast.AggregateCount ->
-        Bindlib.box_apply2
-          (fun predicate acc ->
-            ( EIfThenElse
-                ( predicate,
-                  ( EApp
-                      ( (EOp (Binop (Add KInt)), mark),
-                        [
-                          acc;
-                          ( ELit (LInt (Runtime.integer_of_int 1)),
-                            Marked.get_mark predicate );
-                        ] ),
-                    emark ),
-                  acc ),
-              emark ))
-          (translate_expr scope inside_definition_of ctxt predicate)
-          acc
+        let predicate =
+          translate_expr scope inside_definition_of ctxt predicate
+        in
+        Expr.eifthenelse predicate
+          (Expr.eapp
+             (Expr.eop (Binop (Add KInt)) mark)
+             [
+               acc;
+               Expr.elit
+                 (LInt (Runtime.integer_of_int 1))
+                 (Marked.get_mark predicate);
+             ]
+             emark)
+          acc emark
     in
     let f =
       let make_f (t : typ_lit) =
-        Bindlib.box_apply
-          (fun binder ->
-            ( EAbs
-                ( binder,
-                  [
-                    TLit t, Marked.get_mark op';
-                    TAny, pos
-                    (* we put any here because the type of the elements of the
-                       arrays is not always the type of the accumulator; for
-                       instance in AggregateCount. *);
-                  ] ),
-              emark ))
-          (Bindlib.bind_mvar [| acc_var; param |] f_body)
+        Expr.eabs
+          (Expr.bind [| acc_var; param |] f_body)
+          [
+            TLit t, Marked.get_mark op';
+            TAny, pos
+            (* we put any here because the type of the elements of the arrays is
+               not always the type of the accumulator; for instance in
+               AggregateCount. *);
+          ]
+          emark
       in
       match Marked.unmark op' with
       | Ast.Map | Ast.Filter | Ast.Aggregate (Ast.AggregateArgExtremum _) ->
@@ -740,54 +669,46 @@ let rec translate_expr
         assert false (* should not happen *)
       | Ast.Aggregate Ast.AggregateCount -> make_f TInt
     in
-    Bindlib.box_apply3
-      (fun f collection init ->
-        EApp ((EOp (Ternop Fold), emark), [f; init; collection]), emark)
-      f collection init
+    Expr.eapp (Expr.eop (Ternop Fold) emark) [f; init; collection] emark
   | MemCollection (member, collection) ->
     let param_var = Var.make "collection_member" in
-    let param = Expr.make_var (param_var, emark) in
+    let param = Expr.make_var param_var emark in
     let collection = rec_helper collection in
-    let init = Bindlib.box (ELit (LBool false), emark) in
+    let init = Expr.elit (LBool false) emark in
     let acc_var = Var.make "acc" in
-    let acc = Expr.make_var (acc_var, emark) in
+    let acc = Expr.make_var acc_var emark in
     let f_body =
-      Bindlib.box_apply3
-        (fun member acc param ->
-          ( EApp
-              ( (EOp (Binop Or), emark),
-                [EApp ((EOp (Binop Eq), emark), [member; param]), emark; acc] ),
-            emark ))
-        (translate_expr scope inside_definition_of ctxt member)
-        acc param
+      let member = translate_expr scope inside_definition_of ctxt member in
+      Expr.eapp
+        (Expr.eop (Binop Or) emark)
+        [Expr.eapp (Expr.eop (Binop Eq) emark) [member; param] emark; acc]
+        emark
     in
     let f =
-      Bindlib.box_apply
-        (fun binder -> EAbs (binder, [TLit TBool, pos; TAny, pos]), emark)
-        (Bindlib.bind_mvar [| acc_var; param_var |] f_body)
+      Expr.eabs
+        (Expr.bind [| acc_var; param_var |] f_body)
+        [TLit TBool, pos; TAny, pos]
+        emark
     in
-    Bindlib.box_apply3
-      (fun f collection init ->
-        EApp ((EOp (Ternop Fold), emark), [f; init; collection]), emark)
-      f collection init
-  | Builtin IntToDec -> Bindlib.box (EOp (Unop IntToRat), emark)
-  | Builtin MoneyToDec -> Bindlib.box (EOp (Unop MoneyToRat), emark)
-  | Builtin DecToMoney -> Bindlib.box (EOp (Unop RatToMoney), emark)
-  | Builtin Cardinal -> Bindlib.box (EOp (Unop Length), emark)
-  | Builtin GetDay -> Bindlib.box (EOp (Unop GetDay), emark)
-  | Builtin GetMonth -> Bindlib.box (EOp (Unop GetMonth), emark)
-  | Builtin GetYear -> Bindlib.box (EOp (Unop GetYear), emark)
-  | Builtin FirstDayOfMonth -> Bindlib.box (EOp (Unop FirstDayOfMonth), emark)
-  | Builtin LastDayOfMonth -> Bindlib.box (EOp (Unop LastDayOfMonth), emark)
-  | Builtin RoundMoney -> Bindlib.box (EOp (Unop RoundMoney), emark)
-  | Builtin RoundDecimal -> Bindlib.box (EOp (Unop RoundDecimal), emark)
+    Expr.eapp (Expr.eop (Ternop Fold) emark) [f; init; collection] emark
+  | Builtin IntToDec -> Expr.eop (Unop IntToRat) emark
+  | Builtin MoneyToDec -> Expr.eop (Unop MoneyToRat) emark
+  | Builtin DecToMoney -> Expr.eop (Unop RatToMoney) emark
+  | Builtin Cardinal -> Expr.eop (Unop Length) emark
+  | Builtin GetDay -> Expr.eop (Unop GetDay) emark
+  | Builtin GetMonth -> Expr.eop (Unop GetMonth) emark
+  | Builtin GetYear -> Expr.eop (Unop GetYear) emark
+  | Builtin FirstDayOfMonth -> Expr.eop (Unop FirstDayOfMonth) emark
+  | Builtin LastDayOfMonth -> Expr.eop (Unop LastDayOfMonth) emark
+  | Builtin RoundMoney -> Expr.eop (Unop RoundMoney) emark
+  | Builtin RoundDecimal -> Expr.eop (Unop RoundDecimal) emark
 
 and disambiguate_match_and_build_expression
     (scope : ScopeName.t)
     (inside_definition_of : Desugared.Ast.ScopeDef.t Marked.pos option)
     (ctxt : Name_resolution.context)
     (cases : Ast.match_case Marked.pos list) :
-    Desugared.Ast.expr Bindlib.box EnumConstructorMap.t * EnumName.t =
+    Desugared.Ast.expr boxed EnumConstructorMap.t * EnumName.t =
   let create_var = function
     | None -> ctxt, Var.make "_"
     | Some param ->
@@ -798,20 +719,14 @@ and disambiguate_match_and_build_expression
       (c_uid : EnumConstructor.t)
       (e_uid : EnumName.t)
       (ctxt : Name_resolution.context)
-      (case_body : ('a * untyped mark) Bindlib.box)
-      (e_binder : (Desugared.Ast.expr, Desugared.Ast.expr) mbinder box) :
-      'c Bindlib.box =
-    Bindlib.box_apply2
-      (fun e_binder case_body ->
-        Marked.same_mark_as
-          (EAbs
-             ( e_binder,
-               [
-                 EnumConstructorMap.find c_uid
-                   (EnumMap.find e_uid ctxt.Name_resolution.enums);
-               ] ))
-          case_body)
-      e_binder case_body
+      case_body
+      e_binder =
+    Expr.eabs e_binder
+      [
+        EnumConstructorMap.find c_uid
+          (EnumMap.find e_uid ctxt.Name_resolution.enums);
+      ]
+      (Marked.get_mark case_body)
   in
   let bind_match_cases (cases_d, e_uid, curr_index) (case, case_pos) =
     match case with
@@ -837,17 +752,14 @@ and disambiguate_match_and_build_expression
       | None -> ()
       | Some e_case ->
         Errors.raise_multispanned_error
-          [
-            None, Marked.get_mark case.match_case_expr;
-            None, Expr.pos (Bindlib.unbox e_case);
-          ]
+          [None, Marked.get_mark case.match_case_expr; None, Expr.pos e_case]
           "The constructor %a has been matched twice:" EnumConstructor.format_t
           c_uid);
       let ctxt, param_var = create_var (Option.map Marked.unmark binding) in
       let case_body =
         translate_expr scope inside_definition_of ctxt case.Ast.match_case_expr
       in
-      let e_binder = Bindlib.bind_mvar [| param_var |] case_body in
+      let e_binder = Expr.bind [| param_var |] case_body in
       let case_expr = bind_case_body c_uid e_uid ctxt case_body e_binder in
       EnumConstructorMap.add c_uid case_expr cases_d, Some e_uid, curr_index + 1
     | Ast.WildCard match_case_expr -> (
@@ -898,7 +810,7 @@ and disambiguate_match_and_build_expression
         let case_body =
           translate_expr scope inside_definition_of ctxt match_case_expr
         in
-        let e_binder = Bindlib.bind_mvar [| payload_var |] case_body in
+        let e_binder = Expr.bind [| payload_var |] case_body in
 
         (* For each missing cases, binds the wildcard payload. *)
         EnumConstructorMap.fold
@@ -924,22 +836,16 @@ and disambiguate_match_and_build_expression
     this precondition has to be appended to the justifications of each
     definition in the subscope use. This is what this function does. *)
 let merge_conditions
-    (precond : Desugared.Ast.expr Bindlib.box option)
-    (cond : Desugared.Ast.expr Bindlib.box option)
-    (default_pos : Pos.t) : Desugared.Ast.expr Bindlib.box =
+    (precond : Desugared.Ast.expr boxed option)
+    (cond : Desugared.Ast.expr boxed option)
+    (default_pos : Pos.t) : Desugared.Ast.expr boxed =
   match precond, cond with
   | Some precond, Some cond ->
-    let op_term = EOp (Binop And), Marked.get_mark (Bindlib.unbox cond) in
-    Bindlib.box_apply2
-      (fun precond cond ->
-        EApp (op_term, [precond; cond]), Marked.get_mark cond)
-      precond cond
-  | Some precond, None ->
-    Bindlib.box_apply
-      (fun precond -> Marked.unmark precond, Untyped { pos = default_pos })
-      precond
+    let op_term = Expr.eop (Binop And) (Marked.get_mark cond) in
+    Expr.eapp op_term [precond; cond] (Marked.get_mark cond)
+  | Some precond, None -> Marked.unmark precond, Untyped { pos = default_pos }
   | None, Some cond -> cond
-  | None, None -> Bindlib.box (ELit (LBool true), Untyped { pos = default_pos })
+  | None, None -> Expr.elit (LBool true) (Untyped { pos = default_pos })
 
 (** Translates a surface definition into condition into a desugared {!type:
     Desugared.Ast.rule} *)
@@ -949,7 +855,7 @@ let process_default
     (def_key : Desugared.Ast.ScopeDef.t Marked.pos)
     (rule_id : Desugared.Ast.RuleName.t)
     (param_uid : Desugared.Ast.expr Var.t Marked.pos option)
-    (precond : Desugared.Ast.expr Bindlib.box option)
+    (precond : Desugared.Ast.expr boxed option)
     (exception_situation : Desugared.Ast.exception_situation)
     (label_situation : Desugared.Ast.label_situation)
     (just : Ast.expression Marked.pos option)
@@ -971,12 +877,10 @@ let process_default
        match Marked.unmark def_key_typ, param_uid with
        | TArrow (t_in, _), Some param_uid -> Some (Marked.unmark param_uid, t_in)
        | TArrow _, None ->
-         Errors.raise_spanned_error
-           (Expr.pos (Bindlib.unbox cons))
+         Errors.raise_spanned_error (Expr.pos cons)
            "This definition has a function type but the parameter is missing"
        | _, Some _ ->
-         Errors.raise_spanned_error
-           (Expr.pos (Bindlib.unbox cons))
+         Errors.raise_spanned_error (Expr.pos cons)
            "This definition has a parameter but its type is not a function"
        | _ -> None);
     rule_exception = exception_situation;
@@ -987,7 +891,7 @@ let process_default
 (** Wrapper around {!val: process_default} that performs some name
     disambiguation *)
 let process_def
-    (precond : Desugared.Ast.expr Bindlib.box option)
+    (precond : Desugared.Ast.expr boxed option)
     (scope_uid : ScopeName.t)
     (ctxt : Name_resolution.context)
     (prgm : Desugared.Ast.program)
@@ -1075,7 +979,7 @@ let process_def
 
 (** Translates a {!type: Surface.Ast.rule} from the surface language *)
 let process_rule
-    (precond : Desugared.Ast.expr Bindlib.box option)
+    (precond : Desugared.Ast.expr boxed option)
     (scope : ScopeName.t)
     (ctxt : Name_resolution.context)
     (prgm : Desugared.Ast.program)
@@ -1085,7 +989,7 @@ let process_rule
 
 (** Translates assertions *)
 let process_assert
-    (precond : Desugared.Ast.expr Bindlib.box option)
+    (precond : Desugared.Ast.expr boxed option)
     (scope_uid : ScopeName.t)
     (ctxt : Name_resolution.context)
     (prgm : Desugared.Ast.program)
@@ -1107,12 +1011,9 @@ let process_assert
   let ass =
     match precond with
     | Some precond ->
-      Bindlib.box_apply2
-        (fun precond ass ->
-          ( EIfThenElse
-              (precond, ass, Marked.same_mark_as (ELit (LBool true)) precond),
-            Marked.get_mark precond ))
-        precond ass
+      Expr.eifthenelse precond ass
+        (Expr.elit (LBool true) (Marked.get_mark precond))
+        (Marked.get_mark precond)
     | None -> ass
   in
   let new_scope =
diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index 6f9ca9f9..d6020472 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -312,7 +312,7 @@ let rec generate_verification_conditions_scope_body_expr
            the subscope so we just ought to verify only that the exceptions
            overlap. *)
         let e =
-          Bindlib.unbox (Expr.remove_logging_calls scope_let.scope_let_expr)
+          Expr.unbox (Expr.remove_logging_calls scope_let.scope_let_expr)
         in
         let e = match_and_ignore_outer_reentrant_default ctx e in
         let vc_confl, vc_confl_typs =
diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml
index ce3b80ef..93609da4 100644
--- a/compiler/verification/z3backend.real.ml
+++ b/compiler/verification/z3backend.real.ml
@@ -427,18 +427,15 @@ let rec translate_op (ctx : context) (op : operator) (args : 'm expr list) :
       match args with
       | [e1; e2; e3] -> e1, e2, e3
       | _ ->
-        failwith
-          (Format.asprintf
-             "[Z3 encoding] Ill-formed ternary operator application: %a"
-             (Shared_ast.Expr.format ctx.ctx_decl)
-             ( EApp
-                 ( (EOp op, Untyped { pos = Pos.no_pos }),
-                   List.map
-                     (fun arg -> Bindlib.unbox (Shared_ast.Expr.untype arg))
-                     args ),
-               Untyped { pos = Pos.no_pos } ))
+        Format.kasprintf failwith
+          "[Z3 encoding] Ill-formed ternary operator application: %a"
+          (Shared_ast.Expr.format ctx.ctx_decl)
+          (Shared_ast.Expr.eapp
+             (Shared_ast.Expr.eop op (Untyped { pos = Pos.no_pos }))
+             (List.map Shared_ast.Expr.untype args)
+             (Untyped { pos = Pos.no_pos })
+          |> Shared_ast.Expr.unbox)
     in
-
     failwith "[Z3 encoding] ternary operator application not supported"
   | Binop bop -> (
     (* Special case for GetYear comparisons *)
@@ -520,17 +517,14 @@ let rec translate_op (ctx : context) (op : operator) (args : 'm expr list) :
           let ctx, e2 = translate_expr ctx e2 in
           ctx, e1, e2
         | _ ->
-          failwith
-            (Format.asprintf
-               "[Z3 encoding] Ill-formed binary operator application: %a"
-               (Shared_ast.Expr.format ctx.ctx_decl)
-               ( EApp
-                   ( (EOp op, Untyped { pos = Pos.no_pos }),
-                     List.map
-                       (fun arg ->
-                         arg |> Shared_ast.Expr.untype |> Bindlib.unbox)
-                       args ),
-                 Untyped { pos = Pos.no_pos } ))
+          Format.kasprintf failwith
+            "[Z3 encoding] Ill-formed binary operator application: %a"
+            (Shared_ast.Expr.format ctx.ctx_decl)
+            (Shared_ast.Expr.eapp
+               (Shared_ast.Expr.eop op (Untyped { pos = Pos.no_pos }))
+               (List.map Shared_ast.Expr.untype args)
+               (Untyped { pos = Pos.no_pos })
+            |> Shared_ast.Expr.unbox)
       in
 
       match bop with
@@ -573,16 +567,14 @@ let rec translate_op (ctx : context) (op : operator) (args : 'm expr list) :
       match args with
       | [e1] -> translate_expr ctx e1
       | _ ->
-        failwith
-          (Format.asprintf
-             "[Z3 encoding] Ill-formed unary operator application: %a"
-             (Shared_ast.Expr.format ctx.ctx_decl)
-             ( EApp
-                 ( (EOp op, Untyped { pos = Pos.no_pos }),
-                   List.map
-                     (fun arg -> arg |> Shared_ast.Expr.untype |> Bindlib.unbox)
-                     args ),
-               Untyped { pos = Pos.no_pos } ))
+        Format.kasprintf failwith
+          "[Z3 encoding] Ill-formed unary operator application: %a"
+          (Shared_ast.Expr.format ctx.ctx_decl)
+          (Shared_ast.Expr.eapp
+             (Shared_ast.Expr.eop op (Untyped { pos = Pos.no_pos }))
+             (List.map Shared_ast.Expr.untype args)
+             (Untyped { pos = Pos.no_pos })
+          |> Shared_ast.Expr.unbox)
     in
 
     match uop with