Merge pull request #2110 from trefis/gadt-under-or-pattern

Allow GADT constructors to introduce equations and existential types under or-patterns

3 files changed, 769 insertions, 6 deletions

diff --git a/testsuite/tests/typing-gadts/ocamltests b/testsuite/tests/typing-gadts/ocamltests
index e7ca023188..83d75ab147 100644
--- a/testsuite/tests/typing-gadts/ocamltests
+++ b/testsuite/tests/typing-gadts/ocamltests
@@ -3,6 +3,7 @@ didier.ml
 dynamic_frisch.ml
 nested_equations.ml
 omega07.ml
+or_patterns.ml
 pr5332.ml
 pr5689.ml
 pr5785.ml
diff --git a/testsuite/tests/typing-gadts/or_patterns.ml b/testsuite/tests/typing-gadts/or_patterns.ml
new file mode 100644
index 0000000000..c7e0b18d87
--- /dev/null
+++ b/testsuite/tests/typing-gadts/or_patterns.ml
@@ -0,0 +1,763 @@
+(* TEST
+   * expect
+*)
+
+type _ t =
+  | IntLit : int t
+  | BoolLit : bool t
+;;
+
+[%%expect{|
+type _ t = IntLit : int t | BoolLit : bool t
+|}]
+
+let trivial t =
+  match t with
+  | IntLit -> ()
+  | BoolLit -> ()
+;;
+
+[%%expect{|
+Line 4, characters 4-11:
+4 |   | BoolLit -> ()
+        ^^^^^^^
+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 trivial_annotated (type a) (t : a t) =
+  match t with
+  | IntLit -> ()
+  | BoolLit -> ()
+;;
+
+[%%expect{|
+val trivial_annotated : 'a t -> unit = <fun>
+|}]
+
+let trivial_merged t =
+  match t with
+  | IntLit
+  | BoolLit -> ()
+;;
+
+[%%expect{|
+Line 4, characters 4-11:
+4 |   | BoolLit -> ()
+        ^^^^^^^
+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 trivial_merged_annotated (type a) (t : a t) =
+  match t with
+  | IntLit
+  | BoolLit -> ()
+;;
+
+[%%expect{|
+val trivial_merged_annotated : 'a t -> unit = <fun>
+|}]
+
+let trivial_merged_annotated_under_tuple1 (type a) (t : a t) =
+  match (3, t) with
+  | _, (IntLit
+       | BoolLit) -> ()
+;;
+
+[%%expect{|
+val trivial_merged_annotated_under_tuple1 : 'a t -> unit = <fun>
+|}]
+
+let trivial_merged_annotated_under_tuple2 (type a) (tt : a t * a t) =
+  match tt with
+  | IntLit, (IntLit | BoolLit) -> ()
+  | _ -> ()
+;;
+
+[%%expect{|
+Line 3, characters 22-29:
+3 |   | IntLit, (IntLit | BoolLit) -> ()
+                          ^^^^^^^
+Error: This pattern matches values of type bool t
+       but a pattern was expected which matches values of type a t
+       Type bool is not compatible with type a = int
+|}]
+
+let trivial_merged_annotated_under_tuple2 (type a) (tt : a t * a t) =
+  match tt with
+  | (IntLit | BoolLit), IntLit -> ()
+  | _ -> ()
+;;
+
+[%%expect{|
+val trivial_merged_annotated_under_tuple2 : 'a t * 'a t -> unit = <fun>
+|}]
+
+
+let trivial_merged_annotated_under_array (type a) (t : a t array) =
+  match t with
+  | [| (IntLit | BoolLit); _ |] -> ()
+  | [| _; _; (BoolLit | IntLit) |] -> ()
+  | [| _; _; _; (BoolLit | IntLit) |]
+  | [| _; _; _; (BoolLit | IntLit); _ |] -> ()
+  | _ -> ()
+;;
+
+[%%expect{|
+val trivial_merged_annotated_under_array : 'a t array -> unit = <fun>
+|}]
+
+let simple t a =
+  match t, a with
+  | IntLit, 3 -> ()
+  | BoolLit, true -> ()
+  | _, _ -> ()
+;;
+
+[%%expect{|
+Line 4, characters 4-11:
+4 |   | BoolLit, true -> ()
+        ^^^^^^^
+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) =
+  match t, a with
+  | IntLit, 3 -> ()
+  | BoolLit, true -> ()
+  | _, _ -> ()
+;;
+
+[%%expect{|
+val simple_annotated : 'a t -> 'a -> unit = <fun>
+|}]
+
+let simple_merged t a =
+  match t, a with
+  | IntLit, 3
+  | BoolLit, true -> ()
+  | _, _ -> ()
+;;
+
+[%%expect{|
+Line 4, characters 4-11:
+4 |   | BoolLit, true -> ()
+        ^^^^^^^
+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 simple_merged_ambi (type a) (t : a t) a =
+  match t, a with
+  | IntLit, (3 : a)
+  | BoolLit, true -> ()
+  | _, _ -> ()
+;;
+
+[%%expect{|
+Line 4, characters 13-17:
+4 |   | BoolLit, true -> ()
+                 ^^^^
+Error: This pattern matches values of type bool
+       but a pattern was expected which matches values of type a = bool
+       This instance of bool is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+
+let simple_merged_not_annotated_enough (type a) (t : a t) a =
+  match t, a with
+  | IntLit, 3
+  | BoolLit, true -> ()
+  | _, _ -> ()
+;;
+
+[%%expect{|
+Line 4, characters 13-17:
+4 |   | BoolLit, true -> ()
+                 ^^^^
+Error: This pattern matches values of type bool
+       but a pattern was expected which matches values of type int
+|}]
+
+
+let simple_merged_annotated (type a) (t : a t) (a : a) =
+  match t, a with
+  | IntLit, 3
+  | BoolLit, true -> ()
+  | _, _ -> ()
+;;
+
+[%%expect{|
+val simple_merged_annotated : 'a t -> 'a -> unit = <fun>
+|}]
+
+let simple_mega_merged_annotated (type a) (t : a t) (a : a) =
+  match t, a with
+  | IntLit, 3
+  | BoolLit, true
+  | _, _ -> ()
+;;
+
+[%%expect{|
+val simple_mega_merged_annotated : 'a t -> 'a -> unit = <fun>
+|}]
+
+let simple_merged_annotated_return (type a) (t : a t) (a : a) =
+  match t, a with
+  | IntLit, (3 as x)
+  | BoolLit, (true as x) -> ignore x
+  | _, _ -> ()
+;;
+
+[%%expect{|
+Line 3, characters 12-20:
+3 |   | IntLit, (3 as x)
+                ^^^^^^^^
+Error: This pattern matches values of type a
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+let simple_merged_annotated_return_annotated (type a) (t : a t) (a : a) =
+  match t, a with
+  | IntLit, ((3 : a) as x)
+  | BoolLit, ((true : a) as x) -> ignore x
+  | _, _ -> ()
+;;
+
+[%%expect{|
+Line 3, characters 4-57:
+3 | ....IntLit, ((3 : a) as x)
+4 |   | BoolLit, ((true : a) as x)............
+Error: The variable x on the left-hand side of this or-pattern has type
+       a but on the right-hand side it has type bool
+|}]
+
+(* test more scenarios: when the or-pattern itself is not at toplevel but under
+   other patterns. *)
+
+let simple_merged_annotated_under_tuple (type a) (pair : a t * a) =
+  match (), pair with
+  | (), ( IntLit, 3
+        | BoolLit, true) -> ()
+  | _, _ -> ()
+;;
+
+[%%expect{|
+val simple_merged_annotated_under_tuple : 'a t * 'a -> unit = <fun>
+|}]
+
+let simple_merged_annotated_under_arrays (type a) (pair : a t * a) =
+  match [| [| pair |] |] with
+  | [| _ ; [| ( IntLit, 3
+              | BoolLit, true) |] |] -> ()
+  | _ -> ()
+;;
+
+[%%expect{|
+val simple_merged_annotated_under_arrays : 'a t * 'a -> unit = <fun>
+|}]
+
+
+let simple_merged_annotated_under_poly_variant (type a) (pair : a t * a) =
+  match `Foo pair with
+  | `Foo ( IntLit, 3
+         | BoolLit, true ) -> ()
+  | _ -> ()
+;;
+
+[%%expect{|
+Line 3, characters 19-20:
+3 |   | `Foo ( IntLit, 3
+                       ^
+Error: This pattern matches values of type int
+       but a pattern was expected which matches values of type a = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+let simple_merged_annotated_under_poly_variant_annotated (type a) pair =
+  match (`Foo pair : [ `Foo of (a t * a) ]) with
+  | `Foo ( IntLit, 3
+         | BoolLit, true ) -> ()
+  | _ -> ()
+;;
+
+[%%expect{|
+val simple_merged_annotated_under_poly_variant_annotated : 'a t * 'a -> unit =
+  <fun>
+|}]
+
+type 'a iref = { content : 'a; };;
+[%%expect{|
+type 'a iref = { content : 'a; }
+|}]
+
+let simple_merged_annotated_under_record (type a) (pair : a t * a) =
+  match { content = pair } with
+  | { content = ( IntLit, 3
+                | BoolLit, true ) } -> ()
+  | _ -> ()
+;;
+[%%expect{|
+val simple_merged_annotated_under_record : 'a t * 'a -> unit = <fun>
+|}]
+
+let simple_merged_annotated_under_mutable_record (type a) (pair : a t * a) =
+  match { contents = pair } with
+  | { contents = ( IntLit, 3
+                 | BoolLit, true ) } -> ()
+  | _ -> ()
+;;
+[%%expect{|
+val simple_merged_annotated_under_mutable_record : 'a t * 'a -> unit = <fun>
+|}]
+
+type 'a piref = { pcontent : 'b. 'a * 'b; };;
+[%%expect{|
+type 'a piref = { pcontent : 'b. 'a * 'b; }
+|}]
+
+let simple_merged_annotated_under_poly_record1 (type a) (r : (a t * a) piref) =
+  match r with
+  | { pcontent = ( IntLit, 3
+                 | BoolLit, true ), _ } -> ()
+  | _ -> ()
+;;
+[%%expect{|
+val simple_merged_annotated_under_poly_record1 : ('a t * 'a) piref -> unit =
+  <fun>
+|}]
+
+let simple_merged_annotated_under_poly_record2 (type a) (r : (a t * a) piref) =
+  match r with
+  | { pcontent = ( (IntLit, 3), _
+                 | (BoolLit, true), _ ) } -> ()
+  | _ -> ()
+;;
+[%%expect{|
+val simple_merged_annotated_under_poly_record2 : ('a t * 'a) piref -> unit =
+  <fun>
+|}]
+
+let simple_merged_annotated_under_constructor (type a) (pair : a t * a) =
+  match Some pair with
+  | Some ( IntLit, 3
+         | BoolLit, true ) -> ()
+  | _ -> ()
+;;
+[%%expect{|
+val simple_merged_annotated_under_constructor : 'a t * 'a -> unit = <fun>
+|}]
+
+type _ gadt_opt =
+  | GNone : 'a gadt_opt
+  | GSome : 'a -> 'a gadt_opt
+;;
+[%%expect{|
+type _ gadt_opt = GNone : 'a gadt_opt | GSome : 'a -> 'a gadt_opt
+|}]
+
+let simple_merged_annotated_under_gadt_constructor (type a) (pair : a t * a) =
+  match GSome pair with
+  | GSome ( IntLit, 3
+          | BoolLit, true ) -> ()
+  | _ -> ()
+;;
+[%%expect{|
+val simple_merged_annotated_under_gadt_constructor : 'a t * 'a -> unit =
+  <fun>
+|}]
+
+(* back to simpler tests. *)
+
+let noop t a =
+  match t, a with
+  | IntLit, x -> x
+  | BoolLit, x -> x
+;;
+
+[%%expect{|
+Line 4, characters 4-11:
+4 |   | BoolLit, x -> x
+        ^^^^^^^
+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 =
+  match t, a with
+  | IntLit, x -> x
+  | BoolLit, x -> x
+;;
+
+[%%expect{|
+val noop_annotated : 'a t -> 'a -> 'a = <fun>
+|}]
+
+let noop_merged t a =
+  match t, a with
+  | IntLit, x
+  | BoolLit, x -> x
+;;
+
+[%%expect{|
+Line 4, characters 4-11:
+4 |   | BoolLit, x -> x
+        ^^^^^^^
+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 noop_merged_annotated (type a) (t : a t) (a : a) : a =
+  match t, a with
+  | IntLit, x
+  | BoolLit, x -> x
+;;
+
+[%%expect{|
+val noop_merged_annotated : 'a t -> 'a -> 'a = <fun>
+|}]
+
+(***)
+
+type _ t2 =
+  | Int : int -> int t2
+  | Bool : bool -> bool t2
+
+[%%expect{|
+type _ t2 = Int : int -> int t2 | Bool : bool -> bool t2
+|}]
+
+let trivial2 t2 =
+  match t2 with
+  | Int _ -> ()
+  | Bool _ -> ()
+;;
+
+[%%expect{|
+Line 4, characters 4-10:
+4 |   | Bool _ -> ()
+        ^^^^^^
+Error: This pattern matches values of type bool t2
+       but a pattern was expected which matches values of type int t2
+       Type bool is not compatible with type int
+|}]
+
+let trivial2_annotated (type a) (t2 : a t2) =
+  match t2 with
+  | Int _ -> ()
+  | Bool _ -> ()
+;;
+
+[%%expect{|
+val trivial2_annotated : 'a t2 -> unit = <fun>
+|}]
+
+let trivial2_merged t2 =
+  match t2 with
+  | Int _
+  | Bool _ -> ()
+;;
+
+[%%expect{|
+Line 4, characters 4-10:
+4 |   | Bool _ -> ()
+        ^^^^^^
+Error: This pattern matches values of type bool t2
+       but a pattern was expected which matches values of type int t2
+       Type bool is not compatible with type int
+|}]
+
+let trivial2_merged_annotated (type a) (t2 : a t2) =
+  match t2 with
+  | Int _
+  | Bool _ -> ()
+;;
+
+[%%expect{|
+val trivial2_merged_annotated : 'a t2 -> unit = <fun>
+|}]
+
+
+let extract t2 =
+  match t2 with
+  | Int _ -> x
+  | Bool _ -> x
+;;
+
+[%%expect{|
+Line 4, characters 4-10:
+4 |   | Bool _ -> x
+        ^^^^^^
+Error: This pattern matches values of type bool t2
+       but a pattern was expected which matches values of type int t2
+       Type bool is not compatible with type int
+|}]
+
+let extract_annotated (type a) (t2 : a t2) : a =
+  match t2 with
+  | Int x -> x
+  | Bool x -> x
+;;
+
+[%%expect{|
+val extract_annotated : 'a t2 -> 'a = <fun>
+|}]
+
+let extract_merged t2 =
+  match t2 with
+  | Int x
+  | Bool x -> x
+;;
+
+[%%expect{|
+Line 4, characters 4-10:
+4 |   | Bool x -> x
+        ^^^^^^
+Error: This pattern matches values of type bool t2
+       but a pattern was expected which matches values of type int t2
+       Type bool is not compatible with type int
+|}]
+
+let extract_merged_annotated (type a) (t2 : a t2) : a =
+  match t2 with
+  | Int x
+  | Bool x -> x
+;;
+
+
+[%%expect{|
+Line 3, characters 4-20:
+3 | ....Int x
+4 |   | Bool x.....
+Error: The variable x on the left-hand side of this or-pattern has type
+       int but on the right-hand side it has type bool
+|}]
+
+let extract_merged_super_annotated (type a) (t2 : a t2) : a =
+  match t2 with
+  | Int (x : a)
+  | Bool (x : a) -> x
+;;
+
+[%%expect{|
+val extract_merged_super_annotated : 'a t2 -> 'a = <fun>
+|}]
+
+let extract_merged_too_lightly_annotated (type a) (t2 : a t2) : a =
+  match t2 with
+  | Int (x : a)
+  | Bool x -> x
+;;
+
+[%%expect{|
+Line 3, characters 4-26:
+3 | ....Int (x : a)
+4 |   | Bool x.....
+Error: The variable x on the left-hand side of this or-pattern has type
+       a but on the right-hand side it has type bool
+|}]
+
+let extract_merged_super_lightly_annotated (type a) (t2 : a t2) =
+  match t2 with
+  | Int (x : a)
+  | Bool (x : a) -> x
+;;
+
+[%%expect{|
+val extract_merged_super_lightly_annotated : 'a t2 -> 'a = <fun>
+|}]
+
+let lambiguity (type a) (t2 : a t2) =
+  match t2 with
+  | Int ((_ : a) as x)
+  | Bool (x : a) -> x
+;;
+
+[%%expect{|
+Line 3, characters 8-22:
+3 |   | Int ((_ : a) as x)
+            ^^^^^^^^^^^^^^
+Error: This pattern matches values of type a
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+let rambiguity (type a) (t2 : a t2) =
+  match t2 with
+  | Int (_ as x)
+  | Bool ((_ : a) as x) -> x
+;;
+
+[%%expect{|
+Line 4, characters 9-23:
+4 |   | Bool ((_ : a) as x) -> x
+             ^^^^^^^^^^^^^^
+Error: This pattern matches values of type a
+       This instance of a is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+
+(***)
+
+type _ t3 =
+  | A : int t3
+  | B : int t3
+
+[%%expect{|
+type _ t3 = A : int t3 | B : int t3
+|}]
+
+(* This was always allowed as the branches can unify. *)
+let not_annotated x =
+  match x with
+  | A | B -> 3
+;;
+
+[%%expect{|
+val not_annotated : int t3 -> int = <fun>
+|}]
+
+let return_int (type a) (x : a t3) =
+  match x with
+  | A | B -> 3
+;;
+
+[%%expect{|
+val return_int : 'a t3 -> int = <fun>
+|}]
+
+let return_a (type a) (x : a t3) : a =
+  match x with
+  | A | B -> 3 (* fails because the equation [a = int] doesn't escape any of
+                  the branches of this or-pattern. *)
+;;
+
+[%%expect{|
+Line 3, characters 13-14:
+3 |   | A | B -> 3 (* fails because the equation [a = int] doesn't escape any of
+                 ^
+Error: This expression has type int but an expression was expected of type a
+|}]
+
+(* Making sure we don't break a frequent pattern of GADTs indexed by polymorphic
+   variants, where or-patterns were already accepted under or-patterns. *)
+
+type any = [ `A | `B | `C | `D | `E | `F ]
+
+type voyel = [ `A | `E ]
+
+type _ letter =
+  | A : [< any > `A ] letter
+  | B : [< any > `B ] letter
+  | C : [< any > `C ] letter
+  | D : [< any > `D ] letter
+  | E : [< any > `E ] letter
+  | F : [< any > `F ] letter
+
+type _ cased =
+  | Up : 'a letter -> ([< any ] as 'a) cased
+  | Lo : 'a letter -> ([< any ] as 'a) cased
+
+type gvoyel = voyel cased
+type a = [ `A ] cased
+;;
+[%%expect{|
+type any = [ `A | `B | `C | `D | `E | `F ]
+type voyel = [ `A | `E ]
+type _ letter =
+    A : [< any > `A ] letter
+  | B : [< any > `B ] letter
+  | C : [< any > `C ] letter
+  | D : [< any > `D ] letter
+  | E : [< any > `E ] letter
+  | F : [< any > `F ] letter
+type _ cased =
+    Up : 'a letter -> ([< any ] as 'a) cased
+  | Lo : 'a letter -> ([< any ] as 'a) cased
+type gvoyel = voyel cased
+type a = [ `A ] cased
+|}]
+
+let gvoyel_of_a : a -> gvoyel = function
+  | Up A | Lo A as a -> a
+;;
+[%%expect{|
+val gvoyel_of_a : a -> gvoyel = <fun>
+|}]
+
+(* Some other illustrations of the issues with as-patterns. *)
+
+let f_ok (type a) (t : a t) (a : bool iref) (b : a iref) =
+  match t, a, b with
+  | IntLit,  ({ content = true } as x), _
+  | BoolLit,  _,                        ({ content = true} as x) -> ignore x
+  | _, _, _ -> ()
+;;
+[%%expect{|
+val f_ok : 'a t -> bool iref -> 'a iref -> unit = <fun>
+|}]
+
+
+let f_amb (type a) (t : a t) (a : bool ref) (b : a ref) =
+  match t, a, b with
+  | IntLit,  ({ contents = true } as x), _
+  | BoolLit,  _,                        ({ contents = true} as x) -> ignore x
+  | _, _, _ -> ()
+;;
+[%%expect{|
+Line 3, characters 4-108:
+3 | ....IntLit,  ({ contents = true } as x), _
+4 |   | BoolLit,  _,                        ({ contents = true} as x)............
+Error: The variable x on the left-hand side of this or-pattern has type
+         bool ref
+       but on the right-hand side it has type a ref
+       Type bool is not compatible with type a
+|}]
+
+(********************************************)
+
+type t =
+  | A : 'a -> t
+  | B : 'a -> t
+;;
+[%%expect{|
+type t = A : 'a -> t | B : 'a -> t
+|}]
+
+let f = function
+  | A x
+  | B x -> ignore x
+;;
+[%%expect{|
+Line 2, characters 6-7:
+2 |   | A x
+          ^
+Error: This pattern matches values of type $A_'a
+       The type constructor $A_'a would escape its scope
+|}]
diff --git a/testsuite/tests/typing-gadts/test.ml b/testsuite/tests/typing-gadts/test.ml
index f85ddbe120..61061872d8 100644
--- a/testsuite/tests/typing-gadts/test.ml
+++ b/testsuite/tests/typing-gadts/test.ml
@@ -317,12 +317,11 @@ module Or_patterns =
 end
 ;;
 [%%expect{|
-Line 9, characters 11-19:
-9 |         | (IntLit _ | BoolLit _) -> ()
-               ^^^^^^^^
-Error: This pattern matches values of type int t
-       but a pattern was expected which matches values of type s t
-       Type int is not compatible with type s
+module Or_patterns :
+  sig
+    type _ t = IntLit : int -> int t | BoolLit : bool -> bool t
+    val eval : 's t -> unit
+  end
 |}];;
 
 module Polymorphic_variants =