diff --git a/.nix/catala.nix b/.nix/catala.nix
index 6a55aef4..78f8ff15 100644
--- a/.nix/catala.nix
+++ b/.nix/catala.nix
@@ -25,6 +25,7 @@
 , zarith_stubs_js
 , cohttp-lwt-unix
 , ppx_expect
+, ocaml-crunch
 }:
 
 buildDunePackage {
diff --git a/compiler/driver.ml b/compiler/driver.ml
index 679287dc..d98b0dd1 100644
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@@ -337,7 +337,8 @@ let driver source_file (options : Cli.options) : int =
                 prgm
             in
             let prgm =
-              Shared_ast.Program.untype @@ Shared_ast.Typing.program prgm
+              Shared_ast.Program.untype
+              @@ Shared_ast.Typing.program ~leave_unresolved:false prgm
             in
             let prgm =
               if options.closure_conversion then (
diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml
index 9709873a..f3e35888 100644
--- a/compiler/lcalc/compile_without_exceptions.ml
+++ b/compiler/lcalc/compile_without_exceptions.ml
@@ -207,7 +207,8 @@ let trans_var ctx (x : 'm D.expr Var.t) : 'm Ast.expr Var.t =
 
   new_
 
-let trans_op : (dcalc, 'a) Op.t -> (lcalc, 'a) Op.t = Operator.translate
+let trans_op : type m. (dcalc, m) Op.t -> (lcalc, m) Op.t =
+ fun op -> Operator.translate None op
 
 let rec trans ctx (e : 'm D.expr) : (lcalc, 'm mark) boxed_gexpr =
   let m = Marked.get_mark e in
diff --git a/compiler/lcalc/from_dcalc.ml b/compiler/lcalc/from_dcalc.ml
index d9d7185a..cc02f9b1 100644
--- a/compiler/lcalc/from_dcalc.ml
+++ b/compiler/lcalc/from_dcalc.ml
@@ -18,4 +18,5 @@ let translate_program_with_exceptions =
   Compile_with_exceptions.translate_program
 
 let translate_program_without_exceptions p =
-  Shared_ast.Typing.program (Compile_without_exceptions.translate_program p)
+  Shared_ast.Typing.program ~leave_unresolved:true
+    (Compile_without_exceptions.translate_program p)
diff --git a/compiler/shared_ast/typing.ml b/compiler/shared_ast/typing.ml
index 8a0b0809..1a12580f 100644
--- a/compiler/shared_ast/typing.ml
+++ b/compiler/shared_ast/typing.ml
@@ -68,11 +68,13 @@ let rec typ_to_ast ~leave_unresolved (ty : unionfind_typ) : A.typ =
         "Internal error: typing at this point could not be resolved"
 
 (* Checks that there are no type variables remaining *)
-(* let rec all_resolved ty = match Marked.unmark (UnionFind.get (UnionFind.find
-   ty)) with | TAny _ -> false | TLit _ | TStruct _ | TEnum _ -> true | TOption
-   t1 | TArray t1 -> all_resolved t1 | TArrow (t1, t2) -> List.for_all
-   all_resolved t1 && all_resolved t2 | TTuple ts -> List.for_all all_resolved
-   ts *)
+let rec all_resolved ty =
+  match Marked.unmark (UnionFind.get (UnionFind.find ty)) with
+  | TAny _ -> false
+  | TLit _ | TStruct _ | TEnum _ -> true
+  | TOption t1 | TArray t1 -> all_resolved t1
+  | TArrow (t1, t2) -> List.for_all all_resolved t1 && all_resolved t2
+  | TTuple ts -> List.for_all all_resolved ts
 
 let rec ast_to_typ (ty : A.typ) : unionfind_typ =
   let ty' =
@@ -525,14 +527,17 @@ and typecheck_expr_top_down :
     when name = Definitions.option_enum && cons = Definitions.some_constr ->
     let cell_type = unionfind (TAny (Any.fresh ())) in
     let mark = uf_mark (unionfind (TOption cell_type)) in
-    let e_enum' = typecheck_expr_top_down ctx env cell_type e_enum in
+    let e_enum' =
+      typecheck_expr_top_down ~leave_unresolved ctx env cell_type e_enum
+    in
     Expr.einj e_enum' cons name mark
   | A.EInj { name; cons; e = e_enum }
     when name = Definitions.option_enum && cons = Definitions.none_constr ->
     let cell_type = unionfind (TAny (Any.fresh ())) in
     let mark = uf_mark (unionfind (TOption cell_type)) in
     let e_enum' =
-      typecheck_expr_top_down ctx env (unionfind (TLit TUnit)) e_enum
+      typecheck_expr_top_down ~leave_unresolved ctx env (unionfind (TLit TUnit))
+        e_enum
     in
     Expr.einj e_enum' cons name mark
   | A.EInj { name; cons; e = e_enum } ->
@@ -554,13 +559,13 @@ and typecheck_expr_top_down :
     in
     let t_ret = TAny (Any.fresh ()) in
     let mark = uf_mark (unionfind ~pos:e t_ret) in
-    let e1' = typecheck_expr_top_down ctx env t_arg e1 in
+    let e1' = typecheck_expr_top_down ~leave_unresolved ctx env t_arg e1 in
     let cases' =
       A.EnumConstructor.MapLabels.merge cases cases_ty ~f:(fun _ e e_ty ->
           match e, e_ty with
           | Some e, Some e_ty ->
             Some
-              (typecheck_expr_top_down ctx env
+              (typecheck_expr_top_down ~leave_unresolved ctx env
                  (unionfind ~pos:e
                     (TArrow ([unionfind ~pos:e e_ty], unionfind ~pos:e t_ret)))
                  e)