Fix PR#6275

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

4 files changed, 31 insertions, 2 deletions

diff --git a/Changes b/Changes
index 927e483ac2..7dbf2f50fc 100644
--- a/Changes
+++ b/Changes
@@ -77,7 +77,8 @@ Bug fixes:
 - PR#6241: Assumed inequality between paths involving functor arguments
 - PR#6243: Make "ocamlopt -g" more resistant to ill-formed locations
 - PR#6239: sometimes wrong stack alignment when raising exceptions
-  in -g mode with backtraces active
+           in -g mode with backtraces active
+- PR#6275: Soundness bug related to type constraints
 
 
 OCaml 4.01.0:
diff --git a/testsuite/tests/typing-gadts/pr5985.ml b/testsuite/tests/typing-gadts/pr5985.ml
index fdc66e8238..6d0bbcee7b 100644
--- a/testsuite/tests/typing-gadts/pr5985.ml
+++ b/testsuite/tests/typing-gadts/pr5985.ml
@@ -26,6 +26,14 @@ module F(T:sig type 'a t end) = struct
     object constraint 'a = 'b T.t val x' : 'b = x method x = x' end
 end;; (* fail *)
 
+(* Another (more direct) instance using polymorphic variants *)
+(* PR#6275 *)
+type 'x t = A of 'a constraint 'x = [< `X of 'a ] ;; (* fail *)
+let magic (x : int) : bool = 
+  let A x = A x in
+  x;; (* fail *)
+type 'a t = A : 'a -> [< `X of 'a ] t;; (* fail *)
+
 (* It is not OK to allow modules exported by other compilation units *)
 type (_,_) eq = Eq : ('a,'a) eq;;
 let eq = Obj.magic Eq;;
diff --git a/testsuite/tests/typing-gadts/pr5985.ml.reference b/testsuite/tests/typing-gadts/pr5985.ml.reference
index e9fa3461e4..af6154dda7 100644
--- a/testsuite/tests/typing-gadts/pr5985.ml.reference
+++ b/testsuite/tests/typing-gadts/pr5985.ml.reference
@@ -13,6 +13,20 @@ Error: Syntax error
       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.
+#       Characters 83-128:
+  type 'x t = A of 'a constraint 'x = [< `X of 'a ] ;; (* fail *)
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In this definition, a type variable cannot be deduced
+       from the type parameters.
+#     Characters 36-37:
+    let A x = A x in
+        ^
+Error: Unbound constructor A
+# Characters 4-37:
+  type 'a t = A : 'a -> [< `X of 'a ] t;; (* fail *)
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In this definition, a type variable cannot be deduced
+       from the type parameters.
 #     type (_, _) eq = Eq : ('a, 'a) eq
 # val eq : 'a = <poly>
 #   val eq : ('a Queue.t, 'b Queue.t) eq = Eq
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 214a0b1c2e..3e5591b8c8 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -573,7 +573,13 @@ let compute_variance env visited vari ty =
               Rpresent (Some ty) ->
                 compute_same ty
             | Reither (_, tyl, _, _) ->
-                List.iter compute_same tyl
+                let open Variance in
+                let upper =
+                  List.fold_left (fun s f -> set f true s)
+                    null [May_pos; May_neg; May_weak]
+                in
+                let v = inter vari upper in
+                List.iter (compute_variance_rec v) tyl
             | _ -> ())
           row.row_fields;
         compute_same row.row_more