Merge pull request #8515 from Octachron/reexport_constraint

manual: precise constraints on reexported types

Changes

@@ -116,6 +116,11 @@ Working version
   (Jules Aguillon, with help from Armaël Guéneau,
    review by Gabriel Scherer and Florian Angeletti)
 
+### Manual and documentation:
+
+- PR#8515: manual, precise constraints on reexported types
+  (Florian Angeletti, review by Gabriel Scherer)
+
 ### Bug fixes:
 
 - MPR#3249: ocamlmklib should reject .cmxa files

manual/manual/refman/typedecl.etex

@@ -170,7 +170,9 @@ constructors or fields given in the representation remain attached to
 the defined type constructor. The type expression in the equation part
 must agree with the representation: it must be of the same kind
 (record or variant) and have exactly the same constructors or fields,
-in the same order, with the same arguments.
+in the same order, with the same arguments. Moreover, the new type
+constructor must have the same arity and the same type constraints as the
+original type constructor.
 \end{description}
 
 The type variables appearing as type parameters can optionally be

testsuite/tests/typing-misc/records.ml

@@ -164,3 +164,86 @@ Error: This expression has type string t
        but an expression was expected of type int t
        Type string is not compatible with type int
 |}]
+
+(* reexport *)
+
+type ('a,'b) def = { x:int } constraint 'b = [> `A]
+
+type arity = (int, [`A]) def = {x:int};;
+[%%expect{|
+type ('a, 'b) def = { x : int; } constraint 'b = [> `A ]
+Line 3, characters 0-38:
+3 | type arity = (int, [`A]) def = {x:int};;
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type
+         (int, [ `A ]) def
+       They have different arities.
+|}]
+
+type ('a,'b) ct = (int,'b) def = {x:int};;
+[%%expect{|
+Line 1, characters 0-40:
+1 | type ('a,'b) ct = (int,'b) def = {x:int};;
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type
+         (int, [> `A ]) def
+       Their constraints differ.
+|}]
+
+type ('a,'b) kind = ('a, 'b) def = A constraint 'b = [> `A];;
+[%%expect{|
+Line 1, characters 0-59:
+1 | type ('a,'b) kind = ('a, 'b) def = A constraint 'b = [> `A];;
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type
+         ('a, [> `A ]) def
+       Their kinds differ.
+|}]
+
+type d = { x:int; y : int }
+type mut = d = {x:int; mutable y:int}
+[%%expect{|
+type d = { x : int; y : int; }
+Line 2, characters 0-37:
+2 | type mut = d = {x:int; mutable y:int}
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type d
+       The mutability of field y is different.
+|}]
+
+type missing = d = { x:int }
+[%%expect{|
+Line 1, characters 0-28:
+1 | type missing = d = { x:int }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type d
+       The field y is only present in the original definition.
+|}]
+
+type wrong_type = d = {x:float}
+[%%expect{|
+Line 1, characters 0-31:
+1 | type wrong_type = d = {x:float}
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type d
+       The types for field x are not equal.
+|}]
+
+type unboxed = d = {x:float} [@@unboxed]
+[%%expect{|
+Line 1, characters 0-40:
+1 | type unboxed = d = {x:float} [@@unboxed]
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type d
+       Their internal representations differ:
+       this definition uses unboxed representation.
+|}]
+
+type perm = d = {y:int; x:int}
+[%%expect{|
+Line 1, characters 0-30:
+1 | type perm = d = {y:int; x:int}
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type d
+       Fields number 1 have different names, x and y.
+|}]

testsuite/tests/typing-misc/variant.ml

@@ -42,3 +42,78 @@ module Make :
       val f : [ `A ] -> unit
     end
 |}]
+
+
+(* reexport *)
+type ('a,'b) def = X of int constraint 'b = [> `A]
+
+type arity = (int, [`A]) def = X of int;;
+[%%expect{|
+type ('a, 'b) def = X of int constraint 'b = [> `A ]
+Line 3, characters 0-39:
+3 | type arity = (int, [`A]) def = X of int;;
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type
+         (int, [ `A ]) def
+       They have different arities.
+|}]
+
+type ('a,'b) ct = (int,'b) def = X of int;;
+[%%expect{|
+Line 1, characters 0-41:
+1 | type ('a,'b) ct = (int,'b) def = X of int;;
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type
+         (int, [> `A ]) def
+       Their constraints differ.
+|}]
+
+type ('a,'b) kind = ('a, 'b) def = {a:int} constraint 'b = [> `A];;
+[%%expect{|
+Line 1, characters 0-65:
+1 | type ('a,'b) kind = ('a, 'b) def = {a:int} constraint 'b = [> `A];;
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type
+         ('a, [> `A ]) def
+       Their kinds differ.
+|}]
+
+type d = X of int | Y of int
+
+type missing = d = X of int
+[%%expect{|
+type d = X of int | Y of int
+Line 3, characters 0-27:
+3 | type missing = d = X of int
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type d
+       The field Y is only present in the original definition.
+|}]
+
+type wrong_type = d = X of float
+[%%expect{|
+Line 1, characters 0-32:
+1 | type wrong_type = d = X of float
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type d
+       The types for field X are not equal.
+|}]
+
+type unboxed = d = X of float [@@unboxed]
+[%%expect{|
+Line 1, characters 0-41:
+1 | type unboxed = d = X of float [@@unboxed]
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type d
+       Their internal representations differ:
+       this definition uses unboxed representation.
+|}]
+
+type perm = d = Y of int | X of int
+[%%expect{|
+Line 1, characters 0-35:
+1 | type perm = d = Y of int | X of int
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This variant or record definition does not match that of type d
+       Fields number 1 have different names, X and Y.
+|}]