Injective is an interface that states that a type is injective, where the type is viewed as a function from types to other types. It predates OCaml's support for explicit injectivity annotations in the type system.
conv t x uses the type equality t : (a, b) t as evidence to safely cast x from type a to type b. conv is semantically just the identity function.
In a program that has t : (a, b) t where one has a value of type a that one wants to treat as a value of type b, it is often sufficient to pattern match on Type_equal.T rather than use conv. However, there are situations where OCaml's type checker will not use the type equality a = b, and one must use conv. For example:
module F (M1 : sig type t end) (M2 : sig type t end) : sig
val f : (M1.t, M2.t) equal -> M1.t -> M2.t
end = struct
let f equal (m1 : M1.t) = conv equal m1
end
If one wrote the body of F using pattern matching on T:
let f (T : (M1.t, M2.t) equal) (m1 : M1.t) = (m1 : M2.t)
this would give a type error.
It is always safe to conclude that if type a equals b, then for any type 'a t, type a t equals b t. The OCaml type checker uses this fact when it can. However, sometimes, e.g., when using conv, one needs to explicitly use this fact to construct an appropriate Type_equal.t. The Lift* functors do this.
Id provides identifiers for types, and the ability to test (via Id.same) at runtime if two identifiers are equal, and if so to get a proof of equality of their types. Unlike values of type Type_equal.t, values of type Id.t do have semantic content and must have a nontrivial runtime representation.