fix PR#5450

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

testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference

@@ -9,9 +9,9 @@
   | VString of string
   | VList of variant list
   | VPair of variant * variant
-val variantize : 'a ty -> 'a -> variant = <fun>
+val variantize : 't ty -> 't -> variant = <fun>
 exception VariantMismatch
-val devariantize : 'a ty -> variant -> 'a = <fun>
+val devariantize : 't ty -> variant -> 't = <fun>
 #                                                   type 'a ty =
     Int : int ty
   | String : string ty
@@ -27,7 +27,7 @@ and ('a, 'b) field = { label : string; field_type : 'b ty; get : 'a -> 'b; }
   | VList of variant list
   | VPair of variant * variant
   | VRecord of (string * variant) list
-val variantize : 'a ty -> 'a -> variant = <fun>
+val variantize : 't ty -> 't -> variant = <fun>
 #                                                                                                   type 'a ty =
     Int : int ty
   | String : string ty
@@ -48,7 +48,7 @@ and ('a, 'builder, 'b) field_ = {
   get : 'a -> 'b;
   set : 'builder -> 'b -> unit;
 }
-val devariantize : 'a ty -> variant -> 'a = <fun>
+val devariantize : 't ty -> variant -> 't = <fun>
 #                                                   type my_record = { a : int; b : string list; }
 val my_record : my_record ty =
   Record
@@ -87,8 +87,8 @@ and ('a, 'b) ty_case =
 #                                                         type ('a, 'b) eq = Eq : ('a, 'a) eq
 val eq_sel : ('a, 'b) ty_sel -> ('a, 'c) ty_sel -> ('b, 'c) eq option = <fun>
 val get_case :
-  ('a, 'b) ty_sel ->
-  (string * ('c, 'a) ty_case) list -> string * ('b, 'c) ty option = <fun>
+  ('b, 'a) ty_sel ->
+  (string * ('e, 'b) ty_case) list -> string * ('a, 'e) ty option = <fun>
 #                                                         type variant =
     VInt of int
   | VString of string
@@ -98,8 +98,8 @@ val get_case :
   | VConv of string * variant
   | VSum of string * variant option
 val may_map : ('a -> 'b) -> 'a option -> 'b option = <fun>
-val variantize : 'a ty_env -> ('b, 'a) ty -> 'b -> variant = <fun>
-#                                               val devariantize : 'a ty_env -> ('b, 'a) ty -> variant -> 'b = <fun>
+val variantize : 'e ty_env -> ('a, 'e) ty -> 'a -> variant = <fun>
+#                                               val devariantize : 'e ty_env -> ('t, 'e) ty -> variant -> 't = <fun>
 #     val wrap_A : ('a, 'b) ty -> ([ `A of 'a ], 'b) ty = <fun>
 #   val ty : ('a, ([ `A of ('a * 'b) option ] as 'b) -> 'c) ty -> ('b, 'c) ty =
   <fun>
@@ -124,7 +124,7 @@ val v : variant =
     sum_inj = <fun>}
 #                                             val a : [ `A of int | `B of string | `C ] = `A 3
 type 'a vlist = [ `Cons of 'a * 'a vlist | `Nil ]
-val ty_list : ('a, 'b) ty -> ('a vlist, 'b) ty = <fun>
+val ty_list : ('a, 'e) ty -> ('a vlist, 'e) ty = <fun>
 val v : variant =
   VSum ("Cons",
    Some
@@ -172,5 +172,5 @@ and ('a, 'b) ty_case =
   | TCnoarg : ('b, noarg) ty_sel -> ('e, 'b) ty_case
 #                                                                     val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum <obj>
 type 'a vlist = [ `Cons of 'a * 'a vlist | `Nil ]
-val ty_list : ('a, 'b) ty -> ('a vlist, 'b) ty = <fun>
+val ty_list : ('a, 'e) ty -> ('a vlist, 'e) ty = <fun>
 #   * * * * * * * * *   

testsuite/tests/typing-gadts/dynamic_frisch.ml.reference

@@ -9,9 +9,9 @@
   | VString of string
   | VList of variant list
   | VPair of variant * variant
-val variantize : 'a ty -> 'a -> variant = <fun>
+val variantize : 't ty -> 't -> variant = <fun>
 exception VariantMismatch
-val devariantize : 'a ty -> variant -> 'a = <fun>
+val devariantize : 't ty -> variant -> 't = <fun>
 #                                                   type 'a ty =
     Int : int ty
   | String : string ty
@@ -27,7 +27,7 @@ and ('a, 'b) field = { label : string; field_type : 'b ty; get : 'a -> 'b; }
   | VList of variant list
   | VPair of variant * variant
   | VRecord of (string * variant) list
-val variantize : 'a ty -> 'a -> variant = <fun>
+val variantize : 't ty -> 't -> variant = <fun>
 #                                                                                                   type 'a ty =
     Int : int ty
   | String : string ty
@@ -48,7 +48,7 @@ and ('a, 'builder, 'b) field_ = {
   get : 'a -> 'b;
   set : 'builder -> 'b -> unit;
 }
-val devariantize : 'a ty -> variant -> 'a = <fun>
+val devariantize : 't ty -> variant -> 't = <fun>
 #                                                   type my_record = { a : int; b : string list; }
 val my_record : my_record ty =
   Record
@@ -87,8 +87,8 @@ and ('a, 'b) ty_case =
 #                                                         type ('a, 'b) eq = Eq : ('a, 'a) eq
 val eq_sel : ('a, 'b) ty_sel -> ('a, 'c) ty_sel -> ('b, 'c) eq option = <fun>
 val get_case :
-  ('a, 'b) ty_sel ->
-  (string * ('c, 'a) ty_case) list -> string * ('b, 'c) ty option = <fun>
+  ('b, 'a) ty_sel ->
+  (string * ('e, 'b) ty_case) list -> string * ('a, 'e) ty option = <fun>
 #                                                         type variant =
     VInt of int
   | VString of string
@@ -98,8 +98,8 @@ val get_case :
   | VConv of string * variant
   | VSum of string * variant option
 val may_map : ('a -> 'b) -> 'a option -> 'b option = <fun>
-val variantize : 'a ty_env -> ('b, 'a) ty -> 'b -> variant = <fun>
-#                                               val devariantize : 'a ty_env -> ('b, 'a) ty -> variant -> 'b = <fun>
+val variantize : 'e ty_env -> ('a, 'e) ty -> 'a -> variant = <fun>
+#                                               val devariantize : 'e ty_env -> ('t, 'e) ty -> variant -> 't = <fun>
 #     val wrap_A : ('a, 'b) ty -> ([ `A of 'a ], 'b) ty = <fun>
 #   val ty : ('a, ([ `A of ('a * 'b) option ] as 'b) -> 'c) ty -> ('b, 'c) ty =
   <fun>
@@ -124,7 +124,7 @@ val v : variant =
     sum_inj = <fun>}
 #                                             val a : [ `A of int | `B of string | `C ] = `A 3
 type 'a vlist = [ `Cons of 'a * 'a vlist | `Nil ]
-val ty_list : ('a, 'b) ty -> ('a vlist, 'b) ty = <fun>
+val ty_list : ('a, 'e) ty -> ('a vlist, 'e) ty = <fun>
 val v : variant =
   VSum ("Cons",
    Some
@@ -172,5 +172,5 @@ and ('a, 'b) ty_case =
   | TCnoarg : ('b, noarg) ty_sel -> ('e, 'b) ty_case
 #                                                                     val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum <obj>
 type 'a vlist = [ `Cons of 'a * 'a vlist | `Nil ]
-val ty_list : ('a, 'b) ty -> ('a vlist, 'b) ty = <fun>
+val ty_list : ('a, 'e) ty -> ('a vlist, 'e) ty = <fun>
 #   * * * * * * * * *   

testsuite/tests/typing-gadts/omega07.ml.principal.reference

@@ -10,10 +10,10 @@ type 'a nat = NZ : zero nat | NS : 'a nat -> 'a succ nat
 #       *         type ('a, 'b, 'c) plus =
     PlusZ : 'a nat -> (zero, 'a, 'a) plus
   | PlusS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus
-#         val length : ('a, 'b) seq -> 'b nat = <fun>
+#         val length : ('a, 'n) seq -> 'n nat = <fun>
 #   *                     type ('a, 'b, 'c) app =
     App : ('a, 'p) seq * ('n, 'm, 'p) plus -> ('a, 'n, 'm) app
-val app : ('a, 'b) seq -> ('a, 'c) seq -> ('a, 'b, 'c) app = <fun>
+val app : ('a, 'n) seq -> ('a, 'm) seq -> ('a, 'n, 'm) app = <fun>
 # *                           type tp
 type nd
 type ('a, 'b) fk
@@ -35,9 +35,9 @@ type 'a boolean = BT : tt boolean | BF : ff boolean
   | Tfork : ('x, 'a) tree * ('y, 'a) tree -> (('x, 'y) fk, 'a) tree
 #   val tree1 : (((tp, nd) fk, (nd, nd) fk) fk, int) tree =
   Tfork (Tfork (Ttip, Tnode 4), Tfork (Tnode 4, Tnode 3))
-#                     val find : ('a -> 'a -> bool) -> 'a -> ('b, 'a) tree -> ('b, 'a) path list =
+#                     val find : ('a -> 'a -> bool) -> 'a -> ('sh, 'a) tree -> ('sh, 'a) path list =
   <fun>
-#             val extract : ('b, 'a) path -> ('b, 'a) tree -> 'a = <fun>
+#             val extract : ('sh, 'a) path -> ('sh, 'a) tree -> 'a = <fun>
 #             type ('a, 'b) le =
     LeZ : 'a nat -> (zero, 'a) le
   | LeS : ('n, 'm) le -> ('n succ, 'm succ) le
@@ -68,8 +68,8 @@ Here is an example of a value that is not matched:
 val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
 #               val diff : ('a, 'b) le -> 'b nat -> ('a, 'b) diff = <fun>
 #             type ('a, 'b) filter = Filter : ('m, 'n) le * ('a, 'm) seq -> ('a, 'n) filter
-val leS' : ('a, 'b) le -> ('a, 'b succ) le = <fun>
-#                   val filter : ('a -> bool) -> ('a, 'b) seq -> ('a, 'b) filter = <fun>
+val leS' : ('m, 'n) le -> ('m, 'n succ) le = <fun>
+#                   val filter : ('a -> bool) -> ('a, 'n) seq -> ('a, 'n) filter = <fun>
 #                             type ('a, 'b, 'c) balance =
     Less : ('h, 'h succ, 'h succ) balance
   | Same : ('h, 'h, 'h) balance
@@ -80,21 +80,21 @@ type 'a avl =
       'hR avl -> 'hMax succ avl
 type avl' = Avl : 'h avl -> avl'
 #                 val empty : avl' = Avl Leaf
-val elem : int -> 'a avl -> bool = <fun>
+val elem : int -> 'h avl -> bool = <fun>
 #                           val rotr :
-  'a succ succ avl ->
-  int -> 'a avl -> ('a succ succ avl, 'a succ succ succ avl) sum = <fun>
+  'n succ succ avl ->
+  int -> 'n avl -> ('n succ succ avl, 'n succ succ succ avl) sum = <fun>
 #                         val rotl :
-  'a avl ->
-  int -> 'a succ succ avl -> ('a succ succ avl, 'a succ succ succ avl) sum =
+  'n avl ->
+  int -> 'n succ succ avl -> ('n succ succ avl, 'n succ succ succ avl) sum =
   <fun>
-#                                               val ins : int -> 'a avl -> ('a avl, 'a succ avl) sum = <fun>
+#                                               val ins : int -> 'n avl -> ('n avl, 'n succ avl) sum = <fun>
 #           val insert : int -> avl' -> avl' = <fun>
-#                                                                                                                                 val del_min : 'a succ avl -> int * ('a avl, 'a succ avl) sum = <fun>
+#                                                                                                                                 val del_min : 'n succ avl -> int * ('n avl, 'n succ avl) sum = <fun>
 type 'a avl_del =
     Dsame : 'n avl -> 'n avl_del
   | Ddecr : ('m succ, 'n) equal * 'm avl -> 'n avl_del
-val del : int -> 'a avl -> 'a avl_del = <fun>
+val del : int -> 'n avl -> 'n avl_del = <fun>
 #           val delete : int -> avl' -> avl' = <fun>
 #                             type red
 type black
@@ -114,8 +114,8 @@ type ('a, 'b) ctxt =
       (black, 'n succ) ctxt -> ('c, 'n) ctxt
 #                         val blacken : (red, 'a) sub_tree -> (black, 'a succ) sub_tree = <fun>
 type 'a crep = Red : red crep | Black : black crep
-val color : ('a, 'b) sub_tree -> 'a crep = <fun>
-#                   val fill : ('a, 'b) ctxt -> ('a, 'b) sub_tree -> rb_tree = <fun>
+val color : ('c, 'n) sub_tree -> 'c crep = <fun>
+#                   val fill : ('c, 'n) ctxt -> ('c, 'n) sub_tree -> rb_tree = <fun>
 #             val recolor :
   dir ->
   int ->
@@ -132,8 +132,8 @@ val color : ('a, 'b) sub_tree -> 'a crep = <fun>
   int ->
   (black, 'a) sub_tree -> (red, 'a) sub_tree -> (black, 'a succ) sub_tree =
   <fun>
-#                     val repair : (red, 'a) sub_tree -> ('b, 'a) ctxt -> rb_tree = <fun>
-#                     val ins : int -> ('a, 'b) sub_tree -> ('a, 'b) ctxt -> rb_tree = <fun>
+#                     val repair : (red, 'n) sub_tree -> ('c, 'n) ctxt -> rb_tree = <fun>
+#                     val ins : int -> ('c, 'n) sub_tree -> ('c, 'n) ctxt -> rb_tree = <fun>
 #   val insert : int -> rb_tree -> rb_tree = <fun>
 #                                                                                                 type 'a term =
     Const : int -> int term
@@ -189,7 +189,7 @@ val ex2 : ('a, ('b -> 'c) -> 'b -> 'c) lam =
 #                           type 'a env =
     Enil : rnil env
   | Econs : 'a * 't * 'e env -> ('a, 't, 'e) rcons env
-val eval_lam : 'a env -> ('a, 'b) lam -> 'b = <fun>
+val eval_lam : 'e env -> ('e, 't) lam -> 't = <fun>
 #                               type add = Add
 type suc = Suc
 val env0 :
@@ -246,8 +246,8 @@ type 'a ctx =
 #                             type 'a checked =
     Cerror of string
   | Cok : ('e, 't) lam * 't rep -> 'e checked
-val lookup : string -> 'a ctx -> 'a checked = <fun>
-#                                                   val tc : 'a nat -> 'b ctx -> term -> 'b checked = <fun>
+val lookup : string -> 'e ctx -> 'e checked = <fun>
+#                                                   val tc : 'n nat -> 'e ctx -> term -> 'e checked = <fun>
 #             val ctx0 :
   (zero, int, (suc, int -> int, (add, int -> int -> int, rnil) rcons) rcons)
   rcons ctx =
@@ -291,18 +291,18 @@ type ('a, 'b, 'c) lam =
       ('m2, 'e, 's) lam -> (pexp, 'e, 't) lam
 #                   val ex1 : (pexp, 'a, tint) lam =
   App (Lam (<poly>, Var <poly>), Const (IntR, <poly>))
-val mode : ('a, 'b, 'c) lam -> 'a mode = <fun>
+val mode : ('m, 'e, 't) lam -> 'm mode = <fun>
 #               type ('a, 'b) sub =
     Id : ('r, 'r) sub
   | Bind : 't * ('m, 'r2, 'x) lam *
       ('r, 'r2) sub -> (('t, 'x, 'r) rcons, 'r2) sub
   | Push : ('r1, 'r2) sub -> (('a, 'b, 'r1) rcons, ('a, 'b, 'r2) rcons) sub
 type ('a, 'b) lam' = Ex : ('m, 's, 't) lam -> ('s, 't) lam'
-#                               val subst : ('a, 'b, 'c) lam -> ('b, 'd) sub -> ('d, 'c) lam' = <fun>
+#                               val subst : ('m1, 'r, 't) lam -> ('r, 's) sub -> ('s, 't) lam' = <fun>
 #       type closed = rnil
 type 'a rlam = ((pexp, closed, 'a) lam, (pval, closed, 'a) lam) sum
 #                             val rule :
   (pval, closed, ('a, 'b) tarr) lam -> (pval, closed, 'a) lam -> 'b rlam =
   <fun>
-#                                 val onestep : ('a, closed, 'b) lam -> 'b rlam = <fun>
+#                                 val onestep : ('m, closed, 't) lam -> 't rlam = <fun>
 # 

testsuite/tests/typing-gadts/omega07.ml.reference

@@ -10,10 +10,10 @@ type 'a nat = NZ : zero nat | NS : 'a nat -> 'a succ nat
 #       *         type ('a, 'b, 'c) plus =
     PlusZ : 'a nat -> (zero, 'a, 'a) plus
   | PlusS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus
-#         val length : ('a, 'b) seq -> 'b nat = <fun>
+#         val length : ('a, 'n) seq -> 'n nat = <fun>
 #   *                     type ('a, 'b, 'c) app =
     App : ('a, 'p) seq * ('n, 'm, 'p) plus -> ('a, 'n, 'm) app
-val app : ('a, 'b) seq -> ('a, 'c) seq -> ('a, 'b, 'c) app = <fun>
+val app : ('a, 'n) seq -> ('a, 'm) seq -> ('a, 'n, 'm) app = <fun>
 # *                           type tp
 type nd
 type ('a, 'b) fk
@@ -35,9 +35,9 @@ type 'a boolean = BT : tt boolean | BF : ff boolean
   | Tfork : ('x, 'a) tree * ('y, 'a) tree -> (('x, 'y) fk, 'a) tree
 #   val tree1 : (((tp, nd) fk, (nd, nd) fk) fk, int) tree =
   Tfork (Tfork (Ttip, Tnode 4), Tfork (Tnode 4, Tnode 3))
-#                     val find : ('a -> 'a -> bool) -> 'a -> ('b, 'a) tree -> ('b, 'a) path list =
+#                     val find : ('a -> 'a -> bool) -> 'a -> ('sh, 'a) tree -> ('sh, 'a) path list =
   <fun>
-#             val extract : ('b, 'a) path -> ('b, 'a) tree -> 'a = <fun>
+#             val extract : ('sh, 'a) path -> ('sh, 'a) tree -> 'a = <fun>
 #             type ('a, 'b) le =
     LeZ : 'a nat -> (zero, 'a) le
   | LeS : ('n, 'm) le -> ('n succ, 'm succ) le
@@ -68,8 +68,8 @@ Here is an example of a value that is not matched:
 val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
 #               val diff : ('a, 'b) le -> 'b nat -> ('a, 'b) diff = <fun>
 #             type ('a, 'b) filter = Filter : ('m, 'n) le * ('a, 'm) seq -> ('a, 'n) filter
-val leS' : ('a, 'b) le -> ('a, 'b succ) le = <fun>
-#                   val filter : ('a -> bool) -> ('a, 'b) seq -> ('a, 'b) filter = <fun>
+val leS' : ('m, 'n) le -> ('m, 'n succ) le = <fun>
+#                   val filter : ('a -> bool) -> ('a, 'n) seq -> ('a, 'n) filter = <fun>
 #                             type ('a, 'b, 'c) balance =
     Less : ('h, 'h succ, 'h succ) balance
   | Same : ('h, 'h, 'h) balance
@@ -80,21 +80,21 @@ type 'a avl =
       'hR avl -> 'hMax succ avl
 type avl' = Avl : 'h avl -> avl'
 #                 val empty : avl' = Avl Leaf
-val elem : int -> 'a avl -> bool = <fun>
+val elem : int -> 'h avl -> bool = <fun>
 #                           val rotr :
-  'a succ succ avl ->
-  int -> 'a avl -> ('a succ succ avl, 'a succ succ succ avl) sum = <fun>
+  'n succ succ avl ->
+  int -> 'n avl -> ('n succ succ avl, 'n succ succ succ avl) sum = <fun>
 #                         val rotl :
-  'a avl ->
-  int -> 'a succ succ avl -> ('a succ succ avl, 'a succ succ succ avl) sum =
+  'n avl ->
+  int -> 'n succ succ avl -> ('n succ succ avl, 'n succ succ succ avl) sum =
   <fun>
-#                                               val ins : int -> 'a avl -> ('a avl, 'a succ avl) sum = <fun>
+#                                               val ins : int -> 'n avl -> ('n avl, 'n succ avl) sum = <fun>
 #           val insert : int -> avl' -> avl' = <fun>
-#                                                                                                                                 val del_min : 'a succ avl -> int * ('a avl, 'a succ avl) sum = <fun>
+#                                                                                                                                 val del_min : 'n succ avl -> int * ('n avl, 'n succ avl) sum = <fun>
 type 'a avl_del =
     Dsame : 'n avl -> 'n avl_del
   | Ddecr : ('m succ, 'n) equal * 'm avl -> 'n avl_del
-val del : int -> 'a avl -> 'a avl_del = <fun>
+val del : int -> 'n avl -> 'n avl_del = <fun>
 #           val delete : int -> avl' -> avl' = <fun>
 #                             type red
 type black
@@ -114,8 +114,8 @@ type ('a, 'b) ctxt =
       (black, 'n succ) ctxt -> ('c, 'n) ctxt
 #                         val blacken : (red, 'a) sub_tree -> (black, 'a succ) sub_tree = <fun>
 type 'a crep = Red : red crep | Black : black crep
-val color : ('a, 'b) sub_tree -> 'a crep = <fun>
-#                   val fill : ('a, 'b) ctxt -> ('a, 'b) sub_tree -> rb_tree = <fun>
+val color : ('c, 'n) sub_tree -> 'c crep = <fun>
+#                   val fill : ('c, 'n) ctxt -> ('c, 'n) sub_tree -> rb_tree = <fun>
 #             val recolor :
   dir ->
   int ->
@@ -132,8 +132,8 @@ val color : ('a, 'b) sub_tree -> 'a crep = <fun>
   int ->
   (black, 'a) sub_tree -> (red, 'a) sub_tree -> (black, 'a succ) sub_tree =
   <fun>
-#                     val repair : (red, 'a) sub_tree -> ('b, 'a) ctxt -> rb_tree = <fun>
-#                     val ins : int -> ('a, 'b) sub_tree -> ('a, 'b) ctxt -> rb_tree = <fun>
+#                     val repair : (red, 'n) sub_tree -> ('c, 'n) ctxt -> rb_tree = <fun>
+#                     val ins : int -> ('c, 'n) sub_tree -> ('c, 'n) ctxt -> rb_tree = <fun>
 #   val insert : int -> rb_tree -> rb_tree = <fun>
 #                                                                                                 type 'a term =
     Const : int -> int term
@@ -189,7 +189,7 @@ val ex2 : ('a, ('b -> 'c) -> 'b -> 'c) lam =
 #                           type 'a env =
     Enil : rnil env
   | Econs : 'a * 't * 'e env -> ('a, 't, 'e) rcons env
-val eval_lam : 'a env -> ('a, 'b) lam -> 'b = <fun>
+val eval_lam : 'e env -> ('e, 't) lam -> 't = <fun>
 #                               type add = Add
 type suc = Suc
 val env0 :
@@ -246,8 +246,8 @@ type 'a ctx =
 #                             type 'a checked =
     Cerror of string
   | Cok : ('e, 't) lam * 't rep -> 'e checked
-val lookup : string -> 'a ctx -> 'a checked = <fun>
-#                                                   val tc : 'a nat -> 'b ctx -> term -> 'b checked = <fun>
+val lookup : string -> 'e ctx -> 'e checked = <fun>
+#                                                   val tc : 'n nat -> 'e ctx -> term -> 'e checked = <fun>
 #             val ctx0 :
   (zero, int, (suc, int -> int, (add, int -> int -> int, rnil) rcons) rcons)
   rcons ctx =
@@ -291,18 +291,18 @@ type ('a, 'b, 'c) lam =
       ('m2, 'e, 's) lam -> (pexp, 'e, 't) lam
 #                   val ex1 : (pexp, 'a, tint) lam =
   App (Lam (<poly>, Var <poly>), Const (IntR, <poly>))
-val mode : ('a, 'b, 'c) lam -> 'a mode = <fun>
+val mode : ('m, 'e, 't) lam -> 'm mode = <fun>
 #               type ('a, 'b) sub =
     Id : ('r, 'r) sub
   | Bind : 't * ('m, 'r2, 'x) lam *
       ('r, 'r2) sub -> (('t, 'x, 'r) rcons, 'r2) sub
   | Push : ('r1, 'r2) sub -> (('a, 'b, 'r1) rcons, ('a, 'b, 'r2) rcons) sub
 type ('a, 'b) lam' = Ex : ('m, 's, 't) lam -> ('s, 't) lam'
-#                               val subst : ('a, 'b, 'c) lam -> ('b, 'd) sub -> ('d, 'c) lam' = <fun>
+#                               val subst : ('m1, 'r, 't) lam -> ('r, 's) sub -> ('s, 't) lam' = <fun>
 #       type closed = rnil
 type 'a rlam = ((pexp, closed, 'a) lam, (pval, closed, 'a) lam) sum
 #                             val rule :
   (pval, closed, ('a, 'b) tarr) lam -> (pval, closed, 'a) lam -> 'b rlam =
   <fun>
-#                                 val onestep : ('a, closed, 'b) lam -> 'b rlam = <fun>
+#                                 val onestep : ('m, closed, 't) lam -> 't rlam = <fun>
 # 

testsuite/tests/typing-gadts/pr5332.ml.reference

@@ -14,6 +14,6 @@
 Warning 8: this pattern-matching is not exhaustive.
 Here is an example of a value that is not matched:
 (Tbool, Tvar _)
-val f : ('a, 'b) typ -> ('a, 'b) typ -> int = <fun>
+val f : ('env, 'a) typ -> ('env, 'a) typ -> int = <fun>
 #   Exception: Match_failure ("//toplevel//", 9, 1).
 # 

testsuite/tests/typing-gadts/term-conv.ml.principal.reference

@@ -9,8 +9,8 @@
       | Fun : ('a ty * 'b ty) -> ('a -> 'b) ty
     type ('a, 'b) eq = Eq : ('a, 'a) eq
     exception CastFailure
-    val check_eq : 'a ty -> 'b ty -> ('a, 'b) eq
-    val gcast : 'a ty -> 'b ty -> 'a -> 'b
+    val check_eq : 't ty -> 't' ty -> ('t, 't') eq
+    val gcast : 't ty -> 't' ty -> 't -> 't'
   end
 #                               module HOAS :
   sig
@@ -19,14 +19,14 @@
       | Con : 't -> 't term
       | Lam : 's Typeable.ty * ('s term -> 't term) -> ('s -> 't) term
       | App : ('s -> 't) term * 's term -> 't term
-    val intp : 'a term -> 'a
+    val intp : 't term -> 't
   end
 #                                                               module DeBruijn :
   sig
     type ('env, 't) ix =
         ZeroIx : ('env * 't, 't) ix
       | SuccIx : ('env, 't) ix -> ('env * 's, 't) ix
-    val to_int : ('a, 'b) ix -> int
+    val to_int : ('env, 't) ix -> int
     type ('env, 't) term =
         Var : ('env, 't) ix -> ('env, 't) term
       | Con : 't -> ('env, 't) term
@@ -35,8 +35,8 @@
     type 'a stack =
         Empty : unit stack
       | Push : 'env stack * 't -> ('env * 't) stack
-    val prj : ('a, 'b) ix -> 'a stack -> 'b
-    val intp : ('a, 'b) term -> 'a stack -> 'b
+    val prj : ('env, 't) ix -> 'env stack -> 't
+    val intp : ('env, 't) term -> 'env stack -> 't
   end
 #                                                                             module Convert :
   sig
@@ -44,11 +44,11 @@
         EmptyLayout : ('env, unit) layout
       | PushLayout : 't Typeable.ty * ('env, 'env') layout *
           ('env, 't) DeBruijn.ix -> ('env, 'env' * 't) layout
-    val size : ('a, 'b) layout -> int
-    val inc : ('a, 'b) layout -> ('a * 't, 'b) layout
+    val size : ('env, 'env') layout -> int
+    val inc : ('env, 'env') layout -> ('env * 't, 'env') layout
     val prj :
-      'a Typeable.ty -> int -> ('b, 'c) layout -> ('b, 'a) DeBruijn.ix
-    val cvt : ('a, 'a) layout -> 'b HOAS.term -> ('a, 'b) DeBruijn.term
+      't Typeable.ty -> int -> ('env, 'env') layout -> ('env, 't) DeBruijn.ix
+    val cvt : ('env, 'env) layout -> 't HOAS.term -> ('env, 't) DeBruijn.term
     val convert : 'a HOAS.term -> (unit, 'a) DeBruijn.term
   end
 #                                               module Main :

testsuite/tests/typing-gadts/term-conv.ml.reference

@@ -9,8 +9,8 @@
       | Fun : ('a ty * 'b ty) -> ('a -> 'b) ty
     type ('a, 'b) eq = Eq : ('a, 'a) eq
     exception CastFailure
-    val check_eq : 'a ty -> 'b ty -> ('a, 'b) eq
-    val gcast : 'a ty -> 'b ty -> 'a -> 'b
+    val check_eq : 't ty -> 't' ty -> ('t, 't') eq
+    val gcast : 't ty -> 't' ty -> 't -> 't'
   end
 #                               module HOAS :
   sig
@@ -19,14 +19,14 @@
       | Con : 't -> 't term
       | Lam : 's Typeable.ty * ('s term -> 't term) -> ('s -> 't) term
       | App : ('s -> 't) term * 's term -> 't term
-    val intp : 'a term -> 'a
+    val intp : 't term -> 't
   end
 #                                                               module DeBruijn :
   sig
     type ('env, 't) ix =
         ZeroIx : ('env * 't, 't) ix
       | SuccIx : ('env, 't) ix -> ('env * 's, 't) ix
-    val to_int : ('a, 'b) ix -> int
+    val to_int : ('env, 't) ix -> int
     type ('env, 't) term =
         Var : ('env, 't) ix -> ('env, 't) term
       | Con : 't -> ('env, 't) term
@@ -35,8 +35,8 @@
     type 'a stack =
         Empty : unit stack
       | Push : 'env stack * 't -> ('env * 't) stack
-    val prj : ('a, 'b) ix -> 'a stack -> 'b
-    val intp : ('a, 'b) term -> 'a stack -> 'b
+    val prj : ('env, 't) ix -> 'env stack -> 't
+    val intp : ('env, 't) term -> 'env stack -> 't
   end
 #                                                                             module Convert :
   sig
@@ -44,11 +44,11 @@
         EmptyLayout : ('env, unit) layout
       | PushLayout : 't Typeable.ty * ('env, 'env') layout *
           ('env, 't) DeBruijn.ix -> ('env, 'env' * 't) layout
-    val size : ('a, 'b) layout -> int
-    val inc : ('a, 'b) layout -> ('a * 't, 'b) layout
+    val size : ('env, 'env') layout -> int
+    val inc : ('env, 'env') layout -> ('env * 't, 'env') layout
     val prj :
-      'a Typeable.ty -> int -> ('b, 'c) layout -> ('b, 'a) DeBruijn.ix
-    val cvt : ('a, 'a) layout -> 'b HOAS.term -> ('a, 'b) DeBruijn.term
+      't Typeable.ty -> int -> ('env, 'env') layout -> ('env, 't) DeBruijn.ix
+    val cvt : ('env, 'env) layout -> 't HOAS.term -> ('env, 't) DeBruijn.term
     val convert : 'a HOAS.term -> (unit, 'a) DeBruijn.term
   end
 #                                               module Main :

testsuite/tests/typing-gadts/test.ml.principal.reference

@@ -7,7 +7,7 @@
       | Pair : 'a t * 'b t -> ('a * 'b) t
       | App : ('a -> 'b) t * 'a t -> 'b t
       | Abs : ('a -> 'b) -> ('a -> 'b) t
-    val eval : 'a t -> 'a
+    val eval : 's t -> 's
     val discern : 'a t -> int
   end
 #                                     module List :
@@ -35,17 +35,17 @@ module Nonexhaustive :
   sig
     type 'a u = C1 : int -> int u | C2 : bool -> bool u
     type 'a v = C1 : int -> int v
-    val unexhaustive : 'a u -> 'a
+    val unexhaustive : 's u -> 's
     module M : sig type t type u end
     type 'a t = Foo : M.t -> M.t t | Bar : M.u -> M.u t
-    val same_type : 'a t * 'a t -> bool
+    val same_type : 's t * 's t -> bool
   end
 #                             module Exhaustive :
   sig
     type t = int
     type u = bool
     type 'a v = Foo : t -> t v | Bar : u -> u v
-    val same_type : 'a v * 'a v -> bool
+    val same_type : 's v * 's v -> bool
   end
 #               Characters 119-120:
       let eval (D x) = x
@@ -205,8 +205,8 @@ Error: This expression has type [> `A of a ]
   ....f : type a b. (a,b) eq -> [< `A of a | `B] -> [< `A of b | `B] =
     fun Eq o -> o..............
 Error: This definition has type
-         ('c, 'd) eq -> ([< `A of 'd & 'c | `B ] as 'e) -> 'e
-       which is less general than 'a 'b. ('a, 'b) eq -> 'e -> 'e
+         ('a, 'b) eq -> ([< `A of 'b & 'a | `B ] as 'c) -> 'c
+       which is less general than 'a0 'b0. ('a0, 'b0) eq -> 'c -> 'c
 #     val f : ('a, 'b) eq -> [ `A of 'a | `B ] -> [ `A of 'b | `B ] = <fun>
 #       val f : ('a, int) eq -> [ `A of 'a ] -> bool = <fun>
 #           Characters 166-167:

testsuite/tests/typing-gadts/test.ml.reference

@@ -7,7 +7,7 @@
       | Pair : 'a t * 'b t -> ('a * 'b) t
       | App : ('a -> 'b) t * 'a t -> 'b t
       | Abs : ('a -> 'b) -> ('a -> 'b) t
-    val eval : 'a t -> 'a
+    val eval : 's t -> 's
     val discern : 'a t -> int
   end
 #                                     module List :
@@ -35,17 +35,17 @@ module Nonexhaustive :
   sig
     type 'a u = C1 : int -> int u | C2 : bool -> bool u
     type 'a v = C1 : int -> int v
-    val unexhaustive : 'a u -> 'a
+    val unexhaustive : 's u -> 's
     module M : sig type t type u end
     type 'a t = Foo : M.t -> M.t t | Bar : M.u -> M.u t
-    val same_type : 'a t * 'a t -> bool
+    val same_type : 's t * 's t -> bool
   end
 #                             module Exhaustive :
   sig
     type t = int
     type u = bool
     type 'a v = Foo : t -> t v | Bar : u -> u v
-    val same_type : 'a v * 'a v -> bool
+    val same_type : 's v * 's v -> bool
   end
 #               Characters 119-120:
       let eval (D x) = x
@@ -70,7 +70,7 @@ Error: This pattern matches values of type ([? `A ] as 'a) * bool t
 #                                 module Propagation :
   sig
     type 'a t = IntLit : int -> int t | BoolLit : bool -> bool t
-    val check : 'a t -> 'a
+    val check : 's t -> 's
   end
 #             Characters 87-88:
     let f = function A -> 1 | B -> 2
@@ -199,8 +199,8 @@ Error: This expression has type [> `A of a ]
   ....f : type a b. (a,b) eq -> [< `A of a | `B] -> [< `A of b | `B] =
     fun Eq o -> o..............
 Error: This definition has type
-         ('c, 'd) eq -> ([< `A of 'd & 'c | `B ] as 'e) -> 'e
-       which is less general than 'a 'b. ('a, 'b) eq -> 'e -> 'e
+         ('a, 'b) eq -> ([< `A of 'b & 'a | `B ] as 'c) -> 'c
+       which is less general than 'a0 'b0. ('a0, 'b0) eq -> 'c -> 'c
 #     val f : ('a, 'b) eq -> [ `A of 'a | `B ] -> [ `A of 'b | `B ] = <fun>
 #       val f : ('a, int) eq -> [ `A of 'a ] -> bool = <fun>
 #           val f : ('a, 'b) eq -> [ `A of 'a | `B ] -> [ `A of 'b | `B ] = <fun>

testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference

@@ -16,7 +16,7 @@ Warning 8: this pattern-matching is not exhaustive.
 Here is an example of a value that is not matched:
 (IntLit, 0)
 type 'a t = IntLit : int t | BoolLit : bool t
-val check : 'a t * 'a -> bool = <fun>
+val check : 's t * 's -> bool = <fun>
 #             Characters 91-180:
   .............................................function
     | {fst = BoolLit; snd = false} -> false
@@ -25,5 +25,5 @@ Warning 8: this pattern-matching is not exhaustive.
 Here is an example of a value that is not matched:
 {fst=IntLit; snd=0}
 type ('a, 'b) pair = { fst : 'a; snd : 'b; }
-val check : ('a t, 'a) pair -> bool = <fun>
+val check : ('s t, 's) pair -> bool = <fun>
 # 

testsuite/tests/typing-gadts/yallop_bugs.ml.reference

@@ -16,7 +16,7 @@ Warning 8: this pattern-matching is not exhaustive.
 Here is an example of a value that is not matched:
 (IntLit, 0)
 type 'a t = IntLit : int t | BoolLit : bool t
-val check : 'a t * 'a -> bool = <fun>
+val check : 's t * 's -> bool = <fun>
 #             Characters 91-180:
   .............................................function
     | {fst = BoolLit; snd = false} -> false
@@ -25,5 +25,5 @@ Warning 8: this pattern-matching is not exhaustive.
 Here is an example of a value that is not matched:
 {fst=IntLit; snd=0}
 type ('a, 'b) pair = { fst : 'a; snd : 'b; }
-val check : ('a t, 'a) pair -> bool = <fun>
+val check : ('s t, 's) pair -> bool = <fun>
 # 

testsuite/tests/typing-poly/poly.ml.principal.reference

@@ -576,8 +576,8 @@ val g : 'a -> int = <fun>
 #     Characters 34-74:
     function Leaf _ -> 1 | Node x -> 1 + d x
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This definition has type 'b t -> int which is less general than
-         'a. 'a t -> int
+Error: This definition has type 'a t -> int which is less general than
+         'a0. 'a0 t -> int
 #   Characters 34-78:
     function Leaf x -> x | Node x -> 1 + depth x;; (* fails *)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -586,12 +586,12 @@ 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 'b t -> 'b which is less general than
-         'a. 'a t -> 'b
+Error: This definition has type 'a t -> 'a which is less general than
+         'a0. 'a0 t -> 'a
 #   Characters 38-78:
     function Leaf x -> x | Node x -> depth x;; (* fails *)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This definition has type 'c. 'c t -> 'c which is less general than
+Error: This definition has type 'b. 'b t -> 'b 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>

testsuite/tests/typing-poly/poly.ml.reference

@@ -539,8 +539,8 @@ val g : 'a -> int = <fun>
 #     Characters 34-74:
     function Leaf _ -> 1 | Node x -> 1 + d x
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This definition has type 'b t -> int which is less general than
-         'a. 'a t -> int
+Error: This definition has type 'a t -> int which is less general than
+         'a0. 'a0 t -> int
 #   Characters 34-78:
     function Leaf x -> x | Node x -> 1 + depth x;; (* fails *)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -549,12 +549,12 @@ 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 'b t -> 'b which is less general than
-         'a. 'a t -> 'b
+Error: This definition has type 'a t -> 'a which is less general than
+         'a0. 'a0 t -> 'a
 #   Characters 38-78:
     function Leaf x -> x | Node x -> depth x;; (* fails *)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This definition has type 'c. 'c t -> 'c which is less general than
+Error: This definition has type 'b. 'b t -> 'b 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>

typing/ctype.ml

@@ -1176,9 +1176,15 @@ let rec copy_sep fixed free bound visited ty =
     t
   end
 
-let instance_poly fixed univars sch =
-  let vars = List.map (fun _ -> newvar ()) univars in
-  let pairs = List.map2 (fun u v -> repr u, (v, [])) univars vars in
+let instance_poly ?(keep_names=false) fixed univars sch =
+  let univars = List.map repr univars in
+  let copy_var ty =
+    match ty.desc with
+      Tunivar name -> if keep_names then newty (Tvar name) else newvar ()
+    | _ -> assert false
+  in
+  let vars = List.map copy_var univars in
+  let pairs = List.map2 (fun u v -> u, (v, [])) univars vars in
   delayed_copy := [];
   let ty = copy_sep fixed (compute_univars sch) [] pairs sch in
   List.iter Lazy.force !delayed_copy;

typing/ctype.mli

@@ -128,6 +128,7 @@ val instance_declaration: type_declaration -> type_declaration
 val instance_class:
         type_expr list -> class_type -> type_expr list * class_type
 val instance_poly:
+        ?keep_names:bool ->
         bool -> type_expr list -> type_expr -> type_expr list * type_expr
         (* Take an instance of a type scheme containing free univars *)
 val instance_label:

typing/typecore.ml

@@ -521,7 +521,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
       begin match ty.desc with
       | Tpoly (body, tyl) ->
           begin_def ();
-          let _, ty' = instance_poly false tyl body in
+          let _, ty' = instance_poly ~keep_names:true false tyl body in
           end_def ();
           generalize ty';
           let id = enter_variable loc name ty' in
@@ -2619,7 +2619,8 @@ and type_let env rec_flag spat_sexp_list scope allow =
         let pat =
           match pat.pat_type.desc with
           | Tpoly (ty, tl) ->
-              {pat with pat_type = snd (instance_poly false tl ty)}
+              {pat with pat_type =
+               snd (instance_poly ~keep_names:true false tl ty)}
           | _ -> pat
         in unify_pat env pat (type_approx env sexp))
       pat_list spat_sexp_list;
@@ -2653,7 +2654,7 @@ and type_let env rec_flag spat_sexp_list scope allow =
         | Tpoly (ty, tl) ->
             begin_def ();
             if !Clflags.principal then begin_def ();
-            let vars, ty' = instance_poly true tl ty in
+            let vars, ty' = instance_poly ~keep_names:true true tl ty in
             if !Clflags.principal then begin
               end_def ();
               generalize_structure ty'
@@ -2674,8 +2675,7 @@ and type_let env rec_flag spat_sexp_list scope allow =
          iter_pattern (fun pat -> generalize_expansive env pat.pat_type) pat)
     pat_list exp_list;
   List.iter
-    (fun pat -> iter_pattern
-      (fun pat -> generalize pat.pat_type) pat)
+    (fun pat -> iter_pattern (fun pat -> generalize pat.pat_type) pat)
     pat_list;
   (List.combine pat_list exp_list, new_env, unpacks)