Separability axis basics (#3854)

* separability axis

* promote tests

* jkind tests

* Remove `immutable_separable_value`

* Update testsuite/tests/typing-layouts-or-null/separability.ml

Co-authored-by: Richard Eisenberg <[email protected]>

* Update testsuite/tests/typing-layouts-or-null/separability.ml

Co-authored-by: Richard Eisenberg <[email protected]>

* Update testsuite/tests/typing-layouts-or-null/separability.ml

Co-authored-by: Richard Eisenberg <[email protected]>

* Update testsuite/tests/typing-layouts-or-null/separability.ml

Co-authored-by: Richard Eisenberg <[email protected]>

* promote

* address

* Update testsuite/tests/typing-layouts-or-null/separability.ml

Co-authored-by: Richard Eisenberg <[email protected]>

* Update testsuite/tests/typing-layouts-or-null/separability.ml

Co-authored-by: Richard Eisenberg <[email protected]>

* remove `non_float_value`

* update tests

* 80 ch limit

* 80 ch limit

* 80 ch limit

* fixes

* fix + tests

* accept tests

* fixes

---------

Co-authored-by: Diana Kalinichenko <[email protected]>
Co-authored-by: Richard Eisenberg <[email protected]>

Author: 3 people

testsuite/tests/parsetree/source_jane_street.ml

@@ -1261,7 +1261,7 @@ type 'a abstract
 Lines 2-3, characters 0-67:
 2 | type existential_abstract : immutable_data with (type : value mod portable) abstract =
 3 |   | Mk : ('a : value mod portable) abstract -> existential_abstract
-Error: The kind of type "existential_abstract" is value
+Error: The kind of type "existential_abstract" is value mod non_float
          because it's a boxed variant type.
        But the kind of type "existential_abstract" must be a subkind of
          immutable_data with (type : value mod portable) abstract

testsuite/tests/typing-jkind-bounds/basics.ml

@@ -213,7 +213,7 @@ Error: The layout of type "a" is value
          because of the definition of b at line 2, characters 0-30.
 |}]
 
-type a : value mod global aliased many immutable stateless external_ unyielding
+type a : value mod global aliased many immutable stateless external_ unyielding non_float
 type b : value mod local unique once contended nonportable internal = a
 [%%expect{|
 type a : immediate
@@ -273,8 +273,8 @@ Error: Layout void is more experimental than allowed by the enabled layouts exte
 |}]
 
 type a : immediate
-type b : value mod global aliased many immutable stateless unyielding external_ = a
-type c : value mod global aliased many immutable stateless unyielding external_
+type b : value mod global aliased many immutable stateless unyielding external_ non_float = a
+type c : value mod global aliased many immutable stateless unyielding external_ non_float
 type d : immediate = c
 [%%expect{|
 type a : immediate
@@ -284,8 +284,8 @@ type d = c
 |}]
 
 type a : immediate64
-type b : value mod global aliased many immutable stateless unyielding external64 = a
-type c : value mod global aliased many immutable stateless unyielding external64
+type b : value mod global aliased many immutable stateless unyielding external64 non_float = a
+type c : value mod global aliased many immutable stateless unyielding external64 non_float
 type d : immediate64 = c
 [%%expect{|
 type a : immediate64
@@ -1173,11 +1173,11 @@ type 'a t = { x : 'a @@ global many portable aliased contended; } [@@unboxed]
    [layout_of], we'll be able to give a better jkind to [@@unboxed] types, and
    this will likely improve. *)
 
-type 'a t : value mod global immutable stateless many aliased unyielding =
+type 'a t : value mod global immutable stateless many aliased unyielding non_float =
   Foo of 'a @@ global immutable stateless many aliased [@@unboxed]
 [%%expect {|
 Lines 1-2, characters 0-66:
-1 | type 'a t : value mod global immutable stateless many aliased unyielding =
+1 | type 'a t : value mod global immutable stateless many aliased unyielding non_float =
 2 |   Foo of 'a @@ global immutable stateless many aliased [@@unboxed]
 Error: The kind of type "t" is value
          because it instantiates an unannotated type parameter of t,
@@ -1271,7 +1271,7 @@ Error: The kind of type "t" is immutable_data with 'a @@ unyielding
 type ('a : value mod aliased) t = ('a : value mod global)
 type ('a : immediate) t = ('a : value)
 type ('a : value) t = ('a : immediate)
-type ('a : value mod external_ stateless many unyielding) t = ('a : value mod immutable global aliased)
+type ('a : value mod external_ stateless many unyielding non_float) t = ('a : value mod immutable global aliased)
 type ('a : value) t = ('a : any)
 type ('a : value) t = ('a : value)
 type ('a : bits32 mod aliased) t = ('a : any mod global)
@@ -1438,7 +1438,7 @@ Line 1, characters 41-51:
                                              ^^^^^^^^^^
 Error: This expression has type "<  >" but an expression was expected of type
          "('a : value mod aliased)"
-       The kind of <  > is value mod global many
+       The kind of <  > is value mod global many non_float
          because it's the type of an object.
        But the kind of <  > must be a subkind of value mod aliased
          because of the annotation on the wildcard _ at line 1, characters 19-36.
@@ -1451,7 +1451,7 @@ Line 1, characters 42-52:
                                               ^^^^^^^^^^
 Error: This expression has type "<  >" but an expression was expected of type
          "('a : value mod portable)"
-       The kind of <  > is value mod global many
+       The kind of <  > is value mod global many non_float
          because it's the type of an object.
        But the kind of <  > must be a subkind of value mod portable
          because of the annotation on the wildcard _ at line 1, characters 19-37.
@@ -1464,7 +1464,7 @@ Line 1, characters 43-53:
                                                ^^^^^^^^^^
 Error: This expression has type "<  >" but an expression was expected of type
          "('a : value mod contended)"
-       The kind of <  > is value mod global many
+       The kind of <  > is value mod global many non_float
          because it's the type of an object.
        But the kind of <  > must be a subkind of value mod contended
          because of the annotation on the wildcard _ at line 1, characters 19-38.
@@ -1477,7 +1477,7 @@ Line 1, characters 43-53:
                                                ^^^^^^^^^^
 Error: This expression has type "<  >" but an expression was expected of type
          "('a : value mod external_)"
-       The kind of <  > is value mod global many
+       The kind of <  > is value mod global many non_float
          because it's the type of an object.
        But the kind of <  > must be a subkind of value mod external_
          because of the annotation on the wildcard _ at line 1, characters 19-38.
@@ -1666,8 +1666,8 @@ Error: This expression has type "int t" but an expression was expected of type
 (*********************************)
 (* Test 15: extensible variants *)
 
-(* The best kind an extensible variant can get is [value] *)
-type extensible : value = ..
+(* The best kind an extensible variant can get is [value mod non_float] *)
+type extensible : value mod non_float = ..
 [%%expect{|
 type extensible = ..
 |}]
@@ -1676,10 +1676,10 @@ type extensible = ..
 module M : sig
   type t : immediate with extensible
 end = struct
-  type t
+  type t : value mod non_float
 end
 [%%expect{|
-module M : sig type t end
+module M : sig type t : value mod non_float end
 |}]
 
 (*********************************)
@@ -1721,8 +1721,8 @@ Error: This expression has type "int t" but an expression was expected of type
 (*********************************)
 (* Test 17: extensible variants *)
 
-(* The best kind an extensible variant can get is [value] *)
-type extensible : value = ..
+(* The best kind an extensible variant can get is [value mod non_float] *)
+type extensible : value mod non_float = ..
 [%%expect{|
 type extensible = ..
 |}]
@@ -1731,8 +1731,8 @@ type extensible = ..
 module M : sig
   type t : immediate with extensible
 end = struct
-  type t
+  type t : value mod non_float
 end
 [%%expect{|
-module M : sig type t end
+module M : sig type t : value mod non_float end
 |}]

testsuite/tests/typing-jkind-bounds/composite.ml

@@ -632,7 +632,7 @@ Line 1, characters 0-54:
 1 | type ('a : immutable_data) t = Flat | Nested of 'a t t
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error:
-       The kind of 'a t is value
+       The kind of 'a t is value mod non_float
          because it's a boxed variant type.
        But the kind of 'a t must be a subkind of immutable_data
          because of the annotation on 'a in the declaration of the type t.

testsuite/tests/typing-jkind-bounds/modalities.ml

@@ -146,4 +146,5 @@ Error: This expression has type "(string -> string) t"
 
        The first mode-crosses less than the second along:
          nullability: mod non_null with string -> string ≰ mod non_null
+         separability: mod non_float with string -> string ≰ mod separable
 |}]

testsuite/tests/typing-jkind-bounds/predef.ml

@@ -94,7 +94,7 @@ Line 1, characters 14-35:
                   ^^^^^^^^^^^^^^^^^^^^^
 Error: This type "(unit -> unit) option" should be an instance of type
          "('a : value mod portable)"
-       The kind of (unit -> unit) option is value mod immutable
+       The kind of (unit -> unit) option is value mod immutable non_float
          because it's a boxed variant type.
        But the kind of (unit -> unit) option must be a subkind of
          value mod portable
@@ -312,7 +312,7 @@ Line 1, characters 14-33:
                   ^^^^^^^^^^^^^^^^^^^
 Error: This type "(unit -> unit) list" should be an instance of type
          "('a : value mod portable)"
-       The kind of (unit -> unit) list is value mod immutable
+       The kind of (unit -> unit) list is value mod immutable non_float
          because it's a boxed variant type.
        But the kind of (unit -> unit) list must be a subkind of
          value mod portable
@@ -523,7 +523,7 @@ Line 1, characters 14-35:
                   ^^^^^^^^^^^^^^^^^^^^^
 Error: This type "(unit -> unit) iarray" should be an instance of type
          "('a : value mod portable)"
-       The kind of (unit -> unit) iarray is value mod immutable
+       The kind of (unit -> unit) iarray is value mod immutable non_float
          because it is the primitive value type iarray.
        But the kind of (unit -> unit) iarray must be a subkind of
          value mod portable

testsuite/tests/typing-jkind-bounds/printing.ml

@@ -201,7 +201,7 @@ Line 3, characters 11-25:
                ^^^^^^^^^^^^^^
 Error: This type "(int -> int) u" should be an instance of type
          "('a : immutable_data)"
-       The kind of (int -> int) u is value mod portable immutable
+       The kind of (int -> int) u is value mod portable immutable non_float
          because of the definition of u at line 1, characters 0-33.
        But the kind of (int -> int) u must be a subkind of immutable_data
          because of the definition of t at line 2, characters 0-28.

testsuite/tests/typing-jkind-bounds/records.ml

@@ -156,7 +156,7 @@ type t : immutable_data = { x : unit -> unit }
 Line 1, characters 0-46:
 1 | type t : immutable_data = { x : unit -> unit }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value mod immutable
+Error: The kind of type "t" is value mod immutable non_float
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of immutable_data
          because of the annotation on the declaration of the type t.
@@ -189,7 +189,7 @@ type t : mutable_data = { x : unit -> unit }
 Line 1, characters 0-44:
 1 | type t : mutable_data = { x : unit -> unit }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value mod immutable
+Error: The kind of type "t" is value mod immutable non_float
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of mutable_data
          because of the annotation on the declaration of the type t.
@@ -285,7 +285,7 @@ type 'a t : immutable_data with 'a = { x : 'a -> 'a }
 Line 1, characters 0-53:
 1 | type 'a t : immutable_data with 'a = { x : 'a -> 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value mod immutable
+Error: The kind of type "t" is value mod immutable non_float
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of immutable_data with 'a
          because of the annotation on the declaration of the type t.
@@ -625,7 +625,7 @@ Line 1, characters 24-28:
                             ^^^^
 Error: This expression has type "(unit -> unit) t"
        but an expression was expected of type "('a : value mod portable)"
-       The kind of (unit -> unit) t is value mod immutable
+       The kind of (unit -> unit) t is value mod immutable non_float
          because of the definition of t at line 1, characters 0-22.
        But the kind of (unit -> unit) t must be a subkind of
          value mod portable
@@ -650,7 +650,7 @@ Line 1, characters 24-28:
                             ^^^^
 Error: This expression has type "(unit -> unit) t"
        but an expression was expected of type "('a : value mod external_)"
-       The kind of (unit -> unit) t is value mod immutable
+       The kind of (unit -> unit) t is value mod immutable non_float
          because of the definition of t at line 1, characters 0-22.
        But the kind of (unit -> unit) t must be a subkind of
          value mod external_
@@ -745,7 +745,7 @@ Line 1, characters 14-30:
                   ^^^^^^^^^^^^^^^^
 Error: This type "(unit -> unit) t" should be an instance of type
          "('a : value mod portable)"
-       The kind of (unit -> unit) t is value mod immutable
+       The kind of (unit -> unit) t is value mod immutable non_float
          because of the definition of t at line 1, characters 0-22.
        But the kind of (unit -> unit) t must be a subkind of
          value mod portable

testsuite/tests/typing-jkind-bounds/subsumption/basics.ml

@@ -276,7 +276,7 @@ type t
 Line 2, characters 0-44:
 2 | type u : immutable_data with t = [`foo of t]
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "[ `foo of t ]" is value
+Error: The kind of type "[ `foo of t ]" is value mod non_float
          because it's a polymorphic variant type.
        But the kind of type "[ `foo of t ]" must be a subkind of immutable_data
          with t

testsuite/tests/typing-jkind-bounds/variants.ml

@@ -160,7 +160,7 @@ type t : immutable_data = Foo of (unit -> unit)
 Line 1, characters 0-47:
 1 | type t : immutable_data = Foo of (unit -> unit)
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value mod immutable
+Error: The kind of type "t" is value mod immutable non_float
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of immutable_data
          because of the annotation on the declaration of the type t.
@@ -193,7 +193,7 @@ type t : mutable_data = Foo of { x : unit -> unit }
 Line 1, characters 0-51:
 1 | type t : mutable_data = Foo of { x : unit -> unit }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value mod immutable
+Error: The kind of type "t" is value mod immutable non_float
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of mutable_data
          because of the annotation on the declaration of the type t.
@@ -289,7 +289,7 @@ type 'a t : immutable_data with 'a = Foo of { x : 'a -> 'a }
 Line 1, characters 0-60:
 1 | type 'a t : immutable_data with 'a = Foo of { x : 'a -> 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value mod immutable
+Error: The kind of type "t" is value mod immutable non_float
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of immutable_data with 'a
          because of the annotation on the declaration of the type t.
@@ -628,7 +628,7 @@ Line 1, characters 24-28:
                             ^^^^
 Error: This expression has type "(unit -> unit) t"
        but an expression was expected of type "('a : value mod portable)"
-       The kind of (unit -> unit) t is value mod immutable
+       The kind of (unit -> unit) t is value mod immutable non_float
          because of the definition of t at line 1, characters 0-21.
        But the kind of (unit -> unit) t must be a subkind of
          value mod portable
@@ -653,7 +653,7 @@ Line 1, characters 24-28:
                             ^^^^
 Error: This expression has type "(unit -> unit) t"
        but an expression was expected of type "('a : value mod external_)"
-       The kind of (unit -> unit) t is value mod immutable
+       The kind of (unit -> unit) t is value mod immutable non_float
          because of the definition of t at line 1, characters 0-21.
        But the kind of (unit -> unit) t must be a subkind of
          value mod external_
@@ -748,7 +748,7 @@ Line 1, characters 14-30:
                   ^^^^^^^^^^^^^^^^
 Error: This type "(unit -> unit) t" should be an instance of type
          "('a : value mod portable)"
-       The kind of (unit -> unit) t is value mod immutable
+       The kind of (unit -> unit) t is value mod immutable non_float
          because of the definition of t at line 1, characters 0-21.
        But the kind of (unit -> unit) t must be a subkind of
          value mod portable

testsuite/tests/typing-jkind-bounds/with_basics.ml

@@ -660,11 +660,11 @@ type t = Immutable.t
 module Value = F(struct type t end)
 type t : immutable_data = Value.t
 [%%expect {|
-module Value : sig type t end
+module Value : sig type t : value mod non_float end
 Line 2, characters 0-33:
 2 | type t : immutable_data = Value.t
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "Value.t" is value
+Error: The kind of type "Value.t" is value mod non_float
          because of the definition of t at line 2, characters 2-34.
        But the kind of type "Value.t" must be a subkind of immutable_data
          because of the definition of t at line 2, characters 0-33.