Merge pull request #9781 from yallop/injective-stdlib

Add some injectivity annotations to the standard library.

Changes

@@ -105,6 +105,9 @@ Working version
 
 ### Standard library:
 
+- #9781: add injectivity annotations to parameterized abstract types
+  (Jeremy Yallop, review by Nicolás Ojeda Bär)
+
 * #9554: add primitive __FUNCTION__ that returns the name of the current method
   or function, including any enclosing module or class.
   (Nicolás Ojeda Bär, Stephen Dolan, review by Stephen Dolan)

stdlib/atomic.mli

@@ -27,7 +27,7 @@
     import additional compatibility layers. *)
 
 (** An atomic (mutable) reference to a value of type ['a]. *)
-type 'a t
+type !'a t
 
 (** Create an atomic reference. *)
 val make : 'a -> 'a t

stdlib/bigarray.ml

@@ -92,7 +92,7 @@ let c_layout = C_layout
 let fortran_layout = Fortran_layout
 
 module Genarray = struct
-  type ('a, 'b, 'c) t
+  type (!'a, !'b, !'c) t
   external create: ('a, 'b) kind -> 'c layout -> int array -> ('a, 'b, 'c) t
      = "caml_ba_create"
   external get: ('a, 'b, 'c) t -> int array -> 'a
@@ -132,7 +132,7 @@ module Genarray = struct
 end
 
 module Array0 = struct
-  type ('a, 'b, 'c) t = ('a, 'b, 'c) Genarray.t
+  type (!'a, !'b, !'c) t = ('a, 'b, 'c) Genarray.t
   let create kind layout =
     Genarray.create kind layout [||]
   let get arr = Genarray.get arr [||]
@@ -155,7 +155,7 @@ module Array0 = struct
 end
 
 module Array1 = struct
-  type ('a, 'b, 'c) t = ('a, 'b, 'c) Genarray.t
+  type (!'a, !'b, !'c) t = ('a, 'b, 'c) Genarray.t
   let create kind layout dim =
     Genarray.create kind layout [|dim|]
   external get: ('a, 'b, 'c) t -> int -> 'a = "%caml_ba_ref_1"
@@ -192,7 +192,7 @@ module Array1 = struct
 end
 
 module Array2 = struct
-  type ('a, 'b, 'c) t = ('a, 'b, 'c) Genarray.t
+  type (!'a, !'b, !'c) t = ('a, 'b, 'c) Genarray.t
   let create kind layout dim1 dim2 =
     Genarray.create kind layout [|dim1; dim2|]
   external get: ('a, 'b, 'c) t -> int -> int -> 'a = "%caml_ba_ref_2"
@@ -242,7 +242,7 @@ module Array2 = struct
 end
 
 module Array3 = struct
-  type ('a, 'b, 'c) t = ('a, 'b, 'c) Genarray.t
+  type (!'a, !'b, !'c) t = ('a, 'b, 'c) Genarray.t
   let create kind layout dim1 dim2 dim3 =
     Genarray.create kind layout [|dim1; dim2; dim3|]
   external get: ('a, 'b, 'c) t -> int -> int -> int -> 'a = "%caml_ba_ref_3"

stdlib/bigarray.mli

@@ -255,7 +255,7 @@ val fortran_layout : fortran_layout layout
 
 module Genarray :
   sig
-  type ('a, 'b, 'c) t
+  type (!'a, !'b, !'c) t
   (** The type [Genarray.t] is the type of Bigarrays with variable
      numbers of dimensions.  Any number of dimensions between 0 and 16
      is supported.
@@ -477,7 +477,7 @@ module Genarray :
    faster operations, and more precise static type-checking.
    @since 4.05.0 *)
 module Array0 : sig
-  type ('a, 'b, 'c) t
+  type (!'a, !'b, !'c) t
   (** The type of zero-dimensional Bigarrays whose elements have
      OCaml type ['a], representation kind ['b], and memory layout ['c]. *)
 
@@ -535,7 +535,7 @@ end
    Statically knowing the number of dimensions of the array allows
    faster operations, and more precise static type-checking. *)
 module Array1 : sig
-  type ('a, 'b, 'c) t
+  type (!'a, !'b, !'c) t
   (** The type of one-dimensional Bigarrays whose elements have
      OCaml type ['a], representation kind ['b], and memory layout ['c]. *)
 
@@ -632,7 +632,7 @@ end
    case of two-dimensional arrays. *)
 module Array2 :
   sig
-  type ('a, 'b, 'c) t
+  type (!'a, !'b, !'c) t
   (** The type of two-dimensional Bigarrays whose elements have
      OCaml type ['a], representation kind ['b], and memory layout ['c]. *)
 
@@ -748,7 +748,7 @@ end
    of three-dimensional arrays. *)
 module Array3 :
   sig
-  type ('a, 'b, 'c) t
+  type (!'a, !'b, !'c) t
   (** The type of three-dimensional Bigarrays whose elements have
      OCaml type ['a], representation kind ['b], and memory layout ['c]. *)
 

stdlib/camlinternalAtomic.mli

@@ -19,7 +19,7 @@
    modules_before_stdlib used in stdlib/dune does not support the
    Stdlib__ prefix trick. *)
 
-type 'a t
+type !'a t
 val make : 'a -> 'a t
 val get : 'a t -> 'a
 val set : 'a t -> 'a -> unit

stdlib/hashtbl.ml

@@ -287,7 +287,7 @@ module type SeededHashedType =
 module type S =
   sig
     type key
-    type 'a t
+    type !'a t
     val create: int -> 'a t
     val clear : 'a t -> unit
     val reset : 'a t -> unit
@@ -315,7 +315,7 @@ module type S =
 module type SeededS =
   sig
     type key
-    type 'a t
+    type !'a t
     val create : ?random:bool -> int -> 'a t
     val clear : 'a t -> unit
     val reset : 'a t -> unit

stdlib/hashtbl.mli

@@ -22,7 +22,7 @@
 (** {1 Generic interface} *)
 
 
-type ('a, 'b) t
+type (!'a, !'b) t
 (** The type of hash tables from type ['a] to type ['b]. *)
 
 val create : ?random:bool -> int -> ('a, 'b) t
@@ -327,7 +327,7 @@ module type HashedType =
 module type S =
   sig
     type key
-    type 'a t
+    type !'a t
     val create : int -> 'a t
     val clear : 'a t -> unit
     val reset : 'a t -> unit (** @since 4.00.0 *)
@@ -403,7 +403,7 @@ module type SeededHashedType =
 module type SeededS =
   sig
     type key
-    type 'a t
+    type !'a t
     val create : ?random:bool -> int -> 'a t
     val clear : 'a t -> unit
     val reset : 'a t -> unit

stdlib/map.ml

@@ -22,7 +22,7 @@ module type OrderedType =
 module type S =
   sig
     type key
-    type +'a t
+    type !+'a t
     val empty: 'a t
     val is_empty: 'a t -> bool
     val mem:  key -> 'a t -> bool

stdlib/map.mli

@@ -64,7 +64,7 @@ module type S =
     type key
     (** The type of the map keys. *)
 
-    type (+'a) t
+    type !+'a t
     (** The type of maps from type [key] to type ['a]. *)
 
     val empty: 'a t

stdlib/moreLabels.mli

@@ -59,7 +59,7 @@ module Hashtbl : sig
   module type S =
     sig
       type key
-      and 'a t
+      and !'a t
       val create : int -> 'a t
       val clear : 'a t -> unit
       val reset : 'a t -> unit
@@ -89,7 +89,7 @@ module Hashtbl : sig
   module type SeededS =
     sig
       type key
-      and 'a t
+      and !'a t
       val create : ?random:bool -> int -> 'a t
       val clear : 'a t -> unit
       val reset : 'a t -> unit
@@ -133,7 +133,7 @@ module Map : sig
   module type S =
     sig
       type key
-      and (+'a) t
+      and (!+'a) t
       val empty : 'a t
       val is_empty: 'a t -> bool
       val mem : key -> 'a t -> bool

stdlib/queue.mli

@@ -22,7 +22,7 @@
    Failure to do so can lead to a crash.
 *)
 
-type 'a t
+type !'a t
 (** The type of queues containing elements of type ['a]. *)
 
 

stdlib/stack.mli

@@ -18,7 +18,7 @@
    This module implements stacks (LIFOs), with in-place modification.
 *)
 
-type 'a t
+type !'a t
 (** The type of stacks containing elements of type ['a]. *)
 
 exception Empty

stdlib/stream.mli

@@ -15,7 +15,7 @@
 
 (** Streams and parsers. *)
 
-type 'a t
+type !'a t
 (** The type of streams holding values of type ['a]. *)
 
 exception Failure

stdlib/weak.ml

@@ -15,7 +15,7 @@
 
 (** Weak array operations *)
 
-type 'a t
+type !'a t
 
 external create : int -> 'a t = "caml_weak_create"
 

stdlib/weak.mli

@@ -18,7 +18,7 @@
 
 (** {1 Low-level functions} *)
 
-type 'a t
+type !'a t
 (** The type of arrays of weak pointers (weak arrays).  A weak
    pointer is a value that the garbage collector may erase whenever
    the value is not used any more (through normal pointers) by the

testsuite/tests/typing-gadts/pr5985.ml

@@ -70,16 +70,15 @@ Error: In this definition, a type variable cannot be deduced
 (* It is not OK to allow modules exported by other compilation units *)
 type (_,_) eq = Eq : ('a,'a) eq;;
 let eq = Obj.magic Eq;;
-(* pretend that Queue.t is not injective *)
-let eq : ('a Queue.t, 'b Queue.t) eq = eq;;
-type _ t = T : 'a -> 'a Queue.t t;; (* fail *)
+let eq : (('a, 'b) Ephemeron.K1.t, ('c, 'd) Ephemeron.K1.t) eq = eq;;
+type _ t = T : 'a -> ('a, 'b) Ephemeron.K1.t t;; (* fail *)
 [%%expect{|
 type (_, _) eq = Eq : ('a, 'a) eq
 val eq : 'a = <poly>
-val eq : ('a Queue.t, 'b Queue.t) eq = Eq
-Line 5, characters 0-33:
-5 | type _ t = T : 'a -> 'a Queue.t t;; (* fail *)
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+val eq : (('a, 'b) Ephemeron.K1.t, ('c, 'd) Ephemeron.K1.t) eq = Eq
+Line 4, characters 0-46:
+4 | type _ t = T : 'a -> ('a, 'b) Ephemeron.K1.t t;; (* fail *)
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: In this definition, a type variable cannot be deduced
        from the type parameters.
 |}];;

testsuite/tests/typing-implicit_unpack/implicit_unpack.ml

@@ -303,7 +303,7 @@ end
 module type MapT =
   sig
     type key
-    type +'a t
+    type +!'a t
     val empty : 'a t
     val is_empty : 'a t -> bool
     val mem : key -> 'a t -> bool