move everything to type_expect

git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10796 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

3 files changed, 322 insertions, 351 deletions

diff --git a/typing/path.ml b/typing/path.ml
index 009550261..0d8ebc6f1 100644
--- a/typing/path.ml
+++ b/typing/path.ml
@@ -37,10 +37,12 @@ let rec binding_time = function
   | Pdot(p, s, pos) -> binding_time p
   | Papply(p1, p2) -> max (binding_time p1) (binding_time p2)
 
-let rec name = function
+let kfalse x = false
+
+let rec name ?(paren=kfalse) = function
     Pident id -> Ident.name id
-  | Pdot(p, s, pos) -> name p ^ "." ^ s
-  | Papply(p1, p2) -> name p1 ^ "(" ^ name p2 ^ ")"
+  | Pdot(p, s, pos) -> name ~paren p ^ if paren s then ".( " ^ s ^ " )" else s
+  | Papply(p1, p2) -> name ~paren p1 ^ "(" ^ name ~paren p2 ^ ")"
 
 let rec head = function
     Pident id -> id
diff --git a/typing/path.mli b/typing/path.mli
index 96f3e9836..b1f4dd861 100644
--- a/typing/path.mli
+++ b/typing/path.mli
@@ -25,5 +25,6 @@ val binding_time: t -> int
 
 val nopos: int
 
-val name: t -> string
+val name: ?paren:(string -> bool) -> t -> string
+    (* [paren] tells whether a path suffix needs parentheses *)
 val head: t -> Ident.t
diff --git a/typing/typecore.ml b/typing/typecore.ml
index b3fe2f78e..537776ca1 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -134,7 +134,7 @@ let extract_option_type env ty =
   | _ -> assert false
 
 let rec extract_label_names sexp env ty =
-  let ty = repr ty in
+  let ty = expand_head env ty in
   match ty.desc with
   | Tconstr (path, _, _) ->
       let td = Env.find_type path env in
@@ -1249,26 +1249,35 @@ let unify_exp env exp expected_ty =
     unify_exp_types exp.exp_loc env exp.exp_type expected_ty
 
 let rec type_exp env sexp =
+  (* We now delegate everything to type_expect *)
+  type_expect env sexp (newvar ())
+
+(* Typing of an expression with an expected type.
+   This provide better error messages, and allows controlled
+   propagation of return type information.
+   In the principal case, [type_expected'] may be at generic_level.
+ *)
+
+and type_expect ?in_function env sexp ty_expected =
   let loc = sexp.pexp_loc in
+  (* Record the expression type before unifying it with the expected type *)
+  let rue exp =
+    Stypes.record (Stypes.Ti_expr exp);
+    unify_exp env exp (instance ty_expected);
+    exp
+  in
   match sexp.pexp_desc with
   | Pexp_ident lid ->
       begin
         if !Clflags.annotations then begin
           try let (path, annot) = Env.lookup_annot lid env in
-              let rec name_of_path = function
-                | Path.Pident id -> Ident.name id
-                | Path.Pdot(p, s, pos) ->
-                    if Oprint.parenthesized_ident s then
-                      name_of_path p ^ ".( " ^ s ^ " )"
-                    else
-                      name_of_path p ^ "." ^ s
-                | Path.Papply(p1, p2) -> name_of_path p1 ^ "(" ^ name_of_path p2 ^ ")" in
               Stypes.record
-                (Stypes.An_ident (loc, name_of_path path, annot))
+                (Stypes.An_ident (
+                 loc, Path.name ~paren:Oprint.parenthesized_ident path, annot))
           with _ -> ()
         end;
         let (path, desc) = Typetexp.find_value env loc lid in
-        re {
+        rue {
           exp_desc =
             begin match desc.val_kind with
               Val_ivar (_, cl_num) ->
@@ -1290,8 +1299,20 @@ let rec type_exp env sexp =
           exp_type = instance desc.val_type;
           exp_env = env }
       end
+  | Pexp_constant(Const_string s as cst) ->
+      rue {
+        exp_desc = Texp_constant cst;
+        exp_loc = loc;
+        exp_type =
+        (* Terrible hack for format strings *)
+           begin match (repr (expand_head env ty_expected)).desc with
+             Tconstr(path, _, _) when Path.same path Predef.path_format6 ->
+               type_format loc s
+           | _ -> instance Predef.type_string
+           end;
+        exp_env = env }
   | Pexp_constant cst ->
-      re {
+      rue {
         exp_desc = Texp_constant cst;
         exp_loc = loc;
         exp_type = type_constant cst;
@@ -1305,14 +1326,99 @@ let rec type_exp env sexp =
       in
       let (pat_exp_list, new_env, unpacks) =
         type_let env rec_flag spat_sexp_list scp true in
-      let body = type_exp new_env (wrap_unpacks sbody unpacks) in
+      let body =
+        type_expect new_env (wrap_unpacks sbody unpacks) ty_expected in
       re {
         exp_desc = Texp_let(rec_flag, pat_exp_list, body);
         exp_loc = loc;
         exp_type = body.exp_type;
         exp_env = env }
-  | Pexp_function _ ->     (* defined in type_expect *)
-      type_expect env sexp (newvar())
+  | Pexp_function (l, Some default, [spat, sbody]) ->
+      let default_loc = default.pexp_loc in
+      let scases = [
+         {ppat_loc = default_loc;
+          ppat_desc =
+            Ppat_construct
+              (Longident.(Ldot (Lident "*predef*", "Some")),
+               Some {ppat_loc = default_loc; ppat_desc = Ppat_var "*sth*"},
+               false, None)},
+         {pexp_loc = default_loc;
+          pexp_desc = Pexp_ident(Longident.Lident "*sth*")};
+         {ppat_loc = default_loc;
+          ppat_desc = Ppat_construct
+            (Longident.(Ldot (Lident "*predef*", "None")), None, false, None)},
+         default;
+      ] in
+      let smatch = {
+        pexp_loc = loc;
+        pexp_desc =
+          Pexp_match ({
+            pexp_loc = loc;
+            pexp_desc = Pexp_ident(Longident.Lident "*opt*")
+            },
+            scases
+          )
+      } in
+      let sfun = {
+        pexp_loc = loc;
+        pexp_desc =
+         Pexp_function (
+           l, None,
+           [ {ppat_loc = loc;
+              ppat_desc = Ppat_var "*opt*"},
+             {pexp_loc = loc;
+              pexp_desc = Pexp_let(Default, [spat, smatch], sbody);
+             }
+           ]
+         )
+      } in
+      type_expect ?in_function env sfun ty_expected
+  | Pexp_function (l, _, caselist) ->
+      let (loc_fun, ty_fun) =
+        match in_function with Some p -> p
+        | None -> (loc, instance ty_expected)
+      in
+      if !Clflags.principal then begin_def ();
+      let (ty_arg, ty_res) =
+        try filter_arrow env (instance ty_expected) l
+        with Unify _ ->
+          match expand_head env ty_expected with
+            {desc = Tarrow _} as ty ->
+              raise(Error(loc, Abstract_wrong_label(l, ty)))
+          | _ ->
+              raise(Error(loc_fun,
+                          Too_many_arguments (in_function <> None, ty_fun)))
+      in
+      let ty_arg =
+        if is_optional l then
+          let tv = newvar() in
+          begin
+            try unify env ty_arg (type_option tv)
+            with Unify _ -> assert false
+          end;
+          type_option tv
+        else ty_arg
+      in
+      if !Clflags.principal then begin
+        end_def ();
+        generalize_structure ty_arg;
+        generalize_structure ty_res
+      end;
+      let cases, partial =
+        type_cases ~in_function:(loc_fun,ty_fun) env ty_arg ty_res
+          true loc caselist in
+      let not_function ty =
+        let ls, tvar = list_labels env ty in
+        ls = [] && not tvar
+      in
+      if is_optional l && not_function ty_res then
+        Location.prerr_warning (fst (List.hd cases)).pat_loc
+          Warnings.Unerasable_optional_argument;
+      re {
+        exp_desc = Texp_function(cases, partial);
+        exp_loc = loc;
+        exp_type = instance (newgenty (Tarrow(l, ty_arg, ty_res, Cok)));
+        exp_env = env }
   | Pexp_apply(sfunct, sargs) ->
       begin_def (); (* one more level for non-returning functions *)
       if !Clflags.principal then begin_def ();
@@ -1337,7 +1443,7 @@ let rec type_exp env sexp =
       let (args, ty_res) = type_application env funct sargs in
       end_def ();
       unify_var env (newvar()) funct.exp_type;
-      re {
+      rue {
         exp_desc = Texp_apply(funct, args);
         exp_loc = loc;
         exp_type = ty_res;
@@ -1349,50 +1455,69 @@ let rec type_exp env sexp =
           end_def ();
           generalize_structure arg.exp_type;
       end;
-      let ty_res = newvar() in
       let cases, partial =
-        type_cases env arg.exp_type ty_res true loc caselist
+        type_cases env arg.exp_type ty_expected true loc caselist
       in
       re {
         exp_desc = Texp_match(arg, cases, partial);
         exp_loc = loc;
-        exp_type = ty_res;
+        exp_type = instance ty_expected;
         exp_env = env }
   | Pexp_try(sbody, caselist) ->
-      let body = type_exp env sbody in
+      let body = type_expect env sbody ty_expected in
       let cases, _ =
-        type_cases env Predef.type_exn body.exp_type false loc caselist in
+        type_cases env Predef.type_exn ty_expected false loc caselist in
       re {
         exp_desc = Texp_try(body, cases);
         exp_loc = loc;
         exp_type = body.exp_type;
         exp_env = env }
   | Pexp_tuple sexpl ->
-      let expl = List.map (type_exp env) sexpl in
+      let subtypes = List.map (fun _ -> newgenvar ()) sexpl in 
+      let to_unify = newgenty (Ttuple subtypes) in
+      unify_exp_types loc env to_unify ty_expected;
+      let expl = 
+	List.map2 (fun body ty -> type_expect env body ty) sexpl subtypes 
+      in
       re {
         exp_desc = Texp_tuple expl;
         exp_loc = loc;
-        exp_type = newty (Ttuple(List.map (fun exp -> exp.exp_type) expl));
+        exp_type = instance ty_expected;
         exp_env = env }
   | Pexp_construct(lid, sarg, explicit_arity) ->
-      type_construct env loc lid sarg explicit_arity (newvar ())
+      type_construct env loc lid sarg explicit_arity ty_expected
   | Pexp_variant(l, sarg) ->
-      let arg = may_map (type_exp env) sarg in
-      let arg_type = may_map (fun arg -> arg.exp_type) arg in
-      re {
-        exp_desc = Texp_variant(l, arg);
-        exp_loc = loc;
-        exp_type= newty (Tvariant{row_fields = [l, Rpresent arg_type];
-                                  row_more = newvar ();
-                                  row_bound = ();
-                                  row_closed = false;
-                                  row_fixed = false;
-                                  row_name = None});
-        exp_env = env }
+      begin try match sarg, expand_head env ty_expected with
+      | Some sarg, {desc = Tvariant row} ->
+          let row = row_repr row in
+          begin match row_field_repr (List.assoc l row.row_fields) with
+            Rpresent (Some ty) ->
+              let arg = type_argument env sarg ty in
+              re { exp_desc = Texp_variant(l, Some arg);
+                   exp_loc = loc;
+                   exp_type = instance ty_expected;
+                   exp_env = env }
+          | _ -> raise Not_found
+          end
+      | _ -> raise Not_found
+      with Not_found ->
+        let arg = may_map (type_exp env) sarg in
+        let arg_type = may_map (fun arg -> arg.exp_type) arg in
+        rue {
+          exp_desc = Texp_variant(l, arg);
+          exp_loc = loc;
+          exp_type= newty (Tvariant{row_fields = [l, Rpresent arg_type];
+                                    row_more = newvar ();
+                                    row_bound = ();
+                                    row_closed = false;
+                                    row_fixed = false;
+                                    row_name = None});
+          exp_env = env }
+      end
   | Pexp_record(lid_sexp_list, opt_sexp) ->
-      let ty = newvar () in
       let lbl_exp_list =
-        type_label_a_list (type_label_exp true env loc ty) lid_sexp_list in
+        type_label_a_list (type_label_exp true env loc ty_expected)
+          lid_sexp_list in
       let rec check_duplicates seen_pos lid_sexp lbl_exp =
         match (lid_sexp, lbl_exp) with
           ((lid, _) :: rem1, (lbl, _) :: rem2) ->
@@ -1405,6 +1530,7 @@ let rec type_exp env sexp =
         match opt_sexp, lbl_exp_list with
           None, _ -> None
         | Some sexp, (lbl, _) :: _ ->
+            if !Clflags.principal then begin_def ();
             let ty_exp = newvar () in
             let unify_kept lbl =
               if List.for_all (fun (lbl',_) -> lbl'.lbl_pos <> lbl.lbl_pos)
@@ -1413,10 +1539,14 @@ let rec type_exp env sexp =
                 let _, ty_arg1, ty_res1 = instance_label false lbl
                 and _, ty_arg2, ty_res2 = instance_label false lbl in
                 unify env ty_exp ty_res1;
-                unify env ty ty_res2;
+                unify env (instance ty_expected) ty_res2;
                 unify env ty_arg1 ty_arg2
               end in
             Array.iter unify_kept lbl.lbl_all;
+            if !Clflags.principal then begin
+              end_def ();
+              generalize_structure ty_exp
+            end;
             Some(type_expect env sexp ty_exp)
         | _ -> assert false
       in
@@ -1426,7 +1556,7 @@ let rec type_exp env sexp =
       if opt_sexp = None && List.length lid_sexp_list <> num_fields then begin
         let present_indices =
           List.map (fun (lbl, _) -> lbl.lbl_pos) lbl_exp_list in
-        let label_names = extract_label_names sexp env ty in
+        let label_names = extract_label_names sexp env ty_expected in
         let rec missing_labels n = function
             [] -> []
           | lbl :: rem ->
@@ -1441,14 +1571,14 @@ let rec type_exp env sexp =
       re {
         exp_desc = Texp_record(lbl_exp_list, opt_exp);
         exp_loc = loc;
-        exp_type = ty;
+        exp_type = instance ty_expected;
         exp_env = env }
   | Pexp_field(sarg, lid) ->
       let arg = type_exp env sarg in
       let label = Typetexp.find_label env loc lid in
       let (_, ty_arg, ty_res) = instance_label false label in
       unify_exp env arg ty_res;
-      re {
+      rue {
         exp_desc = Texp_field(arg, label);
         exp_loc = loc;
         exp_type = ty_arg;
@@ -1459,32 +1589,34 @@ let rec type_exp env sexp =
         type_label_exp false env loc record.exp_type (lid, snewval) in
       if label.lbl_mut = Immutable then
         raise(Error(loc, Label_not_mutable lid));
-      re {
+      rue {
         exp_desc = Texp_setfield(record, label, newval);
         exp_loc = loc;
         exp_type = instance Predef.type_unit;
         exp_env = env }
   | Pexp_array(sargl) ->
-      let ty = newvar() in
+      let ty = newgenvar() in
+      let to_unify = Predef.type_array ty in
+      unify_exp_types loc env to_unify ty_expected;
       let argl = List.map (fun sarg -> type_expect env sarg ty) sargl in
       re {
         exp_desc = Texp_array argl;
         exp_loc = loc;
-        exp_type = instance (Predef.type_array ty);
+        exp_type = instance ty_expected;
         exp_env = env }
   | Pexp_ifthenelse(scond, sifso, sifnot) ->
-      let cond = type_expect env scond (instance Predef.type_bool) in
+      let cond = type_expect env scond Predef.type_bool in
       begin match sifnot with
         None ->
-          let ifso = type_expect env sifso (instance Predef.type_unit) in
-          re {
+          let ifso = type_expect env sifso Predef.type_unit in
+          rue {
             exp_desc = Texp_ifthenelse(cond, ifso, None);
             exp_loc = loc;
-            exp_type = instance Predef.type_unit;
+            exp_type = ifso.exp_type;
             exp_env = env }
       | Some sifnot ->
-          let ifso = type_exp env sifso in
-          let ifnot = type_expect env sifnot ifso.exp_type in
+          let ifso = type_expect env sifso ty_expected in
+          let ifnot = type_expect env sifnot ty_expected in
           re {
             exp_desc = Texp_ifthenelse(cond, ifso, Some ifnot);
             exp_loc = loc;
@@ -1493,28 +1625,28 @@ let rec type_exp env sexp =
       end
   | Pexp_sequence(sexp1, sexp2) ->
       let exp1 = type_statement env sexp1 in
-      let exp2 = type_exp env sexp2 in
+      let exp2 = type_expect env sexp2 ty_expected in
       re {
         exp_desc = Texp_sequence(exp1, exp2);
         exp_loc = loc;
         exp_type = exp2.exp_type;
         exp_env = env }
   | Pexp_while(scond, sbody) ->
-      let cond = type_expect env scond (instance Predef.type_bool) in
+      let cond = type_expect env scond Predef.type_bool in
       let body = type_statement env sbody in
-      re {
+      rue {
         exp_desc = Texp_while(cond, body);
         exp_loc = loc;
         exp_type = instance Predef.type_unit;
         exp_env = env }
   | Pexp_for(param, slow, shigh, dir, sbody) ->
-      let low = type_expect env slow (instance Predef.type_int) in
-      let high = type_expect env shigh (instance Predef.type_int) in
+      let low = type_expect env slow Predef.type_int in
+      let high = type_expect env shigh Predef.type_int in
       let (id, new_env) =
         Env.enter_value param {val_type = instance Predef.type_int;
                                 val_kind = Val_reg} env in
       let body = type_statement new_env sbody in
-      re {
+      rue {
         exp_desc = Texp_for(id, low, high, dir, body);
         exp_loc = loc;
         exp_type = instance Predef.type_unit;
@@ -1606,14 +1738,14 @@ let rec type_exp env sexp =
             end else
               (type_argument env sarg ty, ty')
       in
-      re {
+      rue {
         exp_desc = arg.exp_desc;
         exp_loc = arg.exp_loc;
         exp_type = ty';
         exp_env = env }
   | Pexp_when(scond, sbody) ->
-      let cond = type_expect env scond (instance Predef.type_bool) in
-      let body = type_exp env sbody in
+      let cond = type_expect env scond Predef.type_bool in
+      let body = type_expect env sbody ty_expected in
       re {
         exp_desc = Texp_when(cond, body);
         exp_loc = loc;
@@ -1693,11 +1825,11 @@ let rec type_exp env sexp =
           | _ ->
               assert false
         in
-          re {
-            exp_desc = exp;
-            exp_loc = loc;
-            exp_type = typ;
-            exp_env = env }
+        rue {
+          exp_desc = exp;
+          exp_loc = loc;
+          exp_type = typ;
+          exp_env = env }
       with Unify _ ->
         raise(Error(e.pexp_loc, Undefined_method (obj.exp_type, met)))
       end
@@ -1707,7 +1839,7 @@ let rec type_exp env sexp =
           None ->
             raise(Error(loc, Virtual_class cl))
         | Some ty ->
-            re {
+            rue {
               exp_desc = Texp_new (cl_path, cl_decl);
               exp_loc = loc;
               exp_type = instance ty;
@@ -1722,7 +1854,7 @@ let rec type_exp env sexp =
             let (path_self, _) =
               Env.lookup_value (Longident.Lident ("self-" ^ cl_num)) env
             in
-            re {
+            rue {
               exp_desc = Texp_setinstvar(path_self, path, newval);
               exp_loc = loc;
               exp_type = instance Predef.type_unit;
@@ -1764,7 +1896,7 @@ let rec type_exp env sexp =
             end
           in
           let modifs = List.map type_override lst in
-          re {
+          rue {
             exp_desc = Texp_override(path_self, modifs);
             exp_loc = loc;
             exp_type = self_ty;
@@ -1774,20 +1906,24 @@ let rec type_exp env sexp =
       end
   | Pexp_letmodule(name, smodl, sbody) ->
       let ty = newvar() in
+      (* remember original level *)
+      begin_def ();
       Ident.set_current_time ty.level;
       let context = Typetexp.narrow () in
       let modl = !type_module env smodl in
       let (id, new_env) = Env.enter_module name modl.mod_type env in
       Ctype.init_def(Ident.current_time());
       Typetexp.widen context;
-      let body = type_exp new_env sbody in
+      let body = type_expect new_env sbody ty_expected in
+      (* go back to original level *)
+      end_def ();
       (* Unification of body.exp_type with the fresh variable ty
          fails if and only if the prefix condition is violated,
          i.e. if generative types rooted at id show up in the
          type body.exp_type.  Thus, this unification enforces the
          scoping condition on "let module". *)
       begin try
-        Ctype.unify new_env body.exp_type ty
+        Ctype.unify_var new_env ty body.exp_type
       with Unify _ ->
         raise(Error(loc, Scoping_let_module(name, body.exp_type)))
       end;
@@ -1797,38 +1933,78 @@ let rec type_exp env sexp =
         exp_type = ty;
         exp_env = env }
   | Pexp_assert (e) ->
-       let cond = type_expect env e (instance Predef.type_bool) in
-       re {
-         exp_desc = Texp_assert (cond);
-         exp_loc = loc;
-         exp_type = instance Predef.type_unit;
-         exp_env = env;
-       }
+      let cond = type_expect env e Predef.type_bool in
+      rue {
+        exp_desc = Texp_assert (cond);
+        exp_loc = loc;
+        exp_type = instance Predef.type_unit;
+        exp_env = env;
+      }
   | Pexp_assertfalse ->
-       re {
-         exp_desc = Texp_assertfalse;
-         exp_loc = loc;
-         exp_type = newvar ();
-         exp_env = env;
-       }
+      re {
+        exp_desc = Texp_assertfalse;
+        exp_loc = loc;
+        exp_type = instance ty_expected;
+        exp_env = env;
+      }
   | Pexp_lazy e ->
-       let arg = type_exp env e in
-       re {
-         exp_desc = Texp_lazy arg;
-         exp_loc = loc;
-         exp_type = instance (Predef.type_lazy_t arg.exp_type);
-         exp_env = env;
-       }
+      let ty = newgenvar () in
+      let to_unify = Predef.type_lazy_t ty in
+      unify_exp_types loc env to_unify ty_expected;
+      let arg = type_expect env e ty in
+      re {
+        exp_desc = Texp_lazy arg;
+        exp_loc = loc;
+        exp_type = instance ty_expected;
+        exp_env = env;
+      }
   | Pexp_object s ->
       let desc, sign, meths = !type_object env loc s in
-      re {
+      rue {
         exp_desc = Texp_object (desc, sign, meths);
         exp_loc = loc;
         exp_type = sign.cty_self;
         exp_env = env;
       }
-  | Pexp_poly _ ->
-      assert false
+  | Pexp_poly(sbody, sty) ->
+      if !Clflags.principal then begin_def ();
+      let ty =
+        match sty with None -> repr ty_expected
+        | Some sty ->
+            let ty = Typetexp.transl_simple_type env false sty in
+            repr ty
+      in
+      if !Clflags.principal then begin
+        end_def ();
+        generalize_structure ty
+      end;
+      if sty <> None then
+        unify_exp_types loc env (instance ty) (instance ty_expected);
+      begin
+        match (expand_head env ty).desc with
+          Tpoly (ty', []) ->
+            let exp = type_expect env sbody ty' in
+            re { exp with exp_type = instance ty }
+        | Tpoly (ty', tl) ->
+            (* One more level to generalize locally *)
+            begin_def ();
+            if !Clflags.principal then begin_def ();
+            let vars, ty'' = instance_poly true tl ty' in
+            if !Clflags.principal then begin
+              end_def ();
+              generalize_structure ty''
+            end;
+            let exp = type_expect env sbody ty'' in
+            end_def ();
+            check_univars env false "method" exp ty_expected vars;
+            re { exp with exp_type = instance ty }
+	| Tvar ->
+	    let exp = type_exp env sbody in
+	    let exp = {exp with exp_type = newty (Tpoly (exp.exp_type, []))} in
+	    unify_exp env exp ty;
+	    re exp
+        | _ -> assert false
+      end
   | Pexp_newtype(name, sbody) ->
       (* Create a fake abstract type declaration for name. *)
       let decl = {
@@ -1843,12 +2019,15 @@ let rec type_exp env sexp =
       in
 
       let ty = newvar () in
+      (* remember original level *)
+      begin_def ();
       Ident.set_current_time ty.level;
       let (id, new_env) = Env.enter_type name decl env in
       Ctype.init_def(Ident.current_time());
 
       let body = type_exp new_env sbody in
-      (* Replace every instance of this type constructor in the resulting type. *)
+      (* Replace every instance of this type constructor in the resulting
+         type. *)
       let seen = Hashtbl.create 8 in
       let rec replace t =
         if Hashtbl.mem seen t.id then ()
@@ -1861,32 +2040,67 @@ let rec type_exp env sexp =
       in
       let ety = Subst.type_expr Subst.identity body.exp_type in
       replace ety;
+      (* back to original level *)
+      end_def ();
+      (* lower the levels of the result type *)
+      (* unify_var env ty ety; *)
 
       (* non-expansive if the body is non-expansive, so we don't introduce
          any new extra node in the typed AST. *)
-      re { body with exp_loc = sexp.pexp_loc; exp_type = ety }
+      rue { body with exp_loc = sexp.pexp_loc; exp_type = ety }
   | Pexp_pack m ->
-      raise (Error (loc, Cannot_infer_signature))
+      let (p, nl, tl) =
+        match Ctype.expand_head env (instance ty_expected) with
+          {desc = Tpackage (p, nl, tl)} ->
+            if !Clflags.principal &&
+              (Ctype.expand_head env ty_expected).level < Btype.generic_level
+            then
+              Location.prerr_warning loc
+                (Warnings.Not_principal "this module packing");
+            (p, nl, tl)
+        | {desc = Tvar} ->
+            raise (Error (loc, Cannot_infer_signature))
+        | _ ->
+            raise (Error (loc, Not_a_packed_module ty_expected))
+      in
+      let context = Typetexp.narrow () in
+      let (modl, tl') = !type_package env m p nl tl in
+      Typetexp.widen context;
+      rue {
+        exp_desc = Texp_pack modl;
+        exp_loc = loc;
+        exp_type = newty (Tpackage (p, nl, tl'));
+        exp_env = env }
   | Pexp_open (lid, e) ->
-      type_exp (!type_open env sexp.pexp_loc lid) e
+      type_expect (!type_open env sexp.pexp_loc lid) e ty_expected
 
-and type_label_exp create env loc ty (lid, sarg) =
+and type_label_exp create env loc ty_expected (lid, sarg) =
+  (* Here also ty_expected may be at generic_level *)
   let label = Typetexp.find_label env sarg.pexp_loc lid in
   begin_def ();
-  if !Clflags.principal then begin_def ();
+  if !Clflags.principal then (begin_def (); begin_def ()) ;
   let (vars, ty_arg, ty_res) = instance_label true label in
   if !Clflags.principal then begin
     end_def ();
+    (* Generalize label information *)
     generalize_structure ty_arg;
     generalize_structure ty_res
   end;
   begin try
-    unify env (instance ty_res) ty
+    unify env (instance ty_res) (instance ty_expected)
   with Unify trace ->
     raise(Error(loc , Label_mismatch(lid, trace)))
   end;
+  (* Instantiate so that we can generalize internal nodes *)
+  let ty_arg = instance ty_arg in
+  if !Clflags.principal then begin
+    end_def ();
+    (* Generalize information merged from ty_expected *)
+    generalize_structure ty_arg
+  end;
   if label.lbl_private = Private then
-    raise(Error(loc, if create then Private_type ty else Private_label (lid, ty)));
+    raise(Error(loc, if create then Private_type ty_expected
+                               else Private_label (lid, ty_expected)));
   let arg =
     let snap = if vars = [] then None else Some (Btype.snapshot ()) in
     let arg = type_argument env sarg ty_arg in
@@ -2185,252 +2399,6 @@ and type_construct env loc lid sarg explicit_arity ty_expected =
     raise(Error(loc, Private_type ty_res));
   { texp with exp_desc = Texp_construct(constr, args)}
 
-(* Typing of an expression with an expected type.
-   Some constructs are treated specially to provide better error messages. *)
-
-and type_expect ?in_function env sexp ty_expected' =
-  let loc = sexp.pexp_loc in
-  let ty_expected = instance ty_expected' in
-  match sexp.pexp_desc with
-    Pexp_constant(Const_string s as cst) ->
-      let exp =
-        re {
-          exp_desc = Texp_constant cst;
-          exp_loc = loc;
-          exp_type =
-            (* Terrible hack for format strings *)
-            begin match (repr (expand_head env ty_expected)).desc with
-              Tconstr(path, _, _) when Path.same path Predef.path_format6 ->
-                type_format loc s
-            | _ -> instance Predef.type_string
-            end;
-          exp_env = env } in
-      unify_exp env exp ty_expected;
-      exp
-  | Pexp_construct(lid, sarg, explicit_arity) ->
-      type_construct env loc lid sarg explicit_arity ty_expected'
-  | Pexp_variant(l, Some sarg) ->
-      begin try match expand_head env ty_expected' with
-      | {desc = Tvariant row} ->
-          let row = row_repr row in
-          begin match row_field_repr (List.assoc l row.row_fields) with
-            Rpresent (Some ty) ->
-              let arg = type_argument env sarg ty in
-              re { exp_desc = Texp_variant(l, Some arg);
-                   exp_loc = loc;
-                   exp_type = ty_expected;
-                   exp_env = env }
-          | _ -> raise Not_found
-          end
-      | _ -> raise Not_found
-      with Not_found ->
-        let exp = type_exp env sexp in
-        unify_exp env exp ty_expected;
-        exp
-      end
-  | Pexp_let(rec_flag, spat_sexp_list, sbody) ->
-      let (pat_exp_list, new_env, unpacks) =
-        type_let env rec_flag spat_sexp_list None true in
-      let body =
-        type_expect new_env (wrap_unpacks sbody unpacks) ty_expected in
-      re {
-        exp_desc = Texp_let(rec_flag, pat_exp_list, body);
-        exp_loc = loc;
-        exp_type = body.exp_type;
-        exp_env = env }
-  | Pexp_sequence(sexp1, sexp2) ->
-      let exp1 = type_statement env sexp1 in
-      let exp2 = type_expect env sexp2 ty_expected in
-      re {
-        exp_desc = Texp_sequence(exp1, exp2);
-        exp_loc = loc;
-        exp_type = exp2.exp_type;
-        exp_env = env }
-  | Pexp_function (l, Some default, [spat, sbody]) ->
-      let default_loc = default.pexp_loc in
-      let scases = [
-         {ppat_loc = default_loc;
-          ppat_desc =
-            Ppat_construct
-              (Longident.(Ldot (Lident "*predef*", "Some")),
-               Some {ppat_loc = default_loc; ppat_desc = Ppat_var "*sth*"},
-               false, None)},
-         {pexp_loc = default_loc;
-          pexp_desc = Pexp_ident(Longident.Lident "*sth*")};
-         {ppat_loc = default_loc;
-          ppat_desc = Ppat_construct
-            (Longident.(Ldot (Lident "*predef*", "None")), None, false, None)},
-         default;
-      ] in
-      let smatch = {
-        pexp_loc = loc;
-        pexp_desc =
-          Pexp_match ({
-            pexp_loc = loc;
-            pexp_desc = Pexp_ident(Longident.Lident "*opt*")
-            },
-            scases
-          )
-      } in
-      let sfun = {
-        pexp_loc = loc;
-        pexp_desc =
-         Pexp_function (
-           l, None,
-           [ {ppat_loc = loc;
-              ppat_desc = Ppat_var "*opt*"},
-             {pexp_loc = loc;
-              pexp_desc = Pexp_let(Default, [spat, smatch], sbody);
-             }
-           ]
-         )
-      } in
-      type_expect ?in_function env sfun ty_expected'
-  | Pexp_function (l, _, caselist) ->
-      let (loc_fun, ty_fun) =
-        match in_function with Some p -> p
-        | None -> (loc, ty_expected)
-      in
-      if !Clflags.principal then begin_def ();
-      let (ty_arg, ty_res) =
-        try filter_arrow env (instance ty_expected') l
-        with Unify _ ->
-          match expand_head env ty_expected with
-            {desc = Tarrow _} as ty ->
-              raise(Error(loc, Abstract_wrong_label(l, ty)))
-          | _ ->
-              raise(Error(loc_fun,
-                          Too_many_arguments (in_function <> None, ty_fun)))
-      in
-      let ty_arg =
-        if is_optional l then
-          let tv = newvar() in
-          begin
-            try unify env (instance ty_arg) (type_option tv)
-            with Unify _ -> assert false
-          end;
-          type_option tv
-        else ty_arg
-      in
-      if !Clflags.principal then begin
-        end_def ();
-        generalize_structure ty_arg;
-        generalize_structure ty_res
-      end;
-      let cases, partial =
-        type_cases ~in_function:(loc_fun,ty_fun) env ty_arg ty_res
-          true loc caselist in
-      let not_function ty =
-        let ls, tvar = list_labels env ty in
-        ls = [] && not tvar
-      in
-      if is_optional l && not_function ty_res then
-        Location.prerr_warning (fst (List.hd cases)).pat_loc
-          Warnings.Unerasable_optional_argument;
-      re {
-        exp_desc = Texp_function(cases, partial);
-        exp_loc = loc;
-        exp_type = instance (newgenty (Tarrow(l, ty_arg, ty_res, Cok)));
-        exp_env = env }
-  | Pexp_when(scond, sbody) ->
-      let cond = type_expect env scond (instance Predef.type_bool) in
-      let body = type_expect env sbody ty_expected in
-      re {
-        exp_desc = Texp_when(cond, body);
-        exp_loc = loc;
-        exp_type = body.exp_type;
-        exp_env = env }
-  | Pexp_poly(sbody, sty) ->
-      let ty =
-        match sty with None -> repr ty_expected
-        | Some sty ->
-            let ty = Typetexp.transl_simple_type env false sty in
-            repr ty
-      in
-      let set_type ty =
-        unify_exp env
-          { exp_desc = Texp_tuple [];
-            exp_loc = loc;
-            exp_type = ty; exp_env = env } ty_expected in
-      begin
-        match ty.desc with
-          Tpoly (ty', []) ->
-            if sty <> None then set_type ty;
-            let exp = type_expect env sbody ty' in
-            re { exp with exp_type = ty }
-        | Tpoly (ty', tl) ->
-            if sty <> None then set_type ty;
-            (* One more level to generalize locally *)
-            begin_def ();
-            let vars, ty'' = instance_poly true tl ty' in
-            let exp = type_expect env sbody ty'' in
-            end_def ();
-            check_univars env false "method" exp ty_expected vars;
-            re { exp with exp_type = ty }
-	| Tvar ->
-	    let exp = type_exp env sbody in
-	    let exp = {exp with exp_type = newty (Tpoly (exp.exp_type, []))} in
-	    unify_exp env exp ty;
-	    re exp
-        | _ -> assert false
-      end
-  | Pexp_match(sarg, caselist) ->
-      if !Clflags.principal then begin_def ();
-      let arg = type_exp env sarg in
-      if !Clflags.principal then begin
-          end_def ();
-          generalize_structure arg.exp_type;
-      end;
-      let cases, partial =
-        type_cases env arg.exp_type ty_expected' true loc caselist
-      in
-      re {
-        exp_desc = Texp_match(arg, cases, partial);
-        exp_loc = loc;
-        exp_type = ty_expected;
-        exp_env = env }
-  | Pexp_tuple sexpl ->
-      let subtypes = List.map (fun _ -> newgenvar ()) sexpl in 
-      let to_unify = newgenty (Ttuple subtypes) in
-      unify_exp_types loc env to_unify ty_expected' ;
-      let expl = 
-	List.map2 (fun body ty -> type_expect env body ty) sexpl subtypes 
-      in
-      re {
-        exp_desc = Texp_tuple expl;
-        exp_loc = loc;
-        exp_type = ty_expected;
-        exp_env = env }
-  | Pexp_pack m ->
-      let (p, nl, tl) =
-        match Ctype.expand_head env ty_expected with
-          {desc = Tpackage (p, nl, tl)} ->
-            if !Clflags.principal &&
-              (Ctype.expand_head env ty_expected').level < Btype.generic_level
-            then
-              Location.prerr_warning loc
-                (Warnings.Not_principal "this module packing");
-            (p, nl, tl)
-        | {desc = Tvar} ->
-            raise (Error (loc, Cannot_infer_signature))
-        | _ ->
-            raise (Error (loc, Not_a_packed_module ty_expected))
-      in
-      let context = Typetexp.narrow () in
-      let (modl, tl') = !type_package env m p nl tl in
-      Typetexp.widen context;
-      let exp = {
-        exp_desc = Texp_pack modl;
-        exp_loc = loc;
-        exp_type = newty (Tpackage (p, nl, tl'));
-        exp_env = env } in
-      unify_exp env exp ty_expected;
-      re {exp with exp_type = ty_expected}
-  | _ ->
-      let exp = type_exp env sexp in
-      unify_exp env exp ty_expected;
-      exp
-
 (* Typing of statements (expressions whose values are discarded) *)
 
 and type_statement env sexp =