Keep type variable names

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

31 files changed, 505 insertions, 385 deletions

diff --git a/VERSION b/VERSION
index 034dd73a38..917b0d230e 100644
--- a/VERSION
+++ b/VERSION
@@ -1,4 +1,4 @@
-3.13.0+dev6 (2011-07-29)
+3.13.0+dev7 (2011-09-22)
 
 # The version string is the first line of this file.
 # It must be in the format described in stdlib/sys.mli
diff --git a/boot/ocamlc b/boot/ocamlc
index 808d7a5e6c..a8ceda2170 100755
--- a/boot/ocamlc
+++ b/boot/ocamlc
diff --git a/boot/ocamldep b/boot/ocamldep
index a0e399ad10..f0a9eefc27 100755
--- a/boot/ocamldep
+++ b/boot/ocamldep
diff --git a/boot/ocamllex b/boot/ocamllex
index a3afffea27..60da3ed874 100755
--- a/boot/ocamllex
+++ b/boot/ocamllex
diff --git a/bytecomp/translcore.ml b/bytecomp/translcore.ml
index d784e51eea..9441fcc684 100644
--- a/bytecomp/translcore.ml
+++ b/bytecomp/translcore.ml
@@ -780,12 +780,13 @@ and transl_exp0 e =
           begin match e.exp_type.desc with
           (* the following may represent a float/forward/lazy: need a
              forward_tag *)
-          | Tvar | Tlink _ | Tsubst _ | Tunivar
+          | Tvar _ | Tlink _ | Tsubst _ | Tunivar _
           | Tpoly(_,_) | Tfield(_,_,_,_) ->
               Lprim(Pmakeblock(Obj.forward_tag, Immutable), [transl_exp e])
           (* the following cannot be represented as float/forward/lazy:
              optimize *)
-          | Tarrow(_,_,_,_) | Ttuple _ | Tpackage _ | Tobject(_,_) | Tnil | Tvariant _
+          | Tarrow(_,_,_,_) | Ttuple _ | Tpackage _ | Tobject(_,_) | Tnil
+          | Tvariant _
               -> transl_exp e
           (* optimize predefined types (excepted float) *)
           | Tconstr(_,_,_) ->
diff --git a/bytecomp/typeopt.ml b/bytecomp/typeopt.ml
index a8371910e8..e80148f096 100644
--- a/bytecomp/typeopt.ml
+++ b/bytecomp/typeopt.ml
@@ -50,7 +50,7 @@ let maybe_pointer exp =
 
 let array_element_kind env ty =
   match scrape env ty with
-  | Tvar | Tunivar ->
+  | Tvar _ | Tunivar _ ->
       Pgenarray
   | Tconstr(p, args, abbrev) ->
       if Path.same p Predef.path_int || Path.same p Predef.path_char then
diff --git a/ocamldoc/odoc_misc.ml b/ocamldoc/odoc_misc.ml
index c439ef3163..c48c1f6a56 100644
--- a/ocamldoc/odoc_misc.ml
+++ b/ocamldoc/odoc_misc.ml
@@ -478,8 +478,8 @@ let remove_option typ =
     match t with
     | Types.Tconstr(path, [ty], _) when Path.same path Predef.path_option -> ty.Types.desc
     | Types.Tconstr _
-    | Types.Tvar
-    | Types.Tunivar
+    | Types.Tvar _
+    | Types.Tunivar _
     | Types.Tpoly _
     | Types.Tarrow _
     | Types.Ttuple _
diff --git a/ocamldoc/odoc_str.ml b/ocamldoc/odoc_str.ml
index 3df9b5c0c3..d420c05971 100644
--- a/ocamldoc/odoc_str.ml
+++ b/ocamldoc/odoc_str.ml
@@ -31,7 +31,7 @@ let rec is_arrow_type t =
   | Types.Tlink t2 | Types.Tsubst t2 -> is_arrow_type t2
   | Types.Ttuple _
   | Types.Tconstr _
-  | Types.Tvar | Types.Tunivar | Types.Tobject _ | Types.Tpoly _
+  | Types.Tvar _ | Types.Tunivar _ | Types.Tobject _ | Types.Tpoly _
   | Types.Tfield _ | Types.Tnil | Types.Tvariant _ | Types.Tpackage _ -> false
 
 let raw_string_of_type_list sep type_list =
@@ -43,7 +43,7 @@ let raw_string_of_type_list sep type_list =
     | Types.Tlink t2 | Types.Tsubst t2 -> need_parent t2
     | Types.Tconstr _ ->
         false
-    | Types.Tvar | Types.Tunivar | Types.Tobject _ | Types.Tpoly _
+    | Types.Tvar _ | Types.Tunivar _ | Types.Tobject _ | Types.Tpoly _
     | Types.Tfield _ | Types.Tnil | Types.Tvariant _ | Types.Tpackage _ -> false
   in
   let print_one_type variance t =
diff --git a/ocamldoc/odoc_value.ml b/ocamldoc/odoc_value.ml
index a210f0851e..c8881ddfd8 100644
--- a/ocamldoc/odoc_value.ml
+++ b/ocamldoc/odoc_value.ml
@@ -77,13 +77,13 @@ let parameter_list_from_arrows typ =
     | Types.Tsubst texp ->
         iter texp
     | Types.Tpoly (texp, _) -> iter texp
-    | Types.Tvar
+    | Types.Tvar _
     | Types.Ttuple _
     | Types.Tconstr _
     | Types.Tobject _
     | Types.Tfield _
     | Types.Tnil
-    | Types.Tunivar
+    | Types.Tunivar _
     | Types.Tpackage _
     | Types.Tvariant _ ->
         []
diff --git a/otherlibs/labltk/browser/searchid.ml b/otherlibs/labltk/browser/searchid.ml
index 3246fa15bb..1d7a9a8f4b 100644
--- a/otherlibs/labltk/browser/searchid.ml
+++ b/otherlibs/labltk/browser/searchid.ml
@@ -101,7 +101,7 @@ let rec all_args ty =
 
 let rec equal ~prefix t1 t2 =
   match (repr t1).desc, (repr t2).desc with
-    Tvar, Tvar -> true
+    Tvar _, Tvar _ -> true
   | Tvariant row1, Tvariant row2 ->
       let row1 = row_repr row1 and row2 = row_repr row2 in
       let fields1 = filter_row_fields false row1.row_fields
@@ -144,7 +144,7 @@ let get_options = List.filter ~f:is_opt
 
 let rec included ~prefix t1 t2 =
   match (repr t1).desc, (repr t2).desc with
-    Tvar, _ -> true
+    Tvar _, _ -> true
   | Tvariant row1, Tvariant row2 ->
       let row1 = row_repr row1 and row2 = row_repr row2 in
       let fields1 = filter_row_fields false row1.row_fields
diff --git a/testsuite/tests/lib-hashtbl/htbl.ml b/testsuite/tests/lib-hashtbl/htbl.ml
index 5b46afb5ef..84a71beb77 100644
--- a/testsuite/tests/lib-hashtbl/htbl.ml
+++ b/testsuite/tests/lib-hashtbl/htbl.ml
@@ -76,7 +76,7 @@ module HofM (M: Map.S) : Hashtbl.S with type key = M.key =
   struct
     type key = M.key
     type 'a t = (key, 'a) Hashtbl.t
-    let create = Hashtbl.create
+    let create s = Hashtbl.create s
     let clear = Hashtbl.clear
     let copy = Hashtbl.copy
     let add = Hashtbl.add
diff --git a/testsuite/tests/typing-implicit_unpack/implicit_unpack.ml.reference b/testsuite/tests/typing-implicit_unpack/implicit_unpack.ml.reference
index 6e2f486170..0291292bf7 100644
--- a/testsuite/tests/typing-implicit_unpack/implicit_unpack.ml.reference
+++ b/testsuite/tests/typing-implicit_unpack/implicit_unpack.ml.reference
@@ -108,8 +108,8 @@ module type MapT =
     val of_t : data t -> map
     val to_t : map -> data t
   end
-type ('a, 'b, 'c) map =
-    (module MapT with type data = 'b and type key = 'a and type map = 'c)
+type ('k, 'd, 'm) map =
+    (module MapT with type data = 'd and type key = 'k and type map = 'm)
 val add : ('a, 'b, 'c) map -> 'a -> 'b -> 'c -> 'c = <fun>
 module SSMap :
   sig
diff --git a/testsuite/tests/typing-objects/Tests.ml.reference b/testsuite/tests/typing-objects/Tests.ml.reference
index 74b1c25f94..7dde3fba0b 100644
--- a/testsuite/tests/typing-objects/Tests.ml.reference
+++ b/testsuite/tests/typing-objects/Tests.ml.reference
@@ -134,8 +134,8 @@ Error: The type abbreviation t is cyclic
 # # - : bool = true
 #     module M : sig class ['a] c : unit -> object method f : 'a -> unit end end
 #   module M' : sig class ['a] c : unit -> object method f : 'a -> unit end end
-# - : ('b #M.c as 'a) -> 'a = <fun>
-# - : ('b #M'.c as 'a) -> 'a = <fun>
+# - : ('a #M.c as 'b) -> 'b = <fun>
+# - : ('a #M'.c as 'b) -> 'b = <fun>
 # class ['a] c : 'a #c -> object  end
 # class ['a] c : 'a #c -> object  end
 #     class c : unit -> object method f : int end
diff --git a/testsuite/tests/typing-poly/poly.ml.principal.reference b/testsuite/tests/typing-poly/poly.ml.principal.reference
index 98da3b75ca..a87694bb77 100644
--- a/testsuite/tests/typing-poly/poly.ml.principal.reference
+++ b/testsuite/tests/typing-poly/poly.ml.principal.reference
@@ -3,17 +3,17 @@
 # type 'a fold = { fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b; }
 # val f : 'a list -> 'a fold = <fun>
 # - : int = 6
-#               class ['a] ilist :
-  'a list ->
-  object ('b)
-    val l : 'a list
-    method add : 'a -> 'b
-    method fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
+#               class ['b] ilist :
+  'b list ->
+  object ('c)
+    val l : 'b list
+    method add : 'b -> 'c
+    method fold : f:('a -> 'b -> 'a) -> init:'a -> 'a
   end
 #         class virtual ['a] vlist :
-  object ('b)
-    method virtual add : 'a -> 'b
-    method virtual fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
+  object ('c)
+    method virtual add : 'a -> 'c
+    method virtual fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
   end
 #             class ilist2 :
   int list ->
@@ -25,52 +25,52 @@
 #             val ilist2 : 'a list -> 'a vlist = <fun>
 #             class ['a] ilist3 :
   'a list ->
-  object ('b)
+  object ('c)
     val l : 'a list
-    method add : 'a -> 'b
-    method fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
+    method add : 'a -> 'c
+    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
   end
 #               class ['a] ilist4 :
   'a list ->
-  object ('b)
+  object ('c)
     val l : 'a list
-    method add : 'a -> 'b
-    method fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
+    method add : 'a -> 'c
+    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
   end
 #                 class ['a] ilist5 :
   'a list ->
-  object ('b)
+  object ('c)
     val l : 'a list
-    method add : 'a -> 'b
-    method fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
-    method fold2 : f:('d -> 'a -> 'd) -> init:'d -> 'd
+    method add : 'a -> 'c
+    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
+    method fold2 : f:('b -> 'a -> 'b) -> init:'b -> 'b
   end
 #                 class ['a] ilist6 :
   'a list ->
-  object ('b)
+  object ('c)
     val l : 'a list
-    method add : 'a -> 'b
-    method fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
-    method fold2 : f:('d -> 'a -> 'd) -> init:'d -> 'd
+    method add : 'a -> 'c
+    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
+    method fold2 : f:('b -> 'a -> 'b) -> init:'b -> 'b
   end
 #       class virtual ['a] olist :
-  object method virtual fold : f:('a -> 'b -> 'b) -> init:'b -> 'b end
+  object method virtual fold : f:('a -> 'c -> 'c) -> init:'c -> 'c end
 #         class ['a] onil :
-  object method fold : f:('a -> 'b -> 'b) -> init:'b -> 'b end
+  object method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c end
 #             class ['a] ocons :
   hd:'a ->
   tl:'a olist ->
   object
     val hd : 'a
     val tl : 'a olist
-    method fold : f:('a -> 'b -> 'b) -> init:'b -> 'b
+    method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c
   end
 #               class ['a] ostream :
   hd:'a ->
   tl:'a ostream ->
   object
     val hd : 'a
-    val tl : < empty : bool; fold : 'b. f:('a -> 'b -> 'b) -> init:'b -> 'b >
+    val tl : < empty : bool; fold : 'c. f:('a -> 'c -> 'c) -> init:'c -> 'c >
     method empty : bool
     method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c
   end
@@ -123,9 +123,9 @@ val d : float = 11.4536240470737098
 #   Characters 41-42:
   let f (x : < m : 'a. 'a -> 'a list >) = (x : < m : 'b. 'b -> 'c >)
                                            ^
-Error: This expression has type < m : 'a. 'a -> 'a list >
-       but an expression was expected of type < m : 'a. 'a -> 'b >
-       The universal variable 'a would escape its scope
+Error: This expression has type < m : 'b. 'b -> 'b list >
+       but an expression was expected of type < m : 'b. 'b -> 'c >
+       The universal variable 'b would escape its scope
 #           class id : object method id : 'a -> 'a end
 #         class type id_spec = object method id : 'a -> 'a end
 #       class id_impl : object method id : 'a -> 'a end
@@ -142,13 +142,13 @@ Error: This method has type 'a -> 'a which is less general than 'b. 'b -> 'a
 #           Characters 80-85:
     method id _ = x
               ^^^^^
-Error: This method has type 'a -> 'a which is less general than 'b. 'b -> 'b
+Error: This method has type 'b -> 'b which is less general than 'a. 'a -> 'a
 #                 Characters 92-159:
   ............x =
       match r with
         None -> r <- Some x; x
       | Some y -> y
-Error: This method has type 'a -> 'a which is less general than 'b. 'b -> 'b
+Error: This method has type 'b -> 'b which is less general than 'a. 'a -> 'a
 #         class c : object method m : 'a -> 'b -> 'a end
 #     val f1 : id -> int * bool = <fun>
 #   val f2 : id -> int * bool = <fun>
@@ -175,9 +175,9 @@ val f4 : id -> int * bool = <fun>
 Error: The type abbreviation foo is cyclic
 #     class ['a] bar : 'a -> object  end
 #   type 'a foo = 'a foo bar
-#   - : (< m : 'b. 'b * 'a > as 'a) -> 'c * (< m : 'e. 'e * 'd > as 'd) = <fun>
-# - : (< m : 'b. 'a * 'b list > as 'a) ->
-    (< m : 'd. 'c * 'd list > as 'c) * 'e list
+#   - : (< m : 'a. 'a * 'b > as 'b) -> 'c * (< m : 'a. 'a * 'd > as 'd) = <fun>
+# - : (< m : 'a. 'b * 'a list > as 'b) ->
+    (< m : 'a. 'c * 'a list > as 'c) * 'd list
 = <fun>
 # val f :
   (< m : 'b. 'a * (< n : 'b; .. > as 'b) > as 'a) ->
@@ -186,11 +186,11 @@ Error: The type abbreviation foo is cyclic
 # - : (< p : 'b. < m : 'b; n : 'a; .. > as 'b > as 'a) ->
     (< m : 'c; n : < p : 'e. < m : 'e; n : 'd; .. > as 'e > as 'd; .. > as 'c)
 = <fun>
-# - : (< m : 'b. 'b * < p : 'd. 'd * 'c * 'a > as 'c > as 'a) ->
+# - : (< m : 'a. 'a * < p : 'b. 'b * 'd * 'c > as 'd > as 'c) ->
     ('f *
-     < p : 'g.
-             'g * 'e *
-             (< m : 'i. 'i * < p : 'k. 'k * 'j * 'h > as 'j > as 'h) >
+     < p : 'b.
+             'b * 'e *
+             (< m : 'a. 'a * < p : 'b0. 'b0 * 'h * 'g > as 'h > as 'g) >
      as 'e)
 = <fun>
 #   - : < m : 'a. < p : 'a; .. > as 'b > -> 'b = <fun>
@@ -199,14 +199,14 @@ Error: The type abbreviation foo is cyclic
 #   type record = { r : < id : 'a. 'a -> 'a >; }
 # - : record -> 'a -> 'a = <fun>
 # - : record -> 'a -> 'a = <fun>
-#       class myself : object ('a) method self : 'b -> 'a end
+#       class myself : object ('b) method self : 'a -> 'b end
 #                       class number :
-  object ('a)
+  object ('b)
     val num : int
     method num : int
-    method prev : 'a
-    method succ : 'a
-    method switch : zero:(unit -> 'b) -> prev:('a -> 'b) -> 'b
+    method prev : 'b
+    method succ : 'b
+    method switch : zero:(unit -> 'a) -> prev:('b -> 'a) -> 'a
   end
 #     val id : 'a -> 'a = <fun>
 #       class c : object method id : 'a -> 'a end
@@ -216,14 +216,14 @@ Error: The type abbreviation foo is cyclic
     val mutable count : int
     method count : int
     method id : 'a -> 'a
-    method old : 'b -> 'b
+    method old : 'a -> 'a
   end
 #             class ['a] olist :
   'a list ->
-  object ('b)
+  object ('c)
     val l : 'a list
-    method cons : 'a -> 'b
-    method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c
+    method cons : 'a -> 'c
+    method fold : f:('a -> 'b -> 'b) -> init:'b -> 'b
   end
 #   val sum : int #olist -> int = <fun>
 #   val count : 'a #olist -> int = <fun>
@@ -244,16 +244,16 @@ class next : #numeral -> object method fold : ('a -> 'a) -> 'a -> 'a end
 # Characters 17-25:
   let bad = {bad = ref None};;
                    ^^^^^^^^
-Error: This field value has type 'a option ref which is less general than
-         'b. 'b option ref
+Error: This field value has type 'b option ref which is less general than
+         'a. 'a option ref
 # type bad2 = { mutable bad2 : 'a. 'a option ref option; }
 # val bad2 : bad2 = {bad2 = None}
 # Characters 13-28:
   bad2.bad2 <- Some (ref None);;
                ^^^^^^^^^^^^^^^
-Error: This field value has type 'a option ref option
-       which is less general than 'b. 'b option ref option
-#       val f : < m : 'a. < p : 'a * 'b > as 'b > -> 'c -> unit = <fun>
+Error: This field value has type 'b option ref option
+       which is less general than 'a. 'a option ref option
+#       val f : < m : 'a. < p : 'a * 'c > as 'c > -> 'b -> unit = <fun>
 # val f :
   < m : 'a. 'a * (< p : int * 'b > as 'b) > ->
   (< p : int * 'c > as 'c) -> unit = <fun>
@@ -268,7 +268,7 @@ Error: This field value has type 'a option ref option
 Error: This type scheme cannot quantify 'a :
 it escapes this scope.
 #                 type ('a, 'b) list_visitor = < caseCons : 'b -> 'b list -> 'a; caseNil : 'a >
-type 'a alist = < visit : 'b. ('b, 'a) list_visitor -> 'b >
+type 'b alist = < visit : 'a. ('a, 'b) list_visitor -> 'a >
 class type ct = object ('a) method fold : ('b -> 'a -> 'b) -> 'b -> 'b end
 type t = { f : 'a 'b. ('b -> (#ct as 'a) -> 'b) -> 'b; }
 #     Characters 20-25:
@@ -412,9 +412,9 @@ Error: This object is expected to have type < x : int; .. >
 #         Characters 76-77:
     (x : <m : 'a. 'a * (<m:'b. 'a * <m:'c. 'c * 'bar> > as 'bar) >);;
      ^
-Error: This expression has type < m : 'b. 'b * < m : 'b * 'a > > as 'a
+Error: This expression has type < m : 'a. 'a * < m : 'a * 'b > > as 'b
        but an expression was expected of type
-         < m : 'b. 'b * (< m : 'b * < m : 'd. 'd * 'c > > as 'c) >
+         < m : 'a. 'a * (< m : 'a * < m : 'c. 'c * 'd > > as 'd) >
        Types for method m are incompatible
 #         Characters 176-177:
   let f (x : foo') = (x : bar');;
@@ -422,70 +422,70 @@ Error: This expression has type < m : 'b. 'b * < m : 'b * 'a > > as 'a
 Error: This expression has type foo' = < m : 'a. 'a * 'a foo >
        but an expression was expected of type bar' = < m : 'a. 'a * 'a bar >
        Type 'a foo = < m : 'a * 'a foo > is not compatible with type
-         'a bar = < m : 'a * < m : 'b. 'b * 'a bar > > 
+         'a bar = < m : 'a * < m : 'c. 'c * 'a bar > > 
        Type 'a foo = < m : 'a * 'a foo > is not compatible with type
-         < m : 'b. 'b * 'a bar > 
+         < m : 'c. 'c * 'a bar > 
        Types for method m are incompatible
 #     Characters 67-68:
     (x : <m : 'b. 'b * ('b * <m : 'c. 'c * ('c * 'bar)>)> as 'bar);;
      ^
 Error: This expression has type
-         < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) >
+         < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) >
        but an expression was expected of type
-         < m : 'a. 'a * ('a * < m : 'c. 'c * ('c * 'd) >) > as 'd
+         < m : 'b. 'b * ('b * < m : 'c. 'c * ('c * 'd) >) > as 'd
        Types for method m are incompatible
 #   Characters 66-67:
     (x : <m : 'b. 'b * ('b * <m : 'c. 'c * ('b * 'bar)>)> as 'bar);;
      ^
 Error: This expression has type
-         < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) >
+         < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) >
        but an expression was expected of type
-         < m : 'a. 'a * ('a * < m : 'c. 'c * ('a * 'd) >) > as 'd
+         < m : 'b. 'b * ('b * < m : 'c. 'c * ('b * 'd) >) > as 'd
        Types for method m are incompatible
 #   Characters 51-52:
     (x : <m : 'b. 'b * ('b * <m:'c. 'c * 'bar> as 'bar)>);;
      ^
 Error: This expression has type < m : 'b. 'b * ('b * 'a) > as 'a
        but an expression was expected of type
-         < m : 'b. 'b * ('b * < m : 'd. 'd * 'c > as 'c) >
+         < m : 'b. 'b * ('b * < m : 'c. 'c * 'd > as 'd) >
        Types for method m are incompatible
 #     Characters 14-115:
   ....(x : <m : 'a. 'a -> ('a * <m:'c. 'c -> 'bar> as 'bar)>
          :> <m : 'a. 'a -> ('a * 'foo)> as 'foo)..
-Error: Type < m : 'a. 'a -> ('a * (< m : 'd. 'd -> 'b as 'e > as 'c) as 'b) >
+Error: Type < m : 'a. 'a -> ('a * (< m : 'c. 'c -> 'b as 'e > as 'd) as 'b) >
        is not a subtype of < m : 'a. 'a -> ('a * 'f as 'h) as 'g > as 'f 
 #       Characters 88-150:
   = struct let f (x : <m : 'a. 'a * ('a * 'foo)> as 'foo) = () end;;
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: Signature mismatch:
        Modules do not match:
-         sig val f : (< m : 'b. 'b * ('b * 'a) > as 'a) -> unit end
+         sig val f : (< m : 'a. 'a * ('a * 'b) > as 'b) -> unit end
        is not included in
          sig
-           val f : < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) > -> unit
+           val f : < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > -> unit
          end
        Values do not match:
-         val f : (< m : 'b. 'b * ('b * 'a) > as 'a) -> unit
+         val f : (< m : 'a. 'a * ('a * 'b) > as 'b) -> unit
        is not included in
-         val f : < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) > -> unit
+         val f : < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > -> unit
 #     Characters 78-132:
   = struct type t = <m : 'a. 'a * ('a * 'foo)> as 'foo end;;
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: Signature mismatch:
        Modules do not match:
-         sig type t = < m : 'b. 'b * ('b * 'a) > as 'a end
+         sig type t = < m : 'a. 'a * ('a * 'b) > as 'b end
        is not included in
-         sig type t = < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) > end
+         sig type t = < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > end
        Type declarations do not match:
-         type t = < m : 'b. 'b * ('b * 'a) > as 'a
+         type t = < m : 'a. 'a * ('a * 'b) > as 'b
        is not included in
-         type t = < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) >
+         type t = < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) >
 #     module M : sig type 'a t type u = < m : 'a. 'a t > end
 #   module M : sig type 'a t val f : < m : 'a. 'a t > -> int end
 #     module M : sig type 'a t val f : < m : 'a. 'a t > -> int end
 #         val f :
-  (< m : 'b. 'b -> (< m : 'b. 'b -> 'c * <  > > as 'c) * < .. >; .. > as 'a) ->
-  'a -> bool = <fun>
+  (< m : 'a. 'a -> (< m : 'a. 'a -> 'c * <  > > as 'c) * < .. >; .. > as 'b) ->
+  'b -> bool = <fun>
 #         type t = [ `A | `B ]
 # type v = private [> t ]
 # - : t -> v = <fun>
@@ -519,7 +519,7 @@ Error: Type < m : 'a. (< p : int; .. > as 'a) -> int > is not a subtype of
   ..(x : <m:'a. (<p:<a:int;b:int>;..> as 'a) -> int>
       :> <m:'b. (<p:<a:int>;..> as 'b) -> int>)..
 Error: Type < m : 'a. (< p : < a : int; b : int >; .. > as 'a) -> int >
-       is not a subtype of < m : 'a. (< p : < a : int >; .. > as 'a) -> int > 
+       is not a subtype of < m : 'b. (< p : < a : int >; .. > as 'b) -> int > 
 # Characters 11-55:
   let f4 x = (x : <p:<a:int;b:int>;..> :> <p:<a:int>;..>);;
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -533,7 +533,7 @@ The second object type has no method b
     (x : <m:'a. [< `A of < > ] as 'a> :> <m:'a. [< `A of <p:int> ] as 'a>);;
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: Type < m : 'a. [< `A of <  > ] as 'a > is not a subtype of
-         < m : 'a. [< `A of < p : int > ] as 'a > 
+         < m : 'b. [< `A of < p : int > ] as 'b > 
 #     val f : < m : 'a. 'a -> 'a > -> < m : 'a. 'a -> 'a > = <fun>
 # Characters 9-16:
   fun x -> (f x)#m;; (* Warning 18 *)
@@ -569,8 +569,8 @@ val g : 'a -> int = <fun>
 #     Characters 34-74:
     function Leaf _ -> 1 | Node x -> 1 + d x
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This definition has type 'a t -> int which is less general than
-         'b. 'b t -> int
+Error: This definition has type 'b t -> int which is less general than
+         'a. 'a t -> int
 #   Characters 34-78:
     function Leaf x -> x | Node x -> 1 + depth x;; (* fails *)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -579,13 +579,13 @@ Error: This definition has type int t -> int which is less general than
 #   Characters 34-74:
     function Leaf x -> x | Node x -> depth x;; (* fails *)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This definition has type 'a t -> 'a which is less general than
-         'b. 'b t -> 'a
+Error: This definition has type 'b t -> 'b which is less general than
+         'a. 'a t -> 'b
 #   Characters 38-78:
     function Leaf x -> x | Node x -> depth x;; (* fails *)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This definition has type 'a. 'a t -> 'a which is less general than
-         'b 'c. 'c t -> 'b
+Error: This definition has type 'c. 'c t -> 'c which is less general than
+         'b 'a. 'a t -> 'b
 #   val r : 'a list * '_b list ref = ([], {contents = []})
 val q : unit -> 'a list * '_b list ref = <fun>
 # val f : 'a -> 'a = <fun>
@@ -620,9 +620,9 @@ Error: This field value has type unit -> unit which is less general than
          'a. 'a -> unit
 #               module Polux :
   sig
-    type 'a t = 'a
+    type 'par t = 'par
     val ident : 'a -> 'a
     class alias : object method alias : 'a t -> 'a end
-    val f : < m : 'a. 'a t > -> < m : 'b. 'b >
+    val f : < m : 'a. 'a t > -> < m : 'a. 'a >
   end
 # 
diff --git a/testsuite/tests/typing-poly/poly.ml.reference b/testsuite/tests/typing-poly/poly.ml.reference
index e158e8a825..1e11ed0992 100644
--- a/testsuite/tests/typing-poly/poly.ml.reference
+++ b/testsuite/tests/typing-poly/poly.ml.reference
@@ -3,17 +3,17 @@
 # type 'a fold = { fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b; }
 # val f : 'a list -> 'a fold = <fun>
 # - : int = 6
-#               class ['a] ilist :
-  'a list ->
-  object ('b)
-    val l : 'a list
-    method add : 'a -> 'b
-    method fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
+#               class ['b] ilist :
+  'b list ->
+  object ('c)
+    val l : 'b list
+    method add : 'b -> 'c
+    method fold : f:('a -> 'b -> 'a) -> init:'a -> 'a
   end
 #         class virtual ['a] vlist :
-  object ('b)
-    method virtual add : 'a -> 'b
-    method virtual fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
+  object ('c)
+    method virtual add : 'a -> 'c
+    method virtual fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
   end
 #             class ilist2 :
   int list ->
@@ -25,45 +25,45 @@
 #             val ilist2 : 'a list -> 'a vlist = <fun>
 #             class ['a] ilist3 :
   'a list ->
-  object ('b)
+  object ('c)
     val l : 'a list
-    method add : 'a -> 'b
-    method fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
+    method add : 'a -> 'c
+    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
   end
 #               class ['a] ilist4 :
   'a list ->
-  object ('b)
+  object ('c)
     val l : 'a list
-    method add : 'a -> 'b
-    method fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
+    method add : 'a -> 'c
+    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
   end
 #                 class ['a] ilist5 :
   'a list ->
-  object ('b)
+  object ('c)
     val l : 'a list
-    method add : 'a -> 'b
-    method fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
-    method fold2 : f:('d -> 'a -> 'd) -> init:'d -> 'd
+    method add : 'a -> 'c
+    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
+    method fold2 : f:('b -> 'a -> 'b) -> init:'b -> 'b
   end
 #                 class ['a] ilist6 :
   'a list ->
-  object ('b)
+  object ('c)
     val l : 'a list
-    method add : 'a -> 'b
-    method fold : f:('c -> 'a -> 'c) -> init:'c -> 'c
-    method fold2 : f:('d -> 'a -> 'd) -> init:'d -> 'd
+    method add : 'a -> 'c
+    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
+    method fold2 : f:('b -> 'a -> 'b) -> init:'b -> 'b
   end
 #       class virtual ['a] olist :
-  object method virtual fold : f:('a -> 'b -> 'b) -> init:'b -> 'b end
+  object method virtual fold : f:('a -> 'c -> 'c) -> init:'c -> 'c end
 #         class ['a] onil :
-  object method fold : f:('a -> 'b -> 'b) -> init:'b -> 'b end
+  object method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c end
 #             class ['a] ocons :
   hd:'a ->
   tl:'a olist ->
   object
     val hd : 'a
     val tl : 'a olist
-    method fold : f:('a -> 'b -> 'b) -> init:'b -> 'b
+    method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c
   end
 #               class ['a] ostream :
   hd:'a ->
@@ -72,7 +72,7 @@
     val hd : 'a
     val tl : 'a ostream
     method empty : bool
-    method fold : f:('a -> 'b -> 'b) -> init:'b -> 'b
+    method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c
   end
 #                   class ['a] ostream1 :
   hd:'a ->
@@ -119,13 +119,13 @@ val p1 : point = <obj>
 val cp : color_point = <obj>
 val c : circle = <obj>
 val d : float = 11.4536240470737098
-#   val f : < m : 'a. 'a -> 'a > -> < m : 'a. 'a -> 'a > = <fun>
+#   val f : < m : 'b. 'b -> 'b > -> < m : 'b. 'b -> 'b > = <fun>
 #   Characters 41-42:
   let f (x : < m : 'a. 'a -> 'a list >) = (x : < m : 'b. 'b -> 'c >)
                                            ^
-Error: This expression has type < m : 'a. 'a -> 'a list >
-       but an expression was expected of type < m : 'a. 'a -> 'b >
-       The universal variable 'a would escape its scope
+Error: This expression has type < m : 'b. 'b -> 'b list >
+       but an expression was expected of type < m : 'b. 'b -> 'c >
+       The universal variable 'b would escape its scope
 #           class id : object method id : 'a -> 'a end
 #         class type id_spec = object method id : 'a -> 'a end
 #       class id_impl : object method id : 'a -> 'a end
@@ -142,13 +142,13 @@ Error: This method has type 'a -> 'a which is less general than 'b. 'b -> 'a
 #           Characters 80-85:
     method id _ = x
               ^^^^^
-Error: This method has type 'a -> 'a which is less general than 'b. 'b -> 'b
+Error: This method has type 'b -> 'b which is less general than 'a. 'a -> 'a
 #                 Characters 92-159:
   ............x =
       match r with
         None -> r <- Some x; x
       | Some y -> y
-Error: This method has type 'a -> 'a which is less general than 'b. 'b -> 'b
+Error: This method has type 'b -> 'b which is less general than 'a. 'a -> 'a
 #         class c : object method m : 'a -> 'b -> 'a end
 #     val f1 : id -> int * bool = <fun>
 #   val f2 : id -> int * bool = <fun>
@@ -167,16 +167,16 @@ Error: This expression has type bool but an expression was expected of type
 Error: The type abbreviation foo is cyclic
 #     class ['a] bar : 'a -> object  end
 #   type 'a foo = 'a foo bar
-#   - : (< m : 'b. 'b * 'a > as 'a) -> 'c * 'a = <fun>
-# - : (< m : 'b. 'a * 'b list > as 'a) -> 'a * 'c list = <fun>
+#   - : (< m : 'a. 'a * 'b > as 'b) -> 'c * 'b = <fun>
+# - : (< m : 'a. 'b * 'a list > as 'b) -> 'b * 'c list = <fun>
 # val f :
   (< m : 'b. 'a * (< n : 'b; .. > as 'b) > as 'a) ->
   'a * (< n : 'c; .. > as 'c) = <fun>
 # - : (< p : 'b. < m : 'b; n : 'a; .. > as 'b > as 'a) ->
     (< m : 'c; n : 'a; .. > as 'c)
 = <fun>
-# - : (< m : 'b. 'b * < p : 'd. 'd * 'c * 'a > as 'c > as 'a) ->
-    ('f * < p : 'g. 'g * 'e * 'a > as 'e)
+# - : (< m : 'a. 'a * < p : 'b. 'b * 'd * 'c > as 'd > as 'c) ->
+    ('f * < p : 'b. 'b * 'e * 'c > as 'e)
 = <fun>
 #   - : < m : 'a. < p : 'a; .. > as 'b > -> 'b = <fun>
 #   type sum = T of < id : 'a. 'a -> 'a >
@@ -184,14 +184,14 @@ Error: The type abbreviation foo is cyclic
 #   type record = { r : < id : 'a. 'a -> 'a >; }
 # - : record -> 'a -> 'a = <fun>
 # - : record -> 'a -> 'a = <fun>
-#       class myself : object ('a) method self : 'b -> 'a end
+#       class myself : object ('b) method self : 'a -> 'b end
 #                       class number :
-  object ('a)
+  object ('b)
     val num : int
     method num : int
-    method prev : 'a
-    method succ : 'a
-    method switch : zero:(unit -> 'b) -> prev:('a -> 'b) -> 'b
+    method prev : 'b
+    method succ : 'b
+    method switch : zero:(unit -> 'a) -> prev:('b -> 'a) -> 'a
   end
 #     val id : 'a -> 'a = <fun>
 #       class c : object method id : 'a -> 'a end
@@ -201,14 +201,14 @@ Error: The type abbreviation foo is cyclic
     val mutable count : int
     method count : int
     method id : 'a -> 'a
-    method old : 'b -> 'b
+    method old : 'a -> 'a
   end
 #             class ['a] olist :
   'a list ->
-  object ('b)
+  object ('c)
     val l : 'a list
-    method cons : 'a -> 'b
-    method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c
+    method cons : 'a -> 'c
+    method fold : f:('a -> 'b -> 'b) -> init:'b -> 'b
   end
 #   val sum : int #olist -> int = <fun>
 #   val count : 'a #olist -> int = <fun>
@@ -229,16 +229,16 @@ class next : #numeral -> object method fold : ('a -> 'a) -> 'a -> 'a end
 # Characters 17-25:
   let bad = {bad = ref None};;
                    ^^^^^^^^
-Error: This field value has type 'a option ref which is less general than
-         'b. 'b option ref
+Error: This field value has type 'b option ref which is less general than
+         'a. 'a option ref
 # type bad2 = { mutable bad2 : 'a. 'a option ref option; }
 # val bad2 : bad2 = {bad2 = None}
 # Characters 13-28:
   bad2.bad2 <- Some (ref None);;
                ^^^^^^^^^^^^^^^
-Error: This field value has type 'a option ref option
-       which is less general than 'b. 'b option ref option
-#       val f : < m : 'a. < p : 'a * 'b > as 'b > -> 'c -> unit = <fun>
+Error: This field value has type 'b option ref option
+       which is less general than 'a. 'a option ref option
+#       val f : < m : 'a. < p : 'a * 'c > as 'c > -> 'b -> unit = <fun>
 # val f : < m : 'a. 'a * (< p : int * 'b > as 'b) > -> 'b -> unit = <fun>
 #       type 'a t = [ `A of 'a ]
 #       class c : object method m : ([> 'a t ] as 'a) -> unit end
@@ -251,7 +251,7 @@ Error: This field value has type 'a option ref option
 Error: This type scheme cannot quantify 'a :
 it escapes this scope.
 #                 type ('a, 'b) list_visitor = < caseCons : 'b -> 'b list -> 'a; caseNil : 'a >
-type 'a alist = < visit : 'b. ('b, 'a) list_visitor -> 'b >
+type 'b alist = < visit : 'a. ('a, 'b) list_visitor -> 'a >
 class type ct = object ('a) method fold : ('b -> 'a -> 'b) -> 'b -> 'b end
 type t = { f : 'a 'b. ('b -> (#ct as 'a) -> 'b) -> 'b; }
 #     Characters 20-25:
@@ -395,9 +395,9 @@ Error: This object is expected to have type < x : int; .. >
 #         Characters 76-77:
     (x : <m : 'a. 'a * (<m:'b. 'a * <m:'c. 'c * 'bar> > as 'bar) >);;
      ^
-Error: This expression has type < m : 'b. 'b * < m : 'b * 'a > > as 'a
+Error: This expression has type < m : 'a. 'a * < m : 'a * 'b > > as 'b
        but an expression was expected of type
-         < m : 'b. 'b * (< m : 'b * < m : 'd. 'd * 'c > > as 'c) >
+         < m : 'a. 'a * (< m : 'a * < m : 'c. 'c * 'd > > as 'd) >
        Types for method m are incompatible
 #         Characters 176-177:
   let f (x : foo') = (x : bar');;
@@ -405,70 +405,70 @@ Error: This expression has type < m : 'b. 'b * < m : 'b * 'a > > as 'a
 Error: This expression has type foo' = < m : 'a. 'a * 'a foo >
        but an expression was expected of type bar' = < m : 'a. 'a * 'a bar >
        Type 'a foo = < m : 'a * 'a foo > is not compatible with type
-         'a bar = < m : 'a * < m : 'b. 'b * 'a bar > > 
+         'a bar = < m : 'a * < m : 'c. 'c * 'a bar > > 
        Type 'a foo = < m : 'a * 'a foo > is not compatible with type
-         < m : 'b. 'b * 'a bar > 
+         < m : 'c. 'c * 'a bar > 
        Types for method m are incompatible
 #     Characters 67-68:
     (x : <m : 'b. 'b * ('b * <m : 'c. 'c * ('c * 'bar)>)> as 'bar);;
      ^
 Error: This expression has type
-         < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) >
+         < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) >
        but an expression was expected of type
-         < m : 'a. 'a * ('a * < m : 'c. 'c * ('c * 'd) >) > as 'd
+         < m : 'b. 'b * ('b * < m : 'c. 'c * ('c * 'd) >) > as 'd
        Types for method m are incompatible
 #   Characters 66-67:
     (x : <m : 'b. 'b * ('b * <m : 'c. 'c * ('b * 'bar)>)> as 'bar);;
      ^
 Error: This expression has type
-         < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) >
+         < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) >
        but an expression was expected of type
-         < m : 'a. 'a * ('a * < m : 'c. 'c * ('a * 'd) >) > as 'd
+         < m : 'b. 'b * ('b * < m : 'c. 'c * ('b * 'd) >) > as 'd
        Types for method m are incompatible
 #   Characters 51-52:
     (x : <m : 'b. 'b * ('b * <m:'c. 'c * 'bar> as 'bar)>);;
      ^
 Error: This expression has type < m : 'b. 'b * ('b * 'a) > as 'a
        but an expression was expected of type
-         < m : 'b. 'b * ('b * < m : 'd. 'd * 'c > as 'c) >
+         < m : 'b. 'b * ('b * < m : 'c. 'c * 'd > as 'd) >
        Types for method m are incompatible
 #     Characters 14-115:
   ....(x : <m : 'a. 'a -> ('a * <m:'c. 'c -> 'bar> as 'bar)>
          :> <m : 'a. 'a -> ('a * 'foo)> as 'foo)..
-Error: Type < m : 'a. 'a -> ('a * (< m : 'd. 'd -> 'b as 'e > as 'c) as 'b) >
+Error: Type < m : 'a. 'a -> ('a * (< m : 'c. 'c -> 'b as 'e > as 'd) as 'b) >
        is not a subtype of < m : 'a. 'a -> ('a * 'f as 'h) as 'g > as 'f 
 #       Characters 88-150:
   = struct let f (x : <m : 'a. 'a * ('a * 'foo)> as 'foo) = () end;;
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: Signature mismatch:
        Modules do not match:
-         sig val f : (< m : 'b. 'b * ('b * 'a) > as 'a) -> unit end
+         sig val f : (< m : 'a. 'a * ('a * 'b) > as 'b) -> unit end
        is not included in
          sig
-           val f : < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) > -> unit
+           val f : < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > -> unit
          end
        Values do not match:
-         val f : (< m : 'b. 'b * ('b * 'a) > as 'a) -> unit
+         val f : (< m : 'a. 'a * ('a * 'b) > as 'b) -> unit
        is not included in
-         val f : < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) > -> unit
+         val f : < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > -> unit
 #     Characters 78-132:
   = struct type t = <m : 'a. 'a * ('a * 'foo)> as 'foo end;;
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: Signature mismatch:
        Modules do not match:
-         sig type t = < m : 'b. 'b * ('b * 'a) > as 'a end
+         sig type t = < m : 'a. 'a * ('a * 'b) > as 'b end
        is not included in
-         sig type t = < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) > end
+         sig type t = < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > end
        Type declarations do not match:
-         type t = < m : 'b. 'b * ('b * 'a) > as 'a
+         type t = < m : 'a. 'a * ('a * 'b) > as 'b
        is not included in
-         type t = < m : 'a. 'a * ('a * < m : 'c. 'c * 'b > as 'b) >
+         type t = < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) >
 #     module M : sig type 'a t type u = < m : 'a. 'a t > end
 #   module M : sig type 'a t val f : < m : 'a. 'a t > -> int end
 #     module M : sig type 'a t val f : < m : 'a. 'a t > -> int end
 #         val f :
-  (< m : 'b. 'b -> (< m : 'b. 'b -> 'c * <  > > as 'c) * < .. >; .. > as 'a) ->
-  'a -> bool = <fun>
+  (< m : 'a. 'a -> (< m : 'a. 'a -> 'c * <  > > as 'c) * < .. >; .. > as 'b) ->
+  'b -> bool = <fun>
 #         type t = [ `A | `B ]
 # type v = private [> t ]
 # - : t -> v = <fun>
@@ -497,12 +497,12 @@ Error: Type < m : 'a. (< p : int; .. > as 'a) -> int > is not a subtype of
          < m : 'b. (< p : int; q : int; .. > as 'b) -> int > 
 #     val f2 :
   < m : 'a. (< p : < a : int >; .. > as 'a) -> int > ->
-  < m : 'a. (< p : < a : int; b : int >; .. > as 'a) -> int > = <fun>
+  < m : 'b. (< p : < a : int; b : int >; .. > as 'b) -> int > = <fun>
 #     Characters 13-107:
   ..(x : <m:'a. (<p:<a:int;b:int>;..> as 'a) -> int>
       :> <m:'b. (<p:<a:int>;..> as 'b) -> int>)..
 Error: Type < m : 'a. (< p : < a : int; b : int >; .. > as 'a) -> int >
-       is not a subtype of < m : 'a. (< p : < a : int >; .. > as 'a) -> int > 
+       is not a subtype of < m : 'b. (< p : < a : int >; .. > as 'b) -> int > 
 # Characters 11-55:
   let f4 x = (x : <p:<a:int;b:int>;..> :> <p:<a:int>;..>);;
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -511,12 +511,12 @@ Error: Type < p : < a : int; b : int >; .. > is not a subtype of
 The second object type has no method b
 #   val f5 :
   < m : 'a. [< `A of < p : int > ] as 'a > ->
-  < m : 'a. [< `A of <  > ] as 'a > = <fun>
+  < m : 'b. [< `A of <  > ] as 'b > = <fun>
 #   Characters 13-83:
     (x : <m:'a. [< `A of < > ] as 'a> :> <m:'a. [< `A of <p:int> ] as 'a>);;
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: Type < m : 'a. [< `A of <  > ] as 'a > is not a subtype of
-         < m : 'a. [< `A of < p : int > ] as 'a > 
+         < m : 'b. [< `A of < p : int > ] as 'b > 
 #     val f : < m : 'a. 'a -> 'a > -> < m : 'a. 'a -> 'a > = <fun>
 # - : < m : 'a. 'a -> 'a > -> 'b -> 'b = <fun>
 # val f : < m : 'a. 'a -> 'a > * 'b -> < m : 'a. 'a -> 'a > = <fun>
@@ -536,8 +536,8 @@ val g : 'a -> int = <fun>
 #     Characters 34-74:
     function Leaf _ -> 1 | Node x -> 1 + d x
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This definition has type 'a t -> int which is less general than
-         'b. 'b t -> int
+Error: This definition has type 'b t -> int which is less general than
+         'a. 'a t -> int
 #   Characters 34-78:
     function Leaf x -> x | Node x -> 1 + depth x;; (* fails *)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -546,13 +546,13 @@ Error: This definition has type int t -> int which is less general than
 #   Characters 34-74:
     function Leaf x -> x | Node x -> depth x;; (* fails *)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This definition has type 'a t -> 'a which is less general than
-         'b. 'b t -> 'a
+Error: This definition has type 'b t -> 'b which is less general than
+         'a. 'a t -> 'b
 #   Characters 38-78:
     function Leaf x -> x | Node x -> depth x;; (* fails *)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This definition has type 'a. 'a t -> 'a which is less general than
-         'b 'c. 'c t -> 'b
+Error: This definition has type 'c. 'c t -> 'c which is less general than
+         'b 'a. 'a t -> 'b
 #   val r : 'a list * '_b list ref = ([], {contents = []})
 val q : unit -> 'a list * '_b list ref = <fun>
 # val f : 'a -> 'a = <fun>
@@ -587,7 +587,7 @@ Error: This field value has type unit -> unit which is less general than
          'a. 'a -> unit
 #               module Polux :
   sig
-    type 'a t = 'a
+    type 'par t = 'par
     val ident : 'a -> 'a
     class alias : object method alias : 'a t -> 'a end
     val f : < m : 'a. 'a > -> < m : 'a. 'a >
diff --git a/toplevel/genprintval.ml b/toplevel/genprintval.ml
index fe91213f32..9d4311c85d 100644
--- a/toplevel/genprintval.ml
+++ b/toplevel/genprintval.ml
@@ -180,7 +180,7 @@ module Make(O : OBJ)(EVP : EVALPATH with type value = O.t) = struct
           find_printer env ty obj
         with Not_found ->
           match (Ctype.repr ty).desc with
-          | Tvar ->
+          | Tvar _ | Tunivar _ ->
               Oval_stuff "<poly>"
           | Tarrow(_, ty1, ty2, _) ->
               Oval_stuff "<fun>"
@@ -327,8 +327,6 @@ module Make(O : OBJ)(EVP : EVALPATH with type value = O.t) = struct
               fatal_error "Printval.outval_of_value"
           | Tpoly (ty, _) ->
               tree_of_val (depth - 1) obj ty
-          | Tunivar ->
-              Oval_stuff "<poly>"
           | Tpackage _ ->
               Oval_stuff "<module>"
         end
diff --git a/typing/btype.ml b/typing/btype.ml
index 96704aa020..67754d0ab6 100644
--- a/typing/btype.ml
+++ b/typing/btype.ml
@@ -35,9 +35,9 @@ let pivot_level = 2 * lowest_level - 1
 let new_id = ref (-1)
 
 let newty2 level desc  =
-  incr new_id; { desc = desc; level = level; id = !new_id }
+  incr new_id; { desc; level; id = !new_id }
 let newgenty desc      = newty2 generic_level desc
-let newgenvar ()       = newgenty Tvar
+let newgenvar ?name () = newgenty (Tvar name)
 (*
 let newmarkedvar level =
   incr new_id; { desc = Tvar; level = pivot_level - level; id = !new_id }
@@ -46,6 +46,11 @@ let newmarkedgenvar () =
   { desc = Tvar; level = pivot_level - generic_level; id = !new_id }
 *)
 
+(**** Check some types ****)
+
+let is_Tvar = function {desc=Tvar _} -> true | _ -> false
+let is_Tunivar = function {desc=Tunivar _} -> true | _ -> false
+
 (**** Representative of a type ****)
 
 let rec field_kind_repr =
@@ -139,7 +144,7 @@ let proxy ty =
       let rec proxy_obj ty =
         match ty.desc with
           Tfield (_, _, _, ty) | Tlink ty -> proxy_obj ty
-        | Tvar | Tunivar | Tconstr _ -> ty
+        | Tvar _ | Tunivar _ | Tconstr _ -> ty
         | Tnil -> ty0
         | _ -> assert false
       in proxy_obj ty
@@ -180,13 +185,13 @@ let rec iter_row f row =
     row.row_fields;
   match (repr row.row_more).desc with
     Tvariant row -> iter_row f row
-  | Tvar | Tunivar | Tsubst _ | Tconstr _ ->
+  | Tvar _ | Tunivar _ | Tsubst _ | Tconstr _ ->
       Misc.may (fun (_,l) -> List.iter f l) row.row_name
   | _ -> assert false
 
 let iter_type_expr f ty =
   match ty.desc with
-    Tvar                -> ()
+    Tvar _              -> ()
   | Tarrow (_, ty1, ty2, _) -> f ty1; f ty2
   | Ttuple l            -> List.iter f l
   | Tconstr (_, l, _)   -> List.iter f l
@@ -198,7 +203,7 @@ let iter_type_expr f ty =
   | Tnil                -> ()
   | Tlink ty            -> f ty
   | Tsubst ty           -> f ty
-  | Tunivar             -> ()
+  | Tunivar _           -> ()
   | Tpoly (ty, tyl)     -> f ty; List.iter f tyl
   | Tpackage (_, _, l)  -> List.iter f l
 
@@ -239,13 +244,13 @@ let copy_commu c =
    encoding during substitution *)
 let rec norm_univar ty =
   match ty.desc with
-    Tunivar | Tsubst _ -> ty
+    Tunivar _ | Tsubst _ -> ty
   | Tlink ty           -> norm_univar ty
   | Ttuple (ty :: _)   -> norm_univar ty
   | _                  -> assert false
 
 let rec copy_type_desc f = function
-    Tvar                -> Tvar
+    Tvar _              -> Tvar None (* forget the name *)
   | Tarrow (p, ty1, ty2, c)-> Tarrow (p, f ty1, f ty2, copy_commu c)
   | Ttuple l            -> Ttuple (List.map f l)
   | Tconstr (p, l, _)   -> Tconstr (p, List.map f l, ref Mnil)
@@ -258,7 +263,7 @@ let rec copy_type_desc f = function
   | Tnil                -> Tnil
   | Tlink ty            -> copy_type_desc f ty.desc
   | Tsubst ty           -> assert false
-  | Tunivar             -> Tunivar
+  | Tunivar _ as ty     -> ty (* keep the name *)
   | Tpoly (ty, tyl)     ->
       let tyl = List.map (fun x -> norm_univar (f x)) tyl in
       Tpoly (f ty, tyl)
@@ -447,7 +452,7 @@ type change =
   | Cuniv of type_expr option ref * type_expr option
 
 let undo_change = function
-    Ctype  (ty, desc)  -> ty.desc <- desc
+    Ctype  (ty, desc) -> ty.desc <- desc
   | Clevel (ty, level) -> ty.level <- level
   | Cname  (r, v) -> r := v
   | Crow   (r, v) -> r := v
@@ -474,7 +479,22 @@ let log_change ch =
 
 let log_type ty =
   if ty.id <= !last_snapshot then log_change (Ctype (ty, ty.desc))
-let link_type ty ty' = log_type ty; ty.desc <- Tlink ty'
+let link_type ty ty' =
+  log_type ty;
+  let desc = ty.desc in
+  ty.desc <- Tlink ty';
+  (* Name is a user-supplied name for this unification variable (obtained
+   * through a type annotation for instance). *)
+  match desc, ty'.desc with
+    Tvar name, Tvar name' ->
+      begin match name, name' with
+      | Some _, None ->  log_type ty'; ty'.desc <- Tvar name
+      | None, Some _ ->  ()
+      | Some _, Some _ ->
+          if ty.level < ty'.level then (log_type ty'; ty'.desc <- Tvar name)
+      | None, None   ->  ()
+      end
+  | _ -> ()
   (* ; assert (check_memorized_abbrevs ()) *)
   (*  ; check_expans [] ty' *)
 let set_level ty level =
diff --git a/typing/btype.mli b/typing/btype.mli
index fca2d90ed7..755c840c37 100644
--- a/typing/btype.mli
+++ b/typing/btype.mli
@@ -23,7 +23,7 @@ val newty2: int -> type_desc -> type_expr
         (* Create a type *)
 val newgenty: type_desc -> type_expr
         (* Create a generic type *)
-val newgenvar: unit -> type_expr
+val newgenvar: ?name:string -> unit -> type_expr
         (* Return a fresh generic variable *)
 
 (* Use Tsubst instead
@@ -33,6 +33,9 @@ val newmarkedgenvar: unit -> type_expr
         (* Return a fresh marked generic variable *)
 *)
 
+val is_Tvar: type_expr -> bool
+val is_Tunivar: type_expr -> bool
+
 val repr: type_expr -> type_expr
         (* Return the canonical representative of a type. *)
 
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 37b798304c..bd08aa235a 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -153,9 +153,9 @@ let newty2             = Btype.newty2
 let newty desc         = newty2 !current_level desc
 let new_global_ty desc = newty2 !global_level desc
 
-let newvar ()          = newty2 !current_level Tvar
-let newvar2 level      = newty2 level Tvar
-let new_global_var ()  = newty2 !global_level Tvar
+let newvar ?name ()         = newty2 !current_level (Tvar name)
+let newvar2 ?name level     = newty2 level (Tvar name)
+let new_global_var ?name () = newty2 !global_level (Tvar name)
 
 let newobj fields      = newty (Tobject (fields, ref None))
 
@@ -297,14 +297,12 @@ let rec object_row ty =
 
 let opened_object ty =
   match (object_row ty).desc with
-  | Tvar               -> true
-  | Tunivar            -> true
-  | Tconstr _          -> true
-  | _                  -> false
+  | Tvar _  | Tunivar _ | Tconstr _ -> true
+  | _                               -> false
 
 let concrete_object ty =
   match (object_row ty).desc with
-  | Tvar               -> false
+  | Tvar _             -> false
   | _                  -> true
 
 (**** Close an object ****)
@@ -313,7 +311,7 @@ let close_object ty =
   let rec close ty =
     let ty = repr ty in
     match ty.desc with
-      Tvar ->
+      Tvar _ ->
         link_type ty (newty2 ty.level Tnil)
     | Tfield(_, _, _, ty') -> close ty'
     | _                    -> assert false
@@ -329,7 +327,7 @@ let row_variable ty =
     let ty = repr ty in
     match ty.desc with
       Tfield (_, _, _, ty) -> find ty
-    | Tvar                 -> ty
+    | Tvar _               -> ty
     | _                    -> assert false
   in
   match (repr ty).desc with
@@ -434,7 +432,7 @@ let rec closed_schema_rec ty =
     let level = ty.level in
     ty.level <- pivot_level - level;
     match ty.desc with
-      Tvar when level <> generic_level ->
+      Tvar _ when level <> generic_level ->
         raise Non_closed
     | Tfield(_, kind, t1, t2) ->
         if field_kind_repr kind = Fpresent then
@@ -468,7 +466,7 @@ let rec free_vars_rec real ty =
   if ty.level >= lowest_level then begin
     ty.level <- pivot_level - ty.level;
     begin match ty.desc, !really_closed with
-      Tvar, _ ->
+      Tvar _, _ ->
         free_variables := (ty, real) :: !free_variables
     | Tconstr (path, tl, _), Some env ->
         begin try
@@ -639,7 +637,7 @@ let iterative_generalization min_level tyl =
 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
+    if is_Tvar ty && ty.level > var_level then
       set_level ty var_level
     else if ty.level > !current_level then begin
       set_level ty generic_level;
@@ -858,7 +856,7 @@ let compute_univars ty =
           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)
+  TypeHash.iter (fun ty inv -> if is_Tunivar ty then add_univar ty inv)
     inverted;
   fun ty ->
     try !(TypeHash.find node_univars ty) with Not_found -> TypeSet.empty
@@ -913,7 +911,7 @@ let rec copy ?partial ty =
             if keep then ty.level else !current_level
           else generic_level
     in
-    if forget <> generic_level then newty2 forget Tvar else
+    if forget <> generic_level then newty2 forget (Tvar None) else
     let desc = ty.desc in
     save_desc ty desc;
     let t = newvar() in          (* Stub *)
@@ -959,7 +957,7 @@ let rec copy ?partial ty =
                 | Tconstr _ ->
                     if keep then save_desc more more.desc;
                     copy more
-                | Tvar | Tunivar ->
+                | Tvar _ | Tunivar _ ->
                     save_desc more more.desc;
                     if keep then more else newty more.desc
                 |  _ -> assert false
@@ -1117,7 +1115,7 @@ let rec copy_sep fixed free bound visited ty =
     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
+    let dl = if is_Tunivar ty then [] else diff_list bound bound_t in
     if dl <> [] && conflicts univars dl then raise Not_found;
     t
   with Not_found -> begin
@@ -1134,14 +1132,14 @@ let rec copy_sep fixed free bound visited ty =
           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 keep = is_Tvar more && more.level <> generic_level in
           let more' = copy_rec more in
-          let fixed' = fixed && (repr more').desc = Tvar in
+          let fixed' = fixed && is_Tvar (repr 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 tl' = List.map (fun t -> newty t.desc) tl in
           let bound = tl @ bound in
           let visited =
             List.map2 (fun ty t -> ty,(t,bound)) tl tl' @ visited in
@@ -1395,7 +1393,7 @@ let enforce_constraints env ty =
 let rec full_expand env ty =
   let ty = repr (expand_head env ty) in
   match ty.desc with
-    Tobject (fi, {contents = Some (_, v::_)}) when (repr v).desc = Tvar ->
+    Tobject (fi, {contents = Some (_, v::_)}) when is_Tvar (repr v) ->
       newty2 ty.level (Tobject (fi, ref None))
   | _ ->
       ty
@@ -1570,8 +1568,8 @@ let occur_univar env ty =
         true
     then
       match ty.desc with
-        Tunivar ->
-          if not (TypeSet.mem ty bound) then raise (Unify [ty, newgenvar()])
+        Tunivar _ ->
+          if not (TypeSet.mem ty bound) then raise (Unify [ty, newgenvar ()])
       | Tpoly (ty, tyl) ->
           let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in
           occur_rec bound  ty
@@ -1620,7 +1618,7 @@ let univars_escape env univar_pairs vl ty =
         Tpoly (t, tl) ->
           if List.exists (fun t -> TypeSet.mem (repr t) family) tl then ()
           else occur t
-      | Tunivar ->
+      | Tunivar _ ->
           if TypeSet.mem t family then raise Occur
       | Tconstr (_, [], _) -> ()
       | Tconstr (p, tl, _) ->
@@ -1784,7 +1782,7 @@ let reify env t =
               t
           end;
         iter_type_expr (iterator visited) ty
-    | Tvar -> 
+    | Tvar _ -> 
         let t = create_fresh_constr ty.level false in
         link_type ty t
     | _ ->
@@ -1862,8 +1860,8 @@ let rec mcomp type_pairs subst env t1 t2 =
   let t2 = repr t2 in
   if t1 == t2 then () else
     match (t1.desc, t2.desc) with
-      | (Tvar, _)  
-      | (_, Tvar)  ->
+      | (Tvar _, _)  
+      | (_, Tvar _)  ->
         fatal_error "types should not include variables"
       | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
         ()
@@ -1877,7 +1875,7 @@ let rec mcomp type_pairs subst env t1 t2 =
           with Not_found ->
               TypePairs.add type_pairs (t1', t2') ();
               match (t1'.desc, t2'.desc) with
-                  (Tvar, Tvar) ->
+                  (Tvar _, Tvar _) ->
                     fatal_error "types should not include variables"
                 | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2
                   || !Clflags.classic && not (is_optional l1 || is_optional l2) ->
@@ -1903,7 +1901,7 @@ let rec mcomp type_pairs subst env t1 t2 =
                 | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
                   enter_poly env univar_pairs t1 tl1 t2 tl2
                     (mcomp type_pairs subst env)
-                | (Tunivar, Tunivar) ->
+                | (Tunivar _, Tunivar _) ->
                   unify_univar t1' t2' !univar_pairs
                 | (_, _) ->
                   raise (Unify [])
@@ -2048,21 +2046,21 @@ let rec unify (env:Env.t ref) t1 t2 =
   try
     type_changed := true;
     match (t1.desc, t2.desc) with
-      (Tvar, Tconstr _) when deep_occur t1 t2 ->
+      (Tvar _, Tconstr _) when deep_occur t1 t2 ->
         unify2 env t1 t2
-    | (Tconstr _, Tvar) when deep_occur t2 t1 ->
+    | (Tconstr _, Tvar _) when deep_occur t2 t1 ->
         unify2 env t1 t2
-    | (Tvar, _) ->
+    | (Tvar _, _) ->
         occur !env t1 t2; 
         occur_univar !env t2;
         link_type t1 t2;
         update_level !env t1.level t2
-    | (_, Tvar) ->
+    | (_, Tvar _) ->
         occur !env t2 t1; 
         occur_univar !env t1;
         link_type t2 t1;
         update_level !env t2.level t1
-    | (Tunivar, Tunivar) ->
+    | (Tunivar _, Tunivar _) ->
         unify_univar t1 t2 !univar_pairs;
         update_level !env t1.level t2;
         link_type t1 t2
@@ -2104,7 +2102,7 @@ and unify3 env t1 t1' t2 t2' =
   (* Assumes either [t1 == t1'] or [t2 != t2'] *)
   let d1 = t1'.desc and d2 = t2'.desc in
   match (d1, d2) with (* handle univars specially *)
-    (Tunivar, Tunivar) ->
+    (Tunivar _, Tunivar _) ->
       unify_univar t1' t2' !univar_pairs;
       update_level !env t1'.level t2';
       link_type t1' t2'
@@ -2127,12 +2125,12 @@ and unify3 env t1 t1' t2 t2' =
     | Old -> f () (* old_link was already called *)
   in
   match d1, d2 with
-  | Tvar,_ ->
+  | Tvar _, _ ->
       occur !env t1 t2';
       occur_univar !env t2;
       update_level !env t1'.level t2;
       link_type t1' t2;      
-  | _, Tvar ->
+  | _, Tvar _ ->
       occur !env t2 t1';
       occur_univar !env t1;
       update_level !env t2'.level t1;
@@ -2149,8 +2147,8 @@ and unify3 env t1 t1' t2 t2' =
           add_type_equality t1' t2' end;
       try
         begin match (d1, d2) with
-        | (Tvar, _) 
-        | (_, Tvar) ->
+        | (Tvar _, _) 
+        | (_, Tvar _) ->
             (* cases taken care of *)
             assert false
         | (Tarrow (l1, t1, u1, c1), Tarrow (l2, t2, u2, c2)) when l1 = l2
@@ -2214,8 +2212,9 @@ and unify3 env t1 t1' t2 t2' =
             (* Type [t2'] may have been instantiated by [unify_fields] *)
             (* XXX One should do some kind of unification... *)
             begin match (repr t2').desc with
-              Tobject (_, {contents = Some (_, va::_)})
-              when let va = repr va in List.mem va.desc [Tvar; Tunivar; Tnil] ->
+              Tobject (_, {contents = Some (_, va::_)}) when
+	      (match (repr va).desc with
+		Tvar _|Tunivar _|Tnil -> true | _ -> false) ->
                 ()
             | Tobject (_, nm2) ->
                 set_name nm2 !nm1
@@ -2290,16 +2289,32 @@ and unify_list env tl1 tl2 =
     raise (Unify []);
   List.iter2 (unify env) tl1 tl2
 
+(* Build a fresh row variable for unification *)
+and make_rowvar level use1 rest1 use2 rest2  =
+  let set_name ty name =
+    match ty.desc with
+      Tvar None -> log_type ty; ty.desc <- Tvar name
+    | _ -> ()
+  in
+  let name =
+    match rest1.desc, rest2.desc with
+      Tvar (Some _ as name1), Tvar (Some _ as name2) ->
+        if rest1.level <= rest2.level then name1 else name2
+    | Tvar (Some _ as name), _ ->
+        if use2 then set_name rest2 name; name
+    | _, Tvar (Some _ as name) ->
+        if use1 then set_name rest2 name; name
+    | _ -> None
+  in
+  if use1 then rest1 else
+  if use2 then rest2 else newvar2 ?name level
+
 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 l1 = (repr ty1).level and l2 = (repr ty2).level in
-  let va =
-    if miss1 = [] then rest2
-    else if miss2 = [] then rest1
-    else newty2 (min l1 l2) Tvar
-  in
+  let va = make_rowvar (min l1 l2) (miss2=[]) rest1 (miss1=[]) rest2 in
   let d1 = rest1.desc and d2 = rest2.desc in
   try
     unify env (build_fields l1 miss1 va) rest2;
@@ -2390,7 +2405,7 @@ and unify_row env row1 row2 =
     let rm = row_more row in
     if row.row_fixed then
       if row0.row_more == rm then () else
-      if rm.desc = Tvar then link_type rm row0.row_more else
+      if is_Tvar rm then link_type rm row0.row_more else
       unify env rm row0.row_more
     else
       let ty = newty2 generic_level (Tvariant {row0 with row_fields = rest}) in
@@ -2489,7 +2504,7 @@ 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 ->
+    Tvar _ ->
       begin try
         occur env t1 t2;
         update_level env t1.level t2;
@@ -2527,7 +2542,7 @@ let unify env ty1 ty2 =
 let rec filter_arrow env t l =
   let t = expand_head_unif env t in
   match t.desc with
-    Tvar ->
+    Tvar _ ->
       let lv = t.level in
       let t1 = newvar2 lv and t2 = newvar2 lv in
       let t' = newty2 lv (Tarrow (l, t1, t2, Cok)) in
@@ -2543,7 +2558,7 @@ let rec filter_arrow env t l =
 let rec filter_method_field env name priv ty =
   let ty = repr ty in
   match ty.desc with
-    Tvar ->
+    Tvar _ ->
       let level = ty.level in
       let ty1 = newvar2 level and ty2 = newvar2 level in
       let ty' = newty2 level (Tfield (name,
@@ -2570,7 +2585,7 @@ let rec filter_method_field env name priv ty =
 let rec filter_method env name priv ty =
   let ty = expand_head_unif env ty in
   match ty.desc with
-    Tvar ->
+    Tvar _ ->
       let ty1 = newvar () in
       let ty' = newobj ty1 in
       update_level env ty.level ty';
@@ -2606,7 +2621,7 @@ let moregen_occur env level ty =
   let rec occur ty =
     let ty = repr ty in
     if ty.level > level then begin
-      if ty.desc = Tvar && ty.level >= generic_level - 1 then raise Occur;
+      if is_Tvar ty && ty.level >= generic_level - 1 then raise Occur;
       ty.level <- pivot_level - ty.level;
       match ty.desc with
         Tvariant row when static_row row ->
@@ -2636,7 +2651,7 @@ let rec moregen inst_nongen type_pairs env t1 t2 =
 
   try
     match (t1.desc, t2.desc) with
-      (Tvar, _) when may_instantiate inst_nongen t1 ->
+      (Tvar _, _) when may_instantiate inst_nongen t1 ->
         moregen_occur env t1.level t2;
         occur env t1 t2;
         link_type t1 t2
@@ -2653,7 +2668,7 @@ let rec moregen inst_nongen type_pairs env t1 t2 =
         with Not_found ->
           TypePairs.add type_pairs (t1', t2') ();
           match (t1'.desc, t2'.desc) with
-            (Tvar, _) when may_instantiate inst_nongen t1' ->
+            (Tvar _, _) when may_instantiate inst_nongen t1' ->
               moregen_occur env t1'.level t2;
               link_type t1' t2
           | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2
@@ -2684,7 +2699,7 @@ let rec moregen inst_nongen type_pairs env t1 t2 =
           | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
               enter_poly env univar_pairs t1 tl1 t2 tl2
                 (moregen inst_nongen type_pairs env)
-          | (Tunivar, Tunivar) ->
+          | (Tunivar _, Tunivar _) ->
               unify_univar t1' t2' !univar_pairs
           | (_, _) ->
               raise (Unify [])
@@ -2725,7 +2740,7 @@ and moregen_row inst_nongen type_pairs env row1 row2 =
   let row1 = row_repr row1 and row2 = row_repr row2 in
   let rm1 = repr row1.row_more and rm2 = repr row2.row_more in
   if rm1 == rm2 then () else
-  let may_inst = rm1.desc = Tvar && may_instantiate inst_nongen rm1 in
+  let may_inst = is_Tvar rm1 && may_instantiate inst_nongen rm1 in
   let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
   let r1, r2 =
     if row2.row_closed then
@@ -2735,9 +2750,9 @@ and moregen_row inst_nongen type_pairs env row1 row2 =
   if r1 <> [] || row1.row_closed && (not row2.row_closed || r2 <> [])
   then raise (Unify []);
   begin match rm1.desc, rm2.desc with
-    Tunivar, Tunivar ->
+    Tunivar _, Tunivar _ ->
       unify_univar rm1 rm2 !univar_pairs
-  | Tunivar, _ | _, Tunivar ->
+  | Tunivar _, _ | _, Tunivar _ ->
       raise (Unify [])
   | _ when static_row row1 -> ()
   | _ when may_inst ->
@@ -2828,13 +2843,13 @@ let rec rigidify_rec vars ty =
   if ty.level >= lowest_level then begin
     ty.level <- pivot_level - ty.level;
     match ty.desc with
-    | Tvar ->
+    | Tvar _ ->
         if not (List.memq ty !vars) then vars := ty :: !vars
     | Tvariant row ->
         let row = row_repr row in
         let more = repr row.row_more in
-        if more.desc = Tvar && not row.row_fixed then begin
-          let more' = newty2 more.level Tvar in
+        if is_Tvar more && not row.row_fixed then begin
+          let more' = newty2 more.level more.desc in
           let row' = {row with row_fixed=true; row_fields=[]; row_more=more'}
           in link_type more (newty2 ty.level (Tvariant row'))
         end;
@@ -2857,7 +2872,7 @@ let all_distinct_vars env vars =
     (fun ty ->
       let ty = expand_head env ty in
       if List.memq ty !tyl then false else
-      (tyl := ty :: !tyl; ty.desc = Tvar))
+      (tyl := ty :: !tyl; is_Tvar ty))
     vars
 
 let matches env ty ty' =
@@ -2901,7 +2916,7 @@ let rec eqtype rename type_pairs subst env t1 t2 =
 
   try
     match (t1.desc, t2.desc) with
-      (Tvar, Tvar) when rename ->
+      (Tvar _, Tvar _) when rename ->
         begin try
           normalize_subst subst;
           if List.assq t1 !subst != t2 then raise (Unify [])
@@ -2922,7 +2937,7 @@ let rec eqtype rename type_pairs subst env t1 t2 =
         with Not_found ->
           TypePairs.add type_pairs (t1', t2') ();
           match (t1'.desc, t2'.desc) with
-            (Tvar, Tvar) when rename ->
+            (Tvar _, Tvar _) when rename ->
               begin try
                 normalize_subst subst;
                 if List.assq t1' !subst != t2' then raise (Unify [])
@@ -2956,7 +2971,7 @@ let rec eqtype rename type_pairs subst env t1 t2 =
           | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
               enter_poly env univar_pairs t1 tl1 t2 tl2
                 (eqtype rename type_pairs subst env)
-          | (Tunivar, Tunivar) ->
+          | (Tunivar _, Tunivar _) ->
               unify_univar t1' t2' !univar_pairs
           | (_, _) ->
               raise (Unify [])
@@ -3405,7 +3420,7 @@ let has_constr_row' env t =
 let rec build_subtype env visited loops posi level t =
   let t = repr t in
   match t.desc with
-    Tvar ->
+    Tvar _ ->
       if posi then
         try
           let t' = List.assq t loops in
@@ -3454,13 +3469,13 @@ let rec build_subtype env visited loops posi level t =
              as this occurence might break the occur check.
              XXX not clear whether this correct anyway... *)
           if List.exists (deep_occur ty) tl1 then raise Not_found;
-          ty.desc <- Tvar;
+          ty.desc <- Tvar None;
           let t'' = newvar () in
           let loops = (ty, t'') :: loops in
           (* May discard [visited] as level is going down *)
           let (ty1', c) =
             build_subtype env [t'] loops posi (pred_enlarge level') ty1 in
-          assert (t''.desc = Tvar);
+          assert (is_Tvar t'');
           let nm =
             if c > Equiv || deep_occur ty ty1' then None else Some(p,tl1) in
           t''.desc <- Tobject (ty1', ref nm);
@@ -3559,7 +3574,7 @@ let rec build_subtype env visited loops posi level t =
       let (t1', c) = build_subtype env visited loops posi level t1 in
       if c > Unchanged then (newty (Tpoly(t1', tl)), c)
       else (t, Unchanged)
-  | Tunivar | Tpackage _ ->
+  | Tunivar _ | Tpackage _ ->
       (t, Unchanged)
 
 let enlarge_type env ty =
@@ -3623,7 +3638,7 @@ let rec subtype_rec env trace t1 t2 cstrs =
   with Not_found ->
     TypePairs.add subtypes (t1, t2) ();
     match (t1.desc, t2.desc) with
-      (Tvar, _) | (_, Tvar) ->
+      (Tvar _, _) | (_, Tvar _) ->
         (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) ->
@@ -3659,7 +3674,7 @@ let rec subtype_rec env trace t1 t2 cstrs =
     | (Tconstr(p1, tl1, _), _) when private_abbrev env p1 ->
         subtype_rec env trace (expand_abbrev_opt env t1) t2 cstrs
     | (Tobject (f1, _), Tobject (f2, _))
-      when (object_row f1).desc = Tvar && (object_row f2).desc = Tvar ->
+      when is_Tvar (object_row f1) && is_Tvar (object_row f2) ->
         (* Same row variable implies same object. *)
         (trace, t1, t2, !univar_pairs)::cstrs
     | (Tobject (f1, _), Tobject (f2, _)) ->
@@ -3731,7 +3746,7 @@ and subtype_row env trace row1 row2 cstrs =
   match more1.desc, more2.desc with
     Tconstr(p1,_,_), Tconstr(p2,_,_) when Path.same p1 p2 ->
       subtype_rec env ((more1,more2)::trace) more1 more2 cstrs
-  | (Tvar|Tconstr _), (Tvar|Tconstr _)
+  | (Tvar _|Tconstr _), (Tvar _|Tconstr _)
     when row1.row_closed && r1 = [] ->
       List.fold_left
         (fun cstrs (_,f1,f2) ->
@@ -3745,7 +3760,7 @@ and subtype_row env trace row1 row2 cstrs =
           | Rabsent, _ -> cstrs
           | _ -> raise Exit)
         cstrs pairs
-  | Tunivar, Tunivar
+  | Tunivar _, Tunivar _
     when row1.row_closed = row2.row_closed && r1 = [] && r2 = [] ->
       let cstrs =
         subtype_rec env ((more1,more2)::trace) more1 more2 cstrs in
@@ -3789,19 +3804,19 @@ let rec unalias_object ty =
   match ty.desc with
     Tfield (s, k, t1, t2) ->
       newty2 ty.level (Tfield (s, k, t1, unalias_object t2))
-  | Tvar | Tnil ->
+  | Tvar _ | Tnil ->
       newty2 ty.level ty.desc
-  | Tunivar ->
+  | Tunivar _ ->
       ty
   | Tconstr _ ->
-      newty2 ty.level Tvar
+      newvar2 ty.level
   | _ ->
       assert false
 
 let unalias ty =
   let ty = repr ty in
   match ty.desc with
-    Tvar | Tunivar ->
+    Tvar _ | Tunivar _ ->
       ty
   | Tvariant row ->
       let row = row_repr row in
@@ -3875,7 +3890,7 @@ let rec normalize_type_rec env visited ty =
               set_name nm None
             else let v' = repr v in
             begin match v'.desc with
-            | Tvar|Tunivar ->
+            | Tvar _ | Tunivar _ ->
                 if v' != v then set_name nm (Some (n, v' :: l))
             | Tnil ->
                 log_type ty; ty.desc <- Tconstr (n, l, ref Mnil)
@@ -3917,7 +3932,7 @@ let clear_hash ()   =
 
 let rec nondep_type_rec env id ty =
   match ty.desc with
-    Tvar | Tunivar -> ty
+    Tvar _ | Tunivar _ -> ty
   | Tlink ty -> nondep_type_rec env id ty
   | _ -> try TypeHash.find nondep_hash ty
   with Not_found ->
@@ -3987,7 +4002,7 @@ let nondep_type env id ty =
 
 let unroll_abbrev id tl ty =
   let ty = repr ty and path = Path.Pident id in
-  if (ty.desc = Tvar) || (List.exists (deep_occur ty) tl)
+  if is_Tvar ty || (List.exists (deep_occur ty) tl)
   || is_object_type path then
     ty
   else
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 08ab6272f7..a08409c650 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -41,9 +41,10 @@ val restore_global_level: int -> unit
         (* This pair of functions is only used in Typetexp *)
 
 val newty: type_desc -> type_expr
-val newvar: unit -> type_expr
+val newvar: ?name:string -> unit -> type_expr
+val newvar2: ?name:string -> int -> type_expr
         (* Return a fresh variable *)
-val new_global_var: unit -> type_expr
+val new_global_var: ?name:string -> unit -> type_expr
         (* Return a fresh variable, bound at toplevel
            (as type variables ['a] in type constraints). *)
 val newobj: type_expr -> type_expr
diff --git a/typing/datarepr.ml b/typing/datarepr.ml
index b80d22ef8d..8b8a1722fc 100644
--- a/typing/datarepr.ml
+++ b/typing/datarepr.ml
@@ -28,7 +28,7 @@ let rec free_vars ty =
     if ty.level >= lowest_level then begin
       ty.level <- pivot_level - ty.level;
       match ty.desc with
-      | Tvar ->
+      | Tvar _ ->
           ret := TypeSet.add ty !ret
       | Tvariant row ->
           let row = row_repr row in
diff --git a/typing/includecore.ml b/typing/includecore.ml
index 9f0f3618a6..50f5473935 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -61,7 +61,7 @@ let type_manifest env ty1 params1 ty2 params2 priv2 =
     Tvariant row1, Tvariant row2 when is_absrow env (Btype.row_more row2) ->
       let row1 = Btype.row_repr row1 and row2 = Btype.row_repr row2 in
       Ctype.equal env true (ty1::params1) (row2.row_more::params2) &&
-      (match row1.row_more with {desc=Tvar|Tconstr _} -> true | _ -> false) &&
+      (match row1.row_more with {desc=Tvar _|Tconstr _} -> true | _ -> false) &&
       let r1, r2, pairs =
         Ctype.merge_row_fields row1.row_fields row2.row_fields in
       (not row2.row_closed ||
@@ -91,7 +91,7 @@ let type_manifest env ty1 params1 ty2 params2 priv2 =
       let (fields2,rest2) = Ctype.flatten_fields fi2 in
       Ctype.equal env true (ty1::params1) (rest2::params2) &&
       let (fields1,rest1) = Ctype.flatten_fields fi1 in
-      (match rest1 with {desc=Tnil|Tvar|Tconstr _} -> true | _ -> false) &&
+      (match rest1 with {desc=Tnil|Tvar _|Tconstr _} -> true | _ -> false) &&
       let pairs, miss1, miss2 = Ctype.associate_fields fields1 fields2 in
       miss2 = [] &&
       let tl1, tl2 =
@@ -251,7 +251,7 @@ let exception_declarations env ed1 ed2 =
 let encode_val (mut, ty) rem =
   begin match mut with
     Asttypes.Mutable   -> Predef.type_unit
-  | Asttypes.Immutable -> Btype.newgenty Tvar
+  | Asttypes.Immutable -> Btype.newgenvar ()
   end
   ::ty::rem
 
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 6632835ee9..1d44093f8a 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -109,6 +109,10 @@ let rec list_of_memo = function
   | Mcons (priv, p, t1, t2, rem) -> p :: list_of_memo rem
   | Mlink rem -> list_of_memo !rem
 
+let print_name ppf = function
+    None -> fprintf ppf "None"
+  | Some name -> fprintf ppf "\"%s\"" name
+
 let visited = ref []
 let rec raw_type ppf ty =
   let ty = safe_repr [] ty in
@@ -119,7 +123,7 @@ let rec raw_type ppf ty =
   end
 and raw_type_list tl = raw_list raw_type tl
 and raw_type_desc ppf = function
-    Tvar -> fprintf ppf "Tvar"
+    Tvar name -> fprintf ppf "Tvar %a" print_name name
   | Tarrow(l,t1,t2,c) ->
       fprintf ppf "@[<hov1>Tarrow(%s,@,%a,@,%a,@,%s)@]"
         l raw_type t1 raw_type t2
@@ -143,7 +147,7 @@ and raw_type_desc ppf = function
   | Tnil -> fprintf ppf "Tnil"
   | Tlink t -> fprintf ppf "@[<1>Tlink@,%a@]" raw_type t
   | Tsubst t -> fprintf ppf "@[<1>Tsubst@,%a@]" raw_type t
-  | Tunivar -> fprintf ppf "Tunivar"
+  | Tunivar name -> fprintf ppf "Tunivar %a" print_name name
   | Tpoly (t, tl) ->
       fprintf ppf "@[<hov1>Tpoly(@,%a,@,%a)@]"
         raw_type t
@@ -189,28 +193,61 @@ let () = Btype.print_raw := raw_type_expr
 
 let names = ref ([] : (type_expr * string) list)
 let name_counter = ref 0
+let named_vars = ref ([] : string list)
+
+let reset_names () = names := []; name_counter := 0; named_vars := []
+let add_named_var ty =
+  match ty.desc with
+    Tvar (Some name) | Tunivar (Some name) ->
+      if List.mem name !named_vars then () else
+      named_vars := name :: !named_vars
+  | _ -> ()
 
-let reset_names () = names := []; name_counter := 0
-
-let new_name () =
+let rec new_name () =
   let name =
     if !name_counter < 26
     then String.make 1 (Char.chr(97 + !name_counter))
     else String.make 1 (Char.chr(97 + !name_counter mod 26)) ^
            string_of_int(!name_counter / 26) in
   incr name_counter;
-  name
+  if List.mem name !named_vars
+  || List.exists (fun (_, name') -> name = name') !names
+  then new_name ()
+  else name
 
 let name_of_type t =
+  (* We've already been through repr at this stage, so t is our representative
+     of the union-find class. *)
   try List.assq t !names with Not_found ->
-    let name = new_name () in
+    let name =
+      match t.desc with
+        Tvar (Some name) | Tunivar (Some name) ->
+          (* Some part of the type we've already printed has assigned another
+           * unification variable to that name. We want to keep the name, so try
+           * adding a number until we find a name that's not taken. *)
+          let current_name = ref name in
+          let i = ref 0 in
+          while List.exists (fun (_, name') -> !current_name = name') !names do
+            current_name := name ^ (string_of_int !i);
+            i := !i + 1;
+          done;
+          !current_name
+      | _ ->
+          (* No name available, create a new one *)
+          new_name ()
+    in
     names := (t, name) :: !names;
     name
 
 let check_name_of_type t = ignore(name_of_type t)
 
+let remove_names tyl =
+  let tyl = List.map repr tyl in
+  names := List.filter (fun (ty,_) -> not (List.memq ty tyl)) !names
+
+
 let non_gen_mark sch ty =
-  if sch && ty.desc = Tvar && ty.level <> generic_level then "_" else ""
+  if sch && is_Tvar ty && ty.level <> generic_level then "_" else ""
 
 let print_name_of_type sch ppf t =
   fprintf ppf "'%s%s" (non_gen_mark sch t) (name_of_type t)
@@ -225,9 +262,13 @@ let add_delayed t =
 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
+  if not (is_aliased px) then begin
+    aliased := px :: !aliased;
+    add_named_var px
+  end
+
 let aliasable ty =
-  match ty.desc with Tvar | Tunivar | Tpoly _ -> false | _ -> true
+  match ty.desc with Tvar _ | Tunivar _ | Tpoly _ -> false | _ -> true
 
 let namable_row row =
   row.row_name <> None &&
@@ -245,7 +286,7 @@ let rec mark_loops_rec visited ty =
   if List.memq px visited && aliasable ty then add_alias px else
     let visited = px :: visited in
     match ty.desc with
-    | Tvar -> ()
+    | Tvar _ -> add_named_var ty
     | Tarrow(_, ty1, ty2, _) ->
         mark_loops_rec visited ty1; mark_loops_rec visited ty2
     | Ttuple tyl -> List.iter (mark_loops_rec visited) tyl
@@ -290,7 +331,7 @@ let rec mark_loops_rec visited ty =
     | Tpoly (ty, tyl) ->
         List.iter (fun t -> add_alias t) tyl;
         mark_loops_rec visited ty
-    | Tunivar -> ()
+    | Tunivar _ -> add_named_var ty
 
 let mark_loops ty =
   normalize_type Env.empty ty;
@@ -322,7 +363,7 @@ let rec tree_of_typexp sch ty =
 
   let pr_typ () =
     match ty.desc with
-    | Tvar ->
+    | Tvar _ ->
         Otyp_var (is_non_gen sch ty, name_of_type ty)
     | Tarrow(l, ty1, ty2, _) ->
         let pr_arrow l ty1 ty2 =
@@ -387,16 +428,22 @@ let rec tree_of_typexp sch ty =
     | Tpoly (ty, []) ->
         tree_of_typexp sch ty
     | Tpoly (ty, tyl) ->
+        (*let print_names () =
+          List.iter (fun (_, name) -> prerr_string (name ^ " ")) !names;
+          prerr_string "; " in *)
         let tyl = List.map repr tyl in
-        (* let tyl = List.filter is_aliased tyl in *)
         if tyl = [] then tree_of_typexp sch ty else begin
           let old_delayed = !delayed in
+          (* Make the names delayed, so that the real type is
+             printed once when used as proxy *)
           List.iter add_delayed tyl;
           let tl = List.map name_of_type tyl in
           let tr = Otyp_poly (tl, tree_of_typexp sch ty) in
+          (* Forget names when we leave scope *)
+          remove_names tyl;
           delayed := old_delayed; tr
         end
-    | Tunivar ->
+    | Tunivar _ ->
         Otyp_var (false, name_of_type ty)
     | Tpackage (p, n, tyl) ->
         Otyp_module (Path.name p, n, tree_of_typlist sch tyl)
@@ -446,13 +493,13 @@ and tree_of_typobject sch fi nm =
   end
 
 and is_non_gen sch ty =
-    sch && ty.desc = Tvar && ty.level <> generic_level
+    sch && is_Tvar ty && ty.level <> generic_level
 
 and tree_of_typfields sch rest = function
   | [] ->
       let rest =
         match rest.desc with
-        | Tvar | Tunivar -> Some (is_non_gen sch rest)
+        | Tvar _ | Tunivar _ -> Some (is_non_gen sch rest)
         | Tconstr _ -> Some false
         | Tnil -> None
         | _ -> fatal_error "typfields (1)"
@@ -564,7 +611,7 @@ let rec tree_of_type_decl id decl =
     let vari =
       List.map2
         (fun ty (co,cn,ct) ->
-          if abstr || (repr ty).desc <> Tvar then (co,cn) else (true,true))
+          if abstr || not (is_Tvar (repr ty)) then (co,cn) else (true,true))
         decl.type_params decl.type_variance
     in
     (Ident.name id,
@@ -645,16 +692,18 @@ let class_var sch ppf l (m, t) =
 
 let method_type (_, kind, ty) =
   match field_kind_repr kind, repr ty with
-    Fpresent, {desc=Tpoly(ty, _)} -> ty
-  | _       , ty                  -> ty
+    Fpresent, {desc=Tpoly(ty, tyl)} -> (ty, tyl)
+  | _       , ty                    -> (ty, [])
 
 let tree_of_metho sch concrete csil (lab, kind, ty) =
   if lab <> dummy_method then begin
     let kind = field_kind_repr kind in
     let priv = kind <> Fpresent in
     let virt = not (Concr.mem lab concrete) in
-    let ty = method_type (lab, kind, ty) in
-    Ocsg_method (lab, priv, virt, tree_of_typexp sch ty) :: csil
+    let (ty, tyl) = method_type (lab, kind, ty) in
+    let tty = tree_of_typexp sch ty in
+    remove_names tyl;
+    Ocsg_method (lab, priv, virt, tty) :: csil
   end
   else csil
 
@@ -662,7 +711,7 @@ let rec prepare_class_type params = function
   | Tcty_constr (p, tyl, cty) ->
       let sty = Ctype.self_type cty in
       if List.memq (proxy sty) !visited_objects
-      || List.exists (fun ty -> (repr ty).desc <> Tvar) params
+      || not (List.for_all is_Tvar params)
       || List.exists (deep_occur sty) tyl
       then prepare_class_type params cty
       else List.iter mark_loops tyl
@@ -675,7 +724,7 @@ let rec prepare_class_type params = function
       let (fields, _) =
         Ctype.flatten_fields (Ctype.object_fields sign.cty_self)
       in
-      List.iter (fun met -> mark_loops (method_type met)) fields;
+      List.iter (fun met -> mark_loops (fst (method_type met))) fields;
       Vars.iter (fun _ (_, _, ty) -> mark_loops ty) sign.cty_vars
   | Tcty_fun (_, ty, cty) ->
       mark_loops ty;
@@ -686,7 +735,7 @@ let rec tree_of_class_type sch params =
   | Tcty_constr (p', tyl, cty) ->
       let sty = Ctype.self_type cty in
       if List.memq (proxy sty) !visited_objects
-      || List.exists (fun ty -> (repr ty).desc <> Tvar) params
+      || not (List.for_all is_Tvar params)
       then
         tree_of_class_type sch params cty
       else
@@ -743,7 +792,7 @@ let tree_of_class_param param variance =
   (match tree_of_typexp true param with
     Otyp_var (_, s) -> s
   | _ -> "?"),
-  if (repr param).desc = Tvar then (true, true) else variance
+  if is_Tvar (repr param) then (true, true) else variance
 
 let tree_of_class_params params =
   let tyl = tree_of_typlist true params in
@@ -890,7 +939,7 @@ let hide_variant_name t =
   | {desc = Tvariant row} as t when (row_repr row).row_name <> None ->
       newty2 t.level
         (Tvariant {(row_repr row) with row_name = None;
-                   row_more = newty2 (row_more row).level Tvar})
+                   row_more = newvar2 (row_more row).level})
   | _ -> t
 
 let prepare_expansion (t, t') =
@@ -913,9 +962,9 @@ let print_tags ppf fields =
 let has_explanation unif t3 t4 =
   match t3.desc, t4.desc with
     Tfield _, _ | _, Tfield _
-  | Tunivar, Tvar | Tvar, Tunivar
+  | Tunivar _, Tvar _ | Tvar _, Tunivar _
   | Tvariant _, Tvariant _ -> true
-  | Tconstr (p, _, _), Tvar | Tvar, Tconstr (p, _, _) ->
+  | Tconstr (p, _, _), Tvar _ | Tvar _, Tconstr (p, _, _) ->
       unif && min t3.level t4.level < Path.binding_time p
   | _ -> false
 
@@ -931,21 +980,21 @@ let rec mismatch unif = function
 
 let explanation unif t3 t4 ppf =
   match t3.desc, t4.desc with
-  | Tfield _, Tvar | Tvar, Tfield _ ->
+  | Tfield _, Tvar _ | Tvar _, Tfield _ ->
       fprintf ppf "@,Self type cannot escape its class"
-  | Tconstr (p, tl, _), Tvar
+  | Tconstr (p, tl, _), Tvar _
     when unif && (tl = [] || t4.level < Path.binding_time p) ->
       fprintf ppf
         "@,@[The type constructor@;<1 2>%a@ would escape its scope@]"
         path p
-  | Tvar, Tconstr (p, tl, _)
+  | Tvar _, Tconstr (p, tl, _)
     when unif && (tl = [] || t3.level < Path.binding_time p) ->
       fprintf ppf
         "@,@[The type constructor@;<1 2>%a@ would escape its scope@]"
         path p
-  | Tvar, Tunivar | Tunivar, Tvar ->
+  | Tvar _, Tunivar _ | Tunivar _, Tvar _ ->
       fprintf ppf "@,The universal variable %a would escape its scope"
-        type_expr (if t3.desc = Tunivar then t3 else t4)
+        type_expr (if is_Tunivar t3 then t3 else t4)
   | Tfield (lab, _, _, _), _
   | _, Tfield (lab, _, _, _) when lab = dummy_method ->
       fprintf ppf
diff --git a/typing/subst.ml b/typing/subst.ml
index e086a863e6..39e04e5645 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -71,16 +71,19 @@ let new_id = ref (-1)
 let reset_for_saving () = new_id := -1
 
 let newpersty desc =
-  decr new_id; { desc = desc; level = generic_level; id = !new_id }
+  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 | Tunivar ->
+    Tvar _ | Tunivar _ ->
       if s.for_saving || ty.id < 0 then
+        let desc = match ty.desc with (* Tvar _ -> Tvar None *) | d -> d in
         let ty' =
-          if s.for_saving then newpersty ty.desc else newty2 ty.level ty.desc
+          if s.for_saving then newpersty desc
+          else newty2 ty.level desc
         in
         save_desc ty ty.desc; ty.desc <- Tsubst ty'; ty'
       else ty
@@ -94,7 +97,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 newpersty Tvar else newgenvar () in
+    let ty' = if s.for_saving then newpersty (Tvar None) else newgenvar () in
     ty.desc <- Tsubst ty';
     ty'.desc <-
       begin match desc with
@@ -127,10 +130,10 @@ let rec typexp s ty =
                 match more.desc with
                   Tsubst ty -> ty
                 | Tconstr _ -> typexp s more
-                | Tunivar | Tvar ->
+                | Tunivar _ | Tvar _ ->
                     save_desc more more.desc;
                     if s.for_saving then newpersty more.desc else
-                    if dup && more.desc <> Tunivar then newgenvar () else more
+                    if dup && is_Tvar more then newgenty more.desc else more
                 | _ -> assert false
               in
               (* Register new type first for recursion *)
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 111dc4814f..518ab0f236 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -532,7 +532,7 @@ let rec class_field cl_num self_type meths vars
                 (Typetexp.transl_simple_type val_env false sty) ty
           end;
           begin match (Ctype.repr ty).desc with
-            Tvar ->
+            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'
diff --git a/typing/typecore.ml b/typing/typecore.ml
index b148ecfe38..2d9df27348 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -633,7 +633,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
           List.iter generalize vars;
           let instantiated tv  = 
             let tv = expand_head !env tv in
-            tv.desc <> Tvar || tv.level <> generic_level in
+            not (is_Tvar tv) || tv.level <> generic_level in
           if List.exists instantiated vars then
             raise (Error(loc, Polymorphic_label (lid_of_label label)))
         end;
@@ -1126,7 +1126,7 @@ let rec list_labels_aux env visited ls ty_fun =
     Tarrow (l, _, ty_res, _) ->
       list_labels_aux env (ty::visited) (l::ls) ty_res
   | _ ->
-      List.rev ls, ty.desc = Tvar
+      List.rev ls, is_Tvar ty
 
 let list_labels env ty = list_labels_aux env [] [] ty
 
@@ -1142,9 +1142,10 @@ let check_univars env expans kind exp ty_expected vars =
       (fun t ->
         let t = repr t in
         generalize t;
-        if t.desc = Tvar && t.level = generic_level then
-          (log_type t; t.desc <- Tunivar; true)
-        else false)
+        match t.desc with
+          Tvar name when t.level = generic_level ->
+            log_type t; t.desc <- Tunivar name; true
+        | _ -> false)
       vars in
   if List.length vars = List.length vars' then () else
   let ty = newgenty (Tpoly(repr exp.exp_type, vars'))
@@ -1158,7 +1159,7 @@ let check_application_result env statement exp =
   match (expand_head env exp.exp_type).desc with
   | Tarrow _ ->
       Location.prerr_warning exp.exp_loc Warnings.Partial_application
-  | Tvar -> ()
+  | Tvar _ -> ()
   | Tconstr (p, _, _) when Path.same p Predef.path_unit -> ()
   | _ ->
       if statement then
@@ -1742,7 +1743,7 @@ and type_expect ?in_function env sexp ty_expected =
               let (id, typ) =
                 filter_self_method env met Private meths privty
               in
-              if (repr typ).desc = Tvar then
+              if is_Tvar (repr typ) then
                 Location.prerr_warning loc
                   (Warnings.Undeclared_virtual_method met);
               (Texp_send(obj, Tmeth_val id), typ)
@@ -1797,7 +1798,7 @@ and type_expect ?in_function env sexp ty_expected =
                 Location.prerr_warning loc
                   (Warnings.Not_principal "this use of a polymorphic method");
               snd (instance_poly false tl ty)
-          | {desc = Tvar} as ty ->
+          | {desc = Tvar _} as ty ->
               let ty' = newvar () in
               unify env (instance ty) (newty(Tpoly(ty',[])));
               (* if not !Clflags.nolabels then
@@ -1979,7 +1980,7 @@ and type_expect ?in_function env sexp ty_expected =
             end_def ();
             check_univars env false "method" exp ty_expected vars;
             re { exp with exp_type = instance ty }
-        | Tvar ->
+        | Tvar _ ->
             let exp = type_exp env sbody in
             let exp = {exp with exp_type = newty (Tpoly (exp.exp_type, []))} in
             unify_exp env exp ty;
@@ -2038,7 +2039,7 @@ and type_expect ?in_function env sexp ty_expected =
               Location.prerr_warning loc
                 (Warnings.Not_principal "this module packing");
             (p, nl, tl)
-        | {desc = Tvar} ->
+        | {desc = Tvar _} ->
             raise (Error (loc, Cannot_infer_signature))
         | _ ->
             raise (Error (loc, Not_a_packed_module ty_expected))
@@ -2128,7 +2129,7 @@ and type_argument env sarg ty_expected' ty_expected =
               ty_fun
         | Tarrow (l,_,ty_res',_) when l = "" || !Clflags.classic ->
             args, ty_fun, no_labels ty_res'
-        | Tvar ->  args, ty_fun, false
+        | Tvar _ ->  args, ty_fun, false
         |  _ -> [], texp.exp_type, false
       in
       let args, ty_fun', simple_res = make_args [] texp.exp_type in
@@ -2192,7 +2193,7 @@ and type_application env funct sargs =
         let (ty1, ty2) =
           let ty_fun = expand_head env ty_fun in
           match ty_fun.desc with
-            Tvar ->
+            Tvar _ ->
               let t1 = newvar () and t2 = newvar () in
               let not_identity = function
                   Texp_ident(_,{val_kind=Val_prim
@@ -2335,7 +2336,7 @@ and type_application env funct sargs =
       begin match (expand_head env exp.exp_type).desc with
       | Tarrow _ ->
           Location.prerr_warning exp.exp_loc Warnings.Partial_application
-      | Tvar ->
+      | Tvar _ ->
           add_delayed_check (fun () -> check_application_result env false exp)
       | _ -> ()
       end;
@@ -2404,9 +2405,9 @@ and type_statement env sexp =
   | Tarrow _ ->
       Location.prerr_warning loc Warnings.Partial_application
   | Tconstr (p, _, _) when Path.same p Predef.path_unit -> ()
-  | Tvar when ty.level > tv.level ->
+  | Tvar _ when ty.level > tv.level ->
       Location.prerr_warning loc Warnings.Nonreturning_statement
-  | Tvar ->
+  | Tvar _ ->
       add_delayed_check (fun () -> check_application_result env true exp)
   | _ ->
       Location.prerr_warning loc Warnings.Statement_type
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 2a2f451179..d7316ab2d3 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -111,7 +111,7 @@ let set_fixed_row env loc p decl =
     | _ ->
         raise (Error (loc, Bad_fixed_type "is not an object or variant"))
   in
-  if rv.desc <> Tvar then
+  if not (Btype.is_Tvar rv) then
     raise (Error (loc, Bad_fixed_type "has no row variable"));
   rv.desc <- Tconstr (p, decl.type_params, ref Mnil)
 
@@ -503,7 +503,7 @@ let compute_variance env tvl nega posi cntr ty =
           compute_same row.row_more
       | Tpoly (ty, _) ->
           compute_same ty
-      | Tvar | Tnil | Tlink _ | Tunivar -> ()
+      | Tvar _ | Tnil | Tlink _ | Tunivar _ -> ()
       | Tpackage (_, _, tyl) ->
           List.iter (compute_variance_rec true true true) tyl
     end
@@ -546,7 +546,7 @@ let compute_variance_type env check (required, loc) decl tyl =
   in
   List.iter2
     (fun (ty, co, cn, ct) (c, n) ->
-      if ty.desc <> Tvar then begin
+      if not (Btype.is_Tvar ty) then begin
         co := c; cn := n; ct := n;
         compute_variance env tvl2 c n n ty
       end)
@@ -571,7 +571,7 @@ let add_false = List.map (fun ty -> false, ty)
 
 let rec anonymous env ty =
   match (Ctype.expand_head env ty).desc with
-  | Tvar -> false
+  | Tvar _ -> false
   | Tobject (fi, _) ->
       let _, rv = Ctype.flatten_fields fi in anonymous env rv
   | Tvariant row ->
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 78cae50dba..7210eb0fb8 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -764,7 +764,7 @@ let rec type_module sttn funct_body anchor env smod =
               Location.prerr_warning smod.pmod_loc
                 (Warnings.Not_principal "this module unpacking");
             modtype_of_package env smod.pmod_loc p nl tl
-        | {desc = Tvar} ->
+        | {desc = Tvar _} ->
             raise (Typecore.Error
                      (smod.pmod_loc, Typecore.Cannot_infer_signature))
         | _ ->
diff --git a/typing/types.ml b/typing/types.ml
index bca2be0437..494feb1d62 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -25,7 +25,7 @@ type type_expr =
     mutable id: int }
 
 and type_desc =
-    Tvar
+    Tvar of string option
   | Tarrow of label * type_expr * type_expr * commutable
   | Ttuple of type_expr list
   | Tconstr of Path.t * type_expr list * abbrev_memo ref
@@ -35,7 +35,7 @@ and type_desc =
   | Tlink of type_expr
   | Tsubst of type_expr         (* for copying *)
   | Tvariant of row_desc
-  | Tunivar
+  | Tunivar of string option
   | Tpoly of type_expr * type_expr list
   | Tpackage of Path.t * string list * type_expr list
 
diff --git a/typing/types.mli b/typing/types.mli
index cca05c3e8d..9ed72ab7de 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -24,7 +24,7 @@ type type_expr =
     mutable id: int }
 
 and type_desc =
-    Tvar
+    Tvar of string option
   | Tarrow of label * type_expr * type_expr * commutable
   | Ttuple of type_expr list
   | Tconstr of Path.t * type_expr list * abbrev_memo ref
@@ -34,7 +34,7 @@ and type_desc =
   | Tlink of type_expr
   | Tsubst of type_expr         (* for copying *)
   | Tvariant of row_desc
-  | Tunivar
+  | Tunivar of string option
   | Tpoly of type_expr * type_expr list
   | Tpackage of Path.t * string list * type_expr list
 
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index f6eddbf95a..6592f6347b 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -58,7 +58,9 @@ type variable_context = int * (string, type_expr) Tbl.t
 let rec narrow_unbound_lid_error env loc lid make_error =
   let check_module mlid =
     try ignore (Env.lookup_module mlid env)
-    with Not_found -> narrow_unbound_lid_error env loc mlid (fun lid -> Unbound_module lid); assert false
+    with Not_found ->
+      narrow_unbound_lid_error env loc mlid (fun lid -> Unbound_module lid);
+      assert false
   in
   begin match lid with
   | Longident.Lident _ -> ()
@@ -73,28 +75,30 @@ let rec narrow_unbound_lid_error env loc lid make_error =
 let find_component lookup make_error env loc lid =
   try
     match lid with
-    | Longident.Ldot (Longident.Lident "*predef*", s) -> lookup (Longident.Lident s) Env.initial
+    | Longident.Ldot (Longident.Lident "*predef*", s) ->
+        lookup (Longident.Lident s) Env.initial
     | _ -> lookup lid env
   with Not_found ->
     (narrow_unbound_lid_error env loc lid make_error
      : unit (* to avoid a warning *));
     assert false
 
-let find_type = find_component Env.lookup_type (fun lid -> Unbound_type_constructor lid)
-
-let find_constructor = find_component Env.lookup_constructor (fun lid -> Unbound_constructor lid)
-
-let find_label = find_component Env.lookup_label (fun lid -> Unbound_label lid)
-
-let find_class = find_component Env.lookup_class (fun lid -> Unbound_class lid)
-
-let find_value = find_component Env.lookup_value (fun lid -> Unbound_value lid)
-
-let find_module = find_component Env.lookup_module (fun lid -> Unbound_module lid)
-
-let find_modtype = find_component Env.lookup_modtype (fun lid -> Unbound_modtype lid)
-
-let find_cltype = find_component Env.lookup_cltype (fun lid -> Unbound_cltype lid)
+let find_type =
+  find_component Env.lookup_type (fun lid -> Unbound_type_constructor lid)
+let find_constructor =
+  find_component Env.lookup_constructor (fun lid -> Unbound_constructor lid)
+let find_label =
+  find_component Env.lookup_label (fun lid -> Unbound_label lid)
+let find_class =
+  find_component Env.lookup_class (fun lid -> Unbound_class lid)
+let find_value =
+  find_component Env.lookup_value (fun lid -> Unbound_value lid)
+let find_module =
+  find_component Env.lookup_module (fun lid -> Unbound_module lid)
+let find_modtype =
+  find_component Env.lookup_modtype (fun lid -> Unbound_modtype lid)
+let find_cltype =
+  find_component Env.lookup_cltype (fun lid -> Unbound_cltype lid)
 
 (* Support for first-class modules. *)
 
@@ -119,7 +123,8 @@ let create_package_mty fake loc env (p, l) =
                ptype_manifest = if fake then None else Some t;
                ptype_variance = [];
                ptype_loc = loc} in
-      {pmty_desc=Pmty_with (mty, [ Longident.Lident s, Pwith_type d ]); pmty_loc=loc}
+      {pmty_desc=Pmty_with (mty, [ Longident.Lident s, Pwith_type d ]);
+       pmty_loc=loc}
     )
     {pmty_desc=Pmty_ident p; pmty_loc=loc}
     l
@@ -142,6 +147,18 @@ let widen (gl, tv) =
   restore_global_level gl;
   type_variables := tv
 
+let strict_lowercase c = (c = '_' || c >= 'a' && c <= 'z')
+
+let validate_name = function
+    None -> None
+  | Some name as s ->
+      if name <> "" && strict_lowercase name.[0] then s else None
+
+let new_global_var ?name () =
+  new_global_var ?name:(validate_name name) ()
+let newvar ?name () =
+  newvar ?name:(validate_name name) ()
+
 let enter_type_variable strict loc name =
   try
     if name <> "" && name.[0] = '_' then
@@ -150,7 +167,7 @@ let enter_type_variable strict loc name =
     if strict then raise Already_bound;
     v
   with Not_found ->
-    let v = new_global_var() in
+    let v = new_global_var ~name () in
     type_variables := Tbl.add name v !type_variables;
     v
 
@@ -165,8 +182,8 @@ let wrap_method ty =
     Tpoly _ -> ty
   | _ -> Ctype.newty (Tpoly (ty, []))
 
-let new_pre_univar () =
-  let v = newvar () in pre_univars := v :: !pre_univars; v
+let new_pre_univar ?name () =
+  let v = newvar ?name () in pre_univars := v :: !pre_univars; v
 
 let rec swap_list = function
     x :: y :: l -> y :: x :: swap_list l
@@ -190,7 +207,8 @@ let rec transl_type env policy styp =
         instance (fst(Tbl.find name !used_variables))
       with Not_found ->
         let v =
-          if policy = Univars then new_pre_univar () else newvar () in
+          if policy = Univars then new_pre_univar ~name () else newvar ~name ()
+        in
         used_variables := Tbl.add name (v, styp.ptyp_loc) !used_variables;
         v
       end
@@ -333,7 +351,14 @@ let rec transl_type env policy styp =
             end_def ();
             generalize_structure t;
           end;
-          instance t
+          let t = instance t in
+          let px = Btype.proxy t in
+          begin match px.desc with
+          | Tvar None -> Btype.log_type px; px.desc <- Tvar (Some alias)
+          | Tunivar None -> Btype.log_type px; px.desc <- Tunivar (Some alias)
+          | _ -> ()
+          end;
+          t
       end
   | Ptyp_variant(fields, closed, present) ->
       let name = ref None in
@@ -388,7 +413,7 @@ let rec transl_type env policy styp =
               {desc=Tvariant row}, _ when Btype.static_row row ->
                 let row = Btype.row_repr row in
                 row.row_fields
-            | {desc=Tvar}, Some(p, _) ->
+            | {desc=Tvar _}, Some(p, _) ->
                 raise(Error(sty.ptyp_loc, Unbound_type_constructor_2 p))
             | _ ->
                 raise(Error(sty.ptyp_loc, Not_a_variant ty))
@@ -431,7 +456,7 @@ let rec transl_type env policy styp =
       newty (Tvariant row)
   | Ptyp_poly(vars, st) ->
       begin_def();
-      let new_univars = List.map (fun name -> name, newvar()) vars in
+      let new_univars = List.map (fun name -> name, newvar ~name ()) vars in
       let old_univars = !univars in
       univars := new_univars @ !univars;
       let ty = transl_type env policy st in
@@ -443,10 +468,12 @@ let rec transl_type env policy styp =
           (fun tyl (name, ty1) ->
             let v = Btype.proxy ty1 in
             if deep_occur v ty then begin
-              if v.level <> Btype.generic_level || v.desc <> Tvar then
-                raise (Error (styp.ptyp_loc, Cannot_quantify (name, v)));
-              v.desc <- Tunivar;
-              v :: tyl
+              match v.desc with
+                Tvar name when v.level = Btype.generic_level ->
+                  v.desc <- Tunivar name;
+                  v :: tyl
+              | _ ->
+                raise (Error (styp.ptyp_loc, Cannot_quantify (name, v)))
             end else tyl)
           [] new_univars
       in
@@ -483,7 +510,7 @@ let rec make_fixed_univars ty =
     match ty.desc with
     | Tvariant row ->
         let row = Btype.row_repr row in
-        if (Btype.row_more row).desc = Tunivar then
+        if Btype.is_Tunivar (Btype.row_more row) then
           ty.desc <- Tvariant
               {row with row_fixed=true;
                row_fields = List.map
@@ -512,7 +539,7 @@ let globalize_used_variables env fixed =
       then try
         r := (loc, v,  Tbl.find name !type_variables) :: !r
       with Not_found ->
-        if fixed && (repr ty).desc = Tvar then
+        if fixed && Btype.is_Tvar (repr ty) then
           raise(Error(loc, Unbound_type_variable ("'"^name)));
         let v2 = new_global_var () in
         r := (loc, v, v2) :: !r;
@@ -552,8 +579,10 @@ let transl_simple_type_univars env styp =
     List.fold_left
       (fun acc v ->
         let v = repr v in
-        if v.level <> Btype.generic_level || v.desc <> Tvar then acc
-        else (v.desc <- Tunivar ; v :: acc))
+        match v.desc with
+          Tvar name when v.level = Btype.generic_level ->
+            v.desc <- Tunivar name; v :: acc
+        | _ -> acc)
       [] !pre_univars
   in
   make_fixed_univars typ;
@@ -635,8 +664,8 @@ let report_error ppf = function
       fprintf ppf "The type variable name %s is not allowed in programs" name
   | Cannot_quantify (name, v) ->
       fprintf ppf "This type scheme cannot quantify '%s :@ %s." name
-        (if v.desc = Tvar then "it escapes this scope" else
-         if v.desc = Tunivar then "it is aliased to another variable"
+        (if Btype.is_Tvar v then "it escapes this scope" else
+         if Btype.is_Tunivar v then "it is aliased to another variable"
          else "it is not a variable")
   | Multiple_constraints_on_type s ->
       fprintf ppf "Multiple constraints for type %s" s