Skip to content

"module type of" zap modalities to floor #3922

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.

Sign up for GitHub

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 5 commits into from
Apr 30, 2025
Merged

"module type of" zap modalities to floor #3922

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
35cec81
"module type of" zap modalities to floor
riaqn Apr 23, 2025
3bad77a
fix tests
riaqn Apr 24, 2025
e1a691b
add test
riaqn Apr 24, 2025
f117e2d
recover principality issue
riaqn Apr 29, 2025
73e9b86
add CR
riaqn Apr 30, 2025
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
106 changes: 94 additions & 12 deletions testsuite/tests/typing-modes/val_modalities.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,18 +73,48 @@ module Module_type_of_comonadic = struct
module M = struct
let x @ portable = fun x -> x
end
(* for comonadic axes, we default to id = meet_with_max, which is the
weakest. *)
(* for comonadic axes, we default to meet_with_min, which is the strongest.
*)
module M' : module type of M = struct
let x @ portable = fun x -> x
end
let _ = portable_use M.x (* The original inferred modality is zapped *)
end
[%%expect{|
Line 10, characters 25-28:
10 | let _ = portable_use M.x (* The original inferred modality is zapped *)
^^^
Error: This value is "nonportable" but expected to be "portable".
module Module_type_of_comonadic :
sig
module M : sig val x : 'a -> 'a @@ stateless end
module M' : sig val x : 'a -> 'a @@ stateless end
end
|}]

(* zapping behavior can cause type error that shouldn't happen in upstream ocaml *)
module Module_type_of_error = struct
module M = struct
let x = fun x -> x
end

module M' : module type of M = struct
let y = ref 42
let x = fun x -> ignore !y; x
end
end
[%%expect{|
Lines 6-9, characters 33-5:
6 | .................................struct
7 | let y = ref 42
8 | let x = fun x -> ignore !y; x
9 | end
Error: Signature mismatch:
Modules do not match:
sig val y : int ref val x : 'a -> 'a end
is not included in
sig val x : 'a -> 'a @@ stateless end
Values do not match:
val x : 'a -> 'a
is not included in
val x : 'a -> 'a @@ stateless
The second is portable and the first is nonportable.
|}]

module Module_type_of_monadic = struct
Expand All @@ -95,13 +125,28 @@ module Module_type_of_monadic = struct
(* for monadic axes, we try to push to the id = join_with_min. The original
modality is pushed to floor. *)
module M' : module type of M = struct
let x @ contended = ref "hello"
let x @ contended = ref "hello"
end
end
[%%expect{|
Lines 8-10, characters 35-7:
8 | ...................................struct
9 | let x @ contended = ref "hello"
9 | let x @ contended = ref "hello"
10 | end
Error: Signature mismatch:
Modules do not match:
sig val x : string ref @@ contended end
is not included in
sig val x : string ref @@ stateless end
Values do not match:
val x : string ref @@ contended
is not included in
val x : string ref @@ stateless
The second is uncontended and the first is contended.
|}, Principal{|
Lines 8-10, characters 35-7:
8 | ...................................struct
9 | let x @ contended = ref "hello"
10 | end
Error: Signature mismatch:
Modules do not match:
Expand All @@ -123,28 +168,65 @@ module Module_type_nested = struct
end
end
module M' : module type of M = struct
let x @ nonportable = fun t -> t
let x @ portable = fun t -> t
module N = struct
let y @ contended = ref "hello"
end
end
end
(* CR zqian: Need to add mode crossing at binding to remove the principality
issue. See
https://github.com/ocaml-flambda/flambda-backend/pull/3922#discussion_r2059000469
*)
[%%expect{|
Lines 8-13, characters 35-7:
8 | ...................................struct
9 | let x @ nonportable = fun t -> t
9 | let x @ portable = fun t -> t
10 | module N = struct
11 | let y @ contended = ref "hello"
12 | end
13 | end
Error: Signature mismatch:
Modules do not match:
sig
val x : 'a -> 'a @@ stateless
module N : sig val y : string ref @@ contended end
end
is not included in
sig
val x : 'a -> 'a @@ stateless
module N : sig val y : string ref @@ stateless end
end
In module "N":
Modules do not match:
sig val y : string ref @@ contended end
is not included in
sig val y : string ref @@ stateless end
In module "N":
Values do not match:
val y : string ref @@ contended
is not included in
val y : string ref @@ stateless
The second is uncontended and the first is contended.
|}, Principal{|
Lines 8-13, characters 35-7:
8 | ...................................struct
9 | let x @ portable = fun t -> t
10 | module N = struct
11 | let y @ contended = ref "hello"
12 | end
13 | end
Error: Signature mismatch:
Modules do not match:
sig
val x : 'a -> 'a
val x : 'a -> 'a @@ stateless
module N : sig val y : string ref @@ contended end
end
is not included in
sig val x : 'a -> 'a module N : sig val y : string ref end end
sig
val x : 'a -> 'a @@ stateless
module N : sig val y : string ref end
end
In module "N":
Modules do not match:
sig val y : string ref @@ contended end
Expand Down
5 changes: 4 additions & 1 deletion testsuite/tests/typing-modules/aliases.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -663,7 +663,10 @@ module type S =
sig
module N : sig module I = Int end
module P :
sig module I : sig type t = int val compare : 'a -> 'a -> int end end
sig
module I :
sig type t = int val compare : 'a -> 'a -> int @@ portable end
end
module Q :
sig type wrap' = wrap = W of (Set.Make(Int).t, Set.Make(N.I).t) eq end
end
Expand Down
37 changes: 22 additions & 15 deletions testsuite/tests/typing-zero-alloc/signatures.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -865,7 +865,8 @@ end

[%%expect{|
module M_base_for_mto : sig val f : int -> int [@@zero_alloc] end
module type S_base_mto = sig val f : int -> int [@@zero_alloc] end
module type S_base_mto =
sig val f : int -> int @@ portable [@@zero_alloc] end
module M_mto_base_good : S_base_mto
Lines 11-13, characters 37-3:
11 | .....................................struct
Expand All @@ -879,7 +880,7 @@ Error: Signature mismatch:
Values do not match:
val f : int -> int [@@zero_alloc opt]
is not included in
val f : int -> int [@@zero_alloc]
val f : int -> int @@ portable [@@zero_alloc]
The former provides a weaker "zero_alloc" guarantee than the latter.
|}]

Expand All @@ -899,7 +900,8 @@ end

[%%expect{|
module M_strict_for_mto : sig val f : int -> int [@@zero_alloc strict] end
module type S_strict_mto = sig val f : int -> int [@@zero_alloc strict] end
module type S_strict_mto =
sig val f : int -> int @@ portable [@@zero_alloc strict] end
module M_mto_strict_good : S_strict_mto
Lines 11-13, characters 41-3:
11 | .........................................struct
Expand All @@ -913,7 +915,7 @@ Error: Signature mismatch:
Values do not match:
val f : int -> int [@@zero_alloc]
is not included in
val f : int -> int [@@zero_alloc strict]
val f : int -> int @@ portable [@@zero_alloc strict]
The former provides a weaker "zero_alloc" guarantee than the latter.
|}]

Expand All @@ -937,9 +939,11 @@ module type S_no_nrn = module type of M_nrn_for_mto

[%%expect{|
module M_assume_for_mto : sig val f : int -> int * int [@@zero_alloc] end
module type S_no_assume = sig val f : int -> int * int [@@zero_alloc] end
module type S_no_assume =
sig val f : int -> int * int @@ portable [@@zero_alloc] end
module M_nrn_for_mto : sig val f : int -> int * int [@@zero_alloc] end
module type S_no_nrn = sig val f : int -> int * int [@@zero_alloc] end
module type S_no_nrn =
sig val f : int -> int * int @@ portable [@@zero_alloc] end
|}]

(**********************************************)
Expand Down Expand Up @@ -1047,8 +1051,8 @@ module type S = module type of M_infer2
[%%expect{|
module type S =
sig
val f : 'a -> 'a [@@zero_alloc strict]
val g : 'a -> 'a [@@zero_alloc]
val f : 'a -> 'a @@ stateless [@@zero_alloc strict]
val g : 'a -> 'a @@ stateless [@@zero_alloc]
end
|}]

Expand Down Expand Up @@ -1127,7 +1131,10 @@ module type S = module type of M_explicit_arity_2
[%%expect{|
module M_explicit_arity_2 : sig type t = int -> int val f : int -> t end
module type S =
sig type t = int -> int val f : int -> t [@@zero_alloc arity 2] end
sig
type t = int -> int
val f : int -> t @@ stateless [@@zero_alloc arity 2]
end
|}]

(***************************)
Expand All @@ -1146,7 +1153,7 @@ end
module type S = module type of M_for_mto
[%%expect{|
module M_for_mto : sig val f : int -> int end
module type S = sig val f : int -> int end
module type S = sig val f : int -> int @@ portable end
|}]

(* [S] itself is fixed. *)
Expand All @@ -1157,11 +1164,11 @@ Line 1, characters 61-62:
^
Error: Signature mismatch:
Modules do not match:
sig val f : int -> int end
sig val f : int -> int @@ portable end
is not included in
sig val f : int -> int [@@zero_alloc] end
Values do not match:
val f : int -> int
val f : int -> int @@ portable
is not included in
val f : int -> int [@@zero_alloc]
The former provides a weaker "zero_alloc" guarantee than the latter.
Expand All @@ -1178,18 +1185,18 @@ module type S' = module type of M_for_mto
module F' (X : S') : sig val[@zero_alloc] f : int -> int end = X
module F (X : S) : sig val[@zero_alloc] f : int -> int end = X
[%%expect{|
module type S' = sig val f : int -> int [@@zero_alloc] end
module type S' = sig val f : int -> int @@ portable [@@zero_alloc] end
module F' : functor (X : S') -> sig val f : int -> int [@@zero_alloc] end
Line 7, characters 61-62:
7 | module F (X : S) : sig val[@zero_alloc] f : int -> int end = X
^
Error: Signature mismatch:
Modules do not match:
sig val f : int -> int end
sig val f : int -> int @@ portable end
is not included in
sig val f : int -> int [@@zero_alloc] end
Values do not match:
val f : int -> int
val f : int -> int @@ portable
is not included in
val f : int -> int [@@zero_alloc]
The former provides a weaker "zero_alloc" guarantee than the latter.
Expand Down
4 changes: 1 addition & 3 deletions typing/typemod.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3562,11 +3562,9 @@ let type_module_type_of env smod =
let mty = Mtype.scrape_for_type_of ~remove_aliases env tmty.mod_type in
(* PR#5036: must not contain non-generalized type variables *)
check_nongen_modtype env smod.pmod_loc mty;
(* for [module type of], we zap to identity modality for best legacy
compatibility *)
let mty =
remove_modality_and_zero_alloc_variables_mty env
~zap_modality:Mode.Modality.Value.zap_to_id mty
~zap_modality:Mode.Modality.Value.zap_to_floor mty
in
tmty, mty

Expand Down