Wrap says more than that, it states that there is only one way to inject a type in wrap and that it’s the same for any type. From the theorem for free Wadler’s paper, only constant function have this type inj : 'a -> foo for any type foo. (look at this blog post from Bartosz Milewski). In other words, the image by inj of any type is exactly the same singleton subtype of foo (it was the singleton {1} in my example above with foo = int). There is absolutely no way to distinguish two values of type wrap if you only use functions that you can define in the language. Try to implement a function with this type wrap -> wrap -> bool (without any built-in), and you’ll find there is only two : the two constant ones, and the one constantly equal to true is the equality relation on wrap, i.e it’s a singleton.
For instance, I can implement this interface with unit:
module Top_unit : sig
type t
val wrap : 'a -> t
end = struct
type t = unit
let wrap = ignore
end
and you agree that unit is a singleton. But there is no way to distinguish two types with such an interface and there’s only one injection between two of them.
module type Top = sig
type t
val wrap : 'a -> t
end
(* now we compare two distinct implementations *)
module M (Top1 : Top) (Top2 : Top) = struct
(* the only way to produce a value of type Top2.t is
to use the `wrap` function from `Top2` *)
let top1_to_top2 : Top1.t -> Top2.t = fun x -> Top2.wrap x
(* for the same reason there is only one injection in the other sense *)
let top2_to_top1 : Top2.t -> Top1.t = fun x -> Top1.wrap x
end
To me it really looks like a terminal object: for any given type 'a there is only one arrow with domain 'a and codomain Top.t, namely the function Top.wrap.
With type show it’s different. You could have write:
type show = Show : ('a -> string) * 'a -> show
with GADT constructors OCaml uses an uncurry notation, but you should think of it as:
type show = Show : ('a -> string) -> 'a -> show
and so for any type 'a you have a family of injection from 'a to show indexed by conversion function of type 'a -> string. Hence, for a given type the injection is not unique, and it’s not even the same for two distinct types. And if you see it as a module type:
module type Show = sig
type t
val show : ('a -> string) -> 'a -> t
end
the simplest implementation is to use type t = string and show f x = f x. In other words, your type show is equivalent to string. The fact that you can implement this interface with a GADT is just an implementation details.