Say I write the following rather pointless piece of code:

type t = A | B | C
let f x =
  match x with
    A -> 1
  | _ -> match x with
           B -> 2
         | C -> 3

The compiler emits Warning P for the second match because it's incomplete
over the constructors of type t. However, it's not really incomplete because
the branch cannot be hit if x = A so the warning is "sort of" incorrect. In
fact, it would also be good if one wrote:

type t = A | B | C
let f x =
  match x with
    A -> 1
  | _ -> match x with
           A -> 1 (* XX *)
         | B -> 2
         | C -> 3

to get a warning that the branch marked XX cannot be reached.

Are these two cases decidable in the general case? 


David