Compiler Explorer

Source code

module Type_equal = struct
  type ('a, 'b) t = T : ('a, 'a) t
end

module List = struct
  include List

let map ~f l = List.map f l
end

module Tag = struct
  type 'a t =
    | Int : int t
    | Bool : bool t
    | String : string t

(* Given two tags, returns a "proof" (a value of [(a, b) Type.equal.t])
     that their types are equal, or None if they are not. *)
  let type_equal (type a b) (fst : a t) (snd : b t)
    : (a, b) Type_equal.t option
    =
    match fst, snd with
    | Int, Int -> Some T          (* a = int = b *)
    | Bool, Bool -> Some T        (* a = bool = b *)
    | String, String -> Some T    (* a = string = b *)
    | _ -> None
end

module List_with_tag = struct
  type 'a t =
    { data : 'a list
    ; tag : 'a Tag.t
    }
  
  module Packed = struct
    type 'a unpacked = 'a t
    type t = T : 'a unpacked -> t
  end
end

module Rpc = struct
  (* call returns a Packed to simulate what an RPC call would likely return
     (the type information is lost in serialization/deserialization) *)
  let call (type a) ({ data; tag } : a List_with_tag.t) : List_with_tag.Packed.t =
    match tag with
    | Int -> T { tag; data = (List.map ~f:(fun x -> x * 2) data) }
    | Bool -> T { tag; data = (List.map ~f:(fun b -> not b) data) }
    | String -> T { tag; data = (List.map ~f:(fun s -> s ^ s) data) }
end

let call_rpc (type a) (lst : a List_with_tag.t) : a List_with_tag.t =
  let T result = Rpc.call lst in
  match Tag.type_equal lst.tag result.tag with
  | None -> failwith "tag returned from rpc call does not match!"
  | Some T -> result