Fix PR#5985 for constrained parameters too.

Required more variance information, so variance is now an abstract type.


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

18 files changed, 360 insertions, 209 deletions

diff --git a/boot/ocamlc b/boot/ocamlc
index b062a140ea..9423b5803a 100755
--- a/boot/ocamlc
+++ b/boot/ocamlc
diff --git a/boot/ocamldep b/boot/ocamldep
index 28ebb69df2..cd845916d3 100755
--- a/boot/ocamldep
+++ b/boot/ocamldep
diff --git a/boot/ocamllex b/boot/ocamllex
index 7ef0529d2d..42804220be 100755
--- a/boot/ocamllex
+++ b/boot/ocamllex
diff --git a/ocamldoc/odoc_ast.ml b/ocamldoc/odoc_ast.ml
index 4a0f3c4ac9..7d282f6d7c 100644
--- a/ocamldoc/odoc_ast.ml
+++ b/ocamldoc/odoc_ast.ml
@@ -1195,12 +1195,11 @@ module Analyser =
                       ty_info = com_opt ;
                       ty_parameters =
                       List.map2
-                      (fun p (co,cn,_,_) ->
-                         (Odoc_env.subst_type new_env p,
-                          co, cn)
-                      )
-                      tt_type_decl.Types.type_params
-                      tt_type_decl.Types.type_variance ;
+                       (fun p v ->
+                         let (co, cn) = Types.Variance.get_upper v in
+                         (Odoc_env.subst_type new_env p, co, cn))
+                       tt_type_decl.Types.type_params
+                       tt_type_decl.Types.type_variance ;
                       ty_kind = kind ;
                       ty_private = tt_type_decl.Types.type_private;
                       ty_manifest =
diff --git a/ocamldoc/odoc_sig.ml b/ocamldoc/odoc_sig.ml
index 47b1a465dd..24beb02889 100644
--- a/ocamldoc/odoc_sig.ml
+++ b/ocamldoc/odoc_sig.ml
@@ -638,10 +638,9 @@ module Analyser =
                       ty_name = Name.concat current_module_name name.txt ;
                       ty_info = assoc_com ;
                       ty_parameters =
-                        List.map2 (fun p (co,cn,_,_) ->
-                                     (Odoc_env.subst_type new_env p,
-                                      co, cn)
-                                  )
+                        List.map2 (fun p v ->
+                          let (co, cn) = Types.Variance.get_upper v in
+                          (Odoc_env.subst_type new_env p,co, cn))
                         sig_type_decl.Types.type_params
                         sig_type_decl.Types.type_variance;
                       ty_kind = type_kind;
diff --git a/testsuite/tests/typing-gadts/pr5985.ml b/testsuite/tests/typing-gadts/pr5985.ml
index fa28ce5ca7..427c14416d 100644
--- a/testsuite/tests/typing-gadts/pr5985.ml
+++ b/testsuite/tests/typing-gadts/pr5985.ml
@@ -3,8 +3,10 @@ module F (S : sig type 'a s end) = struct
   include S
   type _ t = T : 'a -> 'a s t
 end;; (* fail *)
+(*
 module M = F (struct type 'a s = int end) ;;
 let M.T x = M.T 3 in x = true;;
+*)
 
 (* Fix it using #-annotations *)
 module F (S : sig type #'a s end) = struct
@@ -33,7 +35,7 @@ type _ t = T : 'a -> 'a Queue.t t;; (* fail *)
 (*
 let castT (type a) (type b) (x : a t) (e: (a, b) eq) : b t =
   let Eq = e in (x : b t);;
-let T (x : bool) = castT (T 3) eq;;
+let T (x : bool) = castT (T 3) eq;; (* we found a contradiction *)
 *)
 
 (* The following signature should not be accepted *)
@@ -46,3 +48,28 @@ module rec M : (S with type 'a s = unit) = M;;
 (* For the above reason, we cannot allow the abstract declaration
    of s and the definition of t to be in the same module, as
    we could create the signature using [module type of ...] *)
+
+
+(* Another problem with variance *)
+module M = struct type 'a t = 'a -> unit end;;
+module F(X:sig type #'a t end) =
+  struct type +'a s = S of 'b constraint 'a = 'b X.t end;; (* fail *)
+(*
+module N = F(M);;
+let o = N.S (object end);;
+let N.S o' = (o :> <m : int> M.t N.s);; (* unsound! *)
+*)
+
+(* And yet another *)
+type 'a q = Q;;
+type +'a t = 'b constraint 'a = 'b q;;
+(* shoud fail: we do not know for sure the variance of Queue.t *)
+
+type +'a t = T of 'a;;
+type +'a s = 'b constraint 'a = 'b t;; (* ok *)
+type -'a s = 'b constraint 'a = 'b t;; (* fail *)
+type +'a u = 'a t;;
+type 'a t = T of ('a -> 'a);;
+type -'a s = 'b constraint 'a = 'b t;; (* ok *)
+type +'a s = 'b constraint 'a = 'b q t;; (* ok *)
+type +'a s = 'b constraint 'a = 'b t q;; (* fail *)
diff --git a/testsuite/tests/typing-gadts/pr5985.ml.reference b/testsuite/tests/typing-gadts/pr5985.ml.reference
index 9ce60b1771..7cfa1e2a25 100644
--- a/testsuite/tests/typing-gadts/pr5985.ml.reference
+++ b/testsuite/tests/typing-gadts/pr5985.ml.reference
@@ -3,17 +3,8 @@
     type _ t = T : 'a -> 'a s t
         ^^^^^^^^^^^^^^^^^^^^^^^
 Error: In this definition, a type variable cannot be deduced
-       from the type parameters. It was expected to be unrestricted,
-       but it is injective invariant.
-# Characters 11-12:
-  module M = F (struct type 'a s = int end) ;;
-             ^
-Error: Unbound module F
-# Characters 4-7:
-  let M.T x = M.T 3 in x = true;;
-      ^^^
-Error: Unbound module M
-#           Characters 48-51:
+       from the type parameters.
+# * * *             Characters 131-134:
   module F (S : sig type #'a s end) = struct
                 ^^^
 Syntax error: 'end' expected, the highlighted 'sig' might be unmatched
@@ -21,8 +12,7 @@ Syntax error: 'end' expected, the highlighted 'sig' might be unmatched
   ........['a] c x =
       object constraint 'a = 'b T.t val x' : 'b = x method x = x' end
 Error: In this definition, a type variable cannot be deduced
-       from the type parameters. It was expected to be unrestricted,
-       but it is injective invariant.
+       from the type parameters.
 #     type (_, _) eq = Eq : ('a, 'a) eq
 # val eq : 'a = <poly>
 #   val eq : ('a Queue.t, 'b Queue.t) eq = Eq
@@ -30,16 +20,44 @@ Error: In this definition, a type variable cannot be deduced
   type _ t = T : 'a -> 'a Queue.t t;; (* fail *)
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: In this definition, a type variable cannot be deduced
-       from the type parameters. It was expected to be unrestricted,
-       but it is injective invariant.
-# * * * *             Characters 223-246:
+       from the type parameters.
+# * * * *             Characters 254-277:
     type _ t = T : 'a -> 'a s t
         ^^^^^^^^^^^^^^^^^^^^^^^
 Error: In this definition, a type variable cannot be deduced
-       from the type parameters. It was expected to be unrestricted,
-       but it is injective invariant.
+       from the type parameters.
 #   Characters 59-60:
   module rec M : (S with type 'a s = unit) = M;;
                   ^
 Error: Unbound module type S
-# * *   
+# * *         module M : sig type 'a t = 'a -> unit end
+#   Characters 11-14:
+  module F(X:sig type #'a t end) =
+             ^^^
+Syntax error: 'end' expected, the highlighted 'sig' might be unmatched
+# * * * *       type 'a q = Q
+# Characters 5-36:
+  type +'a t = 'b constraint 'a = 'b q;;
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In this definition, a type variable has a variance that
+       cannot be deduced from the type parameters.
+       It was expected to be unrestricted, but it is covariant.
+#     type 'a t = T of 'a
+# type +'a s = 'b constraint 'a = 'b t
+# Characters 5-36:
+  type -'a s = 'b constraint 'a = 'b t;; (* fail *)
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In this definition, a type variable has a variance that
+       is not reflected by its occurrence in type parameters.
+       It was expected to be contravariant, but it is covariant.
+# type 'a u = 'a t
+# type 'a t = T of ('a -> 'a)
+# type -'a s = 'b constraint 'a = 'b t
+# type +'a s = 'b constraint 'a = 'b q t
+# Characters 5-38:
+  type +'a s = 'b constraint 'a = 'b t q;; (* fail *)
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In this definition, a type variable has a variance that
+       cannot be deduced from the type parameters.
+       It was expected to be unrestricted, but it is covariant.
+# 
diff --git a/testsuite/tests/typing-private/private.ml b/testsuite/tests/typing-private/private.ml
index 6f19b89d1c..5969e18b96 100644
--- a/testsuite/tests/typing-private/private.ml
+++ b/testsuite/tests/typing-private/private.ml
@@ -87,3 +87,9 @@ module M3' : sig
   type t = M'.t
   val mk : int -> t
 end = M';;
+
+module M : sig type 'a t = private T of 'a end =
+  struct type 'a t = T of 'a end;;
+
+module M1 : sig type 'a t = 'a M.t = private T of 'a end =
+  struct type 'a t = 'a M.t = private T of 'a end;;
diff --git a/testsuite/tests/typing-private/private.ml.reference b/testsuite/tests/typing-private/private.ml.reference
index 8a7b3db469..a231a07ab6 100644
--- a/testsuite/tests/typing-private/private.ml.reference
+++ b/testsuite/tests/typing-private/private.ml.reference
@@ -94,4 +94,6 @@ Error: This variant or record definition does not match that of type M.t
 #                   module M' :
   sig type t_priv = private T of int type t = t_priv val mk : int -> t end
 #         module M3' : sig type t = M'.t val mk : int -> t end
+#     module M : sig type 'a t = private T of 'a end
+#     module M1 : sig type 'a t = 'a M.t = private T of 'a end
 # 
diff --git a/typing/ctype.ml b/typing/ctype.ml
index a31c968c38..aadba8809c 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,false)) 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) ->
@@ -1690,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
@@ -1736,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
@@ -2033,7 +2038,7 @@ and mcomp_type_decl type_pairs subst env p1 p2 tl1 tl2 =
       if non_aliasable p1 decl then Format.eprintf "non_aliasable@."
       else Format.eprintf "aliasable@."; *)
       let inj =
-        try List.map for4 (Env.find_type p1 env).type_variance
+        try List.map Variance.(mem Inj) (Env.find_type p1 env).type_variance
         with Not_found -> List.map (fun _ -> false) tl1
       in
       List.iter2
@@ -2266,7 +2271,8 @@ and unify3 env t1 t1' t2 t2' =
             unify_list env tl1 tl2
           else
             let inj =
-              try List.map for4 (Env.find_type p1 !env).type_variance
+              try List.map Variance.(mem Inj)
+                    (Env.find_type p1 !env).type_variance
               with Not_found -> List.map (fun _ -> false) tl1
             in
             List.iter2
@@ -3587,7 +3593,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
@@ -3740,7 +3747,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]),
diff --git a/typing/includecore.ml b/typing/includecore.ml
index 11c9a4b946..23d6537f42 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -244,14 +244,20 @@ let type_declarations ?(equality = false) env name decl1 id decl2 =
         else [Constraint]
   in
   if err <> [] then err else
-  if decl2.type_private = Private
-  || decl2.type_kind = Type_abstract && decl2.type_manifest = None then
-    if List.for_all2
-        (fun (co1,cn1,ct1,i1) (co2,cn2,ct2,i2) ->
-          (not co1 || co2) && (not cn1 || cn2) && (not i2 || i1))
-        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/predef.ml b/typing/predef.ml
index c3b1583d86..e4e96d2de1 100644
--- a/typing/predef.ml
+++ b/typing/predef.ml
@@ -123,7 +123,7 @@ let build_initial_env add_type add_exception empty_env =
     {decl_abstr with
      type_params = [tvar];
      type_arity = 1;
-     type_variance = [true, true, true, true]}
+     type_variance = [Variance.full]}
   and decl_list =
     let tvar = newgenvar() in
     {decl_abstr with
@@ -132,26 +132,26 @@ let build_initial_env add_type add_exception empty_env =
      type_kind =
      Type_variant([ident_nil, [], None; ident_cons, [tvar; type_list tvar],
                    None]);
-     type_variance = [true, false, false, true]}
+     type_variance = [Variance.covariant]}
   and decl_format6 =
     let params = List.map newgenvar [();();();();();()] in
     {decl_abstr with
      type_params = params;
      type_arity = 6;
-     type_variance = List.map (fun _ -> true, true, true, true) params}
+     type_variance = List.map (fun _ -> Variance.full) params}
   and decl_option =
     let tvar = newgenvar() in
     {decl_abstr with
      type_params = [tvar];
      type_arity = 1;
      type_kind = Type_variant([ident_none, [], None; ident_some, [tvar], None]);
-     type_variance = [true, false, false, true]}
+     type_variance = [Variance.covariant]}
   and decl_lazy_t =
     let tvar = newgenvar() in
     {decl_abstr with
      type_params = [tvar];
      type_arity = 1;
-     type_variance = [true, false, false, true]}
+     type_variance = [Variance.covariant]}
   in
 
   let add_exception id l =
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index c04f5a6f9a..88061f0ef8 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -793,8 +793,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,
@@ -989,6 +990,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
 
@@ -1004,7 +1008,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)
 
@@ -1037,7 +1041,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)
 
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index aa160ecd0e..8e75c1d551 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -1114,7 +1114,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, true) !params;
+       type_variance = Misc.replicate_list Variance.full arity;
        type_newtype_level = None;
        type_loc = loc;
       }
@@ -1268,7 +1268,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;
@@ -1329,7 +1329,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, true) obj_params;
+     type_variance = List.map (fun _ -> Variance.full) obj_params;
      type_newtype_level = None;
      type_loc = cl.pci_loc}
   in
@@ -1344,7 +1344,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, true) cl_params;
+     type_variance = List.map (fun _ -> Variance.full) cl_params;
      type_newtype_level = None;
      type_loc = cl.pci_loc}
   in
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 883719d0a5..21d667b2e9 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -57,8 +57,7 @@ let enter_type env (name, 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, true) sdecl.ptype_params;
+      type_variance = List.map (fun _ -> Variance.full) sdecl.ptype_params;
       type_newtype_level = None;
       type_loc = sdecl.ptype_loc;
     }
@@ -164,7 +163,8 @@ let transl_declaration env (name, 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, loc)
+              (name, lid, List.map (transl_simple_type env true) args,
+               None, loc)
             | Some sty ->
               (* if it's a generalized constructor we must first narrow and
                  then widen so as to not introduce any new constraints *)
@@ -228,7 +228,7 @@ let transl_declaration env (name, sdecl) id =
         type_kind = kind;
         type_private = sdecl.ptype_private;
         type_manifest = man;
-        type_variance = List.map (fun _ -> true, true, true, true) params;
+        type_variance = List.map (fun _ -> Variance.full) params;
         type_newtype_level = None;
         type_loc = sdecl.ptype_loc;
       } in
@@ -482,87 +482,93 @@ let check_abbrev_recursion env id_loc_list (id, _, tdecl) =
 
 (* Compute variance *)
 
-let compute_variance env tvl nega posi cntr ijct ty =
-  let pvisited = ref TypeSet.empty
-  and nvisited = ref TypeSet.empty
-  and cvisited = ref TypeSet.empty
-  and ivisited = ref TypeSet.empty in
-  let rec compute_variance_rec posi nega cntr ijct ty =
+let compute_variance env tvl vari ty =
+  let open Btype in
+  let visited = ref TypeMap.empty in
+  let rec compute_variance_rec vari ty =
     let ty = Ctype.repr ty in
-    let pos0 = TypeSet.mem ty !pvisited
-    and neg0 = TypeSet.mem ty !nvisited
-    and cnt0 = TypeSet.mem ty !cvisited
-    and ijc0 = TypeSet.mem ty !ivisited in
-    if posi && not pos0 || nega && not neg0
-    || cntr && not cnt0 || ijct && not ijc0
-    then 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;
-      if ijct then ivisited := TypeSet.add ty !ivisited;
-      let posi = posi || pos0 and nega = nega || neg0
-      and cntr = cntr || cnt0 and ijct = ijct || ijc0 in
-      let compute_same = compute_variance_rec posi nega cntr ijct in
-      match ty.desc with
-        Tarrow (_, ty1, ty2, _) ->
-          compute_variance_rec nega posi true ijct 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,ij) ->
-                  let strict = posi && nega && ij in
-                  compute_variance_rec
-                    (posi && co || nega && cn || strict)
-                    (posi && cn || nega && co || strict)
-                    (cntr && (co || cn) || (posi || nega) && ct || strict)
-                    (ijct && ij)
-                    ty)
-                tl decl.type_variance
-            with Not_found ->
-              let occ = posi || nega in
-              List.iter (compute_variance_rec occ occ occ false) 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 ijct) tyl
-    end
+    let vari' =
+      try TypeMap.find ty !visited with Not_found -> Variance.null 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 ijct ty;
+  compute_variance_rec vari ty;
   List.iter
-    (fun (ty, covar, convar, ctvar, ijr) ->
-      if TypeSet.mem ty !pvisited then covar := true;
-      if TypeSet.mem ty !nvisited then convar := true;
-      if TypeSet.mem ty !cvisited then ctvar := true;
-      if TypeSet.mem ty !ivisited then ijr := true)
+    (fun (ty, var) ->
+      try var := Variance.union !var (TypeMap.find ty !visited)
+      with Not_found -> ())
     tvl
 
-let make_variance ty = (ty, ref false, 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 ->
@@ -576,75 +582,83 @@ 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 compute_variance_type env check (required, loc) decl tyl =
   (* Requirements *)
   let required =
     List.map (fun (c,n,i) -> if c || n then (c,n,i) else (true,true,i))
       required
   in
-  (* Shortcut for private concrete types *)
-  if not check && decl.type_kind <> Type_abstract
-  && decl.type_private = Private then
-    List.map (fun (c,n,i) -> (c,n,n,true)) required
   (* Prepare *)
-  else let params = List.map Btype.repr decl.type_params in
+  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 tvl3 = List.map make_variance fvl in
   let tvl = tvl0 @ tvl1 in
   (* Compute occurences in body *)
-  List.iter (fun (cn,ty) -> compute_variance env tvl true cn cn true ty)
+  let open Variance in
+  List.iter
+    (fun (cn,ty) ->
+      compute_variance env tvl (if cn then full else covariant) ty)
     tyl;
-  (* Explicit variance cases; concrete types are injective *)
-  List.iter2
-    (fun (p,n,i) ty ->
-      if decl.type_private = Private || not (Btype.is_Tvar ty) then
-        compute_variance env tvl p n n false ty;
-      compute_variance env tvl2 p n n i ty;
-      if decl.type_kind <> Type_abstract
-      || i && decl.type_private = Private then
-        compute_variance env tvl false false false true ty)
-    required params;
   if check then begin
     (* Check variance of parameters *)
     let pos = ref 0 in
     List.iter2
-      (fun (ty, co, cn, ct, ij) (c, n, i) ->
+      (fun (ty, var) (c, n, i) ->
         incr pos;
-        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)))))
+        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)))))
       tvl0 required;
-    (* Check that variables occuring in the body are injective *)
-    List.iter (compute_variance env tvl3 false false false true) params;
+    (* Check propagation from constrained parameters *)
     List.iter2
-      (fun (ty, c1, n1, _, i1) (_, c3, n3, _, i3) ->
-        if (!c1 || !n1) && not !i3 then
-          raise (Error(loc, Bad_variance (-2, (!c1,!n1,!i1), (!c3,!n3,!i3)))))
-      tvl1 tvl3;
-    (* Check propagation to constrained parameters *)
+      (fun (p,n,i) ty ->
+        let v =
+          if Btype.is_Tvar ty then full else
+          if p then if n then full else covariant else conjugate covariant in
+        compute_variance env tvl2 v ty)
+      required params;
     List.iter2
-      (fun (ty, c1, n1, t1, i1) (_, c2, n2, t2, i2) ->
-        if !c1 && not !c2 || !n1 && not !n2 || not !i1 && !i2 then
-          let code = if !c2 || !n2 then -1 else -3 in
-          raise (Error(loc, Bad_variance (code, (!c1,!n1,!i1), (!c2,!n2,!i2)))))
+      (fun (ty, v1) (_, v2) ->
+        let (c1,n1) = get_upper !v1 and (c2,n2,_,i2) = get_lower !v2 in
+        if c1 && not c2 || n1 && not n2 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)))))
       tvl1 tvl2;
   end;
-  List.map
-    (fun (ty, co, cn, ct, ij) ->
-      let ct = if decl.type_kind = Type_abstract then ct else cn in
-      (!co, !cn, !ct, !ij))
-    tvl0
+  List.map2
+    (fun (ty, {contents=v}) (p, n, i) ->
+      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)
+    tvl0 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
@@ -658,6 +672,7 @@ 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 fvl = List.map Ctype.free_variables tyl in
           let _ =
             List.fold_left2
@@ -679,27 +694,36 @@ let compute_variance_decl env check decl (required, loc as rloc) =
   if decl.type_kind = Type_abstract && decl.type_manifest = None then
     List.map
       (fun (c, n, i) ->
-        (* let i = i || decl.type_transparence = Type_new in *)
-        if c || n then (c, n, n, i) else (true, true, true, 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
@@ -721,13 +745,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,i1) (c2,n2,t2,i2) -> c1||c2, n1||n2, t1||t2, i1&&i2))
-      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))
@@ -736,7 +764,7 @@ let rec compute_variance_fixpoint env decls required variances =
   end
 
 let init_variance (id, decl) =
-  List.map (fun _ -> (false, false, false, true)) decl.type_params
+  List.map (fun _ -> Variance.null) decl.type_params
 
 let add_injectivity = List.map (fun (cn,cv) -> (cn,cv,false))
 
@@ -753,8 +781,8 @@ let compute_variance_decls env cldecls =
   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,i) -> (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
@@ -893,8 +921,6 @@ let transl_type_decl env name_sdecl_list =
          Some ty -> raise(Error(sdecl.ptype_loc, Unbound_type_var(ty,decl)))
        | None   -> ())
     name_sdecl_list tdecls;
-  (* Check re-exportation *)
-  List.iter2 (check_abbrev newenv) name_sdecl_list decls;
   (* Check that constraints are enforced *)
   List.iter2 (check_constraints newenv) name_sdecl_list decls;
   (* Name recursion *)
@@ -912,6 +938,9 @@ let transl_type_decl env name_sdecl_list =
   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) name_sdecl_list final_decls;
+  (* Keep original declaration *)
   let final_decls = List.map2 (fun (id, name_loc, tdecl) (id2, decl) ->
         (id, name_loc, { tdecl with typ_type = decl })
     ) tdecls final_decls in
@@ -1053,7 +1082,7 @@ let abstract_type_decl arity =
       type_kind = Type_abstract;
       type_private = Public;
       type_manifest = None;
-      type_variance = replicate_list (true, true, true, true) arity;
+      type_variance = replicate_list Variance.full arity;
       type_newtype_level = None;
       type_loc = Location.none;
      } in
@@ -1209,7 +1238,7 @@ let report_error ppf = function
           "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@ It"
+        fprintf ppf "@[%s@ %s@]"
           "In this definition, a type variable cannot be deduced"
           "from the type parameters."
       else if n = -3 then
@@ -1221,8 +1250,9 @@ let report_error ppf = function
           "In this definition, expected parameter"
           "variances are not satisfied."
           n (suffix n);
-      fprintf ppf " was expected to be %s,@ but it is %s.@]"
-        (variance v2) (variance v1)
+      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/typemod.ml b/typing/typemod.ml
index 21e6830f6d..abf738cf73 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -114,6 +114,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 lid constr =
   let real_id = ref None in
   let rec merge env sg namelist row_id =
@@ -131,7 +135,7 @@ let merge_constraint initial_env loc  sg lid constr =
             type_private = Private;
             type_manifest = None;
             type_variance =
-              List.map (fun (c,n) -> (not n, not c, not c, false))
+              List.map (fun (c,n) -> make (not n) (not c) false)
               sdecl.ptype_variance;
             type_loc = Location.none;
             type_newtype_level = None }
diff --git a/typing/types.ml b/typing/types.ml
index a24f4ebb0a..4263116454 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -138,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 =
@@ -146,8 +176,7 @@ type type_declaration =
     type_kind: type_kind;
     type_private: private_flag;
     type_manifest: type_expr option;
-    type_variance: (bool * bool * bool * bool) list;
-    (* covariant, contravariant, weakly contravariant, injective *)
+    type_variance: Variance.t list;
     type_newtype_level: (int * int) option;
     type_loc: Location.t }
 
@@ -187,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 0231778a7c..2020e25827 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,7 +162,7 @@ type type_declaration =
     type_kind: type_kind;
     type_private: private_flag;
     type_manifest: type_expr option;
-    type_variance: (bool * bool * bool * bool) list;
+    type_variance: Variance.t list;
     (* covariant, contravariant, weakly contravariant, injective *)
     type_newtype_level: (int * int) option;
     (* definition level * expansion level *)
@@ -184,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 *)