Auto-closing polymorphic variants ?

[David Teller <David.Teller@univ-orleans.fr>]

   Dear list,

 There are still a number of things I don't quite understand about
polymorphic variants. For instance, polymorphic variants seem to be open
by default.

# let a = `a ;;
val a : [> `a ] = `a
# let b = `b ;;
val b : [> `b ] = `b

I can only assume this was done to keep the property that in
  if ... then some_p else some_q
it must be possible to unify the types of some_p and some_q, which
wouldn't be possible with closed types.

However, as mentioned in the discussion regarding exceptionless error
management, in conjunction with wildcards, sanity checks become
irrelevant, which may lead to hard-to-track errors, e.g.

# let safe_div x = function
  | 0. -> `Div_by_zero
  | y -> `Ok (x /. y) ;;
val safe_div : float -> float -> [> `Div_by_zero | `Ok of float ] = <fun>

# let idiv x y =
  match safe_div (float_of_int x) (float_of_int y) with
  | `Success x -> x
  | _          -> nan ;;
val idiv : int -> int -> float = <fun>


Here, because of the wildcard, ocamlc didn't notice that we wrote
`Success where no such variant could happen.

Now, it seems to me that this wouldn't a real problem if we had a way to
auto-close safe_div during the match, i.e. something like

# let idiv x y =
  match close (safe_div (float_of_int x) (float_of_int y)) with
  | `Success x -> x
     ^^^^^^^^^
  | _          -> nan ;;

 This pattern matches values of type [> `Success of 'a ]
 but is here used to match values of type [ `Div_by_zero | `Ok of  
 float ]
 The second variant type does not allow tag(s) `Success

Of course, we could do that by manually closing the type of safe_div,
but this would essentially mean duplicating information.

Either
# let idiv x y =
  match (safe_div (float_of_int x) (float_of_int y) :
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  [ `Success of float | `Div_by_zero ] ) with
  | `Success x -> x
  | _          -> nan ;;
 This expression has type [> `Div_by_zero | `Ok of float ]
 but is here used with type [ `Div_by_zero | `Success of float ]
 The second variant type does not allow tag(s) `Ok

or
# let idiv x y =
    match(safe_div (float_of_int x) (float_of_int y) : 
    [`Div_by_zero | `Ok of float]) with
    | `Success x -> x
      ^^^^^^^^^^^
    | _          -> nan ;;      
 This pattern matches values of type [> `Success of 'a ]
 but is here used to match values of type [ `Div_by_zero | `Ok of
 float ]
 The second variant type does not allow tag(s) `Success

Unfortunately, I can't seem to find anything comparable to that "close"
operator in the documentation, nor any design pattern which would attain
the same effect.

Does anyone have ideas on this subject ?

Thanks,
 David