diff options
| -rw-r--r-- | Changes | 3 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/pr5689.ml.principal.reference | 15 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/pr5689.ml.reference | 15 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/pr5989.ml | 35 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/pr5989.ml.reference | 24 | ||||
| -rw-r--r-- | typing/ctype.ml | 12 |
6 files changed, 86 insertions, 18 deletions
@@ -123,7 +123,8 @@ Bug fixes: - PR#5907: Undetected cycle during typecheck causes exceptions - PR#5911: Signature substitutions fail in submodules - PR#5948: GADT with polymorphic variants bug -- PR#5982: Incompatibility check assumes abstracted types are injective +- PR#5981: Incompatibility check assumes abstracted types are injective +- PR#5989: Assumed inequalities involving private rows OCaml 4.00.1: ------------- diff --git a/testsuite/tests/typing-gadts/pr5689.ml.principal.reference b/testsuite/tests/typing-gadts/pr5689.ml.principal.reference index f1e142aad..fabdb17cd 100644 --- a/testsuite/tests/typing-gadts/pr5689.ml.principal.reference +++ b/testsuite/tests/typing-gadts/pr5689.ml.principal.reference @@ -16,13 +16,12 @@ type _ inline_t = # type _ linkp = Nonlink : [ `Nonlink ] linkp | Maylink : inkind linkp # val inlineseq_from_astseq : ast_t list -> inkind inline_t list = <fun> # type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2 -# Characters 272-279: - | (Kind Maylink, Ast_Link lnk) -> Link lnk - ^^^^^^^ -Error: This pattern matches values of type inkind linkp - but a pattern was expected which matches values of type - ([< inkind ] as 'a) linkp - Type inkind = [ `Link | `Nonlink ] is not compatible with type - 'a = [< `Link | `Nonlink ] +# Characters 184-192: + | (Kind _, Ast_Text txt) -> Text txt + ^^^^^^^^ +Error: This expression has type ([< inkind > `Nonlink ] as 'a) inline_t + but an expression was expected of type a inline_t + Type 'a = [< `Link | `Nonlink > `Nonlink ] is not compatible with type + a = [< `Link | `Nonlink ] Types for tag `Nonlink are incompatible # diff --git a/testsuite/tests/typing-gadts/pr5689.ml.reference b/testsuite/tests/typing-gadts/pr5689.ml.reference index f1e142aad..fabdb17cd 100644 --- a/testsuite/tests/typing-gadts/pr5689.ml.reference +++ b/testsuite/tests/typing-gadts/pr5689.ml.reference @@ -16,13 +16,12 @@ type _ inline_t = # type _ linkp = Nonlink : [ `Nonlink ] linkp | Maylink : inkind linkp # val inlineseq_from_astseq : ast_t list -> inkind inline_t list = <fun> # type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2 -# Characters 272-279: - | (Kind Maylink, Ast_Link lnk) -> Link lnk - ^^^^^^^ -Error: This pattern matches values of type inkind linkp - but a pattern was expected which matches values of type - ([< inkind ] as 'a) linkp - Type inkind = [ `Link | `Nonlink ] is not compatible with type - 'a = [< `Link | `Nonlink ] +# Characters 184-192: + | (Kind _, Ast_Text txt) -> Text txt + ^^^^^^^^ +Error: This expression has type ([< inkind > `Nonlink ] as 'a) inline_t + but an expression was expected of type a inline_t + Type 'a = [< `Link | `Nonlink > `Nonlink ] is not compatible with type + a = [< `Link | `Nonlink ] Types for tag `Nonlink are incompatible # diff --git a/testsuite/tests/typing-gadts/pr5989.ml b/testsuite/tests/typing-gadts/pr5989.ml new file mode 100644 index 000000000..392df7f2d --- /dev/null +++ b/testsuite/tests/typing-gadts/pr5989.ml @@ -0,0 +1,35 @@ +type (_, _) t = + Any : ('a, 'b) t + | Eq : ('a, 'a) t +;; + +module M : +sig + type s = private [> `A] + val eq : (s, [`A | `B]) t +end = +struct + type s = [`A | `B] + let eq = Eq +end;; + +let f : (M.s, [`A | `B]) t -> string = function + | Any -> "Any" +;; + +let () = print_endline (f M.eq) ;; + +module N : +sig + type s = private < a : int; .. > + val eq : (s, <a : int; b : bool>) t +end = +struct + type s = <a : int; b : bool> + let eq = Eq +end +;; + +let f : (N.s, <a : int; b : bool>) t -> string = function + | Any -> "Any" +;; diff --git a/testsuite/tests/typing-gadts/pr5989.ml.reference b/testsuite/tests/typing-gadts/pr5989.ml.reference new file mode 100644 index 000000000..f881c9b82 --- /dev/null +++ b/testsuite/tests/typing-gadts/pr5989.ml.reference @@ -0,0 +1,24 @@ + +# type (_, _) t = Any : ('a, 'b) t | Eq : ('a, 'a) t +# module M : sig type s = private [> `A ] val eq : (s, [ `A | `B ]) t end +# Characters 40-65: + .......................................function + | Any -> "Any" +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +Eq +val f : (M.s, [ `A | `B ]) t -> string = <fun> +# Exception: Match_failure ("//toplevel//", 14, 39). +# module N : + sig + type s = private < a : int; .. > + val eq : (s, < a : int; b : bool >) t + end +# Characters 50-75: + .................................................function + | Any -> "Any" +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +Eq +val f : (N.s, < a : int; b : bool >) t -> string = <fun> +# diff --git a/typing/ctype.ml b/typing/ctype.ml index df9261327..2bbba4d1f 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -2287,7 +2287,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 -> |