Shove Type into Compat

src/lib/dune

@@ -60,7 +60,7 @@
     ; util
     Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
     Options Timers Util Vec Version Steps Printer
-    My_zip My_unix My_list Theories Nest Compat Type
+    My_zip My_unix My_list Theories Nest Compat
   )
 
  (js_of_ocaml

src/lib/reasoners/bitv_rel.ml

@@ -1644,28 +1644,28 @@ module Any_propagator : sig
   end
 end = struct
   type 'a t =
-    { id : 'a Type.Id.t
+    { id : 'a Compat.Type.Id.t
     ; hashable : 'a hashable
     ; run : state -> 'a -> unit }
 
   let make hashable run =
-    { id = Type.Id.make () ; hashable ; run }
+    { id = Compat.Type.Id.make () ; hashable ; run }
 
   type binding = B : 'k t * 'k -> binding
 
   module Binding = struct
     type t = binding
 
     let equal (B (k1, v1)) (B (k2, v2)) =
-      match Type.Id.provably_equal k1.id k2.id with
+      match Compat.Type.Id.provably_equal k1.id k2.id with
       | Some Equal ->
         let module T = (val k1.hashable) in
         T.equal v1 v2
       | None -> false
 
     let hash (B (k, v)) =
       let module T = (val k.hashable) in
-      Hashtbl.hash (Type.Id.uid k.id, T.hash v)
+      Hashtbl.hash (Compat.Type.Id.uid k.id, T.hash v)
   end
 
   module Q = Uqueue.Make(Binding)

src/lib/util/compat.ml

@@ -127,3 +127,29 @@ module Seq = struct
 
   include Seq
 end
+
+module Type = struct
+  type (_, _) eq = Equal : ('a, 'a) eq
+
+  module Id = struct
+    type _ id = ..
+
+    module type ID = sig
+      type t
+      type _ id += Id : t id
+    end
+
+    type 'a t = (module ID with type t = 'a)
+
+    let make (type a) () : a t =
+      (module struct type t = a type _ id += Id : t id end)
+
+    let[@inline] uid (type a) ((module A) : a t) =
+      Obj.Extension_constructor.id (Obj.Extension_constructor.of_val A.Id)
+
+    let provably_equal
+        (type a b) ((module A) : a t) ((module B) : b t) : (a, b) eq option
+      =
+      match A.Id with B.Id -> Some Equal | _ -> None
+  end
+end

src/lib/util/compat.mli

@@ -112,3 +112,59 @@ module Seq : sig
 
       @since OCaml 4.14 *)
 end
+
+module Type : sig
+  (** Type introspection.
+
+      @since OCaml 5.1 *)
+
+  type (_, _) eq = Equal: ('a, 'a) eq (** *)
+  (** The purpose of [eq] is to represent type equalities that may not
+      otherwise
+      be known by the type checker (e.g. because they may depend on dynamic
+      data).
+
+      A value of type [(a, b) eq] represents the fact that types [a] and [b]
+      are equal.
+
+      If one has a value [eq : (a, b) eq] that proves types [a] and [b] are
+      equal, one can use it to convert a value of type [a] to a value of
+      type [b] by pattern matching on [Equal]:
+      {[
+        let cast (type a) (type b) (Equal : (a, b) Type.eq) (a : a) : b = a
+      ]}
+
+      At runtime, this function simply returns its second argument
+      unchanged.
+  *)
+
+  (** {1:identifiers Type identifiers} *)
+
+  (** Type identifiers.
+
+      A type identifier is a value that denotes a type. Given two type
+      identifiers, they can be tested for {{!Id.provably_equal}equality} to
+      prove they denote the same type. Note that:
+
+      - Unequal identifiers do not imply unequal types: a given type can be
+        denoted by more than one identifier.
+      - Type identifiers can be marshalled, but they get a new, distinct,
+        identity on unmarshalling, so the equalities are lost. *)
+  module Id : sig
+
+    (** {1:ids Type identifiers} *)
+
+    type !'a t
+    (** The type for identifiers for type ['a]. *)
+
+    val make : unit -> 'a t
+    (** [make ()] is a new type identifier. *)
+
+    val uid : 'a t -> int
+    (** [uid id] is a runtime unique identifier for [id]. *)
+
+    val provably_equal : 'a t -> 'b t -> ('a, 'b) eq option
+    (** [provably_equal i0 i1] is [Some Equal] if identifier [i0] is equal
+        to [i1] and [None] otherwise. *)
+  end
+end