Hi Daniel,
I really don't see how this could work, since with the definition of coerce:
let coerce k v = if v.kind <> k then invalid_arg "" else v
the expressions [v] and [coerce k v] must have the same type. So the type of [coerce] necessarily is of the form [kind -> 'a t -> 'a t]. You'd have to return a [t] made from [k] instead to capture its type. Here is another proposal:
module M : sig
type kind = [ `A | `B ]
type +'a t constraint 'a = [< kind]
val a : unit -> [> `A] t
val b : unit -> [> `B] t
val coerce : ([< kind] as 'a) -> [< kind] t -> 'a t
end = struct
type kind = [ `A | `B ]
type +'a t =
{ kind : 'a } constraint 'a = [< kind]
let a () = { kind = `A }
let b () = { kind = `B }
let eq x y = match x, y with `A, `A | `B, `B -> true | `A, `B | `B, `A -> false
let coerce k v = if eq v.kind k then invalid_arg "" else { v with kind = k }
end
Not sure though, that this can be used in practice because of the [eq] function: you can't write it with a catch-all case otherwise it does not type with [< ... ] types as its domains. Maybe using GADTs here would be more appropriate?
Cheers,