merge branches/gadts-devel

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

49 files changed, 2515 insertions, 883 deletions

diff --git a/boot/ocamlc b/boot/ocamlc
index d29b6b0235..29b2110fde 100755
--- a/boot/ocamlc
+++ b/boot/ocamlc
diff --git a/boot/ocamldep b/boot/ocamldep
index bd7e1f945d..bf492825bc 100755
--- a/boot/ocamldep
+++ b/boot/ocamldep
diff --git a/boot/ocamllex b/boot/ocamllex
index e86d3b1f37..ec5302a3d8 100755
--- a/boot/ocamllex
+++ b/boot/ocamllex
diff --git a/debugger/loadprinter.ml b/debugger/loadprinter.ml
index 49f76a402f..0395cfb307 100644
--- a/debugger/loadprinter.ml
+++ b/debugger/loadprinter.ml
@@ -106,7 +106,7 @@ let match_printer_type desc typename =
   let ty_arg = Ctype.newvar() in
   Ctype.unify Env.empty
     (Ctype.newconstr printer_type [ty_arg])
-    (Ctype.instance desc.val_type);
+    (Ctype.instance Env.empty desc.val_type);
   Ctype.end_def();
   Ctype.generalize ty_arg;
   ty_arg
diff --git a/ocamldoc/Makefile b/ocamldoc/Makefile
index d04809aa31..29704e099e 100644
--- a/ocamldoc/Makefile
+++ b/ocamldoc/Makefile
@@ -152,6 +152,7 @@ OCAMLCMOFILES=$(OCAMLSRCDIR)/parsing/printast.cmo \
 	$(OCAMLSRCDIR)/parsing/parser.cmo \
 	$(OCAMLSRCDIR)/parsing/lexer.cmo \
 	$(OCAMLSRCDIR)/parsing/parse.cmo \
+	$(OCAMLSRCDIR)/typing/unused_var.cmo \
 	$(OCAMLSRCDIR)/typing/types.cmo \
 	$(OCAMLSRCDIR)/typing/path.cmo \
 	$(OCAMLSRCDIR)/typing/btype.cmo \
diff --git a/parsing/parser.mly b/parsing/parser.mly
index f69284d8c8..e3b94667f3 100644
--- a/parsing/parser.mly
+++ b/parsing/parser.mly
@@ -247,17 +247,14 @@ let variables_of_type =
   loop  
 
 let varify_constructors var_names t = 
-  let counter = ref 0 in 
   let offlimits = variables_of_type t in
   let freshly_created = ref [] in
-  let rec fresh () = 
-    let ret = "x" ^ (string_of_int !counter) in 
-    counter := !counter + 1;
-    if List.mem ret offlimits then fresh () 
-    else
-      begin 
-        freshly_created := ret :: !freshly_created;
-        ret end
+  let rec fresh ?(count=0) name =
+    let ret = if count = 0 then name else name ^ string_of_int count in
+    if List.mem ret offlimits then fresh ~count:(count+1) name else begin 
+      freshly_created := ret :: !freshly_created;
+      ret
+    end
   in
   let sofar : (string,string) Hashtbl.t = Hashtbl.create 0 in
   let rec loop t = 
@@ -273,7 +270,7 @@ let varify_constructors var_names t =
 		Ptyp_var (Hashtbl.find sofar s)
 	  with
 	    | Not_found ->
-	      let name = fresh () in 
+	      let name = fresh s in 
 	      Hashtbl.add sofar s name;
 	      Ptyp_var name end
       | Ptyp_constr(longident, lst) ->
@@ -310,6 +307,14 @@ let varify_constructors var_names t =
   in
   (!freshly_created,loop t)
 
+let wrap_type_annotation newtypes core_type body =
+  let exp = mkexp(Pexp_constraint(body,Some core_type,None)) in
+  let exp =
+    List.fold_right (fun newtype exp -> mkexp (Pexp_newtype (newtype, exp)))
+      newtypes exp
+  in
+  let polyvars, core_type = varify_constructors newtypes core_type in
+  (exp, ghtyp(Ptyp_poly(polyvars,core_type)))
 
 %}
 
@@ -819,6 +824,10 @@ concrete_method :
       { $4, $3, $2, ghexp(Pexp_poly ($5, None)), symbol_rloc () }
   | METHOD override_flag private_flag label COLON poly_type EQUAL seq_expr
       { $4, $3, $2, ghexp(Pexp_poly($8,Some $6)), symbol_rloc () }
+  | METHOD override_flag private_flag label COLON TYPE lident_list
+    DOT core_type EQUAL seq_expr
+      { let exp, poly = wrap_type_annotation $7 $9 $11 in
+        $4, $3, $2, ghexp(Pexp_poly(exp, Some poly)), symbol_rloc () }
 ;
 
 /* Class types */
@@ -1177,36 +1186,20 @@ let_bindings:
 ;
 
 lident_list:
-    LIDENT                                 { [$1] }
+    LIDENT                            { [$1] }
   | LIDENT lident_list                { $1 :: $2 }
-
-
+;
+pat_ident:
+    val_ident                         { mkpat (Ppat_var $1) }
+;
 let_binding:
-    val_ident fun_binding
-      { ({ppat_desc = Ppat_var $1; ppat_loc = rhs_loc 1}, $2) }
-  | val_ident COLON typevar_list DOT core_type EQUAL seq_expr
-      { (ghpat(Ppat_constraint({ppat_desc = Ppat_var $1; ppat_loc = rhs_loc 1},
-                               ghtyp(Ptyp_poly($3,$5)))),
-         $7) }
-  | val_ident COLON TYPE lident_list DOT core_type EQUAL seq_expr
-      { 
-	let newtypes = $4 in
-	let core_type = $6 in
-	let exp = mkexp(Pexp_constraint($8,Some core_type,None)) in
-	let rec mk_newtypes = 
-	  function
-	    |[newtype] -> mkexp(Pexp_newtype(newtype,exp))
-	    | newtype :: newtypes ->
-		mkexp(Pexp_newtype(newtype,mk_newtypes newtypes))
-	    | [] -> assert false
-	in
-	let exp = mk_newtypes newtypes in
-	let polyvars, core_type = varify_constructors newtypes core_type in
-	
-	(ghpat(Ppat_constraint({ppat_desc = Ppat_var $1; ppat_loc = rhs_loc 1},
-                               ghtyp(Ptyp_poly(polyvars,core_type)))),
-         exp)
-      }
+    pat_ident fun_binding
+      { ($1, $2) }
+  | pat_ident COLON typevar_list DOT core_type EQUAL seq_expr
+      { (ghpat(Ppat_constraint($1, ghtyp(Ptyp_poly($3,$5)))), $7) }
+  | pat_ident COLON TYPE lident_list DOT core_type EQUAL seq_expr
+      { let exp, poly = wrap_type_annotation $4 $6 $8 in
+	(ghpat(Ppat_constraint($1, poly)), exp) }
   | pattern EQUAL seq_expr
       { ($1, $3) }
 ;
diff --git a/testsuite/tests/typing-gadts/dynamic_frisch.ml b/testsuite/tests/typing-gadts/dynamic_frisch.ml
new file mode 100644
index 0000000000..895be5a05c
--- /dev/null
+++ b/testsuite/tests/typing-gadts/dynamic_frisch.ml
@@ -0,0 +1,475 @@
+(* Encoding generics using GADTs *)
+(* (c) Alain Frisch / Lexifi *)
+(* cf. http://www.lexifi.com/blog/dynamic-types *)
+
+(* Basic tag *)
+
+type 'a ty =
+  | Int: int ty
+  | String: string ty
+  | List: 'a ty -> 'a list ty
+  | Pair: ('a ty * 'b ty) -> ('a * 'b) ty
+;;
+
+(* Tagging data *)
+
+type variant =
+  | VInt of int
+  | VString of string
+  | VList of variant list
+  | VPair of variant * variant
+ 
+let rec variantize: type t. t ty -> t -> variant =
+  fun ty x ->
+    (* type t is abstract here *)
+    match ty with
+    | Int -> VInt x  (* in this branch: t = int *)
+    | String -> VString x (* t = string *)
+    | List ty1 ->
+        VList (List.map (variantize ty1) x)
+        (* t = 'a list for some 'a *)
+    | Pair (ty1, ty2) ->
+        VPair (variantize ty1 (fst x), variantize ty2 (snd x))
+        (* t = ('a, 'b) for some 'a and 'b *)
+ 
+exception VariantMismatch
+ 
+let rec devariantize: type t. t ty -> variant -> t =
+  fun ty v ->
+    match ty, v with
+    | Int, VInt x -> x
+    | String, VString x -> x
+    | List ty1, VList vl ->
+        List.map (devariantize ty1) vl
+    | Pair (ty1, ty2), VPair (x1, x2) ->
+        (devariantize ty1 x1, devariantize ty2 x2)
+    | _ -> raise VariantMismatch
+;;
+
+(* Handling records *)
+
+type 'a ty =
+  | Int: int ty
+  | String: string ty
+  | List: 'a ty -> 'a list ty
+  | Pair: ('a ty * 'b ty) -> ('a * 'b) ty
+  | Record: 'a record -> 'a ty
+ 
+and 'a record =
+    {
+     path: string;
+     fields: 'a field_ list;
+    }
+ 
+and 'a field_ =
+  | Field: ('a, 'b) field -> 'a field_
+ 
+and ('a, 'b) field =
+    {
+     label: string;
+     field_type: 'b ty;
+     get: ('a -> 'b);
+    }
+;;
+
+(* Again *)
+
+type variant =
+  | VInt of int
+  | VString of string
+  | VList of variant list
+  | VPair of variant * variant
+  | VRecord of (string * variant) list
+
+let rec variantize: type t. t ty -> t -> variant =
+  fun ty x ->
+    (* type t is abstract here *)
+    match ty with
+    | Int -> VInt x  (* in this branch: t = int *)
+    | String -> VString x (* t = string *)
+    | List ty1 ->
+        VList (List.map (variantize ty1) x)
+        (* t = 'a list for some 'a *)
+    | Pair (ty1, ty2) ->
+        VPair (variantize ty1 (fst x), variantize ty2 (snd x))
+        (* t = ('a, 'b) for some 'a and 'b *)
+    | Record {fields} ->
+        VRecord
+          (List.map (fun (Field{field_type; label; get}) ->
+                       (label, variantize field_type (get x))) fields)
+;;
+ 
+(* Extraction *)
+
+type 'a ty =
+  | Int: int ty
+  | String: string ty
+  | List: 'a ty -> 'a list ty
+  | Pair: ('a ty * 'b ty) -> ('a * 'b) ty
+  | Record: ('a, 'builder) record -> 'a ty
+ 
+and ('a, 'builder) record =
+    {
+     path: string;
+     fields: ('a, 'builder) field list;
+     create_builder: (unit -> 'builder);
+     of_builder: ('builder -> 'a);
+    }
+ 
+and ('a, 'builder) field =
+  | Field: ('a, 'builder, 'b) field_ -> ('a, 'builder) field
+ 
+and ('a, 'builder, 'b) field_ =
+  {
+   label: string;
+   field_type: 'b ty;
+   get: ('a -> 'b);
+   set: ('builder -> 'b -> unit);
+  }
+ 
+let rec devariantize: type t. t ty -> variant -> t =
+  fun ty v ->
+    match ty, v with
+    | Int, VInt x -> x
+    | String, VString x -> x
+    | List ty1, VList vl ->
+        List.map (devariantize ty1) vl
+    | Pair (ty1, ty2), VPair (x1, x2) ->
+        (devariantize ty1 x1, devariantize ty2 x2)
+    | Record {fields; create_builder; of_builder}, VRecord fl ->
+        if List.length fields <> List.length fl then raise VariantMismatch;
+        let builder = create_builder () in
+        List.iter2
+          (fun (Field {label; field_type; set}) (lab, v) ->
+            if label <> lab then raise VariantMismatch;
+            set builder (devariantize field_type v)
+          )
+          fields fl;
+        of_builder builder
+    | _ -> raise VariantMismatch
+;;
+
+type my_record  =
+    {
+     a: int;
+     b: string list;
+    }
+ 
+let my_record =
+  let fields =
+    [
+     Field {label = "a"; field_type = Int;
+            get = (fun {a} -> a);
+            set = (fun (r, _) x -> r := Some x)};
+     Field {label = "b"; field_type = List String;
+            get = (fun {b} -> b);
+            set = (fun (_, r) x -> r := Some x)};
+    ]
+  in
+  let create_builder () = (ref None, ref None) in
+  let of_builder (a, b) =
+    match !a, !b with
+    | Some a, Some b -> {a; b}
+    | _ -> failwith "Some fields are missing in record of type my_record"
+  in
+  Record {path = "My_module.my_record"; fields; create_builder; of_builder}
+;;
+
+(* Extension to recursive types and polymorphic variants *)
+(* by Jacques Garrigue *)
+
+type noarg = Noarg
+
+type (_,_) ty =
+  | Int: (int,_) ty
+  | String: (string,_) ty
+  | List: ('a,'e) ty -> ('a list, 'e) ty
+  | Option: ('a,'e) ty -> ('a option, 'e) ty
+  | Pair: (('a,'e) ty * ('b,'e) ty) -> ('a * 'b,'e) ty
+  (* Support for type variables and recursive types *)
+  | Var: ('a, 'a -> 'e) ty
+  | Rec: ('a, 'a -> 'e) ty -> ('a,'e) ty
+  | Pop: ('a, 'e) ty -> ('a, 'b -> 'e) ty
+  (* Change the representation of a type *)
+  | Conv: string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
+  (* Sum types (both normal sums and polymorphic variants) *)
+  | Sum: ('a, 'e, 'b) ty_sum -> ('a, 'e) ty
+
+and ('a, 'e, 'b) ty_sum =
+    { sum_proj: 'a -> string * 'e ty_dyn option;
+      sum_cases: (string * ('e,'b) ty_case) list;
+      sum_inj: 'c. ('b,'c) ty_sel * 'c -> 'a; }
+
+and 'e ty_dyn =              (* dynamic type *)
+  | Tdyn : ('a,'e) ty * 'a -> 'e ty_dyn
+
+and (_,_) ty_sel =           (* selector from a list of types *)
+  | Thd : ('a -> 'b, 'a) ty_sel
+  | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel
+
+and (_,_) ty_case =          (* type a sum case *)
+  | TCarg : ('b,'a) ty_sel * ('a,'e) ty -> ('e,'b) ty_case
+  | TCnoarg : ('b,noarg) ty_sel -> ('e,'b) ty_case
+;;
+
+type _ ty_env =              (* type variable substitution *)
+  | Enil : unit ty_env
+  | Econs : ('a,'e) ty * 'e ty_env -> ('a -> 'e) ty_env
+;;
+
+(* Comparing selectors *)
+type (_,_) eq = Eq: ('a,'a) eq
+
+let rec eq_sel : type a b c. (a,b) ty_sel -> (a,c) ty_sel -> (b,c) eq option =
+  fun s1 s2 ->
+    match s1, s2 with
+    | Thd, Thd -> Some Eq
+    | Ttl s1, Ttl s2 ->
+        (match eq_sel s1 s2 with None -> None | Some Eq -> Some Eq)
+    | _ -> None
+
+(* Auxiliary function to get the type of a case from its selector *)
+let rec get_case : type a b e.
+  (b, a) ty_sel -> (string * (e,b) ty_case) list -> string * (a, e) ty option =
+  fun sel cases ->
+  match cases with
+  | (name, TCnoarg sel') :: rem ->
+      begin match eq_sel sel sel' with
+      | None -> get_case sel rem
+      | Some Eq -> name, None
+      end
+  | (name, TCarg (sel', ty)) :: rem ->
+      begin match eq_sel sel sel' with
+      | None -> get_case sel rem
+      | Some Eq -> name, Some ty
+      end
+  | [] -> raise Not_found
+;;
+
+(* Untyped representation of values *)
+type variant =
+  | VInt of int
+  | VString of string
+  | VList of variant list
+  | VOption of variant option
+  | VPair of variant * variant
+  | VConv of string * variant
+  | VSum of string * variant option
+
+let may_map f = function Some x -> Some (f x) | None -> None
+
+let rec variantize : type a e. e ty_env -> (a,e) ty -> a -> variant =
+  fun e ty v ->
+  match ty with
+  | Int -> VInt v
+  | String -> VString v
+  | List t -> VList (List.map (variantize e t) v)
+  | Option t -> VOption (may_map (variantize e t) v)
+  | Pair (t1, t2) -> VPair (variantize e t1 (fst v), variantize e t2 (snd v))
+  | Rec t -> variantize (Econs (ty, e)) t v
+  | Pop t -> (match e with Econs (_, e') -> variantize e' t v)
+  | Var -> (match e with Econs (t, e') -> variantize e' t v)
+  | Conv (s, proj, inj, t) -> VConv (s, variantize e t (proj v))
+  | Sum ops ->
+      let tag, arg = ops.sum_proj v in
+      VSum (tag, may_map (function Tdyn (ty,arg) -> variantize e ty arg) arg)
+;;
+
+let rec devariantize : type t e. e ty_env -> (t, e) ty -> variant -> t =
+  fun e ty v ->
+  match ty, v with
+  | Int, VInt x -> x
+  | String, VString x -> x
+  | List ty1, VList vl ->
+      List.map (devariantize e ty1) vl
+  | Pair (ty1, ty2), VPair (x1, x2) ->
+      (devariantize e ty1 x1, devariantize e ty2 x2)
+  | Rec t, _ -> devariantize (Econs (ty, e)) t v
+  | Pop t, _ -> (match e with Econs (_, e') -> devariantize e' t v)
+  | Var, _ -> (match e with Econs (t, e') -> devariantize e' t v)
+  | Conv (s, proj, inj, t), VConv (s', v) when s = s' ->
+      inj (devariantize e t v)
+  | Sum ops, VSum (tag, a) ->
+      begin try match List.assoc tag ops.sum_cases, a with
+      | TCarg (sel, t), Some a -> ops.sum_inj (sel, devariantize e t a)
+      | TCnoarg sel, None -> ops.sum_inj (sel, Noarg)
+      | _ -> raise VariantMismatch
+      with Not_found -> raise VariantMismatch
+      end
+  | _ -> raise VariantMismatch
+;;
+
+(* First attempt: represent 1-constructor variants using Conv *)
+let wrap_A t = Conv ("`A", (fun (`A x) -> x), (fun x -> `A x), t);;
+
+let ty a = Rec (wrap_A (Option (Pair (a, Var)))) ;;
+let v = variantize Enil (ty Int);;
+let x = v (`A (Some (1, `A (Some (2, `A None))))) ;;
+
+(* Can also use it to decompose a tuple *)
+
+let triple t1 t2 t3 =
+  Conv ("Triple", (fun (a,b,c) -> (a,(b,c))),
+        (fun (a,(b,c)) -> (a,b,c)), Pair (t1, Pair (t2, t3)))
+
+let v = variantize Enil (triple String Int Int) ("A", 2, 3) ;;
+
+(* Second attempt: introduce a real sum construct *)
+let ty_abc =
+  (* Could also use [get_case] for proj, but direct definition is shorter *)
+  let proj = function
+      `A n -> "A", Some (Tdyn (Int, n))
+    | `B s -> "B", Some (Tdyn (String, s))
+    | `C   -> "C", None
+  (* Define inj in advance to be able to write the type annotation easily *)
+  and inj : type c. (int -> string -> noarg -> unit, c) ty_sel * c ->
+    [`A of int | `B of string | `C] = function
+        Thd, v -> `A v
+      | Ttl Thd, v -> `B v
+      | Ttl (Ttl Thd), Noarg -> `C
+  in
+  (* Coherence of sum_inj and sum_cases is checked by the typing *)
+  Sum { sum_proj = proj; sum_inj = inj; sum_cases =
+        [ "A", TCarg (Thd, Int); "B", TCarg (Ttl Thd, String);
+          "C", TCnoarg (Ttl (Ttl Thd)) ] }
+;;
+
+let v = variantize Enil ty_abc (`A 3)
+let a = devariantize Enil ty_abc v
+
+(* And an example with recursion... *)
+type 'a vlist = [`Nil | `Cons of 'a * 'a vlist]
+
+let ty_list : type a e. (a, e) ty -> (a vlist, e) ty = fun t ->
+  let tcons = Pair (Pop t, Var) in
+  Rec (Sum {
+       sum_proj = (function
+           `Nil -> "Nil", None
+         | `Cons p -> "Cons", Some (Tdyn (tcons, p)));
+       sum_cases = ["Nil", TCnoarg Thd; "Cons", TCarg (Ttl Thd, tcons)];
+       sum_inj = fun (type c) ->
+         (function
+         | Thd, Noarg -> `Nil
+         | Ttl Thd, v -> `Cons v
+         : (noarg -> a * a vlist -> unit, c) ty_sel * c -> a vlist)
+         (* One can also write the type annotation directly *)
+     })
+
+let v = variantize Enil (ty_list Int) (`Cons (1, `Cons (2, `Nil))) ;;
+
+
+(* Simpler but weaker approach *)
+
+type (_,_) ty =
+  | Int: (int,_) ty
+  | String: (string,_) ty
+  | List: ('a,'e) ty -> ('a list, 'e) ty
+  | Option: ('a,'e) ty -> ('a option, 'e) ty
+  | Pair: (('a,'e) ty * ('b,'e) ty) -> ('a * 'b,'e) ty
+  | Var: ('a, 'a -> 'e) ty
+  | Rec: ('a, 'a -> 'e) ty -> ('a,'e) ty
+  | Pop: ('a, 'e) ty -> ('a, 'b -> 'e) ty
+  | Conv: string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
+  | Sum: ('a -> string * 'e ty_dyn option) * (string * 'e ty_dyn option -> 'a)
+             -> ('a, 'e) ty
+and 'e ty_dyn =
+  | Tdyn : ('a,'e) ty * 'a -> 'e ty_dyn
+
+let ty_abc : ([`A of int | `B of string | `C],'e) ty =
+  (* Could also use [get_case] for proj, but direct definition is shorter *)
+  Sum (
+  (function
+      `A n -> "A", Some (Tdyn (Int, n))
+    | `B s -> "B", Some (Tdyn (String, s))
+    | `C   -> "C", None),
+  (function
+      "A", Some (Tdyn (Int, n)) -> `A n
+    | "B", Some (Tdyn (String, s)) -> `B s
+    | "C", None -> `C
+    | _ -> invalid_arg "ty_abc"))
+;;
+
+(* Breaks: no way to pattern-match on a full recursive type *)
+let ty_list : type a e. (a,e) ty -> (a vlist,e) ty = fun t ->
+  let targ = Pair (Pop t, Var) in
+  Rec (Sum (
+  (function `Nil -> "Nil", None
+    | `Cons p -> "Cons", Some (Tdyn (targ, p))),
+  (function "Nil", None -> `Nil
+    | "Cons", Some (Tdyn (Pair (_, Var), (p : a * a vlist))) -> `Cons p)))
+;;
+
+(* Define Sum using object instead of record for first-class polymorphism *)
+
+type (_,_) ty =
+  | Int: (int,_) ty
+  | String: (string,_) ty
+  | List: ('a,'e) ty -> ('a list, 'e) ty
+  | Option: ('a,'e) ty -> ('a option, 'e) ty
+  | Pair: (('a,'e) ty * ('b,'e) ty) -> ('a * 'b,'e) ty
+  | Var: ('a, 'a -> 'e) ty
+  | Rec: ('a, 'a -> 'e) ty -> ('a,'e) ty
+  | Pop: ('a, 'e) ty -> ('a, 'b -> 'e) ty
+  | Conv: string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
+  | Sum: < proj: 'a -> string * 'e ty_dyn option;
+           cases: (string * ('e,'b) ty_case) list;
+           inj: 'c. ('b,'c) ty_sel * 'c -> 'a >
+          -> ('a, 'e) ty
+
+and 'e ty_dyn =
+  | Tdyn : ('a,'e) ty * 'a -> 'e ty_dyn
+
+and (_,_) ty_sel =
+  | Thd : ('a -> 'b, 'a) ty_sel
+  | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel
+
+and (_,_) ty_case =
+  | TCarg : ('b,'a) ty_sel * ('a,'e) ty -> ('e,'b) ty_case
+  | TCnoarg : ('b,noarg) ty_sel -> ('e,'b) ty_case
+;;
+
+let ty_abc : ([`A of int | `B of string | `C] as 'a, 'e) ty =
+  Sum (object
+    method proj = function
+        `A n -> "A", Some (Tdyn (Int, n))
+      | `B s -> "B", Some (Tdyn (String, s))
+      | `C -> "C", None
+    method cases =
+      [ "A", TCarg (Thd, Int); "B", TCarg (Ttl Thd, String);
+        "C", TCnoarg (Ttl (Ttl Thd)) ];
+    method inj : type c.
+        (int -> string -> noarg -> unit, c) ty_sel * c ->
+          [`A of int | `B of string | `C] =
+      function
+        Thd, v -> `A v
+      | Ttl Thd, v -> `B v
+      | Ttl (Ttl Thd), Noarg -> `C
+      | _ -> assert false
+  end)
+
+type 'a vlist = [`Nil | `Cons of 'a * 'a vlist]
+
+let ty_list : type a e. (a, e) ty -> (a vlist, e) ty = fun t ->
+  let tcons = Pair (Pop t, Var) in
+  Rec (Sum (object
+    method proj = function
+        `Nil -> "Nil", None
+      | `Cons p -> "Cons", Some (Tdyn (tcons, p))
+    method cases = ["Nil", TCnoarg Thd; "Cons", TCarg (Ttl Thd, tcons)]
+    method inj : type c.(noarg -> a * a vlist -> unit, c) ty_sel * c -> a vlist
+    = function
+      | Thd, Noarg -> `Nil
+      | Ttl Thd, v -> `Cons v
+  end))
+;;
+
+(*
+type (_,_) ty_assoc =
+  | Anil : (unit,'e) ty_assoc
+  | Acons : string * ('a,'e) ty * ('b,'e) ty_assoc -> ('a -> 'b, 'e) ty_assoc
+
+and (_,_) ty_pvar =
+  | Pnil : ('a,'e) ty_pvar
+  | Pconst : 't * ('b,'e) ty_pvar -> ('t -> 'b, 'e) ty_pvar
+  | Parg : 't * ('a,'e) ty * ('b,'e) ty_pvar -> ('t * 'a -> 'b, 'e) ty_pvar
+*)
diff --git a/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference b/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference
new file mode 100644
index 0000000000..dda0a0fa7d
--- /dev/null
+++ b/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference
@@ -0,0 +1,176 @@
+
+#                       type 'a ty =
+    Int : int ty
+  | String : string ty
+  | List : 'a ty -> 'a list ty
+  | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
+#                                                                     type variant =
+    VInt of int
+  | VString of string
+  | VList of variant list
+  | VPair of variant * variant
+val variantize : 'a ty -> 'a -> variant = <fun>
+exception VariantMismatch
+val devariantize : 'a ty -> variant -> 'a = <fun>
+#                                                   type 'a ty =
+    Int : int ty
+  | String : string ty
+  | List : 'a ty -> 'a list ty
+  | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
+  | Record : 'a record -> 'a ty
+and 'a record = { path : string; fields : 'a field_ list; }
+and 'a field_ = Field : ('a, 'b) field -> 'a field_
+and ('a, 'b) field = { label : string; field_type : 'b ty; get : 'a -> 'b; }
+#                                                     type variant =
+    VInt of int
+  | VString of string
+  | VList of variant list
+  | VPair of variant * variant
+  | VRecord of (string * variant) list
+val variantize : 'a ty -> 'a -> variant = <fun>
+#                                                                                                   type 'a ty =
+    Int : int ty
+  | String : string ty
+  | List : 'a ty -> 'a list ty
+  | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
+  | Record : ('a, 'builder) record -> 'a ty
+and ('a, 'builder) record = {
+  path : string;
+  fields : ('a, 'builder) field list;
+  create_builder : unit -> 'builder;
+  of_builder : 'builder -> 'a;
+}
+and ('a, 'builder) field =
+    Field : ('a, 'builder, 'b) field_ -> ('a, 'builder) field
+and ('a, 'builder, 'b) field_ = {
+  label : string;
+  field_type : 'b ty;
+  get : 'a -> 'b;
+  set : 'builder -> 'b -> unit;
+}
+val devariantize : 'a ty -> variant -> 'a = <fun>
+#                                                   type my_record = { a : int; b : string list; }
+val my_record : my_record ty =
+  Record
+   {path = "My_module.my_record";
+    fields =
+     [Field {label = "a"; field_type = Int; get = <fun>; set = <fun>};
+      Field {label = "b"; field_type = List String; get = <fun>; set = <fun>}];
+    create_builder = <fun>; of_builder = <fun>}
+#                                                                         type noarg = Noarg
+type ('a, 'b) ty =
+    Int : (int, 'c) ty
+  | String : (string, 'd) ty
+  | List : ('a, 'e) ty -> ('a list, 'e) ty
+  | Option : ('a, 'e) ty -> ('a option, 'e) ty
+  | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty
+  | Var : ('a, 'a -> 'e) ty
+  | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty
+  | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty
+  | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
+  | Sum : ('a, 'e, 'b) ty_sum -> ('a, 'e) ty
+and ('a, 'e, 'b) ty_sum = {
+  sum_proj : 'a -> string * 'e ty_dyn option;
+  sum_cases : (string * ('e, 'b) ty_case) list;
+  sum_inj : 'c. ('b, 'c) ty_sel * 'c -> 'a;
+}
+and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn
+and ('a, 'b) ty_sel =
+    Thd : ('a -> 'b, 'a) ty_sel
+  | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel
+and ('a, 'b) ty_case =
+    TCarg : ('b, 'a) ty_sel * ('a, 'e) ty -> ('e, 'b) ty_case
+  | TCnoarg : ('b, noarg) ty_sel -> ('e, 'b) ty_case
+#         type 'a ty_env =
+    Enil : unit ty_env
+  | Econs : ('a, 'e) ty * 'e ty_env -> ('a -> 'e) ty_env
+#                                                         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>
+#                                                         type variant =
+    VInt of int
+  | VString of string
+  | VList of variant list
+  | VOption of variant option
+  | VPair of variant * variant
+  | 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 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>
+# val v : ([ `A of (int * 'a) option ] as 'a) -> variant = <fun>
+# val x : variant =
+  VConv ("`A",
+   VOption
+    (Some
+      (VPair (VInt 1,
+        VConv ("`A",
+         VOption (Some (VPair (VInt 2, VConv ("`A", VOption None)))))))))
+#               val triple :
+  ('a, 'b) ty -> ('c, 'b) ty -> ('d, 'b) ty -> ('a * 'c * 'd, 'b) ty = <fun>
+val v : variant =
+  VConv ("Triple", VPair (VString "A", VPair (VInt 2, VInt 3)))
+#                                       val ty_abc : ([ `A of int | `B of string | `C ], 'a) ty =
+  Sum
+   {sum_proj = <fun>;
+    sum_cases =
+     [("A", TCarg (Thd, Int)); ("B", TCarg (Ttl Thd, String));
+      ("C", TCnoarg (Ttl (Ttl Thd)))];
+    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 v : variant =
+  VSum ("Cons",
+   Some
+    (VPair (VInt 1, VSum ("Cons", Some (VPair (VInt 2, VSum ("Nil", None)))))))
+#                                                               type ('a, 'b) ty =
+    Int : (int, 'c) ty
+  | String : (string, 'd) ty
+  | List : ('a, 'e) ty -> ('a list, 'e) ty
+  | Option : ('a, 'e) ty -> ('a option, 'e) ty
+  | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty
+  | Var : ('a, 'a -> 'e) ty
+  | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty
+  | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty
+  | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
+  | Sum : ('a -> string * 'e ty_dyn option) *
+      (string * 'e ty_dyn option -> 'a) -> ('a, 'e) ty
+and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn
+val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum (<fun>, <fun>)
+#                   Characters 327-344:
+      | "Cons", Some (Tdyn (Pair (_, Var), (p : a * a vlist))) -> `Cons p)))
+                                           ^^^^^^^^^^^^^^^^^
+Error: This pattern matches values of type a * a vlist
+       but a pattern was expected which matches values of type
+         ex#42 = ex#43 * ex#44
+#                                                         type ('a, 'b) ty =
+    Int : (int, 'd) ty
+  | String : (string, 'f) ty
+  | List : ('a, 'e) ty -> ('a list, 'e) ty
+  | Option : ('a, 'e) ty -> ('a option, 'e) ty
+  | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty
+  | Var : ('a, 'a -> 'e) ty
+  | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty
+  | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty
+  | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
+  | Sum :
+      < cases : (string * ('e, 'b) ty_case) list;
+        inj : 'c. ('b, 'c) ty_sel * 'c -> 'a;
+        proj : 'a -> string * 'e ty_dyn option > -> ('a, 'e) ty
+and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn
+and ('a, 'b) ty_sel =
+    Thd : ('a -> 'b, 'a) ty_sel
+  | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel
+and ('a, 'b) ty_case =
+    TCarg : ('b, 'a) ty_sel * ('a, 'e) ty -> ('e, '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>
+#   * * * * * * * * *   
diff --git a/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference b/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference
new file mode 100644
index 0000000000..dda0a0fa7d
--- /dev/null
+++ b/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference
@@ -0,0 +1,176 @@
+
+#                       type 'a ty =
+    Int : int ty
+  | String : string ty
+  | List : 'a ty -> 'a list ty
+  | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
+#                                                                     type variant =
+    VInt of int
+  | VString of string
+  | VList of variant list
+  | VPair of variant * variant
+val variantize : 'a ty -> 'a -> variant = <fun>
+exception VariantMismatch
+val devariantize : 'a ty -> variant -> 'a = <fun>
+#                                                   type 'a ty =
+    Int : int ty
+  | String : string ty
+  | List : 'a ty -> 'a list ty
+  | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
+  | Record : 'a record -> 'a ty
+and 'a record = { path : string; fields : 'a field_ list; }
+and 'a field_ = Field : ('a, 'b) field -> 'a field_
+and ('a, 'b) field = { label : string; field_type : 'b ty; get : 'a -> 'b; }
+#                                                     type variant =
+    VInt of int
+  | VString of string
+  | VList of variant list
+  | VPair of variant * variant
+  | VRecord of (string * variant) list
+val variantize : 'a ty -> 'a -> variant = <fun>
+#                                                                                                   type 'a ty =
+    Int : int ty
+  | String : string ty
+  | List : 'a ty -> 'a list ty
+  | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
+  | Record : ('a, 'builder) record -> 'a ty
+and ('a, 'builder) record = {
+  path : string;
+  fields : ('a, 'builder) field list;
+  create_builder : unit -> 'builder;
+  of_builder : 'builder -> 'a;
+}
+and ('a, 'builder) field =
+    Field : ('a, 'builder, 'b) field_ -> ('a, 'builder) field
+and ('a, 'builder, 'b) field_ = {
+  label : string;
+  field_type : 'b ty;
+  get : 'a -> 'b;
+  set : 'builder -> 'b -> unit;
+}
+val devariantize : 'a ty -> variant -> 'a = <fun>
+#                                                   type my_record = { a : int; b : string list; }
+val my_record : my_record ty =
+  Record
+   {path = "My_module.my_record";
+    fields =
+     [Field {label = "a"; field_type = Int; get = <fun>; set = <fun>};
+      Field {label = "b"; field_type = List String; get = <fun>; set = <fun>}];
+    create_builder = <fun>; of_builder = <fun>}
+#                                                                         type noarg = Noarg
+type ('a, 'b) ty =
+    Int : (int, 'c) ty
+  | String : (string, 'd) ty
+  | List : ('a, 'e) ty -> ('a list, 'e) ty
+  | Option : ('a, 'e) ty -> ('a option, 'e) ty
+  | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty
+  | Var : ('a, 'a -> 'e) ty
+  | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty
+  | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty
+  | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
+  | Sum : ('a, 'e, 'b) ty_sum -> ('a, 'e) ty
+and ('a, 'e, 'b) ty_sum = {
+  sum_proj : 'a -> string * 'e ty_dyn option;
+  sum_cases : (string * ('e, 'b) ty_case) list;
+  sum_inj : 'c. ('b, 'c) ty_sel * 'c -> 'a;
+}
+and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn
+and ('a, 'b) ty_sel =
+    Thd : ('a -> 'b, 'a) ty_sel
+  | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel
+and ('a, 'b) ty_case =
+    TCarg : ('b, 'a) ty_sel * ('a, 'e) ty -> ('e, 'b) ty_case
+  | TCnoarg : ('b, noarg) ty_sel -> ('e, 'b) ty_case
+#         type 'a ty_env =
+    Enil : unit ty_env
+  | Econs : ('a, 'e) ty * 'e ty_env -> ('a -> 'e) ty_env
+#                                                         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>
+#                                                         type variant =
+    VInt of int
+  | VString of string
+  | VList of variant list
+  | VOption of variant option
+  | VPair of variant * variant
+  | 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 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>
+# val v : ([ `A of (int * 'a) option ] as 'a) -> variant = <fun>
+# val x : variant =
+  VConv ("`A",
+   VOption
+    (Some
+      (VPair (VInt 1,
+        VConv ("`A",
+         VOption (Some (VPair (VInt 2, VConv ("`A", VOption None)))))))))
+#               val triple :
+  ('a, 'b) ty -> ('c, 'b) ty -> ('d, 'b) ty -> ('a * 'c * 'd, 'b) ty = <fun>
+val v : variant =
+  VConv ("Triple", VPair (VString "A", VPair (VInt 2, VInt 3)))
+#                                       val ty_abc : ([ `A of int | `B of string | `C ], 'a) ty =
+  Sum
+   {sum_proj = <fun>;
+    sum_cases =
+     [("A", TCarg (Thd, Int)); ("B", TCarg (Ttl Thd, String));
+      ("C", TCnoarg (Ttl (Ttl Thd)))];
+    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 v : variant =
+  VSum ("Cons",
+   Some
+    (VPair (VInt 1, VSum ("Cons", Some (VPair (VInt 2, VSum ("Nil", None)))))))
+#                                                               type ('a, 'b) ty =
+    Int : (int, 'c) ty
+  | String : (string, 'd) ty
+  | List : ('a, 'e) ty -> ('a list, 'e) ty
+  | Option : ('a, 'e) ty -> ('a option, 'e) ty
+  | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty
+  | Var : ('a, 'a -> 'e) ty
+  | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty
+  | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty
+  | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
+  | Sum : ('a -> string * 'e ty_dyn option) *
+      (string * 'e ty_dyn option -> 'a) -> ('a, 'e) ty
+and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn
+val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum (<fun>, <fun>)
+#                   Characters 327-344:
+      | "Cons", Some (Tdyn (Pair (_, Var), (p : a * a vlist))) -> `Cons p)))
+                                           ^^^^^^^^^^^^^^^^^
+Error: This pattern matches values of type a * a vlist
+       but a pattern was expected which matches values of type
+         ex#42 = ex#43 * ex#44
+#                                                         type ('a, 'b) ty =
+    Int : (int, 'd) ty
+  | String : (string, 'f) ty
+  | List : ('a, 'e) ty -> ('a list, 'e) ty
+  | Option : ('a, 'e) ty -> ('a option, 'e) ty
+  | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty
+  | Var : ('a, 'a -> 'e) ty
+  | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty
+  | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty
+  | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty
+  | Sum :
+      < cases : (string * ('e, 'b) ty_case) list;
+        inj : 'c. ('b, 'c) ty_sel * 'c -> 'a;
+        proj : 'a -> string * 'e ty_dyn option > -> ('a, 'e) ty
+and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn
+and ('a, 'b) ty_sel =
+    Thd : ('a -> 'b, 'a) ty_sel
+  | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel
+and ('a, 'b) ty_case =
+    TCarg : ('b, 'a) ty_sel * ('a, 'e) ty -> ('e, '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>
+#   * * * * * * * * *   
diff --git a/testsuite/tests/typing-gadts/omega07.ml b/testsuite/tests/typing-gadts/omega07.ml
index 22f67d99a6..cddfe460bb 100644
--- a/testsuite/tests/typing-gadts/omega07.ml
+++ b/testsuite/tests/typing-gadts/omega07.ml
@@ -138,6 +138,8 @@ let rec summandLessThanSum : type a b c. (a,b,c) plus -> (a,c) le = fun p ->
 
 type (_,_) equal = Eq : ('a,'a) equal
 
+let convert : type a b. (a,b) equal -> a -> b = fun Eq x -> x
+
 let rec sameNat : type a b. a nat -> b nat -> (a,b) equal option = fun a b ->
   match a, b with
   | NZ, NZ -> Some Eq
diff --git a/testsuite/tests/typing-gadts/omega07.ml.principal.reference b/testsuite/tests/typing-gadts/omega07.ml.principal.reference
index d8cd31f2ce..60ef06cb35 100644
--- a/testsuite/tests/typing-gadts/omega07.ml.principal.reference
+++ b/testsuite/tests/typing-gadts/omega07.ml.principal.reference
@@ -51,7 +51,8 @@ val even2 : two even = EvenSS EvenZ
 val even4 : four even = EvenSS (EvenSS EvenZ)
 #   val p1 : (two, one, three) plus = PlusS (PlusS (PlusZ (NS NZ)))
 #         val summandLessThanSum : ('a, 'b, 'c) plus -> ('a, 'c) le = <fun>
-#                             type ('a, 'b) equal = Eq : ('a, 'a) equal
+#                                 type ('a, 'b) equal = Eq : ('a, 'a) equal
+val convert : ('a, 'b) equal -> 'a -> 'b = <fun>
 val sameNat : 'a nat -> 'b nat -> ('a, 'b) equal option = <fun>
 #             val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun>
 #   type ('a, 'b) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff
diff --git a/testsuite/tests/typing-gadts/omega07.ml.reference b/testsuite/tests/typing-gadts/omega07.ml.reference
index d8cd31f2ce..60ef06cb35 100644
--- a/testsuite/tests/typing-gadts/omega07.ml.reference
+++ b/testsuite/tests/typing-gadts/omega07.ml.reference
@@ -51,7 +51,8 @@ val even2 : two even = EvenSS EvenZ
 val even4 : four even = EvenSS (EvenSS EvenZ)
 #   val p1 : (two, one, three) plus = PlusS (PlusS (PlusZ (NS NZ)))
 #         val summandLessThanSum : ('a, 'b, 'c) plus -> ('a, 'c) le = <fun>
-#                             type ('a, 'b) equal = Eq : ('a, 'a) equal
+#                                 type ('a, 'b) equal = Eq : ('a, 'a) equal
+val convert : ('a, 'b) equal -> 'a -> 'b = <fun>
 val sameNat : 'a nat -> 'b nat -> ('a, 'b) equal option = <fun>
 #             val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun>
 #   type ('a, 'b) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff
diff --git a/testsuite/tests/typing-gadts/term-conv.ml b/testsuite/tests/typing-gadts/term-conv.ml
new file mode 100644
index 0000000000..9b53cd6ea8
--- /dev/null
+++ b/testsuite/tests/typing-gadts/term-conv.ml
@@ -0,0 +1,139 @@
+(* HOAS to de Bruijn, by chak *)
+(* http://www.cse.unsw.edu.au/~chak/haskell/term-conv/ *)
+
+module Typeable = struct
+  type 'a ty =
+    | Int: int ty
+    | String: string ty
+    | List: 'a ty -> 'a list ty
+    | Pair: ('a ty * 'b ty) -> ('a * 'b) ty
+    | Fun: ('a ty * 'b ty) -> ('a -> 'b) ty
+
+  type (_,_) eq = Eq : ('a,'a) eq
+
+  exception CastFailure
+  let rec check_eq : type t t'. t ty -> t' ty -> (t,t') eq = fun t t' ->
+    match t, t' with
+    | Int, Int -> Eq
+    | String, String -> Eq
+    | List t, List t' -> (match check_eq t t' with Eq -> Eq)
+    | Pair (t1,t2), Pair (t1',t2') ->
+        (match check_eq t1 t1', check_eq t2 t2' with Eq, Eq -> Eq)
+    | Fun (t1,t2), Fun (t1',t2') ->
+        (match check_eq t1 t1', check_eq t2 t2' with Eq, Eq -> Eq)
+    | _ -> raise CastFailure
+
+  let gcast : type t t'. t ty -> t' ty -> t -> t' = fun t t' x ->
+    match check_eq t t' with Eq -> x
+end;;
+
+module HOAS = struct
+  open Typeable
+
+  type _ term =
+    | Tag : 't ty * int -> 't term
+    | Con : 't -> 't term
+    | Lam : 's ty * ('s term -> 't term) -> ('s -> 't) term
+    | App : ('s -> 't) term * 's term -> 't term
+
+  let rec intp : type t. t term -> t = function
+    | Tag (_, ix) -> failwith "HOAS.intp"
+    | Con v      -> v
+    | Lam (_, f) -> fun x -> intp (f (Con x))
+    | App (f, a) -> intp f (intp a)
+end;;
+
+module DeBruijn = struct
+  type ('env,'t) ix =
+    | ZeroIx : ('env * 't, 't) ix
+    | SuccIx : ('env,'t) ix -> ('env * 's, 't) ix
+
+  let rec to_int : type env t. (env,t) ix -> int = function
+    | ZeroIx   -> 0
+    | SuccIx n -> to_int n + 1
+
+  type ('env,'t) term =
+    | Var : ('env,'t) ix -> ('env,'t) term
+    | Con : 't -> ('env,'t) term
+    | Lam : ('env * 's, 't) term -> ('env, 's -> 't) term
+    | App : ('env, 's -> 't) term * ('env, 's) term -> ('env, 't) term
+
+  type _ stack =
+    | Empty : unit stack
+    | Push : 'env stack * 't -> ('env * 't) stack
+
+  let rec prj : type env t. (env,t) ix -> env stack -> t = fun i s ->
+    match i, s with
+    | ZeroIx, Push (s,v) -> v
+    | SuccIx i, Push (s,_) -> prj i s
+
+  let rec intp : type env t. (env,t) term -> env stack -> t = fun t s ->
+    match t with
+    | Var ix -> prj ix s
+    | Con v  -> v
+    | Lam b  -> fun x -> intp b (Push (s, x))
+    | App(f,a) -> intp f s (intp a s)
+end;;
+
+module Convert = struct
+  type (_,_) layout =
+    | EmptyLayout : ('env, unit) layout
+    | PushLayout  :
+        't Typeable.ty * ('env,'env') layout * ('env,'t) DeBruijn.ix
+           -> ('env,'env' * 't) layout
+
+  let rec size : type env env'. (env,env') layout -> int = function
+    | EmptyLayout -> 0
+    | PushLayout (_, lyt, _) -> size lyt + 1
+
+  let rec inc : type env env'. (env,env') layout -> (env * 't, env') layout =
+    function
+      | EmptyLayout -> EmptyLayout
+      | PushLayout (t, lyt, ix) -> PushLayout (t, inc lyt, DeBruijn.SuccIx ix)
+
+  let rec prj : type env env' t.
+        t Typeable.ty -> int -> (env,env') layout -> (env,t) DeBruijn.ix
+    = fun t n -> function
+      | EmptyLayout -> failwith "Convert.prj: internal error"
+      | PushLayout (t', l, ix) ->
+          if n = 0 then
+            match Typeable.check_eq t t' with Typeable.Eq -> ix
+          else prj t (n-1) l
+
+  let rec cvt :
+    type env t. (env,env) layout -> t HOAS.term -> (env,t) DeBruijn.term =
+    fun lyt -> function
+      | HOAS.Tag (t, sz) -> DeBruijn.Var (prj t (size lyt - sz -1) lyt)
+      | HOAS.Con v -> DeBruijn.Con v
+      | HOAS.Lam (t, f) ->
+          let lyt' = PushLayout (t, inc lyt, DeBruijn.ZeroIx) in
+          DeBruijn.Lam (cvt lyt' (f (HOAS.Tag (t, size lyt))))
+      | HOAS.App (f, a) ->
+          DeBruijn.App (cvt lyt f, cvt lyt a)
+
+  let convert t = cvt EmptyLayout t
+end;;
+
+module Main = struct
+  open HOAS
+  let i t = Lam (t, fun x -> x)
+  let zero t = Lam (Typeable.Fun(t,t), fun f -> Lam(t, fun x -> x))
+  let one t = Lam (Typeable.Fun(t,t), fun f -> Lam(t, fun x -> App (f, x)))
+  let two t =
+    Lam (Typeable.Fun(t,t), fun f -> Lam(t, fun x -> App (f, App (f, x))))
+  let three t =
+    Lam (Typeable.Fun(t,t),
+         fun f -> Lam(t, fun x -> App (f, App (f, App (f, x)))))
+  let plus t =
+    let t1 = Typeable.Fun(t,t) in let t2 = Typeable.Fun(t1,t1) in
+    Lam (t2, fun m -> Lam (t2, fun n ->
+      Lam (t1, fun f -> Lam(t, fun x -> App(App(m,f), App(App(n,f),x))))))
+
+  let plus_2_3 t = App (App (plus t, two t), three t)
+
+  open Convert
+
+  let i' = convert (i Typeable.Int)
+  let plus_2_3' = convert (plus_2_3 Typeable.Int)
+  let eval_plus_2_3' = DeBruijn.intp plus_2_3' DeBruijn.Empty succ 0
+end;;
diff --git a/testsuite/tests/typing-gadts/term-conv.ml.principal.reference b/testsuite/tests/typing-gadts/term-conv.ml.principal.reference
new file mode 100644
index 0000000000..3c6b335f67
--- /dev/null
+++ b/testsuite/tests/typing-gadts/term-conv.ml.principal.reference
@@ -0,0 +1,71 @@
+
+#                                                       module Typeable :
+  sig
+    type 'a ty =
+        Int : int ty
+      | String : string ty
+      | List : 'a ty -> 'a list ty
+      | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
+      | 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
+  end
+#                               module HOAS :
+  sig
+    type 'a term =
+        Tag : 't Typeable.ty * int -> 't term
+      | 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
+  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
+    type ('env, 't) term =
+        Var : ('env, 't) ix -> ('env, 't) term
+      | Con : 't -> ('env, 't) term
+      | Lam : ('env * 's, 't) term -> ('env, 's -> 't) term
+      | App : ('env, 's -> 't) term * ('env, 's) term -> ('env, 't) term
+    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
+  end
+#                                                                             module Convert :
+  sig
+    type ('a, 'b) layout =
+        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 prj :
+      'a Typeable.ty -> int -> ('b, 'c) layout -> ('b, 'a) DeBruijn.ix
+    val cvt : ('a, 'a) layout -> 'b HOAS.term -> ('a, 'b) DeBruijn.term
+    val convert : 'a HOAS.term -> (unit, 'a) DeBruijn.term
+  end
+#                                               module Main :
+  sig
+    val i : 'a Typeable.ty -> ('a -> 'a) HOAS.term
+    val zero : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
+    val one : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
+    val two : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
+    val three : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
+    val plus :
+      'a Typeable.ty ->
+      ((('a -> 'a) -> 'a -> 'a) ->
+       (('a -> 'a) -> 'a -> 'a) -> ('a -> 'a) -> 'a -> 'a)
+      HOAS.term
+    val plus_2_3 : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
+    val i' : (unit, int -> int) DeBruijn.term
+    val plus_2_3' : (unit, (int -> int) -> int -> int) DeBruijn.term
+    val eval_plus_2_3' : int
+  end
+# 
diff --git a/testsuite/tests/typing-gadts/term-conv.ml.reference b/testsuite/tests/typing-gadts/term-conv.ml.reference
new file mode 100644
index 0000000000..3c6b335f67
--- /dev/null
+++ b/testsuite/tests/typing-gadts/term-conv.ml.reference
@@ -0,0 +1,71 @@
+
+#                                                       module Typeable :
+  sig
+    type 'a ty =
+        Int : int ty
+      | String : string ty
+      | List : 'a ty -> 'a list ty
+      | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
+      | 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
+  end
+#                               module HOAS :
+  sig
+    type 'a term =
+        Tag : 't Typeable.ty * int -> 't term
+      | 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
+  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
+    type ('env, 't) term =
+        Var : ('env, 't) ix -> ('env, 't) term
+      | Con : 't -> ('env, 't) term
+      | Lam : ('env * 's, 't) term -> ('env, 's -> 't) term
+      | App : ('env, 's -> 't) term * ('env, 's) term -> ('env, 't) term
+    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
+  end
+#                                                                             module Convert :
+  sig
+    type ('a, 'b) layout =
+        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 prj :
+      'a Typeable.ty -> int -> ('b, 'c) layout -> ('b, 'a) DeBruijn.ix
+    val cvt : ('a, 'a) layout -> 'b HOAS.term -> ('a, 'b) DeBruijn.term
+    val convert : 'a HOAS.term -> (unit, 'a) DeBruijn.term
+  end
+#                                               module Main :
+  sig
+    val i : 'a Typeable.ty -> ('a -> 'a) HOAS.term
+    val zero : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
+    val one : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
+    val two : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
+    val three : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
+    val plus :
+      'a Typeable.ty ->
+      ((('a -> 'a) -> 'a -> 'a) ->
+       (('a -> 'a) -> 'a -> 'a) -> ('a -> 'a) -> 'a -> 'a)
+      HOAS.term
+    val plus_2_3 : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
+    val i' : (unit, int -> int) DeBruijn.term
+    val plus_2_3' : (unit, (int -> int) -> int -> int) DeBruijn.term
+    val eval_plus_2_3' : int
+  end
+# 
diff --git a/testsuite/tests/typing-gadts/test.ml b/testsuite/tests/typing-gadts/test.ml
index 46e0590c31..1ae0c97484 100644
--- a/testsuite/tests/typing-gadts/test.ml
+++ b/testsuite/tests/typing-gadts/test.ml
@@ -19,6 +19,12 @@ module Exp =
 	    (eval f) (eval a)
 	| Abs f -> f 
 
+    let discern : type a. a t -> _ = function
+        IntLit _ -> 1
+      | BoolLit _ -> 2
+      | Pair _ -> 3
+      | App _ -> 4
+      | Abs _ -> 5
   end
 ;;
 
@@ -159,17 +165,37 @@ type _ t = Int : int t ;;
 
 let ky x y = ignore (x = y); x ;;
 
+let test : type a. a t -> a =
+  function Int -> ky (1 : a) 1
+;;
+
+let test : type a. a t -> _ =
+  function Int -> 1       (* ok *)
+;;
+
+let test : type a. a t -> _ =
+  function Int -> ky (1 : a) 1  (* fails *)
+;;
+
 let test : type a. a t -> a = fun x ->
-  let r = match x with Int -> ky (1 : a) 1
+  let r = match x with Int -> ky (1 : a) 1  (* fails *)
   in r
 ;;
 let test : type a. a t -> a = fun x ->
-  let r = match x with Int -> ky 1 (1 : a)
+  let r = match x with Int -> ky 1 (1 : a)  (* fails *)
+  in r
+;;
+let test (type a) x =
+  let r = match (x : a t) with Int -> ky 1 1
   in r
 ;;
 let test : type a. a t -> a = fun x ->
-  let r = match x with Int -> (1 : a)
-  in r (* fails too *)
+  let r = match x with Int -> (1 : a)       (* ok! *)
+  in r
+;;
+let test : type a. a t -> _ = fun x ->
+  let r = match x with Int -> 1       (* ok! *)
+  in r
 ;;
 let test : type a. a t -> a = fun x ->
   let r : a = match x with Int -> 1
@@ -178,7 +204,7 @@ let test : type a. a t -> a = fun x ->
 let test2 : type a. a t -> a option = fun x ->
   let r = ref None in
   begin match x with Int -> r := Some (1 : a) end;
-  !r (* normalized to int option *)
+  !r (* ok *)
 ;;
 let test2 : type a. a t -> a option = fun x ->
   let r : a option ref = ref None in
@@ -190,19 +216,19 @@ let test2 : type a. a t -> a option = fun x ->
   let u = ref None in
   begin match x with Int -> r := Some 1; u := !r end;
   !u
-;; (* fail *)
+;; (* ok (u non-ambiguous) *)
 let test2 : type a. a t -> a option = fun x ->
   let r : a option ref = ref None in
   let u = ref None in
   begin match x with Int -> u := Some 1; r := !u end;
   !u
-;; (* fail *)
+;; (* fails because u : (int | a) option ref *)
 let test2 : type a. a t -> a option = fun x ->
   let u = ref None in
   let r : a option ref = ref None in
   begin match x with Int -> r := Some 1; u := !r end;
   !u
-;; (* fail *)
+;; (* ok *)
 let test2 : type a. a t -> a option = fun x ->
   let u = ref None in
   let a =
@@ -210,34 +236,136 @@ let test2 : type a. a t -> a option = fun x ->
     begin match x with Int -> r := Some 1; u := !r end;
     !u
   in a
+;; (* ok *)
+let either = ky
+let we_y1x (type a) (x : a) (v : a t) =
+  match v with Int -> let y = either 1 x in y
 ;; (* fail *)
 
 (* Effect of external consraints *)
-
 let f (type a) (x : a t) y =
   ignore (y : a);
-  let r = match x with Int -> (y : a) in (* fails *)
+  let r = match x with Int -> (y : a) in (* ok *)
   r
 ;;
 let f (type a) (x : a t) y =
   let r = match x with Int -> (y : a) in
-  ignore (y : a); (* fails *)
+  ignore (y : a); (* ok *)
   r
 ;;
 let f (type a) (x : a t) y =
   ignore (y : a);
-  let r = match x with Int -> y in
+  let r = match x with Int -> y in (* ok *)
   r
 ;;
 let f (type a) (x : a t) y =
   let r = match x with Int -> y in
-  ignore (y : a);
+  ignore (y : a); (* ok *)
   r
 ;;
 let f (type a) (x : a t) (y : a) =
-  match x with Int -> y (* should return an int! *)
+  match x with Int -> y (* returns 'a *)
 ;;
 
+(* Combination with local modules *)
+
+let f (type a) (x : a t) y =
+  match x with Int ->
+    let module M = struct type b = a let z = (y : b) end
+    in M.z
+;; (* fails because of aliasing... *)
+
+let f (type a) (x : a t) y =
+  match x with Int ->
+    let module M = struct type b = int let z = (y : b) end
+    in M.z
+;; (* ok *)
+
+(* Objects and variants *)
+
+type _ h =
+  | Has_m : <m : int> h
+  | Has_b : <b : bool> h
+
+let f : type a. a h -> a = function
+  | Has_m -> object method m = 1 end
+  | Has_b -> object method b = true end
+;;
+type _ j =
+  | Has_A : [`A of int] j
+  | Has_B : [`B of bool] j
+
+let f : type a. a j -> a = function
+  | Has_A -> `A 1
+  | Has_B -> `B true
+;;
+
+type (_,_) eq = Eq : ('a,'a) eq ;;
+
+let f : type a b. (a,b) eq -> (<m : a; ..> as 'a) -> (<m : b; ..> as 'a) =
+  fun Eq o -> o
+;; (* fail *)
+
+let f : type a b. (a,b) eq -> <m : a; ..> -> <m : b; ..> =
+  fun Eq o -> o
+;; (* fail *)
+
+let f (type a) (type b) (eq : (a,b) eq) (o : <m : a; ..>) : <m : b; ..> =
+  match eq with Eq -> o ;; (* should fail *)
+
+let f : type a b. (a,b) eq -> <m : a> -> <m : b> =
+  fun Eq o -> o
+;; (* ok *)
+
+let int_of_bool : (bool,int) eq = Obj.magic Eq;;
+
+let x = object method m = true end;;
+let y = (x, f int_of_bool x);;
+
+let f : type a. (a, int) eq -> <m : a> -> bool =
+  fun Eq o -> ignore (o : <m : int; ..>); o#m = 3
+;; (* should be ok *)
+
+let f : type a b. (a,b) eq -> < m : a; .. > -> < m : b > =
+  fun eq o ->
+    ignore (o : < m : a >);
+    let r : < m : b > = match eq with Eq -> o in (* fail with principal *)
+    r;;
+
+let f : type a b. (a,b) eq -> < m : a; .. > -> < m : b > =
+  fun eq o ->
+    let r : < m : b > = match eq with Eq -> o in (* fail *)
+    ignore (o : < m : a >);
+    r;;
+
+let f : type a b. (a,b) eq -> [> `A of a] -> [> `A of b] =
+  fun Eq o -> o ;; (* fail *)
+
+let f (type a) (type b) (eq : (a,b) eq) (v : [> `A of a]) : [> `A of b] =
+  match eq with Eq -> v ;; (* should fail *)
+
+let f : type a b. (a,b) eq -> [< `A of a | `B] -> [< `A of b | `B] =
+  fun Eq o -> o ;; (* fail *)
+
+let f : type a b. (a,b) eq -> [`A of a | `B] -> [`A of b | `B] =
+  fun Eq o -> o ;; (* ok *)
+
+let f : type a. (a, int) eq -> [`A of a] -> bool =
+  fun Eq v -> match v with `A 1 -> true | _ -> false
+;; (* ok *)
+
+let f : type a b. (a,b) eq -> [> `A of a | `B] -> [`A of b | `B] =
+  fun eq o ->
+    ignore (o : [< `A of a | `B]);
+    let r : [`A of b | `B] = match eq with Eq -> o in (* fail with principal *)
+    r;;
+
+let f : type a b. (a,b) eq -> [> `A of a | `B] -> [`A of b | `B] =
+  fun eq o ->
+    let r : [`A of b | `B] = match eq with Eq -> o in (* fail *)
+    ignore (o : [< `A of a | `B]);
+    r;;
+
 (* Pattern matching *)
 
 type 'a t =
@@ -307,4 +435,4 @@ let f : type a. a ty -> a t -> int = fun x y ->
   | {left=TE TC; right=D [|1.0|]} -> 14
   | {left=TA; right=D 0} -> -1
   | {left=TA; right=D z} -> z
-;; (* warn *)
+;; (* ok *)
diff --git a/testsuite/tests/typing-gadts/test.ml.principal.reference b/testsuite/tests/typing-gadts/test.ml.principal.reference
index 88065d4435..b770efb905 100644
--- a/testsuite/tests/typing-gadts/test.ml.principal.reference
+++ b/testsuite/tests/typing-gadts/test.ml.principal.reference
@@ -1,5 +1,5 @@
 
-#                                             module Exp :
+#                                                         module Exp :
   sig
     type 'a t =
         IntLit : int -> int t
@@ -8,6 +8,7 @@
       | App : ('a -> 'b) t * 'a t -> 'b t
       | Abs : ('a -> 'b) -> ('a -> 'b) t
     val eval : 'a t -> 'a
+    val discern : 'a t -> int
   end
 #                                     module List :
   sig
@@ -49,9 +50,9 @@ module Nonexhaustive :
 #               Characters 119-120:
       let eval (D x) = x
                        ^
-Error: This expression has type &x7 t but an expression was expected of type
-         &x7 t
-       The type constructor &x7 would escape its scope
+Error: This expression has type ex#12 t
+       but an expression was expected of type ex#12 t
+       The type constructor ex#12 would escape its scope
 #                       Characters 157-158:
   	  C ->
      ^
@@ -69,8 +70,7 @@ Error: This pattern matches values of type ([? `A ] as 'a) * bool t
 #                                 Characters 300-301:
       | BoolLit b -> b
                      ^
-Error: This expression has type bool but an expression was expected of type
-         int
+Error: This expression has type bool but an expression was expected of type s
 #             Characters 87-88:
     let f = function A -> 1 | B -> 2
                               ^
@@ -78,56 +78,153 @@ Error: This pattern matches values of type b
        but a pattern was expected which matches values of type a
 #   type 'a t = Int : int t
 #   val ky : 'a -> 'a -> 'a = <fun>
-#         Characters 88-89:
-    in r
-       ^
-Error: This expression has type int but an expression was expected of type a
-#       Characters 87-88:
-    in r
-       ^
-Error: This expression has type int but an expression was expected of type a
-#       Characters 82-83:
-    in r (* fails too *)
-       ^
-Error: This expression has type int but an expression was expected of type a
 #       val test : 'a t -> 'a = <fun>
-#         Characters 122-124:
-    !r (* normalized to int option *)
-    ^^
-Error: This expression has type int option
-       but an expression was expected of type a option
+#       val test : 'a t -> int = <fun>
+#       Characters 49-61:
+    function Int -> ky (1 : a) 1  (* fails *)
+                    ^^^^^^^^^^^^
+Error: This expression has type a = int
+       but an expression was expected of type a = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#         Characters 70-82:
+    let r = match x with Int -> ky (1 : a) 1  (* fails *)
+                                ^^^^^^^^^^^^
+Error: This expression has type a = int
+       but an expression was expected of type a = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#       Characters 69-81:
+    let r = match x with Int -> ky 1 (1 : a)  (* fails *)
+                                ^^^^^^^^^^^^
+Error: This expression has type a = int
+       but an expression was expected of type a = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#       val test : 'a t -> int = <fun>
+#       val test : 'a t -> 'a = <fun>
+#       val test : 'a t -> int = <fun>
+#       val test : 'a t -> 'a = <fun>
 #         val test2 : 'a t -> 'a option = <fun>
-#           Characters 162-164:
-    !u
-    ^^
-Error: This expression has type int option
-       but an expression was expected of type a option
-#           Characters 162-164:
-    !u
-    ^^
-Error: This expression has type int option
-       but an expression was expected of type a option
-#           Characters 162-164:
-    !u
-    ^^
-Error: This expression has type int option
-       but an expression was expected of type a option
-#               Characters 186-187:
-    in a
-       ^
+#         val test2 : 'a t -> 'a option = <fun>
+#           val test2 : 'a t -> 'a option = <fun>
+#           Characters 152-154:
+    begin match x with Int -> u := Some 1; r := !u end;
+                                                ^^
 Error: This expression has type int option
        but an expression was expected of type a option
-#               Characters 116-117:
-    let r = match x with Int -> (y : a) in (* fails *)
-                                 ^
-Error: This expression has type a but an expression was expected of type int
-#         Characters 80-81:
-    ignore (y : a); (* fails *)
-            ^
-Error: This expression has type int but an expression was expected of type a
+       Type int is not compatible with type a = int 
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#           val test2 : 'a t -> 'a option = <fun>
+#               val test2 : 'a t -> 'a option = <fun>
+#       Characters 100-101:
+    match v with Int -> let y = either 1 x in y
+                                              ^
+Error: This expression has type a = int
+       but an expression was expected of type a = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#             val f : 'a t -> 'a -> 'a = <fun>
+#         val f : 'a t -> 'a -> 'a = <fun>
 #         val f : 'a t -> 'a -> 'a = <fun>
 #         val f : 'a t -> 'a -> 'a = <fun>
-#     val f : 'a t -> 'a -> int = <fun>
+#     val f : 'a t -> 'a -> 'a = <fun>
+#               Characters 136-137:
+      let module M = struct type b = a let z = (y : b) end
+                                                ^
+Error: This expression has type a = int
+       but an expression was expected of type b = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#           val f : 'a t -> int -> int = <fun>
+#                     type 'a h = Has_m : < m : int > h | Has_b : < b : bool > h
+val f : 'a h -> 'a = <fun>
+#               type 'a j = Has_A : [ `A of int ] j | Has_B : [ `B of bool ] j
+val f : 'a j -> 'a = <fun>
+#   type ('a, 'b) eq = Eq : ('a, 'a) eq
+#       Characters 5-91:
+  ....f : type a b. (a,b) eq -> (<m : a; ..> as 'a) -> (<m : b; ..> as 'a) =
+    fun Eq o -> o
+Error: The universal type variable 'b cannot be generalized:
+       it is already bound to another variable.
+#       Characters 74-75:
+    fun Eq o -> o
+                ^
+Error: This expression has type < m : a; .. >
+       but an expression was expected of type < m : b; .. >
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#     Characters 97-98:
+    match eq with Eq -> o ;; (* should fail *)
+                        ^
+Error: This expression has type < m : a; .. >
+       but an expression was expected of type < m : b; .. >
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#       val f : ('a, 'b) eq -> < m : 'a > -> < m : 'b > = <fun>
+#   val int_of_bool : (bool, int) eq = Eq
+#   val x : < m : bool > = <obj>
+# val y : < m : bool > * < m : int > = (<obj>, <obj>)
+#       val f : ('a, int) eq -> < m : 'a > -> bool = <fun>
+#           Characters 146-147:
+      let r : < m : b > = match eq with Eq -> o in (* fail with principal *)
+                                              ^
+Error: This expression has type < m : a >
+       but an expression was expected of type < m : b >
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#           Characters 118-119:
+      let r : < m : b > = match eq with Eq -> o in (* fail *)
+                                              ^
+Error: This expression has type < m : a; .. >
+       but an expression was expected of type < m : b >
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#     Characters 74-75:
+    fun Eq o -> o ;; (* fail *)
+                ^
+Error: This expression has type [> `A of a ]
+       but an expression was expected of type [> `A of b ]
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#     Characters 97-98:
+    match eq with Eq -> v ;; (* should fail *)
+                        ^
+Error: This expression has type [> `A of a ]
+       but an expression was expected of type [> `A of b ]
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#     Characters 5-85:
+  ....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
+#     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:
+      let r : [`A of b | `B] = match eq with Eq -> o in (* fail with principal *)
+                                                   ^
+Error: This expression has type [ `A of a | `B ]
+       but an expression was expected of type [ `A of b | `B ]
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#           Characters 131-132:
+      let r : [`A of b | `B] = match eq with Eq -> o in (* fail *)
+                                                   ^
+Error: This expression has type [> `A of a | `B ]
+       but an expression was expected of type [ `A of b | `B ]
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
 #                                                     type 'a t = A of int | B of bool | C of float | D of 'a
 type 'a ty =
     TE : 'a ty -> 'a array ty
@@ -168,7 +265,7 @@ Error: This pattern matches values of type 'a array
     | {left=TA; right=D z} -> z
 Warning 8: this pattern-matching is not exhaustive.
 Here is an example of a value that is not matched:
-{left=TE TA; right=D [| _ |]}
+{left=TE TC; right=D [|  |]}
 type ('a, 'b) pair = { left : 'a; right : 'b; }
 val f : 'a ty -> 'a t -> int = <fun>
 # 
diff --git a/testsuite/tests/typing-gadts/test.ml.reference b/testsuite/tests/typing-gadts/test.ml.reference
index 3a4633e039..bb44dce52f 100644
--- a/testsuite/tests/typing-gadts/test.ml.reference
+++ b/testsuite/tests/typing-gadts/test.ml.reference
@@ -1,5 +1,5 @@
 
-#                                             module Exp :
+#                                                         module Exp :
   sig
     type 'a t =
         IntLit : int -> int t
@@ -8,6 +8,7 @@
       | App : ('a -> 'b) t * 'a t -> 'b t
       | Abs : ('a -> 'b) -> ('a -> 'b) t
     val eval : 'a t -> 'a
+    val discern : 'a t -> int
   end
 #                                     module List :
   sig
@@ -49,9 +50,9 @@ module Nonexhaustive :
 #               Characters 119-120:
       let eval (D x) = x
                        ^
-Error: This expression has type &x7 t but an expression was expected of type
-         &x7 t
-       The type constructor &x7 would escape its scope
+Error: This expression has type ex#12 t
+       but an expression was expected of type ex#12 t
+       The type constructor ex#12 would escape its scope
 #                       Characters 157-158:
   	  C ->
      ^
@@ -66,11 +67,11 @@ Error: This pattern matches values of type int t
      ^^^^^^^^^^^^^
 Error: This pattern matches values of type ([? `A ] as 'a) * bool t
        but a pattern was expected which matches values of type 'a * int t
-#                                 Characters 300-301:
-      | BoolLit b -> b
-                     ^
-Error: This expression has type bool but an expression was expected of type
-         int
+#                                 module Propagation :
+  sig
+    type 'a t = IntLit : int -> int t | BoolLit : bool -> bool t
+    val check : 'a t -> 'a
+  end
 #             Characters 87-88:
     let f = function A -> 1 | B -> 2
                               ^
@@ -78,45 +79,139 @@ Error: This pattern matches values of type b
        but a pattern was expected which matches values of type a
 #   type 'a t = Int : int t
 #   val ky : 'a -> 'a -> 'a = <fun>
-#         Characters 88-89:
-    in r
-       ^
-Error: This expression has type int but an expression was expected of type a
-#       Characters 87-88:
-    in r
-       ^
-Error: This expression has type int but an expression was expected of type a
-#       Characters 82-83:
-    in r (* fails too *)
-       ^
-Error: This expression has type int but an expression was expected of type a
 #       val test : 'a t -> 'a = <fun>
-#         Characters 122-124:
-    !r (* normalized to int option *)
-    ^^
-Error: This expression has type int option
-       but an expression was expected of type a option
+#       val test : 'a t -> int = <fun>
+#       Characters 49-61:
+    function Int -> ky (1 : a) 1  (* fails *)
+                    ^^^^^^^^^^^^
+Error: This expression has type a = int
+       but an expression was expected of type a = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#         Characters 70-82:
+    let r = match x with Int -> ky (1 : a) 1  (* fails *)
+                                ^^^^^^^^^^^^
+Error: This expression has type a = int
+       but an expression was expected of type a = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#       Characters 69-81:
+    let r = match x with Int -> ky 1 (1 : a)  (* fails *)
+                                ^^^^^^^^^^^^
+Error: This expression has type a = int
+       but an expression was expected of type a = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#       val test : 'a t -> int = <fun>
+#       val test : 'a t -> 'a = <fun>
+#       val test : 'a t -> int = <fun>
+#       val test : 'a t -> 'a = <fun>
+#         val test2 : 'a t -> 'a option = <fun>
 #         val test2 : 'a t -> 'a option = <fun>
 #           val test2 : 'a t -> 'a option = <fun>
-#           Characters 162-164:
-    !u
-    ^^
+#           Characters 152-154:
+    begin match x with Int -> u := Some 1; r := !u end;
+                                                ^^
 Error: This expression has type int option
        but an expression was expected of type a option
+       Type int is not compatible with type a = int 
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
 #           val test2 : 'a t -> 'a option = <fun>
-#               Characters 186-187:
-    in a
-       ^
-Error: This expression has type int option
-       but an expression was expected of type a option
-#               val f : 'a t -> 'a -> int = <fun>
-#         Characters 80-81:
-    ignore (y : a); (* fails *)
-            ^
-Error: This expression has type int but an expression was expected of type a
+#               val test2 : 'a t -> 'a option = <fun>
+#       Characters 100-101:
+    match v with Int -> let y = either 1 x in y
+                                              ^
+Error: This expression has type a = int
+       but an expression was expected of type a = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#             val f : 'a t -> 'a -> 'a = <fun>
+#         val f : 'a t -> 'a -> 'a = <fun>
 #         val f : 'a t -> 'a -> 'a = <fun>
 #         val f : 'a t -> 'a -> 'a = <fun>
 #     val f : 'a t -> 'a -> 'a = <fun>
+#               Characters 136-137:
+      let module M = struct type b = a let z = (y : b) end
+                                                ^
+Error: This expression has type a = int
+       but an expression was expected of type b = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+#           val f : 'a t -> int -> int = <fun>
+#                     type 'a h = Has_m : < m : int > h | Has_b : < b : bool > h
+val f : 'a h -> 'a = <fun>
+#               type 'a j = Has_A : [ `A of int ] j | Has_B : [ `B of bool ] j
+val f : 'a j -> 'a = <fun>
+#   type ('a, 'b) eq = Eq : ('a, 'a) eq
+#       Characters 5-91:
+  ....f : type a b. (a,b) eq -> (<m : a; ..> as 'a) -> (<m : b; ..> as 'a) =
+    fun Eq o -> o
+Error: The universal type variable 'b cannot be generalized:
+       it is already bound to another variable.
+#       Characters 74-75:
+    fun Eq o -> o
+                ^
+Error: This expression has type < m : a; .. >
+       but an expression was expected of type < m : b; .. >
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#     Characters 97-98:
+    match eq with Eq -> o ;; (* should fail *)
+                        ^
+Error: This expression has type < m : a; .. >
+       but an expression was expected of type < m : b; .. >
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#       val f : ('a, 'b) eq -> < m : 'a > -> < m : 'b > = <fun>
+#   val int_of_bool : (bool, int) eq = Eq
+#   val x : < m : bool > = <obj>
+# val y : < m : bool > * < m : int > = (<obj>, <obj>)
+#       val f : ('a, int) eq -> < m : 'a > -> bool = <fun>
+#           val f : ('a, 'b) eq -> < m : 'a > -> < m : 'b > = <fun>
+#           Characters 118-119:
+      let r : < m : b > = match eq with Eq -> o in (* fail *)
+                                              ^
+Error: This expression has type < m : a; .. >
+       but an expression was expected of type < m : b >
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#     Characters 74-75:
+    fun Eq o -> o ;; (* fail *)
+                ^
+Error: This expression has type [> `A of a ]
+       but an expression was expected of type [> `A of b ]
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#     Characters 97-98:
+    match eq with Eq -> v ;; (* should fail *)
+                        ^
+Error: This expression has type [> `A of a ]
+       but an expression was expected of type [> `A of b ]
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+#     Characters 5-85:
+  ....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
+#     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>
+#           Characters 131-132:
+      let r : [`A of b | `B] = match eq with Eq -> o in (* fail *)
+                                                   ^
+Error: This expression has type [> `A of a | `B ]
+       but an expression was expected of type [ `A of b | `B ]
+       Type a is not compatible with type b = a 
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
 #                                                     type 'a t = A of int | B of bool | C of float | D of 'a
 type 'a ty =
     TE : 'a ty -> 'a array ty
@@ -157,7 +252,7 @@ Error: This pattern matches values of type 'a array
     | {left=TA; right=D z} -> z
 Warning 8: this pattern-matching is not exhaustive.
 Here is an example of a value that is not matched:
-{left=TE (TE _); right=D [| _ |]}
+{left=TE TC; right=D [|  |]}
 type ('a, 'b) pair = { left : 'a; right : 'b; }
 val f : 'a ty -> 'a t -> int = <fun>
 # 
diff --git a/testsuite/tests/typing-gadts/yallop_bugs.ml b/testsuite/tests/typing-gadts/yallop_bugs.ml
new file mode 100644
index 0000000000..08708a67cc
--- /dev/null
+++ b/testsuite/tests/typing-gadts/yallop_bugs.ml
@@ -0,0 +1,45 @@
+(* Injectivity *)
+
+type (_, _) eq = Refl : ('a, 'a) eq
+
+let magic : 'a 'b. 'a -> 'b =
+  fun (type a) (type b) (x : a) ->
+    let module M =
+      (functor (T : sig type 'a t end) ->
+       struct
+         let f (Refl : (a T.t, b T.t) eq) = (x :> b)
+       end)
+        (struct type 'a t = unit end)
+    in M.f Refl
+;;
+
+(* Variance and subtyping *)
+
+type (_, +_) eq = Refl : ('a, 'a) eq
+
+let magic : 'a 'b. 'a -> 'b =
+  fun (type a) (type b) (x : a) ->
+    let bad_proof (type a) =
+      (Refl : (< m : a>, <m : a>) eq :> (<m : a>, < >) eq) in
+    let downcast : type a. (a, < >) eq -> < > -> a =
+      fun (type a) (Refl : (a, < >) eq) (s : < >) -> (s :> a) in
+    (downcast bad_proof ((object method m = x end) :> < >)) # m
+;;
+
+(* Record patterns *)
+
+type _ t =
+  | IntLit : int t
+  | BoolLit : bool t
+
+let check : type s . s t * s -> bool = function
+  | BoolLit, false -> false
+  | IntLit , 6 -> false
+;;
+
+type ('a, 'b) pair = { fst : 'a; snd : 'b }
+
+let check : type s . (s t, s) pair -> bool = function
+  | {fst = BoolLit; snd = false} -> false
+  | {fst = IntLit ; snd =  6} -> false
+;;
diff --git a/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference b/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference
new file mode 100644
index 0000000000..527649649b
--- /dev/null
+++ b/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference
@@ -0,0 +1,31 @@
+
+#                           Characters 212-216:
+           let f (Refl : (a T.t, b T.t) eq) = (x :> b)
+                  ^^^^
+Error: This pattern matches values of type (a T.t, a T.t) eq
+       but a pattern was expected which matches values of type
+         (a T.t, b T.t) eq
+#                         Characters 36-67:
+  type (_, +_) eq = Refl : ('a, 'a) eq
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In this GADT definition, the variance of some parameter
+       cannot be checked
+#                     Characters 115-175:
+  .......................................function
+    | BoolLit, false -> false
+    | IntLit , 6 -> false
+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>
+#             Characters 91-180:
+  .............................................function
+    | {fst = BoolLit; snd = false} -> false
+    | {fst = IntLit ; snd =  6} -> false
+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>
+# 
diff --git a/testsuite/tests/typing-gadts/yallop_bugs.ml.reference b/testsuite/tests/typing-gadts/yallop_bugs.ml.reference
new file mode 100644
index 0000000000..527649649b
--- /dev/null
+++ b/testsuite/tests/typing-gadts/yallop_bugs.ml.reference
@@ -0,0 +1,31 @@
+
+#                           Characters 212-216:
+           let f (Refl : (a T.t, b T.t) eq) = (x :> b)
+                  ^^^^
+Error: This pattern matches values of type (a T.t, a T.t) eq
+       but a pattern was expected which matches values of type
+         (a T.t, b T.t) eq
+#                         Characters 36-67:
+  type (_, +_) eq = Refl : ('a, 'a) eq
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In this GADT definition, the variance of some parameter
+       cannot be checked
+#                     Characters 115-175:
+  .......................................function
+    | BoolLit, false -> false
+    | IntLit , 6 -> false
+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>
+#             Characters 91-180:
+  .............................................function
+    | {fst = BoolLit; snd = false} -> false
+    | {fst = IntLit ; snd =  6} -> false
+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>
+# 
diff --git a/testsuite/tests/typing-modules/Test.ml b/testsuite/tests/typing-modules/Test.ml
index 82ea468f9c..77c9d09702 100644
--- a/testsuite/tests/typing-modules/Test.ml
+++ b/testsuite/tests/typing-modules/Test.ml
@@ -3,3 +3,9 @@ module type S' = S with type t := int;;
 
 module type S = sig module rec M : sig end and N : sig end end;;
 module type S' = S with module M := String;;
+
+(* A subtle problem appearing with -principal *)
+type -'a t
+class type c = object method m : [ `A ] t end;;
+module M : sig val v : (#c as 'a) -> 'a end =
+  struct let v x = ignore (x :> c); x end;;
diff --git a/testsuite/tests/typing-modules/Test.ml.principal.reference b/testsuite/tests/typing-modules/Test.ml.principal.reference
new file mode 100644
index 0000000000..258b3ee3de
--- /dev/null
+++ b/testsuite/tests/typing-modules/Test.ml.principal.reference
@@ -0,0 +1,9 @@
+
+# module type S = sig type t and s = t end
+# module type S' = sig type s = int end
+#   module type S = sig module rec M : sig  end and N : sig  end end
+# module type S' = sig module rec N : sig  end end
+#       type -'a t
+class type c = object method m : [ `A ] t end
+#   module M : sig val v : (#c as 'a) -> 'a end
+# 
diff --git a/testsuite/tests/typing-modules/Test.ml.reference b/testsuite/tests/typing-modules/Test.ml.reference
index 823cc1a840..258b3ee3de 100644
--- a/testsuite/tests/typing-modules/Test.ml.reference
+++ b/testsuite/tests/typing-modules/Test.ml.reference
@@ -3,4 +3,7 @@
 # module type S' = sig type s = int end
 #   module type S = sig module rec M : sig  end and N : sig  end end
 # module type S' = sig module rec N : sig  end end
+#       type -'a t
+class type c = object method m : [ `A ] t end
+#   module M : sig val v : (#c as 'a) -> 'a end
 # 
diff --git a/testsuite/tests/typing-objects/Tests.ml.reference b/testsuite/tests/typing-objects/Tests.ml.reference
index 7dde3fba0b..a78367fdfe 100644
--- a/testsuite/tests/typing-objects/Tests.ml.reference
+++ b/testsuite/tests/typing-objects/Tests.ml.reference
@@ -268,11 +268,13 @@ Error: Type int -> bool is not a subtype of int -> int
   fun (x : 'a t as 'a) -> ();;
            ^^^^^^^^^^
 Error: This alias is bound to type 'a t but is used as an instance of type 'a
+       The type variable 'a occurs inside 'a t
 # Characters 19-20:
   fun (x : 'a t) -> (x : 'a); ();;
                      ^
 Error: This expression has type 'a t but an expression was expected of type
          'a
+       The type variable 'a occurs inside 'a t
 # type 'a t = < x : 'a >
 # - : ('a t as 'a) -> unit = <fun>
 # Characters 18-26:
diff --git a/testsuite/tests/typing-poly/poly.ml b/testsuite/tests/typing-poly/poly.ml
index eb3b6f84a4..17e643ad15 100644
--- a/testsuite/tests/typing-poly/poly.ml
+++ b/testsuite/tests/typing-poly/poly.ml
@@ -571,12 +571,17 @@ type u = c option;;
 let just = function None -> failwith "just" | Some x -> x;;
 let f x = let l = [Some x; (None : u)] in (just(List.hd l))#id;;
 let g x =
-  let none = match None with y -> ignore [y;(None:u)]; y in
+  let none = (fun y -> ignore [y;(None:u)]; y) None in
   let x = List.hd [Some x; none] in (just x)#id;;
 let h x =
   let none = let y = None in ignore [y;(None:u)]; y in
   let x = List.hd [Some x; none] in (just x)#id;;
 
+(* Only solved for parameterless abbreviations *)
+type 'a u = c option;;
+let just = function None -> failwith "just" | Some x -> x;;
+let f x = let l = [Some x; (None : _ u)] in (just(List.hd l))#id;;
+
 (* polymorphic recursion *)
 
 let rec f : 'a. 'a -> _ = fun x -> 1 and g x = f x;;
diff --git a/testsuite/tests/typing-poly/poly.ml.principal.reference b/testsuite/tests/typing-poly/poly.ml.principal.reference
index a87694bb77..65043c786e 100644
--- a/testsuite/tests/typing-poly/poly.ml.principal.reference
+++ b/testsuite/tests/typing-poly/poly.ml.principal.reference
@@ -265,8 +265,8 @@ Error: This field value has type 'b option ref option
 #           Characters 145-166:
   object method virtual visit : 'a.('a visitor -> 'a) end;;
                                 ^^^^^^^^^^^^^^^^^^^^^
-Error: This type scheme cannot quantify 'a :
-it escapes this scope.
+Error: The universal type variable 'a cannot be generalized:
+       it escapes its scope.
 #                 type ('a, 'b) list_visitor = < caseCons : 'b -> 'b list -> 'a; caseNil : 'a >
 type 'b alist = < visit : 'a. ('a, 'b) list_visitor -> 'a >
 class type ct = object ('a) method fold : ('b -> 'a -> 'b) -> 'b -> 'b end
@@ -555,13 +555,20 @@ Warning 18: this use of a polymorphic method is not principal.
 #     class c : object method id : 'a -> 'a end
 # type u = c option
 # val just : 'a option -> 'a = <fun>
-# val f : c -> 'a -> 'a = <fun>
-#     Characters 106-117:
+# Characters 42-62:
+  let f x = let l = [Some x; (None : u)] in (just(List.hd l))#id;;
+                                            ^^^^^^^^^^^^^^^^^^^^
+Warning 18: this use of a polymorphic method is not principal.
+val f : c -> 'a -> 'a = <fun>
+#     Characters 101-112:
     let x = List.hd [Some x; none] in (just x)#id;;
                                       ^^^^^^^^^^^
 Warning 18: this use of a polymorphic method is not principal.
 val g : c -> 'a -> 'a = <fun>
 #     val h : < id : 'a; .. > -> 'a = <fun>
+#     type 'a u = c option
+# val just : 'a option -> 'a = <fun>
+# val f : c -> 'a -> 'a = <fun>
 #       val f : 'a -> int = <fun>
 val g : 'a -> int = <fun>
 # type 'a t = Leaf of 'a | Node of ('a * 'a) t
diff --git a/testsuite/tests/typing-poly/poly.ml.reference b/testsuite/tests/typing-poly/poly.ml.reference
index 1e11ed0992..37601416bb 100644
--- a/testsuite/tests/typing-poly/poly.ml.reference
+++ b/testsuite/tests/typing-poly/poly.ml.reference
@@ -248,8 +248,8 @@ Error: This field value has type 'b option ref option
 #           Characters 145-166:
   object method virtual visit : 'a.('a visitor -> 'a) end;;
                                 ^^^^^^^^^^^^^^^^^^^^^
-Error: This type scheme cannot quantify 'a :
-it escapes this scope.
+Error: The universal type variable 'a cannot be generalized:
+       it escapes its scope.
 #                 type ('a, 'b) list_visitor = < caseCons : 'b -> 'b list -> 'a; caseNil : 'a >
 type 'b alist = < visit : 'a. ('a, 'b) list_visitor -> 'a >
 class type ct = object ('a) method fold : ('b -> 'a -> 'b) -> 'b -> 'b end
@@ -529,6 +529,9 @@ Error: Type < m : 'a. [< `A of <  > ] as 'a > is not a subtype of
 # val f : c -> 'a -> 'a = <fun>
 #     val g : c -> 'a -> 'a = <fun>
 #     val h : < id : 'a; .. > -> 'a = <fun>
+#     type 'a u = c option
+# val just : 'a option -> 'a = <fun>
+# val f : c -> 'a -> 'a = <fun>
 #       val f : 'a -> int = <fun>
 val g : 'a -> int = <fun>
 # type 'a t = Leaf of 'a | Node of ('a * 'a) t
diff --git a/toplevel/topdirs.ml b/toplevel/topdirs.ml
index 2a5a359541..6ae3644f7d 100644
--- a/toplevel/topdirs.ml
+++ b/toplevel/topdirs.ml
@@ -150,7 +150,7 @@ let match_printer_type ppf desc typename =
   let ty_arg = Ctype.newvar() in
   Ctype.unify !toplevel_env
     (Ctype.newconstr printer_type [ty_arg])
-    (Ctype.instance desc.val_type);
+    (Ctype.instance_def desc.val_type);
   Ctype.end_def();
   Ctype.generalize ty_arg;
   ty_arg
diff --git a/typing/btype.ml b/typing/btype.ml
index 67754d0ab6..c9bdbf04d4 100644
--- a/typing/btype.ml
+++ b/typing/btype.ml
@@ -16,6 +16,12 @@
 
 open Types
 
+(**** Sets, maps and hashtables of types ****)
+
+module TypeSet = Set.Make(TypeOps)
+module TypeMap = Map.Make (TypeOps)
+module TypeHash = Hashtbl.Make(TypeOps)
+
 (**** Forward declarations ****)
 
 let print_raw =
@@ -185,7 +191,7 @@ 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 _ | Tnil ->
       Misc.may (fun (_,l) -> List.iter f l) row.row_name
   | _ -> assert false
 
@@ -450,6 +456,7 @@ type change =
   | Ckind of field_kind option ref * field_kind option
   | Ccommu of commutable ref * commutable
   | Cuniv of type_expr option ref * type_expr option
+  | Ctypeset of TypeSet.t ref * TypeSet.t
 
 let undo_change = function
     Ctype  (ty, desc) -> ty.desc <- desc
@@ -459,6 +466,7 @@ let undo_change = function
   | Ckind  (r, v) -> r := v
   | Ccommu (r, v) -> r := v
   | Cuniv  (r, v) -> r := v
+  | Ctypeset (r, v) -> r := v
 
 type changes =
     Change of change * changes ref
@@ -510,6 +518,8 @@ let set_kind rk k =
   log_change (Ckind (rk, !rk)); rk := Some k
 let set_commu rc c =
   log_change (Ccommu (rc, !rc)); rc := c
+let set_typeset rs s =
+  log_change (Ctypeset (rs, !rs)); rs := s
 
 let snapshot () =
   let old = !last_snapshot in
@@ -539,9 +549,3 @@ let backtrack (changes, old) =
       changes := Unchanged;
       last_snapshot := old;
       Weak.set trail 0 (Some changes)
-
-(**** Sets, maps and hashtables of types ****)
-
-module TypeSet = Set.Make(TypeOps)
-module TypeMap = Map.Make (TypeOps)
-module TypeHash = Hashtbl.Make(TypeOps)
diff --git a/typing/btype.mli b/typing/btype.mli
index 755c840c37..e2e4c9d6db 100644
--- a/typing/btype.mli
+++ b/typing/btype.mli
@@ -17,6 +17,14 @@
 open Asttypes
 open Types
 
+(**** Sets, maps and hashtables of types ****)
+
+module TypeSet  : Set.S with type elt = type_expr
+module TypeMap  : Map.S with type key = type_expr
+module TypeHash : Hashtbl.S with type key = type_expr
+
+(**** Levels ****)
+
 val generic_level: int
 
 val newty2: int -> type_desc -> type_expr
@@ -46,6 +54,8 @@ val field_kind_repr: field_kind -> field_kind
 val commu_repr: commutable -> commutable
         (* Return the canonical representative of a commutation lock *)
 
+(**** polymorphic variants ****)
+
 val row_repr: row_desc -> row_desc
         (* Return the canonical representative of a row description *)
 val row_field_repr: row_field -> row_field
@@ -153,15 +163,10 @@ val set_row_field: row_field option ref -> row_field -> unit
 val set_univar: type_expr option ref -> type_expr -> unit
 val set_kind: field_kind option ref -> field_kind -> unit
 val set_commu: commutable ref -> commutable -> unit
+val set_typeset: TypeSet.t ref -> TypeSet.t -> unit
         (* Set references, logging the old value *)
 val log_type: type_expr -> unit
         (* Log the old value of a type, before modifying it by hand *)
 
-(**** Sets, maps and hashtables of types ****)
-
-module TypeSet  : Set.S with type elt = type_expr
-module TypeMap  : Map.S with type key = type_expr
-module TypeHash : Hashtbl.S with type key = type_expr
-
 (**** Forward declarations ****)
 val print_raw: (Format.formatter -> type_expr -> unit) ref
diff --git a/typing/ctype.ml b/typing/ctype.ml
index af5d6f7feb..319bec1c39 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -140,9 +140,18 @@ let is_object_type path =
 
 (**** Abbreviations without parameters ****)
 (* Shall reset after generalizing *)
+
+let trace_gadt_instances = ref false
+let check_trace_gadt_instances env =
+  not !trace_gadt_instances && Env.has_local_constraints env &&
+  (trace_gadt_instances := true; cleanup_abbrev (); true)
+
 let simple_abbrevs = ref Mnil
+
 let proper_abbrevs path tl abbrev =
-  if !Clflags.principal || tl <> [] || is_object_type path then abbrev
+  if tl <> [] || !trace_gadt_instances || !Clflags.principal ||
+     is_object_type path
+  then abbrev
   else simple_abbrevs
 
 (**** Some type creators ****)
@@ -182,25 +191,9 @@ module TypePairs =
 type unification_mode = 
   | Expression (* unification in expression *)
   | Pattern (* unification in pattern which may add local constraints *)
-  | Old
-      (* unification in pattern, old style. 
-         local constraints are not used nor generated *)
 
 let umode = ref Expression
 
-let actual_mode env = 
-  match !umode with
-  | Old -> Old
-  | Expression
-    when not (Env.has_local_constraints env) ->
-      Old
-  | Pattern | Expression -> !umode
-
-let use_local () = 
-  match !umode with
-  | Expression | Pattern -> true
-  | Old -> false
-
 let set_mode mode f = 
   let old_unification_mode = !umode in
   try
@@ -208,31 +201,9 @@ let set_mode mode f =
     let ret = f () in
     umode := old_unification_mode;
     ret
-  with
-    e ->
-      umode := old_unification_mode;
-      raise e
-
-let change_mode mode f = 
-  let old_unification_mode = !umode in
-  if old_unification_mode = mode then f () else
-  try
-    begin match old_unification_mode, mode with
-      Expression,Pattern -> 
-        umode := mode; 
-        f ();
-        umode := old_unification_mode;
-    | _ -> 
-        umode := mode; 
-        cleanup_abbrev (); 
-        f (); 
-        cleanup_abbrev ();
-        umode := old_unification_mode end
-  with
-    e -> 
-      umode := old_unification_mode;
-      cleanup_abbrev ();
-      raise e
+  with e ->
+    umode := old_unification_mode;
+    raise e
 
                   (**********************************************)
                   (*  Miscellaneous operations on object types  *)
@@ -470,7 +441,7 @@ let rec free_vars_rec real ty =
         free_variables := (ty, real) :: !free_variables
     | Tconstr (path, tl, _), Some env ->
         begin try
-          let (_, body) = Env.find_type_expansion path env in
+          let (_, body, _) = Env.find_type_expansion path env in
           if (repr body).level <> generic_level then
             free_variables := (ty, real) :: !free_variables
         with Not_found -> ()
@@ -653,10 +624,6 @@ let generalize_structure var_level ty =
   simple_abbrevs := Mnil;
   generalize_structure var_level ty
 
-(* let generalize_expansive ty = generalize_structure !nongen_level ty *)
-let generalize_global ty = generalize_structure !global_level ty
-let generalize_structure ty = generalize_structure !current_level ty
-
 (* Generalize the spine of a function, if the level >= !current_level *)
 
 let rec generalize_spine ty =
@@ -687,7 +654,7 @@ let get_level env p =
   try
     match (Env.find_type p env).type_newtype_level with
       | None -> Path.binding_time p
-      | Some x -> x
+      | Some (x, _) -> x
   with 
     | _ -> 
       (* no newtypes in predef *)
@@ -696,9 +663,13 @@ let get_level env p =
 let rec update_level env level ty =
   let ty = repr ty in
   if ty.level > level then begin
+    if Env.has_local_constraints env then begin
+      match Env.gadt_instance_level env ty with
+        Some lv -> if level < lv then raise (Unify [(ty, newvar2 level)])
+      | None -> ()
+    end;
     match ty.desc with
-      Tconstr(p, tl, abbrev)
-      when level < Env.map_newtype_level env (get_level env p) ->
+      Tconstr(p, tl, abbrev) when level < get_level env p ->
         (* Try first to replace an abbreviation by its expansion. *)
         begin try
           (* if is_newtype env p then raise Cannot_expand; *)
@@ -736,6 +707,9 @@ let rec update_level env level ty =
 
 (* Generalize and lower levels of contravariant branches simultaneously *)
 
+let generalize_contravariant env =
+  if !Clflags.principal then generalize_structure else update_level env
+
 let rec generalize_expansive env var_level ty =
   let ty = repr ty in
   if ty.level <> generic_level then begin
@@ -749,13 +723,13 @@ let rec generalize_expansive env var_level ty =
           abbrev := Mnil;
           List.iter2
             (fun (co,cn,ct) t ->
-              if ct then update_level env var_level t
+              if ct then generalize_contravariant env var_level t
               else generalize_expansive env var_level t)
             variance tyl
       | Tpackage (_, _, tyl) ->
-          List.iter (update_level env var_level) tyl
+          List.iter (generalize_contravariant env var_level) tyl
       | Tarrow (_, t1, t2, _) ->
-          update_level env var_level t1;
+          generalize_contravariant env var_level t1;
           generalize_expansive env var_level t2
       | _ ->
           iter_type_expr (generalize_expansive env var_level) ty
@@ -766,8 +740,11 @@ let generalize_expansive env ty =
   simple_abbrevs := Mnil;
   try
     generalize_expansive env !nongen_level ty
-  with Unify [_, ty'] ->
-    raise (Unify [ty, ty'])
+  with Unify ([_, ty'] as tr) ->
+    raise (Unify ((ty, ty') :: tr))
+
+let generalize_global ty = generalize_structure !global_level ty
+let generalize_structure ty = generalize_structure !current_level ty
 
 (* Correct the levels of type [ty]. *)
 let correct_levels ty =
@@ -893,8 +870,8 @@ let abbreviations = ref (ref Mnil)
 
 (* partial: we may not wish to copy the non generic types
    before we call type_pat *)
-let rec copy ?partial ty =
-  let copy = copy ?partial in
+let rec copy ?env ?partial ty =
+  let copy = copy ?env ?partial in
   let ty = repr ty in
   match ty.desc with
     Tsubst ty -> ty
@@ -915,6 +892,14 @@ let rec copy ?partial ty =
     let desc = ty.desc in
     save_desc ty desc;
     let t = newvar() in          (* Stub *)
+    begin match env with
+      Some env when Env.has_local_constraints env ->
+        begin match Env.gadt_instance_level env ty with
+          Some lv -> Env.add_gadt_instances env lv [t]
+        | None -> ()
+        end
+    | _ -> ()
+    end;
     ty.desc <- Tsubst t;
     t.desc <-
       begin match desc with
@@ -954,7 +939,7 @@ let rec copy ?partial ty =
               let more' =
                 match more.desc with
                   Tsubst ty -> ty
-                | Tconstr _ ->
+                | Tconstr _ | Tnil ->
                     if keep then save_desc more more.desc;
                     copy more
                 | Tvar _ | Tunivar _ ->
@@ -981,30 +966,44 @@ let rec copy ?partial ty =
 
 (**** Variants of instantiations ****)
 
-let instance ?partial sch =
+let gadt_env env =
+  if Env.has_local_constraints env
+  then Some env
+  else None
+
+let instance ?partial env sch =
+  let env = gadt_env env in
   let partial =
     match partial with
       None -> None
     | Some keep -> Some (compute_univars sch, keep)
   in
-  let ty = copy ?partial sch in
+  let ty = copy ?env ?partial sch in
   cleanup_types ();
   ty
 
-let instance_list schl =
-  let tyl = List.map copy schl in
+let instance_def sch =
+  let ty = copy sch in
+  cleanup_types ();
+  ty  
+
+let instance_list env schl =
+  let env = gadt_env env in
+  let tyl = List.map (copy ?env) schl in
   cleanup_types ();
   tyl
 
-let reified_var_counter = ref 0
+let reified_var_counter = ref Vars.empty
     
 (* names given to new type constructors. 
    Used for existential types and 
    local constraints *)
-let get_new_abstract_name () = 
-  let ret = Printf.sprintf "&x%d" !reified_var_counter in
-  incr reified_var_counter;
-  ret
+let get_new_abstract_name s =
+  let index =
+    try Vars.find s !reified_var_counter + 1
+    with Not_found -> 0 in
+  reified_var_counter := Vars.add s index !reified_var_counter;
+  Printf.sprintf "%s#%d" s index
 
 let new_declaration newtype manifest = 
   {
@@ -1024,17 +1023,21 @@ let instance_constructor ?in_pattern cstr =
   begin match in_pattern with
   | None -> ()
   | Some (env, newtype_lev) ->
-      let existentials = List.map copy cstr.cstr_existentials in
       let process existential = 
-        let decl = new_declaration (Some newtype_lev) None in
+        let decl = new_declaration (Some (newtype_lev, newtype_lev)) None in
+        let name =
+          match repr existential with
+            {desc = Tvar (Some name)} -> name
+          | _ -> "ex"
+        in
         let (id, new_env) =
-          Env.enter_type (get_new_abstract_name ()) decl !env in
+          Env.enter_type (get_new_abstract_name name) decl !env in
         env := new_env;
-        let to_unify =
-          newty (Tconstr (Path.Pident id,[],ref Mnil)) in 
-        link_type existential to_unify 
+        let to_unify = newty (Tconstr (Path.Pident id,[],ref Mnil)) in 
+        link_type (copy existential) to_unify 
       in
-      List.iter process existentials end;
+      List.iter process cstr.cstr_existentials
+  end;
   cleanup_types ();
   (ty_args, ty_res)
 
@@ -1234,6 +1237,7 @@ let check_abbrev_env env =
     previous_env := env
   end
 
+
 (* Expand an abbreviation. The expansion is memorized. *)
 (*
    Assume the level is greater than the path binding time of the
@@ -1272,7 +1276,7 @@ let expand_abbrev_gen kind find_type_expansion env ty =
             end;
           ty
       | None ->
-          let (params, body) =
+          let (params, body, lv) =
             try find_type_expansion level path env with Not_found ->
               raise Cannot_expand
           in
@@ -1285,6 +1289,17 @@ let expand_abbrev_gen kind find_type_expansion env ty =
               ty.desc <- Tvariant { row with row_name = Some (path, args) }
           | _ -> ()
           end;
+          (* For gadts, remember type as non exportable *)
+          if !trace_gadt_instances then begin
+            match lv with
+              Some lv ->
+                if level < lv then raise (Unify [(ty, newvar2 level)]);
+                Env.add_gadt_instances env lv [ty; ty']
+            | None ->
+                match Env.gadt_instance_level env ty with
+                  Some lv -> Env.add_gadt_instances env lv [ty']
+                | None -> ()
+          end;
           ty'
       end
   | _ ->
@@ -1293,9 +1308,7 @@ let expand_abbrev_gen kind find_type_expansion env ty =
 (* inside objects and variants we do not want to 
    use local constraints *)
 let expand_abbrev ty =
-  let use_local = use_local () in
-  expand_abbrev_gen Public
-    (fun level -> Env.find_type_expansion ~use_local ~level) ty
+  expand_abbrev_gen Public (fun level -> Env.find_type_expansion ~level) ty
 
 let safe_abbrev env ty =
   let snap = Btype.snapshot () in
@@ -1307,15 +1320,7 @@ let safe_abbrev env ty =
 let try_expand_once env ty =
   let ty = repr ty in
   match ty.desc with
-    Tconstr (p, _, _) ->
-      let ty' = repr (expand_abbrev env ty) in
-      if !Clflags.principal then begin
-        match (Env.find_type p env).type_newtype_level with
-          Some lv when ty.level < Env.map_newtype_level env lv  ->
-            link_type ty ty'
-        | _ -> ()
-      end;
-      ty'
+    Tconstr (p, _, _) -> repr (expand_abbrev env ty)
   | _ -> raise Cannot_expand
 
 let _ = forward_try_expand_once := try_expand_once
@@ -1325,11 +1330,16 @@ let _ = forward_try_expand_once := try_expand_once
    May raise Unify, if a recursion was hidden in the type. *)
 let rec try_expand_head env ty =
   let ty' = try_expand_once env ty in
-  begin try
-    try_expand_head env ty'
-  with Cannot_expand ->
-    ty'
-  end
+  let ty'' =
+    try try_expand_head env ty'
+    with Cannot_expand -> ty'
+  in
+  if Env.has_local_constraints env then begin
+    match Env.gadt_instance_level env ty'' with
+      None    -> ()
+    | Some lv -> Env.add_gadt_instance_chain env lv ty
+  end;
+  ty''
 
 (* Expand once the head of a type *)
 let expand_head_once env ty =
@@ -1406,7 +1416,7 @@ let rec full_expand env ty =
 *)
 let generic_abbrev env path =
   try
-    let (_, body) = Env.find_type_expansion path env in
+    let (_, body, _) = Env.find_type_expansion path env in
     (repr body).level = generic_level
   with
     Not_found ->
@@ -1500,6 +1510,9 @@ let occur env ty0 ty =
     merge type_changed old;
     raise (match exn with Occur -> Unify [] | _ -> exn)
 
+let occur_in env ty0 t =
+  try occur env ty0 t; false with Unify _ -> true
+
 (* checks that a local constraint is non recursive *)
 let rec local_non_recursive_abbrev visited env p ty =
   let ty = repr ty in
@@ -1742,111 +1755,53 @@ let get_newtype_level () =
    They need to be removed using this function *)
 let reify env t =
   let newtype_level = get_newtype_level () in
-  let create_fresh_constr lev row = 
-      let decl = new_declaration (Some (newtype_level)) None in
-      let name = 
-        let name = get_new_abstract_name () in 
-        if row then name ^ "#row" else name
-      in
-      let (id, new_env) = Env.enter_type name decl !env in    
-      let t = newty2 lev (Tconstr (Path.Pident id,[],ref Mnil))  in 
-      env := new_env;
-      t
+  let create_fresh_constr lev name = 
+    let decl = new_declaration (Some (newtype_level, newtype_level)) None in
+    let name = get_new_abstract_name name in
+    let (id, new_env) = Env.enter_type name decl !env in    
+    let t = newty2 lev (Tconstr (Path.Pident id,[],ref Mnil))  in 
+    env := new_env;
+    t
   in
-  let rec iterator visited ty = 
-    if TypeSet.mem ty visited then () else
-    let visited = TypeSet.add t visited in
+  let visited = ref TypeSet.empty in
+  let rec iterator ty = 
     let ty = repr ty in
-    match ty.desc with 
-    | Tobject _ ->
-        close_object ty;
-        let tvar = row_variable ty in 
-        let t = create_fresh_constr tvar.level true in 
-        link_type tvar t;
-        iter_type_expr (iterator visited) ty
-    | Tvariant r ->
-        if static_row r then 
-          ()
-        else
-          begin
-            let row = row_repr r in
-            let t = create_fresh_constr row.row_more.level true in
-            let t = 
-              newty2 ty.level
-                (Tvariant 
-                 {row with row_fields=[]; 
-                  row_fixed=true; 
-                  row_more=t});
-            in
-            link_type 
-              row.row_more
-              t
-          end;
-        iter_type_expr (iterator visited) ty
-    | Tvar _ -> 
-        let t = create_fresh_constr ty.level false in
-        link_type ty t
-    | _ ->
-        iter_type_expr (iterator visited) ty
+    if TypeSet.mem ty !visited then () else begin
+      visited := TypeSet.add ty !visited;
+      match ty.desc with
+        Tvar o ->
+          let name = match o with Some s -> s | _ -> "ex" in
+          let t = create_fresh_constr ty.level name in
+          link_type ty t
+      | Tvariant r ->
+          if not (static_row r) then iterator (row_more r);
+          iter_row iterator r
+      | Tconstr (p, _, _) when is_object_type p ->
+          iter_type_expr iterator (full_expand !env ty)
+      | _ ->
+          iter_type_expr iterator ty
+    end
   in
-  iter_type_expr (iterator TypeSet.empty) (full_expand !env t)
+  iterator t
 
-let unify_eq_set = TypePairs.create 10 
-
-let add_type_equality t1 t2 = 
-      let do_it t1 t2 = 
-        TypePairs.add unify_eq_set (t1,t2) ()
-      in    
-      if t1.id <= t2.id then do_it t1 t2 else do_it t2 t1 
-        
 let is_abstract_newtype env p = 
   let decl = Env.find_type p env in 
   not (decl.type_newtype_level = None) &&
   decl.type_manifest = None &&
   decl.type_kind = Type_abstract
 
-let definitely_abstract env p = 
-  let is_abstract p = 
-    let decl = Env.find_type p env in
-    match decl.type_manifest with
-    | Some _ -> false
-    | None ->
-        match decl.type_kind with
-        | Type_abstract -> true
-        | (Type_record _ | Type_variant _) -> false
-  in
-  let in_current_module = 
-    function
-      | Path.Pident _ -> true
-      | (Path.Pdot _ | Path.Papply _) -> false
-  in
-  is_abstract p && in_current_module p
-
+let in_current_module = function
+  | Path.Pident _ -> true
+  | Path.Pdot _ | Path.Papply _ -> false
 
 let in_pervasives p = 
-    try
-      ignore(Env.find_type p Env.initial);
-      true;
-    with
-      _ -> false
-
-let unify_eq env t1 t2 =
-  let umode = actual_mode env in 
-  match umode with
-  | Old ->
-      t1 == t2
-  | Pattern | Expression ->
-      let do_it t1 t2 = 
-        try 
-          TypePairs.find unify_eq_set (t1, t2);
-          true
-        with
-          Not_found ->
-            false
-      in
-      if t1 == t2 then true else
-      if t1.id <= t2.id then do_it t1 t2 else do_it t2 t1 
+    try ignore (Env.find_type p Env.initial); true
+    with Not_found -> false
         
+let is_datatype = function
+    {type_kind = Type_record _ | Type_variant _} -> true
+  | _ -> false
+
 (* mcomp type_pairs subst env t1 t2 does not raise an 
    exception if it is possible that t1 and t2 are actually
    equal, assuming the types in type_pairs are equal and 
@@ -1876,17 +1831,16 @@ 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 _) ->
-                    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) ->
+                  (Tvar _, Tvar _) -> assert false
+                | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _))
+                  when l1 = l2 || not (is_optional l1 || is_optional l2) ->
                   mcomp type_pairs subst env t1 t2;
                   mcomp type_pairs subst env u1 u2;
                 | (Ttuple tl1, Ttuple tl2) ->
                   mcomp_list type_pairs subst env tl1 tl2
-                | (Tconstr (p1, _, _), Tconstr (p2, _, _)) ->
-                  mcomp_type_decl type_pairs subst env p1 p2;
-                | Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2)
+                | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) ->
+                  mcomp_type_decl type_pairs subst env p1 p2 tl1 tl2
+                | (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2))
                   when Path.same p1 p2 && n1 = n2 ->
                   mcomp_list type_pairs subst env tl1 tl2
                 | (Tvariant row1, Tvariant row2) ->
@@ -1908,20 +1862,19 @@ let rec mcomp type_pairs subst env t1 t2 =
                   raise (Unify [])
           end
 
-
 and mcomp_list type_pairs subst env tl1 tl2 =
   if List.length tl1 <> List.length tl2 then
     raise (Unify []);
   List.iter2 (mcomp type_pairs subst env) tl1 tl2
 
 and mcomp_fields type_pairs subst env ty1 ty2 =
-  if not (concrete_object ty1) || not (concrete_object ty2) then
-    fatal_error "object was not closed";
+  if not (concrete_object ty1 && concrete_object ty2) then assert false;
   let (fields2, rest2) = flatten_fields ty2 in
   let (fields1, rest1) = flatten_fields ty1 in
   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
   mcomp type_pairs subst env rest1 rest2;
-  if (miss1 <> []) || (miss2 <> []) then raise (Unify []); 
+  if miss1 <> []  && (object_row ty1).desc = Tnil
+  || miss2 <> []  && (object_row ty2).desc = Tnil then raise (Unify []);
   List.iter
     (function (n, k1, t1, k2, t2) ->
        mcomp_kind k1 k2;
@@ -1939,54 +1892,51 @@ and mcomp_kind k1 k2 =
 and mcomp_row type_pairs subst env row1 row2 =
   let row1 = row_repr row1 and row2 = row_repr row2 in
   let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
-  if not row1.row_closed then fatal_error "variant should be closed";
-  if not row2.row_closed then fatal_error "variant should be closed";
-  if r1 <> [] || r2 <> [] || filter_row_fields false (r1 @ r2) <> []
-  then raise (Unify []);
+  let cannot_erase (_,f) =
+    match row_field_repr f with
+      Rpresent _ -> true
+    | Rabsent | Reither _ -> false
+  in
+  if row1.row_closed && List.exists cannot_erase r2
+  || row2.row_closed && List.exists cannot_erase r1 then raise (Unify []);
   List.iter
     (fun (_,f1,f2) ->
       match row_field_repr f1, row_field_repr f2 with
+      | Rpresent None, (Rpresent (Some _) | Reither (_, _::_, _, _) | Rabsent)
+      | Rpresent (Some _), (Rpresent None | Reither (true, _, _, _) | Rabsent)
+      | (Reither (_, _::_, _, _) | Rabsent), Rpresent None
+      | (Reither (true, _, _, _) | Rabsent), Rpresent (Some _) ->
+          raise (Unify [])
       | Rpresent(Some t1), Rpresent(Some t2) ->
           mcomp type_pairs subst env t1 t2
-      | Reither(true, [], _, _), Reither(true, [], _, _) ->
-          ()
-      | Reither(false, tl1, _, _), Reither(false, tl2, _, _) ->
-          List.iter (fun t ->
-            List.iter (fun t' -> mcomp type_pairs subst env t t') tl1)
-            tl2
-      | Rpresent None, Rpresent None -> ()
-      | Rabsent, Rabsent -> ()
-      | _ -> raise (Unify []))
+      | Rpresent(Some t1), Reither(false, tl2, _, _) ->
+          List.iter (mcomp type_pairs subst env t1) tl2
+      | Reither(false, tl1, _, _), Rpresent(Some t2) ->
+          List.iter (mcomp type_pairs subst env t2) tl1
+      | _ -> ())
     pairs
 
-and mcomp_type_decl type_pairs subst env p1 p2 = 
-  if Path.same p1 p2 then () else
-  let is_current_module = function
-      Path.Pident _ -> true
-    | _ -> false
+and mcomp_type_decl type_pairs subst env p1 p2 tl1 tl2 = 
+  let non_aliased p decl =
+    in_pervasives p ||
+    in_current_module p && decl.type_newtype_level = None
   in
-
   let decl = Env.find_type p1 env in
   let decl' = Env.find_type p2 env in
-  let both_oldtypes =
-    decl.type_newtype_level = None && decl'.type_newtype_level = None in
-  if 
-    (is_current_module p1 && is_current_module p2 && both_oldtypes) ||
-    (in_pervasives p1 && in_pervasives p2)
-  then 
-    raise (Unify [])
-  else
-    match decl.type_kind, decl'.type_kind with
-    | Type_record (lst,r), Type_record (lst',r') ->
-        if r = r' then 
-          mcomp_record_description type_pairs subst env lst lst'
-        else
-          raise (Unify [])
-    | Type_variant v1, Type_variant v2 ->
-        mcomp_variant_description type_pairs subst env v1 v2
-    | _ -> ()
-
-
+  if Path.same p1 p2 then
+    if non_aliased p1 decl then mcomp_list type_pairs subst env tl1 tl2 else ()
+  else match decl.type_kind, decl'.type_kind with
+  | Type_record (lst,r), Type_record (lst',r') when r = r' ->
+      mcomp_list type_pairs subst env tl1 tl2;
+      mcomp_record_description type_pairs subst env lst lst'
+  | Type_variant v1, Type_variant v2 ->
+      mcomp_list type_pairs subst env tl1 tl2;
+      mcomp_variant_description type_pairs subst env v1 v2
+  | Type_variant _, Type_record _
+  | Type_record _, Type_variant _ -> raise (Unify [])
+  | _ ->
+      if non_aliased p1 decl && (non_aliased p2 decl' || is_datatype decl')
+      || is_datatype decl && non_aliased p2 decl' then raise (Unify [])
 
 and mcomp_type_option type_pairs subst env t t' = 
   match t, t' with
@@ -2020,22 +1970,50 @@ and mcomp_record_description type_pairs subst env =
   in
   iter
 
+let mcomp env t1 t2 =
+  mcomp (TypePairs.create 4) () env t1 t2
 
-(* mcomp type_pairs subst env t1 t2 does not raise an 
-   exception if it is possible that t1 and t2 are actually
-   equal. However, if two types are
-   Assumes that both t1 and t2 do not contain any variables
-   and that both their objects and variants are closed
-*)
+(* Real unification *)
 
-let mcomp env t1 t2 = 
-  mcomp (TypePairs.create 4) () env t1 t2
+let find_lowest_level ty =
+  let lowest = ref generic_level in
+  let rec find ty =
+    let ty = repr ty in
+    if ty.level >= lowest_level then begin
+      if ty.level < !lowest then lowest := ty.level;
+      ty.level <- pivot_level - ty.level;
+      iter_type_expr find ty
+    end
+  in find ty; unmark_type ty; !lowest
 
 let find_newtype_level env path = 
   match (Env.find_type path env).type_newtype_level with
-    | None -> assert false
-    | Some x -> x
+    Some x -> x
+  | None -> assert false
         
+let add_gadt_equation env source destination =
+  let destination = duplicate_type destination in 
+  let source_lev = find_newtype_level !env (Path.Pident source) in
+  let decl = new_declaration (Some source_lev) (Some destination) in
+  let newtype_level = get_newtype_level () in
+  env := Env.add_local_constraint source decl newtype_level !env;
+  cleanup_abbrev ()          
+
+let unify_eq_set = TypePairs.create 11
+
+let order_type_pair t1 t2 =
+  if t1.id <= t2.id then (t1, t2) else (t2, t1)
+
+let add_type_equality t1 t2 = 
+  TypePairs.add unify_eq_set (order_type_pair t1 t2) ()
+        
+let unify_eq env t1 t2 =
+  t1 == t2 ||
+  match !umode with
+  | Expression -> false
+  | Pattern ->
+      try TypePairs.find unify_eq_set (order_type_pair t1 t2); true
+      with Not_found -> false
 
 let rec unify (env:Env.t ref) t1 t2 =
   (* First step: special cases (optimizations) *)
@@ -2043,10 +2021,11 @@ let rec unify (env:Env.t ref) t1 t2 =
   let t1 = repr t1 in
   let t2 = repr t2 in
   if unify_eq !env t1 t2 then () else
+  let reset_tracing = check_trace_gadt_instances !env in
   
   try
     type_changed := true;
-    match (t1.desc, t2.desc) with
+    begin match (t1.desc, t2.desc) with
       (Tvar _, Tconstr _) when deep_occur t1 t2 ->
         unify2 env t1 t2
     | (Tconstr _, Tvar _) when deep_occur t2 t1 ->
@@ -2066,7 +2045,7 @@ let rec unify (env:Env.t ref) t1 t2 =
         update_level !env t1.level t2;
         link_type t1 t2
     | (Tconstr (p1, [], a1), Tconstr (p2, [], a2))
-          when Path.same p1 p2 && actual_mode !env = Old
+          when Path.same p1 p2 (* && actual_mode !env = Old *)
             (* This optimization assumes that t1 does not expand to t2
                (and conversely), so we fall back to the general case
                when any of the types has a cached expansion. *)
@@ -2076,7 +2055,10 @@ let rec unify (env:Env.t ref) t1 t2 =
         link_type t1 t2
     | _ ->
         unify2 env t1 t2
+    end;
+    if reset_tracing then trace_gadt_instances := false;
   with Unify trace ->
+    if reset_tracing then trace_gadt_instances := false;
     raise (Unify ((t1, t2)::trace))
 
 and unify2 env t1 t2 =
@@ -2089,9 +2071,30 @@ and unify2 env t1 t2 =
     expand_both t1' t2'
   in
   let t1', t2' = expand_both t1 t2 in
+  let lv = min t1'.level t2'.level in
+  update_level !env lv t2;
+  update_level !env lv t1;
   if unify_eq !env t1' t2' then () else
 
   let t1 = repr t1 and t2 = repr t2 in
+  if !trace_gadt_instances then begin
+    match Env.gadt_instance_level !env t1',Env.gadt_instance_level !env t2' with
+      Some lv1, Some lv2 ->
+        if lv1 > lv2 then Env.add_gadt_instance_chain !env lv1 t2 else
+        if lv2 > lv2 then Env.add_gadt_instance_chain !env lv2 t1
+    | Some lv1, None -> Env.add_gadt_instance_chain !env lv1 t2
+    | None, Some lv2 -> Env.add_gadt_instance_chain !env lv2 t1
+    | None, None     -> ()
+  end;
+  let t1, t2 =
+    if !Clflags.principal
+    && (find_lowest_level t1' < lv || find_lowest_level t2' < lv) then
+      (* Expand abbreviations hiding a lower level *)
+      (* Should also do it for parameterized types, after unification... *)
+      (match t1.desc with Tconstr (_, [], _) -> t1' | _ -> t1),
+      (match t2.desc with Tconstr (_, [], _) -> t2' | _ -> t2)
+    else (t1, t2)
+  in
   if unify_eq !env t1 t1' || not (unify_eq !env t2 t2') then
     unify3 env t1 t1' t2 t2'
   else
@@ -2102,188 +2105,114 @@ and unify3 env t1 t1' t2 t2' =
   (* Third step: truly unification *)
   (* Assumes either [t1 == t1'] or [t2 != t2'] *)
   let d1 = t1'.desc and d2 = t2'.desc in
-  match (d1, d2) with (* handle univars specially *)
+  let create_recursion = (t2 != t2') && (deep_occur t1' t2) in
+
+  begin match (d1, d2) with (* handle vars and univars specially *)
     (Tunivar _, Tunivar _) ->
       unify_univar t1' t2' !univar_pairs;
-      update_level !env t1'.level t2';
       link_type t1' t2'
-  | _ ->    
-
-  let create_recursion = (t2 != t2') && (deep_occur t1' t2) in
-  let old_link () = 
-      occur !env t1' t2';
-      update_level !env t1'.level t2;
-      link_type t1' t2
-  in
-  let umode = actual_mode !env in
-  let switch_to_old_link f = 
-    match umode with
-    | Pattern | Expression ->
-        change_mode Old 
-          (fun () ->
-            old_link (); 
-            f ())
-    | 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;
       link_type t2' t1;
   | _ ->
-      if !Clflags.principal then begin
-        update_level !env t1'.level t2;
-        update_level !env t2'.level t1;
-      end;
+      let umode = !umode in
       begin match umode with
-      | Old ->
-          old_link ()
-      | Pattern | Expression ->
-          add_type_equality t1' t2' end;
-      try
-        begin match (d1, d2) with
-        | (Tvar _, _) 
-        | (_, Tvar _) ->
-            (* cases taken care of *)
-            assert false
-        | (Tarrow (l1, t1, u1, c1), Tarrow (l2, t2, u2, c2)) when l1 = l2
-        || !Clflags.classic && not (is_optional l1 || is_optional l2) ->
-            unify  env t1 t2; unify env  u1 u2;
-            begin match commu_repr c1, commu_repr c2 with
-              Clink r, c2 -> set_commu r c2
-            | c1, Clink r -> set_commu r c1
-            | _ -> ()
-            end
-        | (Ttuple tl1, Ttuple tl2) ->
-            unify_list env tl1 tl2
-        | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
-            unify_list env tl1 tl2
-        | (Tconstr ((Path.Pident p) as path,[],_),
-           Tconstr ((Path.Pident p') as path',[],_))
-          when is_abstract_newtype !env path && is_abstract_newtype !env path'
-          && umode = Pattern -> 
-            let source,destination = 
-              if find_newtype_level !env path > find_newtype_level !env path'
-              then  p,t2'
-              else  p',t1'
-            in
-            let destination = duplicate_type destination in 
-            let source_lev = find_newtype_level !env (Path.Pident source) in
-            let decl = new_declaration (Some source_lev) (Some destination) in
-            let newtype_level = get_newtype_level () in
-            env := Env.add_local_constraint source decl newtype_level !env;
-            cleanup_abbrev ()          
-        | (Tconstr ((Path.Pident p) as path,[],_), _)
-          when is_abstract_newtype !env path && umode = Pattern -> 
-            reify env t2';
-            local_non_recursive_abbrev !env (Path.Pident p) t2';
-            let t2' = duplicate_type t2' in
-            let source_level = find_newtype_level !env path in
-            let decl = new_declaration (Some source_level) (Some t2') in
-            let newtype_level = get_newtype_level () in
-            env := Env.add_local_constraint p decl newtype_level !env;
-            cleanup_abbrev ()          
-        | (_, Tconstr ((Path.Pident p) as path,[],_))
-          when is_abstract_newtype !env path && umode = Pattern -> 
-            reify env t1' ;
-            local_non_recursive_abbrev !env (Path.Pident p) t1';
-            let t1' = duplicate_type t1' in
-            let source_level = find_newtype_level !env path in
-            let decl = new_declaration (Some source_level) (Some t1') in
-            let newtype_level = get_newtype_level () in
-            env := Env.add_local_constraint p decl newtype_level !env;
-            cleanup_abbrev ()
-        | (Tconstr (p1,_,_), Tconstr (p2,_,_)) when umode = Pattern ->
-            reify env t1';
-            reify env t2';
-            mcomp !env t1' t2'
-        | (Tobject (fi1, nm1), Tobject (fi2, _)) ->
-            if concrete_object t1' && concrete_object t2' then
-              unify_fields env fi1 fi2
-            else          
-              switch_to_old_link 
-                (fun () -> unify_fields env fi1 fi2);
-
-            (* 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
+      | Expression ->
+          occur !env t1' t2';
+          link_type t1' t2
+      | Pattern ->
+          add_type_equality t1' t2'
+      end;
+      try match (d1, d2) with
+        (Tarrow (l1, t1, u1, c1), Tarrow (l2, t2, u2, c2)) when l1 = l2 ||
+        !Clflags.classic && not (is_optional l1 || is_optional l2) ->
+          unify  env t1 t2; unify env  u1 u2;
+          begin match commu_repr c1, commu_repr c2 with
+            Clink r, c2 -> set_commu r c2
+          | c1, Clink r -> set_commu r c1
+          | _ -> ()
+          end
+      | (Ttuple tl1, Ttuple tl2) ->
+          unify_list env tl1 tl2
+      | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
+          if umode = Expression || in_current_module p1 || in_pervasives p1
+          || is_datatype (Env.find_type p1 !env)
+          then unify_list env tl1 tl2
+          else set_mode Expression (fun () -> unify_list env tl1 tl2)
+      | (Tconstr ((Path.Pident p) as path,[],_),
+         Tconstr ((Path.Pident p') as path',[],_))
+        when is_abstract_newtype !env path && is_abstract_newtype !env path'
+        && umode = Pattern -> 
+          let source,destination = 
+            if find_newtype_level !env path > find_newtype_level !env path'
+            then  p,t2'
+            else  p',t1'
+          in add_gadt_equation env source destination
+      | (Tconstr ((Path.Pident p) as path,[],_), _)
+        when is_abstract_newtype !env path && umode = Pattern -> 
+          reify env t2';
+          local_non_recursive_abbrev !env (Path.Pident p) t2';
+          add_gadt_equation env p t2'
+      | (_, Tconstr ((Path.Pident p) as path,[],_))
+        when is_abstract_newtype !env path && umode = Pattern -> 
+          reify env t1' ;
+          local_non_recursive_abbrev !env (Path.Pident p) t1';
+          add_gadt_equation env p t1'
+      | (Tconstr (p1,_,_), Tconstr (p2,_,_)) when umode = Pattern ->
+          reify env t1';
+          reify env t2';
+          mcomp !env t1' t2'
+      | (Tobject (fi1, nm1), Tobject (fi2, _)) ->
+          unify_fields env fi1 fi2;
+          (* 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
 	      (match (repr va).desc with
-		Tvar _|Tunivar _|Tnil -> true | _ -> false) ->
-                ()
-            | Tobject (_, nm2) ->
-                set_name nm2 !nm1
-            | _ ->
-                ()
-            end
-        | (Tvariant row1, Tvariant row2) ->
-            switch_to_old_link
-            (fun () -> unify_row env row1 row2)
-        | (Tfield _, Tfield _) ->           (* Actually unused *)
-            unify_fields env t1' t2'
-        | (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) ->
-            begin match field_kind_repr kind with
-              Fvar r when f <> dummy_method -> set_kind r Fabsent
-            | _      -> raise (Unify [])
-            end
-        | (Tnil, Tnil) ->
-            ()
-        | (Tpoly (t1, []), Tpoly (t2, [])) ->
-            unify env t1 t2
-        | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
-            enter_poly !env univar_pairs t1 tl1 t2 tl2 (unify env)
-        | (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2))
-          when Path.same p1 p2 && n1 = n2 ->
-            unify_list env tl1 tl2
-        | (_, _) ->
-            raise (Unify [])
-        end;
-
-(* XXX Commentaires + changer "create_recursion" *)
-        if create_recursion then begin
-          match t2.desc with
-            Tconstr (p, tl, abbrev) ->
-              forget_abbrev abbrev p;
-              let t2'' = expand_head_unif !env t2 in
-              if not (closed_parameterized_type tl t2'') then
-                link_type (repr t2) (repr t2')
-          | _ ->
-              () (* t2 has already been expanded by update_level *)
-        end
-
-(*
-  (*
-    Can only be done afterwards, once the row variable has
-    (possibly) been instantiated.
-   *)
-  if t1 != t1' (* && t2 != t2' *) then begin
-  match (t1.desc, t2.desc) with
-  (Tconstr (p, ty::_, _), _)
-  when ((repr ty).desc <> Tvar)
-  && weak_abbrev p
-  && not (deep_occur t1 t2) ->
-  update_level env t1.level t2;
-  link_type t1 t2
-  | (_, Tconstr (p, ty::_, _))
-  when ((repr ty).desc <> Tvar)
-  && weak_abbrev p
-  && not (deep_occur t2 t1) ->
-  update_level env t2.level t1;
-  link_type t2 t1;
-  link_type t1' t2'
-  | _ ->
-  ()
-  end
- *)
+                Tvar _|Tunivar _|Tnil -> true | _ -> false) -> ()
+          | Tobject (_, nm2) -> set_name nm2 !nm1
+          | _ -> ()
+          end
+      | (Tvariant row1, Tvariant row2) ->
+          unify_row env row1 row2
+      | (Tfield _, Tfield _) ->           (* Actually unused *)
+          unify_fields env t1' t2'
+      | (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) ->
+          begin match field_kind_repr kind with
+            Fvar r when f <> dummy_method -> set_kind r Fabsent
+          | _      -> raise (Unify [])
+          end
+      | (Tnil, Tnil) ->
+          ()
+      | (Tpoly (t1, []), Tpoly (t2, [])) ->
+          unify env t1 t2
+      | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
+          enter_poly !env univar_pairs t1 tl1 t2 tl2 (unify env)
+      | (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2))
+        when Path.same p1 p2 && n1 = n2 ->
+          unify_list env tl1 tl2
+      | (_, _) ->
+          raise (Unify [])
       with Unify trace ->
         t1'.desc <- d1;
         raise (Unify trace)
+  end;
+  (* XXX Commentaires + changer "create_recursion" *)
+  if create_recursion then begin
+    match t2.desc with
+      Tconstr (p, tl, abbrev) ->
+        forget_abbrev abbrev p;
+        let t2'' = expand_head_unif !env t2 in
+        if not (closed_parameterized_type tl t2'') then
+          link_type (repr t2) (repr t2')
+    | _ ->
+        () (* t2 has already been expanded by update_level *)
+  end
 
 and unify_list env tl1 tl2 =
   if List.length tl1 <> List.length tl2 then
@@ -2323,7 +2252,10 @@ and unify_fields env ty1 ty2 =          (* Optimization *)
     List.iter
       (fun (n, k1, t1, k2, t2) ->
         unify_kind k1 k2;
-        try unify env t1 t2 with Unify trace ->
+        try 
+          if !trace_gadt_instances then update_level !env va.level t1;
+          unify env t1 t2 
+        with Unify trace ->
           raise (Unify ((newty (Tfield(n, k1, t1, va)),
                          newty (Tfield(n, k2, t2, va)))::trace)))
       pairs
@@ -2348,7 +2280,7 @@ and unify_pairs mode env tpl =
 and unify_row env row1 row2 =
   let row1 = row_repr row1 and row2 = row_repr row2 in
   let rm1 = row_more row1 and rm2 = row_more row2 in
-  if rm1 == rm2 then () else
+  if unify_eq !env rm1 rm2 then () else
   let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
   if r1 <> [] && r2 <> [] then begin
     let ht = Hashtbl.create (List.length r1) in
@@ -2362,8 +2294,7 @@ and unify_row env row1 row2 =
   let more =
     if row1.row_fixed then rm1 else
     if row2.row_fixed then rm2 else
-    newgenvar ()
-  in update_level !env (min rm1.level rm2.level) more;
+    newty2 (min rm1.level rm2.level) (Tvar None) in
   let fixed = row1.row_fixed || row2.row_fixed
   and closed = row1.row_closed || row2.row_closed in
   let keep switch =
@@ -2403,13 +2334,16 @@ and unify_row env row1 row2 =
       let t1 = mkvariant [] true and t2 = mkvariant rest false in
       raise (Unify [if row == row1 then (t1,t2) else (t2,t1)])
     end;
+    (* The following test is not principal... should rather use Tnil *)
     let rm = row_more row in
+    if !trace_gadt_instances && rm.desc = Tnil then () else
+    if !trace_gadt_instances then
+      update_level !env rm.level (newgenty (Tvariant row));
     if row.row_fixed then
-      if row0.row_more == rm then () else
-      if is_Tvar rm then link_type rm row0.row_more else
-      unify env rm row0.row_more
+      if more == rm then () else
+      if is_Tvar rm then link_type rm more else unify env rm more
     else
-      let ty = newty2 generic_level (Tvariant {row0 with row_fields = rest}) in
+      let ty = newgenty (Tvariant {row0 with row_fields = rest}) in
       update_level !env rm.level ty;
       link_type rm ty
   in
@@ -2463,10 +2397,12 @@ and unify_row_field env fixed1 fixed2 more l f1 f2 =
   | Rabsent, Rabsent -> ()
   | Reither(false, tl, _, e1), Rpresent(Some t2) when not fixed1 ->
       set_row_field e1 f2;
+      update_level !env (repr more).level t2;
       (try List.iter (fun t1 -> unify env t1 t2) tl
       with exn -> e1 := None; raise exn)
   | Rpresent(Some t1), Reither(false, tl, _, e2) when not fixed2 ->
       set_row_field e2 f1;
+      update_level !env (repr more).level t1;
       (try List.iter (unify env t1) tl
       with exn -> e2 := None; raise exn)
   | Reither(true, [], _, e1), Rpresent None when not fixed1 ->
@@ -2478,48 +2414,45 @@ and unify_row_field env fixed1 fixed2 more l f1 f2 =
 
 let unify env ty1 ty2 =
   try
-    TypePairs.clear unify_eq_set;
     unify env ty1 ty2
-  with 
-  | Unify trace ->
+  with
+    Unify trace ->
       raise (Unify (expand_trace !env trace))
   | Recursive_abbrev ->
       raise (Unification_recursive_abbrev (expand_trace !env [(ty1,ty2)]))
 
-
 let unify_gadt ~newtype_level:lev (env:Env.t ref) ty1 ty2 =
   try
     univar_pairs := [];
     newtype_level := Some lev;
     set_mode Pattern (fun () -> unify env ty1 ty2);
     newtype_level := None;
-  with 
-    | Unify e ->
-        raise (Unify e)
-    | e -> 
-        newtype_level := None;
-        raise e
-
+    TypePairs.clear unify_eq_set;
+  with e ->
+    TypePairs.clear unify_eq_set;
+    match e with
+      Unify e -> raise (Unify e)
+    | e -> newtype_level := None; raise e
 
 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 _ ->
+      let reset_tracing = check_trace_gadt_instances env in
       begin try
         occur env t1 t2;
         update_level env t1.level t2;
-        link_type t1 t2
+        link_type t1 t2;
+        if reset_tracing then trace_gadt_instances := false;
       with Unify trace ->
+        if reset_tracing then trace_gadt_instances := false;
         let expanded_trace = expand_trace env ((t1,t2)::trace) in 
         raise (Unify expanded_trace)
       end
   | _ ->
       unify (ref env) t1 t2
 
-let unify_var env t1 t2 = 
-  unify_var env t1 t2
-
 let _ = unify' := unify_var
 
 let unify_pairs env ty1 ty2 pairs =
@@ -2527,8 +2460,7 @@ let unify_pairs env ty1 ty2 pairs =
   unify env ty1 ty2
 
 let unify env ty1 ty2 =
-  univar_pairs := [];
-  unify (ref env) ty1 ty2
+  unify_pairs (ref env) ty1 ty2 []
 
 
 
@@ -2685,14 +2617,11 @@ let rec moregen inst_nongen type_pairs env t1 t2 =
             when Path.same p1 p2 && n1 = n2 ->
               moregen_list inst_nongen type_pairs env tl1 tl2
           | (Tvariant row1, Tvariant row2) ->
-              change_mode Old
-                (fun () -> moregen_row inst_nongen type_pairs env row1 row2)
+              moregen_row inst_nongen type_pairs env row1 row2
           | (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
-              change_mode Old
-                (fun () -> moregen_fields inst_nongen type_pairs env fi1 fi2)
+              moregen_fields inst_nongen type_pairs env fi1 fi2
           | (Tfield _, Tfield _) ->           (* Actually unused *)
-              change_mode Old
-                (fun () -> moregen_fields inst_nongen type_pairs env t1' t2')
+              moregen_fields inst_nongen type_pairs env t1' t2'
           | (Tnil, Tnil) ->
               ()
           | (Tpoly (t1, []), Tpoly (t2, [])) ->
@@ -2741,7 +2670,8 @@ 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 = is_Tvar rm1 && may_instantiate inst_nongen rm1 in
+  let may_inst =
+    is_Tvar rm1 && may_instantiate inst_nongen rm1 || rm1.desc = Tnil in
   let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
   let r1, r2 =
     if row2.row_closed then
@@ -2823,10 +2753,10 @@ let moregeneral env inst_nongen pat_sch subj_sch =
      then copied with [duplicate_type].  That way, its levels won't be
      changed.
   *)
-  let subj = duplicate_type (instance subj_sch) in
+  let subj = duplicate_type (instance env subj_sch) in
   current_level := generic_level;
   (* Duplicate generic variables *)
-  let patt = instance pat_sch in
+  let patt = instance env pat_sch in
   let res =
     try moregen inst_nongen (TypePairs.create 13) env patt subj; true with
       Unify _ -> false
@@ -3747,7 +3677,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 _|Tnil), (Tvar _|Tconstr _|Tnil)
     when row1.row_closed && r1 = [] ->
       List.fold_left
         (fun cstrs (_,f1,f2) ->
@@ -3979,7 +3909,7 @@ let rec nondep_type_rec env id ty =
             (* Register new type first for recursion *)
             TypeHash.add nondep_variants more ty';
             let static = static_row row in
-            let more' = if static then newgenvar () else more in
+            let more' = if static then newgenty Tnil else more in
             (* Return a new copy *)
             let row =
               copy_row (nondep_type_rec env id) true row true more' in
diff --git a/typing/ctype.mli b/typing/ctype.mli
index a08409c650..0c42edafdf 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -106,12 +106,14 @@ val limited_generalize: type_expr -> type_expr -> unit
         (* Only generalize some part of the type
            Make the remaining of the type non-generalizable *)
 
-val instance: ?partial:bool -> type_expr -> type_expr
+val instance: ?partial:bool -> Env.t -> type_expr -> type_expr
         (* Take an instance of a type scheme *)
         (* partial=None  -> normal
            partial=false -> newvar() for non generic subterms
            partial=true  -> newty2 ty.level Tvar for non generic subterms *)
-val instance_list: type_expr list -> type_expr list
+val instance_def: type_expr -> type_expr
+        (* use defaults *)
+val instance_list: Env.t -> type_expr list -> type_expr list
         (* Take an instance of a list of type schemes *)
 val instance_constructor:
         ?in_pattern:Env.t ref * int -> 
@@ -160,6 +162,7 @@ val filter_method: Env.t -> string -> private_flag -> type_expr -> type_expr
         (* A special case of unification (with {m : 'a; 'b}). *)
 val check_filter_method: Env.t -> string -> private_flag -> type_expr -> unit
         (* A special case of unification (with {m : 'a; 'b}), returning unit. *)
+val occur_in: Env.t -> type_expr -> type_expr -> bool
 val deep_occur: type_expr -> type_expr -> bool
 val filter_self_method:
         Env.t -> string -> private_flag -> (Ident.t * type_expr) Meths.t ref ->
diff --git a/typing/datarepr.ml b/typing/datarepr.ml
index 8b8a1722fc..4b4f234c89 100644
--- a/typing/datarepr.ml
+++ b/typing/datarepr.ml
@@ -68,10 +68,7 @@ let constructor_descrs ty_res cstrs priv =
 	  | None -> []
 	  | Some type_ret ->
 	      let res_vars = free_vars type_ret in
-	      let arg_vars = 
-		List.fold_left TypeSet.union TypeSet.empty
-		  (List.map free_vars ty_args)
-	      in
+	      let arg_vars = free_vars (newgenty (Ttuple ty_args)) in
 	      TypeSet.elements (TypeSet.diff arg_vars res_vars)
 	in
 	let cstr =
diff --git a/typing/env.ml b/typing/env.ml
index df811177c6..3f119244f6 100644
--- a/typing/env.ml
+++ b/typing/env.ml
@@ -20,6 +20,7 @@ open Asttypes
 open Longident
 open Path
 open Types
+open Btype
 
 
 type error =
@@ -56,7 +57,7 @@ type t = {
   cltypes: (Path.t * cltype_declaration) Ident.tbl;
   summary: summary;
   local_constraints: bool;
-  level_map: (int * int) list;
+  gadt_instances: (int * TypeSet.t ref) list;
 }
 
 and module_components = module_components_repr Lazy.t
@@ -96,7 +97,7 @@ let empty = {
   modules = Ident.empty; modtypes = Ident.empty;
   components = Ident.empty; classes = Ident.empty;
   cltypes = Ident.empty; 
-  summary = Env_empty; local_constraints = false; level_map = [] }
+  summary = Env_empty; local_constraints = false; gadt_instances = [] }
 
 let diff_keys is_local tbl1 tbl2 =
   let keys2 = Ident.keys tbl2 in
@@ -280,19 +281,13 @@ and find_cltype =
 (* Find the manifest type associated to a type when appropriate:
    - the type should be public or should have a private row,
    - the type should have an associated manifest type. *)
-let find_type_expansion ?(use_local=true) ?level path env =
+let find_type_expansion ?level path env =
   let decl = find_type path env in
-  if not use_local && not (decl.type_newtype_level = None) then raise Not_found;
-  (* the level is changed when updating newtype definitions *)
-  if !Clflags.principal then begin
-    match level, decl.type_newtype_level with
-      Some level, Some def_level when level < def_level -> raise Not_found
-    | _ -> ()
-  end;
   match decl.type_manifest with
   | Some body when decl.type_private = Public
               || decl.type_kind <> Type_abstract
-              || Btype.has_constr_row body -> (decl.type_params, body)
+              || Btype.has_constr_row body ->
+                  (decl.type_params, body, may_map snd decl.type_newtype_level)
   (* The manifest type of Private abstract data types without
      private row are still considered unknown to the type system.
      Hence, this case is caught by the following clause that also handles
@@ -308,7 +303,7 @@ let find_type_expansion_opt path env =
   match decl.type_manifest with
   (* The manifest type of Private abstract data types can still get
      an approximation using their manifest type. *)
-  | Some body -> (decl.type_params, body)
+  | Some body -> (decl.type_params, body, may_map snd decl.type_newtype_level)
   | _ -> raise Not_found
 
 let find_modtype_expansion path env =
@@ -453,32 +448,50 @@ and lookup_class =
 and lookup_cltype =
   lookup (fun env -> env.cltypes) (fun sc -> sc.comp_cltypes)
 
-(* Level handling *)
-
-(* The level map is a list of pairs describing separate segments (lv,lv'),
-   lv < lv', organized in decreasing order.
-   The definition level is obtained by mapping a level in a segment to the
-   high limit of this segment.
-   The definition level of a newtype should be greater or equal to
-   the highest level of the newtypes in its manifest type.
- *)
-
-let rec map_level lv = function
-  | [] -> lv
-  | (lv1, lv2) :: rem ->
-      if lv > lv2 then lv else
-      if lv >= lv1 then lv2 else map_level lv rem
-
-let map_newtype_level env lv = map_level lv env.level_map
-
-(* precondition: lv < lv' *)
-let rec add_level lv lv' = function
-  | [] -> [lv, lv']
-  | (lv1, lv2) :: rem as l ->
-      if lv2 < lv then (lv, lv') :: l else
-      if lv' < lv1 then (lv1, lv2) :: add_level lv lv' rem
-      else add_level (max lv lv1) (min lv' lv2) rem      
-
+(* GADT instance tracking *)
+
+let add_gadt_instance_level lv env =
+  {env with
+   gadt_instances = (lv, ref TypeSet.empty) :: env.gadt_instances}
+
+let is_Tlink = function {desc = Tlink _} -> true | _ -> false
+
+let gadt_instance_level env t =
+  let rec find_instance = function
+      [] -> None
+    | (lv, r) :: rem ->
+        if TypeSet.exists is_Tlink !r then
+          (* Should we use set_typeset ? *)
+          r := TypeSet.fold (fun ty -> TypeSet.add (repr ty)) !r TypeSet.empty;
+        if TypeSet.mem t !r then Some lv else find_instance rem
+  in find_instance env.gadt_instances
+
+let add_gadt_instances env lv tl =
+  let r =
+    try List.assoc lv env.gadt_instances with Not_found -> assert false in
+  (* Format.eprintf "Added";
+  List.iter (fun ty -> Format.eprintf "@ %a" !Btype.print_raw ty) tl;
+  Format.eprintf "@."; *)
+  set_typeset r (List.fold_right TypeSet.add tl !r)
+
+(* Only use this after expand_head! *)
+let add_gadt_instance_chain env lv t =
+  let r =
+    try List.assoc lv env.gadt_instances with Not_found -> assert false in
+  let rec add_instance t =
+    let t = repr t in
+    if not (TypeSet.mem t !r) then begin
+      (* Format.eprintf "@ %a" !Btype.print_raw t; *)
+      set_typeset r (TypeSet.add t !r);
+      match t.desc with
+        Tconstr (p, _, memo) ->
+          may add_instance (find_expans Private p !memo)
+      | _ -> ()
+    end
+  in
+  (* Format.eprintf "Added chain"; *)
+  add_instance t
+  (* Format.eprintf "@." *)
 
 (* Expand manifest module type names at the top of the given module type *)
 
@@ -497,7 +510,7 @@ let rec scrape_modtype mty env =
 let constructors_of_type ty_path decl =
   let handle_variants cstrs = 
     Datarepr.constructor_descrs
-      (Btype.newgenty (Tconstr(ty_path, decl.type_params, ref Mnil)))
+      (newgenty (Tconstr(ty_path, decl.type_params, ref Mnil)))
       cstrs decl.type_private
   in
   match decl.type_kind with
@@ -510,7 +523,7 @@ let labels_of_type ty_path decl =
   match decl.type_kind with
     Type_record(labels, rep) ->
       Datarepr.label_descrs
-        (Btype.newgenty (Tconstr(ty_path, decl.type_params, ref Mnil)))
+        (newgenty (Tconstr(ty_path, decl.type_params, ref Mnil)))
         labels rep decl.type_private
   | Type_variant _ | Type_abstract -> []
 
@@ -773,14 +786,13 @@ and add_class id ty env =
 and add_cltype id ty env =
   store_cltype id (Pident id) ty env
 
-let add_local_constraint id info mlv env =
+let add_local_constraint id info elv env =
   match info with
-    {type_manifest = Some ty; type_newtype_level = Some lv} ->
-      (* use the newtype level for this definition, lv is the old one *)
-      let env = add_type id {info with type_newtype_level = Some mlv} env in
-      let level_map =
-        if lv < mlv then add_level lv mlv env.level_map else env.level_map in
-      { env with local_constraints = true; level_map = level_map }
+    {type_manifest = Some ty; type_newtype_level = Some (lv, _)} ->
+      (* elv is the expansion level, lv is the definition level *)
+      let env =
+        add_type id {info with type_newtype_level = Some (lv, elv)} env in
+      { env with local_constraints = true }
   | _ -> assert false
 
 (* Insertion of bindings by name *)
diff --git a/typing/env.mli b/typing/env.mli
index 9260b9e657..5816b0fdca 100644
--- a/typing/env.mli
+++ b/typing/env.mli
@@ -33,14 +33,18 @@ val find_class: Path.t -> t -> class_declaration
 val find_cltype: Path.t -> t -> cltype_declaration
 
 val find_type_expansion:
-    ?use_local:bool -> ?level:int -> Path.t -> t -> type_expr list * type_expr
-val find_type_expansion_opt: Path.t -> t -> type_expr list * type_expr
+    ?level:int -> Path.t -> t -> type_expr list * type_expr * int option
+val find_type_expansion_opt:
+    Path.t -> t -> type_expr list * type_expr * int option
 (* Find the manifest type information associated to a type for the sake
    of the compiler's type-based optimisations. *)
 val find_modtype_expansion: Path.t -> t -> Types.module_type
 
 val has_local_constraints: t -> bool
-val map_newtype_level: t -> int -> int
+val add_gadt_instance_level: int -> t -> t
+val gadt_instance_level: t -> type_expr -> int option
+val add_gadt_instances: t -> int -> type_expr list -> unit
+val add_gadt_instance_chain: t -> int -> type_expr -> unit
 
 (* Lookup by long identifiers *)
 
diff --git a/typing/includecore.ml b/typing/includecore.ml
index 50f5473935..78348eb408 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -61,7 +61,10 @@ 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) &&
+      begin match row1.row_more with
+        {desc=Tvar _|Tconstr _|Tnil} -> true
+      | _ -> false
+      end &&
       let r1, r2, pairs =
         Ctype.merge_row_fields row1.row_fields row2.row_fields in
       (not row2.row_closed ||
diff --git a/typing/includemod.ml b/typing/includemod.ml
index e95b07ffaa..70112c7b27 100644
--- a/typing/includemod.ml
+++ b/typing/includemod.ml
@@ -338,7 +338,7 @@ open Printtyp
 
 let show_loc msg ppf loc =
   let pos = loc.Location.loc_start in
-  if List.mem pos.Lexing.pos_fname [""; "_none_"] then ()
+  if List.mem pos.Lexing.pos_fname [""; "_none_"; "//toplevel//"] then ()
   else fprintf ppf "@\n@[<2>%a:@ %s@]" Location.print_loc loc msg
 
 let show_locs ppf (loc1, loc2) =
diff --git a/typing/parmatch.ml b/typing/parmatch.ml
index 518f6f3b56..015d1d6085 100644
--- a/typing/parmatch.ml
+++ b/typing/parmatch.ml
@@ -377,15 +377,15 @@ let discr_pat q pss =
   | (({pat_desc = Tpat_lazy _} as p)::_)::_ -> normalize_pat p
   | (({pat_desc = Tpat_record largs} as p)::_)::pss ->
       let new_omegas =
-        List.fold_left
-          (fun r (lbl,_) ->
+        List.fold_right
+          (fun (lbl,_) r ->
             try
               let _ = get_field lbl.lbl_pos r in
               r
             with Not_found ->
               (lbl,omega)::r)
-          (record_arg acc)
-          largs in
+          largs (record_arg acc)
+      in
       acc_pat
         (make_pat (Tpat_record new_omegas) p.pat_type p.pat_env)
         pss
@@ -2022,4 +2022,5 @@ let check_partial_gadt pred loc casel =
   | Partial -> Partial
   | Total -> 
       (* checks for missing GADT constructors *)
-      check_partial_param (do_check_partial_gadt pred) do_check_fragile_gadt loc casel
+      check_partial_param (do_check_partial_gadt pred)
+        do_check_fragile_gadt loc casel
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index bac8b1a6d8..b74bbe3ccb 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -933,6 +933,8 @@ let rec trace fst txt ppf = function
   | _ -> ()
 
 let rec filter_trace = function
+  | (_, t1') :: (_, t2') :: [] when is_Tvar t1' || is_Tvar t2' ->
+      []
   | (t1, t1') :: (t2, t2') :: rem ->
       let rem' = filter_trace rem in
       if t1 == t1' && t2 == t2'
@@ -969,10 +971,8 @@ let print_tags ppf fields =
 let has_explanation unif t3 t4 =
   match t3.desc, t4.desc with
     Tfield _, _ | _, Tfield _
-  | Tunivar _, Tvar _ | Tvar _, Tunivar _
+  | _, Tvar _ | Tvar _, _
   | Tvariant _, Tvariant _ -> true
-  | Tconstr (p, _, _), Tvar _ | Tvar _, Tconstr (p, _, _) ->
-      unif && min t3.level t4.level < Path.binding_time p
   | _ -> false
 
 let rec mismatch unif = function
@@ -990,18 +990,27 @@ let explanation unif t3 t4 ppf =
   | Tfield _, Tvar _ | Tvar _, Tfield _ ->
       fprintf ppf "@,Self type cannot escape its class"
   | Tconstr (p, tl, _), Tvar _
-    when unif && (tl = [] || t4.level < Path.binding_time p) ->
+    when unif && t4.level < Path.binding_time p ->
       fprintf ppf
         "@,@[The type constructor@;<1 2>%a@ would escape its scope@]"
         path p
   | Tvar _, Tconstr (p, tl, _)
-    when unif && (tl = [] || t3.level < Path.binding_time p) ->
+    when unif && t3.level < Path.binding_time p ->
       fprintf ppf
         "@,@[The type constructor@;<1 2>%a@ would escape its scope@]"
         path p
   | Tvar _, Tunivar _ | Tunivar _, Tvar _ ->
       fprintf ppf "@,The universal variable %a would escape its scope"
         type_expr (if is_Tunivar t3 then t3 else t4)
+  | Tvar _, _ | _, Tvar _ ->
+      let t, t' = if is_Tvar t3 then (t3, t4) else (t4, t3) in
+      if occur_in Env.empty t t' then
+        fprintf ppf "@,@[<hov>The type variable %a occurs inside@ %a@]"
+          type_expr t type_expr t'
+      else
+        fprintf ppf "@,@[<hov>This instance of %a is ambiguous:@ %s@]"
+          type_expr t'
+          "it would escape the scope of its equation"
   | Tfield (lab, _, _, _), _
   | _, Tfield (lab, _, _, _) when lab = dummy_method ->
       fprintf ppf
diff --git a/typing/subst.ml b/typing/subst.ml
index 3b4e18a596..cd8a24e350 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -78,14 +78,13 @@ let newpersty desc =
 let rec typexp s ty =
   let ty = repr ty in
   match ty.desc with
-    Tvar _ | Tunivar _ ->
+    Tvar _ | Tunivar _ as desc ->
       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 desc
           else newty2 ty.level desc
         in
-        save_desc ty ty.desc; ty.desc <- Tsubst ty'; ty'
+        save_desc ty desc; ty.desc <- Tsubst ty'; ty'
       else ty
   | Tsubst ty ->
       ty
@@ -129,7 +128,7 @@ let rec typexp s ty =
               let more' =
                 match more.desc with
                   Tsubst ty -> ty
-                | Tconstr _ -> typexp s more
+                | Tconstr _ | Tnil -> typexp s more
                 | Tunivar _ | Tvar _ ->
                     save_desc more more.desc;
                     if s.for_saving then newpersty more.desc else
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index aa0224c613..c073ca5b69 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -202,11 +202,12 @@ let enter_met_env lab kind ty val_env met_env par_env =
 
 (* Enter an instance variable in the environment *)
 let enter_val cl_num vars inh lab mut virt ty val_env met_env par_env loc =
+  let instance = Ctype.instance val_env in
   let (id, virt) =
     try
       let (id, mut', virt', ty') = Vars.find lab !vars in
       if mut' <> mut then raise (Error(loc, Mutability_mismatch(lab, mut)));
-      Ctype.unify val_env (Ctype.instance ty) (Ctype.instance ty');
+      Ctype.unify val_env (instance ty) (instance ty');
       (if not inh then Some id else None),
       (if virt' = Concrete then virt' else virt)
     with
@@ -607,7 +608,8 @@ let rec class_field cl_num self_type meths vars
           Ctype.raise_nongen_level ();
           let meth_type =
             Ctype.newty
-              (Tarrow ("", self_type, Ctype.instance Predef.type_unit, Cok)) in
+              (Tarrow ("", self_type,
+                       Ctype.instance_def Predef.type_unit, Cok)) in
           vars := vars_local;
           let texp = type_expect met_env expr meth_type in
           Ctype.end_def ();
@@ -828,7 +830,8 @@ and class_expr cl_num val_env met_env scl =
           Warnings.Unerasable_optional_argument;
       rc {cl_desc = Tclass_fun (pat, pv, cl, partial);
           cl_loc = scl.pcl_loc;
-          cl_type = Tcty_fun (l, Ctype.instance pat.pat_type, cl.cl_type);
+          cl_type = Tcty_fun
+            (l, Ctype.instance_def pat.pat_type, cl.cl_type);
           cl_env = val_env}
   | Pcl_apply (scl', sargs) ->
       let cl = class_expr cl_num val_env met_env scl' in
@@ -990,7 +993,7 @@ let rec approx_declaration cl =
   match cl.pcl_desc with
     Pcl_fun (l, _, _, cl) ->
       let arg =
-        if Btype.is_optional l then Ctype.instance var_option
+        if Btype.is_optional l then Ctype.instance_def var_option
         else Ctype.newvar () in
       Ctype.newty (Tarrow (l, arg, approx_declaration cl, Cok))
   | Pcl_let (_, _, cl) ->
@@ -1003,7 +1006,7 @@ let rec approx_description ct =
   match ct.pcty_desc with
     Pcty_fun (l, _, ct) ->
       let arg =
-        if Btype.is_optional l then Ctype.instance var_option
+        if Btype.is_optional l then Ctype.instance_def var_option
         else Ctype.newvar () in
       Ctype.newty (Tarrow (l, arg, approx_description ct, Cok))
   | _ -> Ctype.newvar ()
@@ -1170,7 +1173,7 @@ let class_infos define_class kind
   begin try
     Ctype.unify env
       (constructor_type constr obj_type)
-      (Ctype.instance constr_type)
+      (Ctype.instance env constr_type)
   with Ctype.Unify trace ->
     raise(Error(cl.pci_loc,
                 Constructor_type_mismatch (cl.pci_name, trace)))
@@ -1230,7 +1233,7 @@ let class_infos define_class kind
      cty_new =
        match cl.pci_virt with
          Virtual  -> None
-       | Concrete -> Some (Ctype.instance constr_type)}
+       | Concrete -> Some (Ctype.instance env constr_type)}
   in
   let obj_abbr =
     {type_params = obj_params;
@@ -1418,7 +1421,7 @@ let rec unify_parents env ty cl =
       begin try
         let decl = Env.find_class p env in
         let _, body = Ctype.find_cltype_for_path env decl.cty_path in
-        Ctype.unify env ty (Ctype.instance body)
+        Ctype.unify env ty (Ctype.instance env body)
       with exn -> assert (exn = Not_found)
       end
   | Tclass_structure st -> unify_parents_struct env ty st
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 6e615a78ff..9deb1be40b 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -105,13 +105,13 @@ let rp node =
 (* Typing of constants *)
 
 let type_constant = function
-    Const_int _ -> instance Predef.type_int
-  | Const_char _ -> instance Predef.type_char
-  | Const_string _ -> instance Predef.type_string
-  | Const_float _ -> instance Predef.type_float
-  | Const_int32 _ -> instance Predef.type_int32
-  | Const_int64 _ -> instance Predef.type_int64
-  | Const_nativeint _ -> instance Predef.type_nativeint
+    Const_int _ -> instance_def Predef.type_int
+  | Const_char _ -> instance_def Predef.type_char
+  | Const_string _ -> instance_def Predef.type_string
+  | Const_float _ -> instance_def Predef.type_float
+  | Const_int32 _ -> instance_def Predef.type_int32
+  | Const_int64 _ -> instance_def Predef.type_int64
+  | Const_nativeint _ -> instance_def Predef.type_nativeint
 
 (* Specific version of type_option, using newty rather than newgenty *)
 
@@ -650,7 +650,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
   | Ppat_array spl ->
       let ty_elt = newvar() in
       unify_pat_types
-        loc !env (instance (Predef.type_array ty_elt)) expected_ty;
+        loc !env (instance_def (Predef.type_array ty_elt)) expected_ty;
       let spl_ann = List.map (fun p -> (p,newvar())) spl in
       let pl = List.map (fun (p,t) -> type_pat p ty_elt) spl_ann in
       rp {
@@ -675,7 +675,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
         pat_env = !env }
   | Ppat_lazy sp1 ->
       let nv = newvar () in
-      unify_pat_types loc !env (instance (Predef.type_lazy_t nv)) expected_ty;
+      unify_pat_types loc !env (instance_def (Predef.type_lazy_t nv)) expected_ty;
       let p1 = type_pat sp1 nv in
       rp {
         pat_desc = Tpat_lazy p1;
@@ -920,7 +920,7 @@ external format_to_string :
 
 let type_format loc fmt =
 
-  let ty_arrow gty ty = newty (Tarrow ("", instance gty, ty, Cok)) in
+  let ty_arrow gty ty = newty (Tarrow ("", instance_def gty, ty, Cok)) in
 
   let bad_conversion fmt i c =
     raise (Error (loc, Bad_conversion (fmt, i, c))) in
@@ -1208,13 +1208,24 @@ let create_package_type loc env (p, l) =
                    List.map (Typetexp.transl_simple_type env false)
                      (List.map snd l)))
 
-let iter_ppat f p =
+let wrap_unpacks sexp unpacks =
+  List.fold_left
+    (fun sexp (name, loc) ->
+      {pexp_loc = sexp.pexp_loc; pexp_desc = Pexp_letmodule (
+       name,
+       {pmod_loc = loc; pmod_desc = Pmod_unpack
+          {pexp_desc=Pexp_ident(Longident.Lident name); pexp_loc=loc}},
+       sexp)})
+    sexp unpacks
+
+(* Helpers for type_cases *)
+let iter_ppat f p = 
   match p.ppat_desc with
-  | Ppat_any | Ppat_var _ | Ppat_constant _
-  | Ppat_type _ | Ppat_unpack _ | Ppat_construct _ -> ()
+  | Ppat_any | Ppat_var _ | Ppat_constant _ 
+  | Ppat_type _ | Ppat_unpack _ -> ()    
   | Ppat_array pats -> List.iter f pats
   | Ppat_or (p1,p2) -> f p1; f p2
-  | Ppat_variant (label, arg) -> may f arg
+  | Ppat_variant (_, arg) | Ppat_construct (_, arg, _) -> may f arg
   | Ppat_tuple lst ->  List.iter f lst
   | Ppat_alias (p,_) | Ppat_constraint (p,_) | Ppat_lazy p -> f p
   | Ppat_record (args, flag) -> List.iter (fun (_,p) -> f p) args
@@ -1227,15 +1238,38 @@ let contains_polymorphic_variant p =
   in
   try loop p; false with Exit -> true
 
-let wrap_unpacks sexp unpacks =
+let contains_gadt env p =
+  let rec loop p =
+    match p.ppat_desc with
+      Ppat_construct (lid, _, _) ->
+        begin try
+          if (Env.lookup_constructor lid env).cstr_generalized then raise Exit
+        with Not_found -> ()
+        end; iter_ppat loop p
+    | _ -> iter_ppat loop p
+  in
+  try loop p; false with Exit -> true
+
+let dummy_expr = {pexp_desc = Pexp_tuple []; pexp_loc = Location.none}
+
+(* Duplicate types of values in the environment *)
+(* XXX Should we do something about global type variables too? *)
+let duplicate_ident_types loc caselist env =
+  let caselist =
+    List.filter (fun (pat, _) -> contains_gadt env pat) caselist in
+  let idents = Unused_var.free_idents
+      {pexp_desc = Pexp_match(dummy_expr,caselist); pexp_loc = loc} in
   List.fold_left
-    (fun sexp (name, loc) ->
-      {pexp_loc = sexp.pexp_loc; pexp_desc = Pexp_letmodule (
-       name,
-       {pmod_loc = loc; pmod_desc = Pmod_unpack
-          {pexp_desc=Pexp_ident(Longident.Lident name); pexp_loc=loc}},
-       sexp)})
-    sexp unpacks
+    (fun env s ->
+      try
+        let (path, desc) = Typetexp.find_value env loc (Longident.Lident s) in
+        match path with
+          Path.Pident id ->
+            let desc = {desc with val_type = correct_levels desc.val_type} in
+            Env.add_value id desc env
+        | _ -> env
+      with Not_found -> env)
+    env idents
 
 (* Typing of expressions *)
 
@@ -1259,7 +1293,7 @@ and type_expect ?in_function env sexp ty_expected =
   (* Record the expression type before unifying it with the expected type *)
   let rue exp =
     Stypes.record (Stypes.Ti_expr exp);
-    unify_exp env exp (instance ty_expected);
+    unify_exp env exp (instance env ty_expected);
     exp
   in
   match sexp.pexp_desc with
@@ -1292,7 +1326,7 @@ and type_expect ?in_function env sexp ty_expected =
                 Texp_ident(path, desc)
             end;
           exp_loc = loc;
-          exp_type = instance desc.val_type;
+          exp_type = instance env desc.val_type;
           exp_env = env }
       end
   | Pexp_constant(Const_string s as cst) ->
@@ -1304,7 +1338,7 @@ and type_expect ?in_function env sexp ty_expected =
            begin match (repr (expand_head env ty_expected)).desc with
              Tconstr(path, _, _) when Path.same path Predef.path_format6 ->
                type_format loc s
-           | _ -> instance Predef.type_string
+           | _ -> instance_def Predef.type_string
            end;
         exp_env = env }
   | Pexp_constant cst ->
@@ -1313,6 +1347,10 @@ and type_expect ?in_function env sexp ty_expected =
         exp_loc = loc;
         exp_type = type_constant cst;
         exp_env = env }
+  | Pexp_let(Nonrecursive, [spat, sval], sbody) when contains_gadt env spat ->
+      type_expect ?in_function env
+        {sexp with pexp_desc = Pexp_match (sval, [spat, sbody])}
+        ty_expected
   | Pexp_let(rec_flag, spat_sexp_list, sbody) ->
       let scp =
         match rec_flag with
@@ -1372,11 +1410,12 @@ and type_expect ?in_function env sexp ty_expected =
   | Pexp_function (l, _, caselist) ->
       let (loc_fun, ty_fun) =
         match in_function with Some p -> p
-        | None -> (loc, instance ty_expected)
+        | None -> (loc, instance env ty_expected)
       in
-      if !Clflags.principal then begin_def ();
+      let separate = !Clflags.principal || Env.has_local_constraints env in
+      if separate then begin_def ();
       let (ty_arg, ty_res) =
-        try filter_arrow env (instance ty_expected) l
+        try filter_arrow env (instance env ty_expected) l
         with Unify _ ->
           match expand_head env ty_expected with
             {desc = Tarrow _} as ty ->
@@ -1395,7 +1434,7 @@ and type_expect ?in_function env sexp ty_expected =
           type_option tv
         else ty_arg
       in
-      if !Clflags.principal then begin
+      if separate then begin
         end_def ();
         generalize_structure ty_arg;
         generalize_structure ty_res
@@ -1413,7 +1452,7 @@ and type_expect ?in_function env sexp ty_expected =
       re {
         exp_desc = Texp_function(cases, partial);
         exp_loc = loc;
-        exp_type = instance (newgenty (Tarrow(l, ty_arg, ty_res, Cok)));
+        exp_type = instance env (newgenty (Tarrow(l, ty_arg, ty_res, Cok)));
         exp_env = env }
   | Pexp_apply(sfunct, sargs) ->
       begin_def (); (* one more level for non-returning functions *)
@@ -1432,7 +1471,7 @@ and type_expect ?in_function env sexp ty_expected =
             lower_args (ty::seen) ty_fun
         | _ -> ()
       in
-      let ty = instance funct.exp_type in
+      let ty = instance env funct.exp_type in
       end_def ();
       lower_args [] ty;
       begin_def ();
@@ -1445,19 +1484,18 @@ and type_expect ?in_function env sexp ty_expected =
         exp_type = ty_res;
         exp_env = env }
   | Pexp_match(sarg, caselist) ->
-      if !Clflags.principal then begin_def ();
+      begin_def ();
       let arg = type_exp env sarg in
-      if !Clflags.principal then begin
-          end_def ();
-          generalize_structure arg.exp_type;
-      end;
+      end_def ();
+      if is_nonexpansive arg then generalize arg.exp_type
+      else generalize_expansive env arg.exp_type;
       let cases, partial =
         type_cases env arg.exp_type ty_expected true loc caselist
       in
       re {
         exp_desc = Texp_match(arg, cases, partial);
         exp_loc = loc;
-        exp_type = instance ty_expected;
+        exp_type = instance env ty_expected;
         exp_env = env }
   | Pexp_try(sbody, caselist) ->
       let body = type_expect env sbody ty_expected in
@@ -1485,7 +1523,7 @@ and type_expect ?in_function env sexp ty_expected =
       type_construct env loc lid sarg explicit_arity ty_expected
   | Pexp_variant(l, sarg) ->
       (* Keep sharing *)
-      let ty_expected0 = instance ty_expected in
+      let ty_expected0 = instance env ty_expected in
       begin try match
         sarg, expand_head env ty_expected, expand_head env ty_expected0 with
       | Some sarg, {desc = Tvariant row}, {desc = Tvariant row0} ->
@@ -1540,7 +1578,7 @@ and type_expect ?in_function env sexp ty_expected =
                 let _, ty_arg1, ty_res1 = instance_label false lbl
                 and _, ty_arg2, ty_res2 = instance_label false lbl in
                 unify env ty_exp ty_res1;
-                unify env (instance ty_expected) ty_res2;
+                unify env (instance env ty_expected) ty_res2;
                 unify env ty_arg1 ty_arg2
               end in
             Array.iter unify_kept lbl.lbl_all;
@@ -1572,7 +1610,7 @@ and type_expect ?in_function env sexp ty_expected =
       re {
         exp_desc = Texp_record(lbl_exp_list, opt_exp);
         exp_loc = loc;
-        exp_type = instance ty_expected;
+        exp_type = instance env ty_expected;
         exp_env = env }
   | Pexp_field(sarg, lid) ->
       let arg = type_exp env sarg in
@@ -1594,7 +1632,7 @@ and type_expect ?in_function env sexp ty_expected =
       rue {
         exp_desc = Texp_setfield(record, label, newval);
         exp_loc = loc;
-        exp_type = instance Predef.type_unit;
+        exp_type = instance_def Predef.type_unit;
         exp_env = env }
   | Pexp_array(sargl) ->
       let ty = newgenvar() in
@@ -1604,7 +1642,7 @@ and type_expect ?in_function env sexp ty_expected =
       re {
         exp_desc = Texp_array argl;
         exp_loc = loc;
-        exp_type = instance ty_expected;
+        exp_type = instance env ty_expected;
         exp_env = env }
   | Pexp_ifthenelse(scond, sifso, sifnot) ->
       let cond = type_expect env scond Predef.type_bool in
@@ -1641,13 +1679,13 @@ and type_expect ?in_function env sexp ty_expected =
       rue {
         exp_desc = Texp_while(cond, body);
         exp_loc = loc;
-        exp_type = instance Predef.type_unit;
+        exp_type = instance_def Predef.type_unit;
         exp_env = env }
   | Pexp_for(param, slow, shigh, dir, sbody) ->
       let low = type_expect env slow Predef.type_int in
       let high = type_expect env shigh Predef.type_int in
       let (id, new_env) =
-        Env.enter_value param {val_type = instance Predef.type_int;
+        Env.enter_value param {val_type = instance_def Predef.type_int;
                                val_kind = Val_reg;
                                val_loc = loc;
                               } env in
@@ -1655,31 +1693,32 @@ and type_expect ?in_function env sexp ty_expected =
       rue {
         exp_desc = Texp_for(id, low, high, dir, body);
         exp_loc = loc;
-        exp_type = instance Predef.type_unit;
+        exp_type = instance_def Predef.type_unit;
         exp_env = env }
   | Pexp_constraint(sarg, sty, sty') ->
+      let separate = !Clflags.principal || Env.has_local_constraints env in
       let (arg, ty') =
         match (sty, sty') with
           (None, None) ->               (* Case actually unused *)
             let arg = type_exp env sarg in
             (arg, arg.exp_type)
         | (Some sty, None) ->
-            if !Clflags.principal then begin_def ();
+            if separate then begin_def ();
             let ty = Typetexp.transl_simple_type env false sty in
-            if !Clflags.principal then begin
+            if separate then begin
               end_def ();
               generalize_structure ty;
-              (type_argument env sarg ty (instance ty), instance ty)
+              (type_argument env sarg ty (instance env ty), instance env ty)
             end else
               (type_argument env sarg ty ty, ty)
         | (None, Some sty') ->
             let (ty', force) =
               Typetexp.transl_simple_type_delayed env sty'
             in
-            if !Clflags.principal then begin_def ();
+            if separate then begin_def ();
             let arg = type_exp env sarg in
             let gen =
-              if !Clflags.principal then begin
+              if separate then begin
                 end_def ();
                 let tv = newvar () in
                 let gen = generalizable tv.level arg.exp_type in
@@ -1723,7 +1762,7 @@ and type_expect ?in_function env sexp ty_expected =
             end;
             (arg, ty')
         | (Some sty, Some sty') ->
-            if !Clflags.principal then begin_def ();
+            if separate then begin_def ();
             let (ty, force) =
               Typetexp.transl_simple_type_delayed env sty
             and (ty', force') =
@@ -1735,11 +1774,11 @@ and type_expect ?in_function env sexp ty_expected =
             with Subtype (tr1, tr2) ->
               raise(Error(loc, Not_subtype(tr1, tr2)))
             end;
-            if !Clflags.principal then begin
+            if separate then begin
               end_def ();
               generalize_structure ty;
               generalize_structure ty';
-              (type_argument env sarg ty (instance ty), instance ty')
+              (type_argument env sarg ty (instance env ty), instance env ty')
             end else
               (type_argument env sarg ty ty, ty')
       in
@@ -1788,7 +1827,7 @@ and type_expect ?in_function env sexp ty_expected =
                   let method_type = newvar () in
                   let (obj_ty, res_ty) = filter_arrow env method_type "" in
                   unify env obj_ty desc.val_type;
-                  unify env res_ty (instance typ);
+                  unify env res_ty (instance env typ);
                   (Texp_apply({ exp_desc = Texp_ident(Path.Pident method_id,
                                                      {val_type = method_type;
                                                       val_kind = Val_reg;
@@ -1817,7 +1856,7 @@ and type_expect ?in_function env sexp ty_expected =
         let typ =
           match repr typ with
             {desc = Tpoly (ty, [])} ->
-              instance ty
+              instance env ty
           | {desc = Tpoly (ty, tl); level = l} ->
               if !Clflags.principal && l <> generic_level then
                 Location.prerr_warning loc
@@ -1825,7 +1864,7 @@ and type_expect ?in_function env sexp ty_expected =
               snd (instance_poly false tl ty)
           | {desc = Tvar _} as ty ->
               let ty' = newvar () in
-              unify env (instance ty) (newty(Tpoly(ty',[])));
+              unify env (instance_def ty) (newty(Tpoly(ty',[])));
               (* if not !Clflags.nolabels then
                  Location.prerr_warning loc (Warnings.Unknown_method met); *)
               ty'
@@ -1849,7 +1888,7 @@ and type_expect ?in_function env sexp ty_expected =
             rue {
               exp_desc = Texp_new (cl_path, cl_decl);
               exp_loc = loc;
-              exp_type = instance ty;
+              exp_type = instance_def ty;
               exp_env = env }
         end
   | Pexp_setinstvar (lab, snewval) ->
@@ -1857,14 +1896,14 @@ and type_expect ?in_function env sexp ty_expected =
         let (path, desc) = Env.lookup_value (Longident.Lident lab) env in
         match desc.val_kind with
           Val_ivar (Mutable, cl_num) ->
-            let newval = type_expect env snewval (instance desc.val_type) in
+            let newval = type_expect env snewval (instance env desc.val_type) in
             let (path_self, _) =
               Env.lookup_value (Longident.Lident ("self-" ^ cl_num)) env
             in
             rue {
               exp_desc = Texp_setinstvar(path_self, path, newval);
               exp_loc = loc;
-              exp_type = instance Predef.type_unit;
+              exp_type = instance_def Predef.type_unit;
               exp_env = env }
         | Val_ivar _ ->
             raise(Error(loc,Instance_variable_not_mutable(true,lab)))
@@ -1896,7 +1935,7 @@ and type_expect ?in_function env sexp ty_expected =
           let type_override (lab, snewval) =
             begin try
               let (id, _, _, ty) = Vars.find lab !vars in
-              (Path.Pident id, type_expect env snewval (instance ty))
+              (Path.Pident id, type_expect env snewval (instance env ty))
             with
               Not_found ->
                 raise(Error(loc, Unbound_instance_variable lab))
@@ -1944,14 +1983,14 @@ and type_expect ?in_function env sexp ty_expected =
       rue {
         exp_desc = Texp_assert (cond);
         exp_loc = loc;
-        exp_type = instance Predef.type_unit;
+        exp_type = instance_def Predef.type_unit;
         exp_env = env;
       }
   | Pexp_assertfalse ->
       re {
         exp_desc = Texp_assertfalse;
         exp_loc = loc;
-        exp_type = instance ty_expected;
+        exp_type = instance env ty_expected;
         exp_env = env;
       }
   | Pexp_lazy e ->
@@ -1962,7 +2001,7 @@ and type_expect ?in_function env sexp ty_expected =
       re {
         exp_desc = Texp_lazy arg;
         exp_loc = loc;
-        exp_type = instance ty_expected;
+        exp_type = instance env ty_expected;
         exp_env = env;
       }
   | Pexp_object s ->
@@ -1986,12 +2025,12 @@ and type_expect ?in_function env sexp ty_expected =
         generalize_structure ty
       end;
       if sty <> None then
-        unify_exp_types loc env (instance ty) (instance ty_expected);
+        unify_exp_types loc env (instance env ty) (instance env ty_expected);
       begin
         match (expand_head env ty).desc with
           Tpoly (ty', []) ->
             let exp = type_expect env sbody ty' in
-            re { exp with exp_type = instance ty }
+            re { exp with exp_type = instance env ty }
         | Tpoly (ty', tl) ->
             (* One more level to generalize locally *)
             begin_def ();
@@ -2004,7 +2043,7 @@ and type_expect ?in_function env sexp ty_expected =
             let exp = type_expect env sbody ty'' in
             end_def ();
             check_univars env false "method" exp ty_expected vars;
-            re { exp with exp_type = instance ty }
+            re { exp with exp_type = instance env ty }
         | Tvar _ ->
             let exp = type_exp env sbody in
             let exp = {exp with exp_type = newty (Tpoly (exp.exp_type, []))} in
@@ -2014,6 +2053,7 @@ and type_expect ?in_function env sexp ty_expected =
       end
   | Pexp_newtype(name, sbody) ->
       (* Create a fake abstract type declaration for name. *)
+      let level = get_current_level () in
       let decl = {
         type_params = [];
         type_arity = 0;
@@ -2021,7 +2061,7 @@ and type_expect ?in_function env sexp ty_expected =
         type_private = Public;
         type_manifest = None;
         type_variance = [];
-        type_newtype_level = Some (get_current_level ());
+        type_newtype_level = Some (level, level);
         type_loc = loc;
       }
       in
@@ -2057,7 +2097,7 @@ and type_expect ?in_function env sexp ty_expected =
       rue { body with exp_loc = sexp.pexp_loc; exp_type = ety }
   | Pexp_pack m ->
       let (p, nl, tl) =
-        match Ctype.expand_head env (instance ty_expected) with
+        match Ctype.expand_head env (instance env ty_expected) with
           {desc = Tpackage (p, nl, tl)} ->
             if !Clflags.principal &&
               (Ctype.expand_head env ty_expected).level < Btype.generic_level
@@ -2082,22 +2122,23 @@ and type_expect ?in_function env sexp ty_expected =
 and type_label_exp create env loc ty_expected (label, sarg) =
   (* Here also ty_expected may be at generic_level *)
   begin_def ();
-  if !Clflags.principal then (begin_def (); begin_def ());
+  let separate = !Clflags.principal || Env.has_local_constraints env in
+  if separate then (begin_def (); begin_def ());
   let (vars, ty_arg, ty_res) = instance_label true label in
-  if !Clflags.principal then begin
+  if separate then begin
     end_def ();
     (* Generalize label information *)
     generalize_structure ty_arg;
     generalize_structure ty_res
   end;
   begin try
-    unify env (instance ty_res) (instance ty_expected)
+    unify env (instance_def ty_res) (instance env ty_expected)
   with Unify trace ->
     raise(Error(loc , Label_mismatch(lid_of_label label, trace)))
   end;
   (* Instantiate so that we can generalize internal nodes *)
-  let ty_arg = instance ty_arg in
-  if !Clflags.principal then begin
+  let ty_arg = instance_def ty_arg in
+  if separate then begin
     end_def ();
     (* Generalize information merged from ty_expected *)
     generalize_structure ty_arg
@@ -2107,7 +2148,7 @@ and type_label_exp create env loc ty_expected (label, sarg) =
                      else Private_label (lid_of_label label, ty_expected)));
   let arg =
     let snap = if vars = [] then None else Some (Btype.snapshot ()) in
-    let arg = type_argument env sarg ty_arg (instance ty_arg) in
+    let arg = type_argument env sarg ty_arg (instance env ty_arg) in
     end_def ();
     try
       check_univars env (vars <> []) "field value" arg label.lbl_arg vars;
@@ -2125,7 +2166,7 @@ and type_label_exp create env loc ty_expected (label, sarg) =
     with Error (_, Less_general _) as e -> raise e
     | _ -> raise exn    (* In case of failure return the first error *)
   in
-  (label, {arg with exp_type = instance arg.exp_type})
+  (label, {arg with exp_type = instance env arg.exp_type})
 
 and type_argument env sarg ty_expected' ty_expected =
   (* ty_expected' may be generic *)
@@ -2150,7 +2191,7 @@ and type_argument env sarg ty_expected' ty_expected =
         match (expand_head env ty_fun).desc with
         | Tarrow (l,ty_arg,ty_fun,_) when is_optional l ->
             make_args
-              ((Some(option_none (instance ty_arg) sarg.pexp_loc), Optional)
+              ((Some(option_none (instance env ty_arg) sarg.pexp_loc), Optional)
                :: args)
               ty_fun
         | Tarrow (l,_,ty_res',_) when l = "" || !Clflags.classic ->
@@ -2161,8 +2202,8 @@ and type_argument env sarg ty_expected' ty_expected =
       let args, ty_fun', simple_res = make_args [] texp.exp_type in
       let warn = !Clflags.principal &&
         (lv <> generic_level || (repr ty_fun').level <> generic_level)
-      and texp = {texp with exp_type = instance texp.exp_type}
-      and ty_fun = instance ty_fun' in
+      and texp = {texp with exp_type = instance env texp.exp_type}
+      and ty_fun = instance env ty_fun' in
       if not (simple_res || no_labels ty_res) then begin
         unify_exp env texp ty_expected;
         texp
@@ -2214,7 +2255,7 @@ and type_application env funct sargs =
         (List.map
            (function None, x -> None, x | Some f, x -> Some (f ()), x)
            (List.rev args),
-         instance (result_type omitted ty_fun))
+         instance env (result_type omitted ty_fun))
     | (l1, sarg1) :: sargl ->
         let (ty1, ty2) =
           let ty_fun = expand_head env ty_fun in
@@ -2333,7 +2374,7 @@ and type_application env funct sargs =
               may_warn funct.exp_loc
                 (Warnings.Without_principality "eliminated optional argument");
               ignored := (l,ty,lv) :: !ignored;
-              Some (fun () -> option_none (instance ty) Location.none)
+              Some (fun () -> option_none (instance env ty) Location.none)
             end else begin
               may_warn funct.exp_loc
                 (Warnings.Without_principality "commuted an argument");
@@ -2357,7 +2398,7 @@ and type_application env funct sargs =
     (* Special case for ignore: avoid discarding warning *)
     Texp_ident (_, {val_kind=Val_prim{Primitive.prim_name="%ignore"}}),
     ["", sarg] ->
-      let ty_arg, ty_res = filter_arrow env (instance funct.exp_type) "" in
+      let ty_arg, ty_res = filter_arrow env (instance env funct.exp_type) "" in
       let exp = type_expect env sarg ty_arg in
       begin match (expand_head env exp.exp_type).desc with
       | Tarrow _ ->
@@ -2370,9 +2411,9 @@ and type_application env funct sargs =
   | _ ->
       let ty = funct.exp_type in
       if ignore_labels then
-        type_args [] [] ty (instance ty) ty [] sargs
+        type_args [] [] ty (instance env ty) ty [] sargs
       else
-        type_args [] [] ty (instance ty) ty sargs []
+        type_args [] [] ty (instance env ty) ty sargs []
 
 and type_construct env loc lid sarg explicit_arity ty_expected =
   let constr = Typetexp.find_constructor env loc lid in
@@ -2385,7 +2426,8 @@ and type_construct env loc lid sarg explicit_arity ty_expected =
   if List.length sargs <> constr.cstr_arity then
     raise(Error(loc, Constructor_arity_mismatch
                   (lid, constr.cstr_arity, List.length sargs)));
-  if !Clflags.principal then (begin_def (); begin_def ());
+  let separate = !Clflags.principal || Env.has_local_constraints env in
+  if separate then (begin_def (); begin_def ());
   let (ty_args, ty_res) = instance_constructor constr in
   let texp =
     re {
@@ -2393,22 +2435,22 @@ and type_construct env loc lid sarg explicit_arity ty_expected =
       exp_loc = loc;
       exp_type = ty_res;
       exp_env = env } in
-  if !Clflags.principal then begin
+  if separate then begin
     end_def ();
     generalize_structure ty_res;
-    unify_exp env {texp with exp_type = instance ty_res}
-                  (instance ty_expected);
+    unify_exp env {texp with exp_type = instance_def ty_res}
+                  (instance env ty_expected);
     end_def ();
     List.iter generalize_structure ty_args;
     generalize_structure ty_res;
   end;
   let ty_args0, ty_res =
-    match instance_list (ty_res :: ty_args) with
+    match instance_list env (ty_res :: ty_args) with
       t :: tl -> tl, t
     | _ -> assert false
   in
-  let texp = {texp with exp_type = instance ty_res} in
-  if not !Clflags.principal then unify_exp env texp (instance ty_expected);
+  let texp = {texp with exp_type = ty_res} in
+  if not separate then unify_exp env texp (instance env ty_expected);
   let args = List.map2 (fun e (t,t0) -> type_argument env e t t0) sargs
       (List.combine ty_args ty_args0) in
   if constr.cstr_private = Private then
@@ -2423,7 +2465,7 @@ and type_statement env sexp =
   let exp = type_exp env sexp in
   end_def();
   if !Clflags.strict_sequence then
-    let expected_ty = instance Predef.type_unit in
+    let expected_ty = instance_def Predef.type_unit in
     unify_exp env exp expected_ty;
     exp else
   let ty = expand_head env exp.exp_type and tv = newvar() in
@@ -2444,14 +2486,29 @@ and type_statement env sexp =
 (* Typing of match cases *)
 
 and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
-  begin_def ();
-  Ident.set_current_time (get_current_level ());
-  let lev = Ident.current_time () in
-  Ctype.init_def (lev+1000);
-  if !Clflags.principal then begin_def (); (* propagation of the argument *)
+  (* ty_arg is _fully_ generalized *)
+  let dont_propagate, has_gadts =
+    let patterns = List.map fst caselist in
+    List.exists contains_polymorphic_variant patterns,
+    List.exists (contains_gadt env) patterns in
+  (* prerr_endline ( if has_gadts then "contains gadt" else "no gadt"); *)
+  let ty_arg, ty_res, env =
+    if has_gadts && not !Clflags.principal then
+      correct_levels ty_arg, correct_levels ty_res,
+      duplicate_ident_types loc caselist env
+    else ty_arg, ty_res, env in
+  let lev, env =
+    if has_gadts then begin
+      (* raise level for existentials *)
+      begin_def ();
+      Ident.set_current_time (get_current_level ()); 
+      let lev = Ident.current_time () in
+      Ctype.init_def (lev+1000);                 (* up to 1000 existentials *)
+      (lev, Env.add_gadt_instance_level lev env)
+    end else (get_current_level (), env)
+  in
+  begin_def (); (* propagation of the argument *)
   let ty_arg' = newvar () in
-  let dont_propagate =
-    List.exists (fun (p,_) -> contains_polymorphic_variant p) caselist in
   let pattern_force = ref [] in
   (* Format.printf "@[%i %i@ %a@]@." lev (get_current_level())
     Printtyp.raw_type_expr ty_arg; *)
@@ -2465,7 +2522,7 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
           let partial =
             if !Clflags.principal then Some false else None in
           let ty_arg =
-            if dont_propagate then newvar () else instance ?partial ty_arg
+            if dont_propagate then newvar () else instance ?partial env ty_arg
           in type_pattern ~lev env spat scope ty_arg
         in
         pattern_force := force @ !pattern_force;
@@ -2473,7 +2530,7 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
           if !Clflags.principal then begin
             end_def ();
             iter_pattern (fun {pat_type=t} -> generalize_structure t) pat;
-            { pat with pat_type = instance pat.pat_type }
+            { pat with pat_type = instance env pat.pat_type }
           end else pat
         in
         unify_pat env pat ty_arg';
@@ -2487,18 +2544,15 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
   end;
   (* `Contaminating' unifications start here *)
   List.iter (fun f -> f()) !pattern_force;
-  begin match pat_env_list with [] -> ()
-  | (pat, _) :: _ -> unify_pat env pat (instance ty_arg)
-  end;
-  if !Clflags.principal then begin
-    let patl = List.map fst pat_env_list in
-    List.iter (iter_pattern (fun {pat_type=t} -> unify_var env t (newvar())))
-      patl;
-    end_def ();
-    List.iter (iter_pattern (fun {pat_type=t} -> generalize_structure t)) patl
-  end;
+  (* Post-processing and generalization *)
+  let patl = List.map fst pat_env_list in
+  List.iter (iter_pattern (fun {pat_type=t} -> unify_var env t (newvar())))
+    patl;
+  List.iter (fun pat -> unify_pat env pat (instance env ty_arg)) patl;
+  end_def ();
+  List.iter (iter_pattern (fun {pat_type=t} -> generalize t)) patl;
+  (* type bodies *)
   let in_function = if List.length caselist = 1 then in_function else None in
-  let ty_arg' = instance ty_arg in
   let cases =
     List.map2
       (fun (pat, (ext_env, unpacks)) (spat, sexp) ->
@@ -2506,24 +2560,22 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
         let ty_res' =
           if !Clflags.principal then begin
             begin_def ();
-            let ty = instance ~partial:true ty_res in
+            let ty = instance ~partial:true env ty_res in
             end_def ();
             generalize_structure ty; ty
-          end else ty_res in
+          end
+          else if contains_gadt env spat then correct_levels ty_res
+          else ty_res in
         (* Format.printf "@[%i %i, ty_res' =@ %a@]@." lev (get_current_level())
           Printtyp.raw_type_expr ty_res'; *)
         let exp = type_expect ?in_function ext_env sexp ty_res' in
-        ({pat with pat_type = ty_arg'},
-         {exp with exp_type = instance ty_res'}))
+        (pat, {exp with exp_type = instance env ty_res'}))
       pat_env_list caselist
   in
-  if !Clflags.principal then begin
-    let ty_res' = instance ty_res in
+  if !Clflags.principal || has_gadts then begin
+    let ty_res' = instance env ty_res in
     List.iter (fun (_,exp) -> unify_exp env exp ty_res') cases
   end;
-  end_def ();
-  (* Ensure that existential types do not escape *)
-  unify_exp_types loc env (instance ty_res) (newvar ());
   let partial =
     if partial_flag then
       Parmatch.check_partial_gadt (partial_pred ~lev env ty_arg) loc cases
@@ -2531,6 +2583,11 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
       Partial
   in
   add_delayed_check (fun () -> Parmatch.check_unused env cases);
+  if has_gadts then begin
+    end_def ();
+    (* Ensure that existential types do not escape *)
+    unify_exp_types loc env (instance env ty_res) (newvar ()) ;
+  end;
   cases, partial
 
 (* Typing of let bindings *)
@@ -2572,7 +2629,7 @@ and type_let env rec_flag spat_sexp_list scope allow =
       List.map
         (fun pat ->
           iter_pattern (fun pat -> generalize_structure pat.pat_type) pat;
-          {pat with pat_type = instance pat.pat_type})
+          {pat with pat_type = instance env pat.pat_type})
         pat_list
     end else pat_list in
   (* Polymoprhic variant processing *)
@@ -2604,7 +2661,7 @@ and type_let env rec_flag spat_sexp_list scope allow =
             let exp = type_expect exp_env sexp ty' in
             end_def ();
             check_univars env true "definition" exp pat.pat_type vars;
-            {exp with exp_type = instance exp.exp_type}
+            {exp with exp_type = instance env exp.exp_type}
         | _ -> type_expect exp_env sexp pat.pat_type)
       spat_sexp_list pat_list in
   List.iter2
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 1ee14b5750..8b93fdef61 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -406,7 +406,7 @@ let check_recursion env loc path decl to_check =
           else if to_check path' && not (List.mem path' prev_exp) then begin
             try
               (* Attempt expansion *)
-              let (params0, body0) = Env.find_type_expansion path' env in
+              let (params0, body0, _) = Env.find_type_expansion path' env in
               let (params, body) =
                 Ctype.instance_parameterized_type params0 body0 in
               begin
@@ -571,15 +571,40 @@ let compute_variance_type env check (required, loc) decl tyl =
 
 let add_false = List.map (fun ty -> false, ty)
 
-let rec anonymous env ty =
-  match (Ctype.expand_head env ty).desc with
-  | Tvar _ -> false
-  | Tobject (fi, _) ->
-      let _, rv = Ctype.flatten_fields fi in anonymous env rv
-  | Tvariant row ->
-      let rv = Btype.row_more row in anonymous env rv
+(* A parameter is constrained if either is is instantiated,
+   or it is a variable appearing in another parameter *)
+let constrained env vars ty =
+  let ty = Ctype.expand_head env ty in
+  match ty.desc with
+  | Tvar _ -> List.exists (fun tl -> List.memq ty tl) vars
   | _ -> true
-      
+
+let compute_variance_gadt env check (required, loc as rloc) decl
+    (_, tl, ret_type_opt) =
+  match ret_type_opt with
+  | None ->
+      compute_variance_type env check rloc {decl with type_private = Private}
+        (add_false tl)
+  | Some ret_type ->
+      match Ctype.repr ret_type with
+      | {desc=Tconstr (path, tyl, _)} ->
+          let fvl = List.map Ctype.free_variables tyl in
+          let _ =
+            List.fold_left2
+              (fun (fv1,fv2) ty (c,n) ->
+                match fv2 with [] -> assert false
+                | fv :: fv2 ->
+                    (* fv1 @ fv2 = free_variables of other parameters *)
+                    if (c||n) && constrained env (fv1 @ fv2) ty then
+                      raise (Error(loc, Varying_anonymous));
+                    (fv :: fv1, fv2))
+              ([], fvl) tyl required
+          in
+          compute_variance_type env check rloc
+            {decl with type_params = tyl; type_private = Private}
+            (add_false tl)
+      | _ -> assert false
+            
 let compute_variance_decl env check decl (required, loc as rloc) =
   if decl.type_kind = Type_abstract && decl.type_manifest = None then
     List.map (fun (c, n) -> if c || n then (c, n, n) else (true, true, true))
@@ -594,33 +619,10 @@ let compute_variance_decl env check decl (required, loc as rloc) =
       if List.for_all (fun (_,_,ret) -> ret = None) tll then
         compute_variance_type env check rloc decl
           (add_false (List.flatten (List.map (fun (_,tyl,_) -> tyl) tll)))
-      else begin match
-        List.map
-          (fun (_,tl,ret_type_opt) ->
-	    match ret_type_opt with
-	    | None ->
-                compute_variance_type env check rloc
-                  {decl with type_private = Private}
-                  (add_false tl)
-	    | Some ret_type ->
-                match Ctype.repr ret_type with
-                | {desc=Tconstr (path, tyl, _)} ->
-                    let varying =
-                      List.filter
-                        (fun ((ty1,ty2),(c,n)) -> (c||n) && anonymous env ty2)
-                        (List.combine (List.combine decl.type_params tyl)
-                           required)
-                    in
-                    let vpar, vret = List.split (List.map fst varying) in
-                    if not (Ctype.equal env true vpar vret) then
-                      raise (Error(loc, Varying_anonymous));
-                    compute_variance_type env check rloc
-                      {decl with type_params = tyl; type_private = Private}
-                      (add_false tl)
-                | _ -> assert false)
-          tll
-      with vari :: _ -> vari
-      | _ -> assert false
+      else begin
+        match List.map (compute_variance_gadt env check rloc decl) tll with
+        | vari :: _ -> vari
+        | _ -> assert false
       end
   | Type_record (ftl, _) ->
       compute_variance_type env check rloc decl
diff --git a/typing/types.ml b/typing/types.ml
index cabf03ae08..ef958501a5 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -149,9 +149,8 @@ type type_declaration =
     type_manifest: type_expr option;
     type_variance: (bool * bool * bool) list;
     (* covariant, contravariant, weakly contravariant *)
-    type_newtype_level: int option;
-    type_loc: Location.t;
-   }
+    type_newtype_level: (int * int) option;
+    type_loc: Location.t }
 
 and type_kind =
     Type_abstract
diff --git a/typing/types.mli b/typing/types.mli
index f325d00f7b..64ed128479 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -146,9 +146,9 @@ type type_declaration =
     type_manifest: type_expr option;
     type_variance: (bool * bool * bool) list;
     (* covariant, contravariant, weakly contravariant *)
-    type_newtype_level: int option;
-    type_loc: Location.t;
-   }
+    type_newtype_level: (int * int) option;
+    (* definition level * expansion level *)
+    type_loc: Location.t }
 
 and type_kind =
     Type_abstract
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index 6592f6347b..1a13da5cb7 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -53,6 +53,10 @@ exception Error of Location.t * error
 
 type variable_context = int * (string, type_expr) Tbl.t
 
+(* Local definitions *)
+
+let instance_list = Ctype.instance_list Env.empty
+
 (* Narrowing unbound identifier errors. *)
 
 let rec narrow_unbound_lid_error env loc lid make_error =
@@ -202,9 +206,9 @@ let rec transl_type env policy styp =
       if name <> "" && name.[0] = '_' then
         raise (Error (styp.ptyp_loc, Invalid_variable_name ("'" ^ name)));
       begin try
-        instance (List.assoc name !univars)
+        instance env (List.assoc name !univars)
       with Not_found -> try
-        instance (fst(Tbl.find name !used_variables))
+        instance env (fst(Tbl.find name !used_variables))
       with Not_found ->
         let v =
           if policy = Univars then new_pre_univar ~name () else newvar ~name ()
@@ -224,7 +228,7 @@ let rec transl_type env policy styp =
         raise(Error(styp.ptyp_loc, Type_arity_mismatch(lid, decl.type_arity,
                                                            List.length stl)));
       let args = List.map (transl_type env policy) stl in
-      let params = Ctype.instance_list decl.type_params in
+      let params = instance_list decl.type_params in
       let unify_param =
         match decl.type_manifest with
           None -> unify_var
@@ -278,7 +282,7 @@ let rec transl_type env policy styp =
         raise(Error(styp.ptyp_loc, Type_arity_mismatch(lid, decl.type_arity,
                                                        List.length stl)));
       let args = List.map (transl_type env policy) stl in
-      let params = Ctype.instance_list decl.type_params in
+      let params = instance_list decl.type_params in
       List.iter2
         (fun (sty, ty) ty' ->
            try unify_var env ty' ty with Unify trace ->
@@ -313,7 +317,8 @@ let rec transl_type env policy styp =
                       row_fixed = false; row_more = newvar () } in
           let static = Btype.static_row row in
           let row =
-            if static || policy <> Univars then row
+            if static then { row with row_more = newty Tnil }
+            else if policy <> Univars then row
             else { row with row_more = new_pre_univar () }
           in
           newty (Tvariant row)
@@ -330,7 +335,7 @@ let rec transl_type env policy styp =
           let t =
             try List.assoc alias !univars
             with Not_found ->
-              instance (fst(Tbl.find alias !used_variables))
+              instance env (fst(Tbl.find alias !used_variables))
           in
           let ty = transl_type env policy st in
           begin try unify_var env t ty with Unify trace ->
@@ -351,7 +356,7 @@ let rec transl_type env policy styp =
             end_def ();
             generalize_structure t;
           end;
-          let t = instance t in
+          let t = instance env t in
           let px = Btype.proxy t in
           begin match px.desc with
           | Tvar None -> Btype.log_type px; px.desc <- Tvar (Some alias)
@@ -450,7 +455,8 @@ let rec transl_type env policy styp =
           row_fixed = false; row_name = !name } in
       let static = Btype.static_row row in
       let row =
-        if static || policy <> Univars then row
+        if static then { row with row_more = newty Tnil }
+        else if policy <> Univars then row
         else { row with row_more = new_pre_univar () }
       in
       newty (Tvariant row)
@@ -586,7 +592,7 @@ let transl_simple_type_univars env styp =
       [] !pre_univars
   in
   make_fixed_univars typ;
-  instance (Btype.newgenty (Tpoly (typ, univs)))
+  instance env (Btype.newgenty (Tpoly (typ, univs)))
 
 let transl_simple_type_delayed env styp =
   univars := []; used_variables := Tbl.empty;
@@ -658,14 +664,16 @@ let report_error ppf = function
         Printtyp.type_expr ty
   | Variant_tags (lab1, lab2) ->
       fprintf ppf
-        "Variant tags `%s@ and `%s have the same hash value.@ Change one of them."
-        lab1 lab2
+        "@[Variant tags `%s@ and `%s have the same hash value.@ %s@]"
+        lab1 lab2 "Change one of them."
   | Invalid_variable_name name ->
       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 Btype.is_Tvar v then "it escapes this scope" else
-         if Btype.is_Tunivar v then "it is aliased to another variable"
+      fprintf ppf
+        "@[<hov>The universal type variable '%s cannot be generalized:@ %s.@]"
+        name
+        (if Btype.is_Tvar v then "it escapes its scope" else
+         if Btype.is_Tunivar v then "it is already bound to another variable"
          else "it is not a variable")
   | Multiple_constraints_on_type s ->
       fprintf ppf "Multiple constraints for type %s" s
diff --git a/typing/unused_var.ml b/typing/unused_var.ml
index ec468980c1..8b9dfcf36b 100644
--- a/typing/unused_var.ml
+++ b/typing/unused_var.ml
@@ -31,10 +31,15 @@ let rm_vars tbl (vll1, vll2) =
 let w_suspicious x = Warnings.Unused_var x;;
 let w_strict x = Warnings.Unused_var_strict x;;
 
+type ppf_or_idents = Ppf of Format.formatter | Free of string list ref
+
 let check_rm_vars ppf tbl (vlul_pat, vlul_as) =
   let check_rm_var kind (v, loc, used) =
-    if not !used && not (silent v)
-    then Location.print_warning loc ppf (kind v);
+    begin match ppf with
+      Ppf ppf when not !used && not (silent v) ->
+        Location.print_warning loc ppf (kind v)
+    | _ -> ()
+    end;
     Hashtbl.remove tbl v;
   in
   List.iter (check_rm_var w_strict) vlul_pat;
@@ -47,8 +52,10 @@ let check_rm_let ppf tbl vlulpl =
     flag && (silent v || not !used)
   in
   let warn_var w_kind (v, loc, used) =
-    if not (silent v) && not !used
-    then Location.print_warning loc ppf (w_kind v)
+    match ppf with
+      Ppf ppf when not (silent v) && not !used ->
+        Location.print_warning loc ppf (w_kind v)
+    | _ -> ()
   in
   let check_rm_pat (def, def_as) =
     let def_unused = List.fold_left check_rm_one true def in
@@ -59,6 +66,14 @@ let check_rm_let ppf tbl vlulpl =
   List.iter check_rm_pat vlulpl;
 ;;
 
+let add_free_ident ppf s =
+  match ppf with
+    Free r ->
+      if List.mem s !r then () else
+      r := s :: !r
+  | _ -> ()
+;;
+
 let rec get_vars ((vacc, asacc) as acc) p =
   match p.ppat_desc with
   | Ppat_any -> acc
@@ -112,7 +127,7 @@ and expression ppf tbl e =
   match e.pexp_desc with
   | Pexp_ident (Longident.Lident id) ->
       begin try (Hashtbl.find tbl id) := true;
-      with Not_found -> ()
+      with Not_found -> add_free_ident ppf id
       end;
   | Pexp_ident _ -> ()
   | Pexp_constant _ -> ()
@@ -136,7 +151,8 @@ and expression ppf tbl e =
   | Pexp_record (iel, eo) ->
       List.iter (fun (_, e) -> expression ppf tbl e) iel;
       expression_option ppf tbl eo;
-  | Pexp_field (e, _) -> expression ppf tbl e;
+  | Pexp_field (e, _) ->
+      expression ppf tbl e;
   | Pexp_setfield (e1, _, e2) ->
       expression ppf tbl e1;
       expression ppf tbl e2;
@@ -164,7 +180,9 @@ and expression ppf tbl e =
       expression ppf tbl e2;
   | Pexp_send (e, _) -> expression ppf tbl e;
   | Pexp_new _ -> ()
-  | Pexp_setinstvar (_, e) -> expression ppf tbl e;
+  | Pexp_setinstvar (f, e) ->
+      add_free_ident ppf f;
+      expression ppf tbl e;
   | Pexp_override sel -> List.iter (fun (_, e) -> expression ppf tbl e) sel;
   | Pexp_letmodule (_, me, e) ->
       module_expr ppf tbl me;
@@ -262,7 +280,14 @@ let warn ppf ast =
   if Warnings.is_active (w_suspicious "") || Warnings.is_active (w_strict "")
   then begin
     let tbl = Hashtbl.create 97 in
-    structure ppf tbl ast;
+    structure (Ppf ppf) tbl ast;
   end;
   ast
 ;;
+
+let free_idents e =
+  let tbl = Hashtbl.create 7 in
+  let idents = ref [] in
+  expression (Free idents) tbl e;
+  !idents
+;;
diff --git a/typing/unused_var.mli b/typing/unused_var.mli
index fb2d2dfa25..dc8137aef5 100644
--- a/typing/unused_var.mli
+++ b/typing/unused_var.mli
@@ -14,3 +14,6 @@
 
 val warn : Format.formatter -> Parsetree.structure -> Parsetree.structure;;
 (* Warn on unused variables; return the second argument. *)
+
+val free_idents : Parsetree.expression -> string list
+(* Conservatively approximate the free variables of an expression. *)