On Thursday 08 February 2007 18:01, David Allsopp wrote:
> Are these two cases decidable in the general case?

It depends how general you make your proposal. In this case, the error can be 
avoided by writing better code, using a single pattern match. When does "in 
general" make that impossible?

You can also do something similar using polymorphic variants to implement 
unions of sum types:

# type a = [`A]
  type bc = [`B | `C];;

  let f : [ a | bc ] -> int = function
    | `A -> 0
    | #bc as b -> match b with
        | `B -> 1
        | `C -> 2;;
val f : [< `A | `B | `C ] -> int = <fun>

Here, the value matching #bc is known to be either `B or `C but not `A.

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists