Re: [Caml-list] Phantom types and variants

["Daniel Bünzli" <daniel.buenzli@erratique.ch>]

Le vendredi, 22 août 2014 à 20:49, Philippe Veber a écrit :
> Here is another proposal:

Thanks Philippe. I also thought about this solution but I wanted to avoid the new allocation. Note that you can actually write that solution without having to write that eq function. This makes the trick:

let coerce kind v = match kind with
| kind when (kind :> kind) = (v.kind :> kind) -> { v with kind = kind }
| _ -> invalid_arg ""


Pierre Chambart also responded to me privately (thanks), suggesting that I do not try to use variants themselves as the coercion specification but another more structured value. His solution (at the end of this email) works. But since I'm a little bit stubborn and that I would really like to use the variant for the coercion specification I tried to adapt its solution as follows. But it fails with a type error that I fail to understand:

Error: This definition has type ([< kind ] as 'a) -> 'a t
which is less general than 'b. ([< kind ] as 'b) -> 'b t



-------------
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) -> 'b t -> 'a t
end = struct
  type kind = [ `A | `B ]

  type +'a t =
    { kind : kind;
      coerce : 'b. ([< kind] as 'b) -> 'b t }
    constraint 'a = [< kind ]

  let a () =
    let rec v = { kind = `A; coerce }
    and coerce : 'b. ([< kind] as 'b) -> 'b t = function
    | `A -> v | `B -> invalid_arg ""
    in
    v

  let b () =
    let rec v = { kind = `B; coerce }
    and coerce : 'b. ([< kind] as 'b) ->'b t = function
    | `A -> v | `B -> invalid_arg ""
    in
    v

  let coerce kind v = v.coerce kind
end

-----------

Any hints ?  

Best,

Daniel

Pierre Chambart's solution:

module M : sig
  type kind = [ `A | `B ]
  type +'a t constraint 'a = [< kind ]
  type 'a coercer constraint 'a = [< kind]
                                   
  val a : unit -> [> `A] t
  val b : unit -> [> `B] t       

  val ac : [`A] coercer
  val coerce : 'a coercer -> 'b t -> 'a t       
end = struct
  type kind = [ `A | `B ]
  type +'a t =
    { kind : kind }
    constraint 'a = [< kind]
                     
  type 'a coercer =
    { f : 'b. 'b t -> 'a t option }
    constraint 'a = [< kind]
                 
  let a () = { kind = `A }
  let b () = { kind = `B }
              
  let ac = { f = (function ({ kind = `A } as v) -> Some v
                         | _ -> None) }
     
  let coerce k v =
    match k.f v with
    | None -> invalid_arg ""
    | Some v -> v
end