generic Tvar should have fixed jkind

ocaml/testsuite/tests/typing-layouts-bits32/basics.ml

@@ -300,7 +300,7 @@ Line 1, characters 31-45:
 Error: This type signature for x is not a value type.
        The layout of type 'a t_bits32_id is bits32, because
          of the definition of t_bits32_id at line 2, characters 0-35.
-       But the layout of type 'a t_bits32_id must overlap with value, because
+       But the layout of type 'a t_bits32_id must be a sublayout of value, because
          it's the type of something stored in a module structure.
 |}];;
 

ocaml/testsuite/tests/typing-layouts-bits64/basics.ml

@@ -300,7 +300,7 @@ Line 1, characters 31-45:
 Error: This type signature for x is not a value type.
        The layout of type 'a t_bits64_id is bits64, because
          of the definition of t_bits64_id at line 2, characters 0-35.
-       But the layout of type 'a t_bits64_id must overlap with value, because
+       But the layout of type 'a t_bits64_id must be a sublayout of value, because
          it's the type of something stored in a module structure.
 |}];;
 

ocaml/testsuite/tests/typing-layouts-err-msg/concrete.ml

@@ -135,7 +135,7 @@ external eq : t_any -> 'a -> bool = "%equal"
 Line 1, characters 14-19:
 1 | external eq : t_any -> 'a -> bool = "%equal"
                   ^^^^^
-Error: External types must have a representable layout.
+Error: Types in an external must have a representable layout.
        The layout of t_any is any, because
          of the definition of t_any at line 1, characters 0-16.
        But the layout of t_any must be representable, because
@@ -149,7 +149,7 @@ external eq : 'a -> 'a -> t_any = "%equal"
 Line 1, characters 26-31:
 1 | external eq : 'a -> 'a -> t_any = "%equal"
                               ^^^^^
-Error: External types must have a representable layout.
+Error: Types in an external must have a representable layout.
        The layout of t_any is any, because
          of the definition of t_any at line 1, characters 0-16.
        But the layout of t_any must be representable, because

ocaml/testsuite/tests/typing-layouts-float64/basics.ml

@@ -336,7 +336,7 @@ Line 1, characters 31-46:
 Error: This type signature for x is not a value type.
        The layout of type 'a t_float64_id is float64, because
          of the definition of t_float64_id at line 2, characters 0-37.
-       But the layout of type 'a t_float64_id must overlap with value, because
+       But the layout of type 'a t_float64_id must be a sublayout of value, because
          it's the type of something stored in a module structure.
 |}];;
 

ocaml/testsuite/tests/typing-layouts-word/basics.ml

@@ -300,7 +300,7 @@ Line 1, characters 31-43:
 Error: This type signature for x is not a value type.
        The layout of type 'a t_word_id is word, because
          of the definition of t_word_id at line 2, characters 0-31.
-       But the layout of type 'a t_word_id must overlap with value, because
+       But the layout of type 'a t_word_id must be a sublayout of value, because
          it's the type of something stored in a module structure.
 |}];;
 

ocaml/testsuite/tests/typing-layouts/basics.ml

@@ -598,7 +598,14 @@ Error: Layout void is more experimental than allowed by the enabled layouts exte
 
 type ('a : any) any4 = Any4 of 'a
 [%%expect{|
-type 'a any4 = Any4 of 'a
+Line 1, characters 23-33:
+1 | type ('a : any) any4 = Any4 of 'a
+                           ^^^^^^^^^^
+Error: Constructor argument types must have a representable layout.
+       The layout of 'a is any, because
+         of the annotation on 'a in the declaration of the type any4.
+       But the layout of 'a must be representable, because
+         it's the type of a constructor field.
 |}];;
 
 (************************************************************)
@@ -1816,6 +1823,32 @@ Error: This type signature for foo33 is not a value type.
          it's the type of something stored in a module structure.
 |}]
 
+external foo44 : ('a : any). 'a -> unit = "foo44";;
+
+[%%expect{|
+Line 1, characters 29-31:
+1 | external foo44 : ('a : any). 'a -> unit = "foo44";;
+                                 ^^
+Error: Types in an external must have a representable layout.
+       The layout of 'a is any, because
+         of the annotation on the universal variable 'a.
+       But the layout of 'a must be representable, because
+         it's the type of an argument in an external declaration.
+|}]
+
+external foo55 : ('a : any). unit -> 'a = "foo55";;
+
+[%%expect{|
+Line 1, characters 37-39:
+1 | external foo55 : ('a : any). unit -> 'a = "foo55";;
+                                         ^^
+Error: Types in an external must have a representable layout.
+       The layout of 'a is any, because
+         of the annotation on the universal variable 'a.
+       But the layout of 'a must be representable, because
+         it's the type of the result of an external declaration.
+|}]
+
 (****************************************************)
 (* Test 34: Layout clash in polymorphic record type *)
 
@@ -2342,17 +2375,11 @@ and 'a t2 = 'a
 Line 2, characters 0-14:
 2 | and 'a t2 = 'a
     ^^^^^^^^^^^^^^
-Error: Layout mismatch in checking consistency of mutually recursive groups.
-       This is most often caused by the fact that type inference is not
-       clever enough to propagate layouts through variables in different
-       declarations. It is also not clever enough to produce a good error
-       message, so we'll say this instead:
-         The layout of 'a t2 is value, because
-           it instantiates an unannotated type parameter of t2, defaulted to layout value.
-         But the layout of 'a t2 must be a sublayout of immediate, because
-           of the annotation on the wildcard _ at line 1, characters 28-37.
-       A good next step is to add a layout annotation on a parameter to
-       the declaration where this error is reported.
+Error:
+       The layout of 'a t2 is value, because
+         it instantiates an unannotated type parameter of t2, defaulted to layout value.
+       But the layout of 'a t2 must be a sublayout of immediate, because
+         of the annotation on the wildcard _ at line 1, characters 28-37.
 |}]
 
 (* This example is unfortunately rejected as a consequence of the fix for the
@@ -2366,17 +2393,11 @@ and 'a t2 = 'a
 Line 2, characters 0-14:
 2 | and 'a t2 = 'a
     ^^^^^^^^^^^^^^
-Error: Layout mismatch in checking consistency of mutually recursive groups.
-       This is most often caused by the fact that type inference is not
-       clever enough to propagate layouts through variables in different
-       declarations. It is also not clever enough to produce a good error
-       message, so we'll say this instead:
-         The layout of 'a t2/2 is value, because
-           it instantiates an unannotated type parameter of t2, defaulted to layout value.
-         But the layout of 'a t2/2 must be a sublayout of immediate, because
-           of the annotation on the wildcard _ at line 1, characters 27-36.
-       A good next step is to add a layout annotation on a parameter to
-       the declaration where this error is reported.
+Error:
+       The layout of 'a t2 is value, because
+         it instantiates an unannotated type parameter of t2, defaulted to layout value.
+       But the layout of 'a t2 must be a sublayout of immediate, because
+         of the annotation on the wildcard _ at line 1, characters 27-36.
 |}]
 
 (* This one also unfortunately rejected for the same reason. *)
@@ -2387,15 +2408,9 @@ and 'a t2 = 'a
 Line 2, characters 0-14:
 2 | and 'a t2 = 'a
     ^^^^^^^^^^^^^^
-Error: Layout mismatch in checking consistency of mutually recursive groups.
-       This is most often caused by the fact that type inference is not
-       clever enough to propagate layouts through variables in different
-       declarations. It is also not clever enough to produce a good error
-       message, so we'll say this instead:
-         The layout of 'a t2/3 is value, because
-           it instantiates an unannotated type parameter of t2, defaulted to layout value.
-         But the layout of 'a t2/3 must be a sublayout of immediate, because
-           of the annotation on the wildcard _ at line 1, characters 25-34.
-       A good next step is to add a layout annotation on a parameter to
-       the declaration where this error is reported.
+Error:
+       The layout of 'a t2 is value, because
+         it instantiates an unannotated type parameter of t2, defaulted to layout value.
+       But the layout of 'a t2 must be a sublayout of immediate, because
+         of the annotation on the wildcard _ at line 1, characters 25-34.
 |}]

ocaml/testsuite/tests/typing-layouts/basics_alpha.ml

@@ -355,7 +355,6 @@ and ('a : any) t4
    moved to [basics_beta.ml]. *)
 
 type ('a : void) void5 = Void5  of 'a
-type ('a : any) any5 = Any5 of 'a
 
 let id5 : 'a void5 -> 'a void5 = function
   | Void5 x -> Void5 x
@@ -377,9 +376,8 @@ let id5 : 'a void5 -> 'a void5 = function
 
 [%%expect{|
 type ('a : void) void5 = Void5 of 'a
-type 'a any5 = Any5 of 'a
-Line 5, characters 15-22:
-5 |   | Void5 x -> Void5 x
+Line 4, characters 15-22:
+4 |   | Void5 x -> Void5 x
                    ^^^^^^^
 Error: Non-value detected in [value_kind].
        Please report this error to the Jane Street compilers team.
@@ -402,16 +400,16 @@ Error: This type int should be an instance of type ('a : void)
          of the definition of void5 at line 1, characters 0-37.
 |}];;
 
-let h5' (x : int any5) = Void5 x
+let h5' (x : int) = Void5 x
 [%%expect{|
-Line 1, characters 31-32:
-1 | let h5' (x : int any5) = Void5 x
-                                   ^
-Error: This expression has type int any5
-       but an expression was expected of type ('a : void)
-       The layout of int any5 is value, because
-         of the definition of any5 at line 2, characters 0-33.
-       But the layout of int any5 must be a sublayout of void, because
+Line 1, characters 26-27:
+1 | let h5' (x : int) = Void5 x
+                              ^
+Error: This expression has type int but an expression was expected of type
+         ('a : void)
+       The layout of int is immediate, because
+         it is the primitive immediate type int.
+       But the layout of int must be a sublayout of void, because
          of the definition of void5 at line 1, characters 0-37.
 |}];;
 

ocaml/typing/ctype.ml

@@ -1998,6 +1998,16 @@ let rec estimate_type_jkind env ty =
       if tvariant_not_immediate row
       then Jkind (value ~why:Polymorphic_variant)
       else Jkind (immediate ~why:Immediate_polymorphic_variant)
+  | Tvar { jkind } when get_level ty = generic_level ->
+    (* Once a Tvar gets generalized with a jkind, it should be considered
+       as fixed (similar to the Tunivar case below).
+
+       This notably prevents [constrain_type_jkind] from changing layout
+       [any] to a sort or changing the externality once the Tvar gets
+       generalized.
+
+       This, however, still allows sort variables to get instantiated. *)
+    Jkind jkind
   | Tvar { jkind } -> TyVar (jkind, ty)
   | Tarrow _ -> Jkind (value ~why:Arrow)
   | Ttuple _ -> Jkind (value ~why:Tuple)

ocaml/typing/typedecl.ml

@@ -2961,12 +2961,12 @@ let report_error ppf = function
   | Jkind_sort {kloc; typ; err} ->
     let s =
       match kloc with
-      | Cstr_tuple -> "Constructor argument"
-      | Record -> "Record element"
-      | Unboxed_record -> "Unboxed record element"
-      | External -> "External"
+      | Cstr_tuple -> "Constructor argument types"
+      | Record -> "Record element types"
+      | Unboxed_record -> "Unboxed record element types"
+      | External -> "Types in an external"
     in
-    fprintf ppf "@[%s types must have a representable layout.@ %a@]" s
+    fprintf ppf "@[%s must have a representable layout.@ %a@]" s
       (Jkind.Violation.report_with_offender
          ~offender:(fun ppf -> Printtyp.type_expr ppf typ)) err
   | Jkind_empty_record ->