From 9b0d5de625d8cb5c994bceef6e297eca1ee85251 Mon Sep 17 00:00:00 2001 From: Leo White Date: Thu, 17 Aug 2023 14:33:24 +0100 Subject: [PATCH] Allow parameter modes to be relaxed in type_argument --- ocaml/testsuite/tests/typing-local/local.ml | 70 +++++++++++++++---- .../tests/typing-poly/poly_params.ml | 6 +- ocaml/typing/typecore.ml | 9 +-- 3 files changed, 66 insertions(+), 19 deletions(-) diff --git a/ocaml/testsuite/tests/typing-local/local.ml b/ocaml/testsuite/tests/typing-local/local.ml index 71e1bf5f194..2e15833f93c 100644 --- a/ocaml/testsuite/tests/typing-local/local.ml +++ b/ocaml/testsuite/tests/typing-local/local.ml @@ -777,6 +777,45 @@ Line 2, characters 20-45: Error: This function is local-returning, but was expected otherwise |}] +(* + * Modification of parameter modes in argument position + *) + +let use_local (local_ f : _ -> _ -> _) x y = + f x y +let use_global (f : _ -> _ -> _) x y = f x y + +let foo x y = x +. y +let bar (local_ x) (local_ y) = let _ = x +. y in () + +let result = use_local foo 1. 2. +[%%expect{| +val use_local : local_ ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = +val use_global : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = +val foo : float -> float -> float = +val bar : local_ float -> local_ float -> unit = +val result : float = 3. +|}] + +let result = use_local bar 1. 2. +[%%expect{| +val result : unit = () +|}] + +let result = use_global foo 1. 2. +[%%expect{| +val result : float = 3. +|}] + +let result = use_global bar 1. 2. +[%%expect{| +Line 1, characters 24-27: +1 | let result = use_global bar 1. 2. + ^^^ +Error: This expression has type local_ float -> local_ float -> unit + but an expression was expected of type local_ 'a -> ('b -> 'c) +|}] + (* * Closures and context locks @@ -2124,24 +2163,31 @@ let foo f = ignore (f :> string -> float); () val foo : (string -> float) -> unit = |}] -let local_to_global (local_ _s : string) = 42.0 +let global_to_global_to_global (f : float -> string) = f 42.0 -let foo f = ignore (f :> string -> float); [f; local_to_global] +let foo f = + ignore (f :> (local_ float -> string) -> string); + [f; global_to_global_to_global] [%%expect{| -val local_to_global : local_ string -> float = -val foo : (local_ string -> float) -> (local_ string -> float) list = +val global_to_global_to_global : (float -> string) -> string = +val foo : ((float -> string) -> string) -> ((float -> string) -> string) list = + |}] -let global_to_local (_s : string) = local_ 42.0 +let local_to_global_to_global (f : local_ float -> string) = f 42.0 -let foo f = ignore (f :> string -> float); [f; global_to_local] +let foo f = + ignore (f :> (float -> string) -> string); + [f; local_to_global_to_global] [%%expect{| -val global_to_local : string -> local_ float = -Line 3, characters 47-62: -3 | let foo f = ignore (f :> string -> float); [f; global_to_local] - ^^^^^^^^^^^^^^^ -Error: This expression has type string -> local_ float - but an expression was expected of type string -> float +val local_to_global_to_global : (local_ float -> string) -> string = +Line 5, characters 6-31: +5 | [f; local_to_global_to_global] + ^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: This expression has type (local_ float -> string) -> string + but an expression was expected of type (float -> string) -> string + Type local_ float -> string is not compatible with type + float -> string |}] (* Submoding during module inclusion *) diff --git a/ocaml/testsuite/tests/typing-poly/poly_params.ml b/ocaml/testsuite/tests/typing-poly/poly_params.ml index aba9bce510d..7624a40513b 100644 --- a/ocaml/testsuite/tests/typing-poly/poly_params.ml +++ b/ocaml/testsuite/tests/typing-poly/poly_params.ml @@ -279,7 +279,7 @@ Line 1, characters 24-25: 1 | let foo (f : p1) : p2 = f ^ Error: This expression has type p1 = ('a. 'a -> 'a) -> int - but an expression was expected of type p2 = ('a 'b. 'a -> 'b) -> int + but an expression was expected of type ('a 'b. 'a -> 'b) -> int Type 'a is not compatible with type 'b |}];; @@ -328,13 +328,13 @@ Line 4, characters 24-25: 4 | let foo (x : p1) : p2 = x ^ Error: This expression has type p1 = (bool -> bool) -> int - but an expression was expected of type p2 = ('a. 'a -> 'a) -> int + but an expression was expected of type ('a. 'a -> 'a) -> int Type bool is not compatible with type 'a |}];; let foo x = (x : p1 :> p2) [%%expect {| -val foo : p1 -> p2 = +val foo : ((bool -> bool) -> int) -> p2 = |}];; module Foo (X : sig val f : p1 end) : sig val f : p2 end = X diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index f06d9f79e94..cea0aa35132 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -6598,7 +6598,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg not tvar && List.for_all ((=) Nolabel) ls in let inferred = is_inferred sarg in - let rec loosen_ret_modes ty' ty = + let rec loosen_arrow_modes ty' ty = let expty = expand_head env ty in let expty' = expand_head env ty' in let lv = get_level expty in @@ -6607,9 +6607,10 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg | Tarrow((l, marg, mret), ty_arg', ty_res', _), Tarrow(_, ty_arg, ty_res, _) when lv' = generic_level || not !Clflags.principal -> - let ty_res', ty_res, changed = loosen_ret_modes ty_res' ty_res in + let ty_res', ty_res, changed = loosen_arrow_modes ty_res' ty_res in let mret, changed' = Alloc.newvar_below_comonadic mret in - if changed || changed' then + let marg, changed'' = Alloc_mode.newvar_above marg in + if changed || changed' || changed'' then newty2 ~level:lv' (Tarrow((l, marg, mret), ty_arg', ty_res', commu_ok)), newty2 ~level:lv (Tarrow((l, marg, mret), ty_arg, ty_res, commu_ok)), true @@ -6626,7 +6627,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg then Some (Btype.snapshot ()) else None in - let t', t, changed = loosen_ret_modes ty_expected' ty_expected in + let t', t, changed = loosen_arrow_modes ty_expected' ty_expected in if not changed then Option.iter Btype.backtrack snap; t', t else