vive les methodes polymorphes!

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

39 files changed, 1166 insertions, 309 deletions

diff --git a/boot/ocamlc b/boot/ocamlc
index 008e73ba7..2ad1f5f4e 100755
--- a/boot/ocamlc
+++ b/boot/ocamlc
diff --git a/boot/ocamllex b/boot/ocamllex
index 937aadfb3..8baed4885 100755
--- a/boot/ocamllex
+++ b/boot/ocamllex
diff --git a/bytecomp/bytelibrarian.ml b/bytecomp/bytelibrarian.ml
index 1194fc1b3..bad04b7a5 100644
--- a/bytecomp/bytelibrarian.ml
+++ b/bytecomp/bytelibrarian.ml
@@ -69,7 +69,6 @@ let copy_object_file oc name =
       let compunit_pos = input_binary_int ic in
       seek_in ic compunit_pos;
       let compunit = (input_value ic : compilation_unit) in
-      Bytelink.check_consistency file_name compunit;
       copy_compunit ic oc compunit;
       close_in ic;
       [compunit]
@@ -78,7 +77,6 @@ let copy_object_file oc name =
       let toc_pos = input_binary_int ic in
       seek_in ic toc_pos;
       let toc = (input_value ic : library) in
-      List.iter (Bytelink.check_consistency file_name) toc.lib_units;
       add_ccobjs toc;
       List.iter (copy_compunit ic oc) toc.lib_units;
       close_in ic;
diff --git a/bytecomp/bytelink.ml b/bytecomp/bytelink.ml
index 6ac77a49b..e9c0425c0 100644
--- a/bytecomp/bytelink.ml
+++ b/bytecomp/bytelink.ml
@@ -431,14 +431,14 @@ let build_custom_runtime prim_name exec_name =
        (Printf.sprintf
           "%s -o %s %s %s %s %s %s -lcamlrun %s"
           !Clflags.c_linker
-          (Filename.quote exec_name)
+          exec_name
           (Clflags.std_include_flag "-I")
           (String.concat " " (List.rev !Clflags.ccopts))
           prim_name
-          (Ccomp.quote_files
+          (String.concat " "
             (List.map (fun dir -> if dir = "" then "" else "-L" ^ dir)
                       !load_path))
-          (Ccomp.quote_files (List.rev !Clflags.ccobjs))
+          (String.concat " " (List.rev !Clflags.ccobjs))
           Config.bytecomp_c_libraries)
   | "Win32" ->
       let retcode =
@@ -446,13 +446,13 @@ let build_custom_runtime prim_name exec_name =
        (Printf.sprintf
           "%s /Fe%s %s %s %s %s %s %s"
           !Clflags.c_linker
-          (Filename.quote exec_name)
+          exec_name
           (Clflags.std_include_flag "-I")
           (String.concat " " (List.rev !Clflags.ccopts))
           prim_name
-          (Ccomp.quote_files
-            (List.rev_map Ccomp.expand_libname !Clflags.ccobjs))
-          (Filename.quote (Ccomp.expand_libname "-lcamlrun"))
+          (String.concat " "
+                         (List.rev_map Ccomp.expand_libname !Clflags.ccobjs))
+          (Ccomp.expand_libname "-lcamlrun")
           Config.bytecomp_c_libraries) in
       (* C compiler doesn't clean up after itself.  Note that the .obj
          file is created in the current working directory. *)
diff --git a/byterun/lexing.c b/byterun/lexing.c
index dab0a962f..ec44eb053 100644
--- a/byterun/lexing.c
+++ b/byterun/lexing.c
@@ -22,7 +22,7 @@
 struct lexer_buffer {
   value refill_buff;
   value lex_buffer;
-  value lex_buffer_len;
+  value lex_buffer_end;
   value lex_abs_pos;
   value lex_start_pos;
   value lex_curr_pos;
@@ -72,7 +72,7 @@ CAMLprim value lex_engine(struct lexing_table *tbl, value start_state,
       lexbuf->lex_last_action = Val_int(backtrk);
     }
     /* See if we need a refill */
-    if (lexbuf->lex_curr_pos >= lexbuf->lex_buffer_len){
+    if (lexbuf->lex_curr_pos >= lexbuf->lex_buffer_end){
       if (lexbuf->lex_eof_reached == Val_bool (0)){
         return Val_int(-state - 1);
       }else{
diff --git a/byterun/unix.c b/byterun/unix.c
index 38b9b4aad..62961c40e 100644
--- a/byterun/unix.c
+++ b/byterun/unix.c
@@ -157,10 +157,13 @@ char * search_dll_in_path(struct ext_table * path, char * name)
 #ifndef RTLD_GLOBAL
 #define RTLD_GLOBAL 0
 #endif
+#ifndef RTLD_NODELETE
+#define RTLD_NODELETE 0
+#endif
 
 void * caml_dlopen(char * libname)
 {
-  return dlopen(libname, RTLD_NOW|RTLD_GLOBAL);
+  return dlopen(libname, RTLD_NOW|RTLD_GLOBAL|RTLD_NODELETE);
 }
 
 void caml_dlclose(void * handle)
diff --git a/driver/main.ml b/driver/main.ml
index 3d0aa0cf0..6ee14e5c0 100644
--- a/driver/main.ml
+++ b/driver/main.ml
@@ -95,6 +95,7 @@ module Options = Main_args.Make_options (struct
   let _output_obj () = output_c_object := true; custom_runtime := true
   let _pack = set make_package
   let _pp s = preprocessor := Some s
+  let _principal = set principal
   let _rectypes = set recursive_types
   let _thread = set thread_safe
   let _unsafe = set fast
diff --git a/driver/main_args.ml b/driver/main_args.ml
index b474ccfa1..0beea91e4 100644
--- a/driver/main_args.ml
+++ b/driver/main_args.ml
@@ -39,6 +39,7 @@ module Make_options (F :
      val _output_obj : unit -> unit
      val _pack : unit -> unit
      val _pp : string -> unit
+     val _principal : unit -> unit
      val _rectypes : unit -> unit
      val _thread : unit -> unit
      val _unsafe : unit -> unit
@@ -101,6 +102,8 @@ struct
            " Package the given .cmo files into one .cmo";
     "-pp", Arg.String F._pp,
            "<command>  Pipe sources through preprocessor <command>";
+    "-principal", Arg.Unit F._principal,
+           " Check principality of type inference";
     "-rectypes", Arg.Unit F._rectypes, " Allow arbitrary recursive types";
     "-thread", Arg.Unit F._thread, " Use thread-safe standard library";
     "-unsafe", Arg.Unit F._unsafe,
diff --git a/driver/main_args.mli b/driver/main_args.mli
index 1d28c8b19..137ed6892 100644
--- a/driver/main_args.mli
+++ b/driver/main_args.mli
@@ -39,6 +39,7 @@ module Make_options (F :
       val _output_obj : unit -> unit
       val _pack : unit -> unit
       val _pp : string -> unit
+      val _principal : unit -> unit
       val _rectypes : unit -> unit
       val _thread : unit -> unit
       val _unsafe : unit -> unit
diff --git a/driver/optmain.ml b/driver/optmain.ml
index 9cfbe2259..f1a6c39bc 100644
--- a/driver/optmain.ml
+++ b/driver/optmain.ml
@@ -110,6 +110,8 @@ let main () =
               " Package the given .cmo files into one .cmo";
        "-pp", Arg.String(fun s -> preprocessor := Some s),
              "<command>  Pipe sources through preprocessor <command>";
+       "-principal", Arg.Set principal,
+             " Check principality of type inference";
        "-rectypes", Arg.Set recursive_types,
              " Allow arbitrary recursive types";
        "-S", Arg.Set keep_asm_file, " Keep intermediate assembly file";
diff --git a/otherlibs/labltk/browser/searchpos.ml b/otherlibs/labltk/browser/searchpos.ml
index cf4f009b3..4302ad002 100644
--- a/otherlibs/labltk/browser/searchpos.ml
+++ b/otherlibs/labltk/browser/searchpos.ml
@@ -127,7 +127,8 @@ let rec search_pos_type t ~pos ~env =
   | Ptyp_class (lid, tl, _) ->
       List.iter tl ~f:(search_pos_type ~pos ~env);
       add_found_sig (`Type, lid) ~env ~loc:t.ptyp_loc
-  | Ptyp_alias (t, _) -> search_pos_type ~pos ~env t
+  | Ptyp_alias (t, _)
+  | Ptyp_poly (_, t) -> search_pos_type ~pos ~env t
   end
 
 let rec search_pos_class_type cl ~pos ~env =
diff --git a/parsing/parser.mly b/parsing/parser.mly
index d6dabc057..a037ccb08 100644
--- a/parsing/parser.mly
+++ b/parsing/parser.mly
@@ -612,14 +612,18 @@ value:
             symbol_rloc () }
 ;
 virtual_method:
-    METHOD PRIVATE VIRTUAL label COLON core_type
+    METHOD PRIVATE VIRTUAL label COLON poly_type
       { $4, Private, $6, symbol_rloc () }
-  | METHOD VIRTUAL private_flag label COLON core_type
+  | METHOD VIRTUAL private_flag label COLON poly_type
       { $4, $3, $6, symbol_rloc () }
 ;
 concrete_method :
-    METHOD private_flag label fun_binding
-      { $3, $2, $4, symbol_rloc () }
+    METHOD private_flag label strict_binding
+      { $3, $2, mkexp(Pexp_poly ($4, None)), symbol_rloc () }
+  | METHOD private_flag label COLON poly_type EQUAL seq_expr
+      { $3, $2, mkexp(Pexp_poly($7,Some $5)), symbol_rloc () }
+  | METHOD private_flag LABEL poly_type EQUAL seq_expr
+      { $3, $2, mkexp(Pexp_poly($6,Some $4)), symbol_rloc () }
 ;
 
 /* Class types */
@@ -680,7 +684,7 @@ XXX Should be removed
 */
 ;
 method_type:
-    METHOD private_flag label COLON core_type
+    METHOD private_flag label COLON poly_type
       { $3, $2, $5, symbol_rloc () }
 ;
 constrain:
@@ -964,10 +968,20 @@ let_binding:
       { ($1, $3) }
 ;
 fun_binding:
+/*
     EQUAL seq_expr
       { $2 }
+  | labeled_simple_pattern fun_binding
+      { let (l, o, p) = $1 in mkexp(Pexp_function(l, o, [p, $2])) }
+*/
+    strict_binding
+      { $1 }
   | type_constraint EQUAL seq_expr
       { let (t, t') = $1 in mkexp(Pexp_constraint($3, t, t')) }
+;
+strict_binding:
+    EQUAL seq_expr
+      { $2 }
   | labeled_simple_pattern fun_binding
       { let (l, o, p) = $1 in mkexp(Pexp_function(l, o, [p, $2])) }
 ;
@@ -1164,7 +1178,7 @@ label_declarations:
   | label_declarations SEMI label_declaration   { $3 :: $1 }
 ;
 label_declaration:
-    mutable_flag label COLON core_type          { ($2, $1, $4) }
+    mutable_flag label COLON poly_type          { ($2, $1, $4) }
 ;
 
 /* "with" constraints (additional type equations over signature components) */
@@ -1188,6 +1202,19 @@ with_constraint:
       { ($2, Pwith_module $4) }
 ;
 
+/* Polymorphic types */
+
+typevar_list:
+	QUOTE ident				{ [$2] }
+      | typevar_list QUOTE ident		{ $3 :: $1 }
+;
+poly_type:
+	core_type
+	  { mktyp(Ptyp_poly([], $1)) }
+      |	typevar_list DOT core_type
+	  { mktyp(Ptyp_poly(List.rev $1, $3)) }
+;
+
 /* Core types */
 
 core_type:
@@ -1306,7 +1333,7 @@ meth_list:
   | DOTDOT                                      { [mkfield Pfield_var] }
 ;
 field:
-    label COLON core_type                       { mkfield(Pfield($1, $3)) }
+    label COLON poly_type                       { mkfield(Pfield($1, $3)) }
 ;
 label:
     LIDENT                                      { $1 }
diff --git a/parsing/parsetree.mli b/parsing/parsetree.mli
index b3aa968d2..9c055afdf 100644
--- a/parsing/parsetree.mli
+++ b/parsing/parsetree.mli
@@ -32,6 +32,7 @@ and core_type_desc =
   | Ptyp_class of Longident.t * core_type list * label list
   | Ptyp_alias of core_type * string
   | Ptyp_variant of row_field list * bool * label list option
+  | Ptyp_poly of string list * core_type
 
 and core_field_type =
   { pfield_desc: core_field_desc;
@@ -108,6 +109,7 @@ and expression_desc =
   | Pexp_assert of expression
   | Pexp_assertfalse
   | Pexp_lazy of expression
+  | Pexp_poly of expression * core_type option
 
 (* Value descriptions *)
 
diff --git a/parsing/printast.ml b/parsing/printast.ml
index ec96e871d..5088e590d 100644
--- a/parsing/printast.ml
+++ b/parsing/printast.ml
@@ -125,6 +125,10 @@ let rec core_type i ppf x =
   | Ptyp_alias (ct, s) ->
       line i ppf "Ptyp_alias \"%s\"\n" s;
       core_type i ppf ct;
+  | Ptyp_poly (sl, ct) ->
+      line i ppf "Ptyp_poly%a\n"
+        (fun ppf -> List.iter (fun x -> fprintf ppf " '%s" x)) sl;
+      core_type i ppf ct;
 
 and core_field_type i ppf x =
   line i ppf "core_field_type %a\n" fmt_location x.pfield_loc;
@@ -274,6 +278,10 @@ and expression i ppf x =
   | Pexp_lazy (e) ->
       line i ppf "Pexp_lazy";
       expression i ppf e;
+  | Pexp_poly (e, cto) ->
+      line i ppf "Pexp_poly\n";
+      expression i ppf e;
+      option i core_type ppf cto;
 
 and value_description i ppf x =
   line i ppf "value_description\n";
diff --git a/stdlib/sys.ml b/stdlib/sys.ml
index 99a164380..98373b724 100644
--- a/stdlib/sys.ml
+++ b/stdlib/sys.ml
@@ -78,4 +78,4 @@ let catch_break on =
 (* OCaml version string, moved from utils/config.mlp.
    Must be in the format described in sys.mli. *)
 
-let ocaml_version = "3.04+9 (2002-04-04)"
+let ocaml_version = "3.04+10 (2002-04-18)"
diff --git a/tools/addlabels.ml b/tools/addlabels.ml
index c04809b53..f17e9d4fd 100644
--- a/tools/addlabels.ml
+++ b/tools/addlabels.ml
@@ -253,7 +253,8 @@ let rec add_labels_expr ~text ~values ~classes expr =
   | Pexp_setinstvar (_, e)
   | Pexp_letmodule (_, _, e)
   | Pexp_assert e
-  | Pexp_lazy e ->
+  | Pexp_lazy e
+  | Pexp_poly (e, _) ->
       add_labels_rec e
   | Pexp_record (lst, opt) ->
       List.iter lst ~f:(fun (_,e) -> add_labels_rec e);
diff --git a/tools/depend.ml b/tools/depend.ml
index 5b4f9a2c6..4f543a192 100644
--- a/tools/depend.ml
+++ b/tools/depend.ml
@@ -51,6 +51,7 @@ let rec add_type bv ty =
         (function Rtag(_,_,stl) -> List.iter (add_type bv) stl
           | Rinherit sty -> add_type bv sty)
         fl
+  | Ptyp_poly(_, t) -> add_type bv t
 
 and add_field_type bv ft =
   match ft.pfield_desc with
@@ -151,6 +152,7 @@ let rec add_expr bv exp =
   | Pexp_assert (e) -> add_expr bv e
   | Pexp_assertfalse -> ()
   | Pexp_lazy (e) -> add_expr bv e
+  | Pexp_poly (e, t) -> add_expr bv e; add_opt add_type bv t
 
 and add_pat_expr_list bv pel =
   List.iter (fun (p, e) -> add_pattern bv p; add_expr bv e) pel
diff --git a/tools/ocamlcp.ml b/tools/ocamlcp.ml
index 95838365d..baad2256f 100644
--- a/tools/ocamlcp.ml
+++ b/tools/ocamlcp.ml
@@ -58,6 +58,7 @@ module Options = Main_args.Make_options (struct
   let _output_obj = option "-output-obj"
   let _pack = option "-pack"
   let _pp s = incompatible "-pp"
+  let _principal = option "-principal"
   let _rectypes = option "-rectypes"
   let _thread () = ismultithreaded := "-thread"; option "-thread" ()
   let _unsafe = option "-unsafe"
diff --git a/tools/ocamlprof.ml b/tools/ocamlprof.ml
index 64d737c3d..b9d80c304 100644
--- a/tools/ocamlprof.ml
+++ b/tools/ocamlprof.ml
@@ -287,6 +287,8 @@ and rw_exp iflag sexp =
 
   | Pexp_lazy (expr) -> rewrite_exp iflag expr
 
+  | Pexp_poly (sexp, _) -> rewrite_exp iflag sexp
+
 and rewrite_ifbody iflag ghost sifbody =
   if !instr_if && not ghost then
     insert_profile rw_exp sifbody
diff --git a/toplevel/genprintval.ml b/toplevel/genprintval.ml
index 788c69db4..dcafc639a 100644
--- a/toplevel/genprintval.ml
+++ b/toplevel/genprintval.ml
@@ -313,6 +313,10 @@ module Make(O : OBJ)(EVP : EVALPATH with type value = O.t) = struct
               tree_of_val (depth - 1) obj ty
           | Tfield(_, _, _, _) | Tnil | Tlink _ ->
               fatal_error "Printval.outval_of_value"
+          | Tpoly (ty, _) ->
+              tree_of_val (depth - 1) obj ty
+          | Tunivar ->
+              Oval_stuff "<poly>"
         end
 
       and tree_of_val_list start depth obj ty_list =
diff --git a/toplevel/topmain.ml b/toplevel/topmain.ml
index 5396e9fff..49142eeaa 100644
--- a/toplevel/topmain.ml
+++ b/toplevel/topmain.ml
@@ -45,6 +45,7 @@ let main () =
      "-nolabels", Arg.Set classic, " Ignore labels and do not commute";
      "-nostdlib", Arg.Set no_std_include,
            " do not add default directory to the list of include directories";
+     "-principal", Arg.Set principal, " Check principality of type inference";
      "-rectypes", Arg.Set recursive_types, " Allow arbitrary recursive types";
      "-unsafe", Arg.Set fast, " No bound checking on array and string access";
      "-w", Arg.String (Warnings.parse_options false),
diff --git a/typing/btype.ml b/typing/btype.ml
index 8a8879a26..35d18909b 100644
--- a/typing/btype.ml
+++ b/typing/btype.ml
@@ -121,7 +121,7 @@ let rec iter_row f row =
     row.row_fields;
   match (repr row.row_more).desc with
     Tvariant row -> iter_row f row
-  | Tvar | Tnil ->
+  | Tvar | Tnil | Tunivar ->
       Misc.may (fun (_,l) -> List.iter f l) row.row_name;
       List.iter f row.row_bound
   | _ -> assert false
@@ -140,8 +140,15 @@ let iter_type_expr f ty =
   | Tnil                -> ()
   | Tlink ty            -> f ty
   | Tsubst ty           -> f ty
+  | Tunivar             -> ()
+  | Tpoly (ty, tyl)     -> f ty; List.iter f tyl
 
-let copy_row f row keep more =
+let rec iter_abbrev f = function
+    Mnil                   -> ()
+  | Mcons(_, ty, ty', rem) -> f ty; f ty'; iter_abbrev f rem
+  | Mlink rem              -> iter_abbrev f !rem
+
+let copy_row f fixed row keep more =
   let bound = ref [] in
   let fields = List.map
       (fun (l, fi) -> l,
@@ -149,6 +156,7 @@ let copy_row f row keep more =
         | Rpresent(Some ty) -> Rpresent(Some(f ty))
         | Reither(c, tl, m, e) ->
             let e = if keep then e else ref None in
+            let m = if row.row_fixed then fixed else m in
             let tl = List.map f tl in
             bound := List.filter
                 (function {desc=Tconstr(_,[],_)} -> false | _ -> true)
@@ -160,7 +168,8 @@ let copy_row f row keep more =
   let name =
     match row.row_name with None -> None
     | Some (path, tl) -> Some (path, List.map f tl) in
-  { row_fields = fields; row_more = more; row_bound = !bound;
+  { row_fields = fields; row_more = more;
+    row_bound = !bound; row_fixed = row.row_fixed && fixed;
     row_closed = row.row_closed; row_name = name; }
 
 let rec copy_kind = function
@@ -182,56 +191,14 @@ let rec copy_type_desc f = function
   | Tobject (ty, _)     -> Tobject (f ty, ref None)
   | Tvariant row        ->
       let row = row_repr row in
-      Tvariant (copy_row f row false (f row.row_more))
+      Tvariant (copy_row f true row false (f row.row_more))
   | Tfield (p, k, ty1, ty2) -> Tfield (p, copy_kind k, f ty1, f ty2)
   | Tnil                -> Tnil
   | Tlink ty            -> copy_type_desc f ty.desc
   | Tsubst ty           -> assert false
+  | Tunivar             -> Tunivar
+  | Tpoly (ty, tyl)     -> Tpoly (f ty, List.map f tyl)
 
-(*
-let rec iter_signature f =
-  List.iter (iter_signature_item f)
-
-and iter_signature_item f = function
-    Tsig_value (_, d) ->
-      f d.val_type;
-      (match d.val_kind with Val_reg | Val_prim _ -> () | _ -> assert false)
-  | Tsig_type (_, d) ->
-      List.iter f d.type_params;
-      begin match d.type_kind with
-        Type_abstract -> ()
-      | Type_variant l -> List.iter (fun (_, tl) -> List.iter f tl) l
-      | Type_record r -> List.iter (fun (_, _, t) -> f t)
-      end;
-      may f d.type_manifest
-  | Tsig_exception (_, d) -> List.iter f d
-  | Tsig_module (_, m) -> iter_module_type f m
-  | Tsig_modtype (_, Tmodtype_manifest m) -> iter_module_type f m
-  | Tsig_modtype (_, Tmodtype_bastract) -> ()
-  | Tsig_class (_, d) ->
-      List.iter f d.cty_params;
-      iter_class_type f d.cty_type;
-      may f d.cty_new
-  | Tsig_cltype (_, d) ->
-      List.iter f d.clty_params;
-      iter_class_type f d.clty_type
-
-and iter_module_type f = function
-    Tmty_ident _ -> ()
-  | Tmty_signature sg -> iter_signature f sg
-  | Tmty_functor (_, m1, m2) -> iter_module_type f m1; iter_module_type f m2
-
-and iter_class_type f = function
-    Tcty_constr (_, tl, ct) ->
-      List.iter f tl;
-      iter_class_type f ct
-  | Tcty_fun (_, t, ct) ->
-      f t;
-      iter_class_type f ct
-  | Tcty_signature s ->
-      f s.cty_self;
-      Vars.iter (fun _ (_, t) -> f t) s.cty_vars
-*)
 
 (* Utilities for copying *)
 
diff --git a/typing/btype.mli b/typing/btype.mli
index a37cb2ac7..f0609d844 100644
--- a/typing/btype.mli
+++ b/typing/btype.mli
@@ -60,11 +60,14 @@ val iter_type_expr: (type_expr -> unit) -> type_expr -> unit
         (* Iteration on types *)
 val iter_row: (type_expr -> unit) -> row_desc -> unit
         (* Iteration on types in a row *)
+val iter_abbrev: (type_expr -> unit) -> abbrev_memo -> unit
+        (* Iteration on types in an abbreviation list *)
 
 val copy_type_desc: (type_expr -> type_expr) -> type_desc -> type_desc
         (* Copy on types *)
 val copy_row:
-    (type_expr -> type_expr) -> row_desc -> bool -> type_expr -> row_desc
+    (type_expr -> type_expr) ->
+    bool -> row_desc -> bool -> type_expr -> row_desc
 val copy_kind: field_kind -> field_kind
 
 val save_desc: type_expr -> type_desc -> unit
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 8a5637077..1bfe2538b 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -129,6 +129,10 @@ let restore_global_level () =
     gl::rem -> global_level := gl; saved_global_level := rem
   | []      -> assert false
 
+(* Abbreviations without parameters *)
+(* Shall reset after generalizing *)
+let simple_abbrevs = ref Mnil
+
 (**** Some type creators ****)
 
 (* Re-export generic type creators *)
@@ -381,8 +385,7 @@ let rec free_vars_rec real ty =
     | Tvariant row ->
         let row = row_repr row in
         iter_row (free_vars_rec true) {row with row_bound = []};
-        if not (static_row row) then
-          free_variables := (row_more row, false) :: !free_variables
+        if not (static_row row) then free_vars_rec false row.row_more
     | _    ->
         iter_type_expr (free_vars_rec true) ty
     end;
@@ -497,22 +500,18 @@ let rec iter_generalize tyl ty =
     ty.level <- generic_level;
     begin match ty.desc with
       Tconstr (_, _, abbrev) ->
-        generalize_expans tyl !abbrev
+        iter_abbrev (iter_generalize tyl) !abbrev
     | _ -> ()
     end;
     iter_type_expr (iter_generalize tyl) ty
   end else
     tyl := ty :: !tyl
 
-and generalize_expans tyl =
-  function
-    Mnil                   -> ()
-  | Mcons(_, ty, ty', rem) -> iter_generalize tyl ty;
-                              iter_generalize tyl ty';
-                              generalize_expans tyl rem
-  | Mlink rem              -> generalize_expans tyl !rem
+let iter_generalize tyl ty =
+  simple_abbrevs := Mnil;
+  iter_generalize tyl ty
 
-let rec generalize ty =
+let generalize ty =
   iter_generalize (ref []) ty
 
 (* Efficient repeated generalisation of the same type *)
@@ -522,6 +521,43 @@ let iterative_generalization min_level tyl =
   List.fold_right (fun ty l -> if ty.level <= min_level then l else ty::l)
     !tyl' []
 
+(* Generalize the structure and lower the variables *)
+
+let rec generalize_structure var_level ty =
+  let ty = repr ty in
+  if ty.level <> generic_level then begin
+    if ty.desc = Tvar && ty.level > var_level then
+      ty.level <- var_level
+    else if ty.level > !current_level then begin
+      ty.level <- generic_level;
+      begin match ty.desc with
+	Tconstr (_, _, abbrev) ->
+          iter_abbrev (generalize_structure var_level) !abbrev
+      | _ -> ()
+      end;
+      iter_type_expr (generalize_structure var_level) ty
+    end
+  end
+
+let generalize_structure var_level ty =
+  simple_abbrevs := Mnil;
+  generalize_structure var_level ty
+
+let generalize_expansive ty = generalize_structure !nongen_level ty
+let generalize_global ty = generalize_structure !global_level ty
+let generalize_structure ty = generalize_structure !current_level ty
+
+(* Generalize the spine of a function, if the level >= !current_level *)
+
+let rec generalize_spine ty =
+  let ty = repr ty in
+  if ty.level < !current_level || ty.level = generic_level then () else
+  match ty.desc with
+    Tarrow (_, _, ty', _) | Tpoly (ty', _) ->
+      ty.level <- generic_level;
+      generalize_spine ty'
+  | _ -> ()
+
 let try_expand_head' = (* Forward declaration *)
   ref (fun env ty -> raise Cannot_expand)
 
@@ -662,7 +698,10 @@ let rec copy ty =
     t.desc <-
       begin match desc with
       | Tconstr (p, tl, _) ->
-          begin match find_repr p !(!abbreviations) with
+          let abbrevs =
+            if tl = [] && not !Clflags.principal then simple_abbrevs
+            else !abbreviations in
+          begin match find_repr p !abbrevs with
             Some ty when repr ty != t -> (* XXX Commentaire... *)
               Tlink ty
           | _ ->
@@ -685,19 +724,24 @@ let rec copy ty =
           let more = repr row.row_more in
           (* We must substitute in a subtle way *)
           begin match more.desc with
-            Tsubst ty2 ->
+            Tsubst ({desc=Tvariant _} as ty2) ->
               (* This variant type has been already copied *)
               ty.desc <- Tsubst ty2; (* avoid Tlink in the new type *)
               Tlink ty2
           | _ ->
               (* If the row variable is not generic, we must keep it *)
               let keep = more.level <> generic_level in
+              let desc = more.desc in
               (* Register new type first for recursion *)
               save_desc more more.desc;
               more.desc <- ty.desc;
               (* Return a new copy *)
-              let more' = if keep then more else newvar () in
-              Tvariant (copy_row copy row keep more')
+              let more' =
+                if keep then more else
+                match desc with Tsubst ty -> ty
+                | _ -> newty desc
+              in
+              Tvariant (copy_row copy true row keep more')
           end
       | _ -> copy_type_desc copy desc
       end;
@@ -721,12 +765,6 @@ let instance_constructor cstr =
   cleanup_types ();
   (ty_args, ty_res)
 
-let instance_label lbl =
-  let ty_res = copy lbl.lbl_res in
-  let ty_arg = copy lbl.lbl_arg in
-  cleanup_types ();
-  (ty_arg, ty_res)
-
 let instance_parameterized_type sch_args sch =
   let ty_args = List.map copy sch_args in
   let ty = copy sch in
@@ -759,6 +797,130 @@ let instance_class params cty =
   cleanup_types ();
   (params', cty')
 
+(**** Instanciation for types with free universal variables ****)
+
+module TypeHash = Hashtbl.Make(TypeOps)
+module TypeSet = Set.Make(TypeOps)
+
+type inv_type_expr =
+    { inv_type : type_expr;
+      mutable inv_parents : inv_type_expr list }
+
+let rec inv_type hash pty ty =
+  let ty = repr ty in
+  try
+    let inv = TypeHash.find hash ty in
+    inv.inv_parents <- pty @ inv.inv_parents
+  with Not_found ->
+    let inv = { inv_type = ty; inv_parents = pty } in
+    TypeHash.add hash ty inv;
+    iter_type_expr (inv_type hash [inv]) ty
+
+let compute_univars ty =
+  let inverted = TypeHash.create 17 in
+  inv_type inverted [] ty;
+  let node_univars = TypeHash.create 17 in
+  let rec add_univar univ inv =
+    match inv.inv_type.desc with
+      Tpoly (ty, tl) when List.memq univ (List.map repr tl) -> ()
+    | _ ->
+        try
+          let univs = TypeHash.find node_univars inv.inv_type in
+          if not (TypeSet.mem univ !univs) then begin
+            univs := TypeSet.add univ !univs;
+            List.iter (add_univar univ) inv.inv_parents
+          end
+        with Not_found ->
+          TypeHash.add node_univars inv.inv_type (ref(TypeSet.singleton univ));
+          List.iter (add_univar univ) inv.inv_parents
+  in
+  TypeHash.iter
+    (fun ty inv -> if ty.desc = Tunivar then add_univar ty inv)
+    inverted;
+  fun ty ->
+    try !(TypeHash.find node_univars ty) with Not_found -> TypeSet.empty
+  
+let rec diff_list l1 l2 =
+  if l1 == l2 then [] else
+  match l1 with [] -> invalid_arg "Ctype.diff_list"
+  | a :: l1 -> a :: diff_list l1 l2
+
+let conflicts free bound =
+  let bound = List.map repr bound in
+  TypeSet.exists (fun t -> List.memq (repr t) bound) free
+
+let delayed_copy = ref []
+    (* copying to do later *)
+
+(* Copy without sharing until there are no free univars left *)
+(* all free univars must be included in [visited]            *)
+let rec copy_sep fixed free bound visited ty =
+  let ty = repr ty in
+  let univars = free ty in
+  if TypeSet.is_empty univars then 
+    if ty.level <> generic_level then ty else
+    let t = newvar () in
+    delayed_copy :=
+      lazy (t.desc <- Tlink (copy ty))
+      :: !delayed_copy;
+    t
+  else try
+    let t, bound_t = List.assq ty visited in
+    let dl = if ty.desc = Tunivar then [] else diff_list bound bound_t in
+    if dl <> [] && conflicts univars dl then raise Not_found;
+    t
+  with Not_found -> begin
+    let t = newvar() in          (* Stub *)
+    let visited =
+      match ty.desc with
+	Tarrow _ | Ttuple _ | Tvariant _ | Tconstr _ | Tobject _ ->
+          (ty,(t,bound)) :: visited
+      |	_ -> visited in
+    let copy_rec = copy_sep fixed free bound visited in
+    t.desc <-
+      begin match ty.desc with
+      | Tvariant row0 ->
+          let row = row_repr row0 in
+          let more = repr row.row_more in
+          (* We shall really check the level on the row variable *)
+          let keep = more.desc = Tvar && more.level <> generic_level in
+          let more' = copy_rec more in
+          let row = copy_row copy_rec fixed row keep more' in
+          Tvariant row
+      |	Tpoly (t1, tl) ->
+	  let tl = List.map repr tl in
+	  let tl' = List.map (fun t -> newty Tunivar) tl in
+	  let bound = tl @ bound in
+	  let visited =
+	    List.map2 (fun ty t -> ty,(t,bound)) tl tl' @ visited in
+	  Tpoly (copy_rec t1, tl')
+      | _ -> copy_type_desc copy_rec ty.desc
+      end;
+    t
+  end
+
+let instance_poly fixed univars sch =
+  let vars = List.map (fun _ -> newvar ()) univars in
+  let pairs = List.map2 (fun u v -> repr u, (v, [])) univars vars in
+  delayed_copy := [];
+  let ty = copy_sep fixed (compute_univars sch) [] pairs sch in
+  List.iter Lazy.force !delayed_copy;
+  delayed_copy := [];
+  cleanup_types ();
+  vars, ty
+
+let instance_label fixed lbl =
+  let ty_res = copy lbl.lbl_res in
+  let vars, ty_arg =
+    match repr lbl.lbl_arg with
+      {desc = Tpoly (ty, tl)} ->
+        instance_poly fixed tl ty
+    | ty ->
+        [], copy lbl.lbl_arg
+  in
+  cleanup_types ();
+  (vars, ty_arg, ty_res)
+
 (**** Instantiation with parameter substitution ****)
 
 let unify' = (* Forward declaration *)
@@ -771,7 +933,10 @@ let rec subst env level abbrev ty params args body =
     let body0 = newvar () in          (* Stub *)
     begin match ty with
       None      -> ()
-    | Some ({desc = Tconstr (path, _, _)} as ty) ->
+    | Some ({desc = Tconstr (path, tl, _)} as ty) ->
+        let abbrev =
+          if tl = [] && not !Clflags.principal then simple_abbrevs else abbrev
+        in
         memorize_abbrev abbrev path ty body0
     | _ ->
         assert false
@@ -856,7 +1021,10 @@ let expand_abbrev env ty =
   end;
   match ty with
     {desc = Tconstr (path, args, abbrev); level = level} ->
-      begin match find_expans path !abbrev with
+      let lookup_abbrev =
+        if args = [] && not !Clflags.principal then simple_abbrevs
+        else abbrev in
+      begin match find_expans path !lookup_abbrev with
         Some ty ->
           if level <> generic_level then
             begin try
@@ -1021,6 +1189,68 @@ let occur env ty0 ty =
       raise (match exn with Occur -> Unify [] | _ -> exn)
 
 
+                   (*****************************)
+                   (*  Polymorphic Unification  *)
+                   (*****************************)
+
+(* Since we cannot duplicate universal variables, unification must
+   be done at meta-level, using bindings in univar_pairs *)
+let rec unify_univar t1 t2 = function
+    (cl1, cl2) :: rem ->
+      let repr_univ = List.map (fun (t,o) -> repr t, o) in
+      let cl1 = repr_univ cl1 and cl2 = repr_univ cl2 in
+      begin try
+	let r1 = List.assq t1 cl1 in
+	match !r1 with
+	  Some t -> if t2 != repr t then raise (Unify [])
+	| None ->
+	    try
+	      let r2 = List.assq t2 cl2 in
+	      if !r2 <> None then raise (Unify []);
+	      r1 := Some t2; r2 := Some t1
+	    with Not_found ->
+	      raise (Unify [])
+      with Not_found ->
+	unify_univar t1 t2 rem
+      end
+  | [] -> raise (Unify [])
+
+module TypeMap = Map.Make (TypeOps)
+
+(* Test the occurence of free univars in a type *)
+(* that's way too expansive. Must do some kind of cacheing *)
+let occur_univar ty =
+  let visited = ref TypeMap.empty in
+  let rec occur_rec bound ty =
+    let ty = repr ty in
+    if ty.level >= lowest_level &&
+      if TypeSet.is_empty bound then
+        (ty.level <- pivot_level - ty.level; true)
+      else try
+        let bound' = TypeMap.find ty !visited in
+        if TypeSet.exists (fun x -> not (TypeSet.mem x bound)) bound' then
+          (visited := TypeMap.add ty (TypeSet.inter bound bound') !visited;
+           true)
+        else false
+      with Not_found ->
+        visited := TypeMap.add ty bound !visited;
+        true
+    then
+      match ty.desc with
+	Tunivar -> if not (TypeSet.mem ty bound) then raise Occur
+      |	Tpoly (ty, tyl) ->
+          let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in
+          occur_rec bound  ty
+      |	_ -> iter_type_expr (occur_rec bound) ty
+  in
+  try
+    occur_rec TypeSet.empty ty; unmark_type ty
+  with Occur ->
+    unmark_type ty; raise (Unify [])
+
+let univar_pairs = ref []
+
+
                               (*****************)
                               (*  Unification  *)
                               (*****************)
@@ -1097,13 +1327,17 @@ let rec unify env t1 t2 =
     | (Tconstr _, Tvar) when deep_occur t2 t1 ->
         unify2 env t1 t2
     | (Tvar, _) ->
-        occur env t1 t2;
+        occur env t1 t2; occur_univar t2;
         update_level env t1.level t2;
         t1.desc <- Tlink t2
     | (_, Tvar) ->
-        occur env t2 t1;
+        occur env t2 t1; occur_univar t1;
         update_level env t2.level t1;
         t2.desc <- Tlink t1
+    | (Tunivar, Tunivar) ->
+	unify_univar t1 t2 !univar_pairs;
+	update_level env t1.level t2;
+	t1.desc <- Tlink t2
     | (Tconstr (p1, [], a1), Tconstr (p2, [], a2))
           when Path.same p1 p2
             (* This optimization assumes that t1 does not expand to t2
@@ -1147,9 +1381,11 @@ and unify3 env t1 t1' t2 t2' =
   try
     begin match (d1, d2) with
       (Tvar, _) ->
-        ()
+        occur_univar t2
     | (_, Tvar) ->
-        occur env t2' (newty d1);
+        let td1 = newgenty d1 in
+        occur env t2' td1;
+        occur_univar td1;
         if t1 == t1' then begin
           (* The variable must be instantiated... *)
           let ty = newty2 t1'.level d1 in
@@ -1178,8 +1414,8 @@ and unify3 env t1 t1' t2 t2' =
         (* XXX One should do some kind of unification... *)
         begin match (repr t2').desc with
           Tobject (_, {contents = Some (_, va::_)})
-                when (repr va).desc = Tvar ->
-            ()  
+          when let va = repr va in va.desc = Tvar || va.desc = Tunivar ->
+            ()
         | Tobject (_, nm2) ->
             nm2 := !nm1
         | _ ->
@@ -1191,6 +1427,30 @@ and unify3 env t1 t1' t2 t2' =
         unify_fields env t1' t2'
     | (Tnil, Tnil) ->
         ()
+    | (Tpoly (t1, []), Tpoly (t2, [])) ->
+	unify env t1 t2
+    | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
+        if List.length tl1 <> List.length tl2 then raise (Unify []);
+	let old_univars = !univar_pairs in
+	let cl1 = List.map (fun t -> t, ref None) tl1
+	and cl2 = List.map (fun t -> t, ref None) tl2 in
+	univar_pairs := (cl1,cl2) :: (cl2,cl1) :: old_univars;
+	begin try
+	  unify env t1 t2;
+          let tl1 = List.map repr tl1 and tl2 = List.map repr tl2 in
+          List.iter
+            (fun t1 ->
+              if List.memq t1 tl2 then () else
+              try
+                let t2 =
+                  List.find (fun t2 -> not (List.memq (repr t2) tl1)) tl2 in
+                t2.desc <- Tlink t1
+              with Not_found -> assert false)
+            tl1;
+          univar_pairs := old_univars
+	with exn ->
+	  univar_pairs := old_univars; raise exn
+	end
     | (_, _) ->
         raise (Unify [])
     end;
@@ -1244,7 +1504,11 @@ and unify_fields env ty1 ty2 =          (* Optimization *)
   let (fields1, rest1) = flatten_fields ty1
   and (fields2, rest2) = flatten_fields ty2 in
   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
-  let va = newvar () in
+  let va =
+    if miss1 = [] then rest2
+    else if miss2 = [] then rest1
+    else newvar ()
+  in
   unify env (build_fields (repr ty1).level miss1 va) rest2;
   unify env rest1 (build_fields (repr ty2).level miss2 va);
   List.iter
@@ -1276,7 +1540,12 @@ and unify_row env row1 row2 =
               with Not_found -> (h,l)::hl)
             (List.map (fun (l,_) -> (hash_variant l, l)) row1.row_fields)
             (List.map fst r2));
-  let more = newty2 (min rm1.level rm2.level) Tvar
+  let more =
+    if row1.row_fixed then rm1 else
+    if row2.row_fixed then rm2 else
+    newgenvar ()
+  in update_level env (min rm1.level rm2.level) more;
+  let fixed = row1.row_fixed || row2.row_fixed
   and closed = row1.row_closed || row2.row_closed in
   let keep switch =
     List.for_all
@@ -1305,28 +1574,36 @@ and unify_row env row1 row2 =
   in
   let bound = row1.row_bound @ row2.row_bound in
   let row0 = {row_fields = []; row_more = more; row_bound = bound;
-              row_closed = closed; row_name = name} in
-  let more row rest =
+              row_closed = closed; row_fixed = fixed; row_name = name} in
+  let set_more row rest =
     let rest =
       if closed then
         filter_row_fields row.row_closed rest
       else rest in
-    if rest <> [] && row.row_closed then raise (Unify []);
-    let ty =
-      newty2 generic_level (Tvariant {row0 with row_fields = rest}) in
-    update_level env (repr row.row_more).level ty;
-    ty
+    if rest <> [] && (row.row_closed || row.row_fixed)
+    || closed && row.row_fixed && not row.row_closed
+    then raise (Unify []);
+    let rm = row_more row in
+    if row.row_fixed then
+      if row0.row_more == rm then () else rm.desc <- Tlink row0.row_more
+    else
+      let ty = newty2 generic_level (Tvariant {row0 with row_fields = rest}) in
+      update_level env rm.level ty;
+      rm.desc <- Tlink ty
   in
   let md1 = rm1.desc and md2 = rm2.desc in
   begin try
-    rm1.desc <- Tlink (more row1 r2);
-    rm2.desc <- Tlink (more row2 r1);
-    List.iter (fun (l,f1,f2) -> unify_row_field env f1 f2) pairs
+    set_more row1 r2;
+    set_more row2 r1;
+    List.iter
+      (fun (l,f1,f2) ->
+        unify_row_field env row1.row_fixed row2.row_fixed f1 f2)
+      pairs
   with exn ->
     rm1.desc <- md1; rm2.desc <- md2; raise exn
   end
 
-and unify_row_field env f1 f2 =
+and unify_row_field env fixed1 fixed2 f1 f2 =
   let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
   if f1 == f2 then () else
   match f1, f2 with
@@ -1350,19 +1627,19 @@ and unify_row_field env f1 f2 =
       let f1 = Reither(c1 || c2, tl1', m1 || m2, e)
       and f2 = Reither(c1 || c2, tl2', m1 || m2, e) in
       e1 := Some f1; e2 := Some f2
-  | Reither(false, tl, _, e1), Rpresent(Some t2) ->
+  | Reither(_, _, false, e1), Rabsent -> e1 := Some f2
+  | Rabsent, Reither(_, _, false, e2) -> e2 := Some f1
+  | Rabsent, Rabsent -> ()
+  | Reither(false, tl, _, e1), Rpresent(Some t2) when not fixed1 ->
       e1 := Some f2;
       (try List.iter (fun t1 -> unify env t1 t2) tl
       with exn -> e1 := None; raise exn)
-  | Rpresent(Some t1), Reither(false, tl, _, e2) ->
+  | Rpresent(Some t1), Reither(false, tl, _, e2) when not fixed2 ->
       e2 := Some f1;
       (try List.iter (unify env t1) tl
       with exn -> e2 := None; raise exn)
-  | Reither(true, [], _, e1), Rpresent None -> e1 := Some f2
-  | Rpresent None, Reither(true, [], _, e2) -> e2 := Some f1
-  | Reither(_, _, false, e1), Rabsent -> e1 := Some f2
-  | Rabsent, Reither(_, _, false, e2) -> e2 := Some f1
-  | Rabsent, Rabsent -> ()
+  | Reither(true, [], _, e1), Rpresent None when not fixed1 -> e1 := Some f2
+  | Rpresent None, Reither(true, [], _, e2) when not fixed2 -> e2 := Some f1
   | _ -> raise (Unify [])
 
 let unify env ty1 ty2 =
@@ -1371,7 +1648,31 @@ let unify env ty1 ty2 =
   with Unify trace ->
     raise (Unify (expand_trace env trace))
 
-let _ = unify' := unify
+let unify_var env t1 t2 =
+  let t1 = repr t1 and t2 = repr t2 in
+  if t1 == t2 then () else
+  match t1.desc with
+    Tvar ->
+      begin try
+	occur env t1 t2;
+	update_level env t1.level t2;
+	t1.desc <- Tlink t2
+      with Unify trace ->
+	raise (Unify ((t1,t2)::trace))
+      end
+  | _ ->
+      unify env t1 t2
+
+let _ = unify' := unify_var
+
+let unify_pairs env ty1 ty2 pairs =
+  univar_pairs := pairs;
+  unify env ty1 ty2
+
+let unify env ty1 ty2 =
+  univar_pairs := [];
+  unify env ty1 ty2
+
 
 (**** Special cases of unification ****)
 
@@ -1477,6 +1778,8 @@ let moregen_occur env level ty =
   with Occur ->
     unmark_type ty; raise (Unify [])
   end;
+  (* also check for free univars *)
+  occur_univar ty;
   update_level env level ty
 
 let rec moregen inst_nongen type_pairs env t1 t2 =
@@ -1487,7 +1790,9 @@ let rec moregen inst_nongen type_pairs env t1 t2 =
 
   try
     match (t1.desc, t2.desc) with
-      (Tvar, _) when if inst_nongen then t1.level <> generic_level - 1
+      (Tunivar, Tunivar) ->
+	unify_univar t1 t2 !univar_pairs
+    | (Tvar, _) when if inst_nongen then t1.level <> generic_level - 1
                                     else t1.level =  generic_level ->
         moregen_occur env t1.level t2;
         occur env t1 t2;
@@ -1532,6 +1837,19 @@ let rec moregen inst_nongen type_pairs env t1 t2 =
               moregen inst_nongen type_pairs env t1' t2''
           | (Tnil, Tnil) ->
               ()
+	  | (Tpoly (t1, []), Tpoly (t2, [])) ->
+	      moregen inst_nongen type_pairs env t1 t2
+	  | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
+	      let old_univars = !univar_pairs in
+	      let cl1 = List.map (fun t -> t, ref None) tl1
+	      and cl2 = List.map (fun t -> t, ref None) tl2 in
+	      univar_pairs := (cl1,cl2) :: (cl2,cl1) :: old_univars;
+	      begin try
+		moregen inst_nongen type_pairs env t1 t2;
+		univar_pairs := old_univars
+	      with exn ->
+		univar_pairs := old_univars; raise exn
+	      end
           | (_, _) ->
               raise (Unify [])
         end
@@ -1635,6 +1953,7 @@ let moregeneral env inst_nongen pat_sch subj_sch =
   current_level := generic_level;
   (* Duplicate generic variables *)
   let patt = instance pat_sch in
+  univar_pairs := [];
   let res =
     try moregen inst_nongen (TypePairs.create 13) env patt subj; true with
       Unify _ -> false
@@ -1704,6 +2023,21 @@ let rec eqtype rename type_pairs subst env t1 t2 =
               eqtype rename type_pairs subst env t1' t2''
           | (Tnil, Tnil) ->
               ()
+	  | (Tpoly (t1, []), Tpoly (t2, [])) ->
+	      eqtype rename type_pairs subst env t1 t2
+	  | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
+	      let old_univars = !univar_pairs in
+	      let cl1 = List.map (fun t -> t, ref None) tl1
+	      and cl2 = List.map (fun t -> t, ref None) tl2 in
+	      univar_pairs := (cl1,cl2) :: (cl2,cl1) :: old_univars;
+	      begin try eqtype rename type_pairs subst env t1 t2
+	      with exn ->
+		univar_pairs := old_univars;
+		raise exn
+	      end;
+	      univar_pairs := old_univars
+	  | (Tunivar, Tunivar) ->
+	      unify_univar t1 t2 !univar_pairs
           | (_, _) ->
               raise (Unify [])
         end
@@ -1772,6 +2106,7 @@ and eqtype_row rename type_pairs subst env row1 row2 =
 (* Two modes: with or without renaming of variables *)
 let equal env rename tyl1 tyl2 =
   try
+    univar_pairs := [];
     eqtype_list rename (TypePairs.create 11) (ref []) env tyl1 tyl2; true
   with
     Unify _ -> false
@@ -1843,6 +2178,7 @@ let match_class_types env pat_sch subj_sch =
   let type_pairs = TypePairs.create 53 in
   let old_level = !current_level in
   current_level := generic_level - 1;
+  univar_pairs := [];
   (*
      Generic variables are first duplicated with [instance].  So,
      their levels are lowered to [generic_level - 1].  The subject is
@@ -1971,6 +2307,7 @@ let rec equal_clty trace type_pairs subst env cty1 cty2 =
 (* XXX Correct ? (variables de type dans parametres et corps de classe *)
 let match_class_declarations env patt_params patt_type subj_params subj_type =
   let type_pairs = TypePairs.create 53 in
+  univar_pairs := [];
   let subst = ref [] in
   let sign1 = signature_of_class_type patt_type in
   let sign2 = signature_of_class_type subj_type in
@@ -2137,7 +2474,7 @@ let rec build_subtype env visited loops posi onlyloop t =
           let (ty1', _) = build_subtype env visited loops posi onlyloop ty1 in
           assert (t''.desc = Tvar);
           t''.desc <- Tobject (ty1', ref None);
-          (try unify env ty t with Unify _ -> assert false);
+          (try unify_var env ty t with Unify _ -> assert false);
           (t'', true)
       | _ -> raise Not_found
       with Not_found -> build_subtype env visited loops posi onlyloop t'
@@ -2191,7 +2528,7 @@ let rec build_subtype env visited loops posi onlyloop t =
       if posi && fields = [] then (t, false) else
       let row =
         { row_fields = List.map fst fields; row_more = newvar();
-          row_bound = !bound; row_closed = posi;
+          row_bound = !bound; row_closed = posi; row_fixed = false;
           row_name = if List.exists snd fields then None else row.row_name }
       in
       (newty (Tvariant row), true)
@@ -2217,6 +2554,12 @@ let rec build_subtype env visited loops posi onlyloop t =
         (t, false)
   | Tsubst _ | Tlink _ ->
       assert false
+  | Tpoly(t1, tl) ->
+      let (t1', c) = build_subtype env visited loops posi onlyloop t1 in
+      if c then (newty (Tpoly(t1', tl)), true)
+      else (t, false)
+  | Tunivar ->
+      (t, false)
 
 let enlarge_type env ty =
   let (ty', _) = build_subtype env [] [] true false ty in
@@ -2255,7 +2598,7 @@ let rec subtype_rec env trace t1 t2 cstrs =
     TypePairs.add subtypes (t1, t2) ();
     match (t1.desc, t2.desc) with
       (Tvar, _) | (_, Tvar) ->
-        (trace, t1, t2)::cstrs
+        (trace, t1, t2, !univar_pairs)::cstrs
     | (Tarrow(l1, t1, u1, _), Tarrow(l2, t2, u2, _)) when l1 = l2
       || !Clflags.classic && not (is_optional l1 || is_optional l2) ->
         let cstrs = subtype_rec env ((t2, t1)::trace) t2 t1 cstrs in
@@ -2276,19 +2619,19 @@ let rec subtype_rec env trace t1 t2 cstrs =
               if co then
                 if cn then
                   (trace, newty2 t1.level (Ttuple[t1]),
-                   newty2 t2.level (Ttuple[t2])) :: cstrs 
+                   newty2 t2.level (Ttuple[t2]), !univar_pairs) :: cstrs 
                 else subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
               else
                 if cn then subtype_rec env ((t2, t1)::trace) t2 t1 cstrs
                 else cstrs)
             cstrs decl.type_variance (List.combine tl1 tl2)
         with Not_found ->
-          (trace, t1, t2)::cstrs
+          (trace, t1, t2, !univar_pairs)::cstrs
         end
     | (Tobject (f1, _), Tobject (f2, _))
               when opened_object f1 && opened_object f2 ->
         (* Same row variable implies same object. *)
-        (trace, t1, t2)::cstrs
+        (trace, t1, t2, !univar_pairs)::cstrs
     | (Tobject (f1, _), Tobject (f2, _)) ->
         subtype_fields env trace f1 f2 cstrs
     | (Tvariant row1, Tvariant row2) ->
@@ -2311,10 +2654,20 @@ let rec subtype_rec env trace t1 t2 cstrs =
               | _ -> raise Exit)
             cstrs pairs
         with Exit ->
-          (trace, t1, t2)::cstrs
+          (trace, t1, t2, !univar_pairs)::cstrs
         end
+    | (Tpoly (u1, []), Tpoly (u2, [])) ->
+	subtype_rec env trace u1 u2 cstrs
+    | (Tpoly (t1, tl1), Tpoly (t2,tl2)) ->
+	let old_univars = !univar_pairs in
+	let cl1 = List.map (fun t -> t, ref None) tl1
+	and cl2 = List.map (fun t -> t, ref None) tl2 in
+	univar_pairs := (cl1,cl2) :: (cl2,cl1) :: old_univars;
+	let cstrs = subtype_rec env trace t1 t2 cstrs in
+	univar_pairs := old_univars;
+	cstrs
     | (_, _) ->
-        (trace, t1, t2)::cstrs
+        (trace, t1, t2, !univar_pairs)::cstrs
   end
 
 and subtype_list env trace tl1 tl2 cstrs =
@@ -2328,11 +2681,13 @@ and subtype_fields env trace ty1 ty2 cstrs =
   let (fields1, rest1) = flatten_fields ty1 in
   let (fields2, rest2) = flatten_fields ty2 in
   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
-  [(trace, rest1, build_fields (repr ty2).level miss2 (newvar ()))]
-    @
+  (trace, rest1, build_fields (repr ty2).level miss2 (newvar ()),
+   !univar_pairs)
+    ::
   begin match rest2.desc with
     Tnil   -> []
-  | _      -> [(trace, build_fields (repr ty1).level miss1 rest1, rest2)]
+  | _      ->
+      [trace, build_fields (repr ty1).level miss1 rest1, rest2, !univar_pairs]
   end
     @
   (List.fold_left
@@ -2343,14 +2698,15 @@ and subtype_fields env trace ty1 ty2 cstrs =
 
 let subtype env ty1 ty2 =
   TypePairs.clear subtypes;
+  univar_pairs := [];
   (* Build constraint set. *)
   let cstrs = subtype_rec env [(ty1, ty2)] ty1 ty2 [] in
   TypePairs.clear subtypes;
   (* Enforce constraints. *)
   function () ->
     List.iter
-      (function (trace0, t1, t2) ->
-         try unify env t1 t2 with Unify trace ->
+      (function (trace0, t1, t2, pairs) ->
+         try unify_pairs env t1 t2 pairs with Unify trace ->
            raise (Subtype (expand_trace env (List.rev trace0),
                            List.tl (List.tl trace))))
       (List.rev cstrs)
@@ -2444,7 +2800,7 @@ let rec normalize_type_rec env ty =
         | Some (n, v :: l) ->
             let v' = repr v in
             begin match v'.desc with
-            | Tvar -> if v' != v then nm := Some (n, v' :: l)
+            | Tvar|Tunivar -> if v' != v then nm := Some (n, v' :: l)
             | Tnil -> ty.desc <- Tconstr (n, l, ref Mnil)
             | _ -> nm := None
             end
@@ -2484,7 +2840,7 @@ let normalize_type env ty =
 let rec nondep_type_rec env id ty =
   let ty = repr ty in
   match ty.desc with
-    Tvar     -> ty
+    Tvar | Tunivar -> ty
   | Tsubst ty -> ty
   | _ ->
     let desc = ty.desc in
@@ -2532,7 +2888,8 @@ let rec nondep_type_rec env id ty =
               more.desc <- ty.desc;
               let more' = if static then newgenvar () else more in
               (* Return a new copy *)
-              let row = copy_row (nondep_type_rec env id) row true more' in
+              let row =
+                copy_row (nondep_type_rec env id) true row true more' in
               match row.row_name with
                 Some (p, tl) when Path.isfree id p ->
                   Tvariant {row with row_name = None}
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 4510dfafc..ce590e04a 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -83,6 +83,15 @@ val generalize: type_expr -> unit
         (* Generalize in-place the given type *)
 val iterative_generalization: int -> type_expr list -> type_expr list
         (* Efficient repeated generalization of a type *)
+val generalize_expansive: type_expr -> unit
+        (* Generalize the structure of a type, making variables
+           non-generalizable *)
+val generalize_global: type_expr -> unit
+        (* Same, but variables are lowered to !global_level *)
+val generalize_structure: type_expr -> unit
+        (* Same, but variables are only lowered to !current_level *)
+val generalize_spine: type_expr -> unit
+        (* Special function to generalize a method during inference *)
 val make_nongen: type_expr -> unit
         (* Make non-generalizable the given type *)
 val correct_levels: type_expr -> type_expr
@@ -98,8 +107,6 @@ val instance_list: type_expr list -> type_expr list
 val instance_constructor:
         constructor_description -> type_expr list * type_expr
         (* Same, for a constructor *)
-val instance_label: label_description -> type_expr * type_expr
-        (* Same, for a label *)
 val instance_parameterized_type:
         type_expr list -> type_expr -> type_expr list * type_expr
 val instance_parameterized_type_2:
@@ -107,6 +114,12 @@ val instance_parameterized_type_2:
         type_expr list * type_expr list * type_expr
 val instance_class:
         type_expr list -> class_type -> type_expr list * class_type
+val instance_poly:
+        bool -> type_expr list -> type_expr -> type_expr list * type_expr
+        (* Take an instance of a type scheme containing free univars *)
+val instance_label:
+        bool -> label_description -> type_expr list * type_expr * type_expr
+        (* Same, for a label *)
 val apply:
         Env.t -> type_expr list -> type_expr -> type_expr list -> type_expr
         (* [apply [p1...pN] t [a1...aN]] match the arguments [ai] to
@@ -120,6 +133,9 @@ val enforce_constraints: Env.t -> type_expr -> unit
 
 val unify: Env.t -> type_expr -> type_expr -> unit
         (* Unify the two types given. Raise [Unify] if not possible. *)
+val unify_var: Env.t -> type_expr -> type_expr -> unit
+        (* Same as [unify], but allow free univars when first type
+           is a variable. *)
 val filter_arrow: Env.t -> type_expr -> label -> type_expr * type_expr
         (* A special case of unification (with l:'a -> 'b). *)
 val filter_method: Env.t -> string -> private_flag -> type_expr -> type_expr
diff --git a/typing/oprint.ml b/typing/oprint.ml
index e7042d124..4a16f45a8 100644
--- a/typing/oprint.ml
+++ b/typing/oprint.ml
@@ -116,10 +116,20 @@ let rec print_list pr sep ppf =
 let pr_present =
   print_list (fun ppf s -> fprintf ppf "`%s" s) (fun ppf -> fprintf ppf "@ ")
 
+let pr_vars =
+  print_list (fun ppf s -> fprintf ppf "'%s" s) (fun ppf -> fprintf ppf "@ ")
+
 let rec print_out_type ppf =
   function
-    Otyp_alias (ty, s) -> fprintf ppf "@[%a as '%s@]" print_out_type ty s
-  | ty -> print_out_type_1 ppf ty
+  | Otyp_alias (ty, s) ->
+      fprintf ppf "@[%a as '%s@]" print_out_type ty s
+  | Otyp_poly (sl, ty) ->
+      fprintf ppf "@[<hov 2>%a.@ %a@]"
+        pr_vars sl
+        print_out_type ty
+  | ty ->
+      print_out_type_1 ppf ty
+
 and print_out_type_1 ppf =
   function
     Otyp_arrow (lab, ty1, ty2) ->
@@ -158,10 +168,10 @@ and print_simple_out_type ppf =
       in
       fprintf ppf "%s[%s@[<hv>@[<hv>%a@]%a]@]" (if non_gen then "_" else "")
         (if closed then if tags = None then " " else "< "
-         else if tags = None then "> "
-         else "? ")
-        print_fields row_fields print_present tags
-  | Otyp_alias (_, _) | Otyp_arrow (_, _, _) | Otyp_tuple _ as ty ->
+         else if tags = None then "> " else "? ")
+        print_fields row_fields
+        print_present tags
+  | Otyp_alias _ | Otyp_poly _ | Otyp_arrow _ | Otyp_tuple _ as ty ->
       fprintf ppf "@[<1>(%a)@]" print_out_type ty
   | Otyp_abstract | Otyp_sum _ | Otyp_record _ | Otyp_manifest (_, _) -> ()
 and print_fields rest ppf =
diff --git a/typing/outcometree.mli b/typing/outcometree.mli
index b1be465c4..6ab7cdfd8 100644
--- a/typing/outcometree.mli
+++ b/typing/outcometree.mli
@@ -56,6 +56,7 @@ type out_type =
   | Otyp_var of bool * string
   | Otyp_variant of
       bool * out_variant * bool * (string list) option
+  | Otyp_poly of string list * out_type
 and out_variant =
   | Ovar_fields of (string * bool * out_type list) list
   | Ovar_name of out_ident * out_type list
diff --git a/typing/parmatch.ml b/typing/parmatch.ml
index 9ef2b7c4a..0a63dc632 100644
--- a/typing/parmatch.ml
+++ b/typing/parmatch.ml
@@ -380,7 +380,7 @@ let full_match tdefs force env =  match env with
         env
     in
     let row = Btype.row_repr row in
-    if force then begin
+    if force && not row.row_fixed then begin
       (* force=true, we are called from check_partial, and must close *)
       let (ok, nm) =
         List.fold_left
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 8b28c49da..3bece5747 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -24,6 +24,16 @@ open Types
 open Btype
 open Outcometree
 
+(* Redefine it here since goal differs *)
+
+let rec opened_object ty =
+  match (repr ty).desc with
+    Tobject (t, _)     -> opened_object t
+  | Tfield(_, _, _, t) -> opened_object t
+  | Tvar               -> true
+  | Tunivar            -> true
+  | _                  -> false
+
 (* Print a long identifier *)
 
 let rec longident ppf = function
@@ -83,21 +93,35 @@ let name_of_type t =
 
 let check_name_of_type t = ignore(name_of_type t)
 
-let print_name_of_type ppf t = fprintf ppf "%s" (name_of_type t)
-
-let visited_objects = ref ([] : type_expr list)
-let aliased = ref ([] : type_expr list)
+let non_gen_mark sch ty =
+  if sch && ty.desc = Tvar && ty.level <> generic_level then "_" else "" 
 
-let is_aliased ty = List.memq ty !aliased
-let add_alias ty =
-  if not (is_aliased ty) then aliased := ty :: !aliased
+let print_name_of_type sch ppf t =
+  fprintf ppf "'%s%s" (non_gen_mark sch t) (name_of_type t)
 
 let proxy ty =
   let ty = repr ty in
   match ty.desc with
   | Tvariant row -> Btype.row_more row
+  | Tobject (ty, _) ->
+      let rec proxy_obj ty =
+        let ty = repr ty in
+        match ty.desc with
+          Tfield (_, _, _, ty)  -> proxy_obj ty
+        | Tvar | Tnil | Tunivar -> ty
+        | _ -> assert false
+      in proxy_obj ty
   | _ -> ty
 
+let visited_objects = ref ([] : type_expr list)
+let aliased = ref ([] : type_expr list)
+let delayed = ref ([] : type_expr list)
+
+let is_aliased ty = List.memq (proxy ty) !aliased
+let add_alias ty =
+  let px = proxy ty in
+  if not (is_aliased px) then aliased := px :: !aliased
+
 let namable_row row =
   row.row_name <> None &&
   List.for_all
@@ -139,9 +163,14 @@ let rec mark_loops_rec visited ty =
             visited_objects := px :: !visited_objects;
           begin match !nm with
           | None ->
-              mark_loops_rec visited fi
+              let fields, _ = flatten_fields fi in
+              List.iter
+                (fun (_, kind, ty) ->
+                  if field_kind_repr kind = Fpresent then
+                    mark_loops_rec visited ty)
+                fields
           | Some (_, l) ->
-              List.iter (mark_loops_rec visited) l
+              List.iter (mark_loops_rec visited) (List.tl l)
           end
         end
     | Tfield(_, kind, ty1, ty2) when field_kind_repr kind = Fpresent ->
@@ -151,22 +180,26 @@ let rec mark_loops_rec visited ty =
     | Tnil -> ()
     | Tsubst ty -> mark_loops_rec visited ty
     | Tlink _ -> fatal_error "Printtyp.mark_loops_rec (2)"
+    | Tpoly (ty, tyl) ->
+	List.iter (fun t -> add_alias t) tyl;
+	mark_loops_rec visited ty
+    | Tunivar -> ()
 
 let mark_loops ty =
   normalize_type Env.empty ty;
   mark_loops_rec [] ty;;
 
 let reset_loop_marks () =
-  visited_objects := []; aliased := []
+  visited_objects := []; aliased := []; delayed := []
 
 let reset () =
   reset_names (); reset_loop_marks ()
 
 let reset_and_mark_loops ty =
-  reset (); mark_loops ty;;
+  reset (); mark_loops ty
 
 let reset_and_mark_loops_list tyl =
- reset (); List.iter mark_loops tyl;;
+  reset (); List.iter mark_loops tyl
 
 (* Disabled in classic mode when printing an unification error *)
 let print_labels = ref true
@@ -176,12 +209,12 @@ let print_label ppf l =
 let rec tree_of_typexp sch ty =
   let ty = repr ty in
   let px = proxy ty in
-  if List.mem_assq px !names then
-   let mark = if ty.desc = Tvar then is_non_gen sch px else false in
+  if List.mem_assq px !names && not (List.memq px !delayed) then
+   let mark = is_non_gen sch px in
    Otyp_var (mark, name_of_type px) else
 
   let pr_typ () =
-   (match ty.desc with
+    match ty.desc with
     | Tvar ->
         Otyp_var (is_non_gen sch ty, name_of_type ty)
     | Tarrow(l, ty1, ty2, _) ->
@@ -239,13 +272,25 @@ let rec tree_of_typexp sch ty =
             Otyp_variant (non_gen, Ovar_fields fields, row.row_closed, tags)
         end
     | Tobject (fi, nm) ->
-        tree_of_typobject sch ty fi nm
+        tree_of_typobject sch fi nm
     | Tsubst ty ->
         tree_of_typexp sch ty
     | Tlink _ | Tnil | Tfield _ ->
         fatal_error "Printtyp.tree_of_typexp"
-   ) in
-  if is_aliased px then begin
+    | Tpoly (ty, []) ->
+	tree_of_typexp sch ty
+    | Tpoly (ty, tyl) ->
+        let tyl = List.map repr tyl in
+        let tyl = List.filter is_aliased tyl in
+        if tyl = [] then tree_of_typexp sch ty else
+        let tl = List.map name_of_type tyl in
+        delayed := tyl @ !delayed;
+        Otyp_poly (tl, tree_of_typexp sch ty)
+    | Tunivar ->
+        Otyp_var (false, name_of_type ty)
+  in
+  if List.memq px !delayed then delayed := List.filter ((!=) px) !delayed;
+  if is_aliased px && ty.desc <> Tvar && ty.desc <> Tunivar then begin
     check_name_of_type px;
     Otyp_alias (pr_typ (), name_of_type px) end
   else pr_typ ()
@@ -266,7 +311,7 @@ and tree_of_typlist sch = function
       let tr = tree_of_typexp sch ty in
       tr :: tree_of_typlist sch tyl
 
-and tree_of_typobject sch ty fi nm =
+and tree_of_typobject sch fi nm =
   begin match !nm with
   | None ->
       let pr_fields fi =
@@ -283,8 +328,8 @@ and tree_of_typobject sch ty fi nm =
         tree_of_typfields sch rest sorted_fields in
       let (fields, rest) = pr_fields fi in
       Otyp_object (fields, rest)
-  | Some (p, {desc = Tvar} :: tyl) ->
-      let non_gen = is_non_gen sch ty in
+  | Some (p, ty :: tyl) ->
+      let non_gen = is_non_gen sch (repr ty) in
       let args = tree_of_typlist sch tyl in
       Otyp_class (non_gen, tree_of_path p, args)
   | _ ->
@@ -292,13 +337,13 @@ and tree_of_typobject sch ty fi nm =
   end
 
 and is_non_gen sch ty =
-    sch && ty.level <> generic_level
+    sch && ty.desc = Tvar && ty.level <> generic_level
 
 and tree_of_typfields sch rest = function
   | [] ->
       let rest =
         match rest.desc with
-        | Tvar -> Some (is_non_gen sch rest)
+        | Tvar | Tunivar -> Some (is_non_gen sch rest)
         | Tnil -> None
         | _ -> fatal_error "typfields (1)"
       in
@@ -362,7 +407,7 @@ let rec tree_of_type_decl id decl =
 
   let params = filter_params decl.type_params in
 
-  aliased := params @ !aliased;
+  List.iter add_alias params;
   List.iter mark_loops params;
   List.iter check_name_of_type (List.map proxy params);
   begin match decl.type_manifest with
@@ -485,6 +530,12 @@ let tree_of_metho sch concrete csil (lab, kind, ty) =
   end
   else csil
 
+let prepare_class_field ty =
+  let ty = repr ty in
+  match ty.desc with
+    Tpoly(ty, _) -> mark_loops ty
+  | _ -> mark_loops ty
+
 let rec prepare_class_type params = function
   | Tcty_constr (p, tyl, cty) ->
       let sty = Ctype.self_type cty in
@@ -501,11 +552,11 @@ let rec prepare_class_type params = function
       let sty = repr sign.cty_self in
       (* Self may have a name *)
       if List.memq sty !visited_objects then add_alias sty
-      else visited_objects := sty :: !visited_objects;
+      else visited_objects := proxy sty :: !visited_objects;
       let (fields, _) =
         Ctype.flatten_fields (Ctype.object_fields sign.cty_self)
       in
-      List.iter (fun (_, _, ty) -> mark_loops ty) fields;
+      List.iter (fun (_, _, ty) -> prepare_class_field ty) fields;
       Vars.iter (fun _ (_, ty) -> mark_loops ty) sign.cty_vars
   | Tcty_fun (_, ty, cty) ->
       mark_loops ty;
@@ -524,7 +575,8 @@ let rec tree_of_class_type sch params =
   | Tcty_signature sign ->
       let sty = repr sign.cty_self in
       let self_ty =
-        if is_aliased sty then Some (Otyp_var (false, name_of_type sty))
+        if is_aliased sty then
+          Some (Otyp_var (false, name_of_type (proxy sty)))
         else None
       in
       let (fields, _) =
@@ -574,13 +626,13 @@ let tree_of_class_declaration id cl =
   let params = filter_params cl.cty_params in
 
   reset ();
-  aliased := params @ !aliased;
+  List.iter add_alias params;
   prepare_class_type params cl.cty_type;
   let sty = self_type cl.cty_type in
   List.iter mark_loops params;
 
   List.iter check_name_of_type (List.map proxy params);
-  if is_aliased sty then check_name_of_type sty;
+  if is_aliased sty then check_name_of_type (proxy sty);
 
   let vir_flag = cl.cty_new = None in
   Osig_class
@@ -600,7 +652,7 @@ let tree_of_cltype_declaration id cl =
   List.iter mark_loops params;
 
   List.iter check_name_of_type (List.map proxy params);
-  if is_aliased sty then check_name_of_type sty;
+  if is_aliased sty then check_name_of_type (proxy sty);
 
   let sign = Ctype.signature_of_class_type cl.clty_type in
 
diff --git a/typing/subst.ml b/typing/subst.ml
index 0c04771cb..66646c157 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -58,17 +58,17 @@ let type_path s = function
 let new_id = ref (-1)
 let reset_for_saving () = new_id := -1
 
-let newpersvar () =
-  decr new_id; { desc = Tvar; level = generic_level; id = !new_id }
+let newpersty desc =
+  decr new_id; { desc = desc; level = generic_level; id = !new_id }
 
 (* Similar to [Ctype.nondep_type_rec]. *)
 let rec typexp s ty =
   let ty = repr ty in
   match ty.desc with
-    Tvar ->
+    Tvar | Tunivar ->
       if s.for_saving then
-        let ty' = newpersvar () in
-        save_desc ty Tvar; ty.desc <- Tsubst ty'; ty'
+        let ty' = newpersty ty.desc in
+        save_desc ty ty.desc; ty.desc <- Tsubst ty'; ty'
       else ty
   | Tsubst ty ->
       ty
@@ -80,7 +80,7 @@ let rec typexp s ty =
     let desc = ty.desc in
     save_desc ty desc;
     (* Make a stub *)
-    let ty' = if s.for_saving then newpersvar () else newgenvar () in
+    let ty' = if s.for_saving then newpersty Tvar else newgenvar () in
     ty.desc <- Tsubst ty';
     ty'.desc <-
       begin match desc with
@@ -97,20 +97,25 @@ let rec typexp s ty =
           let more = repr row.row_more in
           (* We must substitute in a subtle way *)
           begin match more.desc with
-            Tsubst ty2 ->
+            Tsubst ({desc=Tvariant _} as ty2) ->
               (* This variant type has been already copied *)
               ty.desc <- Tsubst ty2; (* avoid Tlink in the new type *)
               Tlink ty2
           | _ ->
               let static = static_row row in
+              (* Various cases for the row variable *)
+              let more' =
+                match more.desc with Tsubst ty -> ty
+                | _ ->
+                    if s.for_saving then newpersty more.desc else
+                    if static then newgenvar () else more
+              in
               (* Register new type first for recursion *)
               save_desc more more.desc;
               more.desc <- ty.desc;
-              let more' =
-                if s.for_saving then newpersvar () else
-                if static then newgenvar () else more in
               (* Return a new copy *)
-              let row = copy_row (typexp s) row (not s.for_saving) more' in
+              let row =
+                copy_row (typexp s) true row (not s.for_saving) more' in
               let row =
                 if s.for_saving then {row with row_bound = []} else row in
               match row.row_name with
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 3ede8f6fc..511ae4f67 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(* $Id$ *)
+(* typeclass.ml,v 1.57.4.6 2002/02/15 14:26:04 garrigue Exp *)
 
 open Misc
 open Parsetree
@@ -233,6 +233,19 @@ let virtual_method val_env meths self_type lab priv sty loc =
   try Ctype.unify val_env ty ty' with Ctype.Unify trace ->
     raise(Error(loc, Method_type_mismatch (lab, trace)))
 
+let declare_method val_env meths self_type lab priv sty loc =
+  let (_, ty') =
+     Ctype.filter_self_method val_env lab priv meths self_type
+  in
+  let ty =
+    match sty.ptyp_desc with
+      Ptyp_poly ([],sty) -> transl_simple_type_univars val_env sty
+    | _                  -> transl_simple_type val_env false sty
+  in
+  begin try Ctype.unify val_env ty ty' with Ctype.Unify trace ->
+    raise(Error(loc, Method_type_mismatch (lab, trace)))
+  end
+
 let type_constraint val_env sty sty' loc =
   let ty  = transl_simple_type val_env false sty in
   let ty' = transl_simple_type val_env false sty' in
@@ -279,11 +292,11 @@ let rec class_type_field env self_type meths (val_sig, concr_meths) =
       (Vars.add lab (mut, ty) val_sig, concr_meths)
 
   | Pctf_virt (lab, priv, sty, loc) ->
-      virtual_method env meths self_type lab priv sty loc;
+      declare_method env meths self_type lab priv sty loc;
       (val_sig, concr_meths)
 
   | Pctf_meth (lab, priv, sty, loc)  ->
-      virtual_method env meths self_type lab priv sty loc;
+      declare_method env meths self_type lab priv sty loc;
       (val_sig, Concr.add lab concr_meths)
 
   | Pctf_cstr (sty, sty', loc) ->
@@ -399,10 +412,15 @@ let rec class_field cl_num self_type meths vars
   | Pcf_val (lab, mut, sexp, loc) ->
       if StringSet.mem lab inh_vals then
         Location.prerr_warning loc (Warnings.Hide_instance_variable lab);
+      if !Clflags.principal then Ctype.begin_def ();
       let exp =
         try type_exp val_env sexp with Ctype.Unify [(ty, _)] ->
           raise(Error(loc, Make_nongen_seltype ty))
       in
+      if !Clflags.principal then begin
+        Ctype.end_def ();
+        Ctype.generalize_structure exp.exp_type
+      end;
       let (id, val_env, met_env, par_env) =
         enter_val cl_num vars lab mut exp.exp_type val_env met_env par_env
       in
@@ -414,23 +432,38 @@ let rec class_field cl_num self_type meths vars
       (val_env, met_env, par_env, fields, concr_meths, inh_vals)
 
   | Pcf_meth (lab, priv, expr, loc)  ->
-      let meth_expr = make_method cl_num expr in
-      Ctype.raise_nongen_level ();
       let (_, ty) =
         Ctype.filter_self_method val_env lab priv meths self_type
       in
-      let meth_type = Ctype.newvar () in
-      let (obj_ty, res_ty) = Ctype.filter_arrow val_env meth_type "" in
-      Ctype.unify val_env obj_ty self_type;
-      Ctype.unify val_env res_ty ty;
-      let ty' = type_approx met_env expr in
-      begin try Ctype.unify met_env ty' res_ty with Ctype.Unify trace ->
-        raise(Typecore.Error(expr.pexp_loc, Expr_type_clash(trace)))
+      begin try match expr.pexp_desc with
+	Pexp_poly (sbody, sty) ->
+	  begin match sty with None -> ()
+	  | Some sty ->
+	      Ctype.unify val_env
+		(Typetexp.transl_simple_type val_env false sty) ty
+	  end;
+	  begin match (Ctype.repr ty).desc with
+	    Tvar ->
+	      let ty' = Ctype.newvar () in
+	      Ctype.unify val_env (Ctype.newty (Tpoly (ty', []))) ty;
+	      Ctype.unify val_env (type_approx val_env sbody) ty'
+	  | Tpoly (ty1, tl) ->
+	      let _, ty1' = Ctype.instance_poly false tl ty1 in
+	      let ty2 = type_approx val_env sbody in
+	      Ctype.unify val_env ty2 ty1'
+	  | _ -> assert false
+	  end
+      |	_ -> assert false
+      with Ctype.Unify trace ->
+	raise(Error(loc, Method_type_mismatch (lab, trace)))
       end;
-      Ctype.end_def ();
+      let meth_expr = make_method cl_num expr in
       let vars_local = !vars in
+
       let field =
         lazy begin
+          let meth_type =
+            Ctype.newty (Tarrow("", self_type, Ctype.instance ty, Cok)) in
           Ctype.raise_nongen_level ();
           vars := vars_local;
           let texp = type_expect met_env meth_expr meth_type in
@@ -480,10 +513,9 @@ let rec class_field cl_num self_type meths vars
       let field =
         lazy begin
           Ctype.raise_nongen_level ();
-          let meth_type = Ctype.newvar () in
-          let (obj_ty, res_ty) = Ctype.filter_arrow val_env meth_type "" in
-          Ctype.unify val_env obj_ty self_type;
-          Ctype.unify val_env res_ty (Ctype.instance Predef.type_unit);
+          let meth_type =
+            Ctype.newty
+              (Tarrow ("", self_type, Ctype.instance Predef.type_unit, Cok)) in
           vars := vars_local;
           let texp = type_expect met_env expr meth_type in
           Ctype.end_def ();
@@ -518,9 +550,16 @@ and class_structure cl_num val_env met_env (spat, str) =
       (val_env, meth_env, par_env, [], Concr.empty, StringSet.empty)
       str
   in
+  Ctype.unify val_env self_type (Ctype.newvar ());
+  let methods =
+    if !Clflags.principal then
+      fst (Ctype.flatten_fields (Ctype.object_fields self_type))
+    else [] in
+  List.iter (fun (_,_,ty) -> Ctype.generalize_spine ty) methods;
   let vars_final = !vars in
   let fields = List.map Lazy.force (List.rev fields) in
   vars := vars_final;
+  List.iter (fun (_,_,ty) -> Ctype.unify val_env ty (Ctype.newvar ())) methods;
 
   {cl_field = fields;
    cl_meths = Meths.map (function (id, ty) -> id) !meths},
@@ -592,10 +631,15 @@ and class_expr cl_num val_env met_env scl =
                   Pcl_let(Default, [spat, smatch], sbody)})}
       in
       class_expr cl_num val_env met_env sfun
-  | Pcl_fun (l, _, spat, scl') ->
+  | Pcl_fun (l, None, spat, scl') ->
+      if !Clflags.principal then Ctype.begin_def ();
       let (pat, pv, val_env, met_env) =
         Typecore.type_class_arg_pattern cl_num val_env met_env l spat
       in
+      if !Clflags.principal then begin
+        Ctype.end_def ();
+        iter_pattern (fun {pat_type=ty} -> Ctype.generalize_structure ty) pat
+      end;
       let pv =
         List.map
           (function (id, id', ty) ->
@@ -625,7 +669,7 @@ and class_expr cl_num val_env met_env scl =
           (Warnings.Other "This optional argument cannot be erased");
       {cl_desc = Tclass_fun (pat, pv, cl, partial);
        cl_loc = scl.pcl_loc;
-       cl_type = Tcty_fun (l, pat.pat_type, cl.cl_type)}
+       cl_type = Tcty_fun (l, Ctype.instance pat.pat_type, cl.cl_type)}
   | Pcl_apply (scl', sargs) ->
       let cl = class_expr cl_num val_env met_env scl' in
       let rec nonopt_labels ls ty_fun =
@@ -826,6 +870,7 @@ let rec initial_env define_class approx
   
   (* Temporary type for the class constructor *)
   let constr_type = approx cl.pci_expr in
+  if !Clflags.principal then Ctype.generalize_spine constr_type;
   let dummy_cty =
     Tcty_signature
       { cty_self = Ctype.newvar ();
@@ -948,7 +993,9 @@ let class_infos define_class kind
 
   (* Type of the class constructor *)
   begin try
-    Ctype.unify env (constructor_type constr obj_type) constr_type
+    Ctype.unify env
+      (constructor_type constr obj_type)
+      (Ctype.instance constr_type)
   with Ctype.Unify trace ->
     raise(Error(cl.pci_loc,
                 Constructor_type_mismatch (cl.pci_name, trace)))
@@ -998,7 +1045,7 @@ let class_infos define_class kind
      cty_new =
        match cl.pci_virt with
          Virtual  -> None
-       | Concrete -> Some constr_type}
+       | Concrete -> Some (Ctype.instance constr_type)}
   in
   let obj_abbr =
     {type_params = obj_params;
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 025f6716e..b585295c9 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -55,6 +55,7 @@ type error =
   | Masked_instance_variable of Longident.t
   | Not_a_variant_type of Longident.t
   | Incoherent_label_order
+  | Less_general of string * (type_expr * type_expr) list
 
 exception Error of Location.t * error
 
@@ -177,18 +178,19 @@ let rec build_as_type env p =
   | Tpat_variant(l, p', _) ->
       let ty = may_map (build_as_type env) p' in
       newty (Tvariant{row_fields=[l, Rpresent ty]; row_more=newvar();
-                      row_bound=[]; row_name=None; row_closed=false})
+                      row_bound=[]; row_name=None;
+                      row_fixed=false; row_closed=false})
   | Tpat_record lpl ->
       let lbl = fst(List.hd lpl) in
       let ty = newvar () in
       let do_label lbl =
-        let ty_arg, ty_res = instance_label lbl in
+        let _, ty_arg, ty_res = instance_label false lbl in
         unify_pat env {p with pat_type = ty} ty_res;
         if lbl.lbl_mut = Immutable && List.mem_assoc lbl lpl then begin
           let arg = List.assoc lbl lpl in
           unify_pat env {arg with pat_type = build_as_type env arg} ty_arg
         end else begin
-          let ty_arg', ty_res' = instance_label lbl in
+          let _, ty_arg', ty_res' = instance_label false lbl in
           unify env ty_arg ty_arg';
           unify_pat env p ty_res'
         end in
@@ -242,7 +244,7 @@ let build_or_pat env loc lid =
       ([],[]) fields in
   let row =
     { row_fields = List.rev fields; row_more = newvar(); row_bound = !bound;
-      row_closed = false; row_name = Some (path, tyl) }
+      row_closed = false; row_fixed = false; row_name = Some (path, tyl) }
   in
   let ty = newty (Tvariant row) in
   let pats =
@@ -326,6 +328,7 @@ let rec type_pat env sp =
                   row_bound = arg_type;
                   row_closed = false;
                   row_more = newvar ();
+                  row_fixed = false;
                   row_name = None } in
       { pat_desc = Tpat_variant(l, arg, row);
         pat_loc = sp.ppat_loc;
@@ -346,7 +349,7 @@ let rec type_pat env sp =
             Env.lookup_label lid env
           with Not_found ->
             raise(Error(sp.ppat_loc, Unbound_label lid)) in
-        let (ty_arg, ty_res) = instance_label label in
+        let (_, ty_arg, ty_res) = instance_label false label in
         begin try
           unify env ty_res ty
         with Unify trace ->
@@ -470,7 +473,7 @@ let check_unused_variant pat =
           begin match opat with None -> assert false
           | Some pat -> List.iter (unify_pat pat.pat_env pat) (ty::tl)
           end
-      | Reither (c, l, true, e) ->
+      | Reither (c, l, true, e) when not row.row_fixed ->
           e := Some (Reither (c, [], false, ref None))
       | _ -> ()
       end
@@ -675,6 +678,23 @@ let rec list_labels_aux env visited ls ty_fun =
 
 let list_labels env ty = list_labels_aux env [] [] ty
 
+(* Check that all univars are safe in a type *)
+let check_univars env kind exp ty_expected vars =
+  let vars' =
+    List.filter
+      (fun t ->
+        let t = repr t in
+        generalize t;
+        if t.desc = Tvar && t.level = generic_level then
+          (t.desc <- Tunivar; true)
+        else false)
+      vars in
+  if List.length vars = List.length vars' then () else
+  let ty = newgenty (Tpoly(repr exp.exp_type, vars'))
+  and ty_expected = repr ty_expected in
+  raise (Error (exp.exp_loc,
+                Less_general(kind, [ty, ty; ty_expected, ty_expected])))
+
 (* Hack to allow coercion of self. Will clean-up later. *)
 let self_coercion = ref ([] : (Path.t * Location.t list ref) list)
 
@@ -732,8 +752,14 @@ let rec type_exp env sexp =
   | Pexp_function _ ->     (* defined in type_expect *)
       type_expect env sexp (newvar())
   | Pexp_apply(sfunct, sargs) ->
+      if !Clflags.principal then begin_def ();
       let funct = type_exp env sfunct in
+      if !Clflags.principal then begin
+        end_def ();
+        generalize_structure funct.exp_type
+      end;
       let (args, ty_res) = type_application env funct sargs in
+      let funct = {funct with exp_type = instance funct.exp_type} in
       { exp_desc = Texp_apply(funct, args);
         exp_loc = sexp.pexp_loc;
         exp_type = ty_res;
@@ -773,6 +799,7 @@ let rec type_exp env sexp =
                                   row_more = newvar ();
                                   row_bound = [];
                                   row_closed = false;
+                                  row_fixed = false;
                                   row_name = None});
         exp_env = env }
   | Pexp_record(lid_sexp_list, opt_sexp) ->
@@ -784,13 +811,22 @@ let rec type_exp env sexp =
             Env.lookup_label lid env
           with Not_found ->
             raise(Error(sexp.pexp_loc, Unbound_label lid)) in
-        let (ty_arg, ty_res) = instance_label label in
+        begin_def ();
+        if !Clflags.principal then begin_def ();
+        let (vars, ty_arg, ty_res) = instance_label true label in
+        if !Clflags.principal then begin
+          end_def ();
+          generalize_structure ty_arg;
+          generalize_structure ty_res
+        end;
         begin try
-          unify env ty_res ty
+          unify env (instance ty_res) ty
         with Unify trace ->
           raise(Error(sexp.pexp_loc, Label_mismatch(lid, trace)))
         end;
-        let arg = type_expect env sarg ty_arg in
+        let arg = type_argument env sarg ty_arg in
+        end_def ();
+        check_univars env "field value" arg label.lbl_arg vars;
         num_fields := Array.length label.lbl_all;
         (label, arg) in
       let lbl_exp_list = List.map type_label_exp lid_sexp_list in
@@ -810,8 +846,8 @@ let rec type_exp env sexp =
               if List.for_all (fun (lbl',_) -> lbl'.lbl_pos <> lbl.lbl_pos)
                   lbl_exp_list
               then begin
-                let ty_arg1, ty_res1 = instance_label lbl
-                and ty_arg2, ty_res2 = instance_label lbl in
+                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 ty_arg1 ty_arg2
@@ -844,7 +880,7 @@ let rec type_exp env sexp =
           Env.lookup_label lid env
         with Not_found ->
           raise(Error(sexp.pexp_loc, Unbound_label lid)) in
-      let (ty_arg, ty_res) = instance_label label in
+      let (_, ty_arg, ty_res) = instance_label false label in
       unify_exp env arg ty_res;
       { exp_desc = Texp_field(arg, label);
         exp_loc = sexp.pexp_loc;
@@ -859,9 +895,12 @@ let rec type_exp env sexp =
           raise(Error(sexp.pexp_loc, Unbound_label lid)) in
       if label.lbl_mut = Immutable then
         raise(Error(sexp.pexp_loc, Label_not_mutable lid));
-      let (ty_arg, ty_res) = instance_label label in
+      begin_def ();
+      let (vars, ty_arg, ty_res) = instance_label true label in
       unify_exp env record ty_res;
       let newval = type_expect env snewval ty_arg in
+      end_def ();
+      check_univars env "field value" newval label.lbl_arg vars;
       { exp_desc = Texp_setfield(record, label, newval);
         exp_loc = sexp.pexp_loc;
         exp_type = instance Predef.type_unit;
@@ -922,8 +961,15 @@ let rec type_exp env sexp =
             let arg = type_exp env sarg in
             (arg, arg.exp_type)
         | (Some sty, None) ->
+            if !Clflags.principal then begin_def ();
             let ty = Typetexp.transl_simple_type env false sty in
-            (type_expect env sarg ty, ty)
+            if !Clflags.principal then begin
+              end_def ();
+              generalize_structure ty;
+              let ty1 = instance ty and ty2 = instance ty in
+              (type_expect env sarg ty1, ty2)
+            end else
+              (type_expect env sarg ty, ty)
         | (None, Some sty') ->
             let (ty', force) =
               Typetexp.transl_simple_type_delayed env sty'
@@ -969,6 +1015,7 @@ let rec type_exp env sexp =
         exp_type = body.exp_type;
         exp_env = env }
   | Pexp_send (e, met) ->
+      if !Clflags.principal then begin_def ();
       let obj = type_exp env e in
       begin try
         let (exp, typ) =
@@ -996,7 +1043,7 @@ let rec type_exp env sexp =
                   let method_type = newvar () in
                   let (obj_ty, res_ty) = filter_arrow env method_type "" in
                   unify env obj_ty desc.val_type;
-                  unify env res_ty typ;
+                  unify env res_ty (instance typ);
                   (Texp_apply({exp_desc = Texp_ident(Path.Pident method_id,
                                                      {val_type = method_type;
                                                        val_kind = Val_reg});
@@ -1016,6 +1063,29 @@ let rec type_exp env sexp =
               (Texp_send(obj, Tmeth_name met),
                filter_method env met Public obj.exp_type)
         in
+        if !Clflags.principal then begin
+          end_def ();
+          generalize_structure typ;
+        end;
+        let typ =
+          match repr typ with
+            {desc = Tpoly (ty, [])} ->
+              instance ty
+          | {desc = Tpoly (ty, tl); level = l} ->
+              if !Clflags.principal && l <> generic_level then
+                Location.prerr_warning sexp.pexp_loc
+                  (Warnings.Other
+                     "This use of a polymorphic method is not principal");
+              snd (instance_poly false tl ty)
+          | {desc = Tvar} as ty ->
+              let ty' = newvar () in
+              unify env (instance ty) (newty(Tpoly(ty',[])));
+              (* if not !Clflags.nolabels then
+                 Location.prerr_warning loc (Warnings.Unknown_method met); *)
+              ty'
+          | _ ->
+              assert false
+        in
           { exp_desc = exp;
             exp_loc = sexp.pexp_loc;
             exp_type = typ;
@@ -1042,7 +1112,7 @@ let rec type_exp env sexp =
         let (path, desc) = Env.lookup_value (Longident.Lident lab) env in
         match desc.val_kind with
           Val_ivar (Mutable, cl_num) ->
-            let newval = type_expect env snewval desc.val_type in
+            let newval = type_expect env snewval (instance desc.val_type) in
             let (path_self, _) =
               Env.lookup_value (Longident.Lident ("self-" ^ cl_num)) env
             in
@@ -1080,7 +1150,7 @@ let rec type_exp env sexp =
           let type_override (lab, snewval) =
             begin try
               let (id, _, ty) = Vars.find lab !vars in
-              (Path.Pident id, type_expect env snewval ty)
+              (Path.Pident id, type_expect env snewval (instance ty))
             with
               Not_found ->
                 raise(Error(sexp.pexp_loc, Unbound_instance_variable lab))
@@ -1138,31 +1208,45 @@ let rec type_exp env sexp =
          exp_type = instance (Predef.type_lazy_t arg.exp_type);
          exp_env = env;
        }
+  | Pexp_poly _ ->
+      assert false
 
-and type_argument env sarg ty_expected =
+and type_argument env sarg ty_expected' =
+  (* ty_expected' may be generic *)
   let no_labels ty =
     let ls, tvar = list_labels env ty in
     not tvar && List.for_all ((=) "") ls
   in
-  match expand_head env ty_expected, sarg with
+  let ty_expected = instance ty_expected' in
+  match expand_head env ty_expected', sarg with
   | _, {pexp_desc = Pexp_function(l,_,_)} when not (is_optional l) ->
       type_expect env sarg ty_expected
-  | {desc = Tarrow("",ty_arg,ty_res,_)}, _ ->
+  | {desc = Tarrow("",ty_arg,ty_res,_); level = lv}, _ ->
       (* apply optional arguments when expected type is "" *)
       (* we must be very careful about not breaking the semantics *)
+      if !Clflags.principal then begin_def ();
       let texp = type_exp env sarg in
+      if !Clflags.principal then begin
+        end_def ();
+        generalize_structure texp.exp_type
+      end;
       let rec make_args args ty_fun =
         match (expand_head env ty_fun).desc with
         | Tarrow (l,ty_arg,ty_fun,_) when is_optional l ->
             make_args
-              ((Some(option_none ty_arg sarg.pexp_loc), Optional) :: args)
+              ((Some(option_none (instance ty_arg) sarg.pexp_loc), Optional)
+               :: args)
               ty_fun
         | Tarrow (l,_,ty_res',_) when l = "" || !Clflags.classic ->
             args, ty_fun, no_labels ty_res'
         | Tvar ->  args, ty_fun, false
         |  _ -> [], texp.exp_type, false
       in
-      let args, ty_fun, simple_res = make_args [] texp.exp_type in
+      let args, ty_fun', simple_res = make_args [] texp.exp_type in
+      let warn = !Clflags.principal &&
+        (lv <> generic_level || (repr ty_fun').level <> generic_level)
+      and texp = {texp with exp_type = instance texp.exp_type}
+      and ty_fun = instance ty_fun' in
       if not (simple_res || no_labels ty_res) then begin
         unify_exp env texp ty_expected;
         texp
@@ -1184,6 +1268,8 @@ and type_argument env sarg ty_expected =
                                    Texp_apply (texp, args@
                                                [Some eta_var, Required])}],
                         Total) } in
+      if warn then Location.prerr_warning texp.exp_loc
+          (Warnings.Other "Eliminated optional argument without principality");
       if is_nonexpansive texp then func texp else
       (* let-expand to have side effects *)
       let let_pat, let_var = var_pair "let" texp.exp_type in
@@ -1194,6 +1280,7 @@ and type_argument env sarg ty_expected =
       type_expect env sarg ty_expected
 
 and type_application env funct sargs =
+  (* funct.exp_type may be generic *)
   let result_type omitted ty_fun =
     List.fold_left
       (fun ty_fun (l,ty,lv) -> newty2 lv (Tarrow(l,ty,ty_fun,Cok)))
@@ -1209,7 +1296,7 @@ and type_application env funct sargs =
         (List.map
            (function None, x -> None, x | Some f, x -> Some (f ()), x)
            (List.rev args),
-         result_type omitted ty_fun)
+         instance (result_type omitted ty_fun))
     | (l1, sarg1) :: sargl ->
         let (ty1, ty2) =
           match (expand_head env ty_fun).desc with
@@ -1256,10 +1343,18 @@ and type_application env funct sargs =
        true)
     end
   in
+  let warned = ref false in
   let rec type_args args omitted ty_fun ty_old sargs more_sargs =
     match expand_head env ty_fun with
       {desc=Tarrow (l, ty, ty_fun, com); level=lv} as ty_fun'
       when (sargs <> [] || more_sargs <> []) && commu_repr com = Cok ->
+        let may_warn loc msg =
+          if not !warned && !Clflags.principal && lv <> generic_level
+          then begin
+            warned := true;
+            Location.prerr_warning loc (Warnings.Other msg)
+          end
+        in
         let name = label_name l
         and optional = if is_optional l then Optional else Required in
         let sargs, more_sargs, arg =
@@ -1278,28 +1373,45 @@ and type_application env funct sargs =
           end else try
             let (l', sarg0, sargs, more_sargs) =
               try
-                let (l', sarg0, sargs1, sargs2) = extract_label name sargs
-                in (l', sarg0, sargs1 @ sargs2, more_sargs)
+                let (l', sarg0, sargs1, sargs2) = extract_label name sargs in
+                if sargs1 <> [] then
+                  may_warn sarg0.pexp_loc
+                    "Commuting this argument is not principal";
+                (l', sarg0, sargs1 @ sargs2, more_sargs)
               with Not_found ->
-                let (l', sarg0, sargs1, sargs2) = extract_label name more_sargs
-                in (l', sarg0, sargs @ sargs1, sargs2)
+                let (l', sarg0, sargs1, sargs2) =
+                  extract_label name more_sargs in
+                if sargs1 <> [] || sargs <> [] then
+                  may_warn sarg0.pexp_loc
+                    "Commuting this argument is not principal";
+                (l', sarg0, sargs @ sargs1, sargs2)
             in
             sargs, more_sargs,
             if optional = Required || is_optional l' then
               Some (fun () -> type_argument env sarg0 ty)
-            else
+            else begin
+              may_warn sarg0.pexp_loc
+                "Using an optional argument here is not principal";
               Some (fun () -> option_some (type_argument env sarg0 
                                              (extract_option_type env ty)))
+            end
           with Not_found ->
             sargs, more_sargs,
             if optional = Optional &&
               (List.mem_assoc "" sargs || List.mem_assoc "" more_sargs)
             then begin
+              may_warn funct.exp_loc
+                "Eliminated an optional argument without principality";
               ignored := (l,ty,lv) :: !ignored;
-              Some (fun () -> option_none ty Location.none)
-            end else None
+              Some (fun () -> option_none (instance ty) Location.none)
+            end else begin
+              may_warn funct.exp_loc
+                "Commuted an argument without principality";
+              None
+            end
         in
-        let omitted = if arg = None then (l,ty,lv) :: omitted else omitted in
+        let omitted =
+          if arg = None then (l,ty,lv) :: omitted else omitted in
         let ty_old = if sargs = [] then ty_fun else ty_old in
         type_args ((arg,optional)::args) omitted ty_fun ty_old sargs more_sargs
     | _ ->
@@ -1307,13 +1419,14 @@ and type_application env funct sargs =
           (l, sarg0) :: _ when ignore_labels ->
             raise(Error(sarg0.pexp_loc, Apply_wrong_label(l, ty_old)));
         | _ ->
-            type_unknown_args args omitted ty_fun (sargs @ more_sargs)
+            type_unknown_args args omitted (instance ty_fun)
+              (sargs @ more_sargs)
   in
   match funct.exp_desc, sargs with
     (* Special case for ignore: avoid discarding warning *)
     Texp_ident (_, {val_kind=Val_prim{Primitive.prim_name="%ignore"}}),
     ["", sarg] ->
-      let ty_arg, ty_res = filter_arrow env funct.exp_type "" in
+      let ty_arg, ty_res = filter_arrow env (instance funct.exp_type) "" in
       let exp = type_expect env sarg ty_arg in
       begin match expand_head env exp.exp_type with
       | {desc = Tarrow _} ->
@@ -1343,14 +1456,20 @@ and type_construct env loc lid sarg explicit_arity ty_expected =
   if List.length sargs <> constr.cstr_arity then
     raise(Error(loc, Constructor_arity_mismatch
                   (lid, constr.cstr_arity, List.length sargs)));
+  if !Clflags.principal then begin_def ();
   let (ty_args, ty_res) = instance_constructor constr in
+  if !Clflags.principal then begin
+    end_def ();
+    List.iter generalize_structure ty_args;
+    generalize_structure ty_res
+  end;
   let texp =
     { exp_desc = Texp_construct(constr, []);
       exp_loc = loc;
-      exp_type = ty_res;
+      exp_type = instance ty_res;
       exp_env = env } in
   unify_exp env texp ty_expected;
-  let args = List.map2 (type_expect env) sargs ty_args in
+  let args = List.map2 (type_argument env) sargs ty_args in
   { texp with exp_desc = Texp_construct(constr, args) }
 
 (* Typing of an expression with an expected type.
@@ -1444,6 +1563,34 @@ and type_expect ?in_function env sexp ty_expected =
         exp_loc = sexp.pexp_loc;
         exp_type = newty (Tarrow(l, ty_arg, ty_res, Cok));
         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 = sexp.pexp_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
+            { 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 "method" exp ty_expected vars;
+            { exp with exp_type = ty }
+        | _ -> assert false
+      end
   | _ ->
       let exp = type_exp env sexp in
       unify_exp env exp ty_expected;
@@ -1470,7 +1617,15 @@ and type_cases ?in_function env ty_arg ty_res partial_loc caselist =
   let pat_env_list =
     List.map
       (fun (spat, sexp) ->
+        if !Clflags.principal then begin_def ();
         let (pat, ext_env) = type_pattern env spat in
+        let pat =
+          if !Clflags.principal then begin
+            end_def ();
+            iter_pattern (fun {pat_type=t} -> generalize_structure t) pat;
+            { pat with pat_type = instance pat.pat_type }
+          end else pat
+        in
         unify_pat env pat ty_arg';
         (pat, ext_env))
       caselist in
@@ -1509,6 +1664,7 @@ and type_cases ?in_function env ty_arg ty_res partial_loc caselist =
 
 and type_let env rec_flag spat_sexp_list =
   begin_def();
+  if !Clflags.principal then begin_def ();
   let (pat_list, new_env) =
     type_pattern_list env (List.map (fun (spat, sexp) -> spat) spat_sexp_list)
   in
@@ -1516,6 +1672,15 @@ and type_let env rec_flag spat_sexp_list =
     List.iter2
       (fun pat (_, sexp) -> unify_pat env pat (type_approx env sexp))
       pat_list spat_sexp_list;
+  let pat_list =
+    if !Clflags.principal then begin
+      end_def ();
+      List.map
+        (fun pat ->
+          iter_pattern (fun pat -> generalize_structure pat.pat_type) pat;
+          {pat with pat_type = instance pat.pat_type})
+        pat_list
+    end else pat_list in
   let exp_env =
     match rec_flag with Nonrecursive | Default -> env | Recursive -> new_env in
   let exp_list =
@@ -1529,7 +1694,9 @@ and type_let env rec_flag spat_sexp_list =
   List.iter2
     (fun pat exp ->
        if not (is_nonexpansive exp) then
-         iter_pattern (fun pat -> make_nongen pat.pat_type) pat)
+         let f =
+           if !Clflags.principal then generalize_expansive else make_nongen in
+         iter_pattern (fun pat -> f pat.pat_type) pat)
     pat_list exp_list;
   List.iter
     (fun pat -> iter_pattern (fun pat -> generalize pat.pat_type) pat)
@@ -1550,6 +1717,7 @@ let type_expression env sexp =
   let exp = type_exp env sexp in
   end_def();
   if is_nonexpansive exp then generalize exp.exp_type
+  else if !Clflags.principal then generalize_expansive exp.exp_type
   else make_nongen exp.exp_type;
   exp
 
@@ -1690,3 +1858,7 @@ let report_error ppf = function
       fprintf ppf "This function is applied to arguments@ ";
       fprintf ppf "in an order different from other calls.@ ";
       fprintf ppf "This is only allowed when the real type is known."
+  | Less_general (kind, trace) ->
+      report_unification_error ppf trace
+        (fun ppf -> fprintf ppf "This %s has type" kind)
+        (fun ppf -> fprintf ppf "which is less general than")
diff --git a/typing/typecore.mli b/typing/typecore.mli
index 6df4002b5..78a8c7799 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -53,6 +53,7 @@ val type_argument:
 val option_some: Typedtree.expression -> Typedtree.expression
 val option_none: type_expr -> Location.t -> Typedtree.expression
 val extract_option_type: Env.t -> type_expr -> type_expr
+val iter_pattern: (Typedtree.pattern -> unit) -> Typedtree.pattern -> unit
 
 val self_coercion : (Path.t * Location.t list ref) list ref
 
@@ -88,6 +89,7 @@ type error =
   | Masked_instance_variable of Longident.t
   | Not_a_variant_type of Longident.t
   | Incoherent_label_order
+  | Less_general of string * (type_expr * type_expr) list
 
 exception Error of Location.t * error
 
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 4fdbbed7c..4ae53bacd 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -87,11 +87,18 @@ module StringSet =
 let transl_declaration env (name, sdecl) id =
   (* Bind type parameters *)
   reset_type_variables();
+  Ctype.begin_def ();
   let params =
     try List.map (enter_type_variable true) sdecl.ptype_params
     with Already_bound ->
       raise(Error(sdecl.ptype_loc, Repeated_parameter))
   in
+  let cstrs = List.map
+      (fun (sty, sty', loc) ->
+        transl_simple_type env false sty,
+        transl_simple_type env false sty', loc)
+      sdecl.ptype_cstrs
+  in
   let decl =
     { type_params = params;
       type_arity = List.length params;
@@ -125,7 +132,8 @@ let transl_declaration env (name, sdecl) id =
             let lbls' =
               List.map
                 (fun (name, mut, arg) ->
-                         (name, mut, transl_simple_type env true arg))
+                  let ty = transl_simple_type env true arg in
+                  name, mut, match ty.desc with Tpoly(t,[]) -> t | _ -> ty)
                 lbls in
             let rep =
               if List.for_all (fun (name, mut, arg) -> is_float env arg) lbls'
@@ -147,13 +155,11 @@ let transl_declaration env (name, sdecl) id =
 
   (* Check constraints *)
   List.iter
-    (function (sty, sty', loc) ->
-       try
-         Ctype.unify env (transl_simple_type env false sty)
-                         (transl_simple_type env false sty')
-       with Ctype.Unify tr ->
-         raise(Error(loc, Unconsistent_constraint tr)))
-    sdecl.ptype_cstrs;
+    (fun (ty, ty', loc) ->
+      try Ctype.unify env ty ty' with Ctype.Unify tr ->
+        raise(Error(loc, Unconsistent_constraint tr)))
+    cstrs;
+  Ctype.end_def ();
 
   (id, decl)
 
@@ -201,6 +207,9 @@ let rec check_constraints_rec env loc visited ty =
       if not (List.for_all2 (Ctype.moregeneral env false) args' args) then
         raise (Error(loc, Constraint_failed (ty, ty')));
       List.iter (check_constraints_rec env loc visited) args
+  | Tpoly (ty, tl) ->
+      let _, ty = Ctype.instance_poly false tl ty in
+      check_constraints_rec env loc visited ty
   | _ ->
       Btype.iter_type_expr (check_constraints_rec env loc visited) ty
   end
@@ -376,7 +385,9 @@ let compute_variance env tvl nega posi ty =
                   List.iter (compute_variance_rec posi nega) tyl
               | _ -> ())
             (Btype.row_repr row).row_fields
-      | Tvar | Tnil | Tlink _ -> ()
+      | Tpoly (ty, _) ->
+          compute_variance_rec posi nega ty
+      | Tvar | Tnil | Tlink _ | Tunivar -> ()
     end
   in
   compute_variance_rec nega posi ty;
diff --git a/typing/types.ml b/typing/types.ml
index f1ed0cf01..0b9c4350f 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -35,12 +35,15 @@ and type_desc =
   | Tlink of type_expr
   | Tsubst of type_expr
   | Tvariant of row_desc
+  | Tunivar
+  | Tpoly of type_expr * type_expr list
 
 and row_desc =
     { row_fields: (label * row_field) list;
       row_more: type_expr;
       row_bound: type_expr list;
       row_closed: bool;
+      row_fixed: bool;
       row_name: (Path.t * type_expr list) option }
 
 and row_field =
@@ -63,6 +66,13 @@ and commutable =
   | Cunknown
   | Clink of commutable ref
 
+module TypeOps = struct
+  type t = type_expr
+  let compare t1 t2 = t1.id - t2.id
+  let hash t = t.id
+  let equal t1 t2 = t1 == t2
+end
+
 (* Maps of methods and instance variables *)
 
 module OrderedString = struct type t = string let compare = compare end
diff --git a/typing/types.mli b/typing/types.mli
index 95ac8c887..096ced67a 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -34,12 +34,15 @@ and type_desc =
   | Tlink of type_expr
   | Tsubst of type_expr         (* for copying *)
   | Tvariant of row_desc
+  | Tunivar
+  | Tpoly of type_expr * type_expr list
 
 and row_desc =
     { row_fields: (label * row_field) list;
       row_more: type_expr;
       row_bound: type_expr list;
       row_closed: bool;
+      row_fixed: bool;
       row_name: (Path.t * type_expr list) option }
 
 and row_field =
@@ -65,6 +68,13 @@ and commutable =
   | Cunknown
   | Clink of commutable ref
 
+module TypeOps : sig
+  type t = type_expr
+  val compare : t -> t -> int
+  val equal : t -> t -> bool
+  val hash : t -> int
+end
+
 (* Maps of methods and instance variables *)
 
 module Meths : Map.S with type key = string
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index d2947b62a..47469ecb4 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(* $Id$ *)
+(* typetexp.ml,v 1.34.4.9 2002/01/07 08:39:16 garrigue Exp *)
 
 (* Typechecking of type expressions for the core language *)
 
@@ -37,6 +37,8 @@ type error =
   | Constructor_mismatch of type_expr * type_expr
   | Not_a_variant of type_expr
   | Variant_tags of string * string
+  | No_row_variable of string
+  | Bad_alias of string
 
 exception Error of Location.t * error
 
@@ -44,6 +46,8 @@ exception Error of Location.t * error
 
 let type_variables = ref (Tbl.empty : (string, type_expr) Tbl.t)
 let saved_type_variables = ref ([] : (string, type_expr) Tbl.t list)
+let univars        = ref ([] : (string * type_expr) list)
+let pre_univars    = ref ([] : type_expr list)
 
 let used_variables = ref (Tbl.empty : (string, type_expr) Tbl.t)
 let bindings       = ref ([] : (Location.t * type_expr * type_expr) list)
@@ -80,33 +84,61 @@ let type_variable loc name =
   with Not_found ->
     raise(Error(loc, Unbound_type_variable ("'" ^ name)))
 
-type policy = Fixed | Extensible | Delayed
+let wrap_method ty =
+  match (Ctype.repr ty).desc with
+    Tpoly _ -> ty
+  | _ -> Ctype.newty (Tpoly (ty, []))
 
-let rec transl_type env policy styp =
+let new_pre_univar () =
+  let v = newvar () in pre_univars := v :: !pre_univars; v
+
+let rec swap_list = function
+    x :: y :: l -> y :: x :: swap_list l
+  | l -> l
+
+type policy = Fixed | Extensible | Delayed | Univars
+
+let rec transl_type env policy rowvar styp =
+  if rowvar <> None then begin
+    match styp.ptyp_desc with
+      Ptyp_variant _ | Ptyp_object _ | Ptyp_class _ -> ()
+    | _ -> raise(Error(styp.ptyp_loc, No_row_variable ""))
+  end;
   match styp.ptyp_desc with
-    Ptyp_any -> Ctype.newvar ()
+    Ptyp_any ->
+      if policy = Univars then new_pre_univar () else newvar ()
   | Ptyp_var name ->
-      begin
+      begin try
+	List.assoc name !univars
+      with Not_found ->
         match policy with
           Fixed ->
             begin try
-              Tbl.find name !type_variables
+              instance (Tbl.find name !type_variables)
             with Not_found ->
               raise(Error(styp.ptyp_loc, Unbound_type_variable ("'" ^ name)))
             end
         | Extensible ->
             begin try
-              Tbl.find name !type_variables
+              instance (Tbl.find name !type_variables)
             with Not_found ->
               let v = new_global_var () in
               type_variables := Tbl.add name v !type_variables;
               v
             end
+        | Univars ->
+            begin try
+              instance (Tbl.find name !type_variables)
+            with Not_found ->
+	      let v = new_pre_univar () in
+              type_variables := Tbl.add name v !type_variables;
+	      v
+            end
         | Delayed ->
             begin try
               Tbl.find name !used_variables
             with Not_found -> try
-              let v1 = Tbl.find name !type_variables in
+              let v1 = instance (Tbl.find name !type_variables) in
               let v2 = new_global_var () in
               used_variables := Tbl.add name v2 !used_variables;
               bindings := (styp.ptyp_loc, v1, v2)::!bindings;
@@ -119,11 +151,11 @@ let rec transl_type env policy styp =
             end
       end
   | Ptyp_arrow(l, st1, st2) ->
-      let ty1 = transl_type env policy st1 in
-      let ty2 = transl_type env policy st2 in
+      let ty1 = transl_type env policy None st1 in
+      let ty2 = transl_type env policy None st2 in
       newty (Tarrow(l, ty1, ty2, Cok))
   | Ptyp_tuple stl ->
-      newty (Ttuple(List.map (transl_type env policy) stl))
+      newty (Ttuple(List.map (transl_type env policy None) stl))
   | Ptyp_constr(lid, stl) ->
       let (path, decl) =
         try
@@ -133,7 +165,7 @@ let rec transl_type env policy styp =
       if List.length stl <> decl.type_arity then
         raise(Error(styp.ptyp_loc, Type_arity_mismatch(lid, decl.type_arity,
                                                            List.length stl)));
-      let args = List.map (transl_type env policy) stl in
+      let args = List.map (transl_type env policy None) stl in
       let params = List.map (fun _ -> Ctype.newvar ()) args in
       let cstr = newty (Tconstr(path, params, ref Mnil)) in
       begin try
@@ -143,14 +175,18 @@ let rec transl_type env policy styp =
       end;
       List.iter2
         (fun (sty, ty) ty' ->
-           try unify env ty ty' with Unify trace ->
-             raise (Error(sty.ptyp_loc, Type_mismatch trace)))
+           try unify_var env ty' ty with Unify trace ->
+             raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace))))
         (List.combine stl args) params;
       cstr
   | Ptyp_object fields ->
-      newobj (transl_fields env policy fields)
+      begin try
+	newobj (transl_fields env policy rowvar fields)
+      with Error (loc, No_row_variable _) when loc = Location.none ->
+	raise (Error(styp.ptyp_loc, No_row_variable "object "))
+      end
   | Ptyp_class(lid, stl, present) ->
-      if policy = Fixed then
+      if policy = Fixed & rowvar = None then
         raise(Error(styp.ptyp_loc, Unbound_row_variable lid));
       let (path, decl, is_variant) =
         try
@@ -182,8 +218,8 @@ let rec transl_type env policy styp =
       in
       if List.length stl <> decl.type_arity then
         raise(Error(styp.ptyp_loc, Type_arity_mismatch(lid, decl.type_arity,
-                                                           List.length stl)));
-      let args = List.map (transl_type env policy) stl in
+						       List.length stl)));
+      let args = List.map (transl_type env policy None) stl in
       let cstr = newty (Tconstr(path, args, ref Mnil)) in
       let ty =
         try Ctype.expand_head env cstr
@@ -193,8 +229,8 @@ let rec transl_type env policy styp =
       let params = Ctype.instance_list decl.type_params in
       List.iter2
         (fun (sty, ty') ty ->
-           try unify env ty' ty with Unify trace ->
-             raise (Error(sty.ptyp_loc, Type_mismatch trace)))
+           try unify_var env ty ty' with Unify trace ->
+             raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace))))
         (List.combine stl args) params;
       begin match ty.desc with
         Tvariant row ->
@@ -204,6 +240,7 @@ let rec transl_type env policy styp =
               raise(Error(styp.ptyp_loc, Present_has_no_type l)))
             present;
           let bound = ref row.row_bound in
+          let fixed = rowvar <> None || policy = Univars in
           let fields =
             List.map
               (fun (l,f) -> l,
@@ -211,34 +248,78 @@ let rec transl_type env policy styp =
                 match Btype.row_field_repr f with
                 | Rpresent (Some ty) ->
                     bound := ty :: !bound;
-                    Reither(false, [ty], false, ref None)
+                    Reither(false, [ty], fixed, ref None)
                 | Rpresent None ->
-                    Reither (true, [], false, ref None)
+                    Reither (true, [], fixed, ref None)
                 | _ -> f)
               row.row_fields
           in
-          let row = { row with row_fields = fields; row_bound = !bound;
-                      row_name = Some (path, args) } in
-          newty (Tvariant row)
-      | _ ->
+          let row = { row_closed = true;
+                      row_fields = fields;
+                      row_bound = !bound;
+                      row_name = Some (path, args);
+                      row_fixed = fixed;
+                      row_more = match rowvar with Some v -> v
+                      | None ->
+	                  if policy = Univars then new_pre_univar ()
+                          else newvar () }
+          in newty (Tvariant row)
+      | Tobject (fi, _) ->
+          let _, tv = flatten_fields fi in
+          if policy = Univars then pre_univars := tv :: !pre_univars;
+          begin match rowvar with None -> ()
+          | Some rv ->
+              let _, tv = flatten_fields fi in
+              try unify_var env tv rv with Unify trace ->
+                raise(Error(styp.ptyp_loc, Alias_type_mismatch trace))
+          end;
           ty
+      | _ ->
+          assert false
       end
   | Ptyp_alias(st, alias) ->
-      if Tbl.mem alias !type_variables then
-        raise(Error(styp.ptyp_loc, Bound_type_variable alias))
-      else
-        let ty' = new_global_var () in
-        type_variables := Tbl.add alias ty' !type_variables;
-        let ty = transl_type env policy st in
-        begin try unify env ty ty' with Unify trace ->
-          raise(Error(styp.ptyp_loc, Alias_type_mismatch trace))
-        end;
-        ty
+      if List.mem_assoc alias !univars then
+        match List.assoc alias !univars with
+	  {desc=Tlink({desc=Tunivar} as tc)} as tr ->
+	    let ty = transl_type env policy (Some tc) st in
+            tr.level <- tc.level;
+	    tr.desc <- Tvar;
+            begin try unify_var env tr ty with Unify trace ->
+              let trace = swap_list trace in
+              raise(Error(styp.ptyp_loc, Alias_type_mismatch trace))
+            end;
+            ty
+        | _ ->
+            raise(Error(styp.ptyp_loc, Bound_type_variable alias))
+      else begin
+        try
+          let t = instance (Tbl.find alias !type_variables) in
+          let ty = transl_type env policy None st in
+          begin try unify_var env t ty with Unify trace ->
+            let trace = swap_list trace in
+            raise(Error(styp.ptyp_loc, Alias_type_mismatch trace))
+          end;
+          ty
+        with Not_found ->
+          begin_def ();
+          let t = newvar () in
+          type_variables := Tbl.add alias t !type_variables;
+          let ty = transl_type env policy None st in
+          begin try unify_var env t ty with Unify trace ->
+            let trace = swap_list trace in
+            raise(Error(styp.ptyp_loc, Alias_type_mismatch trace))
+          end;
+          end_def ();
+          generalize_global t;
+          instance t
+      end
   | Ptyp_variant(fields, closed, present) ->
       let bound = ref [] and name = ref None in
+      let fixed = rowvar <> None || policy = Univars in
       let mkfield l f =
         newty (Tvariant {row_fields=[l,f]; row_more=newty Tnil;
-                         row_bound=[]; row_closed=true; row_name=None}) in
+                         row_bound=[]; row_closed=true;
+                         row_fixed=fixed; row_name=None}) in
       let add_typed_field loc l f fields =
         try
           let f' = List.assoc l fields in
@@ -253,18 +334,18 @@ let rec transl_type env policy styp =
             name := None;
             let f = match present with
               Some present when not (List.mem l present) ->
-                let tl = List.map (transl_type env policy) stl in
+                let tl = List.map (transl_type env policy None) stl in
                 bound := tl @ !bound;
-                Reither(c, tl, false, ref None)
+                Reither(c, tl, fixed, ref None)
             | _ ->
                 if List.length stl > 1 || c && stl <> [] then
                   raise(Error(styp.ptyp_loc, Present_has_conjunction l));
                 match stl with [] -> Rpresent None
-                | st :: _ -> Rpresent (Some(transl_type env policy st))
+                | st :: _ -> Rpresent (Some(transl_type env policy None st))
             in
             add_typed_field styp.ptyp_loc l f fields
         | Rinherit sty ->
-            let ty = transl_type env policy sty in
+            let ty = transl_type env policy None sty in
             let nm =
               match repr ty with
                 {desc=Tconstr(p, tl, _)} -> Some(p, tl)
@@ -287,9 +368,9 @@ let rec transl_type env policy styp =
                     begin match f with
                       Rpresent(Some ty) ->
                         bound := ty :: !bound;
-                        Reither(false, [ty], false, ref None)
+                        Reither(false, [ty], fixed, ref None)
                     | Rpresent None ->
-                        Reither(true, [], false, ref None)
+                        Reither(true, [], fixed, ref None)
                     | _ ->
                         assert false
                     end
@@ -320,32 +401,77 @@ let rec transl_type env policy styp =
       end;
       let row =
         { row_fields = List.rev fields; row_more = newvar ();
-          row_bound = !bound; row_closed = closed; row_name = !name } in
-      if policy = Fixed && not (Btype.static_row row) then
-        raise(Error(styp.ptyp_loc, Unbound_type_variable "[..]"));
+          row_bound = !bound; row_closed = closed;
+          row_fixed = fixed; row_name = !name } in
+      let static = Btype.static_row row in
+      let row =
+        { row with row_more =
+            match rowvar with Some v -> v
+            | None ->
+	        if static then newty Tnil else
+	        if policy = Univars then new_pre_univar () else
+                if policy = Fixed && not static then
+                  raise(Error(styp.ptyp_loc, Unbound_type_variable "[..]"))
+	        else row.row_more
+        } in
       newty (Tvariant row)
+  | Ptyp_poly(vars, st) ->
+      (* aliases are stubs, in case one wants to redefine them *)
+      let ty_list = List.map (fun _ -> newty Tunivar) vars in
+      let new_univars =
+        List.map2 (fun name ty -> name, newty (Tlink ty)) vars ty_list in
+      let old_univars = !univars in
+      univars := new_univars @ !univars;
+      let ty = transl_type env policy None st in
+      univars := old_univars;
+      newty (Tpoly(ty, ty_list))
 
-and transl_fields env policy =
+and transl_fields env policy rowvar =
   function
     [] ->
       newty Tnil
   | {pfield_desc = Pfield_var} as field::_ ->
-      if policy = Fixed then
-        raise(Error(field.pfield_loc, Unbound_type_variable "<..>"));
-      newvar ()
+      begin match rowvar with
+	None ->
+	  if policy = Fixed then
+            raise(Error(field.pfield_loc, Unbound_type_variable ".."));
+	  if policy = Univars then new_pre_univar () else newvar ()
+      |	Some v -> v
+      end
   | {pfield_desc = Pfield(s, e)}::l ->
-      let ty1 = transl_type env policy e in
-      let ty2 = transl_fields env policy l in
+      let ty1 = transl_type env policy None e in
+      let ty2 = transl_fields env policy rowvar l in
         newty (Tfield (s, Fpresent, ty1, ty2))
 
 let transl_simple_type env fixed styp =
-  let typ = transl_type env (if fixed then Fixed else Extensible) styp in
+  univars := [];
+  let typ = transl_type env (if fixed then Fixed else Extensible) None styp in
   typ
 
+let transl_simple_type_univars env styp =
+  univars := [];
+  pre_univars := [];
+  begin_def ();
+  let typ = transl_type env Univars None styp in
+  end_def ();
+  generalize typ;
+  let univs =
+    List.fold_left
+      (fun acc v ->
+        let v = repr v in
+	if v.desc <> Tvar || v.level <> Btype.generic_level || List.memq v acc
+        then acc
+        else (v.desc <- Tunivar ; v :: acc))
+      [] !pre_univars
+  in
+  pre_univars := [];
+  instance (Btype.newgenty (Tpoly (typ, univs)))
+
 let transl_simple_type_delayed env styp =
+  univars := [];
   used_variables := Tbl.empty;
   bindings := [];
-  let typ = transl_type env Delayed styp in
+  let typ = transl_type env Delayed None styp in
   let b = !bindings in
   used_variables := Tbl.empty;
   bindings := [];
@@ -424,3 +550,9 @@ let report_error ppf = function
       fprintf ppf
         "Variant tags `%s@ and `%s have same hash value.@ Change one of them."
         lab1 lab2
+  | No_row_variable s ->
+      fprintf ppf "This %stype has no row variable" s
+  | Bad_alias name ->
+      fprintf ppf
+        "The alias %s cannot be used here. It captures universal variables."
+        name
diff --git a/typing/typetexp.mli b/typing/typetexp.mli
index 618c6e2bf..23ff76e90 100644
--- a/typing/typetexp.mli
+++ b/typing/typetexp.mli
@@ -18,6 +18,8 @@ open Format;;
 
 val transl_simple_type:
         Env.t -> bool -> Parsetree.core_type -> Types.type_expr
+val transl_simple_type_univars:
+        Env.t -> Parsetree.core_type -> Types.type_expr
 val transl_simple_type_delayed:
         Env.t -> Parsetree.core_type -> Types.type_expr * (unit -> unit)
         (* Translate a type, but leave type variables unbound. Returns
@@ -48,6 +50,8 @@ type error =
   | Constructor_mismatch of Types.type_expr * Types.type_expr
   | Not_a_variant of Types.type_expr
   | Variant_tags of string * string
+  | No_row_variable of string
+  | Bad_alias of string
 
 exception Error of Location.t * error
 
diff --git a/utils/clflags.ml b/utils/clflags.ml
index f7e9ada69..295e2837a 100644
--- a/utils/clflags.ml
+++ b/utils/clflags.ml
@@ -40,8 +40,9 @@ and noassert = ref false                (* -noassert *)
 and verbose = ref false                 (* -verbose *)
 and use_prims = ref ""                  (* -use-prims ... *)
 and use_runtime = ref ""                (* -use-runtime ... *)
+and principal = ref false               (* -principal *)
 and recursive_types = ref false         (* -rectypes *)
-and make_runtime = ref false            (* -make-runtime *)
+and make_runtime = ref false            (* -make_runtime *)
 and gprofile = ref false                (* -p *)
 and c_compiler = ref Config.bytecomp_c_compiler (* -cc *)
 and c_linker = ref Config.bytecomp_c_linker (* -cc *)