(* TEST
 expect;
*)

type _ ty = Int : int ty
type dyn = Dyn : 'a ty * 'a -> dyn
[%%expect{|
type _ ty = Int : int ty
type dyn = Dyn : 'a ty * 'a -> dyn
|}]

let ok1 = function Dyn (type a) (w, x : a ty * a) -> ignore (x : a)
let ok2 = function Dyn (type a) (w, x : _ * a) -> ignore (x : a)
[%%expect{|
val ok1 : dyn -> unit = <fun>
val ok2 : dyn -> unit = <fun>
|}]

let ko1 = function Dyn (type a) (w, x) -> ()
[%%expect{|
Line 1, characters 32-38:
1 | let ko1 = function Dyn (type a) (w, x) -> ()
                                    ^^^^^^
Error: Existential types introduced in a constructor pattern
       must be bound by a type constraint on the argument.
|}]
let ko1 = function Dyn (type a) (w, x : _) -> ()
[%%expect{|
Line 1, characters 40-41:
1 | let ko1 = function Dyn (type a) (w, x : _) -> ()
                                            ^
Error: This type does not bind all existentials in the constructor:
         "type a. 'a ty * 'a"
|}]
let ko2 = function Dyn (type a b) (a, x : a ty * b) -> ignore (x : b)
[%%expect{|
Line 1, characters 42-50:
1 | let ko2 = function Dyn (type a b) (a, x : a ty * b) -> ignore (x : b)
                                              ^^^^^^^^
Error: This pattern matches values of type "a ty * b"
       but a pattern was expected which matches values of type "a ty * a"
       Type "b" is not compatible with type "a"
|}]

type u = C : 'a * ('a -> 'b list) -> u
let f = function C (type a b) (x, f : _ * (a -> b list)) -> ignore (x : a)
[%%expect{|
type u = C : 'a * ('a -> 'b list) -> u
val f : u -> unit = <fun>
|}]

let f = function C (type a) (x, f : a * (a -> a list)) -> ignore (x : a)
[%%expect{|
Line 1, characters 36-53:
1 | let f = function C (type a) (x, f : a * (a -> a list)) -> ignore (x : a)
                                        ^^^^^^^^^^^^^^^^^
Error: This type does not bind all existentials in the constructor:
         "type a. a * (a -> a list)"
|}]

(* with GADT unification *)
type _ expr =
  | Int : int -> int expr
  | Add : (int -> int -> int) expr
  | App : ('a -> 'b) expr * 'a expr -> 'b expr

let rec eval : type t. t expr -> t = function
    Int n -> n
  | Add -> (+)
  | App (type a) (f, x : _ * a expr) -> eval f (eval x : a)
[%%expect{|
type _ expr =
    Int : int -> int expr
  | Add : (int -> int -> int) expr
  | App : ('a -> 'b) expr * 'a expr -> 'b expr
val eval : 't expr -> 't = <fun>
|}]

let rec test : type a. a expr -> a = function
  | Int (type b) (n : a) -> n
  | Add -> (+)
  | App (type b) (f, x : (b -> a) expr * _) -> test f (test x : b)
[%%expect{|
Line 2, characters 22-23:
2 |   | Int (type b) (n : a) -> n
                          ^
Error: This type does not bind all existentials in the constructor: "type b. a"
|}]

(* Strange wildcard *)

[@@@warning "-28"]
let () =
  match None with
  | None (type a) (_ : a * int) -> ()
  | Some _ -> ()
[%%expect{|
Line 4, characters 4-31:
4 |   | None (type a) (_ : a * int) -> ()
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The constructor "None" expects 0 argument(s),
       but is applied here to 1 argument(s)
|}]

let () =
  match None with
  | None _ -> ()
  | Some _ -> ()
[%%expect{|
|}]

(* Also allow annotations on multiary constructors *)
type ('a,'b) pair = Pair of 'a * 'b

let f = function Pair (x, y : int * _) -> x + y
[%%expect{|
type ('a, 'b) pair = Pair of 'a * 'b
val f : (int, int) pair -> int = <fun>
|}]
