diff options
| -rw-r--r-- | Changes | 3 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/pr5985.ml | 8 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/pr5985.ml.reference | 14 | ||||
| -rw-r--r-- | typing/typedecl.ml | 8 |
4 files changed, 31 insertions, 2 deletions
@@ -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 fdc66e823..6d0bbcee7 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 e9fa3461e..af6154dda 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 214a0b1c2..3e5591b8c 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 |