gistfile1.fs

module type Equal = sig
  type fst
  type snd
  module Coerce :
    functor (F : sig type 'a t end) -> sig
      val f : fst F.t -> snd F.t
    end
end

type ('a, 'b) equal = (module Equal with type fst = 'a and type snd = 'b)

module Equality : sig
  val refl : ('a, 'a) equal
  val symm : ('a, 'b) equal -> ('b, 'a) equal
  val trans : ('a, 'b) equal -> ('b, 'c) equal -> ('a, 'c) equal

  module Lift (F : sig type 'a t end) : sig
    val lift : ('a, 'b) equal -> ('a F.t, 'b F.t) equal
  end

  val coerce : ('a, 'b) equal -> 'a -> 'b
end =
struct
  let refl (type a) =
    (module struct
       type fst = a
       type snd = a
       module Coerce (F : sig type 'a t end) = struct
         let f x = x
       end
     end : Equal with type fst = a and type snd = a)

  let trans (type a) (type b) (type c) ab bc =
    (module struct
       type fst = a
       type snd = c
       module Coerce (F : sig type 'a t end) = struct
         let f x =
           let module M = (val ab : Equal with type fst = a and type snd = b) in
           let module AB = M.Coerce(F) in
           let module M = (val bc : Equal with type fst = b and type snd = c) in
           let module BC = M.Coerce(F) in
           BC.f (AB.f x)
       end
     end : Equal with type fst = a and type snd = c)

  let coerce (type a) (type b) ab a =
    let module M = (val ab : Equal with type fst = a and type snd = b) in
    let module AB = M.Coerce(struct type 'a t = 'a end) in
    AB.f a

  module Compose (F1 : sig type 'a t end) (F2 : sig type 'a t end) = struct
    type 'a t = 'a F2.t F1.t
  end

  module Lift (F2 : sig type 'a t end) = struct

    let lift (type a) (type b) ab =
      (module struct
         type fst = a F2.t
         type snd = b F2.t
         module Coerce (F1 : sig type 'a t end) = struct
           let f x =
             let module M = (val ab : Equal with type fst = a and type snd = b) in
             let module AB = M.Coerce(Compose(F1)(F2)) in
             AB.f x
         end
       end : Equal with type fst = a F2.t and type snd = b F2.t)
  end

  module FlipEqual (T : sig type t end) = struct
    type 'a t = ('a, T.t) equal
  end

  let symm (type a) (type b) ab =
    let module M = (val ab : Equal with type fst = a and type snd = b) in
    let module AB = M.Coerce(FlipEqual(struct type t = a end)) in
    AB.f refl
end