Synchronize with trunk.

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

29 files changed, 1085 insertions, 585 deletions

diff --git a/typing/cmt_format.ml b/typing/cmt_format.ml
index 9953c3b019..9d117cd3f7 100644
--- a/typing/cmt_format.ml
+++ b/typing/cmt_format.ml
@@ -75,8 +75,8 @@ module ClearEnv  = TypedtreeMap.MakeMap (struct
   let leave_pattern p = { p with pat_env = keep_only_summary p.pat_env }
   let leave_expression e =
     let exp_extra = List.map (function
-        (Texp_open (path, lloc, env), loc, attrs) ->
-          (Texp_open (path, lloc, keep_only_summary env), loc, attrs)
+        (Texp_open (ovf, path, lloc, env), loc, attrs) ->
+          (Texp_open (ovf, path, lloc, keep_only_summary env), loc, attrs)
       | exp_extra -> exp_extra) e.exp_extra in
     { e with
       exp_env = keep_only_summary e.exp_env;
diff --git a/typing/ctype.ml b/typing/ctype.ml
index c3dfc26598..f62cb5546f 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -753,11 +753,12 @@ let rec generalize_expansive env var_level ty =
         Tconstr (path, tyl, abbrev) ->
           let variance =
             try (Env.find_type path env).type_variance
-            with Not_found -> List.map (fun _ -> (true,true,true)) tyl in
+            with Not_found -> List.map (fun _ -> Variance.may_inv) tyl in
           abbrev := Mnil;
           List.iter2
-            (fun (co,cn,ct) t ->
-              if ct then generalize_contravariant env var_level t
+            (fun v t ->
+              if Variance.(mem May_weak v)
+              then generalize_contravariant env var_level t
               else generalize_expansive env var_level t)
             variance tyl
       | Tpackage (_, _, tyl) ->
@@ -1508,6 +1509,15 @@ let generic_abbrev env path =
     Not_found ->
       false
 
+let generic_private_abbrev env path =
+  try
+    match Env.find_type path env with
+      {type_kind = Type_abstract;
+       type_private = Private;
+       type_manifest = Some body} ->
+         (repr body).level = generic_level
+    | _ -> false
+  with Not_found -> false
 
                               (*****************)
                               (*  Occur check  *)
@@ -1681,7 +1691,9 @@ let occur_univar env ty =
           begin try
             let td = Env.find_type p env in
             List.iter2
-              (fun t (pos,neg,_) -> if pos || neg then occur_rec bound t)
+              (fun t v ->
+                if Variance.(mem May_pos v || mem May_neg v)
+                then occur_rec bound t)
               tl td.type_variance
           with Not_found ->
             List.iter (occur_rec bound) tl
@@ -1727,7 +1739,9 @@ let univars_escape env univar_pairs vl ty =
       | Tconstr (p, tl, _) ->
           begin try
             let td = Env.find_type p env in
-            List.iter2 (fun t (pos,neg,_) -> if pos || neg then occur t)
+            List.iter2
+              (fun t v ->
+                if Variance.(mem May_pos v || mem May_neg v) then occur t)
               tl td.type_variance
           with Not_found ->
             List.iter occur tl
@@ -1863,7 +1877,19 @@ let reify env t =
           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);
+	  let r = row_repr r in
+          if not (static_row r) then begin
+	    if r.row_fixed then iterator (row_more r) else
+	    let m = r.row_more in
+	    match m.desc with
+	      Tvar o ->
+		let name = match o with Some s -> s | _ -> "ex" in
+		let t = create_fresh_constr m.level name in
+		let row =
+		  {r with row_fields=[]; row_fixed=true; row_more = t} in
+		link_type m (newty2 m.level (Tvariant row))
+	    | _ -> assert false
+	  end;
           iter_row iterator r
       | Tconstr (p, _, _) when is_object_type p ->
           iter_type_expr iterator (full_expand !env ty)
@@ -1873,12 +1899,12 @@ let reify env t =
   in
   iterator t
 
-let is_abstract_newtype env p =
+let is_newtype env p =
   try
     let decl = Env.find_type p env in
-    not (decl.type_newtype_level = None) &&
-    decl.type_manifest = None &&
-    decl.type_kind = Type_abstract
+    decl.type_newtype_level <> None &&
+    decl.type_kind = Type_abstract &&
+    decl.type_private = Public
   with Not_found -> false
 
 let non_aliasable p decl =
@@ -2006,8 +2032,19 @@ and mcomp_type_decl type_pairs subst env p1 p2 tl1 tl2 =
   try
     let decl = Env.find_type p1 env in
     let decl' = Env.find_type p2 env in
-    if Path.same p1 p2 then
-      (if non_aliasable p1 decl then mcomp_list type_pairs subst env tl1 tl2)
+    if Path.same p1 p2 then begin
+      (* Format.eprintf "@[%a@ %a@]@."
+	!print_raw (newconstr p1 tl2) !print_raw (newconstr p2 tl2);
+      if non_aliasable p1 decl then Format.eprintf "non_aliasable@."
+      else Format.eprintf "aliasable@."; *)
+      let inj =
+        try List.map Variance.(mem Inj) (Env.find_type p1 env).type_variance
+        with Not_found -> List.map (fun _ -> false) tl1
+      in
+      List.iter2
+        (fun i (t1,t2) -> if i then mcomp type_pairs subst env t1 t2)
+        inj (List.combine tl1 tl2)
+    end
     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;
@@ -2028,25 +2065,26 @@ and mcomp_type_option type_pairs subst env t t' =
   | Some t, Some t' -> mcomp type_pairs subst env t t'
   | _ -> raise (Unify [])
 
-and mcomp_variant_description type_pairs subst env =
+and mcomp_variant_description type_pairs subst env xs ys =
   let rec iter = fun x y ->
     match x, y with
-    (name,mflag,t) :: xs, (name', mflag', t') :: ys   ->
+    (id, tl, t) :: xs, (id', tl', t') :: ys   ->
       mcomp_type_option type_pairs subst env t t';
-      if name = name' && mflag = mflag'
+      mcomp_list type_pairs subst env tl tl';
+      if Ident.name id = Ident.name id'
       then iter xs ys
       else raise (Unify [])
     | [],[] -> ()
     | _ -> raise (Unify [])
   in
-  iter
+  iter xs ys
 
 and mcomp_record_description type_pairs subst env =
   let rec iter = fun x y ->
     match x, y with
-      (name, mutable_flag, t) :: xs, (name', mutable_flag', t') :: ys ->
+      (id, mutable_flag, t) :: xs, (id', mutable_flag', t') :: ys ->
         mcomp type_pairs subst env t t';
-        if name = name' && mutable_flag = mutable_flag'
+        if Ident.name id = Ident.name id' && mutable_flag = mutable_flag'
         then iter xs ys
         else raise (Unify [])
     | [], [] -> ()
@@ -2138,6 +2176,18 @@ let rec unify (env:Env.t ref) t1 t2 =
                  || has_cached_expansion p2 !a2) ->
         update_level !env t1.level t2;
         link_type t1 t2
+    | (Tconstr (p1, [], _), Tconstr (p2, [], _))
+      when Env.has_local_constraints !env
+      && is_newtype !env p1 && is_newtype !env p2 ->
+        (* Do not use local constraints more than necessary *)
+        begin try
+          if find_newtype_level !env p1 < find_newtype_level !env p2 then
+            unify env t1 (try_expand_once !env t2)
+          else
+            unify env (try_expand_once !env t1) t2
+        with Cannot_expand ->
+          unify2 env t1 t2
+        end
     | _ ->
         unify2 env t1 t2
     end;
@@ -2232,10 +2282,25 @@ and unify3 env t1 t1' t2 t2' =
           then
             unify_list env tl1 tl2
           else
-            set_mode Pattern ~generate:false (fun () -> unify_list env tl1 tl2)
+            let inj =
+              try List.map Variance.(mem Inj)
+                    (Env.find_type p1 !env).type_variance
+              with Not_found -> List.map (fun _ -> false) tl1
+            in
+            List.iter2
+              (fun i (t1, t2) ->
+                if i then unify env t1 t2 else
+                set_mode Pattern ~generate:false
+                  begin fun () ->
+                    let snap = snapshot () in
+                    try unify env t1 t2 with Unify _ ->
+                      backtrack snap;
+                      reify env t1; reify env t2
+                  end)
+              inj (List.combine 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'
+        when is_newtype !env path && is_newtype !env path'
         && !generate_equations ->
           let source,destination =
             if find_newtype_level !env path > find_newtype_level !env path'
@@ -2243,19 +2308,19 @@ and unify3 env t1 t1' t2 t2' =
             else  p',t1'
           in add_gadt_equation env source destination
       | (Tconstr ((Path.Pident p) as path,[],_), _)
-        when is_abstract_newtype !env path && !generate_equations ->
+        when is_newtype !env path && !generate_equations ->
           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 && !generate_equations ->
+        when is_newtype !env path && !generate_equations ->
           reify env t1' ;
           local_non_recursive_abbrev !env (Path.Pident p) t1';
           add_gadt_equation env p t1'
-      | (Tconstr (_,[],_), _) | (_, Tconstr (_,[],_)) when !umode = Pattern ->
+      | (Tconstr (_,_,_), _) | (_, Tconstr (_,_,_)) when !umode = Pattern ->
           reify env t1';
           reify env t2';
-          mcomp !env t1' t2'
+          if !generate_equations then mcomp !env t1' t2'
       | (Tobject (fi1, nm1), Tobject (fi2, _)) ->
           unify_fields env fi1 fi2;
           (* Type [t2'] may have been instantiated by [unify_fields] *)
@@ -2268,7 +2333,17 @@ and unify3 env t1 t1' t2 t2' =
           | _ -> ()
           end
       | (Tvariant row1, Tvariant row2) ->
-          unify_row env row1 row2
+          if !umode = Expression then
+            unify_row env row1 row2
+          else begin
+            let snap = snapshot () in
+            try unify_row env row1 row2
+            with Unify _ ->
+              backtrack snap;
+              reify env t1';
+              reify env t2';
+              if !generate_equations then mcomp !env t1' t2'
+          end
       | (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) ->
           begin match field_kind_repr kind with
             Fvar r when f <> dummy_method ->
@@ -2785,13 +2860,8 @@ and moregen_row inst_nongen type_pairs env row1 row2 =
       raise (Unify [])
   | _ when static_row row1 -> ()
   | _ when may_inst ->
-      if not (static_row row2) then moregen_occur env rm1.level rm2;
-      let ext =
-        if r2 = [] then rm2 else
-        let row_ext = {row2 with row_fields = r2} in
-        iter_row (moregen_occur env rm1.level) row_ext;
-        newty2 rm1.level (Tvariant row_ext)
-      in
+      let ext = newgenty (Tvariant {row2 with row_fields = r2}) in
+      moregen_occur env rm1.level ext;
       link_type rm1 ext
   | Tconstr _, Tconstr _ ->
       moregen inst_nongen type_pairs env rm1 rm2
@@ -3530,7 +3600,8 @@ let rec build_subtype env visited loops posi level t =
         then warn := true;
         let tl' =
           List.map2
-            (fun (co,cn,_) t ->
+            (fun v t ->
+              let (co,cn) = Variance.get_upper v in
               if cn then
                 if co then (t, Unchanged)
                 else build_subtype env visited loops (not posi) level t
@@ -3635,12 +3706,6 @@ let subtypes = TypePairs.create 17
 let subtype_error env trace =
   raise (Subtype (expand_trace env (List.rev trace), []))
 
-let private_abbrev env path =
-  try
-    let decl = Env.find_type path env in
-    decl.type_private = Private && decl.type_manifest <> None
-  with Not_found -> false
-
 (* check list inclusion, assuming lists are ordered *)
 let rec included nl1 nl2 =
   match nl1, nl2 with
@@ -3689,7 +3754,8 @@ let rec subtype_rec env trace t1 t2 cstrs =
         begin try
           let decl = Env.find_type p1 env in
           List.fold_left2
-            (fun cstrs (co, cn, _) (t1, t2) ->
+            (fun cstrs v (t1, t2) ->
+              let (co, cn) = Variance.get_upper v in
               if co then
                 if cn then
                   (trace, newty2 t1.level (Ttuple[t1]),
@@ -3702,8 +3768,10 @@ let rec subtype_rec env trace t1 t2 cstrs =
         with Not_found ->
           (trace, t1, t2, !univar_pairs)::cstrs
         end
-    | (Tconstr(p1, tl1, _), _) when private_abbrev env p1 ->
+    | (Tconstr(p1, _, _), _) when generic_private_abbrev env p1 ->
         subtype_rec env trace (expand_abbrev_opt env t1) t2 cstrs
+(*  | (_, Tconstr(p2, _, _)) when generic_private_abbrev false env p2 ->
+        subtype_rec env trace t1 (expand_abbrev_opt env t2) cstrs *)
     | (Tobject (f1, _), Tobject (f2, _))
       when is_Tvar (object_row f1) && is_Tvar (object_row f2) ->
         (* Same row variable implies same object. *)
diff --git a/typing/env.ml b/typing/env.ml
index 2018753f95..2f0bc6b92c 100644
--- a/typing/env.ml
+++ b/typing/env.ml
@@ -54,7 +54,7 @@ let used_constructors :
 let prefixed_sg = Hashtbl.create 113
 
 type error =
-  | Illegal_renaming of string * string
+  | Illegal_renaming of string * string * string
   | Inconsistent_import of string * string * string
   | Need_recursive_types of string * string
 
@@ -113,41 +113,45 @@ type summary =
 module EnvTbl =
   struct
     (* A table indexed by identifier, with an extra slot to record usage. *)
-    type 'a t = ('a * bool ref) Ident.tbl
+    type 'a t = ('a * (unit -> unit)) Ident.tbl
 
     let empty = Ident.empty
-    let dummy_slot = ref true
-    let current_slot = ref dummy_slot
-
-    let add id x tbl =
-      Ident.add id (x, !current_slot) tbl
+    let nothing = fun () -> ()
+
+    let already_defined s tbl =
+      try ignore (Ident.find_name s tbl); true
+      with Not_found -> false
+
+    let add kind slot id x tbl ref_tbl =
+      let slot =
+        match slot with
+        | None -> nothing
+        | Some f ->
+          (fun () ->
+             let s = Ident.name id in
+             f kind s (already_defined s ref_tbl)
+          )
+      in
+      Ident.add id (x, slot) tbl
 
     let add_dont_track id x tbl =
-      Ident.add id (x, dummy_slot) tbl
+      Ident.add id (x, nothing) tbl
 
     let find_same_not_using id tbl =
       fst (Ident.find_same id tbl)
 
     let find_same id tbl =
       let (x, slot) = Ident.find_same id tbl in
-      slot := true;
+      slot ();
       x
 
     let find_name s tbl =
       let (x, slot) = Ident.find_name s tbl in
-      slot := true;
+      slot ();
       x
 
     let find_all s tbl =
-      let xs = Ident.find_all s tbl in
-        List.map (fun (x, slot) -> (x, (fun () -> slot := true))) xs
-
-    let with_slot slot f x =
-      let old_slot = !current_slot in
-      current_slot := slot;
-      try_finally
-        (fun () -> f x)
-        (fun () -> current_slot := old_slot)
+      Ident.find_all s tbl
 
     let fold_name f = Ident.fold_name (fun k (d,_) -> f k d)
     let keys tbl = Ident.fold_all (fun k _ accu -> k::accu) tbl []
@@ -289,7 +293,7 @@ let check_consistency filename crcs =
 
 (* Reading persistent structures from .cmi files *)
 
-let read_pers_struct modname filename =
+let read_pers_struct modname filename = (
   let cmi = read_cmi filename in
   let name = cmi.cmi_name in
   let sign = cmi.cmi_sign in
@@ -304,9 +308,9 @@ let read_pers_struct modname filename =
                ps_comps = comps;
                ps_crcs = crcs;
                ps_filename = filename;
-               ps_flags = flags } in
+               ps_flags = flags } in 
     if ps.ps_name <> modname then
-      raise(Error(Illegal_renaming(ps.ps_name, filename)));
+      raise(Error(Illegal_renaming(modname, ps.ps_name, filename)));
     check_consistency filename ps.ps_crcs;
     List.iter
       (function Rectypes ->
@@ -315,6 +319,7 @@ let read_pers_struct modname filename =
       ps.ps_flags;
     Hashtbl.add persistent_structures modname (Some ps);
     ps
+)
 
 let find_pers_struct name =
   if name = "*predef*" then raise Not_found;
@@ -486,6 +491,8 @@ let find_module path env =
 
 (* Lookup by name *)
 
+exception Recmodule
+
 let rec lookup_module_descr lid env =
   match lid with
     Lident s ->
@@ -520,7 +527,14 @@ and lookup_module lid env =
   match lid with
     Lident s ->
       begin try
-        EnvTbl.find_name s env.modules
+        let (_, ty) as r = EnvTbl.find_name s env.modules in
+        begin match ty with
+        | Mty_ident (Path.Pident id) when Ident.name id = "#recmod#" ->
+          (* see #5965 *)
+          raise Recmodule
+        | _ -> ()
+        end;
+        r
       with Not_found ->
         if s = !current_unit then raise Not_found;
         let ps = find_pers_struct s in
@@ -775,7 +789,7 @@ let lookup_cltype lid env =
 let iter_env proj1 proj2 f env =
   Ident.iter (fun id (x,_) -> f (Pident id) x) (proj1 env);
   let rec iter_components path path' mcomps =
-    if EnvLazy.is_val mcomps then
+    (* if EnvLazy.is_val mcomps then *)
     match EnvLazy.force !components_of_module_maker' mcomps with
       Structure_comps comps ->
         Tbl.iter
@@ -800,6 +814,51 @@ let iter_env proj1 proj2 f env =
 
 let iter_types f = iter_env (fun env -> env.types) (fun sc -> sc.comp_types) f
 
+let same_types env1 env2 =
+  env1.types == env2.types && env1.components == env2.components
+
+let used_persistent () =
+  let r = ref Concr.empty in
+  Hashtbl.iter (fun s pso -> if pso != None then r := Concr.add s !r)
+    persistent_structures;
+  !r
+
+let find_all_comps proj s (p,mcomps) =
+  match EnvLazy.force !components_of_module_maker' mcomps with
+    Functor_comps _ -> []
+  | Structure_comps comps ->
+      try let (c,n) = Tbl.find s (proj comps) in [Pdot(p,s,n), c]
+      with Not_found -> []
+
+let rec find_shadowed_comps path env =
+  match path with
+    Pident id ->
+      List.map fst (Ident.find_all (Ident.name id) env.components)
+  | Pdot (p, s, _) ->
+      let l = find_shadowed_comps p env in
+      let l' =
+	List.map (find_all_comps (fun comps -> comps.comp_components) s) l in
+      List.flatten l'
+  | Papply _ -> []
+
+let find_shadowed proj1 proj2 path env =
+  match path with
+    Pident id ->
+      List.map fst (Ident.find_all (Ident.name id) (proj1 env))
+  | Pdot (p, s, _) ->
+      let l = find_shadowed_comps p env in
+      let l' = List.map (find_all_comps proj2 s) l in
+      List.flatten l'
+  | Papply _ -> []
+
+let find_shadowed_types path env =
+  let l =
+    find_shadowed
+      (fun env -> env.types) (fun comps -> comps.comp_types) path env
+  in
+  List.map fst l
+
+
 (* GADT instance tracking *)
 
 let add_gadt_instance_level lv env =
@@ -1013,7 +1072,7 @@ and components_of_module_maker (env, sub, path, mty) =
                 c.comp_labels <-
                   add_to_tbl descr.lbl_name (descr, nopos) c.comp_labels)
               labels;
-            env := store_type_infos id path decl !env
+            env := store_type_infos None id path decl !env !env
         | Sig_exception(id, decl) ->
             let decl' = Subst.exception_declaration sub decl in
             let cstr = Datarepr.exception_descr path decl' in
@@ -1028,13 +1087,13 @@ and components_of_module_maker (env, sub, path, mty) =
             let comps = components_of_module !env sub path mty in
             c.comp_components <-
               Tbl.add (Ident.name id) (comps, !pos) c.comp_components;
-            env := store_module id path mty !env;
+            env := store_module None id path mty !env !env;
             incr pos
         | Sig_modtype(id, decl) ->
             let decl' = Subst.modtype_declaration sub decl in
             c.comp_modtypes <-
               Tbl.add (Ident.name id) (decl', nopos) c.comp_modtypes;
-            env := store_modtype id path decl !env
+            env := store_modtype None id path decl !env !env
         | Sig_class(id, decl, _) ->
             let decl' = Subst.class_declaration sub decl in
             c.comp_classes <-
@@ -1082,13 +1141,13 @@ and check_usage loc id warn tbl =
         (fun () -> if not !used then Location.prerr_warning loc (warn name))
   end;
 
-and store_value ?check id path decl env =
+and store_value ?check slot id path decl env renv =
   may (fun f -> check_usage decl.val_loc id f value_declarations) check;
   { env with
-    values = EnvTbl.add id (path, decl) env.values;
+    values = EnvTbl.add "value" slot id (path, decl) env.values renv.values;
     summary = Env_value(env.summary, id, decl) }
 
-and store_type id path info env =
+and store_type slot id path info env renv =
   let loc = info.type_loc in
   check_usage loc id (fun s -> Warnings.Unused_type_declaration s)
     type_declarations;
@@ -1119,28 +1178,28 @@ and store_type id path info env =
   { env with
     constrs =
       List.fold_right
-        (fun (id, descr) constrs -> EnvTbl.add id descr constrs)
+        (fun (id, descr) constrs -> EnvTbl.add "constructor" slot id descr constrs renv.constrs)
         constructors
         env.constrs;
     labels =
       List.fold_right
-        (fun (id, descr) labels -> EnvTbl.add id descr labels)
+        (fun (id, descr) labels -> EnvTbl.add "label" slot id descr labels renv.labels)
         labels
         env.labels;
-    types = EnvTbl.add id (path, (info, descrs)) env.types;
+    types = EnvTbl.add "type" slot id (path, (info, descrs)) env.types renv.types;
     summary = Env_type(env.summary, id, info) }
 
-and store_type_infos id path info env =
+and store_type_infos slot id path info env renv =
   (* Simplified version of store_type that doesn't compute and store
      constructor and label infos, but simply record the arity and
      manifest-ness of the type.  Used in components_of_module to
      keep track of type abbreviations (e.g. type t = float) in the
      computation of label representations. *)
   { env with
-    types = EnvTbl.add id (path, (info,([],[]))) env.types;
+    types = EnvTbl.add "type" slot id (path, (info,([],[]))) env.types renv.types;
     summary = Env_type(env.summary, id, info) }
 
-and store_exception id path decl env =
+and store_exception slot id path decl env renv =
   let loc = decl.exn_loc in
   if not loc.Location.loc_ghost &&
     Warnings.is_active (Warnings.Unused_exception ("", false))
@@ -1162,30 +1221,30 @@ and store_exception id path decl env =
     end;
   end;
   { env with
-    constrs = EnvTbl.add id (Datarepr.exception_descr path decl) env.constrs;
+    constrs = EnvTbl.add "constructor" slot id (Datarepr.exception_descr path decl) env.constrs renv.constrs;
     summary = Env_exception(env.summary, id, decl) }
 
-and store_module id path mty env =
+and store_module slot id path mty env renv =
   { env with
-    modules = EnvTbl.add id (path, mty) env.modules;
+    modules = EnvTbl.add "module" slot id (path, mty) env.modules renv.modules;
     components =
-      EnvTbl.add id (path, components_of_module env Subst.identity path mty)
-                   env.components;
+      EnvTbl.add "module" slot id (path, components_of_module env Subst.identity path mty)
+                   env.components renv.components;
     summary = Env_module(env.summary, id, mty) }
 
-and store_modtype id path info env =
+and store_modtype slot id path info env renv =
   { env with
-    modtypes = EnvTbl.add id (path, info) env.modtypes;
+    modtypes = EnvTbl.add "module type" slot id (path, info) env.modtypes renv.modtypes;
     summary = Env_modtype(env.summary, id, info) }
 
-and store_class id path desc env =
+and store_class slot id path desc env renv =
   { env with
-    classes = EnvTbl.add id (path, desc) env.classes;
+    classes = EnvTbl.add "class" slot id (path, desc) env.classes renv.classes;
     summary = Env_class(env.summary, id, desc) }
 
-and store_cltype id path desc env =
+and store_cltype slot id path desc env renv =
   { env with
-    cltypes = EnvTbl.add id (path, desc) env.cltypes;
+    cltypes = EnvTbl.add "class type" slot id (path, desc) env.cltypes renv.cltypes;
     summary = Env_cltype(env.summary, id, desc) }
 
 (* Compute the components of a functor application in a path. *)
@@ -1212,25 +1271,25 @@ let _ =
 (* Insertion of bindings by identifier *)
 
 let add_value ?check id desc env =
-  store_value ?check id (Pident id) desc env
+  store_value None ?check id (Pident id) desc env env
 
 let add_type id info env =
-  store_type id (Pident id) info env
+  store_type None id (Pident id) info env env
 
 and add_exception id decl env =
-  store_exception id (Pident id) decl env
+  store_exception None id (Pident id) decl env env
 
 and add_module id mty env =
-  store_module id (Pident id) mty env
+  store_module None id (Pident id) mty env env
 
 and add_modtype id info env =
-  store_modtype id (Pident id) info env
+  store_modtype None id (Pident id) info env env
 
 and add_class id ty env =
-  store_class id (Pident id) ty env
+  store_class None id (Pident id) ty env env
 
 and add_cltype id ty env =
-  store_cltype id (Pident id) ty env
+  store_cltype None id (Pident id) ty env env
 
 let add_local_constraint id info elv env =
   match info with
@@ -1244,7 +1303,7 @@ let add_local_constraint id info elv env =
 (* Insertion of bindings by name *)
 
 let enter store_fun name data env =
-  let id = Ident.create name in (id, store_fun id (Pident id) data env)
+  let id = Ident.create name in (id, store_fun None id (Pident id) data env env)
 
 let enter_value ?check = enter (store_value ?check)
 and enter_type = enter store_type
@@ -1273,7 +1332,7 @@ let rec add_signature sg env =
 
 (* Open a signature path *)
 
-let open_signature root sg env =
+let open_signature slot root sg env0 =
   (* First build the paths and substitution *)
   let (pl, sub, sg) = prefix_idents_and_subst root Subst.identity sg in
   let sg = Lazy.force sg in
@@ -1285,31 +1344,31 @@ let open_signature root sg env =
       (fun env item p ->
         match item with
           Sig_value(id, decl) ->
-            store_value (Ident.hide id) p decl env
+            store_value slot (Ident.hide id) p decl env env0
         | Sig_type(id, decl, _) ->
-            store_type (Ident.hide id) p decl env
+            store_type slot (Ident.hide id) p decl env env0
         | Sig_exception(id, decl) ->
-            store_exception (Ident.hide id) p decl env
+            store_exception slot (Ident.hide id) p decl env env0
         | Sig_module(id, mty, _) ->
-            store_module (Ident.hide id) p mty env
+            store_module slot (Ident.hide id) p mty env env0
         | Sig_modtype(id, decl) ->
-            store_modtype (Ident.hide id) p decl env
+            store_modtype slot (Ident.hide id) p decl env env0
         | Sig_class(id, decl, _) ->
-            store_class (Ident.hide id) p decl env
+            store_class slot (Ident.hide id) p decl env env0
         | Sig_class_type(id, decl, _) ->
-            store_cltype (Ident.hide id) p decl env
+            store_cltype slot (Ident.hide id) p decl env env0
       )
-      env sg pl in
-  { newenv with summary = Env_open(env.summary, root) }
+      env0 sg pl in
+  { newenv with summary = Env_open(env0.summary, root) }
 
 (* Open a signature from a file *)
 
 let open_pers_signature name env =
   let ps = find_pers_struct name in
-  open_signature (Pident(Ident.create_persistent name)) ps.ps_sig env
+  open_signature None (Pident(Ident.create_persistent name)) ps.ps_sig env
 
-let open_signature ?(loc = Location.none) ?(toplevel = false) root sg env =
-  if not toplevel && not loc.Location.loc_ghost && Warnings.is_active (Warnings.Unused_open "")
+let open_signature ?(loc = Location.none) ?(toplevel = false) ovf root sg env =
+  if not toplevel && ovf = Asttypes.Fresh && not loc.Location.loc_ghost && (Warnings.is_active (Warnings.Unused_open "") || Warnings.is_active (Warnings.Open_shadow_identifier ("", "")) || Warnings.is_active (Warnings.Open_shadow_label_constructor ("", "")))
   then begin
     let used = ref false in
     !add_delayed_check_forward
@@ -1317,9 +1376,22 @@ let open_signature ?(loc = Location.none) ?(toplevel = false) root sg env =
         if not !used then
           Location.prerr_warning loc (Warnings.Unused_open (Path.name root))
       );
-    EnvTbl.with_slot used (open_signature root sg) env
+    let shadowed = ref [] in
+    let slot kind s b =
+      if b && not (List.mem (kind, s) !shadowed) then begin
+        shadowed := (kind, s) :: !shadowed;
+        let w =
+          match kind with
+          | "label" | "constructor" -> Warnings.Open_shadow_label_constructor (kind, s)
+          | _ -> Warnings.Open_shadow_identifier (kind, s)
+        in
+        Location.prerr_warning loc w
+      end;
+      used := true
+    in
+    open_signature (Some slot) root sg env
   end
-  else open_signature root sg env
+  else open_signature None root sg env
 
 (* Read a signature from a file *)
 
@@ -1507,9 +1579,9 @@ let env_of_only_summary env_from_summary env =
 open Format
 
 let report_error ppf = function
-  | Illegal_renaming(modname, filename) -> fprintf ppf
-      "Wrong file naming: %a@ contains the compiled interface for@ %s"
-      Location.print_filename filename modname
+  | Illegal_renaming(name, modname, filename) -> fprintf ppf
+      "Wrong file naming: %a@ contains the compiled interface for @ %s when %s was expected"
+      Location.print_filename filename name modname 
   | Inconsistent_import(name, source1, source2) -> fprintf ppf
       "@[<hov>The files %a@ and %a@ \
               make inconsistent assumptions@ over interface %s@]"
diff --git a/typing/env.mli b/typing/env.mli
index 5da976399f..89d4bd1d8b 100644
--- a/typing/env.mli
+++ b/typing/env.mli
@@ -34,9 +34,13 @@ val diff: t -> t -> Ident.t list
 type type_descriptions =
     constructor_description list * label_description list
 
+(* For short-paths *)
 val iter_types:
     (Path.t -> Path.t * (type_declaration * type_descriptions) -> unit) ->
     t -> unit
+val same_types: t -> t -> bool
+val used_persistent: unit -> Concr.t
+val find_shadowed_types: Path.t -> t -> Path.t list
 
 (* Lookup by paths *)
 
@@ -77,6 +81,11 @@ val lookup_modtype: Longident.t -> t -> Path.t * modtype_declaration
 val lookup_class: Longident.t -> t -> Path.t * class_declaration
 val lookup_cltype: Longident.t -> t -> Path.t * class_type_declaration
 
+exception Recmodule
+  (* Raise by lookup_module when the identifier refers
+     to one of the modules of a recursive definition
+     during the computation of its approximation (see #5965). *)
+
 (* Insertion by identifier *)
 
 val add_value:
@@ -97,7 +106,7 @@ val add_signature: signature -> t -> t
 (* Insertion of all fields of a signature, relative to the given path.
    Used to implement open. *)
 
-val open_signature: ?loc:Location.t -> ?toplevel:bool -> Path.t -> signature -> t -> t
+val open_signature: ?loc:Location.t -> ?toplevel:bool -> Asttypes.override_flag -> Path.t -> signature -> t -> t
 val open_pers_signature: string -> t -> t
 
 (* Insertion by name *)
@@ -159,7 +168,7 @@ val env_of_only_summary : (summary -> Subst.t -> t) -> t -> t
 (* Error report *)
 
 type error =
-  | Illegal_renaming of string * string
+  | Illegal_renaming of string * string * string
   | Inconsistent_import of string * string * string
   | Need_recursive_types of string * string
 
diff --git a/typing/envaux.ml b/typing/envaux.ml
index 4edf3b46a2..30146be1ed 100644
--- a/typing/envaux.ml
+++ b/typing/envaux.ml
@@ -63,7 +63,7 @@ let rec env_from_summary sum subst =
             with Not_found ->
               raise (Error (Module_not_found path'))
           in
-          Env.open_signature path' (extract_sig env mty) env
+          Env.open_signature Asttypes.Override path' (extract_sig env mty) env
     in
       Hashtbl.add env_cache (sum, subst) env;
       env
diff --git a/typing/includecore.ml b/typing/includecore.ml
index 3a2d9df82a..802dda3b19 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -122,12 +122,6 @@ type type_mismatch =
   | Field_missing of bool * Ident.t
   | Record_representation of bool
 
-let nth n =
-  if n = 1 then "first" else
-  if n = 2 then "2nd" else
-  if n = 3 then "3rd" else
-  string_of_int n ^ "th"
-
 let report_type_mismatch0 first second decl ppf err =
   let pr fmt = Format.fprintf ppf fmt in
   match err with
@@ -144,8 +138,8 @@ let report_type_mismatch0 first second decl ppf err =
   | Field_arity s ->
       pr "The arities for field %s differ" (Ident.name s)
   | Field_names (n, name1, name2) ->
-      pr "Their %s fields have different names, %s and %s"
-        (nth n) (Ident.name name1) (Ident.name name2)
+      pr "Fields number %i have different names, %s and %s"
+        n (Ident.name name1) (Ident.name name2)
   | Field_missing (b, s) ->
       pr "The field %s is only present in %s %s"
         (Ident.name s) (if b then second else first) decl
@@ -244,18 +238,20 @@ let type_declarations ?(equality = false) env name decl1 id decl2 =
         else [Constraint]
   in
   if err <> [] then err else
-  if match decl2.type_kind with
-  | Type_record (_,_) | Type_variant _ -> decl2.type_private = Private
-  | Type_abstract ->
-      match decl2.type_manifest with
-      | None -> true
-      | Some ty -> Btype.has_constr_row (Ctype.expand_head env ty)
-  then
-    if List.for_all2
-        (fun (co1,cn1,ct1) (co2,cn2,ct2) -> (not co1 || co2)&&(not cn1 || cn2))
-        decl1.type_variance decl2.type_variance
-    then [] else [Variance]
-  else []
+  let abstr =
+    decl2.type_private = Private ||
+    decl2.type_kind = Type_abstract && decl2.type_manifest = None in
+  if List.for_all2
+      (fun ty (v1,v2) ->
+        let open Variance in
+        let imp a b = not a || b in
+        let (co1,cn1) = get_upper v1 and (co2,cn2) = get_upper v2 in
+        imp abstr (imp co1 co2 && imp cn1 cn2) &&
+        (abstr || Btype.(is_Tvar (repr ty)) || co1 = co2 && cn1 = cn2) &&
+        let (p1,n1,i1,j1) = get_lower v1 and (p2,n2,i2,j2) = get_lower v2 in
+        imp abstr (imp p2 p1 && imp n2 n1 && imp i2 i1 && imp j2 j1))
+      decl2.type_params (List.combine decl1.type_variance decl2.type_variance)
+  then [] else [Variance]
 
 (* Inclusion between exception declarations *)
 
diff --git a/typing/includemod.ml b/typing/includemod.ml
index 180ba272c4..086dfe4d83 100644
--- a/typing/includemod.ml
+++ b/typing/includemod.ml
@@ -120,6 +120,16 @@ let item_ident_name = function
   | Sig_class(id, _, _) -> (id, Field_class(Ident.name id))
   | Sig_class_type(id, _, _) -> (id, Field_classtype(Ident.name id))
 
+let is_runtime_component = function
+  | Sig_value(_,{val_kind = Val_prim _})
+  | Sig_type(_,_,_)
+  | Sig_modtype(_,_)
+  | Sig_class_type(_,_,_) -> false
+  | Sig_value(_,_)
+  | Sig_exception(_,_)
+  | Sig_module(_,_,_)
+  | Sig_class(_, _,_) -> true
+
 (* Simplify a structure coercion *)
 
 let simplify_structure_coercion cc =
@@ -186,23 +196,20 @@ and signatures env cxt subst sig1 sig2 =
   (* Build a table of the components of sig1, along with their positions.
      The table is indexed by kind and name of component *)
   let rec build_component_table pos tbl = function
-      [] -> tbl
+      [] -> pos, tbl
     | item :: rem ->
         let (id, name) = item_ident_name item in
-        let nextpos =
-          match item with
-            Sig_value(_,{val_kind = Val_prim _})
-          | Sig_type(_,_,_)
-          | Sig_modtype(_,_)
-          | Sig_class_type(_,_,_) -> pos
-          | Sig_value(_,_)
-          | Sig_exception(_,_)
-          | Sig_module(_,_,_)
-          | Sig_class(_, _,_) -> pos+1 in
+        let nextpos = if is_runtime_component item then pos + 1 else pos in
         build_component_table nextpos
                               (Tbl.add name (id, item, pos) tbl) rem in
-  let comps1 =
+  let len1, comps1 =
     build_component_table 0 Tbl.empty sig1 in
+  let len2 =
+    List.fold_left
+      (fun n i -> if is_runtime_component i then n + 1 else n)
+      0
+      sig2
+  in
   (* Pair each component of sig2 with a component of sig1,
      identifying the names along the way.
      Return a coercion list indicating, for all run-time components
@@ -211,7 +218,14 @@ and signatures env cxt subst sig1 sig2 =
   let rec pair_components subst paired unpaired = function
       [] ->
         begin match unpaired with
-            [] -> signature_components new_env cxt subst (List.rev paired)
+            [] ->
+              let cc =
+                signature_components new_env cxt subst (List.rev paired)
+              in
+              if len1 = len2 then (* see PR#5098 *)
+                simplify_structure_coercion cc
+              else
+                Tcoerce_structure cc
           | _  -> raise(Error unpaired)
         end
     | item2 :: rem ->
@@ -248,7 +262,7 @@ and signatures env cxt subst sig1 sig2 =
           pair_components subst paired unpaired rem
         end in
   (* Do the pairing and checking, and return the final coercion *)
-  simplify_structure_coercion (pair_components subst [] [] sig2)
+  pair_components subst [] [] sig2
 
 (* Inclusion between signature components *)
 
diff --git a/typing/parmatch.ml b/typing/parmatch.ml
index 2862e54569..efca422034 100644
--- a/typing/parmatch.ml
+++ b/typing/parmatch.ml
@@ -276,9 +276,29 @@ let top_pretty ppf v =
   fprintf ppf "@[%a@]@?" pretty_val v
 
 
-let prerr_pat v =
-  top_pretty str_formatter v ;
-  prerr_string (flush_str_formatter ())
+let pretty_pat p =
+  top_pretty Format.str_formatter p ;
+  prerr_string (Format.flush_str_formatter ())
+
+type matrix = pattern list list
+
+let pretty_line ps =
+  List.iter
+    (fun p ->
+      top_pretty Format.str_formatter p ;
+      prerr_string " <" ;
+      prerr_string (Format.flush_str_formatter ()) ;
+      prerr_string ">")
+    ps
+
+let pretty_matrix (pss : matrix) =
+  prerr_endline "begin matrix" ;
+  List.iter
+    (fun ps ->
+      pretty_line ps ;
+      prerr_endline "")
+    pss ;
+  prerr_endline "end matrix"
 
 
 (****************************)
@@ -1261,29 +1281,6 @@ type answer =
   | Upartial of Typedtree.pattern list  (* Mixed, with list of useless ones *)
 
 
-let pretty_pat p =
-  top_pretty Format.str_formatter p ;
-  prerr_string (Format.flush_str_formatter ())
-
-type matrix = pattern list list
-
-let pretty_line ps =
-  List.iter
-    (fun p ->
-      top_pretty Format.str_formatter p ;
-      prerr_string " <" ;
-      prerr_string (Format.flush_str_formatter ()) ;
-      prerr_string ">")
-    ps
-
-let pretty_matrix (pss : matrix) =
-  prerr_endline "begin matrix" ;
-  List.iter
-    (fun ps ->
-      pretty_line ps ;
-      prerr_endline "")
-    pss ;
-  prerr_endline "end matrix"
 
 (* this row type enable column processing inside the matrix
     - left  ->  elements not to be processed,
diff --git a/typing/parmatch.mli b/typing/parmatch.mli
index 1215c165d4..947f16fa2c 100644
--- a/typing/parmatch.mli
+++ b/typing/parmatch.mli
@@ -40,7 +40,7 @@ val lubs : pattern list -> pattern list -> pattern list
 
 val get_mins : ('a -> 'a -> bool) -> 'a list -> 'a list
 
-(* Those to functions recombine one pattern and its arguments:
+(* Those two functions recombine one pattern and its arguments:
    For instance:
      (_,_)::p1::p2::rem -> (p1, p2)::rem
    The second one will replace mutable arguments by '_'
diff --git a/typing/predef.ml b/typing/predef.ml
index 7d05a7d2da..e4e96d2de1 100644
--- a/typing/predef.ml
+++ b/typing/predef.ml
@@ -12,7 +12,6 @@
 
 (* Predefined type constructors (with special typing rules in typecore) *)
 
-open Asttypes
 open Path
 open Types
 open Btype
@@ -92,6 +91,16 @@ let path_match_failure = Pident ident_match_failure
 and path_assert_failure = Pident ident_assert_failure
 and path_undefined_recursive_module = Pident ident_undefined_recursive_module
 
+let decl_abstr =
+  {type_params = [];
+   type_arity = 0;
+   type_kind = Type_abstract;
+   type_loc = Location.none;
+   type_private = Asttypes.Public;
+   type_manifest = None;
+   type_variance = [];
+   type_newtype_level = None}
+
 let ident_false = ident_create "false"
 and ident_true = ident_create "true"
 and ident_void = ident_create "()"
@@ -100,100 +109,49 @@ and ident_cons = ident_create "::"
 and ident_none = ident_create "None"
 and ident_some = ident_create "Some"
 let build_initial_env add_type add_exception empty_env =
-  let decl_abstr =
-    {type_params = [];
-     type_arity = 0;
-     type_kind = Type_abstract;
-     type_loc = Location.none;
-     type_private = Public;
-     type_manifest = None;
-     type_variance = [];
-     type_newtype_level = None}
-  and decl_bool =
-    {type_params = [];
-     type_arity = 0;
-     type_kind = Type_variant([ident_false, [], None; ident_true, [], None]);
-     type_loc = Location.none;
-     type_private = Public;
-     type_manifest = None;
-     type_variance = [];
-     type_newtype_level = None}
+  let decl_bool =
+    {decl_abstr with
+     type_kind = Type_variant([ident_false, [], None; ident_true, [], None])}
   and decl_unit =
-    {type_params = [];
-     type_arity = 0;
-     type_kind = Type_variant([ident_void, [], None]);
-     type_loc = Location.none;
-     type_private = Public;
-     type_manifest = None;
-     type_variance = [];
-     type_newtype_level = None}
+    {decl_abstr with
+     type_kind = Type_variant([ident_void, [], None])}
   and decl_exn =
-    {type_params = [];
-     type_arity = 0;
-     type_kind = Type_variant [];
-     type_loc = Location.none;
-     type_private = Public;
-     type_manifest = None;
-     type_variance = [];
-     type_newtype_level = None}
+    {decl_abstr with
+     type_kind = Type_variant []}
   and decl_array =
     let tvar = newgenvar() in
-    {type_params = [tvar];
+    {decl_abstr with
+     type_params = [tvar];
      type_arity = 1;
-     type_kind = Type_abstract;
-     type_loc = Location.none;
-     type_private = Public;
-     type_manifest = None;
-     type_variance = [true, true, true];
-     type_newtype_level = None}
+     type_variance = [Variance.full]}
   and decl_list =
     let tvar = newgenvar() in
-    {type_params = [tvar];
+    {decl_abstr with
+     type_params = [tvar];
      type_arity = 1;
      type_kind =
      Type_variant([ident_nil, [], None; ident_cons, [tvar; type_list tvar],
                    None]);
-     type_loc = Location.none;
-     type_private = Public;
-     type_manifest = None;
-     type_variance = [true, false, false];
-     type_newtype_level = None}
+     type_variance = [Variance.covariant]}
   and decl_format6 =
-    {type_params = [
-     newgenvar(); newgenvar(); newgenvar();
-     newgenvar(); newgenvar(); newgenvar();
-   ];
+    let params = List.map newgenvar [();();();();();()] in
+    {decl_abstr with
+     type_params = params;
      type_arity = 6;
-     type_kind = Type_abstract;
-     type_loc = Location.none;
-     type_private = Public;
-     type_manifest = None;
-     type_variance = [
-     true, true, true; true, true, true;
-     true, true, true; true, true, true;
-     true, true, true; true, true, true;
-   ];
-     type_newtype_level = None}
+     type_variance = List.map (fun _ -> Variance.full) params}
   and decl_option =
     let tvar = newgenvar() in
-    {type_params = [tvar];
+    {decl_abstr with
+     type_params = [tvar];
      type_arity = 1;
      type_kind = Type_variant([ident_none, [], None; ident_some, [tvar], None]);
-     type_loc = Location.none;
-     type_private = Public;
-     type_manifest = None;
-     type_variance = [true, false, false];
-     type_newtype_level = None}
+     type_variance = [Variance.covariant]}
   and decl_lazy_t =
     let tvar = newgenvar() in
-    {type_params = [tvar];
+    {decl_abstr with
+     type_params = [tvar];
      type_arity = 1;
-     type_kind = Type_abstract;
-     type_loc = Location.none;
-     type_private = Public;
-     type_manifest = None;
-     type_variance = [true, false, false];
-     type_newtype_level = None}
+     type_variance = [Variance.covariant]}
   in
 
   let add_exception id l =
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 6f6bf74088..e3a841f829 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -69,6 +69,15 @@ let rec path ppf = function
   | Papply(p1, p2) ->
       fprintf ppf "%a(%a)" path p1 path p2
 
+let rec string_of_out_ident = function
+  | Oide_ident s -> s
+  | Oide_dot (id, s) -> String.concat "." [string_of_out_ident id; s]
+  | Oide_apply (id1, id2) ->
+      String.concat ""
+        [string_of_out_ident id1; "("; string_of_out_ident id2; ")"]
+
+let string_of_path p = string_of_out_ident (tree_of_path p)
+
 (* Print a recursive annotation *)
 
 let tree_of_rec = function
@@ -204,8 +213,26 @@ let apply_subst s1 tyl =
   | Map l1 -> List.map (List.nth tyl) l1
   | Id -> tyl
 
+type best_path = Paths of Path.t list | Best of Path.t
+
 let printing_env = ref Env.empty
-let printing_map = ref (Lazy.lazy_from_val Tbl.empty)
+let printing_old = ref Env.empty
+let printing_pers = ref Concr.empty
+module Path2 = struct
+  include Path
+  let rec compare p1 p2 =
+    (* must ignore position when comparing paths *)
+    match (p1, p2) with
+      (Pdot(p1, s1, pos1), Pdot(p2, s2, pos2)) ->
+        let c = compare p1 p2 in
+        if c <> 0 then c else String.compare s1 s2
+    | (Papply(fun1, arg1), Papply(fun2, arg2)) ->
+        let c = compare fun1 fun2 in
+        if c <> 0 then c else compare arg1 arg2
+    | _ -> Pervasives.compare p1 p2
+end
+module PathMap = Map.Make(Path2)
+let printing_map = ref (Lazy.lazy_from_val PathMap.empty)
 
 let same_type t t' = repr t == repr t'
 
@@ -255,42 +282,83 @@ let rec path_size = function
       let (l, b) = path_size p1 in
       (l + fst (path_size p2), b)
 
+let same_printing_env env =
+  let used_pers = Env.used_persistent () in
+  Env.same_types !printing_old env && Concr.equal !printing_pers used_pers
+
 let set_printing_env env =
-  if not !Clflags.real_paths && env != !printing_env then begin
+  printing_env := if !Clflags.real_paths then Env.empty else env;
+  if !printing_env == Env.empty || same_printing_env env then () else
+  begin
     (* printf "Reset printing_map@."; *)
-    printing_env := env;
+    printing_old := env;
+    printing_pers := Env.used_persistent ();
     printing_map := lazy begin
       (* printf "Recompute printing_map.@."; *)
-      let map = ref Tbl.empty in
+      let map = ref PathMap.empty in
       Env.iter_types
         (fun p (p', decl) ->
           let (p1, s1) = normalize_type_path env p' ~cache:true in
+          (* Format.eprintf "%a -> %a = %a@." path p path p' path p1 *)
           if s1 = Id then
           try
-            let p2 = Tbl.find p1 !map in
-            if path_size p < path_size p2 then raise Not_found
+            let r = PathMap.find p1 !map in
+            match !r with
+              Paths l -> r := Paths (p :: l)
+            | Best _  -> assert false
           with Not_found ->
-            (* printf "%a --> %a@." path p1 path p; *)
-            map := Tbl.add p1 p !map)
+            map := PathMap.add p1 (ref (Paths [p])) !map)
         env;
       !map
     end
   end
 
 let wrap_printing_env env f =
-  if env == !printing_env then f () else
-  begin
-    set_printing_env env;
-    try_finally f (fun () -> set_printing_env Env.empty)
-  end
+  set_printing_env env;
+  try_finally f (fun () -> set_printing_env Env.empty)
+
+let is_unambiguous path env =
+  let l = Env.find_shadowed_types path env in
+  List.exists (Path.same path) l || (* concrete paths are ok *)
+  match l with
+    [] -> true
+  | p :: rem ->
+      (* allow also coherent paths:  *)
+      let normalize p = fst (normalize_type_path ~cache:true env p) in
+      let p' = normalize p in
+      List.for_all (fun p -> Path.same (normalize p) p') rem ||
+      (* also allow repeatedly defining and opening (for toplevel) *)
+      let id = lid_of_path p in
+      List.for_all (fun p -> lid_of_path p = id) rem &&
+      Path.same p (fst (Env.lookup_type id env))
+
+let rec get_best_path r =
+  match !r with
+    Best p' -> p'
+  | Paths [] -> raise Not_found
+  | Paths l ->
+      r := Paths [];
+      List.iter
+        (fun p ->
+          (* Format.eprintf "evaluating %a@." path p; *)
+          match !r with
+            Best p' when path_size p >= path_size p' -> ()
+          | _ -> if is_unambiguous p !printing_env then r := Best p)
+              (* else Format.eprintf "%a ignored as ambiguous@." path p *)
+        l;
+      get_best_path r
 
 let best_type_path p =
   if !Clflags.real_paths || !printing_env == Env.empty
   then (p, Id)
   else
     let (p', s) = normalize_type_path !printing_env p in
-    (try Tbl.find  p' (Lazy.force !printing_map) with Not_found -> p'),
-    s
+    let p'' =
+      try get_best_path (PathMap.find  p' (Lazy.force !printing_map))
+      with Not_found -> p'
+    in
+    (* Format.eprintf "%a = %a -> %a@." path p path p' path p''; *)
+    (p'', s)
 
 (* Print a type expression *)
 
@@ -683,6 +751,17 @@ let rec tree_of_type_decl id decl =
 
   let params = filter_params decl.type_params in
 
+  begin match decl.type_manifest with
+  | Some ty ->
+      let vars = free_variables ty in
+      List.iter
+        (function {desc = Tvar (Some "_")} as ty ->
+            if List.memq ty vars then ty.desc <- Tvar None
+          | _ -> ())
+        params
+  | None -> ()
+  end;
+
   List.iter add_alias params;
   List.iter mark_loops params;
   List.iter check_name_of_type (List.map proxy params);
@@ -734,8 +813,9 @@ let rec tree_of_type_decl id decl =
     in
     let vari =
       List.map2
-        (fun ty (co,cn,ct) ->
-          if abstr || not (is_Tvar (repr ty)) then (co,cn) else (true,true))
+        (fun ty v ->
+          if abstr || not (is_Tvar (repr ty)) then Variance.get_upper v
+          else (true,true))
         decl.type_params decl.type_variance
     in
     (Ident.name id,
@@ -930,6 +1010,9 @@ let tree_of_class_params params =
   let tyl = tree_of_typlist true params in
   List.map (function Otyp_var (_, s) -> s | _ -> "?") tyl
 
+let class_variance =
+  List.map Variance.(fun v -> mem May_pos v, mem May_neg v)
+
 let tree_of_class_declaration id cl rs =
   let params = filter_params cl.cty_params in
 
@@ -945,7 +1028,7 @@ let tree_of_class_declaration id cl rs =
   let vir_flag = cl.cty_new = None in
   Osig_class
     (vir_flag, Ident.name id,
-     List.map2 tree_of_class_param params cl.cty_variance,
+     List.map2 tree_of_class_param params (class_variance cl.cty_variance),
      tree_of_class_type true params cl.cty_type,
      tree_of_rec rs)
 
@@ -978,7 +1061,7 @@ let tree_of_cltype_declaration id cl rs =
 
   Osig_class_type
     (virt, Ident.name id,
-     List.map2 tree_of_class_param params cl.clty_variance,
+     List.map2 tree_of_class_param params (class_variance cl.clty_variance),
      tree_of_class_type true params cl.clty_type,
      tree_of_rec rs)
 
@@ -1003,6 +1086,26 @@ let filter_rem_sig item rem =
   | _ ->
       ([], rem)
 
+let dummy =
+  { type_params = []; type_arity = 0; type_kind = Type_abstract;
+    type_private = Public; type_manifest = None; type_variance = [];
+    type_newtype_level = None; type_loc = Location.none; }
+
+let hide_rec_items = function
+  | Sig_type(id, decl, rs) ::rem
+    when rs <> Trec_next && not !Clflags.real_paths ->
+      let rec get_ids = function
+          Sig_type (id, _, Trec_next) :: rem ->
+            id :: get_ids rem
+        | _ -> []
+      in
+      let ids = id :: get_ids rem in
+      set_printing_env
+        (List.fold_right
+           (fun id -> Env.add_type (Ident.rename id) dummy)
+           ids !printing_env)
+  | _ -> ()
+
 let rec tree_of_modtype = function
   | Mty_ident p ->
       Omty_ident (tree_of_path p)
@@ -1014,11 +1117,15 @@ let rec tree_of_modtype = function
          wrap_env (Env.add_module param ty_arg) tree_of_modtype ty_res)
 
 and tree_of_signature sg =
-  wrap_env (fun env -> env) tree_of_signature_rec sg
+  wrap_env (fun env -> env) (tree_of_signature_rec !printing_env) sg
 
-and tree_of_signature_rec = function
+and tree_of_signature_rec env' = function
     [] -> []
   | item :: rem ->
+      begin match item with
+        Sig_type (_, _, rs) when rs <> Trec_next -> ()
+      | _ -> set_printing_env env'
+      end;
       let (sg, rem) = filter_rem_sig item rem in
       let trees =
         match item with
@@ -1027,6 +1134,7 @@ and tree_of_signature_rec = function
         | Sig_type(id, _, _) when is_row_name (Ident.name id) ->
             []
         | Sig_type(id, decl, rs) ->
+            hide_rec_items (item :: rem);
             [Osig_type(tree_of_type_decl id decl, tree_of_rec rs)]
         | Sig_exception(id, decl) ->
             [tree_of_exception_declaration id decl]
@@ -1039,8 +1147,8 @@ and tree_of_signature_rec = function
         | Sig_class_type(id, decl, rs) ->
             [tree_of_cltype_declaration id decl rs]
       in
-      set_printing_env (Env.add_signature (item :: sg) !printing_env);
-      trees @ tree_of_signature_rec rem
+      let env' = Env.add_signature (item :: sg) env' in
+      trees @ tree_of_signature_rec env' rem
 
 and tree_of_modtype_declaration id decl =
   let mty =
@@ -1207,7 +1315,7 @@ let explanation unif t3 t4 ppf =
   | Tnil, Tconstr _ | Tconstr _, Tnil ->
       fprintf ppf
         "@,@[The %s object type has an abstract row, it cannot be closed@]"
-	(if t4.desc = Tnil then "first" else "second")
+        (if t4.desc = Tnil then "first" else "second")
   | Tvariant row1, Tvariant row2 ->
       let row1 = row_repr row1 and row2 = row_repr row2 in
       begin match
@@ -1325,7 +1433,7 @@ let report_ambiguous_type_error ppf env (tp0, tp0') tpl txt1 txt2 txt3 =
     match tpl with
       [] -> assert false
     | [tp, tp'] ->       
-	fprintf ppf
+        fprintf ppf
           "@[%t@;<1 2>%a@ \
              %t@;<1 2>%a\
            @]"
diff --git a/typing/printtyp.mli b/typing/printtyp.mli
index 09edd43527..e319f18f1f 100644
--- a/typing/printtyp.mli
+++ b/typing/printtyp.mli
@@ -20,6 +20,7 @@ val longident: formatter -> Longident.t -> unit
 val ident: formatter -> Ident.t -> unit
 val tree_of_path: Path.t -> out_ident
 val path: formatter -> Path.t -> unit
+val string_of_path: Path.t -> string
 val raw_type_expr: formatter -> type_expr -> unit
 
 val wrap_printing_env: Env.t -> (unit -> 'a) -> 'a
@@ -78,3 +79,5 @@ val report_ambiguous_type_error:
     formatter -> Env.t -> (Path.t * Path.t) -> (Path.t * Path.t) list -> 
     (formatter -> unit) -> (formatter -> unit) -> (formatter -> unit) -> unit
 
+(* for toploop *)
+val hide_rec_items: signature_item list -> unit
diff --git a/typing/printtyped.ml b/typing/printtyped.ml
index 81e1829b1e..c45a7dae63 100644
--- a/typing/printtyped.ml
+++ b/typing/printtyped.ml
@@ -254,8 +254,8 @@ and expression_extra i ppf x attrs =
       attributes i ppf attrs;
       option i core_type ppf cto1;
       core_type i ppf cto2;
-  | Texp_open (m, _, _) ->
-      line i ppf "Pexp_open \"%a\"\n" fmt_path m;
+  | Texp_open (ovf, m, _, _) ->
+      line i ppf "Pexp_open %a \"%a\"\n" fmt_override_flag ovf fmt_path m;
       attributes i ppf attrs;
   | Texp_poly cto ->
       line i ppf "Pexp_poly\n";
@@ -598,8 +598,8 @@ and signature_item i ppf x =
       line i ppf "Psig_modtype \"%a\"\n" fmt_ident x.mtd_id;
       attributes i ppf x.mtd_attributes;
       modtype_declaration i ppf x.mtd_type
-  | Tsig_open (li,_,attrs) ->
-      line i ppf "Psig_open %a\n" fmt_path li;
+  | Tsig_open (ovf, li,_,attrs) ->
+      line i ppf "Psig_open %a %a\n" fmt_override_flag ovf  fmt_path li;
       attributes i ppf attrs
   | Tsig_include (mt, _, attrs) ->
       line i ppf "Psig_include\n";
@@ -704,8 +704,8 @@ and structure_item i ppf x =
       line i ppf "Pstr_modtype \"%a\"\n" fmt_ident x.mtd_id;
       attributes i ppf x.mtd_attributes;
       modtype_declaration i ppf x.mtd_type
-  | Tstr_open (li, _, attrs) ->
-      line i ppf "Pstr_open %a\n" fmt_path li;
+  | Tstr_open (ovf, li, _, attrs) ->
+      line i ppf "Pstr_open %a %a\n" fmt_override_flag ovf fmt_path li;
       attributes i ppf attrs
   | Tstr_class (l) ->
       line i ppf "Pstr_class\n";
diff --git a/typing/stypes.ml b/typing/stypes.ml
index 042821619d..6c9a1df23e 100644
--- a/typing/stypes.ml
+++ b/typing/stypes.ml
@@ -143,7 +143,7 @@ let print_ident_annot pp str k =
 
 (* The format of the annotation file is documented in emacs/caml-types.el. *)
 
-let print_info pp ppf prev_loc ti =
+let print_info pp prev_loc ti =
   match ti with
   | Ti_class _ | Ti_mod _ -> prev_loc
   | Ti_pat  {pat_loc = loc; pat_type = typ; pat_env = env}
@@ -153,12 +153,13 @@ let print_info pp ppf prev_loc ti =
         output_char pp '\n'
       end;
       output_string pp "type(\n";
-      flush pp;
       printtyp_reset_maybe loc;
       Printtyp.mark_loops typ;
-      Format.pp_print_string ppf "  ";
-      Printtyp.wrap_printing_env env (fun () -> Printtyp.type_sch ppf typ);
-      Format.pp_print_newline ppf ();
+      Format.pp_print_string Format.str_formatter "  ";
+      Printtyp.wrap_printing_env env (fun () -> Printtyp.type_sch Format.str_formatter typ);
+      Format.pp_print_newline Format.str_formatter ();
+      let s = Format.flush_str_formatter () in
+      output_string pp s;
       output_string pp ")\n";
       loc
   | An_call (loc, k) ->
@@ -194,9 +195,8 @@ let dump filename =
       match filename with
           None -> stdout
         | Some filename -> open_out filename in
-    let ppf = Format.formatter_of_out_channel pp in
     sort_filter_phrases ();
-    ignore (List.fold_left (print_info pp ppf) Location.none info);
+    ignore (List.fold_left (print_info pp) Location.none info);
     phrases := [];
   end else begin
     annotations := [];
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 6ae67ccb34..fa9ba280f3 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -45,6 +45,7 @@ type error =
   | Final_self_clash of (type_expr * type_expr) list
   | Mutability_mismatch of string * mutable_flag
   | No_overriding of string * string
+  | Duplicate of string * string
   | Extension of string
 
 exception Error of Location.t * Env.t * error
@@ -84,18 +85,22 @@ let rec scrape_class_type =
   | cty                     -> cty
 
 (* Generalize a class type *)
-let rec generalize_class_type =
+let rec generalize_class_type gen =
   function
     Cty_constr (_, params, cty) ->
-      List.iter Ctype.generalize params;
-      generalize_class_type cty
+      List.iter gen params;
+      generalize_class_type gen cty
   | Cty_signature {cty_self = sty; cty_vars = vars; cty_inher = inher} ->
-      Ctype.generalize sty;
-      Vars.iter (fun _ (_, _, ty) -> Ctype.generalize ty) vars;
-      List.iter (fun (_,tl) -> List.iter Ctype.generalize tl) inher
+      gen sty;
+      Vars.iter (fun _ (_, _, ty) -> gen ty) vars;
+      List.iter (fun (_,tl) -> List.iter gen tl) inher
   | Cty_arrow (_, ty, cty) ->
-      Ctype.generalize ty;
-      generalize_class_type cty
+      gen ty;
+      generalize_class_type gen cty
+
+let generalize_class_type vars =
+  let gen = if vars then Ctype.generalize else Ctype.generalize_structure in
+  generalize_class_type gen
 
 (* Return the virtual methods of a class type *)
 let virtual_methods sign =
@@ -497,7 +502,7 @@ let class_type env scty =
 (*******************************)
 
 let rec class_field self_loc cl_num self_type meths vars
-    (val_env, met_env, par_env, fields, concr_meths, warn_vals, inher)
+    (val_env, met_env, par_env, fields, concr_meths, warn_vals, inher, local_meths, local_vals)
   cf =
   let loc = cf.pcf_loc in
   let mkcf desc = { cf_desc = desc; cf_loc = loc; cf_attributes = cf.pcf_attributes } in
@@ -546,7 +551,7 @@ let rec class_field self_loc cl_num self_type meths vars
       (val_env, met_env, par_env,
        lazy (mkcf (Tcf_inherit (ovf, parent, super, inh_vars, inh_meths)))
        :: fields,
-       concr_meths, warn_vals, inher)
+       concr_meths, warn_vals, inher, local_meths, local_vals)
 
   | Pcf_val (lab, mut, Cfk_virtual styp) ->
       if !Clflags.principal then Ctype.begin_def ();
@@ -561,11 +566,14 @@ let rec class_field self_loc cl_num self_type meths vars
           val_env met_env par_env loc
       in
       (val_env, met_env', par_env,
-       lazy (mkcf (Tcf_val (lab, mut, id, Tcfk_virtual cty, met_env == met_env')))
+       lazy (mkcf (Tcf_val (lab, mut, id, Tcfk_virtual cty,
+                            met_env == met_env')))
              :: fields,
-             concr_meths, warn_vals, inher)
+             concr_meths, warn_vals, inher, local_meths, local_vals)
 
   | Pcf_val (lab, mut, Cfk_concrete (ovf, sexp)) ->
+      if Concr.mem lab.txt local_vals then
+        raise(Error(loc, val_env, Duplicate ("instance variable", lab.txt)));
       if Concr.mem lab.txt warn_vals then begin
         if ovf = Fresh then
           Location.prerr_warning lab.loc
@@ -592,14 +600,15 @@ let rec class_field self_loc cl_num self_type meths vars
        lazy (mkcf (Tcf_val (lab, mut, id,
                             Tcfk_concrete (ovf, exp), met_env == met_env')))
        :: fields,
-       concr_meths, Concr.add lab.txt warn_vals, inher)
+       concr_meths, Concr.add lab.txt warn_vals, inher, local_meths,
+       Concr.add lab.txt local_vals)
 
   | Pcf_method (lab, priv, Cfk_virtual sty) ->
       let cty = virtual_method val_env meths self_type lab.txt priv sty loc in
       (val_env, met_env, par_env,
         lazy (mkcf(Tcf_method (lab, priv, Tcfk_virtual cty)))
        ::fields,
-        concr_meths, warn_vals, inher)
+        concr_meths, warn_vals, inher, local_meths, local_vals)
 
   | Pcf_method (lab, priv, Cfk_concrete (ovf, expr))  ->
       let expr =
@@ -607,6 +616,8 @@ let rec class_field self_loc cl_num self_type meths vars
         | Pexp_poly _ -> expr
         | _ -> Ast_helper.Exp.poly ~loc:expr.pexp_loc expr None
       in
+      if Concr.mem lab.txt local_meths then
+        raise(Error(loc, val_env, Duplicate ("method", lab.txt)));
       if Concr.mem lab.txt concr_meths then begin
         if ovf = Fresh then
           Location.prerr_warning loc (Warnings.Method_override [lab.txt])
@@ -657,13 +668,14 @@ let rec class_field self_loc cl_num self_type meths vars
           mkcf (Tcf_method (lab, priv, Tcfk_concrete (ovf, texp)))
         end in
       (val_env, met_env, par_env, field::fields,
-       Concr.add lab.txt concr_meths, warn_vals, inher)
+       Concr.add lab.txt concr_meths, warn_vals, inher,
+       Concr.add lab.txt local_meths, local_vals)
 
   | Pcf_constraint (sty, sty') ->
       let (cty, cty') = type_constraint val_env sty sty' loc in
       (val_env, met_env, par_env,
         lazy (mkcf (Tcf_constraint (cty, cty'))) :: fields,
-        concr_meths, warn_vals, inher)
+        concr_meths, warn_vals, inher, local_meths, local_vals)
 
   | Pcf_initializer expr ->
       let expr = make_method self_loc cl_num expr in
@@ -680,7 +692,8 @@ let rec class_field self_loc cl_num self_type meths vars
           Ctype.end_def ();
           mkcf (Tcf_initializer texp)
         end in
-      (val_env, met_env, par_env, field::fields, concr_meths, warn_vals, inher)
+      (val_env, met_env, par_env, field::fields, concr_meths, warn_vals,
+       inher, local_meths, local_vals)
 
   | Pcf_extension (s, _arg) ->
       raise (Error (s.loc, val_env, Extension s.txt))
@@ -732,9 +745,10 @@ and class_structure cl_num final val_env met_env loc
   end;
 
   (* Typing of class fields *)
-  let (_, _, _, fields, concr_meths, _, inher) =
+  let (_, _, _, fields, concr_meths, _, inher, _local_meths, _local_vals) =
     List.fold_left (class_field self_loc cl_num self_type meths vars)
-      (val_env, meth_env, par_env, [], Concr.empty, Concr.empty, [])
+      (val_env, meth_env, par_env, [], Concr.empty, Concr.empty, [],
+       Concr.empty, Concr.empty)
       str
   in
   Ctype.unify val_env self_type (Ctype.newvar ());
@@ -935,7 +949,12 @@ and class_expr cl_num val_env met_env scl =
           cl_attributes = scl.pcl_attributes;
          }
   | Pcl_apply (scl', sargs) ->
+      if !Clflags.principal then Ctype.begin_def ();
       let cl = class_expr cl_num val_env met_env scl' in
+      if !Clflags.principal then begin
+        Ctype.end_def ();
+        generalize_class_type false cl.cl_type;
+      end;
       let rec nonopt_labels ls ty_fun =
         match ty_fun with
         | Cty_arrow (l, _, ty_res) ->
@@ -954,9 +973,10 @@ and class_expr cl_num val_env met_env scl =
           true
         end
       in
-      let rec type_args args omitted ty_fun sargs more_sargs =
-        match ty_fun with
-        | Cty_arrow (l, ty, ty_fun) when sargs <> [] || more_sargs <> [] ->
+      let rec type_args args omitted ty_fun ty_fun0 sargs more_sargs =
+        match ty_fun, ty_fun0 with
+        | Cty_arrow (l, ty, ty_fun), Cty_arrow (_, ty0, ty_fun0)
+          when sargs <> [] || more_sargs <> [] ->
             let name = Btype.label_name l
             and optional =
               if Btype.is_optional l then Optional else Required in
@@ -970,7 +990,7 @@ and class_expr cl_num val_env met_env scl =
                       raise(Error(sarg0.pexp_loc, val_env,
                                   Apply_wrong_label l'))
                     else ([], more_sargs,
-                          Some (type_argument val_env sarg0 ty ty))
+                          Some (type_argument val_env sarg0 ty ty0))
                 | _ ->
                     assert false
               end else try
@@ -989,21 +1009,23 @@ and class_expr cl_num val_env met_env scl =
                     (Warnings.Nonoptional_label l);
                 sargs, more_sargs,
                 if optional = Required || Btype.is_optional l' then
-                  Some (type_argument val_env sarg0 ty ty)
+                  Some (type_argument val_env sarg0 ty ty0)
                 else
-                  let ty0 = extract_option_type val_env ty in
-                  let arg = type_argument val_env sarg0 ty0 ty0 in
+                  let ty' = extract_option_type val_env ty
+                  and ty0' = extract_option_type val_env ty0 in
+                  let arg = type_argument val_env sarg0 ty' ty0' in
                   Some (option_some arg)
               with Not_found ->
                 sargs, more_sargs,
                 if Btype.is_optional l &&
                   (List.mem_assoc "" sargs || List.mem_assoc "" more_sargs)
                 then
-                  Some (option_none ty Location.none)
+                  Some (option_none ty0 Location.none)
                 else None
             in
-            let omitted = if arg = None then (l,ty) :: omitted else omitted in
-            type_args ((l,arg,optional)::args) omitted ty_fun sargs more_sargs
+            let omitted = if arg = None then (l,ty0) :: omitted else omitted in
+            type_args ((l,arg,optional)::args) omitted ty_fun ty_fun0
+              sargs more_sargs
         | _ ->
             match sargs @ more_sargs with
               (l, sarg0)::_ ->
@@ -1015,13 +1037,14 @@ and class_expr cl_num val_env met_env scl =
                 (List.rev args,
                  List.fold_left
                    (fun ty_fun (l,ty) -> Cty_arrow(l,ty,ty_fun))
-                   ty_fun omitted)
+                   ty_fun0 omitted)
       in
       let (args, cty) =
+        let (_, ty_fun0) = Ctype.instance_class [] cl.cl_type in
         if ignore_labels then
-          type_args [] [] cl.cl_type [] sargs
+          type_args [] [] cl.cl_type ty_fun0 [] sargs
         else
-          type_args [] [] cl.cl_type sargs []
+          type_args [] [] cl.cl_type ty_fun0 sargs []
       in
       rc {cl_desc = Tcl_apply (cl, args);
           cl_loc = scl.pcl_loc;
@@ -1149,7 +1172,7 @@ let temp_abbrev loc env id arity =
        type_kind = Type_abstract;
        type_private = Public;
        type_manifest = Some ty;
-       type_variance = List.map (fun _ -> true, true, true) !params;
+       type_variance = Misc.replicate_list Variance.full arity;
        type_newtype_level = None;
        type_loc = loc;
       }
@@ -1302,7 +1325,7 @@ let class_infos define_class kind
   end;
 
   (* Class and class type temporary definitions *)
-  let cty_variance = List.map (fun _ -> true, true) params in
+  let cty_variance = List.map (fun _ -> Variance.full) params in
   let cltydef =
     {clty_params = params; clty_type = class_body typ;
      clty_variance = cty_variance;
@@ -1363,7 +1386,7 @@ let class_infos define_class kind
      type_kind = Type_abstract;
      type_private = Public;
      type_manifest = Some obj_ty;
-     type_variance = List.map (fun _ -> true, true, true) obj_params;
+     type_variance = List.map (fun _ -> Variance.full) obj_params;
      type_newtype_level = None;
      type_loc = cl.pci_loc}
   in
@@ -1378,7 +1401,7 @@ let class_infos define_class kind
      type_kind = Type_abstract;
      type_private = Public;
      type_manifest = Some cl_ty;
-     type_variance = List.map (fun _ -> true, true, true) cl_params;
+     type_variance = List.map (fun _ -> Variance.full) cl_params;
      type_newtype_level = None;
      type_loc = cl.pci_loc}
   in
@@ -1396,21 +1419,12 @@ let final_decl env define_class
   end;
 
   List.iter Ctype.generalize clty.cty_params;
-  generalize_class_type clty.cty_type;
-  begin match clty.cty_new with
-    None -> ()
-  | Some ty -> Ctype.generalize ty
-  end;
+  generalize_class_type true clty.cty_type;
+  Misc.may  Ctype.generalize clty.cty_new;
   List.iter Ctype.generalize obj_abbr.type_params;
-  begin match obj_abbr.type_manifest with
-    None    -> ()
-  | Some ty -> Ctype.generalize ty
-  end;
+  Misc.may  Ctype.generalize obj_abbr.type_manifest;
   List.iter Ctype.generalize cl_abbr.type_params;
-  begin match cl_abbr.type_manifest with
-    None    -> ()
-  | Some ty -> Ctype.generalize ty
-  end;
+  Misc.may  Ctype.generalize cl_abbr.type_manifest;
 
   if not (closed_class clty) then
     raise(Error(cl.pci_loc, env, Non_generalizable_class (id, clty)));
@@ -1758,6 +1772,9 @@ let report_error env ppf = function
         "instance variable"
   | No_overriding (kind, name) ->
       fprintf ppf "@[The %s `%s'@ has no previous definition@]" kind name
+  | Duplicate (kind, name) ->
+      fprintf ppf "@[The %s `%s'@ has multiple definitions in this object@]"
+                    kind name
   | Extension s ->
       fprintf ppf "Uninterpreted extension '%s'." s
 
diff --git a/typing/typeclass.mli b/typing/typeclass.mli
index 81e56bd1b5..abc8633bc3 100644
--- a/typing/typeclass.mli
+++ b/typing/typeclass.mli
@@ -103,6 +103,7 @@ type error =
   | Final_self_clash of (type_expr * type_expr) list
   | Mutability_mismatch of string * mutable_flag
   | No_overriding of string * string
+  | Duplicate of string * string
   | Extension of string
 
 exception Error of Location.t * Env.t * error
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 46a583ecb6..c35cb162a6 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -34,7 +34,7 @@ type error =
   | Label_missing of Ident.t list
   | Label_not_mutable of Longident.t
   | Wrong_name of string * Path.t * Longident.t
-  | Name_type_mismatch of 
+  | Name_type_mismatch of
       string * Longident.t * (Path.t * Path.t) * (Path.t * Path.t) list
   | Incomplete_format of string
   | Bad_conversion of string * int * char
@@ -108,6 +108,7 @@ let rp node =
 ;;
 
 
+let fst3 (x, _, _) = x
 let snd3 (_,x,_) = x
 
 let case lhs rhs =
@@ -136,7 +137,7 @@ let iter_expression f e =
     | Pexp_variant (_, eo) -> may expr eo
     | Pexp_record (iel, eo) ->
         may expr eo; List.iter (fun (_, e) -> expr e) iel
-    | Pexp_open (_, e)
+    | Pexp_open (_, _, e)
     | Pexp_newtype (_, e)
     | Pexp_poly (e, _)
     | Pexp_lazy e
@@ -602,16 +603,20 @@ end) = struct
       end
     | _ -> raise Not_found
 
-  let is_ambiguous env lbl others =
+  let rec unique eq acc = function
+      [] -> List.rev acc
+    | x :: rem ->
+        if List.exists (eq x) acc then unique eq acc rem
+        else unique eq (x :: acc) rem
+
+  let ambiguous_types env lbl others =
     let tpath = get_type_path env lbl in
-    let different_tpath (lbl, _) =
-      let lbl_tpath = get_type_path env lbl in
-      not (compare_type_path env tpath lbl_tpath)
-    in
     let others =
-      List.filter different_tpath others
-    in
-    others <> []
+      List.map (fun (lbl, _) -> get_type_path env lbl) others in
+    let tpaths = unique (compare_type_path env) [tpath] others in
+    match tpaths with
+      [_] -> []
+    | _ -> List.map Printtyp.string_of_path tpaths
 
   let disambiguate_by_type env tpath lbls =
     let check_type (lbl, _) =
@@ -629,9 +634,11 @@ end) = struct
           [] -> unbound_name_error env lid
 	| (lbl, use) :: rest ->
 	    use ();
-	    if is_ambiguous env lbl rest then
+            let paths = ambiguous_types env lbl rest in
+	    if paths <> [] then
 	      warn lid.loc
-		(Warnings.Ambiguous_name ([Longident.last lid.txt], false));
+		(Warnings.Ambiguous_name ([Longident.last lid.txt],
+                                          paths, false));
 	    lbl
 	end
     | Some(tpath0, tpath, pr) ->
@@ -651,16 +658,20 @@ end) = struct
             | (lbl', use') :: rest ->
                 let lbl_tpath = get_type_path env lbl' in
                 if not (compare_type_path env tpath lbl_tpath) then warn_pr ()
-                else if is_ambiguous env lbl' rest then
-                  warn lid.loc
-                    (Warnings.Ambiguous_name ([Longident.last lid.txt], false))
+                else
+                  let paths = ambiguous_types env lbl rest in
+                  if paths <> [] then
+                    warn lid.loc
+                      (Warnings.Ambiguous_name ([Longident.last lid.txt],
+                                                paths, false))
           end;
           lbl
         with Not_found -> try
           let lbl = lookup_from_type env tpath lid in
           check_lk tpath lbl;
+          let s = Printtyp.string_of_path tpath in
           warn lid.loc
-            (Warnings.Name_out_of_scope ([Longident.last lid.txt], false));
+            (Warnings.Name_out_of_scope (s, [Longident.last lid.txt], false));
           if not pr then warn_pr ();
           lbl
 	with Not_found ->
@@ -712,13 +723,15 @@ let disambiguate_label_by_ids keep env closed ids labels =
 (* Only issue warnings once per record constructor/pattern *)
 let disambiguate_lid_a_list loc closed env opath lid_a_list =
   let ids = List.map (fun (lid, _) -> Longident.last lid.txt) lid_a_list in
-  let w_pr = ref false and w_amb = ref [] and w_scope = ref [] in
+  let w_pr = ref false and w_amb = ref []
+  and w_scope = ref [] and w_scope_ty = ref "" in
   let warn loc msg =
     let open Warnings in
     match msg with
     | Not_principal _ -> w_pr := true
-    | Ambiguous_name([s], _) -> w_amb := s :: !w_amb
-    | Name_out_of_scope([s], _) -> w_scope := s :: !w_scope
+    | Ambiguous_name([s], l, _) -> w_amb := (s, l) :: !w_amb
+    | Name_out_of_scope(ty, [s], _) ->
+        w_scope := s :: !w_scope; w_scope_ty := ty
     | _ -> Location.prerr_warning loc msg
   in
   let process_label lid =
@@ -747,13 +760,26 @@ let disambiguate_lid_a_list loc closed env opath lid_a_list =
     List.map (fun (lid,a) -> lid, process_label lid, a) lid_a_list in
   if !w_pr then
     Location.prerr_warning loc
-      (Warnings.Not_principal "this type-based record disambiguation");
-  if !w_amb <> [] && not !w_pr then
-    Location.prerr_warning loc
-      (Warnings.Ambiguous_name (List.rev !w_amb, true));
+      (Warnings.Not_principal "this type-based record disambiguation")
+  else begin
+    match List.rev !w_amb with
+      (_,types)::others as amb ->
+        let paths =
+          List.map (fun (_,lbl,_) -> Label.get_type_path env lbl) lbl_a_list in
+        let path = List.hd paths in
+        if List.for_all (compare_type_path env path) (List.tl paths) then
+          Location.prerr_warning loc
+            (Warnings.Ambiguous_name (List.map fst amb, types, true))
+        else
+          List.iter
+            (fun (s,l) -> Location.prerr_warning loc
+                (Warnings.Ambiguous_name ([s],l,false)))
+            amb
+    | _ -> ()
+  end;
   if !w_scope <> [] then
     Location.prerr_warning loc
-      (Warnings.Name_out_of_scope (List.rev !w_scope, true));
+      (Warnings.Name_out_of_scope (!w_scope_ty, List.rev !w_scope, true));
   lbl_a_list
 
 let rec find_record_qual = function
@@ -1290,9 +1316,6 @@ let force_delayed_checks () =
   reset_delayed_checks ();
   Btype.backtrack snap
 
-let fst3 (x, _, _) = x
-let snd3 (_, x, _) = x
-
 let rec final_subexpression sexp =
   match sexp.pexp_desc with
     Pexp_let (_, _, e)
@@ -1315,6 +1338,12 @@ let rec is_nonexpansive exp =
   | Texp_function _ -> true
   | Texp_apply(e, (_,None,_)::el) ->
       is_nonexpansive e && List.for_all is_nonexpansive_opt (List.map snd3 el)
+  | Texp_match(e, cases, _) ->
+      is_nonexpansive e &&
+      List.for_all
+        (fun {c_lhs = _; c_guard; c_rhs} ->
+           is_nonexpansive_opt c_guard && is_nonexpansive c_rhs
+        ) cases
   | Texp_tuple el ->
       List.for_all is_nonexpansive el
   | Texp_construct( _, _, el) ->
@@ -2717,11 +2746,13 @@ and type_expect_ ?in_function env sexp ty_expected =
         exp_type = newty (Tpackage (p, nl, tl'));
         exp_attributes = sexp.pexp_attributes;
         exp_env = env }
-  | Pexp_open (lid, e) ->
-      let (path, newenv) = !type_open env sexp.pexp_loc lid in
+  | Pexp_open (ovf, lid, e) ->
+      let (path, newenv) = !type_open ovf env sexp.pexp_loc lid in
       let exp = type_expect newenv e ty_expected in
       { exp with
-        exp_extra = (Texp_open (path, lid, newenv), loc, sexp.pexp_attributes) :: exp.exp_extra;
+        exp_extra = (Texp_open (ovf, path, lid, newenv), loc,
+                     sexp.pexp_attributes) ::
+                      exp.exp_extra;
       }
   | Pexp_extension (s, _arg) ->
       raise (Error (s.loc, env, Extension s.txt))
@@ -2855,7 +2886,7 @@ and type_argument env sarg ty_expected' ty_expected =
   let rec is_inferred sexp =
     match sexp.pexp_desc with
       Pexp_ident _ | Pexp_apply _ | Pexp_send _ | Pexp_field _ -> true
-    | Pexp_open (_, e) -> is_inferred e
+    | Pexp_open (_, _, e) -> is_inferred e
     | _ -> false
   in
   match expand_head env ty_expected' with
diff --git a/typing/typecore.mli b/typing/typecore.mli
index 9c9e036f20..e5e8516da5 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -115,7 +115,7 @@ val report_error: Env.t -> formatter -> error -> unit
 (* Forward declaration, to be filled in by Typemod.type_module *)
 val type_module: (Env.t -> Parsetree.module_expr -> Typedtree.module_expr) ref
 (* Forward declaration, to be filled in by Typemod.type_open *)
-val type_open: (Env.t -> Location.t -> Longident.t loc -> Path.t * Env.t) ref
+val type_open: (override_flag -> Env.t -> Location.t -> Longident.t loc -> Path.t * Env.t) ref
 (* Forward declaration, to be filled in by Typeclass.class_structure *)
 val type_object:
   (Env.t -> Location.t -> Parsetree.class_structure ->
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index d64c697809..c6c92ff2de 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -35,7 +35,7 @@ type error =
   | Unbound_type_var of type_expr * type_declaration
   | Unbound_exception of Longident.t
   | Not_an_exception of Longident.t
-  | Bad_variance of int * (bool * bool) * (bool * bool)
+  | Bad_variance of int * (bool * bool * bool) * (bool * bool * bool)
   | Unavailable_type_constructor of Path.t
   | Bad_fixed_type of string
   | Unbound_type_var_exc of type_expr * type_expr
@@ -58,7 +58,7 @@ let enter_type env sdecl id =
       type_manifest =
         begin match sdecl.ptype_manifest with None -> None
         | Some _ -> Some(Ctype.newvar ()) end;
-      type_variance = List.map (fun _ -> true, true, true) sdecl.ptype_params;
+      type_variance = List.map (fun _ -> Variance.full) sdecl.ptype_params;
       type_newtype_level = None;
       type_loc = sdecl.ptype_loc;
     }
@@ -121,7 +121,7 @@ let set_fixed_row env loc p decl =
 module StringSet =
   Set.Make(struct
     type t = string
-    let compare = compare
+    let compare (x:t) y = compare x y
   end)
 
 let make_params sdecl =
@@ -165,7 +165,8 @@ let transl_declaration env sdecl id =
           let name = Ident.create lid.txt in
           match ret_type with
             | None ->
-              (name, lid, List.map (transl_simple_type env true) args, None, None, loc, attrs)
+              (name, lid, List.map (transl_simple_type env true) args,
+               None, None, loc, attrs)
             | Some sty ->
               (* if it's a generalized constructor we must first narrow and
                  then widen so as to not introduce any new constraints *)
@@ -232,7 +233,7 @@ let transl_declaration env sdecl id =
         type_kind = kind;
         type_private = sdecl.ptype_private;
         type_manifest = man;
-        type_variance = List.map (fun _ -> true, true, true) params;
+        type_variance = List.map (fun _ -> Variance.full) params;
         type_newtype_level = None;
         type_loc = sdecl.ptype_loc;
       } in
@@ -319,6 +320,8 @@ let rec check_constraints_rec env loc visited ty =
       Btype.iter_type_expr (check_constraints_rec env loc visited) ty
   end
 
+module SMap = Map.Make(String)
+
 let check_constraints env sdecl (_, decl) =
   let visited = ref TypeSet.empty in
   begin match decl.type_kind with
@@ -329,12 +332,16 @@ let check_constraints env sdecl (_, decl) =
         | Ptype_record _ | Ptype_abstract -> assert false
       in
       let pl = find_pl sdecl.ptype_kind in
+      let pl_index =
+        let foldf acc x =
+          SMap.add x.pcd_name.txt x acc
+        in
+        List.fold_left foldf SMap.empty pl
+      in
       List.iter
         (fun (name, tyl, ret_type) ->
-          let (styl, sret_type) =
-            try
-              let pcd = List.find (fun pcd -> pcd.pcd_name.txt = Ident.name name)  pl in
-              pcd.pcd_args, pcd.pcd_res
+          let {pcd_args = styl; pcd_res = sret_type; _} =
+            try SMap.find (Ident.name name) pl_index
             with Not_found -> assert false in
           List.iter2
             (fun sty ty ->
@@ -376,7 +383,7 @@ let check_constraints env sdecl (_, decl) =
    need to check that the equation refers to a type of the same kind
    with the same constructors and labels.
 *)
-let check_abbrev env sdecl (id, decl) =
+let check_coherence env loc id decl =
   match decl with
     {type_kind = (Type_variant _ | Type_record _); type_manifest = Some ty} ->
       begin match (Ctype.repr ty).desc with
@@ -397,14 +404,17 @@ let check_abbrev env sdecl (id, decl) =
                      (Subst.add_type id path Subst.identity) decl)
             in
             if err <> [] then
-              raise(Error(sdecl.ptype_loc, Definition_mismatch (ty, err)))
+              raise(Error(loc, Definition_mismatch (ty, err)))
           with Not_found ->
-            raise(Error(sdecl.ptype_loc, Unavailable_type_constructor path))
+            raise(Error(loc, Unavailable_type_constructor path))
           end
-      | _ -> raise(Error(sdecl.ptype_loc, Definition_mismatch (ty, [])))
+      | _ -> raise(Error(loc, Definition_mismatch (ty, [])))
       end
   | _ -> ()
 
+let check_abbrev env sdecl (id, decl) =
+  check_coherence env sdecl.ptype_loc id decl
+
 (* Check that recursion is well-founded *)
 
 let check_well_founded env loc path decl =
@@ -482,77 +492,91 @@ let check_abbrev_recursion env id_loc_list tdecl =
 
 (* Compute variance *)
 
-let compute_variance env tvl nega posi cntr ty =
-  let pvisited = ref TypeSet.empty
-  and nvisited = ref TypeSet.empty
-  and cvisited = ref TypeSet.empty in
-  let rec compute_variance_rec posi nega cntr ty =
+module TypeMap = Btype.TypeMap
+
+let get_variance ty visited =
+  try TypeMap.find ty !visited with Not_found -> Variance.null
+
+let compute_variance env visited vari ty =
+  let rec compute_variance_rec vari ty =
+    (* Format.eprintf "%a: %x@." Printtyp.type_expr ty (Obj.magic vari); *)
     let ty = Ctype.repr ty in
-    if (not posi || TypeSet.mem ty !pvisited)
-    && (not nega || TypeSet.mem ty !nvisited)
-    && (not cntr || TypeSet.mem ty !cvisited) then
-      ()
-    else begin
-      if posi then pvisited := TypeSet.add ty !pvisited;
-      if nega then nvisited := TypeSet.add ty !nvisited;
-      if cntr then cvisited := TypeSet.add ty !cvisited;
-      let compute_same = compute_variance_rec posi nega cntr in
-      match ty.desc with
-        Tarrow (_, ty1, ty2, _) ->
-          compute_variance_rec nega posi true ty1;
-          compute_same ty2
-      | Ttuple tl ->
-          List.iter compute_same tl
-      | Tconstr (path, tl, _) ->
-          if tl = [] then () else begin
-            try
-              let decl = Env.find_type path env in
-              List.iter2
-                (fun ty (co,cn,ct) ->
-                  compute_variance_rec
-                    (posi && co || nega && cn)
-                    (posi && cn || nega && co)
-                    (cntr || ct)
-                    ty)
-                tl decl.type_variance
-            with Not_found ->
-              List.iter (compute_variance_rec true true true) tl
-          end
-      | Tobject (ty, _) ->
-          compute_same ty
-      | Tfield (_, _, ty1, ty2) ->
-          compute_same ty1;
-          compute_same ty2
-      | Tsubst ty ->
-          compute_same ty
-      | Tvariant row ->
-          let row = Btype.row_repr row in
-          List.iter
-            (fun (_,f) ->
-              match Btype.row_field_repr f with
-                Rpresent (Some ty) ->
-                  compute_same ty
-              | Reither (_, tyl, _, _) ->
-                  List.iter compute_same tyl
-              | _ -> ())
-            row.row_fields;
-          compute_same row.row_more
-      | Tpoly (ty, _) ->
-          compute_same ty
-      | Tvar _ | Tnil | Tlink _ | Tunivar _ -> ()
-      | Tpackage (_, _, tyl) ->
-          List.iter (compute_variance_rec true true true) tyl
-    end
+    let vari' = get_variance ty visited in
+    if Variance.subset vari vari' then () else
+    let vari = Variance.union vari vari' in
+    visited := TypeMap.add ty vari !visited;
+    let compute_same = compute_variance_rec vari in
+    match ty.desc with
+      Tarrow (_, ty1, ty2, _) ->
+        let open Variance in
+        let v = conjugate vari in
+        let v1 =
+          if mem May_pos v || mem May_neg v
+          then set May_weak true v else v
+        in
+        compute_variance_rec v1 ty1;
+        compute_same ty2
+    | Ttuple tl ->
+        List.iter compute_same tl
+    | Tconstr (path, tl, _) ->
+        let open Variance in
+        if tl = [] then () else begin
+          try
+            let decl = Env.find_type path env in
+            let cvari f = mem f vari in
+            List.iter2
+              (fun ty v ->
+                let cv f = mem f v in
+                let strict =
+                  cvari Inv && cv Inj || (cvari Pos || cvari Neg) && cv Inv
+                in
+                if strict then compute_variance_rec full ty else
+                let p1 = inter v vari
+                and n1 = inter v (conjugate vari) in
+                let v1 = 
+                  union (inter covariant (union p1 (conjugate p1)))
+                    (inter (conjugate covariant) (union n1 (conjugate n1)))
+                and weak =
+                  cvari May_weak && (cv May_pos || cv May_neg) ||
+                  (cvari May_pos || cvari May_neg) && cv May_weak
+                in
+                let v2 = set May_weak weak v1 in
+                compute_variance_rec v2 ty)
+              tl decl.type_variance
+          with Not_found ->
+            List.iter (compute_variance_rec may_inv) tl
+        end
+    | Tobject (ty, _) ->
+        compute_same ty
+    | Tfield (_, _, ty1, ty2) ->
+        compute_same ty1;
+        compute_same ty2
+    | Tsubst ty ->
+        compute_same ty
+    | Tvariant row ->
+        let row = Btype.row_repr row in
+        List.iter
+          (fun (_,f) ->
+            match Btype.row_field_repr f with
+              Rpresent (Some ty) ->
+                compute_same ty
+            | Reither (_, tyl, _, _) ->
+                List.iter compute_same tyl
+            | _ -> ())
+          row.row_fields;
+        compute_same row.row_more
+    | Tpoly (ty, _) ->
+        compute_same ty
+    | Tvar _ | Tnil | Tlink _ | Tunivar _ -> ()
+    | Tpackage (_, _, tyl) ->
+        let v =
+          Variance.(if mem Pos vari || mem Neg vari then full else may_inv)
+        in
+        List.iter (compute_variance_rec v) tyl
   in
-  compute_variance_rec nega posi cntr ty;
-  List.iter
-    (fun (ty, covar, convar, ctvar) ->
-      if TypeSet.mem ty !pvisited then covar := true;
-      if TypeSet.mem ty !nvisited then convar := true;
-      if TypeSet.mem ty !cvisited then ctvar := true)
-    tvl
+  compute_variance_rec vari ty
 
-let make_variance ty = (ty, ref false, ref false, ref false)
+let make_variance ty = (ty, ref Variance.null)
 let whole_type decl =
   match decl.type_kind with
     Type_variant tll ->
@@ -566,54 +590,110 @@ let whole_type decl =
         Some ty -> ty
       | _ -> Btype.newgenty (Ttuple [])
 
+let make p n i =
+  let open Variance in
+  set May_pos p (set May_neg n (set May_weak n (set Inj i null)))
+
+let flags (v, i) =
+  let (c, n) =
+    match v with
+    | Covariant -> (true, false)
+    | Contravariant -> (false, true)
+    | Invariant -> (true, true)
+  in
+  (c, n, i)
+
 let compute_variance_type env check (required, loc) decl tyl =
-  let params = List.map Btype.repr decl.type_params in
-  let tvl0 = List.map make_variance params in
-  let args = Btype.newgenty (Ttuple params) in
-  let fvl = if check then Ctype.free_variables args else [] in
-  let fvl = List.filter (fun v -> not (List.memq v params)) fvl in
-  let tvl1 = List.map make_variance fvl in
-  let tvl2 = List.map make_variance fvl in
-  let tvl = tvl0 @ tvl1 in
-  List.iter (fun (cn,ty) -> compute_variance env tvl true cn cn ty) tyl;
+  (* Requirements *)
   let required =
-    List.map
-      (function
-        | Covariant -> (true, false)
-        | Contravariant -> (false, true)
-        | Invariant -> (true, true)
-      )
+    List.map (fun (c,n,i) -> if c || n then (c,n,i) else (true,true,i))
       required
   in
-  List.iter2
-    (fun (ty, co, cn, ct) (c, n) ->
-      if not (Btype.is_Tvar ty) then begin
-        co := c; cn := n; ct := n;
-        compute_variance env tvl2 c n n ty
-      end)
-    tvl0 required;
-  List.iter2
-    (fun (ty, c1, n1, t1) (_, c2, n2, t2) ->
-      if !c1 && not !c2 || !n1 && not !n2
-      then raise (Error(loc, Bad_variance (0, (!c1,!n1), (!c2,!n2)))))
-    tvl1 tvl2;
-  let pos = ref 0 in
+  (* Prepare *)
+  let params = List.map Btype.repr decl.type_params in
+  let tvl = ref TypeMap.empty in
+  (* Compute occurences in body *)
+  let open Variance in
+  List.iter
+    (fun (cn,ty) ->
+      compute_variance env tvl (if cn then full else covariant) ty)
+    tyl;
+  if check then begin
+    (* Check variance of parameters *)
+    let pos = ref 0 in
+    List.iter2
+      (fun ty (c, n, i) ->
+        incr pos;
+        let var = get_variance ty tvl in
+        let (co,cn) = get_upper var and ij = mem Inj var in
+        if Btype.is_Tvar ty && (co && not c || cn && not n || not ij && i)
+        then raise (Error(loc, Bad_variance (!pos, (co,cn,ij), (c,n,i)))))
+      params required;
+    (* Check propagation from constrained parameters *)
+    let args = Btype.newgenty (Ttuple params) in
+    let fvl = Ctype.free_variables args in
+    let fvl = List.filter (fun v -> not (List.memq v params)) fvl in
+    (* If there are no extra variables there is nothing to do *)
+    if fvl = [] then () else
+    let tvl2 = ref TypeMap.empty in
+    List.iter2
+      (fun ty (p,n,i) ->
+        if Btype.is_Tvar ty then () else
+        let v =
+          if p then if n then full else covariant else conjugate covariant in
+        compute_variance env tvl2 v ty)
+      params required;
+    let visited = ref TypeSet.empty in
+    let rec check ty =
+      let ty = Ctype.repr ty in
+      if TypeSet.mem ty !visited then () else
+      let visited' = TypeSet.add ty !visited in
+      visited := visited';
+      let v1 = get_variance ty tvl in
+      let snap = Btype.snapshot () in
+      let v2 =
+        TypeMap.fold
+          (fun t vt v ->
+            if Ctype.equal env false [ty] [t] then union vt v else v)
+          !tvl2 null in
+      Btype.backtrack snap;
+      let (c1,n1) = get_upper v1 and (c2,n2,_,i2) = get_lower v2 in
+      if c1 && not c2 || n1 && not n2 then
+        if List.memq ty fvl then 
+          let code = if not i2 then -2 else if c2 || n2 then -1 else -3 in
+          raise (Error (loc, Bad_variance (code, (c1,n1,false), (c2,n2,false))))
+        else
+          Btype.iter_type_expr check ty
+    in
+    List.iter (fun (_,ty) -> check ty) tyl;
+  end;
   List.map2
-    (fun (_, co, cn, ct) (c, n) ->
-      incr pos;
-      if !co && not c || !cn && not n
-      then raise (Error(loc, Bad_variance (!pos, (!co,!cn), (c,n))));
-      if decl.type_private = Private then (c,n,n) else
-      let ct = if decl.type_kind = Type_abstract then ct else cn in
-      (!co, !cn, !ct))
-    tvl0 required
+    (fun ty (p, n, i) ->
+      let v = get_variance ty tvl in
+      let tr = decl.type_private in
+      (* Use required variance where relevant *)
+      let concr = decl.type_kind <> Type_abstract (*|| tr = Type_new*) in
+      let (p, n) =
+        if tr = Private || not (Btype.is_Tvar ty) then (p, n) (* set *)
+        else (false, false) (* only check *)
+      and i = concr  || i && tr = Private in
+      let v = union v (make p n i) in
+      let v =
+        if not concr then v else
+        if mem Pos v && mem Neg v then full else
+        if Btype.is_Tvar ty then v else
+        union v
+          (if p then if n then full else covariant else conjugate covariant)
+      in
+      if decl.type_kind = Type_abstract && tr = Public then v else
+      set May_weak (mem May_neg v) v)
+    params required
 
 let add_false = List.map (fun ty -> false, ty)
 
 (* 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
@@ -627,14 +707,16 @@ let compute_variance_gadt env check (required, loc as rloc) decl
   | Some ret_type ->
       match Ctype.repr ret_type with
       | {desc=Tconstr (path, tyl, _)} ->
+          (* let tyl = List.map (Ctype.expand_head env) tyl in *)
+          let tyl = List.map Ctype.repr tyl in
           let fvl = List.map Ctype.free_variables tyl in
           let _ =
             List.fold_left2
-              (fun (fv1,fv2) ty variance ->
+              (fun (fv1,fv2) ty (c,n,i) ->
                 match fv2 with [] -> assert false
                 | fv :: fv2 ->
                     (* fv1 @ fv2 = free_variables of other parameters *)
-                    if (variance <> Invariant) && constrained env (fv1 @ fv2) ty then
+                    if (c||n) && constrained env (fv1 @ fv2) ty then
                       raise (Error(loc, Varying_anonymous));
                     (fv :: fv1, fv2))
               ([], fvl) tyl required
@@ -647,30 +729,37 @@ let compute_variance_gadt env check (required, loc as rloc) decl
 let compute_variance_decl env check decl (required, loc as rloc) =
   if decl.type_kind = Type_abstract && decl.type_manifest = None then
     List.map
-      (function
-        | Covariant -> (true, false, false)
-        | Contravariant -> (false, true, true)
-        | Invariant -> (true, true, true)
-      )
+      (fun (c, n, i) ->
+        make (not n) (not c) (i (*|| decl.type_transparence = Type_new*)))
       required
-  else match decl.type_kind with
-  | Type_abstract ->
-      begin match decl.type_manifest with
-        None -> assert false
-      | Some ty -> compute_variance_type env check rloc decl [false, ty]
-      end
+  else
+  let mn =
+    match decl.type_manifest with
+      None -> []
+    | Some ty -> [false, ty]
+  in
+  match decl.type_kind with
+    Type_abstract ->
+      compute_variance_type env check rloc decl mn
   | Type_variant tll ->
       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)))
+          (mn @ add_false (List.flatten (List.map (fun (_,tyl,_) -> tyl) tll)))
       else begin
+        let mn =
+          List.map (fun (_,ty) -> (Ident.create_persistent"",[ty],None)) mn in
+        let tll = mn @ tll in
         match List.map (compute_variance_gadt env check rloc decl) tll with
-        | vari :: _ -> vari
+        | vari :: rem ->
+            let varl = List.fold_left (List.map2 Variance.union) vari rem in
+            List.map
+              Variance.(fun v -> if mem Pos v && mem Neg v then full else v)
+              varl
         | _ -> assert false
       end
   | Type_record (ftl, _) ->
       compute_variance_type env check rloc decl
-        (List.map (fun (_, mut, ty) -> (mut = Mutable, ty)) ftl)
+        (mn @ List.map (fun (_, mut, ty) -> (mut = Mutable, ty)) ftl)
 
 let is_sharp id =
   let s = Ident.name id in
@@ -692,12 +781,17 @@ let rec compute_variance_fixpoint env decls required variances =
       new_decls required
   in
   let new_variances =
-    List.map2
-      (List.map2 (fun (c1,n1,t1) (c2,n2,t2) -> c1||c2, n1||n2, t1||t2))
-      new_variances variances in
+    List.map2 (List.map2 Variance.union) new_variances variances in
   if new_variances <> variances then
     compute_variance_fixpoint env decls required new_variances
   else begin
+    (* List.iter (fun (id, decl) ->
+      Printf.eprintf "%s:" (Ident.name id);
+      List.iter (fun (v : Variance.t) ->
+        Printf.eprintf " %x" (Obj.magic v : int))
+        decl.type_variance;
+      prerr_endline "")
+      new_decls; *)
     List.iter2
       (fun (id, decl) req -> if not (is_sharp id) then
         ignore (compute_variance_decl new_env true decl req))
@@ -706,7 +800,15 @@ let rec compute_variance_fixpoint env decls required variances =
   end
 
 let init_variance (id, decl) =
-  List.map (fun _ -> (false, false, false)) decl.type_params
+  List.map (fun _ -> Variance.null) decl.type_params
+
+let add_injectivity =
+  List.map
+    (function
+      | Covariant -> (true, false, false)
+      | Contravariant -> (false, true, false)
+      | Invariant -> (false, false, false)
+    )
 
 (* for typeclass.ml *)
 let compute_variance_decls env cldecls =
@@ -714,15 +816,16 @@ let compute_variance_decls env cldecls =
     List.fold_right
       (fun (obj_id, obj_abbr, cl_abbr, clty, cltydef, ci) (decls, req) ->
         let variance = List.map snd ci.ci_params in
-        (obj_id, obj_abbr) :: decls, (variance, ci.ci_loc) :: req)
+        (obj_id, obj_abbr) :: decls,
+        (add_injectivity variance, ci.ci_loc) :: req)
       cldecls ([],[])
   in
   let variances = List.map init_variance decls in
   let (decls, _) = compute_variance_fixpoint env decls required variances in
   List.map2
     (fun (_,decl) (_, _, cl_abbr, clty, cltydef, _) ->
-      let variance = List.map (fun (c,n,t) -> (c,n)) decl.type_variance in
-      (decl, {cl_abbr with type_variance = decl.type_variance},
+      let variance = decl.type_variance in
+      (decl, {cl_abbr with type_variance = variance},
        {clty with cty_variance = variance},
        {cltydef with clty_variance = variance}))
     decls cldecls
@@ -859,8 +962,6 @@ let transl_type_decl env sdecl_list =
          Some ty -> raise(Error(sdecl.ptype_loc, Unbound_type_var(ty,decl)))
        | None   -> ())
     sdecl_list tdecls;
-  (* Check re-exportation *)
-  List.iter2 (check_abbrev newenv) sdecl_list decls;
   (* Check that constraints are enforced *)
   List.iter2 (check_constraints newenv) sdecl_list decls;
   (* Name recursion *)
@@ -870,12 +971,19 @@ let transl_type_decl env sdecl_list =
   in
   (* Add variances to the environment *)
   let required =
-    List.map (fun sdecl -> List.map snd sdecl.ptype_params, sdecl.ptype_loc)
+    List.map
+      (fun sdecl ->
+         add_injectivity (List.map snd sdecl.ptype_params),
+         sdecl.ptype_loc
+      )
       sdecl_list
   in
   let final_decls, final_env =
     compute_variance_fixpoint env decls required (List.map init_variance decls)
   in
+  (* Check re-exportation *)
+  List.iter2 (check_abbrev final_env) sdecl_list final_decls;
+  (* Keep original declaration *)
   let final_decls =
     List.map2
       (fun tdecl (id2, decl) ->
@@ -1018,7 +1126,7 @@ let transl_with_constraint env id row_path orig_decl sdecl =
   let decl =
     {decl with type_variance =
      compute_variance_decl env false decl
-       (List.map snd sdecl.ptype_params, sdecl.ptype_loc)} in
+       (add_injectivity (List.map snd sdecl.ptype_params), sdecl.ptype_loc)} in
   Ctype.end_def();
   generalize_decl decl;
   {
@@ -1046,7 +1154,7 @@ let abstract_type_decl arity =
       type_kind = Type_abstract;
       type_private = Public;
       type_manifest = None;
-      type_variance = replicate_list (true, true, true) arity;
+      type_variance = replicate_list Variance.full arity;
       type_newtype_level = None;
       type_loc = Location.none;
      } in
@@ -1181,11 +1289,13 @@ let report_error ppf = function
       fprintf ppf "The constructor@ %a@ is not an exception"
         Printtyp.longident lid
   | Bad_variance (n, v1, v2) ->
-      let variance = function
-          (true, true)  -> "invariant"
-        | (true, false) -> "covariant"
-        | (false,true)  -> "contravariant"
-        | (false,false) -> "unrestricted"
+      let variance (p,n,i) =
+        let inj = if i then "injective " else "" in
+        match p, n with
+          true,  true  -> inj ^ "invariant"
+        | true,  false -> inj ^ "covariant"
+        | false, true  -> inj ^ "contravariant"
+        | false, false -> if inj = "" then "unrestricted" else inj
       in
       let suffix n =
         let teen = (n mod 100)/10 = 1 in
@@ -1195,17 +1305,26 @@ let report_error ppf = function
         | 3 when not teen -> "rd"
         | _ -> "th"
       in
-      if n < 1 then
-        fprintf ppf "@[%s@ %s@]"
+      if n = -1 then
+        fprintf ppf "@[%s@ %s@ It"
           "In this definition, a type variable has a variance that"
           "is not reflected by its occurrence in type parameters."
+      else if n = -2 then
+        fprintf ppf "@[%s@ %s@]"
+          "In this definition, a type variable cannot be deduced"
+          "from the type parameters."
+      else if n = -3 then
+        fprintf ppf "@[%s@ %s@ It"
+          "In this definition, a type variable has a variance that"
+          "cannot be deduced from the type parameters."
       else
-        fprintf ppf "@[%s@ %s@ %s %d%s %s %s,@ %s %s@]"
+        fprintf ppf "@[%s@ %s@ The %d%s type parameter"
           "In this definition, expected parameter"
           "variances are not satisfied."
-          "The" n (suffix n)
-          "type parameter was expected to be" (variance v2)
-          "but it is" (variance v1)
+          n (suffix n);
+      if n <> -2 then
+        fprintf ppf " was expected to be %s,@ but it is %s.@]"
+          (variance v2) (variance v1)
   | Unavailable_type_constructor p ->
       fprintf ppf "The definition of type %a@ is unavailable" Printtyp.path p
   | Bad_fixed_type r ->
diff --git a/typing/typedecl.mli b/typing/typedecl.mli
index dddfd18280..89eb07517e 100644
--- a/typing/typedecl.mli
+++ b/typing/typedecl.mli
@@ -40,6 +40,8 @@ val approx_type_decl:
                                   (Ident.t * type_declaration) list
 val check_recmod_typedecl:
     Env.t -> Location.t -> Ident.t list -> Path.t -> type_declaration -> unit
+val check_coherence:
+    Env.t -> Location.t -> Ident.t -> type_declaration -> unit
 
 (* for fixed types *)
 val is_fixed_type : Parsetree.type_declaration -> bool
@@ -69,7 +71,7 @@ type error =
   | Unbound_type_var of type_expr * type_declaration
   | Unbound_exception of Longident.t
   | Not_an_exception of Longident.t
-  | Bad_variance of int * (bool*bool) * (bool*bool)
+  | Bad_variance of int * (bool*bool*bool) * (bool*bool*bool)
   | Unavailable_type_constructor of Path.t
   | Bad_fixed_type of string
   | Unbound_type_var_exc of type_expr * type_expr
diff --git a/typing/typedtree.ml b/typing/typedtree.ml
index dc5d474267..90cd6198bb 100644
--- a/typing/typedtree.ml
+++ b/typing/typedtree.ml
@@ -66,7 +66,7 @@ and expression =
 and exp_extra =
   | Texp_constraint of core_type
   | Texp_coerce of core_type option * core_type
-  | Texp_open of Path.t * Longident.t loc * Env.t
+  | Texp_open of override_flag * Path.t * Longident.t loc * Env.t
   | Texp_poly of core_type option
   | Texp_newtype of string
 
@@ -215,7 +215,7 @@ and structure_item_desc =
   | Tstr_module of module_binding
   | Tstr_recmodule of module_binding list
   | Tstr_modtype of module_type_declaration
-  | Tstr_open of Path.t * Longident.t loc * attribute list
+  | Tstr_open of override_flag * Path.t * Longident.t loc * attribute list
   | Tstr_class of (class_declaration * string list * virtual_flag) list
   | Tstr_class_type of (Ident.t * string loc * class_type_declaration) list
   | Tstr_include of module_expr * Ident.t list * attribute list
@@ -275,7 +275,7 @@ and signature_item_desc =
   | Tsig_module of module_declaration
   | Tsig_recmodule of module_declaration list
   | Tsig_modtype of module_type_declaration
-  | Tsig_open of Path.t * Longident.t loc * attribute list
+  | Tsig_open of override_flag * Path.t * Longident.t loc * attribute list
   | Tsig_include of module_type * Types.signature * attribute list
   | Tsig_class of class_description list
   | Tsig_class_type of class_type_declaration list
diff --git a/typing/typedtree.mli b/typing/typedtree.mli
index ac075e6bbd..e55561d08c 100644
--- a/typing/typedtree.mli
+++ b/typing/typedtree.mli
@@ -65,7 +65,7 @@ and expression =
 and exp_extra =
   | Texp_constraint of core_type
   | Texp_coerce of core_type option * core_type
-  | Texp_open of Path.t * Longident.t loc * Env.t
+  | Texp_open of override_flag * Path.t * Longident.t loc * Env.t
   | Texp_poly of core_type option
   | Texp_newtype of string
 
@@ -214,7 +214,7 @@ and structure_item_desc =
   | Tstr_module of module_binding
   | Tstr_recmodule of module_binding list
   | Tstr_modtype of module_type_declaration
-  | Tstr_open of Path.t * Longident.t loc * attributes
+  | Tstr_open of override_flag * Path.t * Longident.t loc * attributes
   | Tstr_class of (class_declaration * string list * virtual_flag) list
   | Tstr_class_type of (Ident.t * string loc * class_type_declaration) list
   | Tstr_include of module_expr * Ident.t list * attributes
@@ -274,7 +274,7 @@ and signature_item_desc =
   | Tsig_module of module_declaration
   | Tsig_recmodule of module_declaration list
   | Tsig_modtype of module_type_declaration
-  | Tsig_open of Path.t * Longident.t loc * attributes
+  | Tsig_open of override_flag * Path.t * Longident.t loc * attributes
   | Tsig_include of module_type * Types.signature * attributes
   | Tsig_class of class_description list
   | Tsig_class_type of class_type_declaration list
diff --git a/typing/typedtreeIter.ml b/typing/typedtreeIter.ml
index 4b28c7649b..edb5587986 100644
--- a/typing/typedtreeIter.ml
+++ b/typing/typedtreeIter.ml
@@ -228,7 +228,7 @@ module MakeIterator(Iter : IteratorArgument) : sig
             iter_core_type ct
         | Texp_coerce (cty1, cty2) ->
             option iter_core_type cty1; iter_core_type cty2
-        | Texp_open (path, _, _) -> ()
+        | Texp_open (_, path, _, _) -> ()
         | Texp_poly cto -> option iter_core_type cto
         | Texp_newtype s -> ())
         exp.exp_extra;
diff --git a/typing/typedtreeMap.ml b/typing/typedtreeMap.ml
index ed3b41fd1d..a59b66c9a7 100644
--- a/typing/typedtreeMap.ml
+++ b/typing/typedtreeMap.ml
@@ -123,7 +123,7 @@ module MakeMap(Map : MapArgument) = struct
           Tstr_recmodule list
         | Tstr_modtype mtd ->
           Tstr_modtype (map_module_type_declaration mtd)
-        | Tstr_open (path, lid, attrs) -> Tstr_open (path, lid, attrs)
+        | Tstr_open (ovf, path, lid, attrs) -> Tstr_open (ovf, path, lid, attrs)
         | Tstr_class list ->
           let list =
             List.map (fun (ci, string_list, virtual_flag) ->
@@ -394,7 +394,7 @@ module MakeMap(Map : MapArgument) = struct
               )
         | Tsig_modtype mtd ->
           Tsig_modtype (map_module_type_declaration mtd)
-        | Tsig_open (path, lid, _attrs) -> item.sig_desc
+        | Tsig_open _ -> item.sig_desc
         | Tsig_include (mty, lid, attrs) -> Tsig_include (map_module_type mty, lid, attrs)
         | Tsig_class list -> Tsig_class (List.map map_class_description list)
         | Tsig_class_type list ->
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 6aaebc8d87..c281fdc77a 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -66,10 +66,10 @@ let extract_sig_open env loc mty =
 
 (* Compute the environment after opening a module *)
 
-let type_open ?toplevel env loc lid =
+let type_open ?toplevel ovf env loc lid =
   let (path, mty) = Typetexp.find_module env loc lid.txt in
   let sg = extract_sig_open env loc mty in
-  path, Env.open_signature ~loc ?toplevel path sg env
+  path, Env.open_signature ~loc ?toplevel ovf path sg env
 
 (* Record a module type *)
 let rm node =
@@ -89,12 +89,13 @@ let rec add_rec_types env = function
       add_rec_types (Env.add_type id decl env) rem
   | _ -> env
 
-let check_type_decl env id row_id newdecl decl rs rem =
+let check_type_decl env loc id row_id newdecl decl rs rem =
   let env = Env.add_type id newdecl env in
   let env =
     match row_id with None -> env | Some id -> Env.add_type id newdecl env in
   let env = if rs = Trec_not then env else add_rec_types env rem in
-  Includemod.type_declarations env id newdecl decl
+  Includemod.type_declarations env id newdecl decl;
+  Typedecl.check_coherence env loc id newdecl
 
 let rec make_params n = function
     [] -> []
@@ -114,6 +115,10 @@ let sig_item desc typ env loc = {
   Typedtree.sig_desc = desc; sig_loc = loc; sig_env = env
 }
 
+let make p n i =
+  let open Variance in
+  set May_pos p (set May_neg n (set May_weak n (set Inj i null)))
+
 let merge_constraint initial_env loc sg constr =
   let lid =
     match constr with
@@ -138,21 +143,24 @@ let merge_constraint initial_env loc sg constr =
             type_manifest = None;
             type_variance =
               List.map
-              (fun (_, v) ->
-                match v with
-                | Covariant -> true, false, false
-                | Contravariant -> false, true, true
-                | Invariant -> true, true, true
-              )
-              sdecl.ptype_params;
-            type_loc = Location.none;
+                (fun (_, v) ->
+                   let (c, n) =  
+                     match v with
+                     | Covariant -> true, false
+                     | Contravariant -> false, true
+                     | Invariant -> false, false
+                   in
+                   make (not n) (not c) false
+                )
+                sdecl.ptype_params;
+            type_loc = sdecl.ptype_loc;
             type_newtype_level = None }
         and id_row = Ident.create (s^"#row") in
         let initial_env = Env.add_type id_row decl_row initial_env in
         let tdecl = Typedecl.transl_with_constraint
                         initial_env id (Some(Pident id_row)) decl sdecl in
         let newdecl = tdecl.typ_type in
-        check_type_decl env id row_id newdecl decl rs rem;
+        check_type_decl env sdecl.ptype_loc id row_id newdecl decl rs rem;
         let decl_row = {decl_row with type_params = newdecl.type_params} in
         let rs' = if rs = Trec_first then Trec_not else rs in
         (Pident id, lid, Twith_type tdecl),
@@ -162,7 +170,7 @@ let merge_constraint initial_env loc sg constr =
         let tdecl =
           Typedecl.transl_with_constraint initial_env id None decl sdecl in
         let newdecl = tdecl.typ_type in
-        check_type_decl env id row_id newdecl decl rs rem;
+        check_type_decl env sdecl.ptype_loc id row_id newdecl decl rs rem;
         (Pident id, lid, Twith_type tdecl), Sig_type(id, newdecl, rs) :: rem
     | (Sig_type(id, decl, rs) :: rem, [s], (Pwith_type _ | Pwith_typesubst _))
       when Ident.name id = s ^ "#row" ->
@@ -173,7 +181,7 @@ let merge_constraint initial_env loc sg constr =
         let tdecl =
           Typedecl.transl_with_constraint initial_env id None decl sdecl in
         let newdecl = tdecl.typ_type in
-        check_type_decl env id row_id newdecl decl rs rem;
+        check_type_decl env sdecl.ptype_loc id row_id newdecl decl rs rem;
         real_id := Some id;
         (Pident id, lid, Twith_typesubst tdecl),
         make_next_first rs rem
@@ -324,8 +332,8 @@ and approx_sig env ssg =
           let info = approx_modtype_info env d.pmtd_type in
           let (id, newenv) = Env.enter_modtype d.pmtd_name.txt info env in
           Sig_modtype(id, info) :: approx_sig newenv srem
-      | Psig_open (lid, _attrs) ->
-          let (path, mty) = type_open env item.psig_loc lid in
+      | Psig_open (ovf, lid, _attrs) ->
+          let (path, mty) = type_open ovf env item.psig_loc lid in
           approx_sig mty srem
       | Psig_include (smty, _attrs) ->
           let mty = approx_modtype env smty in
@@ -370,7 +378,8 @@ let check_recmod_typedecls env sdecls decls =
 
 (* Auxiliaries for checking uniqueness of names in signatures and structures *)
 
-module StringSet = Set.Make(struct type t = string let compare = compare end)
+module StringSet =
+  Set.Make(struct type t = string let compare (x:t) y = compare x y end)
 
 let check cl loc set_ref name =
   if StringSet.mem name !set_ref
@@ -386,17 +395,25 @@ let check_sig_item type_names module_names modtype_names loc = function
       check "module type" loc modtype_names (Ident.name id)
   | _ -> ()
 
-let rec remove_values ids = function
+let rec remove_duplicates val_ids exn_ids  = function
     [] -> []
   | Sig_value (id, _) :: rem
-    when List.exists (Ident.equal id) ids -> remove_values ids rem
-  | f :: rem -> f :: remove_values ids rem
+    when List.exists (Ident.equal id) val_ids -> remove_duplicates val_ids exn_ids rem
+  | Sig_exception(id, _) :: rem
+    when List.exists (Ident.equal id) exn_ids -> remove_duplicates val_ids exn_ids rem
+  | f :: rem -> f :: remove_duplicates val_ids exn_ids rem
 
 let rec get_values = function
     [] -> []
   | Sig_value (id, _) :: rem -> id :: get_values rem
   | f :: rem -> get_values rem
 
+let rec get_exceptions = function
+    [] -> []
+  | Sig_exception (id, _) :: rem -> id :: get_exceptions rem
+  | f :: rem -> get_exceptions rem
+
+
 (* Check and translate a module type expression *)
 
 let transl_modtype_longident loc env lid =
@@ -492,8 +509,10 @@ and transl_signature env sg =
         | Psig_exception sarg ->
             let (arg, decl, newenv) = Typedecl.transl_exception env sarg in
             let (trem, rem, final_env) = transl_sig newenv srem in
+            let id = arg.cd_id in
             mksig (Tsig_exception arg) env loc :: trem,
-            Sig_exception(arg.cd_id, decl) :: rem,
+            (if List.exists (Ident.equal id) (get_exceptions rem) then rem
+             else Sig_exception(id, decl) :: rem),
             final_env
         | Psig_module pmd ->
             check "module" item.psig_loc module_names pmd.pmd_name.txt;
@@ -524,10 +543,11 @@ and transl_signature env sg =
             mksig (Tsig_modtype mtd) env loc :: trem,
             sg :: rem,
             final_env
-        | Psig_open (lid, attrs) ->
-            let (path, newenv) = type_open env item.psig_loc lid in
+        | Psig_open (ovf, lid, attrs) ->
+            let (path, newenv) = type_open ovf env item.psig_loc lid in
             let (trem, rem, final_env) = transl_sig newenv srem in
-            mksig (Tsig_open (path,lid,attrs)) env loc :: trem, rem, final_env
+            mksig (Tsig_open (ovf, path,lid,attrs)) env loc :: trem,
+            rem, final_env
         | Psig_include (smty, attrs) ->
             let tmty = transl_modtype env smty in
             let mty = tmty.mty_type in
@@ -540,7 +560,8 @@ and transl_signature env sg =
             let newenv = Env.add_signature sg env in
             let (trem, rem, final_env) = transl_sig newenv srem in
             mksig (Tsig_include (tmty, sg, attrs)) env loc :: trem,
-            remove_values (get_values rem) sg @ rem, final_env
+            remove_duplicates (get_values rem) (get_exceptions rem) sg @ rem,
+            final_env
         | Psig_class cl ->
             List.iter
               (fun {pci_name = name} ->
@@ -632,11 +653,27 @@ and transl_recmodule_modtypes loc env sdecls =
     List.map2
       (fun pmd (id, id_loc, mty) -> (id, id_loc, transl_modtype env_c pmd.pmd_type))
       sdecls curr in
+  let ids = List.map (fun x -> Ident.create x.pmd_name.txt) sdecls in
+  let approx_env =
+    (*
+       cf #5965
+       We use a dummy module type in order to detect a reference to one
+       of the module being defined during the call to approx_modtype.
+       It will be detected in Env.lookup_module.
+    *)
+    List.fold_left
+      (fun env id ->
+         let dummy = Mty_ident (Path.Pident (Ident.create "#recmod#")) in
+         Env.add_module id dummy env
+      )
+      env ids
+  in
   let init =
-    List.map
-      (fun pmd->
-        (Ident.create pmd.pmd_name.txt, pmd.pmd_name, approx_modtype env pmd.pmd_type))
-      sdecls in
+    List.map2
+      (fun id pmd ->
+        (id, pmd.pmd_name, approx_modtype approx_env pmd.pmd_type))
+      ids sdecls
+  in
   let env0 = make_env init in
   let dcl1 = transition env0 init in
   let env1 = make_env2 dcl1 in
@@ -1118,9 +1155,9 @@ and type_structure ?(toplevel = false) funct_body anchor env sstr scope =
         mk (Tstr_modtype mtd) :: str_rem,
         sg :: sig_rem,
         final_env
-    | Pstr_open (lid, attrs) ->
-        let (path, newenv) = type_open ~toplevel env loc lid in
-        let item = mk (Tstr_open (path, lid, attrs)) in
+    | Pstr_open (ovf, lid, attrs) ->
+        let (path, newenv) = type_open ovf ~toplevel env loc lid in
+        let item = mk (Tstr_open (ovf, path, lid, attrs)) in
         let (str_rem, sig_rem, final_env) = type_struct newenv srem in
         (item :: str_rem, sig_rem, final_env)
     | Pstr_class cl ->
diff --git a/typing/types.ml b/typing/types.ml
index 8134fc1f82..f5d9527641 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -76,7 +76,8 @@ end
 
 (* Maps of methods and instance variables *)
 
-module OrderedString = struct type t = string let compare = compare end
+module OrderedString =
+  struct type t = string let compare (x:t) y = compare x y end
 module Meths = Map.Make(OrderedString)
 module Vars = Meths
 
@@ -137,6 +138,36 @@ and record_representation =
     Record_regular                      (* All fields are boxed / tagged *)
   | Record_float                        (* All fields are floats *)
 
+(* Variance *)
+
+module Variance = struct
+  type t = int
+  type f = May_pos | May_neg | May_weak | Inj | Pos | Neg | Inv
+  let single = function
+    | May_pos -> 1
+    | May_neg -> 2
+    | May_weak -> 4
+    | Inj -> 8
+    | Pos -> 16
+    | Neg -> 32
+    | Inv -> 64
+  let union v1 v2 = v1 lor v2
+  let inter v1 v2 = v1 land v2
+  let subset v1 v2 = (v1 land v2 = v1)
+  let set x b v =
+    if b then v lor single x else  v land (lnot (single x))
+  let mem x = subset (single x)
+  let null = 0
+  let may_inv = 7
+  let full = 127
+  let covariant = single May_pos lor single Pos lor single Inj
+  let swap f1 f2 v =
+    let v' = set f1 (mem f2 v) v in set f2 (mem f1 v) v'
+  let conjugate v = swap May_pos May_neg (swap Pos Neg v)
+  let get_upper v = (mem May_pos v, mem May_neg v)
+  let get_lower v = (mem Pos v, mem Neg v, mem Inv v, mem Inj v)
+end 
+
 (* Type definitions *)
 
 type type_declaration =
@@ -145,8 +176,7 @@ type type_declaration =
     type_kind: type_kind;
     type_private: private_flag;
     type_manifest: type_expr option;
-    type_variance: (bool * bool * bool) list;
-    (* covariant, contravariant, weakly contravariant *)
+    type_variance: Variance.t list;
     type_newtype_level: (int * int) option;
     type_loc: Location.t }
 
@@ -156,6 +186,11 @@ and type_kind =
       (Ident.t * mutable_flag * type_expr) list * record_representation
   | Type_variant of (Ident.t * type_expr list * type_expr option) list
 
+and type_transparence =
+    Type_public      (* unrestricted expansion *)
+  | Type_new         (* "new" type *)
+  | Type_private     (* private type *)
+
 type exception_declaration =
     { exn_args: type_expr list;
       exn_loc: Location.t }
@@ -181,13 +216,13 @@ type class_declaration =
     mutable cty_type: class_type;
     cty_path: Path.t;
     cty_new: type_expr option;
-    cty_variance: (bool * bool) list }
+    cty_variance: Variance.t list }
 
 type class_type_declaration =
   { clty_params: type_expr list;
     clty_type: class_type;
     clty_path: Path.t;
-    clty_variance: (bool * bool) list }
+    clty_variance: Variance.t list }
 
 (* Type expressions for the module language *)
 
diff --git a/typing/types.mli b/typing/types.mli
index df73388fa9..94559e2e1e 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -135,6 +135,25 @@ and record_representation =
     Record_regular                      (* All fields are boxed / tagged *)
   | Record_float                        (* All fields are floats *)
 
+(* Variance *)
+
+module Variance : sig
+  type t
+  type f = May_pos | May_neg | May_weak | Inj | Pos | Neg | Inv
+  val null : t                          (* no occurence *)
+  val full : t                          (* strictly invariant *)
+  val covariant : t                     (* strictly covariant *)
+  val may_inv : t                       (* maybe invariant *)
+  val union  : t -> t -> t
+  val inter  : t -> t -> t
+  val subset : t -> t -> bool
+  val set : f -> bool -> t -> t
+  val mem : f -> t -> bool
+  val conjugate : t -> t                (* exchange positive and negative *)
+  val get_upper : t -> bool * bool                  (* may_pos, may_neg   *)
+  val get_lower : t -> bool * bool * bool * bool    (* pos, neg, inv, inj *)
+end 
+
 (* Type definitions *)
 
 type type_declaration =
@@ -143,8 +162,8 @@ type type_declaration =
     type_kind: type_kind;
     type_private: private_flag;
     type_manifest: type_expr option;
-    type_variance: (bool * bool * bool) list;
-    (* covariant, contravariant, weakly contravariant *)
+    type_variance: Variance.t list;
+    (* covariant, contravariant, weakly contravariant, injective *)
     type_newtype_level: (int * int) option;
     (* definition level * expansion level *)
     type_loc: Location.t }
@@ -155,6 +174,11 @@ and type_kind =
       (Ident.t * mutable_flag * type_expr) list * record_representation
   | Type_variant of (Ident.t * type_expr list * type_expr option) list
 
+and type_transparence =
+    Type_public      (* unrestricted expansion *)
+  | Type_new         (* "new" type *)
+  | Type_private     (* private type *)
+
 type exception_declaration =
     { exn_args: type_expr list;
       exn_loc: Location.t }
@@ -179,13 +203,13 @@ type class_declaration =
     mutable cty_type: class_type;
     cty_path: Path.t;
     cty_new: type_expr option;
-    cty_variance: (bool * bool) list }
+    cty_variance: Variance.t list }
 
 type class_type_declaration =
   { clty_params: type_expr list;
     clty_type: class_type;
     clty_path: Path.t;
-    clty_variance: (bool * bool) list }
+    clty_variance: Variance.t list }
 
 (* Type expressions for the module language *)
 
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index 8749244745..7d6a9f864d 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -50,6 +50,7 @@ type error =
   | Unbound_modtype of Longident.t
   | Unbound_cltype of Longident.t
   | Ill_typed_functor_application of Longident.t
+  | Illegal_reference_to_recursive_module
   | Extension of string
 
 exception Error of Location.t * Env.t * error
@@ -69,6 +70,8 @@ let rec narrow_unbound_lid_error : 'a. _ -> _ -> _ -> _ -> 'a =
     with Not_found ->
       narrow_unbound_lid_error env loc mlid
         (fun lid -> Unbound_module lid)
+       | Env.Recmodule ->
+         raise (Error (loc, env, Illegal_reference_to_recursive_module))
   in
   begin match lid with
   | Longident.Lident _ -> ()
@@ -88,6 +91,8 @@ let find_component lookup make_error env loc lid =
     | _ -> lookup lid env
   with Not_found ->
     narrow_unbound_lid_error env loc lid make_error
+  | Env.Recmodule ->
+    raise (Error (loc, env, Illegal_reference_to_recursive_module))
 
 let find_type =
   find_component Env.lookup_type (fun lid -> Unbound_type_constructor lid)
@@ -299,7 +304,8 @@ let rec transl_type env policy styp =
                     check (Env.find_type path env)
                 | _ -> raise Not_found
           in check decl;
-          Location.prerr_warning styp.ptyp_loc Warnings.Deprecated;
+          Location.prerr_warning styp.ptyp_loc
+            (Warnings.Deprecated "old syntax for polymorphic variant type");
           (path, decl,true)
         with Not_found -> try
           let lid2 =
@@ -315,7 +321,7 @@ let rec transl_type env policy styp =
       in
       if List.length stl <> decl.type_arity then
         raise(Error(styp.ptyp_loc, env,
-		    Type_arity_mismatch(lid.txt, decl.type_arity,
+                    Type_arity_mismatch(lid.txt, decl.type_arity,
                                         List.length stl)));
       let args = List.map (transl_type env policy) stl in
       let params = instance_list decl.type_params in
@@ -814,5 +820,7 @@ let report_error env ppf = function
       spellcheck ppf Env.fold_cltypes env lid;
   | Ill_typed_functor_application lid ->
       fprintf ppf "Ill-typed functor application %a" longident lid
+  | Illegal_reference_to_recursive_module ->
+      fprintf ppf "Illegal recursive module reference"
   | Extension s ->
       fprintf ppf "Uninterpreted extension '%s'." s
diff --git a/typing/typetexp.mli b/typing/typetexp.mli
index c9fbda6f39..eb78d1ae1b 100644
--- a/typing/typetexp.mli
+++ b/typing/typetexp.mli
@@ -61,6 +61,7 @@ type error =
   | Unbound_modtype of Longident.t
   | Unbound_cltype of Longident.t
   | Ill_typed_functor_application of Longident.t
+  | Illegal_reference_to_recursive_module
   | Extension of string
 
 exception Error of Location.t * Env.t * error