Skip to content

Move layout restriction from -> to fun #2107

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 28 commits into from
Dec 27, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
ef83626
wip
alanechang Nov 29, 2023
b0f9372
change Wildcard and Unification_var to sort vars
alanechang Nov 29, 2023
e8bedff
test changes
alanechang Nov 29, 2023
eac5307
more tests
alanechang Nov 30, 2023
b0cc09f
fix test
alanechang Nov 30, 2023
b1f8c65
test changes
alanechang Nov 30, 2023
9306375
Rework jkind default (#2158)
alanechang Dec 18, 2023
1fab504
rebase over type var print order change
alanechang Dec 19, 2023
81a75ca
Add a bunch of tests
goldfirere Dec 19, 2023
4262e98
check instead of constrain
alanechang Dec 19, 2023
a885f86
jkind check in unify_univar
alanechang Dec 19, 2023
c006e5e
update test outputs
alanechang Dec 19, 2023
0f8fdf1
change unify_univar to take jkinds
alanechang Dec 19, 2023
de31691
Testing representability of function argument
goldfirere Dec 20, 2023
136dfbb
More tests
goldfirere Dec 21, 2023
e19affc
Yet more tests
goldfirere Dec 21, 2023
7ea22b0
Accept test output
goldfirere Dec 21, 2023
e8c4817
Propagate new test to _alpha
goldfirere Dec 21, 2023
1c2a3e6
More tests, this time about inference
goldfirere Dec 21, 2023
41e8647
add tests to _alpha
alanechang Dec 21, 2023
b57bbb9
small test changes
alanechang Dec 21, 2023
d8b5597
relax approx_type
alanechang Dec 22, 2023
7b4c549
reword history message
alanechang Dec 22, 2023
feea377
add cr for bad error message
alanechang Dec 22, 2023
899010b
fix test
alanechang Dec 22, 2023
0d1034f
rename layout to jkind
alanechang Dec 26, 2023
2b16e4a
add comments about check_type_jkind_exn
alanechang Dec 26, 2023
31bca7e
add comment about unify_univar invariant
alanechang Dec 26, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 11 additions & 12 deletions ocaml/testsuite/tests/typing-layouts/annots.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
;;
Expand Down Expand Up @@ -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 *)
Expand Down
110 changes: 110 additions & 0 deletions ocaml/testsuite/tests/typing-layouts/any_in_types.ml
Original file line number Diff line number Diff line change
@@ -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.)
;;
10 changes: 10 additions & 0 deletions ocaml/testsuite/tests/typing-layouts/any_in_types.reference
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
20.000000
20
20.000000
20
Printing a float#: 1.000000
Printing a int: 1
a
b
c
d
Loading