variant filtering

[Manuel Fahndrich <maf@microsoft.com>]

Variants are great, but pattern matching should filter used cases in the
default branch. This seems to be a dual of the record modification problem
we've seen some time ago on this list.

Consider the following code:


type 'a status = [`Success 'a | `FailureA | `FailureB | `FailureC ];;

let f () = (`Success "Yeah" :> string status)


let g () =
   match f () with
     `Success s -> `Success 1
   | other      -> (other :> int status)


Status encodes return values that can take a number of different causes,
along with a success case which carries an arbitrary value. Function g tries
to return an int status in the case where f returns success, and the failure
status of f otherwise.

% ocamlc -c status.ml

This expression cannot be coerced to type
  int status = [`Success int|`FailureA|`FailureB|`FailureC];
it has type string status = [`Success string|`FailureA|`FailureB|`FailureC]
but is here used with type int #status as 'a = 'a

The compiler does not filter the Success case out in the default branch of
the compiler, which could tell it to give other the type

  other : [`FailureA | `FailureB | `FailureC ]

which could then be coerced to int status.


I know that the exception type system of Francois Pessaux does a similar
filtering. How hard would it be to add this feature to OCaml?

-Manuel