flambda-backend: Move layout restriction from -> to fun (#2107)

* wip

* change Wildcard and Unification_var to sort vars

* test changes

* more tests

* fix test

* test changes

* 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

* rebase over type var print order change

* Add a bunch of tests

* check instead of constrain

* jkind check in unify_univar

* update test outputs

* change unify_univar to take jkinds

* Testing representability of function argument

* More tests

* Yet more tests

* Accept test output

* Propagate new test to _alpha

* More tests, this time about inference

* add tests to _alpha

* small test changes

* relax approx_type

* reword history message

* add cr for bad error message

* fix test

* rename layout to jkind

* add comments about check_type_jkind_exn

* add comment about unify_univar invariant

---------

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

Author: alanechang

testsuite/tests/typing-layouts/annots.ml

@@ -242,14 +242,15 @@ val f : 'a -> 'a = <fun>
 let f : ('a : any). 'a -> 'a = fun x -> x
 ;;
 [%%expect {|
-Line 1, characters 8-28:
+Line 1, characters 31-41:
 1 | let f : ('a : any). 'a -> 'a = fun x -> x
-            ^^^^^^^^^^^^^^^^^^^^
-Error: The universal type variable 'a was declared to have
-       layout any, but was inferred to have a representable layout.
+                                   ^^^^^^^^^^
+Error: This definition has type 'b -> 'b which is less general than
+         ('a : any). 'a -> 'a
+       'a has layout any, which is not representable.
 |}]
-(* CR layouts v2.5: This error message should change to complain
-   about the [fun x], not the arrow type. *)
+(* CR layouts v2.9: This error message is not great. Check later if layout history
+   is able to improve it. *)
 
 let f : ('a : float64). 'a -> 'a = fun x -> x
 ;;
@@ -401,14 +402,12 @@ val f : ('a : float64). 'a -> 'a = <fun>
 let f : type (a : any). a -> a = fun x -> x
 ;;
 [%%expect {|
-Line 1, characters 24-30:
+Line 1, characters 33-43:
 1 | let f : type (a : any). a -> a = fun x -> x
-                            ^^^^^^
-Error: The universal type variable 'a was declared to have
-       layout any, but was inferred to have a representable layout.
+                                     ^^^^^^^^^^
+Error: Function arguments and returns must be representable.
+       a has layout any, which is not representable.
 |}]
-(* CR layouts v2.5: This error message will change to complain
-   about the fun x, not the arrow type. *)
 
 (**************************************************)
 (* Test 7: Defaulting universal variable to value *)

testsuite/tests/typing-layouts/any_in_types.ml

@@ -0,0 +1,110 @@
+(* TEST
+   flags = "-extension layouts"
+   * native
+   * bytecode
+*)
+
+(* See also Test 10 in modules.ml, which tests for type-checking failures in
+   code that is similar to this. *)
+
+let unbox = Stdlib__Float_u.of_float
+
+module type S = sig
+  type t : any
+
+  val add : t -> t -> t
+  val one : unit -> t
+  val print : (unit -> t) -> unit
+end
+
+(* type substitution *)
+module M1 : S with type t = float# = struct
+  type t = float#
+
+  let add x y = Stdlib__Float_u.add x y
+  let one () = unbox 1.
+  let print f = Printf.printf "Printing a float#: %f\n" (Stdlib__Float_u.to_float (f ()))
+end
+
+module M2 : S with type t = int = struct
+  type t = int
+
+  let add x y = x + y
+  let one () = 1
+  let print f = Printf.printf "Printing a int: %d\n" (f ())
+end
+
+let () = Printf.printf "%f\n" (Stdlib__Float_u.to_float (M1.add (unbox 10.) (unbox 10.)))
+let () = Printf.printf "%d\n" (M2.add 10 10)
+
+(* destructive substitution *)
+module M3 : S with type t := float# = struct
+  let add x y = Stdlib__Float_u.add x y
+  let one () = unbox 1.
+  let print f = Printf.printf "Printing a float#: %f\n" (Stdlib__Float_u.to_float (f ()))
+end
+
+module M4 : S with type t := int = struct
+  let add x y = x + y
+  let one () = 1
+  let print f = Printf.printf "Printing a int: %d\n" (f ())
+end
+
+let () = Printf.printf "%f\n" (Stdlib__Float_u.to_float (M3.add (unbox 10.) (unbox 10.)))
+let () = Printf.printf "%d\n" (M4.add 10 10)
+
+(* functor *)
+module type Q = sig
+  include S
+
+  val print_one : unit -> unit
+end
+
+module Make (M : S) : Q = struct
+  include M
+
+  let print_one () = M.print M.one
+end
+
+module M1' = Make (M1)
+module M2' = Make (M2)
+
+let () = M1'.print_one ()
+let () = M2'.print_one ()
+
+(* edge cases and order of evaluation *)
+let g : type (a : any). unit -> a -> a = fun () -> assert false
+
+let () =
+  try
+    let r =
+      g
+        ()
+        (Printf.printf "a\n";
+         unbox 10.)
+    in
+    Printf.printf "%f\n" (Stdlib__Float_u.to_float r)
+  with
+  | _ -> Printf.printf "b\n"
+;;
+
+let () =
+  try
+    let r =
+      g
+        ()
+        (Printf.printf "c\n";
+         10)
+    in
+    Printf.printf "%d\n" r
+  with
+  | _ -> Printf.printf "d\n"
+;;
+
+(* This should type check *)
+let rec f : type (a : any). unit -> a -> a = fun () -> f ()
+
+let f' () =
+  let _ = f () 10 in
+  f () (unbox 10.)
+;;

testsuite/tests/typing-layouts/any_in_types.reference

@@ -0,0 +1,10 @@
+20.000000
+20
+20.000000
+20
+Printing a float#: 1.000000
+Printing a int: 1
+a
+b
+c
+d