Actually, I was planning to discuss how to handle this using polymorphic variants (also pointed out by @cristianoc on Discord), so here it is 
As a teaser, the syntactic noise of coercion turns out to be a good thing, relative to what we actually resort to 
With polymorphic variants
One should be able to do:
type 'a completed_state =
[ `Resolved of `a
| `Failed of exn ]
type 'a pending_state =
[ `Pending of ('a completed_state -> unit) list ]
(* callbacks accept only 2 constructors *)
type 'a promise_state =
[ 'a completed_state
| 'a pending_state ]
(* all 3 constructors included *)
type 'a promise =
{mutable state : 'a promise_state}
Then, you get nice callbacks like
let callback =
fun p's_new_state ->
match p's_new_state with
| `Resolved v -> (* ... `f v` ... *)
| `Failed exn -> (* ... something with exn ... *)
and again no need for a `Pending case. However…
Why the simple approach doesn’t work
There are several subtle difficulties. One is that we actually use an existential type right in the “real” promise_state, but let’s set that aside for the existential type post, and focus on simpler and more immediate things Let’s try writing the function that takes a pending promise, and completes it:
let complete p new_completed_state =
match p.state with (* the existing state *)
| `Resolved _ -> assert false (* :( *)
| `Failed _ -> assert false (* :(((((((((( *)
| `Pending callback_list ->
p.state <- (new_completed_state :> _ promise_state);
callback_list |> List.iter (fun f -> f new_completed_state)
The problem here is that we can’t easily write a type for “a promise whose state field can only be `Pending.” So far, we can only put constraints directly on the constructors of promise_state.
Solution: add more type information to promise
One way to solve this is with types like completed and pending from the previous post:
(* Everything is as in the previous GADT post, except that I am explicitly
showing that type promise now takes a 'state type parameter. *)
type completed
type pending
type ('a, 'state) promise =
{mutable state : ('a, 'state) promise_state}
and ('a, 'state) promise_state =
(* ...we would like to link each constructor with a possible value of
type variable `'state`, i.e. `completed` and `pending`, and that's
exactly 50% of what GADTs do (the other 50% being existential
types). So let's just use a GADT: *)
| Resolved : 'a -> ('a, completed) promise_state
| Failed : exn -> ('a, completed) promise_state
| Pending : (('a, completed) promise_state -> unit) list
-> ('a, pending) promise_state
So, with types completed and pending and a GADT, we get to have not only ('a, pending) promise_state, but also ('a, pending) promise, so we can write
val complete :
('a, pending) promise -> ('a, completed) promise_state -> unit
and the entire match expression reduces to a let:
let complete p new_completed_state =
let Pending callback_list = p.state in
p.state <- Obj.magic new_completed_state;
callback_list |> List.iter (fun f -> f new_completed_state)
The Obj.magic is a source of major embarrassment; see the last section of this post.
Insisting on polymorphic variants
Another way to get precise typing, but using polymorphic variants, is to use promise_state itself as a type argument to promise:
(* This is the same as at the top of this post... *)
type 'a completed_state =
[ `Resolved of 'a
| `Failed of exn ]
type 'a pending_state =
[ `Pending of ('a completed_state -> unit) list ]
type 'a promise_state =
[ 'a completed_state
| 'a pending_state ]
(* ...until here, where the type parameter is the type of the state! *)
type 'state promise =
{mutable state : 'state}
and now we have
val complete :
'a pending_state promise -> 'a completed_state -> unit
This actually seems not too bad, but I haven’t explored the consequences for all use cases in lwt.ml. Meanwhile, GADTs immediately fit all of them, and GADTs offer other things we need, like existential types, so GADTs were the clear choice. Their only real drawbacks are (1) relatively few good tutorials (2) the opaque and scary acronym GADT
Regarding the coercion
In the first attempt with polymorphic variants, there was the line
p.state <- (new_completed_state :> _ promise_state);
This is unpleasant, but it’s good compared to what we do with the GADT solution, or would have to do with the precise polymorphic variant solution.
- GADT: if
p is an ('a, pending) promise, then it has an ('a, pending) promise_state, and we have to use Obj.magic to assign an ('a, completed) promise_state to it.
- Polymorphic variant: if
p is an 'a pending_state promise, then it has an 'a pending_state, and we also have to use Obj.magic to assign an 'a completed_state to it.
As far as I know, this is an inevitable tradeoff when you have such precise types, but also mutability. What we currently do in lwt.ml is hide the Obj.magic inside a set_state function:
val set_state :
('a, _) promise -> ('a, 'state) promise_state -> ('a, 'state) promise
and you are supposed to always call it like this:
(* ... we have a promise `p` ... *)
let p = set_state p some_new_state in
(* ... the name `p` is now shadowed, and the new reference has
accurate type constraints ... *)
This is a cheap imitation of a restricted form of linear typing. In practice, p is never used in lwt.ml after set_state anyway, but we still call set_state and shadow the reference, in order to be extra careful and paranoid.
I want to note that all of this is purely internal to the implementation of Lwt. No user has to interact with this casting, nor GADTs, etc.
And, if you have a better way, please propose or contribute it
Its current status is summarized in