> I'm trying to use an OCaml program to form an umambiguous protocol
> specification.  I've convinced myself that by proper definition of my types,
> and avoiding using the _ in matches, I can get OCaml to help me verify that
> I have a complete specification.  I'm doing this by defining a function that
> specifies the behavior of one of the protocol partners when it receives a
> message.  Here is an example of what I have.
> 
> let requestOp = REQUEST_KEY | SUCCESS;;
> 
> let message = None | Register of requestOp * int;;
> 
> let receive idList msg =
>  match message with
>     None -> None
> 
> |    Register( REQUEST_KEY, id ) -> begin
>         match idList with
>             [] -> Register(SUCCESS, id)
>         |   l when (List.mem id l) -> Register(Success, (next_available_id
> l))
>         |  _ -> Register(Success, id)
> ;;
> 

To avoid | _ -> ... matching clauses, have a look at the -w E warning.
<http://caml.inria.fr/pub/docs/manual-ocaml/manual022.html>
Section 8.2 'Options'


I cannot get your exact point, besides the above code does not even go through
parsing (missing end), let -> type etc.

In fact what you want to achieve is still unclear.
As regards your message and requestOp types there should be no problem,

Something like

match msg with
| None -> ...
| Register (REQUEST_KEY, id) -> ...
| Register (SUCCESS, id) -> ...

Is easily shown to be exhaustive.

As regards your list example, perhaps you'd like better
match idList with
| [] -> Register(SUCCESS, id)
| _::_ ->
  if List.mem id idList then  Register(SUCCESS, next_available idList)
  else Register(SUCCESS, id)

or even

match idList with
| [] -> Register(SUCCESS, id)
| _::_ when List.mem id idList -> Register(SUCCESS, next_available idList)
| _::_ -> Register(SUCCESS, id)

Both are easily shown to be exhaustive, but frankly, this brings you
no more guarantee than the much more direct code

if List.mem  id idList then
   Register(SUCCESS, next_available_id idList))
else
   Register (SUCESS, id)

-- 
Luc Maranget