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

@@ -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

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 = <fun>
 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 = <fun>
 |}];;
 
 module Let_not_propagated = struct
@@ -713,12 +715,16 @@ let bad_location =
 [%%expect{|
 val bad_location : 'a GADT_ordering.is_point -> 'a -> int = <fun>
 |}, Principal{|
-Line 4, characters 6-10:
+Line 4, characters 11-19:
 4 |       let+ Is_point = is_point
-          ^^^^
+               ^^^^^^^^
-Error: This pattern matches values of type
+Warning 18: typing this pattern requires considering GADT_ordering.point and a as equal.
-         GADT_ordering.point GADT_ordering.is_point * GADT_ordering.point
+But the knowledge of these types is not principal.
-       but a pattern was expected which matches values of type
+Line 5, characters 13-14:
-         a GADT_ordering.is_point * a
+5 |       and+ { x; y } = a in
-       Type GADT_ordering.point is not compatible with type a
+                 ^
+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
 |}];;

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

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 =

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)

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
 |}];;

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
 |}]

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 = <fun>
+|}];;
+
+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 = <fun>
+|}, 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 = <fun>
+|}]
+
+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 = <fun>
+|}, 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 = <fun>
+|}]
+
+
+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 = <fun>
+|}, 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 = <fun>
+|}]
+
+let f2 (type x) t1 =
+  ignore (t1 : x t);
+  match t1 with
+  | AB -> true
+  | MAB -> false;;
+[%%expect{|
+val f2 : 'x M.t -> bool = <fun>
+|}, 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 = <fun>
+|}]
+
+(* 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 = <fun>
+|}, 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 = <fun>
+|}]
+
+(* 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 = <fun>
+|}]
+
+(* 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 = <fun>
+|}, 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 = <fun>
+|}]
+
+(* 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 = <fun>
+|}, 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 = <fun>
+|}]
+
+let foo x =
+  match x with
+  | { x = (x : int); eq = Refl3 } -> x
+;;
+[%%expect{|
+val foo : int foo -> int = <fun>
+|}, 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 = <fun>
+|}]
+
+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 = <fun>
+|}, 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 = <fun>
+|}]
+
+let bar x =
+  match x with
+  | { x = x; _ } -> x
+;;
+[%%expect{|
+val bar : 'a foo -> 'a = <fun>
+|}]
+
+let bar x =
+  match x with
+  | { x = (x : int); _ } -> x
+;;
+[%%expect{|
+val bar : int foo -> int = <fun>
+|}]
+
+let bar x =
+  match x with
+  | { x = (x : N.t); _ } -> x
+;;
+[%%expect{|
+val bar : N.t foo -> N.t = <fun>
+|}]
+
+let bar x =
+  match x with
+  | { x = (x : string); _ } -> x
+;;
+[%%expect{|
+val bar : string foo -> string = <fun>
+|}]

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

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 = <fun>
 |}, 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 = <fun>
 |}]
 
 let i x =
@@ -142,6 +147,16 @@ Line 4, characters 4-15:
         ^^^^^^^^^^^
 Warning 12: this sub-pattern is unused.
 val j : M.r -> unit = <fun>
+|}, 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 = <fun>
 |}]
 
 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 = <fun>
 |}, 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 = <fun>
 |}]
 
 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 = <fun>
+|}, 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 = <fun>
 |}]
 
 let q x =
@@ -364,7 +394,8 @@ val h : M.t -> unit = <fun>
 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 = <fun>
 |}]
 
 let i x =
@@ -386,6 +417,12 @@ let j x =
 ;;
 [%%expect{|
 val j : M.t -> unit = <fun>
+|}, Principal{|
+Line 4, characters 4-5:
+4 |   | B -> ()
+        ^
+Warning 18: this type-based constructor disambiguation is not principal.
+val j : M.t -> unit = <fun>
 |}]
 
 let k x =
@@ -434,7 +471,12 @@ val n : M.t ref -> unit = <fun>
 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 = <fun>
 |}]
 
 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 = <fun>
+|}, 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 = <fun>
 |}]
 
 let q x =

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
 |}]

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
 |}]

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 =
+  <fun>
+|}, 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 =
   <fun>
 |}]

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
+Warning 18: this type-based constructor disambiguation is not principal.
-The first one was selected. Please disambiguate if this is wrong.
 Line 1, characters 26-27:
 1 | function Not_found -> 1 | A -> 2 | _ -> 3
                               ^
-Error: This pattern matches values of type a
+Warning 42: this use of A relies on type-directed disambiguation,
-       but a pattern was expected which matches values of type exn
+it will not compile with OCaml 4.00 or earlier.
+- : exn -> int = <fun>
 |}]
 ;;
 

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
+Warning 18: this type-based record disambiguation is not principal.
-The first one was selected. Please disambiguate if this is wrong.
+Line 6, characters 8-9:
-Line 6, characters 7-13:
 6 |        {x; y} -> y + y
-           ^^^^^^
+            ^
-Error: This pattern matches values of type M1.u
+Warning 27: unused variable x.
-       but a pattern was expected which matches values of type M1.t
+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
+Warning 18: this type-based record disambiguation is not principal.
-The first one was selected. Please disambiguate if this is wrong.
+module P6235' :
-Line 7, characters 10-15:
+  sig
-7 |     |`Key {loc} -> loc
+    type t = { loc : string; }
-              ^^^^^
+    type v = { loc : string; x : int; }
-Warning 9: the following labels are not bound in this record pattern:
+    type u = [ `Key of t ]
-x
+    val f : u -> string
-Either bind these labels explicitly or add '; _' to the pattern.
+  end
-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
 |}]
 
 (** no candidates after filtering;

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
+    let equated_types = TypePairs.create 0 in
-                     (fun () -> unify env ty1 ty2);
+    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;

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. *)

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
+        then Some false
-      unify_pat_types ~refine loc env ty_res expected_ty;
+        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 *)