diff --git a/src/whyml/mlw_dty.ml b/src/whyml/mlw_dty.ml
index b96e20bc0514ad28e04ed3a3de85c06e4fa415d6..a3e1f16cd76e446d2f9e54dbc679fc1d6f4116ae 100644
--- a/src/whyml/mlw_dty.ml
+++ b/src/whyml/mlw_dty.ml
@@ -205,7 +205,15 @@ let make_arrow_type tyl ty =
   List.fold_right arrow tyl ty
 
 let rec unify_list d1 el res =
-  let unify_loc loc d1 d2 = try unify d1 d2 with
+  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"
diff --git a/src/whyml/mlw_pretty.ml b/src/whyml/mlw_pretty.ml
index b9520b44cfa34dc5e16b540a1865783c552606ca..1b5ad72662c3acfe2068e52f54158043cb202db0 100644
--- a/src/whyml/mlw_pretty.ml
+++ b/src/whyml/mlw_pretty.ml
@@ -307,7 +307,7 @@ and print_enode pri fmt e = match e.e_node with
   | Eabsurd ->
       fprintf fmt "absurd"
   | Eassert (ak,f) ->
-      fprintf fmt "%a@ { %a }" print_ak ak print_term f
+      fprintf fmt "%a { %a }" print_ak ak print_term f
   | Eabstr (e,q,_xq) ->
     (* TODO: print_xpost *)
       fprintf fmt "abstract %a@ { %a }" print_expr e print_post q
@@ -388,17 +388,17 @@ let print_ty_decl fmt ts =
   print_ty_decl fmt ts; forget_tvs_regs ()
 
 let print_data_decl fst fmt (ts,csl) =
-  fprintf fmt "@[<hov 2>%a =@\n@[<hov>%a@]@]"
+  fprintf fmt "@[<hov 2>%a =@ %a@]"
     (print_head fst) ts (print_list newline print_constr) csl;
   forget_tvs_regs ()
 
 let print_val_decl fmt { val_name = lv ; val_spec = tyv } =
-  fprintf fmt "@[<hov 2>val (%a) : @[%a@]@]" print_lv lv print_type_v tyv;
+  fprintf fmt "@[<hov 2>val (%a) :@ %a@]" print_lv lv print_type_v tyv;
   (* FIXME: don't forget global regions *)
   forget_tvs_regs ()
 
 let print_let_decl fmt { let_var = lv ; let_expr = e } =
-  fprintf fmt "@[<hov 2>let %a = @[%a@]@]" print_lv lv print_expr e;
+  fprintf fmt "@[<hov 2>let %a =@ %a@]" print_lv lv print_expr e;
   (* FIXME: don't forget global regions *)
   forget_tvs_regs ()
 
diff --git a/src/whyml/mlw_typing.ml b/src/whyml/mlw_typing.ml
index c9e9275d21e41d2cb0f558d85d54564f4d57b5b9..f1d5ce5145c8f83852954d7c6e8dc2f78253e384 100644
--- a/src/whyml/mlw_typing.ml
+++ b/src/whyml/mlw_typing.ml
@@ -537,7 +537,9 @@ and de_desc denv loc = function
         let id, denv = match id with
           | Some id -> id, add_var id dity denv
           | None -> mk_id "void" loc, denv in
-        xs, id, dexpr denv e
+        let e = dexpr denv e in
+        expected_type e e1.de_type;
+        xs, id, e
       in
       let cl = List.map branch cl in
       DEtry (e1, cl), e1.de_type
@@ -610,10 +612,8 @@ let create_lenv uc = {
 }
 
 let rec dty_of_ty ty = match ty.ty_node with
-  | Ty.Tyvar v ->
-      Typing.create_user_type_var v.tv_name.id_string
-  | Ty.Tyapp (ts, tyl) ->
-      Denv.tyapp ts (List.map dty_of_ty tyl)
+  | Ty.Tyapp (ts, tyl) -> Denv.tyapp ts (List.map dty_of_ty tyl)
+  | Ty.Tyvar v -> Denv.tyuvar v
 
 let create_post lenv x ty f =
   let res = create_vsymbol (id_fresh x) ty in
@@ -820,10 +820,8 @@ and expr_desc lenv loc de = match de.de_desc with
   | DEglobal_ps ps ->
       e_cast ps (vty_of_dity de.de_type)
   | DEglobal_pl pl ->
-      assert (pl.pl_ls.ls_args = []);
       e_plapp pl [] (ity_of_dity de.de_type)
   | DEglobal_ls ls ->
-      assert (ls.ls_args = []);
       e_lapp ls [] (ity_of_dity de.de_type)
   | DEif (de1, de2, de3) ->
       e_if (expr lenv de1) (expr lenv de2) (expr lenv de3)