Something something eqtype

eqtype.ml

type (_,_) eq = Refl : ('a,'a) eq

module type EqTag = sig
  type 'a t
  val create : unit -> 'a t
  val equal : 'a t -> 'b t -> ('a, 'b) eq option
end


module M : EqTag = struct

  type 'a w = ..

  module type S = sig
    type a
    type 'a w += T : a w
  end

  type 'a t = (module S with type a = 'a)

  let create (type a') () : a' t =
    let module M = struct
      type a = a'
      type 'a w += T : a w
    end
    in (module M : S with type a = a')

  let equal (type a) (type b) ((module A) : a t) ((module B) : b t) : (a, b) eq option =
    match A.T with
    | B.T -> Some Refl
    | _ -> None

end