From 167e66e15d94f685b2bed2b29aa0a743978dc425 Mon Sep 17 00:00:00 2001 From: Thomas Refis Date: Wed, 8 Jul 2020 10:35:40 +0200 Subject: [PATCH] type_cases: rely on levels to enforce principality (#1931) Instead of the erasure scheme that was used up to now, where we considered that the type was always principal. Note: the erasure still happens when polymorphic variants appear in the patterns, and the type of the scrutinee contains a Reither. --- Changes | 3 + testsuite/tests/let-syntax/let_syntax.ml | 24 +- .../tests/typing-core-bugs/const_int_hint.ml | 6 - testsuite/tests/typing-gadts/or_patterns.ml | 14 - testsuite/tests/typing-gadts/pr6690.ml | 20 - testsuite/tests/typing-gadts/pr7222.ml | 12 - testsuite/tests/typing-gadts/pr7902.ml | 8 - .../typing-gadts/principality-and-gadts.ml | 442 ++++++++++++++++++ testsuite/tests/typing-gadts/test.ml | 6 - .../typing-misc/disambiguate_principality.ml | 68 ++- testsuite/tests/typing-misc/pr7937.ml | 33 +- testsuite/tests/typing-poly/pr9603.ml | 12 - .../ambiguous_guarded_disjunction.ml | 29 ++ testsuite/tests/typing-warnings/pr6872.ml | 8 +- testsuite/tests/typing-warnings/records.ml | 48 +- typing/ctype.ml | 69 ++- typing/ctype.mli | 9 +- typing/typecore.ml | 50 +- 18 files changed, 695 insertions(+), 166 deletions(-) create mode 100644 testsuite/tests/typing-gadts/principality-and-gadts.ml diff --git a/Changes b/Changes index d7635997e..78261f437 100644 --- a/Changes +++ b/Changes @@ -159,6 +159,9 @@ Working version ### Compiler user-interface and warnings: +- #1931: rely on levels to enforce principality in patterns + (Thomas Refis and Leo White, review by Jacques Garrigue) + * #9011: Do not create .a/.lib files when creating a .cmxa with no modules. macOS ar doesn't support creating empty .a files (#1094) and MSVC doesn't permit .lib files to contain no objects. When linking with a .cmxa containing diff --git a/testsuite/tests/let-syntax/let_syntax.ml b/testsuite/tests/let-syntax/let_syntax.ml index 9f19e0e4a..502aac6a4 100644 --- a/testsuite/tests/let-syntax/let_syntax.ml +++ b/testsuite/tests/let-syntax/let_syntax.ml @@ -587,7 +587,8 @@ val let_not_principal : unit = () Line 3, characters 9-10: 3 | let+ A = A.A in ^ -Error: Unbound constructor A +Warning 18: this type-based constructor disambiguation is not principal. +val let_not_principal : unit = () |}];; module And_not_principal = struct @@ -615,7 +616,8 @@ val and_not_principal : A.t -> A.t -> unit = Line 5, characters 11-12: 5 | and+ A = y in ^ -Error: Unbound constructor A +Warning 18: this type-based constructor disambiguation is not principal. +val and_not_principal : A.t -> A.t -> unit = |}];; module Let_not_propagated = struct @@ -713,12 +715,16 @@ let bad_location = [%%expect{| val bad_location : 'a GADT_ordering.is_point -> 'a -> int = |}, Principal{| -Line 4, characters 6-10: +Line 4, characters 11-19: 4 | let+ Is_point = is_point - ^^^^ -Error: This pattern matches values of type - GADT_ordering.point GADT_ordering.is_point * GADT_ordering.point - but a pattern was expected which matches values of type - a GADT_ordering.is_point * a - Type GADT_ordering.point is not compatible with type a + ^^^^^^^^ +Warning 18: typing this pattern requires considering GADT_ordering.point and a as equal. +But the knowledge of these types is not principal. +Line 5, characters 13-14: +5 | and+ { x; y } = a in + ^ +Error: The record field x belongs to the type GADT_ordering.point + but is mixed here with fields of type a = GADT_ordering.point + This instance of GADT_ordering.point is ambiguous: + it would escape the scope of its equation |}];; diff --git a/testsuite/tests/typing-core-bugs/const_int_hint.ml b/testsuite/tests/typing-core-bugs/const_int_hint.ml index bc4b528bd..b103791b8 100644 --- a/testsuite/tests/typing-core-bugs/const_int_hint.ml +++ b/testsuite/tests/typing-core-bugs/const_int_hint.ml @@ -75,12 +75,6 @@ Line 2, characters 4-5: Error: This pattern matches values of type int but a pattern was expected which matches values of type int32 Hint: Did you mean `0l'? -|}, Principal{| -Line 2, characters 4-5: -2 | | 0 -> 0l - ^ -Error: This pattern matches values of type int - but a pattern was expected which matches values of type int32 |}] let _ : int64 -> int64 = function diff --git a/testsuite/tests/typing-gadts/or_patterns.ml b/testsuite/tests/typing-gadts/or_patterns.ml index 6fc7f8c25..cfe711395 100644 --- a/testsuite/tests/typing-gadts/or_patterns.ml +++ b/testsuite/tests/typing-gadts/or_patterns.ml @@ -124,13 +124,6 @@ Line 4, characters 4-11: Error: This pattern matches values of type bool t but a pattern was expected which matches values of type int t Type bool is not compatible with type int -|}, Principal{| -Line 4, characters 4-17: -4 | | BoolLit, true -> () - ^^^^^^^^^^^^^ -Error: This pattern matches values of type bool t * bool - but a pattern was expected which matches values of type int t * int - Type bool is not compatible with type int |}] let simple_annotated (type a) (t : a t) (a : a) = @@ -392,13 +385,6 @@ Line 4, characters 4-11: Error: This pattern matches values of type bool t but a pattern was expected which matches values of type int t Type bool is not compatible with type int -|}, Principal{| -Line 4, characters 4-14: -4 | | BoolLit, x -> x - ^^^^^^^^^^ -Error: This pattern matches values of type bool t * 'a - but a pattern was expected which matches values of type int t * 'b - Type bool is not compatible with type int |}] let noop_annotated (type a) (t : a t) (a : a) : a = diff --git a/testsuite/tests/typing-gadts/pr6690.ml b/testsuite/tests/typing-gadts/pr6690.ml index 858547ea9..ebf308d09 100644 --- a/testsuite/tests/typing-gadts/pr6690.ml +++ b/testsuite/tests/typing-gadts/pr6690.ml @@ -34,19 +34,6 @@ Error: This pattern matches values of type but a pattern was expected which matches values of type ($0, $0 * insert, visit_action) context The type constructor $0 would escape its scope -|}, Principal{| -type 'a visit_action -type insert -type 'a local_visit_action -type ('a, 'result, 'visit_action) context = - Local : ('a, 'a * insert, 'a local_visit_action) context - | Global : ('a, 'a, 'a visit_action) context -Line 15, characters 4-9: -15 | | Local -> fun _ -> raise Exit - ^^^^^ -Error: This pattern matches values of type - ($0, $0 * insert, visit_action) context - The type constructor $0 would escape its scope |}];; let vexpr (type visit_action) @@ -64,13 +51,6 @@ Error: This pattern matches values of type but a pattern was expected which matches values of type ($'a, $'a * insert, visit_action) context The type constructor $'a would escape its scope -|}, Principal{| -Line 4, characters 4-9: -4 | | Local -> fun _ -> raise Exit - ^^^^^ -Error: This pattern matches values of type - ($0, $0 * insert, visit_action) context - The type constructor $0 would escape its scope |}];; let vexpr (type result) (type visit_action) diff --git a/testsuite/tests/typing-gadts/pr7222.ml b/testsuite/tests/typing-gadts/pr7222.ml index 683458b4c..d0177e23c 100644 --- a/testsuite/tests/typing-gadts/pr7222.ml +++ b/testsuite/tests/typing-gadts/pr7222.ml @@ -27,16 +27,4 @@ Error: This pattern matches values of type ($Cons_'x, 'a -> $Cons_'x) elt but a pattern was expected which matches values of type ($Cons_'x, 'a -> $'b -> nil) elt The type constructor $'b would escape its scope -|}, Principal{| -type +'a n = private int -type nil = private Nil_type -type (_, _) elt = - Elt_fine : 'nat n -> ('l, 'nat * 'l) elt - | Elt : 'nat n -> ('l, 'nat -> 'l) elt -type _ t = Nil : nil t | Cons : ('x, 'fx) elt * 'x t -> 'fx t -Line 9, characters 6-22: -9 | let Cons(Elt dim, _) = sh in () - ^^^^^^^^^^^^^^^^ -Error: This pattern matches values of type ('a -> $0 -> nil) t - The type constructor $0 would escape its scope |}];; diff --git a/testsuite/tests/typing-gadts/pr7902.ml b/testsuite/tests/typing-gadts/pr7902.ml index d034d8b60..b88fc23e4 100644 --- a/testsuite/tests/typing-gadts/pr7902.ml +++ b/testsuite/tests/typing-gadts/pr7902.ml @@ -30,12 +30,4 @@ Error: This pattern matches values of type ('a * 'a, 'a * 'a) segment but a pattern was expected which matches values of type ('a * 'a, 'a) segment The type variable 'a occurs inside 'a * 'a -|}, Principal{| -Line 3, characters 4-18: -3 | | SegCons SegNil -> 0 - ^^^^^^^^^^^^^^ -Error: This pattern matches values of type ('a, 'a * 'a) segment - but a pattern was expected which matches values of type - ('a, 'a) segment - The type variable 'a occurs inside 'a * 'a |}] diff --git a/testsuite/tests/typing-gadts/principality-and-gadts.ml b/testsuite/tests/typing-gadts/principality-and-gadts.ml new file mode 100644 index 000000000..9a1d13961 --- /dev/null +++ b/testsuite/tests/typing-gadts/principality-and-gadts.ml @@ -0,0 +1,442 @@ +(* TEST + * expect *) + +module M = struct type t = A | B end;; +[%%expect{| +module M : sig type t = A | B end +|}];; + +type 'a t = I : int t | M : M.t t;; +[%%expect{| +type 'a t = I : int t | M : M.t t +|}];; + +type dyn = Sigma : 'a t * 'a -> dyn;; +[%%expect{| +type dyn = Sigma : 'a t * 'a -> dyn +|}];; + +let f = function Sigma (M, A) -> ();; +[%%expect{| +Line 1, characters 8-35: +1 | let f = function Sigma (M, A) -> ();; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +Sigma (M, B) +val f : dyn -> unit = +|}];; + +type _ t = IntLit : int t | BoolLit : bool t;; +[%%expect{| +type _ t = IntLit : int t | BoolLit : bool t +|}] + +(* The following should warn *) + +let f (type a) t (x : a) = + ignore (t : a t); + match t, x with + | IntLit, n -> n+1 + | BoolLit, b -> 1 +;; +[%%expect{| +val f : 'a t -> 'a -> int = +|}, Principal{| +Line 4, characters 4-10: +4 | | IntLit, n -> n+1 + ^^^^^^ +Warning 18: typing this pattern requires considering int and a as equal. +But the knowledge of these types is not principal. +Line 5, characters 4-11: +5 | | BoolLit, b -> 1 + ^^^^^^^ +Warning 18: typing this pattern requires considering bool and a as equal. +But the knowledge of these types is not principal. +val f : 'a t -> 'a -> int = +|}] + +let f (type a) t (x : a) = + ignore (t : a t); + match t, x with + | IntLit, n -> n+1 + | _, _ -> 1 +;; +[%%expect{| +val f : 'a t -> 'a -> int = +|}, Principal{| +Line 4, characters 4-10: +4 | | IntLit, n -> n+1 + ^^^^^^ +Warning 18: typing this pattern requires considering int and a as equal. +But the knowledge of these types is not principal. +val f : 'a t -> 'a -> int = +|}] + + +let f (type a) t (x : a) = + begin match t, x with + | IntLit, n -> n+1 + | BoolLit, b -> 1 + end; + ignore (t : a t) +;; +[%%expect{| +Line 4, characters 4-11: +4 | | BoolLit, b -> 1 + ^^^^^^^ +Error: This pattern matches values of type bool t + but a pattern was expected which matches values of type int t + Type bool is not compatible with type int +|}] + +let f (type a) t (x : a) = + begin match t, x with + | IntLit, n -> n+1 + | _, _ -> 1 + end; + ignore (t : a t) +;; +[%%expect{| +Line 3, characters 17-18: +3 | | IntLit, n -> n+1 + ^ +Error: This expression has type a but an expression was expected of type int +|}] + +(**********************) +(* Derived from #9019 *) +(**********************) + +type _ ab = A | B + +module M : sig + type _ mab + type _ t = AB : unit ab t | MAB : unit mab t +end = struct + type 'a mab = 'a ab = A | B + type _ t = AB : unit ab t | MAB : unit mab t +end;; +[%%expect{| +type _ ab = A | B +module M : sig type _ mab type _ t = AB : unit ab t | MAB : unit mab t end +|}] + +open M;; +[%%expect{| +|}] + +let f1 t1 = + match t1 with + | AB -> true + | MAB -> false;; +[%%expect{| +val f1 : unit ab M.t -> bool = +|}, Principal{| +Line 4, characters 4-7: +4 | | MAB -> false;; + ^^^ +Warning 18: typing this pattern requires considering unit M.mab and unit ab as equal. +But the knowledge of these types is not principal. +val f1 : unit ab M.t -> bool = +|}] + +let f2 (type x) t1 = + ignore (t1 : x t); + match t1 with + | AB -> true + | MAB -> false;; +[%%expect{| +val f2 : 'x M.t -> bool = +|}, Principal{| +Line 4, characters 4-6: +4 | | AB -> true + ^^ +Warning 18: typing this pattern requires considering unit ab and x as equal. +But the knowledge of these types is not principal. +Line 5, characters 4-7: +5 | | MAB -> false;; + ^^^ +Warning 18: typing this pattern requires considering unit M.mab and x as equal. +But the knowledge of these types is not principal. +val f2 : 'x M.t -> bool = +|}] + +(* This should warn *) +let f3 t1 = + ignore (t1 : unit ab t); + match t1 with + | AB -> true + | MAB -> false;; +[%%expect{| +val f3 : unit ab M.t -> bool = +|}, Principal{| +Line 5, characters 4-7: +5 | | MAB -> false;; + ^^^ +Warning 18: typing this pattern requires considering unit M.mab and unit ab as equal. +But the knowledge of these types is not principal. +val f3 : unit ab M.t -> bool = +|}] + +(* Example showing we need to warn when any part of the type is non generic. *) +type (_,_) eq = Refl : ('a,'a) eq;; +[%%expect{| +type (_, _) eq = Refl : ('a, 'a) eq +|}] + +let g1 (type x) (e : (x, int option) eq) (x : x) : int option = + let Refl = e in x;; +[%%expect{| +val g1 : ('x, int option) eq -> 'x -> int option = +|}] + +(* This should warn *) +let g2 (type x) (e : (x, _ option) eq) (x : x) : int option = + ignore (e : (x, int option) eq); + let Refl = e in x;; +[%%expect{| +val g2 : ('x, int option) eq -> 'x -> int option = +|}, Principal{| +Line 3, characters 7-11: +3 | let Refl = e in x;; + ^^^^ +Warning 18: typing this pattern requires considering x and int option as equal. +But the knowledge of these types is not principal. +val g2 : ('x, int option) eq -> 'x -> int option = +|}] + +(* Issues with "principal level" *) + +module Foo : sig + type t +end = struct + type t = int +end + +type _ gadt = F : Foo.t gadt + +type 'a t = { a: 'a; b: 'a gadt } ;; +[%%expect{| +module Foo : sig type t end +type _ gadt = F : Foo.t gadt +type 'a t = { a : 'a; b : 'a gadt; } +|}] + +let () = + match [] with + | [ { a = 3; _ } ; { b = F; _ }] -> () + | _ -> ();; +[%%expect{| +|}, Principal{| +Line 3, characters 27-28: +3 | | [ { a = 3; _ } ; { b = F; _ }] -> () + ^ +Warning 18: typing this pattern requires considering Foo.t and int as equal. +But the knowledge of these types is not principal. +|}] + +let () = + match [] with + | [ { b = F; _ } ; { a = 3; _ }] -> () + | _ -> ();; +[%%expect{| +Line 3, characters 27-28: +3 | | [ { b = F; _ } ; { a = 3; _ }] -> () + ^ +Error: This pattern matches values of type int + but a pattern was expected which matches values of type Foo.t +|}] + +type (_, _, _) eq3 = Refl3 : ('a, 'a, 'a) eq3 + +type 'a t = { a: 'a; b: (int, Foo.t, 'a) eq3 } +;; +[%%expect{| +type (_, _, _) eq3 = Refl3 : ('a, 'a, 'a) eq3 +type 'a t = { a : 'a; b : (int, Foo.t, 'a) eq3; } +|}] + +let () = + match [] with + | [ { a = 3; _ }; { b = Refl3 ; _ }] -> () + | _ -> () +;; +[%%expect{| +|}, Principal{| +Line 3, characters 26-31: +3 | | [ { a = 3; _ }; { b = Refl3 ; _ }] -> () + ^^^^^ +Warning 18: typing this pattern requires considering int and Foo.t as equal. +But the knowledge of these types is not principal. +|}] + +let () = + match [] with + | [ { b = Refl3 ; _ }; { a = 3; _ } ] -> () + | _ -> () +;; +[%%expect{| +|}, Principal{| +Line 3, characters 12-17: +3 | | [ { b = Refl3 ; _ }; { a = 3; _ } ] -> () + ^^^^^ +Warning 18: typing this pattern requires considering int and Foo.t as equal. +But the knowledge of these types is not principal. +|}] + +(* Unify with 'a first *) + +type 'a t = { a: 'a; b: ('a, int, Foo.t) eq3 } +;; +[%%expect{| +type 'a t = { a : 'a; b : ('a, int, Foo.t) eq3; } +|}] + +let () = + match [] with + | [ { a = 3; _ }; { b = Refl3 ; _ }] -> () + | _ -> () +[%%expect{| +|}, Principal{| +Line 3, characters 26-31: +3 | | [ { a = 3; _ }; { b = Refl3 ; _ }] -> () + ^^^^^ +Warning 18: typing this pattern requires considering int and Foo.t as equal. +But the knowledge of these types is not principal. +|}] + +let () = + match [] with + | [ { b = Refl3 ; _ }; { a = 3; _ } ] -> () + | _ -> () +[%%expect{| +|}, Principal{| +Line 3, characters 12-17: +3 | | [ { b = Refl3 ; _ }; { a = 3; _ } ] -> () + ^^^^^ +Warning 18: typing this pattern requires considering int and Foo.t as equal. +But the knowledge of these types is not principal. +|}] + + +(*************) +(* Some more *) +(*************) + +module M : sig type t end = struct type t = int end +module N : sig type t end = struct type t = int end +;; +[%%expect{| +module M : sig type t end +module N : sig type t end +|}] + +type 'a foo = { x : 'a; eq : (M.t, N.t, 'a) eq3 };; +[%%expect{| +type 'a foo = { x : 'a; eq : (M.t, N.t, 'a) eq3; } +|}] + +let foo x = + match x with + | { x = x; eq = Refl3 } -> x +;; +[%%expect{| +val foo : M.t foo -> M.t = +|}, Principal{| +Line 3, characters 18-23: +3 | | { x = x; eq = Refl3 } -> x + ^^^^^ +Warning 18: typing this pattern requires considering M.t and N.t as equal. +But the knowledge of these types is not principal. +val foo : M.t foo -> M.t = +|}] + +let foo x = + match x with + | { x = (x : int); eq = Refl3 } -> x +;; +[%%expect{| +val foo : int foo -> int = +|}, Principal{| +Line 3, characters 26-31: +3 | | { x = (x : int); eq = Refl3 } -> x + ^^^^^ +Warning 18: typing this pattern requires considering M.t and N.t as equal. +But the knowledge of these types is not principal. +val foo : int foo -> int = +|}] + +let foo x = + match x with + | { x = (x : N.t); eq = Refl3 } -> x +;; +[%%expect{| +Line 3, characters 4-33: +3 | | { x = (x : N.t); eq = Refl3 } -> x + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: This pattern matches values of type N.t foo + but a pattern was expected which matches values of type 'a + This instance of M.t is ambiguous: + it would escape the scope of its equation +|}, Principal{| +Line 3, characters 26-31: +3 | | { x = (x : N.t); eq = Refl3 } -> x + ^^^^^ +Warning 18: typing this pattern requires considering M.t and N.t as equal. +But the knowledge of these types is not principal. +Line 3, characters 4-33: +3 | | { x = (x : N.t); eq = Refl3 } -> x + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: This pattern matches values of type N.t foo + but a pattern was expected which matches values of type 'a + This instance of M.t is ambiguous: + it would escape the scope of its equation +|}] + +let foo x = + match x with + | { x = (x : string); eq = Refl3 } -> x +;; +[%%expect{| +val foo : string foo -> string = +|}, Principal{| +Line 3, characters 29-34: +3 | | { x = (x : string); eq = Refl3 } -> x + ^^^^^ +Warning 18: typing this pattern requires considering M.t and string as equal. +But the knowledge of these types is not principal. +val foo : string foo -> string = +|}] + +let bar x = + match x with + | { x = x; _ } -> x +;; +[%%expect{| +val bar : 'a foo -> 'a = +|}] + +let bar x = + match x with + | { x = (x : int); _ } -> x +;; +[%%expect{| +val bar : int foo -> int = +|}] + +let bar x = + match x with + | { x = (x : N.t); _ } -> x +;; +[%%expect{| +val bar : N.t foo -> N.t = +|}] + +let bar x = + match x with + | { x = (x : string); _ } -> x +;; +[%%expect{| +val bar : string foo -> string = +|}] diff --git a/testsuite/tests/typing-gadts/test.ml b/testsuite/tests/typing-gadts/test.ml index 99da0b696..a5293d785 100644 --- a/testsuite/tests/typing-gadts/test.ml +++ b/testsuite/tests/typing-gadts/test.ml @@ -385,12 +385,6 @@ Line 5, characters 28-29: ^ Error: This variant pattern is expected to have type a The constructor B does not belong to type a -|}, Principal{| -Line 5, characters 28-29: -5 | let f = function A -> 1 | B -> 2 - ^ -Error: This pattern matches values of type b - but a pattern was expected which matches values of type a |}];; module PR6849 = struct diff --git a/testsuite/tests/typing-misc/disambiguate_principality.ml b/testsuite/tests/typing-misc/disambiguate_principality.ml index d1b61f033..fd2cae38c 100644 --- a/testsuite/tests/typing-misc/disambiguate_principality.ml +++ b/testsuite/tests/typing-misc/disambiguate_principality.ml @@ -113,10 +113,15 @@ Line 4, characters 4-15: Warning 11: this match case is unused. val h : M.r -> unit = |}, Principal{| -Line 4, characters 6-9: +Line 4, characters 4-15: 4 | | { lbl = _ } -> () - ^^^ -Error: Unbound record field lbl + ^^^^^^^^^^^ +Warning 18: this type-based record disambiguation is not principal. +Line 4, characters 4-15: +4 | | { lbl = _ } -> () + ^^^^^^^^^^^ +Warning 11: this match case is unused. +val h : M.r -> unit = |}] let i x = @@ -142,6 +147,16 @@ Line 4, characters 4-15: ^^^^^^^^^^^ Warning 12: this sub-pattern is unused. val j : M.r -> unit = +|}, Principal{| +Line 4, characters 4-15: +4 | | { lbl = _ } -> () + ^^^^^^^^^^^ +Warning 18: this type-based record disambiguation is not principal. +Line 4, characters 4-15: +4 | | { lbl = _ } -> () + ^^^^^^^^^^^ +Warning 12: this sub-pattern is unused. +val j : M.r -> unit = |}] let k x = @@ -187,10 +202,15 @@ Line 4, characters 4-30: Warning 11: this match case is unused. val n : M.r ref -> unit = |}, Principal{| -Line 4, characters 19-22: +Line 4, characters 17-28: 4 | | { contents = { lbl = _ } } -> () - ^^^ -Error: Unbound record field lbl + ^^^^^^^^^^^ +Warning 18: this type-based record disambiguation is not principal. +Line 4, characters 4-30: +4 | | { contents = { lbl = _ } } -> () + ^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning 11: this match case is unused. +val n : M.r ref -> unit = |}] let o x = @@ -216,6 +236,16 @@ Line 4, characters 4-30: ^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 12: this sub-pattern is unused. val p : M.r ref -> unit = +|}, Principal{| +Line 4, characters 17-28: +4 | | { contents = { lbl = _ } } -> () + ^^^^^^^^^^^ +Warning 18: this type-based record disambiguation is not principal. +Line 4, characters 4-30: +4 | | { contents = { lbl = _ } } -> () + ^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning 12: this sub-pattern is unused. +val p : M.r ref -> unit = |}] let q x = @@ -364,7 +394,8 @@ val h : M.t -> unit = Line 4, characters 4-5: 4 | | B -> () ^ -Error: Unbound constructor B +Warning 18: this type-based constructor disambiguation is not principal. +val h : M.t -> unit = |}] let i x = @@ -386,6 +417,12 @@ let j x = ;; [%%expect{| val j : M.t -> unit = +|}, Principal{| +Line 4, characters 4-5: +4 | | B -> () + ^ +Warning 18: this type-based constructor disambiguation is not principal. +val j : M.t -> unit = |}] let k x = @@ -434,7 +471,12 @@ val n : M.t ref -> unit = Line 4, characters 17-18: 4 | | { contents = A } -> () ^ -Error: Unbound constructor A +Warning 18: this type-based constructor disambiguation is not principal. +Line 4, characters 4-20: +4 | | { contents = A } -> () + ^^^^^^^^^^^^^^^^ +Warning 11: this match case is unused. +val n : M.t ref -> unit = |}] let o x = @@ -460,6 +502,16 @@ Line 4, characters 4-20: ^^^^^^^^^^^^^^^^ Warning 12: this sub-pattern is unused. val p : M.t ref -> unit = +|}, Principal{| +Line 4, characters 17-18: +4 | | { contents = A } -> () + ^ +Warning 18: this type-based constructor disambiguation is not principal. +Line 4, characters 4-20: +4 | | { contents = A } -> () + ^^^^^^^^^^^^^^^^ +Warning 12: this sub-pattern is unused. +val p : M.t ref -> unit = |}] let q x = diff --git a/testsuite/tests/typing-misc/pr7937.ml b/testsuite/tests/typing-misc/pr7937.ml index c4e42c7d7..731252b2b 100644 --- a/testsuite/tests/typing-misc/pr7937.ml +++ b/testsuite/tests/typing-misc/pr7937.ml @@ -15,13 +15,11 @@ Error: This expression has type bool but an expression was expected of type Types for tag `X are incompatible |}, Principal{| type 'a r = 'a constraint 'a = [< `X of int & 'a ] -Line 3, characters 30-31: +Line 3, characters 35-39: 3 | let f: 'a. 'a r -> 'a r = fun x -> true;; - ^ -Error: This pattern matches values of type + ^^^^ +Error: This expression has type bool but an expression was expected of type ([< `X of 'b & 'a & 'c & 'd & 'e ] as 'a) r - but a pattern was expected which matches values of type - ([< `X of int & 'f ] as 'f) r Types for tag `X are incompatible |}] @@ -34,13 +32,12 @@ Error: This expression has type int ref but an expression was expected of type ([< `X of int & 'a ] as 'a) r Types for tag `X are incompatible |}, Principal{| -Line 1, characters 30-31: +Line 1, characters 35-51: 1 | let g: 'a. 'a r -> 'a r = fun x -> { contents = 0 };; - ^ -Error: This pattern matches values of type + ^^^^^^^^^^^^^^^^ +Error: This expression has type int ref + but an expression was expected of type ([< `X of 'b & 'a & 'c & 'd & 'e ] as 'a) r - but a pattern was expected which matches values of type - ([< `X of int & 'f ] as 'f) r Types for tag `X are incompatible |}] @@ -53,14 +50,6 @@ Error: This pattern matches values of type bool but a pattern was expected which matches values of type ([< `X of int & 'a ] as 'a) r Types for tag `X are incompatible -|}, Principal{| -Line 1, characters 32-36: -1 | let h: 'a. 'a r -> _ = function true | false -> ();; - ^^^^ -Error: This pattern matches values of type bool - but a pattern was expected which matches values of type - ([< `X of 'b & 'a & 'c ] as 'a) r - Types for tag `X are incompatible |}] @@ -73,12 +62,4 @@ Error: This pattern matches values of type int ref but a pattern was expected which matches values of type ([< `X of int & 'a ] as 'a) r Types for tag `X are incompatible -|}, Principal{| -Line 1, characters 32-48: -1 | let i: 'a. 'a r -> _ = function { contents = 0 } -> ();; - ^^^^^^^^^^^^^^^^ -Error: This pattern matches values of type int ref - but a pattern was expected which matches values of type - ([< `X of 'b & 'a & 'c ] as 'a) r - Types for tag `X are incompatible |}] diff --git a/testsuite/tests/typing-poly/pr9603.ml b/testsuite/tests/typing-poly/pr9603.ml index 382b1c2ba..9052a1a43 100644 --- a/testsuite/tests/typing-poly/pr9603.ml +++ b/testsuite/tests/typing-poly/pr9603.ml @@ -33,16 +33,4 @@ Error: This expression has type is not compatible with type < left : 'left0; right : 'right0 > pair The method left has type 'a, but the expected method type was 'left The universal variable 'left would escape its scope -|}, Principal{| -Line 4, characters 6-7: -4 | = fun x -> x - ^ -Error: This pattern matches values of type - < m : 'left 'right. < left : 'left; right : 'right > pair > - but a pattern was expected which matches values of type - < m : 'left 'right. < left : 'left; right : 'right > pair > - Type < left : 'left; right : 'right > pair = 'a * 'b - is not compatible with type < left : 'left0; right : 'right0 > pair - The method left has type 'a, but the expected method type was 'left - The universal variable 'left would escape its scope |}] diff --git a/testsuite/tests/typing-warnings/ambiguous_guarded_disjunction.ml b/testsuite/tests/typing-warnings/ambiguous_guarded_disjunction.ml index 27b12920d..90f50623e 100644 --- a/testsuite/tests/typing-warnings/ambiguous_guarded_disjunction.ml +++ b/testsuite/tests/typing-warnings/ambiguous_guarded_disjunction.ml @@ -380,6 +380,35 @@ Line 2, characters 4-56: ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 57: Ambiguous or-pattern variables under guard; variables x,y may match different arguments. (See manual section 9.5) +val ambiguous_xy_but_not_ambiguous_z : (int -> int -> bool) -> t2 -> int = + +|}, Principal{| +Line 2, characters 4-5: +2 | | A (x as z,(0 as y))|A (0 as y as z,x)|B (x,(y as z)) when g x (y+z) -> 1 + ^ +Warning 41: A belongs to several types: t2 t +The first one was selected. Please disambiguate if this is wrong. +Line 2, characters 24-25: +2 | | A (x as z,(0 as y))|A (0 as y as z,x)|B (x,(y as z)) when g x (y+z) -> 1 + ^ +Warning 41: A belongs to several types: t2 t +The first one was selected. Please disambiguate if this is wrong. +Line 2, characters 42-43: +2 | | A (x as z,(0 as y))|A (0 as y as z,x)|B (x,(y as z)) when g x (y+z) -> 1 + ^ +Warning 41: B belongs to several types: t2 t +The first one was selected. Please disambiguate if this is wrong. +Lines 1-3, characters 41-10: +1 | .........................................function +2 | | A (x as z,(0 as y))|A (0 as y as z,x)|B (x,(y as z)) when g x (y+z) -> 1 +3 | | _ -> 2 +Warning 4: this pattern-matching is fragile. +It will remain exhaustive when constructors are added to type t2. +Line 2, characters 4-56: +2 | | A (x as z,(0 as y))|A (0 as y as z,x)|B (x,(y as z)) when g x (y+z) -> 1 + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning 57: Ambiguous or-pattern variables under guard; +variables x,y may match different arguments. (See manual section 9.5) val ambiguous_xy_but_not_ambiguous_z : (int -> int -> bool) -> t2 -> int = |}] diff --git a/testsuite/tests/typing-warnings/pr6872.ml b/testsuite/tests/typing-warnings/pr6872.ml index 2bf9b8489..80859124b 100644 --- a/testsuite/tests/typing-warnings/pr6872.ml +++ b/testsuite/tests/typing-warnings/pr6872.ml @@ -62,13 +62,13 @@ it will not compile with OCaml 4.00 or earlier. Line 1, characters 26-27: 1 | function Not_found -> 1 | A -> 2 | _ -> 3 ^ -Warning 41: A belongs to several types: a exn -The first one was selected. Please disambiguate if this is wrong. +Warning 18: this type-based constructor disambiguation is not principal. Line 1, characters 26-27: 1 | function Not_found -> 1 | A -> 2 | _ -> 3 ^ -Error: This pattern matches values of type a - but a pattern was expected which matches values of type exn +Warning 42: this use of A relies on type-directed disambiguation, +it will not compile with OCaml 4.00 or earlier. +- : exn -> int = |}] ;; diff --git a/testsuite/tests/typing-warnings/records.ml b/testsuite/tests/typing-warnings/records.ml index 769d46720..7977693f0 100644 --- a/testsuite/tests/typing-warnings/records.ml +++ b/testsuite/tests/typing-warnings/records.ml @@ -122,16 +122,25 @@ Line 6, characters 8-9: Warning 27: unused variable x. module F2 : sig val f : M1.t -> int end |}, Principal{| +Line 6, characters 8-9: +6 | {x; y} -> y + y + ^ +Warning 42: this use of x relies on type-directed disambiguation, +it will not compile with OCaml 4.00 or earlier. +Line 6, characters 11-12: +6 | {x; y} -> y + y + ^ +Warning 42: this use of y relies on type-directed disambiguation, +it will not compile with OCaml 4.00 or earlier. Line 6, characters 7-13: 6 | {x; y} -> y + y ^^^^^^ -Warning 41: these field labels belong to several types: M1.u M1.t -The first one was selected. Please disambiguate if this is wrong. -Line 6, characters 7-13: +Warning 18: this type-based record disambiguation is not principal. +Line 6, characters 8-9: 6 | {x; y} -> y + y - ^^^^^^ -Error: This pattern matches values of type M1.u - but a pattern was expected which matches values of type M1.t + ^ +Warning 27: unused variable x. +module F2 : sig val f : M1.t -> int end |}] (* Use type information with modules*) @@ -633,23 +642,22 @@ module P6235' : val f : u -> string end |}, Principal{| +Line 7, characters 11-14: +7 | |`Key {loc} -> loc + ^^^ +Warning 42: this use of loc relies on type-directed disambiguation, +it will not compile with OCaml 4.00 or earlier. Line 7, characters 10-15: 7 | |`Key {loc} -> loc ^^^^^ -Warning 41: these field labels belong to several types: v t -The first one was selected. Please disambiguate if this is wrong. -Line 7, characters 10-15: -7 | |`Key {loc} -> loc - ^^^^^ -Warning 9: the following labels are not bound in this record pattern: -x -Either bind these labels explicitly or add '; _' to the pattern. -Line 7, characters 5-15: -7 | |`Key {loc} -> loc - ^^^^^^^^^^ -Error: This pattern matches values of type [? `Key of v ] - but a pattern was expected which matches values of type u - Types for tag `Key are incompatible +Warning 18: this type-based record disambiguation is not principal. +module P6235' : + sig + type t = { loc : string; } + type v = { loc : string; x : int; } + type u = [ `Key of t ] + val f : u -> string + end |}] (** no candidates after filtering; diff --git a/typing/ctype.ml b/typing/ctype.ml index a53e909d1..eb8011b76 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -301,15 +301,24 @@ type unification_mode = | Expression (* unification in expression *) | Pattern (* unification in pattern which may add local constraints *) +type equations_generation = + | Forbidden + | Allowed of { equated_types : unit TypePairs.t } + let umode = ref Expression -let generate_equations = ref false +let equations_generation = ref Forbidden let assume_injective = ref false let allow_recursive_equation = ref false +let can_generate_equations () = + match !equations_generation with + | Forbidden -> false + | _ -> true + let set_mode_pattern ~generate ~injective ~allow_recursive f = Misc.protect_refs [ Misc.R (umode, Pattern); - Misc.R (generate_equations, generate); + Misc.R (equations_generation, generate); Misc.R (assume_injective, injective); Misc.R (allow_recursive_equation, allow_recursive); ] f @@ -1065,6 +1074,22 @@ let compute_univars ty = try !(TypeHash.find node_univars ty) with Not_found -> TypeSet.empty +let fully_generic ty = + let rec aux acc ty = + acc && + let ty = repr ty in + ty.level < lowest_level || ( + ty.level = generic_level && ( + mark_type_node ty; + fold_type_expr aux true ty + ) + ) + in + let res = aux true ty in + unmark_type ty; + res + + (*******************) (* Instantiation *) (*******************) @@ -2536,6 +2561,12 @@ let unify1_var env t1 t2 = t1.desc <- d1; raise e +(* Can only be called when generate_equations is true *) +let record_equation t1 t2 = + match !equations_generation with + | Forbidden -> assert false + | Allowed { equated_types } -> TypePairs.add equated_types (t1, t2) () + let rec unify (env:Env.t ref) t1 t2 = (* First step: special cases (optimizations) *) if t1 == t2 then () else @@ -2665,10 +2696,10 @@ and unify3 env t1 t1' t2 t2' = | (Ttuple tl1, Ttuple tl2) -> unify_list env tl1 tl2 | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 -> - if !umode = Expression || not !generate_equations then + if !umode = Expression || !equations_generation = Forbidden then unify_list env tl1 tl2 else if !assume_injective then - set_mode_pattern ~generate:true ~injective:false + set_mode_pattern ~generate:!equations_generation ~injective:false ~allow_recursive:!allow_recursive_equation (fun () -> unify_list env tl1 tl2) else if in_current_module p1 (* || in_pervasives p1 *) @@ -2683,7 +2714,7 @@ and unify3 env t1 t1' t2 t2' = List.iter2 (fun i (t1, t2) -> if i then unify env t1 t2 else - set_mode_pattern ~generate:false ~injective:false + set_mode_pattern ~generate:Forbidden ~injective:false ~allow_recursive:!allow_recursive_equation begin fun () -> let snap = snapshot () in @@ -2695,25 +2726,31 @@ and unify3 env t1 t1' t2 t2' = | (Tconstr (path,[],_), Tconstr (path',[],_)) when is_instantiable !env path && is_instantiable !env path' - && !generate_equations -> + && can_generate_equations () -> let source, destination = if Path.scope path > Path.scope path' then path , t2' else path', t1' in + record_equation t1' t2'; add_gadt_equation env source destination | (Tconstr (path,[],_), _) - when is_instantiable !env path && !generate_equations -> + when is_instantiable !env path && can_generate_equations () -> reify env t2'; + record_equation t1' t2'; add_gadt_equation env path t2' | (_, Tconstr (path,[],_)) - when is_instantiable !env path && !generate_equations -> + when is_instantiable !env path && can_generate_equations () -> reify env t1'; + record_equation t1' t2'; add_gadt_equation env path t1' | (Tconstr (_,_,_), _) | (_, Tconstr (_,_,_)) when !umode = Pattern -> reify env t1'; reify env t2'; - if !generate_equations then mcomp !env t1' t2' + if can_generate_equations () then ( + mcomp !env t1' t2'; + record_equation t1' t2' + ) | (Tobject (fi1, nm1), Tobject (fi2, _)) -> unify_fields env fi1 fi2; (* Type [t2'] may have been instantiated by [unify_fields] *) @@ -2735,7 +2772,10 @@ and unify3 env t1 t1' t2 t2' = backtrack snap; reify env t1'; reify env t2'; - if !generate_equations then mcomp !env t1' t2' + if can_generate_equations () then ( + mcomp !env t1' t2'; + record_equation t1' t2' + ) end | (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) -> begin match field_kind_repr kind with @@ -3062,10 +3102,15 @@ let unify_gadt ~equations_level:lev ~allow_recursive (env:Env.t ref) ty1 ty2 = try univar_pairs := []; gadt_equations_level := Some lev; - set_mode_pattern ~generate:true ~injective:true ~allow_recursive - (fun () -> unify env ty1 ty2); + let equated_types = TypePairs.create 0 in + set_mode_pattern + ~generate:(Allowed { equated_types }) + ~injective:true + ~allow_recursive + (fun () -> unify env ty1 ty2); gadt_equations_level := None; TypePairs.clear unify_eq_set; + equated_types with e -> gadt_equations_level := None; TypePairs.clear unify_eq_set; diff --git a/typing/ctype.mli b/typing/ctype.mli index e91b38b13..997207e39 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -18,6 +18,8 @@ open Asttypes open Types +module TypePairs : Hashtbl.S with type key = type_expr * type_expr + module Unification_trace: sig (** Unification traces are used to explain unification errors when printing error messages *) @@ -189,6 +191,8 @@ val limited_generalize: type_expr -> type_expr -> unit (* Only generalize some part of the type Make the remaining of the type non-generalizable *) +val fully_generic: type_expr -> bool + val check_scope_escape : Env.t -> int -> type_expr -> unit (* [check_scope_escape env lvl ty] ensures that [ty] could be raised to the level [lvl] without any scope escape. @@ -253,9 +257,10 @@ val unify: Env.t -> type_expr -> type_expr -> unit (* Unify the two types given. Raise [Unify] if not possible. *) val unify_gadt: equations_level:int -> allow_recursive:bool -> - Env.t ref -> type_expr -> type_expr -> unit + Env.t ref -> type_expr -> type_expr -> unit TypePairs.t (* Unify the two types given and update the environment with the - local constraints. Raise [Unify] if not possible. *) + local constraints. Raise [Unify] if not possible. + Returns the pairs of types that have been equated. *) val unify_var: Env.t -> type_expr -> type_expr -> unit (* Same as [unify], but allow free univars when first type is a variable. *) diff --git a/typing/typecore.ml b/typing/typecore.ml index 649554c04..eec62eda9 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -302,21 +302,27 @@ let get_gadt_equations_level () = Some y -> y | None -> assert false +let nothing_equated = TypePairs.create 0 + (* unification inside type_pat*) -let unify_pat_types ?(refine = None) loc env ty ty' = +let unify_pat_types_return_equated_pairs ?(refine = None) loc env ty ty' = try match refine with | Some allow_recursive -> unify_gadt ~equations_level:(get_gadt_equations_level ()) ~allow_recursive env ty ty' | None -> - unify !env ty ty' + unify !env ty ty'; + nothing_equated with | Unify trace -> raise(Error(loc, !env, Pattern_type_clash(trace, None))) | Tags(l1,l2) -> raise(Typetexp.Error(loc, !env, Typetexp.Variant_tags (l1, l2))) +let unify_pat_types ?refine loc env ty ty' = + ignore (unify_pat_types_return_equated_pairs ?refine loc env ty ty') + let unify_pat ?refine env pat expected_ty = try unify_pat_types ?refine pat.pat_loc env pat.pat_type expected_ty with Error (loc, env, Pattern_type_clash(trace, None)) -> @@ -1495,7 +1501,10 @@ and type_pat_aux let expected_type = try let (p0, p, _) = extract_concrete_variant !env expected_ty in - Some (p0, p, true) + let principal = + (repr expected_ty).level = generic_level || not !Clflags.principal + in + Some (p0, p, principal) with Not_found -> None in let constr = @@ -1556,12 +1565,36 @@ and type_pat_aux (* PR#7214: do not use gadt unification for toplevel lets *) let refine = if refine = None && constr.cstr_generalized && no_existentials = None - then Some false else refine in - unify_pat_types ~refine loc env ty_res expected_ty; + then Some false + else refine + in + let equated_types = + unify_pat_types_return_equated_pairs ~refine loc env ty_res expected_ty + in end_def (); generalize_structure expected_ty; generalize_structure ty_res; List.iter generalize_structure ty_args; + if !Clflags.principal then ( + let exception Warn_only_once in + try + TypePairs.iter (fun (t1, t2) () -> + generalize_structure t1; + generalize_structure t2; + if not (fully_generic t1 && fully_generic t2) then + let msg = + Format.asprintf + "typing this pattern requires considering@ %a@ and@ %a@ as \ + equal.@,\ + But the knowledge of these types" + Printtyp.type_expr t1 + Printtyp.type_expr t2 + in + Location.prerr_warning loc (Warnings.Not_principal msg); + raise Warn_only_once + ) equated_types + with Warn_only_once -> () + ); let rec check_non_escaping p = match p.ppat_desc with @@ -1627,7 +1660,10 @@ and type_pat_aux let ty = instance expected_ty in end_def (); generalize_structure ty; - Some (p0, p, true), ty + let principal = + (repr expected_ty).level = generic_level || not !Clflags.principal + in + Some (p0, p, principal), ty with Not_found -> None, newvar () in let type_label_pat (label_lid, label, sarg) k = @@ -4568,7 +4604,7 @@ and type_cases get_current_level () in let take_partial_instance = - if !Clflags.principal || erase_either + if erase_either then Some false else None in begin_def (); (* propagation of the argument *)