(* TEST flags = " -w A -strict-sequence " * expect *) let f = function None, None -> 1 | Some _, Some _ -> 2;; [%%expect {| Lines 1-3, characters 8-23: 1 | ........function 2 | None, None -> 1 3 | | Some _, Some _ -> 2.. Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (None, Some _) val f : 'a option * 'b option -> int = |}] type _ t = A : int t | B : bool t | C : char t | D : float t type (_,_,_,_) u = U : (int, int, int, int) u type v = E | F | G ;; [%%expect {| type _ t = A : int t | B : bool t | C : char t | D : float t type (_, _, _, _) u = U : (int, int, int, int) u type v = E | F | G |}] (* Unused cases *) let f (x : int t) = match x with A -> 1 | _ -> 2;; (* warn *) [%%expect {| Line 1, characters 20-48: 1 | let f (x : int t) = match x with A -> 1 | _ -> 2;; (* warn *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 4 [fragile-match]: this pattern-matching is fragile. It will remain exhaustive when constructors are added to type t. Line 1, characters 42-43: 1 | let f (x : int t) = match x with A -> 1 | _ -> 2;; (* warn *) ^ Warning 56 [unreachable-case]: this match case is unreachable. Consider replacing it with a refutation case ' -> .' val f : int t -> int = |}] let f (x : unit t option) = match x with None -> 1 | _ -> 2 ;; (* warn? *) [%%expect {| Line 1, characters 53-54: 1 | let f (x : unit t option) = match x with None -> 1 | _ -> 2 ;; (* warn? *) ^ Warning 56 [unreachable-case]: this match case is unreachable. Consider replacing it with a refutation case ' -> .' val f : unit t option -> int = |}] let f (x : unit t option) = match x with None -> 1 | Some _ -> 2 ;; (* warn *) [%%expect {| Line 1, characters 53-59: 1 | let f (x : unit t option) = match x with None -> 1 | Some _ -> 2 ;; (* warn *) ^^^^^^ Warning 56 [unreachable-case]: this match case is unreachable. Consider replacing it with a refutation case ' -> .' val f : unit t option -> int = |}] let f (x : int t option) = match x with None -> 1 | _ -> 2;; [%%expect {| val f : int t option -> int = |}] let f (x : int t option) = match x with None -> 1;; (* warn *) [%%expect {| Line 1, characters 27-49: 1 | let f (x : int t option) = match x with None -> 1;; (* warn *) ^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Some A val f : int t option -> int = |}] (* Example with record, type, single case *) type 'a box = Box of 'a type 'a pair = {left: 'a; right: 'a};; [%%expect {| type 'a box = Box of 'a type 'a pair = { left : 'a; right : 'a; } |}] let f : (int t box pair * bool) option -> unit = function None -> ();; [%%expect {| Line 1, characters 49-68: 1 | let f : (int t box pair * bool) option -> unit = function None -> ();; ^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Some ({left=Box A; right=Box A}, _) val f : (int t box pair * bool) option -> unit = |}] let f : (string t box pair * bool) option -> unit = function None -> ();; [%%expect {| val f : (string t box pair * bool) option -> unit = |}] let f = function {left=Box 0; _ } -> ();; [%%expect {| Line 1, characters 8-39: 1 | let f = function {left=Box 0; _ } -> ();; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: {left=Box 1; _ } val f : int box pair -> unit = |}] let f = function {left=Box 0;right=Box 1} -> ();; [%%expect {| Line 1, characters 8-47: 1 | let f = function {left=Box 0;right=Box 1} -> ();; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: {left=Box 0; right=Box 0} val f : int box pair -> unit = |}] (* Examples from ML2015 paper *) type _ t = | Int : int t | Bool : bool t ;; [%%expect {| type _ t = Int : int t | Bool : bool t |}] let f : type a. a t -> a = function | Int -> 1 | Bool -> true ;; [%%expect {| val f : 'a t -> 'a = |}] let g : int t -> int = function | Int -> 1 ;; [%%expect {| val g : int t -> int = |}] let h : type a. a t -> a t -> bool = fun x y -> match x, y with | Int, Int -> true | Bool, Bool -> true ;; [%%expect {| val h : 'a t -> 'a t -> bool = |}] type (_, _) cmp = | Eq : ('a, 'a) cmp | Any: ('a, 'b) cmp module A : sig type a type b val eq : (a, b) cmp end = struct type a type b = a let eq = Eq end ;; [%%expect {| type (_, _) cmp = Eq : ('a, 'a) cmp | Any : ('a, 'b) cmp module A : sig type a type b val eq : (a, b) cmp end |}] let f : (A.a, A.b) cmp -> unit = function Any -> () ;; [%%expect {| Line 1, characters 33-51: 1 | let f : (A.a, A.b) cmp -> unit = function Any -> () ^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Eq val f : (A.a, A.b) cmp -> unit = |}] let deep : char t option -> char = function None -> 'c' ;; [%%expect {| val deep : char t option -> char = |}] type zero = Zero type _ succ = Succ ;; [%%expect {| type zero = Zero type _ succ = Succ |}] type (_,_,_) plus = | Plus0 : (zero, 'a, 'a) plus | PlusS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus ;; [%%expect {| type (_, _, _) plus = Plus0 : (zero, 'a, 'a) plus | PlusS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus |}] let trivial : (zero succ, zero, zero) plus option -> bool = function None -> false ;; [%%expect {| val trivial : (zero succ, zero, zero) plus option -> bool = |}] let easy : (zero, zero succ, zero) plus option -> bool = function None -> false ;; [%%expect {| val easy : (zero, zero succ, zero) plus option -> bool = |}] let harder : (zero succ, zero succ, zero succ) plus option -> bool = function None -> false ;; [%%expect {| Line 2, characters 2-24: 2 | function None -> false ^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Some (PlusS _) val harder : (zero succ, zero succ, zero succ) plus option -> bool = |}] let harder : (zero succ, zero succ, zero succ) plus option -> bool = function None -> false | Some (PlusS _) -> . ;; [%%expect {| val harder : (zero succ, zero succ, zero succ) plus option -> bool = |}] let inv_zero : type a b c d. (a,b,c) plus -> (c,d,zero) plus -> bool = fun p1 p2 -> match p1, p2 with | Plus0, Plus0 -> true ;; [%%expect {| val inv_zero : ('a, 'b, 'c) plus -> ('c, 'd, zero) plus -> bool = |}] (* Empty match *) type _ t = Int : int t;; [%%expect {| type _ t = Int : int t |}] let f (x : bool t) = match x with _ -> . ;; (* ok *) [%%expect {| val f : bool t -> 'a = |}] (* trefis in PR#6437 *) let f () = match None with _ -> .;; (* error *) [%%expect {| Line 1, characters 27-28: 1 | let f () = match None with _ -> .;; (* error *) ^ Error: This match case could not be refuted. Here is an example of a value that would reach it: _ |}] let g () = match None with _ -> () | exception _ -> .;; (* error *) [%%expect {| Line 1, characters 47-48: 1 | let g () = match None with _ -> () | exception _ -> .;; (* error *) ^ Error: This match case could not be refuted. Here is an example of a value that would reach it: _ |}] let h () = match None with _ -> . | exception _ -> .;; (* error *) [%%expect {| Line 1, characters 27-28: 1 | let h () = match None with _ -> . | exception _ -> .;; (* error *) ^ Error: This match case could not be refuted. Here is an example of a value that would reach it: _ |}] let f x = match x with _ -> () | None -> .;; (* do not warn *) [%%expect {| val f : 'a option -> unit = |}] (* #7059, all clauses guarded *) let f x y = match 1 with 1 when x = y -> 1;; [%%expect {| Line 1, characters 12-42: 1 | let f x y = match 1 with 1 when x = y -> 1;; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. All clauses in this pattern-matching are guarded. val f : 'a -> 'a -> int = |}] (* #7504, Example with no constraints on a record *) let f = function {contents=_}, 0 -> 0;; [%%expect {| Line 1, characters 8-37: 1 | let f = function {contents=_}, 0 -> 0;; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_, 1) val f : 'a ref * int -> int = |}] (* inexhaustive however some guarded clause might match *) let f = function | None -> () | Some x when x > 0 -> () | Some x when x <= 0 -> () ;; [%%expect {| Lines 1-4, characters 8-28: 1 | ........function 2 | | None -> () 3 | | Some x when x > 0 -> () 4 | | Some x when x <= 0 -> () Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Some _ (However, some guarded clause may match this value.) val f : int option -> unit = |}] (* in the single-row case we can generate more compact witnesses *) module Single_row_optim = struct type t = A | B (* This synthetic program is representative of user-written programs that try to distinguish the cases "only A" and "at least one B" while avoiding a fragile pattern-matching (using just _ in the last row would be fragile). It is a "single row" program from the point of view of exhaustiveness checking because the first row is subsumed by the second and thus removed by the [get_mins] preprocessing of Parmatch. With the single-row optimization implemented in the compiler, it generates a single counter-example that contains or-patterns. Without this optimization, it would generate 2^(N-1) counter-examples (here N=4 so 8), one for each possible expansion of the or-patterns. *) let non_exhaustive : t * t * t * t -> unit = function | A, A, A, A -> () | (A|B), (A|B), (A|B), A (*missing B here*) -> () end;; [%%expect {| Lines 20-22, characters 45-49: 20 | .............................................function 21 | | A, A, A, A -> () 22 | | (A|B), (A|B), (A|B), A (*missing B here*) -> () Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: ((A|B), (A|B), (A|B), B) module Single_row_optim : sig type t = A | B val non_exhaustive : t * t * t * t -> unit end |}]