“Non-exhaustive pattern matching” warning in let matching

Learning
5

For me such pattern seems mostly convenient when applying the same function (or a composition of functions) to multiple values of the same type and then binding the results to different variable names. Tuples don’t work well here as there has to be a distinct mapping function for each tuple size. I use the following trick:

module F_list = struct
  type ('a, 'b) t =
    | [] : ('a, [`Z]) t
    | (::) : 'a * ('a, [< `Z | `S of _] as 'b) t -> ('a, [`S of 'b]) t

  module T = struct
    type ('a, 'b) f_list = ('a, 'b) t =
      | [] : ('a, [`Z]) f_list
      | (::) : 'a * ('a, [< `Z | `S of _] as 'b) t -> ('a, [`S of 'b]) f_list
  end

  let rec map : type a. _ -> (_, a) t -> (_, a) t = fun f ->
    function
    | [] -> []
    | x :: xs -> f x :: map f xs
end;;
open F_list.T;;
let                                                        [c0; c1; c2; c8] =
     F_list.map (fun n -> Some (`Const (string_of_int n))) [0;  1;  2;  8];;

No warning here since there’s a proof that the lengths of the lists match (due to GADT exhaustiveness).

5 Likes