From: "David Allsopp" <dra-news@metastack.com>

> > Given a polymorphic variant type t with a label `B how does one build
> > the type corresponding to t without the label `B.
> 
> So that you could write something like:
> 
> type t = [ `A | `B | `C ]
> 
> let f x =
>   match x with
>     `B                     -> (* x has type t *)
>   | #(t minus [ `B ]) as x -> (* x has type [ `A | `C ] *)
> 
> I end up having to write lots of tedious extra types to achieve that
> normally... I'd find a subtraction syntax very handy too.

There is no theoretical difficulty in adding this (when t is defined),
but this would mean yet more syntax...
I would be curious to see code where this becomes such a pain.
In my view, having to name this type should help clarity.

> On a similar subject, am I the only person who finds I often need to take a
> fixed polymorphic variant value and coerce it so that it can just accept
> more constructors e.g. (seriously contrived example)...
> 
> type t = [ `A | `B | `C ]
> 
> let f (x : t) =
>   match x with
>     `A -> `D
>   | _  -> (x : t :> [> t ])
> 
> Something more concise than (x : t :> [> t ]) would be nice: e.g. (x ::> t)
> But perhaps that really is a job for camlp4!

Indeed, this one is just about syntactic sugar, so camlp4 can do it.
An alternative without new syntax would be to let
  (x :> [> t]) mean (x : [< t] :> [> t]),
but this would break the invariant that coercions always work when the
coerced value is already an instance of the target type (not that
anybody uses this invariant...)

Jacques Garrigue