hurf.ml

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

module EqTag : sig
  type 'a t
  val create : unit -> 'a t
  val equal : 'a t -> 'b t -> ('a, 'b) equality option
end = struct
  type 'a tag = ..;;
  type 'a polymorphic_equality = {
    eq : 'b . ('a tag -> 'b tag -> ('a, 'b) equality option);
  }
  type 'a t = 'a tag * 'a polymorphic_equality
  let create (type s) () =
    let module M = struct
      type _ tag += Tag : (s, s) equality -> s tag
      let eq : type a b . a tag -> b tag -> (a, b) equality option =
        fun a b ->
          match a, b with
          | Tag x, Tag _ -> Some x
          | _, _ -> None
    end in
    M.Tag Refl, {eq = M.eq}
  let equal (tag1, {eq}) (tag2, _) = eq tag1 tag2
end