diff --git a/src/whyml/mlw_dtree.ml b/src/whyml/mlw_dtree.ml
index e948e22f0bd6f93744cf0adaa92e07e29a1d4708..e615319e0428af4fbed8211db8cce386257b6d2b 100644
--- a/src/whyml/mlw_dtree.ml
+++ b/src/whyml/mlw_dtree.ml
@@ -61,7 +61,7 @@ type dinvariant = Ptree.lexpr option
 
 type dexpr = {
   de_desc : dexpr_desc;
-  de_type : dity;
+  de_type : dvty;
   de_lab  : Ident.Slab.t;
   de_loc  : loc;
 }
@@ -93,6 +93,6 @@ and dexpr_desc =
   | DEghost of dexpr
   | DEany of dtype_c
 
-and drecfun = loc * ident * ghost * dity * dlambda
+and drecfun = loc * ident * ghost * dvty * dlambda
 
 and dlambda = dbinder list * dvariant list * dpre * dexpr * dpost * dxpost
diff --git a/src/whyml/mlw_dty.ml b/src/whyml/mlw_dty.ml
index a3e1f16cd76e446d2f9e54dbc679fc1d6f4116ae..d1f2d13e53dedbcb0654ca0962d214382b902a71 100644
--- a/src/whyml/mlw_dty.ml
+++ b/src/whyml/mlw_dty.ml
@@ -192,58 +192,25 @@ and unify_reg r1 r2 =
     | Rreg (reg1,_), Rreg (reg2,_) when reg_equal reg1 reg2 -> ()
     | _ -> raise Exit
 
-let unify ?(weak=false) d1 d2 =
+let unify ~weak d1 d2 =
   try unify ~weak d1 d2
   with Exit -> raise (TypeMismatch (ity_of_dity d1, ity_of_dity d2))
 
-let ts_arrow =
-  let v = List.map (fun s -> create_tvsymbol (Ident.id_fresh s)) ["a"; "b"] in
-  Ty.create_tysymbol (Ident.id_fresh "arrow") v None
+let unify_weak d1 d2 = unify ~weak:true d1 d2
+let unify d1 d2 = unify ~weak:false d1 d2
 
-let make_arrow_type tyl ty =
-  let arrow ty1 ty2 = ts_app_real ts_arrow [ty1;ty2] in
-  List.fold_right arrow tyl ty
+type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
 
-let rec unify_list d1 el res =
-  let rec check_val loc = function
-    | Dts (ts, _) when ts_equal ts ts_arrow ->
-        Loc.errorm ~loc "This expression is not a first-order value"
-    | Dvar { contents = Dval d } -> check_val loc d
-    | _ -> ()
-  in
-  let unify_loc loc d1 d2 =
-    check_val loc d2;
-    try unify d1 d2 with
-    | TypeMismatch (ity1, ity2) ->
-        Loc.errorm ~loc "This expression has type %a, \
-          but is expected to have type %a"
-        Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
-    | exn -> Loc.error ~loc exn
-  in
-  match d1, el with
-  | Dts (ts, [d1;d2]), ((loc,dity)::el) when ts_equal ts ts_arrow ->
-      (* this is an ugly and overcomplicated way to treat
-         implicit fields in record update expressions *)
-      if Loc.equal loc Loc.dummy_position
-      then (unify_loc loc d1 dity; unify_list d2 el res)
-      else (unify_list d2 el res; unify_loc loc d1 dity)
-  | Dvar { contents = Dval d1 }, _ ->
-      unify_list d1 el res
-  | _ ->
-      unify d1 (make_arrow_type (List.map snd el) res)
-
-let rec vty_of_dity = function
-  | Dvar { contents = Dval d } ->
-      vty_of_dity d
-  | Dts (ts, [d1; d2]) when ts_equal ts ts_arrow ->
-      VTarrow (vty_arrow (vty_value (ity_of_dity d1)) (vty_of_dity d2))
-  | dity ->
-      VTvalue (vty_value (ity_of_dity dity))
+let vty_of_dvty (argl,res) =
+  let add a v = VTarrow (vty_arrow (vty_value (ity_of_dity a)) v) in
+  List.fold_right add argl (VTvalue (vty_value (ity_of_dity res)))
 
 type tvars = dity list
+
 let empty_tvars = []
 
-let add_tvars tvs dity = dity :: tvs
+let add_dity tvs dity = dity :: tvs
+let add_dvty tvs (argl,res) = res :: List.rev_append argl tvs
 
 let tv_in_tvars tv tvs =
   try List.iter (occur_check tv) tvs; false with Exit -> true
@@ -251,7 +218,7 @@ let tv_in_tvars tv tvs =
 let reg_in_tvars tv tvs =
   try List.iter (occur_check_reg tv) tvs; false with Exit -> true
 
-let specialize_scheme tvs dity =
+let specialize_scheme tvs (argl,res) =
   let htvs = Htv.create 17 in
   let hreg = Htv.create 17 in
   let rec specialize = function
@@ -277,7 +244,7 @@ let specialize_scheme tvs dity =
         end
     | Rreg _ as r -> r
   in
-  specialize dity
+  List.map specialize argl, specialize res
 
 (* Specialization of symbols *)
 
@@ -320,11 +287,11 @@ let specialize_vtarrow vars vta =
   let conv vtv = dity_of_vtv htv hreg vars vtv in
   let rec specialize a =
     let arg = conv a.vta_arg in
-    let res = match a.vta_result with
-      | VTvalue v -> conv v
+    let argl,res = match a.vta_result with
+      | VTvalue v -> [], conv v
       | VTarrow a -> specialize a
     in
-    make_arrow_type [arg] res
+    arg::argl, res
   in
   specialize vta
 
@@ -334,7 +301,7 @@ let specialize_psymbol ps =
 let specialize_plsymbol pls =
   let htv = Htv.create 3 and hreg = Hreg.create 3 in
   let conv vtv = dity_of_vtv htv hreg vars_empty vtv in
-  make_arrow_type (List.map conv pls.pl_args) (conv pls.pl_value)
+  List.map conv pls.pl_args, conv pls.pl_value
 
 let dity_of_ty htv hreg vars ty =
   dity_of_ity htv hreg vars (ity_of_ty ty)
@@ -343,4 +310,4 @@ let specialize_lsymbol ls =
   let htv = Htv.create 3 and hreg = Hreg.create 3 in
   let conv ty = dity_of_ty htv hreg vars_empty ty in
   let ty = Util.def_option ty_bool ls.ls_value in
-  make_arrow_type (List.map conv ls.ls_args) (conv ty)
+  List.map conv ls.ls_args, conv ty
diff --git a/src/whyml/mlw_dty.mli b/src/whyml/mlw_dty.mli
index 573533e3d272d0bd8c640ccb8802909d4ad8f344..e3cadf3af7c81f8e0d9b6b741fd4b548edf0bfa2 100644
--- a/src/whyml/mlw_dty.mli
+++ b/src/whyml/mlw_dty.mli
@@ -31,31 +31,29 @@ open Mlw_module
 
 type dreg
 type dity
+type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
 
 type tvars (* a set of type variables *)
 val empty_tvars: tvars
-val add_tvars: tvars -> dity -> tvars
+val add_dity: tvars -> dity -> tvars
+val add_dvty: tvars -> dvty -> tvars
 
-val create_user_type_variable: Ptree.ident -> dity
 val create_type_variable: unit -> dity
+val create_user_type_variable: Ptree.ident -> dity
 val its_app: user:bool -> itysymbol -> dity list -> dity
 val ts_app: tysymbol -> dity list -> dity
 
-val make_arrow_type: dity list -> dity -> dity
-
-val unify: ?weak:bool -> dity -> dity -> unit
-  (** destructive unification, with or without region unification *)
-
-val unify_list: dity -> (Loc.position * dity) list -> dity -> unit
+val unify: dity -> dity -> unit
+val unify_weak: dity -> dity -> unit (* don't unify regions *)
 
 val ity_of_dity: dity -> ity
-val vty_of_dity: dity -> vty
+val vty_of_dvty: dvty -> vty
   (** use with care, only once unification is done *)
 
-val specialize_scheme: tvars -> dity -> dity
+val specialize_scheme: tvars -> dvty -> dvty
 
-val specialize_lsymbol: lsymbol -> dity
+val specialize_lsymbol: lsymbol -> dvty
 val specialize_pvsymbol: pvsymbol -> dity
-val specialize_psymbol: psymbol -> dity
-val specialize_plsymbol: plsymbol -> dity
+val specialize_psymbol: psymbol -> dvty
+val specialize_plsymbol: plsymbol -> dvty
 val specialize_xsymbol: xsymbol -> dity
diff --git a/src/whyml/mlw_typing.ml b/src/whyml/mlw_typing.ml
index ee4c96f324b5ddfffb041756afa5aa7cf27ab0ad..3849ee2e0d0a95eeb110e92f90f386e9155ff71d 100644
--- a/src/whyml/mlw_typing.ml
+++ b/src/whyml/mlw_typing.ml
@@ -91,7 +91,7 @@ let () = Exn_printer.register (fun fmt e -> match e with
 
 type denv = {
   uc     : module_uc;
-  locals : (tvars * dity) Mstr.t;
+  locals : (tvars * dvty) Mstr.t;
   tvars  : tvars;
   uloc   : Ptree.loc option;
 }
@@ -167,16 +167,19 @@ let dity_bool = ts_app ts_bool []
 let dity_unit = ts_app ts_unit []
 let dity_mark = ts_app ts_mark []
 
-let unify_loc loc fn_unify x1 x2 =
-  try fn_unify x1 x2 with
-    | TypeMismatch (ity1,ity2) ->
-        errorm ~loc "This expression has type %a, \
-          but is expected to have type %a"
-        Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
-    | exn -> error ~loc exn
+let unify_loc unify_fn loc x1 x2 = try unify_fn x1 x2 with
+  | TypeMismatch (ity1,ity2) -> errorm ~loc 
+      "This expression has type %a, but is expected to have type %a"
+      Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
+  | exn -> error ~loc exn
 
-let expected_type ?(weak=false) e dity =
-  unify_loc e.de_loc (unify ~weak) dity e.de_type
+let expected_type { de_loc = loc ; de_type = (argl,res) } dity =
+  if argl <> [] then errorm ~loc "This expression is not a first-order value";
+  unify_loc unify loc dity res
+
+let expected_type_weak { de_loc = loc ; de_type = (argl,res) } dity =
+  if argl <> [] then errorm ~loc "This expression is not a first-order value";
+  unify_loc unify_weak loc dity res
 
 let rec extract_labels labs loc e = match e.Ptree.expr_desc with
   | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (Slab.add s labs) loc e
@@ -244,24 +247,24 @@ let mk_var e =
 let mk_id s loc =
   { id = s; id_loc = loc; id_lab = [] }
 
-let mk_dexpr desc dity loc labs =
-  { de_desc = desc; de_type = dity; de_loc = loc; de_lab = labs }
+let mk_dexpr desc dvty loc labs =
+  { de_desc = desc; de_type = dvty; de_loc = loc; de_lab = labs }
 
-let mk_let ~loc ~uloc e (desc,dity) =
-  if test_var e then desc, dity else
+let mk_let ~loc ~uloc e (desc,dvty) =
+  if test_var e then desc, dvty else
   let loc = def_option loc uloc in
-  let e1 = mk_dexpr desc dity loc Slab.empty in
-  DElet (mk_id "q" loc, false, e, e1), dity
+  let e1 = mk_dexpr desc dvty loc Slab.empty in
+  DElet (mk_id "q" loc, false, e, e1), dvty
 
 (* patterns *)
 
 let add_var id dity denv =
-  let tvars = add_tvars denv.tvars dity in
-  let locals = Mstr.add id.id (tvars,dity) denv.locals in
+  let tvars = add_dity denv.tvars dity in
+  let locals = Mstr.add id.id (tvars,([],dity)) denv.locals in
   { denv with locals = locals; tvars = tvars }
 
 let specialize_qualid uc p = match uc_find_ps uc p with
-  | PV pv -> DEglobal_pv pv, specialize_pvsymbol pv
+  | PV pv -> DEglobal_pv pv, ([],specialize_pvsymbol pv)
   | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
   | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
   | LS ls -> DEglobal_ls ls, specialize_lsymbol ls
@@ -287,8 +290,8 @@ let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
       let dity = create_type_variable () in
       PPvar (Denv.create_user_id id), dity, add_var id dity denv
   | Ptree.PPpapp (q,ppl) ->
-      let sym, dity = specialize_qualid denv.uc q in
-      dpat_app denv loc (mk_dexpr sym dity loc Slab.empty) ppl
+      let sym, dvty = specialize_qualid denv.uc q in
+      dpat_app denv loc (mk_dexpr sym dvty loc Slab.empty) ppl
   | Ptree.PPprec fl when is_pure_record denv.uc fl ->
       let kn = Theory.get_known (get_theory denv.uc) in
       let fl = List.map (find_pure_field denv.uc) fl in
@@ -308,7 +311,7 @@ let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
   | Ptree.PPpor (lpp1, lpp2) ->
       let pp1, dity1, denv = dpattern denv lpp1 in
       let pp2, dity2, denv = dpattern denv lpp2 in
-      unify_loc lpp2.pat_loc unify dity1 dity2;
+      unify_loc unify lpp2.pat_loc dity1 dity2;
       PPor (pp1, pp2), dity1, denv
   | Ptree.PPpas (pp, id) ->
       let pp, dity, denv = dpattern denv pp in
@@ -319,15 +322,18 @@ and dpat_app denv gloc ({ de_loc = loc } as de) ppl =
     let pp, ty, denv = dpattern denv lp in
     pp::ppl, (lp.pat_loc,ty)::tyl, denv in
   let ppl, tyl, denv = List.fold_right add_pp ppl ([],[],denv) in
-  let pp = match de.de_desc with
-    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl)
-    | DEglobal_ls ls -> PPlapp (ls, ppl)
+  let pp, ls = match de.de_desc with
+    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl), pl.pl_ls
+    | DEglobal_ls ls -> Mlw_expr.PPlapp (ls, ppl), ls
     | DEglobal_pv pv -> errorm ~loc "%a is not a constructor" print_pv pv
     | DEglobal_ps ps -> errorm ~loc "%a is not a constructor" print_ps ps
     | _ -> assert false
   in
-  let res = create_type_variable () in
-  Loc.try2 gloc unify_list de.de_type tyl res;
+  let argl, res = de.de_type in
+  if List.length argl <> List.length ppl then error ~loc:gloc
+    (Term.BadArity (ls, List.length argl, List.length ppl));
+  let unify_arg ta (loc,tv) = unify_loc unify loc ta tv in
+  List.iter2 unify_arg argl tyl;
   pp, res, denv
 
 (* specifications *)
@@ -352,22 +358,22 @@ let deff_of_peff uc pe =
 let dxpost uc ql = List.map (fun (q,f) -> find_xsymbol uc q, f) ql
 
 let rec dtype_c denv tyc =
-  let tyv, dity = dtype_v denv tyc.pc_result_type in
+  let tyv, dvty = dtype_v denv tyc.pc_result_type in
   { dc_result = tyv;
     dc_effect = deff_of_peff denv.uc tyc.pc_effect;
     dc_pre    = tyc.pc_pre;
     dc_post   = fst tyc.pc_post;
     dc_xpost  = dxpost denv.uc (snd tyc.pc_post); },
-  dity
+  dvty
 
 and dtype_v denv = function
   | Tpure pty ->
       let dity = dity_of_pty ~user:true denv pty in
-      DSpecV (false,dity), dity
+      DSpecV (false,dity), ([],dity)
   | Tarrow (bl,tyc) ->
       let denv,bl,tyl = dbinders denv bl in
-      let tyc,dity = dtype_c denv tyc in
-      DSpecA (bl,tyc), make_arrow_type tyl dity
+      let tyc,(argl,res) = dtype_c denv tyc in
+      DSpecA (bl,tyc), (tyl @ argl,res)
 
 let dvariant uc = function
   | Some (le, Some q) -> [le, Some (find_variant_ls uc q)]
@@ -381,11 +387,20 @@ let dvariant uc = function
 
 let de_unit ~loc = hidden_ls ~loc (Term.fs_tuple 0)
 
-let de_app loc e el =
-  let res = create_type_variable () in
-  let tyl = List.map (fun a -> (a.de_loc, a.de_type)) el in
-  Loc.try2 loc unify_list e.de_type tyl res;
-  DEapply (e, el), res
+let de_app _loc e el =
+  let argl, res = e.de_type in
+  let rec unify_list argl el = match argl, el with
+    | arg::argl, e::el when Loc.equal e.de_loc Loc.dummy_position ->
+        expected_type e arg; unify_list argl el
+    | arg::argl, e::el ->
+        let res = unify_list argl el in expected_type e arg; res
+    | argl, [] -> argl, res
+    | [], _ when fst e.de_type = [] -> errorm ~loc:e.de_loc
+        "This expression is not a function and cannot be applied"
+    | [], _ -> errorm ~loc:e.de_loc
+        "This function is applied to too many arguments"
+  in
+  DEapply (e, el), unify_list argl el
 
 let rec dexpr denv e =
   let loc = e.Ptree.expr_loc in
@@ -398,9 +413,9 @@ let rec dexpr denv e =
 and de_desc denv loc = function
   | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
       (* local variable *)
-      let tvs, dity = Mstr.find x denv.locals in
-      let dity = specialize_scheme tvs dity in
-      DElocal x, dity
+      let tvs, dvty = Mstr.find x denv.locals in
+      let dvty = specialize_scheme tvs dvty in
+      DElocal x, dvty
   | Ptree.Eident p ->
       specialize_qualid denv.uc p
   | Ptree.Eapply (e1, e2) ->
@@ -409,24 +424,25 @@ and de_desc denv loc = function
       de_app loc (dexpr denv e) el
   | Ptree.Elet (id, gh, e1, e2) ->
       let e1 = dexpr denv e1 in
-      let dity = e1.de_type in
+      let dvty = e1.de_type in
       let tvars = match e1.de_desc with
         | DEfun _ -> denv.tvars
-        | _ -> add_tvars denv.tvars dity in
-      let locals = Mstr.add id.id (tvars, dity) denv.locals in
+        | _ -> add_dvty denv.tvars dvty in
+      let locals = Mstr.add id.id (tvars, dvty) denv.locals in
       let denv = { denv with locals = locals; tvars = tvars } in
       let e2 = dexpr denv e2 in
       DElet (id, gh, e1, e2), e2.de_type
   | Ptree.Eletrec (rdl, e1) ->
       let rdl = dletrec denv rdl in
-      let add_one denv (_, { id = id }, _, dity, _) =
-        { denv with locals = Mstr.add id (denv.tvars, dity) denv.locals } in
+      let add_one denv (_, { id = id }, _, dvty, _) =
+        { denv with locals = Mstr.add id (denv.tvars, dvty) denv.locals } in
       let denv = List.fold_left add_one denv rdl in
       let e1 = dexpr denv e1 in
       DEletrec (rdl, e1), e1.de_type
   | Ptree.Efun (bl, tr) ->
-      let lam, dity = dlambda denv bl None tr in
-      DEfun lam, dity
+      let denv, bl, tyl = dbinders denv bl in
+      let lam, (argl, res) = dlambda denv bl None tr in
+      DEfun lam, (tyl @ argl, res)
   | Ptree.Ecast (e1, pty) ->
       let e1 = dexpr denv e1 in
       expected_type e1 (dity_of_pty ~user:false denv pty);
@@ -443,7 +459,9 @@ and de_desc denv loc = function
       expected_type e1 dity_bool;
       let e2 = dexpr denv e2 in
       let e3 = dexpr denv e3 in
-      expected_type e3 e2.de_type;
+      let res = create_type_variable () in
+      expected_type e2 res;
+      expected_type e3 res;
       DEif (e1, e2, e3), e2.de_type
   | Ptree.Etuple el ->
       let ls = fs_tuple (List.length el) in
@@ -474,8 +492,8 @@ and de_desc denv loc = function
         | Some e -> dexpr denv e
         | None ->
             let loc = Loc.dummy_position in
-            let d, dity = de_app loc (hidden_ls ~loc pj) [e0] in
-            mk_dexpr d dity loc Slab.empty in
+            let d, dvty = de_app loc (hidden_ls ~loc pj) [e0] in
+            mk_dexpr d dvty loc Slab.empty in
       let res = de_app loc (hidden_ls ~loc cs) (List.map get_val pjl) in
       mk_let ~loc ~uloc:denv.uloc e1 res
   | Ptree.Eupdate (e1, fl) ->
@@ -487,8 +505,8 @@ and de_desc denv loc = function
         | Some e -> dexpr denv e
         | None ->
             let loc = Loc.dummy_position in
-            let d, dity = de_app loc (hidden_pl ~loc pj) [e0] in
-            mk_dexpr d dity loc Slab.empty in
+            let d, dvty = de_app loc (hidden_pl ~loc pj) [e0] in
+            mk_dexpr d dvty loc Slab.empty in
       let res = de_app loc (hidden_pl ~loc cs) (List.map get_val pjl) in
       mk_let ~loc ~uloc:denv.uloc e1 res
   | Ptree.Eassign (e1, q, e2) ->
@@ -496,34 +514,37 @@ and de_desc denv loc = function
       let e1 = { expr_desc = Eapply (fl,e1); expr_loc = loc } in
       let e1 = dexpr denv e1 in
       let e2 = dexpr denv e2 in
-      expected_type ~weak:true e2 e1.de_type;
-      DEassign (e1, e2), dity_unit
+      let res = create_type_variable () in
+      expected_type e1 res;
+      expected_type_weak e2 res;
+      DEassign (e1, e2), ([], dity_unit)
   | Ptree.Econstant (ConstInt _ as c) ->
-      DEconstant c, dity_int
+      DEconstant c, ([], dity_int)
   | Ptree.Econstant (ConstReal _ as c) ->
-      DEconstant c, dity_real
+      DEconstant c, ([], dity_real)
   | Ptree.Enot e1 ->
       let e1 = dexpr denv e1 in
       expected_type e1 dity_bool;
-      DEnot e1, dity_bool
+      DEnot e1, ([], dity_bool)
   | Ptree.Elazy (op, e1, e2) ->
       let e1 = dexpr denv e1 in
       let e2 = dexpr denv e2 in
       expected_type e1 dity_bool;
       expected_type e2 dity_bool;
-      DElazy (op, e1, e2), dity_bool
+      DElazy (op, e1, e2), ([], dity_bool)
   | Ptree.Ematch (e1, bl) ->
       let e1 = dexpr denv e1 in
+      let ety = create_type_variable () in
       let res = create_type_variable () in
+      expected_type e1 ety;
       let branch (pp,e) =
         let ppat, dity, denv = dpattern denv pp in
-        unify_loc pp.pat_loc unify e1.de_type dity;
+        unify_loc unify pp.pat_loc ety dity;
         let e = dexpr denv e in
         expected_type e res;
         ppat, e in
-      DEmatch (e1, List.map branch bl), res
+      DEmatch (e1, List.map branch bl), ([], res)
   | Ptree.Eraise (q, e1) ->
-      let res = create_type_variable () in
       let xs = find_xsymbol denv.uc q in
       let dity = specialize_xsymbol xs in
       let e1 = match e1 with
@@ -531,9 +552,11 @@ and de_desc denv loc = function
         | None when ity_equal xs.xs_ity ity_unit -> de_unit ~loc
         | _ -> errorm ~loc "exception argument expected" in
       expected_type e1 dity;
-      DEraise (xs, e1), res
+      DEraise (xs, e1), ([], create_type_variable ())
   | Ptree.Etry (e1, cl) ->
+      let res = create_type_variable () in
       let e1 = dexpr denv e1 in
+      expected_type e1 res;
       let branch (q, id, e) =
         let xs = find_xsymbol denv.uc q in
         let dity = specialize_xsymbol xs in
@@ -541,21 +564,21 @@ and de_desc denv loc = function
           | Some id -> id, add_var id dity denv
           | None -> mk_id "void" loc, denv in
         let e = dexpr denv e in
-        expected_type e e1.de_type;
+        expected_type e res;
         xs, id, e
       in
       let cl = List.map branch cl in
       DEtry (e1, cl), e1.de_type
   | Ptree.Eabsurd ->
-      DEabsurd, create_type_variable ()
+      DEabsurd, ([], create_type_variable ())
   | Ptree.Eassert (ak, lexpr) ->
-      DEassert (ak, lexpr), dity_unit
+      DEassert (ak, lexpr), ([], dity_unit)
   | Ptree.Emark (id, e1) ->
       let e1 = dexpr denv e1 in
       DEmark (id, e1), e1.de_type
   | Ptree.Eany tyc ->
-      let tyc, dity = dtype_c denv tyc in
-      DEany tyc, dity
+      let tyc, dvty = dtype_c denv tyc in
+      DEany tyc, dvty
   | Ptree.Eghost e1 ->
       let e1 = dexpr denv e1 in
       DEghost e1, e1.de_type
@@ -579,24 +602,34 @@ and de_desc denv loc = function
       DEfor (id,efrom,dir,eto,inv,e1), e1.de_type
 
 and dletrec denv rdl =
-  (* add all functions into environment *)
-  let add_one denv (_,id,_,_,_,_) =
-    let res = create_type_variable () in
-    add_var id res denv, res in
-  let denv, tyl = Util.map_fold_left add_one denv rdl in
-  (* then type-check all of them and unify *)
-  let type_one (loc, id, gh, bl, var, tr) res =
-    let lam, dity = dlambda denv bl var tr in
-    Loc.try2 id.id_loc unify dity res;
-    loc, id, gh, dity, lam in
-  List.map2 type_one rdl tyl
+  (* add all functions into the environment *)
+  let add_one denv (_,id,_,bl,_,_) =
+    let argl = List.map (fun _ -> create_type_variable ()) bl in
+    let dvty = argl, create_type_variable () in
+    let tvars = add_dvty denv.tvars dvty in
+    let locals = Mstr.add id.id (tvars, dvty) denv.locals in
+    { denv with locals = locals; tvars = tvars }, dvty in
+  let denv, dvtyl = Util.map_fold_left add_one denv rdl in
+  (* then unify the binders *)
+  let bind_one (_,_,_,bl,_,_) (argl,res) =
+    let denv,bl,tyl = dbinders denv bl in
+    List.iter2 unify argl tyl;
+    denv,bl,tyl,res in
+  let denvl = List.map2 bind_one rdl dvtyl in
+  (* then type-check the bodies *)
+  let type_one (loc, id, gh, _, var, tr) (denv,bl,tyl,tyv) =
+    let lam, (argl, res) = dlambda denv bl var tr in
+    if argl <> [] then errorm ~loc
+      "The body of a recursive function must be a first-order value";
+    unify_loc unify loc tyv res;
+    loc, id, gh, (tyl, tyv), lam in
+  List.map2 type_one rdl denvl
 
 and dlambda denv bl var (p, e, (q, xq)) =
-  let denv,bl,tyl = dbinders denv bl in
   let e = dexpr denv e in
   let var = dvariant denv.uc var in
   let xq = dxpost denv.uc xq in
-  (bl, var, p, e, q, xq), make_arrow_type tyl e.de_type
+  (bl, var, p, e, q, xq), e.de_type
 
 (** stage 2 *)
 
@@ -704,7 +737,7 @@ let rec get_eff_expr lenv { pp_desc = d; pp_loc = loc } = match d with
       let itya, vtvv =
         try Mls.find (uc_find_ls lenv.mod_uc p) pjm with Not_found ->
           errorm ~loc:(qloc p) "'%a' must be a field name" print_qualid p in
-      let sbs = unify_loc loc (ity_match ity_subst_empty) itya vtv.vtv_ity in
+      let sbs = unify_loc (ity_match ity_subst_empty) loc itya vtv.vtv_ity in
       let mut = Util.option_map (reg_full_inst sbs) vtvv.vtv_mut in
       let ghost = vtv.vtv_ghost || vtvv.vtv_ghost in
       vty_value ~ghost ?mut (ity_full_inst sbs vtvv.vtv_ity)
@@ -790,7 +823,7 @@ and expr_desc lenv loc de = match de.de_desc with
       assert (Mstr.mem x lenv.let_vars);
       begin match Mstr.find x lenv.let_vars with
       | LetV pv -> e_value pv
-      | LetA ps -> e_cast ps (vty_of_dity de.de_type)
+      | LetA ps -> e_cast ps (vty_of_dvty de.de_type)
       end
   | DElet (x, gh, { de_desc = DEfun lam }, de2) ->
       let def = expr_fun lenv x gh lam in
@@ -827,18 +860,18 @@ and expr_desc lenv loc de = match de.de_desc with
   | DEapply (de1, del) ->
       let el = List.map (expr lenv) del in
       begin match de1.de_desc with
-        | DEglobal_pl pls -> e_plapp pls el (ity_of_dity de.de_type)
-        | DEglobal_ls ls  -> e_lapp  ls  el (ity_of_dity de.de_type)
+        | DEglobal_pl pls -> e_plapp pls el (ity_of_dity (snd de.de_type))
+        | DEglobal_ls ls  -> e_lapp  ls  el (ity_of_dity (snd de.de_type))
         | _               -> e_app (expr lenv de1) el
       end
   | DEglobal_pv pv ->
       e_value pv
   | DEglobal_ps ps ->
-      e_cast ps (vty_of_dity de.de_type)
+      e_cast ps (vty_of_dvty de.de_type)
   | DEglobal_pl pl ->
-      e_plapp pl [] (ity_of_dity de.de_type)
+      e_plapp pl [] (ity_of_dity (snd de.de_type))
   | DEglobal_ls ls ->
-      e_lapp ls [] (ity_of_dity de.de_type)
+      e_lapp ls [] (ity_of_dity (snd de.de_type))
   | DEif (de1, de2, de3) ->
       e_if (expr lenv de1) (expr lenv de2) (expr lenv de3)
   | DEassign (de1, de2) ->
@@ -873,9 +906,9 @@ and expr_desc lenv loc de = match de.de_desc with
         | Ptree.Acheck  -> Acheck in
       e_assert ak (create_pre lenv f)
   | DEabsurd ->
-      e_absurd (ity_of_dity de.de_type)
+      e_absurd (ity_of_dity (snd de.de_type))
   | DEraise (xs, de1) ->
-      e_raise xs (expr lenv de1) (ity_of_dity de.de_type)
+      e_raise xs (expr lenv de1) (ity_of_dity (snd de.de_type))
   | DEtry (de1, bl) ->
       let e1 = expr lenv de1 in
       let branch (xs,id,de) =
@@ -918,8 +951,8 @@ and expr_desc lenv loc de = match de.de_desc with
       e_for pv efrom dir eto inv e1
 
 and expr_rec lenv rdl =
-  let step1 lenv (_loc, id, gh, dity, lam) =
-    let vta = match vty_ghostify gh (vty_of_dity dity) with
+  let step1 lenv (_loc, id, gh, dvty, lam) =
+    let vta = match vty_ghostify gh (vty_of_dvty dvty) with
       | VTarrow vta -> vta
       | VTvalue _ -> assert false in
     let ps = create_psymbol (Denv.create_user_id id) vta vars_empty in
diff --git a/tests/test-pgm-jcf.mlx b/tests/test-pgm-jcf.mlx
index c00787e098b4551fa3402ae95d8aa4118641312c..3e5c416c271677748b847adcfd446353436cd2c3 100644
--- a/tests/test-pgm-jcf.mlx
+++ b/tests/test-pgm-jcf.mlx
@@ -5,7 +5,7 @@ module TestWP
     let rec f (x:int) = {} g x {}
        with g (x:int) = {} f x {}
     in
-    f x x
+    f x
 end
 
 (***