Rework jkind default (#2158)

* extend policy to control ty var jkind init

* annotation on type vars should be upper bounds

* proper jkind reason

* sort init rhs of constraints for backward compatibility

* add comment&rename to jkind_initialization_choice

* refactor policy

* comment about transl_simple_type_delayed

* use Any more in typeclass

* add new_var_jkind param and thread it through

* use Any for with constraint

* add note

* more tests

* more tests

Author: alanechang

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

@@ -49,19 +49,103 @@ module type S1 = sig val f : t_any -> int end
 module type S1 = sig
   type t : any
 
-  type ('a : any) s = ('a : any) -> int constraint ('a : any) = t
+  type ('a : any) s = 'a -> int constraint 'a = t
+
+  type q = t s
+end;;
+[%%expect{|
+module type S1 =
+  sig type t : any type 'a s = 'a -> int constraint 'a = t type q = t s end
+|}]
+
+module type S1 = sig
+  type t : any
+
+  type ('a : any) s = int -> 'a constraint 'a = t
+
+  type q = t s
+end;;
+[%%expect{|
+module type S1 =
+  sig type t : any type 'a s = int -> 'a constraint 'a = t type q = t s end
+|}]
+
+module type S1 = sig
+  type t : any
+
+  type ('a : any) s = { a: 'a -> 'a }
+
+  type q = t s
+end;;
+[%%expect{|
+module type S1 =
+  sig type t : any type ('a : any) s = { a : 'a -> 'a; } type q = t s end
+|}]
+
+module type S1 = sig
+  type t : any
+
+  type ('a : any) s = A of ('a -> 'a)
+
+  type q = t s
 end;;
 [%%expect{|
-module type S1 = sig type t : any type 'a s = 'a -> int constraint 'a = t end
+module type S1 =
+  sig type t : any type ('a : any) s = A of ('a -> 'a) type q = t s end
 |}]
 
 module type S1 = sig
   type t : any
 
-  type ('a : any) s = int -> ('a : any) constraint ('a : any) = t
+  type ('a : any) s = A of { a: 'a -> 'a }
+
+  type q = t s
 end;;
 [%%expect{|
-module type S1 = sig type t : any type 'a s = int -> 'a constraint 'a = t end
+module type S1 =
+  sig
+    type t : any
+    type ('a : any) s = A of { a : 'a -> 'a; }
+    type q = t s
+  end
+|}]
+
+module S1 = struct
+  type t : any
+
+  type ('a : any) s = A : { a: 'a -> 'b -> 'a } -> 'a s
+
+  type q = t s
+
+  let f () = A {a = (fun x y -> x)}
+end;;
+[%%expect{|
+module S1 :
+  sig
+    type t : any
+    type ('a : any) s = A : { a : 'a -> 'b -> 'a; } -> 'a s
+    type q = t s
+    val f : unit -> 'a s
+  end
+|}]
+
+module S1 = struct
+  type t : any
+
+  type ('a : any) s = A : ('a -> 'b -> 'a) -> 'a s
+
+  type q = t s
+
+  let f () = A (fun x y -> x)
+end
+[%%expect{|
+module S1 :
+  sig
+    type t : any
+    type ('a : any) s = A : ('a -> 'b -> 'a) -> 'a s
+    type q = t s
+    val f : unit -> 'a s
+  end
 |}]
 
 module type S1 = sig
@@ -289,7 +373,7 @@ Error:
 |}]
 (* CR layouts v2.9: improve error, which requires layout histories *)
 
-type ('a : any) t4 = ('a : any)
+type ('a : any) t4 = 'a
 and s4 = string t4;;
 [%%expect{|
 type ('a : any) t4 = 'a
@@ -1100,7 +1184,7 @@ val f : ('a : float64). unit -> 'a t22f t22f = <fun>
 
 (* CR layouts v5: bring void version here from layouts_alpha *)
 
-type (_ : any, _ : any) eq = Refl :  ('a : any). ('a, 'a) eq
+type (_ : any, _ : any) eq = Refl : ('a : any). ('a, 'a) eq
 
 module Mf : sig
   type t_float64 : float64
@@ -1207,7 +1291,7 @@ let q () =
   ()
 
 [%%expect{|
-val ( let* ) : 'a -> (t_float64 -> 'b) -> unit = <fun>
+val ( let* ) : ('b : any) 'a. 'a -> (t_float64 -> 'b) -> unit = <fun>
 val q : unit -> unit = <fun>
 |}]
 
@@ -1219,7 +1303,7 @@ let q () =
   assert false
 
 [%%expect{|
-val ( let* ) : 'a -> ('b -> t_float64) -> unit = <fun>
+val ( let* ) : ('b : any) 'a. 'a -> ('b -> t_float64) -> unit = <fun>
 val q : unit -> unit = <fun>
 |}]
 

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

@@ -45,7 +45,7 @@ module type S1 = sig val f : t_any -> int end
 module type S1 = sig
   type t : any
 
-  type ('a : any) s = ('a : any) -> int constraint ('a : any) = t
+  type ('a : any) s = 'a -> int constraint 'a = t
 end;;
 [%%expect{|
 module type S1 = sig type t : any type 'a s = 'a -> int constraint 'a = t end
@@ -54,7 +54,7 @@ module type S1 = sig type t : any type 'a s = 'a -> int constraint 'a = t end
 module type S1 = sig
   type t : any
 
-  type ('a : any) s = int -> ('a : any) constraint ('a : any) = t
+  type ('a : any) s = int -> 'a constraint 'a = t
 end;;
 [%%expect{|
 module type S1 = sig type t : any type 'a s = int -> 'a constraint 'a = t end
@@ -301,7 +301,7 @@ Error:
 |}]
 (* CR layouts v2.9: improve error, which will require jkind histories *)
 
-type ('a : any) t4 = ('a : any)
+type ('a : any) t4 = 'a
 and s4 = string t4;;
 [%%expect{|
 type ('a : any) t4 = 'a
@@ -1321,7 +1321,7 @@ let q () =
   ()
 
 [%%expect{|
-val ( let* ) : 'a -> (t_float64 -> 'b) -> unit = <fun>
+val ( let* ) : ('b : any) 'a. 'a -> (t_float64 -> 'b) -> unit = <fun>
 val q : unit -> unit = <fun>
 |}]
 
@@ -1347,7 +1347,7 @@ let q () =
   assert false
 
 [%%expect{|
-val ( let* ) : 'a -> ('b -> t_float64) -> unit = <fun>
+val ( let* ) : ('b : any) 'a. 'a -> ('b -> t_float64) -> unit = <fun>
 val q : unit -> unit = <fun>
 |}]
 

ocaml/testsuite/tests/typing-local/local.ml

@@ -1023,7 +1023,8 @@ val catch : (unit -> local_ string) -> string * string = <fun>
 (* same, but this time the function is allowed to return its argument *)
 let use_locally (f : local_ 'a -> local_ 'a) : local_ 'a -> local_ 'a = f
 [%%expect{|
-val use_locally : (local_ 'a -> local_ 'a) -> local_ 'a -> local_ 'a = <fun>
+val use_locally :
+  ('a : any). (local_ 'a -> local_ 'a) -> local_ 'a -> local_ 'a = <fun>
 |}]
 
 let loc = ((fun x -> local_ x) : local_ int -> local_ int)

ocaml/testsuite/tests/typing-poly/poly.ml

@@ -1795,10 +1795,10 @@ external reraise : exn -> 'a = "%reraise"
 module M :
   functor () ->
     sig
-      val f : 'a -> 'a
-      val g : 'a -> 'a
-      val h : 'a -> 'a
-      val i : 'a -> 'a
+      val f : ('a : any). 'a -> 'a
+      val g : ('a : any). 'a -> 'a
+      val h : ('a : any). 'a -> 'a
+      val i : ('a : any). 'a -> 'a
     end
 |}]
 

ocaml/typing/jkind.ml

@@ -629,6 +629,8 @@ type any_creation_reason =
   | Dummy_jkind
   | Type_expression_call
   | Inside_of_Tarrow
+  | Wildcard
+  | Unification_var
 
 type float64_creation_reason = Primitive of Ident.t
 
@@ -988,6 +990,8 @@ end = struct
     | Type_expression_call ->
       fprintf ppf "a call to [type_expression] via the ocaml API"
     | Inside_of_Tarrow -> fprintf ppf "argument or result of a Tarrow"
+    | Wildcard -> fprintf ppf "a _ in a type"
+    | Unification_var -> fprintf ppf "a fresh unification variable"
 
   let format_immediate_creation_reason ppf : immediate_creation_reason -> _ =
     function
@@ -1359,6 +1363,8 @@ module Debug_printers = struct
     | Dummy_jkind -> fprintf ppf "Dummy_jkind"
     | Type_expression_call -> fprintf ppf "Type_expression_call"
     | Inside_of_Tarrow -> fprintf ppf "Inside_of_Tarrow"
+    | Wildcard -> fprintf ppf "Wildcard"
+    | Unification_var -> fprintf ppf "Unification_var"
 
   let immediate_creation_reason ppf : immediate_creation_reason -> _ = function
     | Empty_record -> fprintf ppf "Empty_record"

ocaml/typing/jkind.mli

@@ -256,6 +256,8 @@ type any_creation_reason =
        unified to correct levels *)
   | Type_expression_call
   | Inside_of_Tarrow
+  | Wildcard
+  | Unification_var
 
 type float64_creation_reason = Primitive of Ident.t
 

ocaml/typing/typeclass.ml

@@ -261,9 +261,9 @@ let unify_delayed_method_type loc env label ty expected_ty=
       raise(Error(loc, env, Field_type_mismatch ("method", label, trace)))
 
 let type_constraint val_env sty sty' loc =
-  let cty  = transl_simple_type val_env ~closed:false Alloc.Const.legacy sty in
+  let cty  = transl_simple_type ~new_var_jkind:Any val_env ~closed:false Alloc.Const.legacy sty in
   let ty = cty.ctyp_type in
-  let cty' = transl_simple_type val_env ~closed:false Alloc.Const.legacy sty' in
+  let cty' = transl_simple_type ~new_var_jkind:Sort val_env ~closed:false Alloc.Const.legacy sty' in
   let ty' = cty'.ctyp_type in
   begin
     try Ctype.unify val_env ty ty' with Ctype.Unify err ->
@@ -308,7 +308,7 @@ let rec class_type_field env sign self_scope ctf =
   | Pctf_val ({txt=lab}, mut, virt, sty) ->
       mkctf_with_attrs
         (fun () ->
-          let cty = transl_simple_type env ~closed:false Alloc.Const.legacy sty in
+          let cty = transl_simple_type ~new_var_jkind:Sort env ~closed:false Alloc.Const.legacy sty in
           let ty = cty.ctyp_type in
           begin match
             Ctype.constrain_type_jkind
@@ -343,7 +343,7 @@ let rec class_type_field env sign self_scope ctf =
                  ) :: !delayed_meth_specs;
                Tctf_method (lab, priv, virt, returned_cty)
            | _ ->
-               let cty = transl_simple_type env ~closed:false Alloc.Const.legacy sty in
+               let cty = transl_simple_type ~new_var_jkind:Any env ~closed:false Alloc.Const.legacy sty in
                let ty = cty.ctyp_type in
                add_method loc env lab priv virt ty sign;
                Tctf_method (lab, priv, virt, cty))
@@ -367,7 +367,7 @@ and class_signature virt env pcsig self_scope loc =
   (* Introduce a dummy method preventing self type from being closed. *)
   Ctype.add_dummy_method env ~scope:self_scope sign;
 
-  let self_cty = transl_simple_type env ~closed:false Alloc.Const.legacy sty in
+  let self_cty = transl_simple_type ~new_var_jkind:Any env ~closed:false Alloc.Const.legacy sty in
   let self_type = self_cty.ctyp_type in
   begin try
     Ctype.unify env self_type sign.csig_self
@@ -417,7 +417,7 @@ and class_type_aux env virt self_scope scty =
                                                    List.length styl)));
       let ctys = List.map2
         (fun sty ty ->
-          let cty' = transl_simple_type env ~closed:false Alloc.Const.legacy sty in
+          let cty' = transl_simple_type ~new_var_jkind:Any env ~closed:false Alloc.Const.legacy sty in
           let ty' = cty'.ctyp_type in
           begin
            try Ctype.unify env ty' ty with Ctype.Unify err ->
@@ -437,7 +437,7 @@ and class_type_aux env virt self_scope scty =
       cltyp (Tcty_signature clsig) typ
 
   | Pcty_arrow (l, sty, scty) ->
-      let cty = transl_simple_type env ~closed:false Alloc.Const.legacy sty in
+      let cty = transl_simple_type ~new_var_jkind:Any env ~closed:false Alloc.Const.legacy sty in
       let ty = cty.ctyp_type in
       let ty =
         if Btype.is_optional l
@@ -670,7 +670,7 @@ let rec class_field_first_pass self_loc cl_num sign self_scope acc cf =
         (fun () ->
            let cty =
              Ctype.with_local_level_if_principal
-               (fun () -> Typetexp.transl_simple_type val_env
+               (fun () -> Typetexp.transl_simple_type ~new_var_jkind:Any val_env
                             ~closed:false Alloc.Const.legacy styp)
                ~post:(fun cty -> Ctype.generalize_structure cty.ctyp_type)
            in
@@ -760,7 +760,7 @@ let rec class_field_first_pass self_loc cl_num sign self_scope acc cf =
       with_attrs
         (fun () ->
            let sty = Ast_helper.Typ.force_poly sty in
-           let cty = transl_simple_type val_env ~closed:false Alloc.Const.legacy sty in
+           let cty = transl_simple_type ~new_var_jkind:Any val_env ~closed:false Alloc.Const.legacy sty in
            let ty = cty.ctyp_type in
            add_method loc val_env label.txt priv Virtual ty sign;
            let field =
@@ -800,7 +800,7 @@ let rec class_field_first_pass self_loc cl_num sign self_scope acc cf =
              | Some sty ->
                  let sty = Ast_helper.Typ.force_poly sty in
                  let cty' =
-                   Typetexp.transl_simple_type val_env ~closed:false Alloc.Const.legacy sty
+                   Typetexp.transl_simple_type ~new_var_jkind:Any val_env ~closed:false Alloc.Const.legacy sty
                  in
                  cty'.ctyp_type
            in
@@ -1118,7 +1118,7 @@ and class_expr_aux cl_num val_env met_env virt self_scope scl =
       if Path.same decl.cty_path unbound_class then
         raise(Error(scl.pcl_loc, val_env, Unbound_class_2 lid.txt));
       let tyl = List.map
-          (fun sty -> transl_simple_type val_env ~closed:false Alloc.Const.legacy sty)
+          (fun sty -> transl_simple_type ~new_var_jkind:Any val_env ~closed:false Alloc.Const.legacy sty)
           styl
       in
       let (params, clty) =

ocaml/typing/typecore.ml

@@ -4006,7 +4006,7 @@ let rec approx_type env sty =
           (* Polymorphic types will only unify with types that match all of their
            polymorphic parts, so we need to fully translate the type here
            unlike in the monomorphic case *)
-          Typetexp.transl_simple_type env ~closed:false arg_mode arg_sty
+          Typetexp.transl_simple_type ~new_var_jkind:Any env ~closed:false arg_mode arg_sty
         in
         let ret = approx_type env sty in
         let marg = Alloc.of_const arg_mode in
@@ -4061,7 +4061,7 @@ let type_pattern_approx env spat ty_expected =
         mode_annots_or_default mode_annots ~default:Alloc.Const.legacy
       in
       let ty_pat =
-        Typetexp.transl_simple_type env ~closed:false arg_type_mode sty
+        Typetexp.transl_simple_type ~new_var_jkind:Any env ~closed:false arg_type_mode sty
       in
       begin try unify env ty_pat.ctyp_type ty_expected with Unify trace ->
         raise(Error(spat.ppat_loc, env, Pattern_type_clash(trace, None)))
@@ -5678,7 +5678,7 @@ and type_expect_
           let type_mode =
             mode_annots_or_default mode_annots ~default:Alloc.Const.legacy
           in
-          Typetexp.transl_simple_type env ~closed:false type_mode sty
+          Typetexp.transl_simple_type ~new_var_jkind:Any env ~closed:false type_mode sty
         end
         ~post:(fun cty -> generalize_structure cty.ctyp_type)
       in
@@ -6013,7 +6013,7 @@ and type_expect_
             | Some sty ->
                 let sty = Ast_helper.Typ.force_poly sty in
                 let cty =
-                  Typetexp.transl_simple_type env ~closed:false
+                  Typetexp.transl_simple_type ~new_var_jkind:Any env ~closed:false
                     Alloc.Const.legacy sty
                 in
                 cty.ctyp_type, Some cty