-
Notifications
You must be signed in to change notification settings - Fork 76
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add a new attribute for allowing any mode crossing
Replace the [@@unsafe_allow_any_kind_in_{impl,intf}] attributes with a new [@@unsafe_allow_any_mode_crossing] attribute. This is different in that it: 1. Works on the type declaration, not the inclusion check, so is more powerful - it can be used to illegally mode cross types defined in the same module, or illegally mode cross non-abstract types in interfaces. The latter especially is necessary to fully subsume -allow-illegal-crossing in stdlib 2. Only allows changing the modal bounds of a kind, not the layout - it's unclear that anyone should ever want to unsafely change the layout of a kind; I personally can't think of any sound reason to do so. Some [past discussion][0] on the specific syntax for this attribute suggested specifying the bounds directly on the attribute, rather than using the jkind annotation, but I and others feel reasonably strongly that this way of doing things is a better design for the sake of consistency. [0]: #3385 (comment)
- Loading branch information
1 parent
4de5a72
commit a6c01ea
Showing
9 changed files
with
176 additions
and
185 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,190 +1,166 @@ | ||
(* TEST | ||
flags = "-extension layouts_beta"; | ||
flags = "-extension layouts_alpha"; | ||
expect; | ||
*) | ||
|
||
let use_as_value : ('a : value) -> 'a = fun x -> x | ||
let use_uncontended : 'a @ uncontended -> 'a = fun x -> x | ||
|
||
(* Baseline: if the jkind doesn't match, we should get an error. *) | ||
module Mismatched_no_attrs : sig | ||
type t : float64 | ||
end = struct | ||
type t = string | ||
end | ||
type t : value mod uncontended = { mutable contents : string } | ||
[%%expect{| | ||
Lines 3-5, characters 6-3: | ||
3 | ......struct | ||
4 | type t = string | ||
5 | end | ||
Error: Signature mismatch: | ||
Modules do not match: | ||
sig type t = string end | ||
is not included in | ||
sig type t : float64 end | ||
Type declarations do not match: | ||
type t = string | ||
is not included in | ||
type t : float64 | ||
The layout of the first is value | ||
because it is the primitive type string. | ||
But the layout of the first must be a sublayout of float64 | ||
because of the definition of t at line 2, characters 2-18. | ||
val use_as_value : 'a -> 'a = <fun> | ||
val use_uncontended : ('a : value_or_null). 'a -> 'a = <fun> | ||
Line 5, characters 0-62: | ||
5 | type t : value mod uncontended = { mutable contents : string } | ||
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
Error: The kind of type "t" is value | ||
because it's a boxed record type. | ||
But the kind of type "t" must be a subkind of value mod uncontended | ||
because of the annotation on the declaration of the type t. | ||
|}] | ||
|
||
(* On the other hand, if we set the correct attributes on both the impl and the intf, we | ||
shouldn't get an error (though, obviously, this is completely unsound!) *) | ||
module Mismatched_with_both_attrs : sig | ||
type t : float64 | ||
[@@unsafe_allow_any_kind_in_impl "I love segfaults"] | ||
end = struct | ||
type t = string | ||
[@@unsafe_allow_any_kind_in_intf "I love segfaults"] | ||
end | ||
(* On the other hand, if we set the attribute, we shouldn't get an error. *) | ||
type t : value mod uncontended = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
let f (x : t @@ contended) = use_uncontended x | ||
[%%expect{| | ||
module Mismatched_with_both_attrs : sig type t : float64 end | ||
type t : value mod uncontended = { mutable contents : string; } | ||
val f : t @ contended -> t = <fun> | ||
|}] | ||
|
||
(* If we set the attributes but *don't* get a kind mismatch, we ought to be fine *) | ||
module Matching : sig | ||
type t : value | ||
[@@unsafe_allow_any_kind_in_impl "I love segfaults"] | ||
end = struct | ||
type t = string | ||
[@@unsafe_allow_any_kind_in_intf "I love segfaults"] | ||
end | ||
(* If we set the attribute but *don't* get a kind mismatch, we ought to be fine *) | ||
type t : value mod many portable uncontended = string | ||
[@@unsafe_allow_any_mode_crossing] | ||
[%%expect{| | ||
Lines 2-3, characters 2-54: | ||
2 | ..type t : value | ||
3 | [@@unsafe_allow_any_kind_in_impl "I love segfaults"] | ||
Warning 212 [unnecessary-allow-any-kind]: [@@allow_any_kind_in_intf] and [@@allow_any_kind_in_impl] set on a | ||
type, but the kind matches. The attributes can be removed. | ||
|
||
module Matching : sig type t end | ||
type t = string | ||
|}] | ||
|
||
(* If the attr is only on the signature we should get an error *) | ||
module Mismatched_with_attr_on_intf : sig | ||
type t : float64 | ||
[@@unsafe_allow_any_kind_in_impl "I love segfaults"] | ||
end = struct | ||
type t = string | ||
end | ||
(* The attribute shouldn't allow us to change the layout *) | ||
type t : float64 mod uncontended = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
[%%expect{| | ||
Lines 4-6, characters 6-3: | ||
4 | ......struct | ||
5 | type t = string | ||
6 | end | ||
Error: Signature mismatch: | ||
Modules do not match: | ||
sig type t = string end | ||
is not included in | ||
sig type t : float64 end | ||
Type declarations do not match: | ||
type t = string | ||
is not included in | ||
type t : float64 | ||
The layout of the first is value | ||
because it is the primitive type string. | ||
But the layout of the first must be a sublayout of float64 | ||
because of the definition of t at lines 2-3, characters 2-54. | ||
Lines 1-2, characters 0-34: | ||
1 | type t : float64 mod uncontended = { mutable contents : string } | ||
2 | [@@unsafe_allow_any_mode_crossing] | ||
Error: The layout of type "t" is value | ||
because it's a boxed record type. | ||
But the layout of type "t" must be a sublayout of float64 | ||
because of the annotation on the declaration of the type t. | ||
|}] | ||
|
||
(* If the attr is only on the struct we should get an error *) | ||
module Mismatched_with_attr_on_impl : sig | ||
type t : float64 | ||
(* Abstract types in signatures should work with the unsafe kind *) | ||
module M : sig | ||
type t : value mod uncontended | ||
end = struct | ||
type t = string | ||
[@@unsafe_allow_any_kind_in_intf "I love segfaults"] | ||
type t : value mod uncontended = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
|
||
let f (x : t @@ contended) = use_uncontended x | ||
end | ||
[%%expect{| | ||
Lines 3-6, characters 6-3: | ||
3 | ......struct | ||
4 | type t = string | ||
5 | [@@unsafe_allow_any_kind_in_intf "I love segfaults"] | ||
6 | end | ||
Error: Signature mismatch: | ||
Modules do not match: | ||
sig type t = string end | ||
is not included in | ||
sig type t : float64 end | ||
Type declarations do not match: | ||
type t = string | ||
is not included in | ||
type t : float64 | ||
The layout of the first is value | ||
because it is the primitive type string. | ||
But the layout of the first must be a sublayout of float64 | ||
because of the definition of t at line 2, characters 2-18. | ||
module M : sig type t : value mod uncontended end | ||
|}] | ||
|
||
(* Some more complex stuff with functors *) | ||
|
||
module type S1 = sig | ||
type t : value | ||
end | ||
module M1 : sig | ||
type t : value mod uncontended = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
end = struct | ||
type t : value mod uncontended = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
|
||
module type S2 = sig | ||
type t : float64 | ||
[@@unsafe_allow_any_kind_in_impl] | ||
let f (x : t @@ contended) = use_uncontended x | ||
end | ||
module M2 : sig | ||
type t : value mod uncontended = M1.t = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
end = struct | ||
type t : value mod uncontended = M1.t = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
|
||
module type S1 = sig | ||
type t : value | ||
[@@unsafe_allow_any_kind_in_intf] | ||
let f (x : t @@ contended) = use_uncontended x | ||
end | ||
|
||
module F1 (X : S1) : S2 = X | ||
|
||
[%%expect{| | ||
module type S1 = sig type t end | ||
module type S2 = sig type t : float64 end | ||
module type S1 = sig type t end | ||
module F1 : functor (X : S1) -> S2 | ||
module M1 : | ||
sig type t : value mod uncontended = { mutable contents : string; } end | ||
module M2 : | ||
sig | ||
type t = M1.t : value mod uncontended = { mutable contents : string; } | ||
end | ||
|}] | ||
|
||
module F2 (X : S2) : S1 = X | ||
(* Private types still require the attribute *) | ||
module Private : sig | ||
type t : value mod uncontended = private { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
end = struct | ||
type t : value mod uncontended = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
|
||
let f (x : t @@ contended) = use_uncontended x | ||
end | ||
[%%expect{| | ||
Line 1, characters 26-27: | ||
1 | module F2 (X : S2) : S1 = X | ||
^ | ||
Error: Signature mismatch: | ||
Modules do not match: sig type t = X.t end is not included in S1 | ||
Type declarations do not match: type t = X.t is not included in type t | ||
The layout of the first is float64 | ||
because of the definition of t at lines 6-7, characters 2-35. | ||
But the layout of the first must be a sublayout of value | ||
because of the definition of t at lines 11-12, characters 2-35. | ||
module Private : | ||
sig | ||
type t : value mod uncontended = private { mutable contents : string; } | ||
end | ||
|}] | ||
|
||
(* Non-abstract types can be annotated with [@@unsafe_allow_any_kind_in_intf] too, and get | ||
checked against signatures during inclusion. *) | ||
(* Non-abstract types in signatures should work as long as they specify the attribute *) | ||
module M : sig | ||
type t1 : value mod uncontended = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
|
||
module M1 : sig | ||
type t : value = string [@@unsafe_allow_any_kind_in_intf] | ||
type t2 : value mod uncontended = private { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
|
||
type t3 : value mod uncontended = | ||
| Immut of string | ||
| Mut of { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
end = struct | ||
type t = string | ||
end | ||
type t1 : value mod uncontended = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
|
||
type t2 : value mod uncontended = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
|
||
module M2 : S2 = M1 | ||
type t3 : value mod uncontended = | ||
| Immut of string | ||
| Mut of { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
|
||
let f1 (x : t1 @@ contended) = use_uncontended x | ||
let f2 (x : t2 @@ contended) = use_uncontended x | ||
let f3 (x : t3 @@ contended) = use_uncontended x | ||
end | ||
[%%expect{| | ||
module M1 : sig type t = string end | ||
module M2 : S2 | ||
module M : | ||
sig | ||
type t1 : value mod uncontended = { mutable contents : string; } | ||
type t2 : value mod uncontended = private { mutable contents : string; } | ||
type t3 | ||
: value mod uncontended = | ||
Immut of string | ||
| Mut of { mutable contents : string; } | ||
end | ||
|}] | ||
|
||
module type S3 = sig | ||
type t : value | ||
[@@unsafe_allow_any_kind_in_impl] | ||
end | ||
(* If the kind annotation on a (non-abstract) type has a more general layout than the one | ||
inferred from the declaration, we should be able to use the type as if it had the | ||
inferred layout - but also able to use it as if it had the modal bounds on the | ||
annotation. | ||
*) | ||
module Weaker_layout_stronger_modes : sig | ||
type t : any mod uncontended | ||
end = struct | ||
type t : any mod uncontended = { mutable contents : string } | ||
[@@unsafe_allow_any_mode_crossing] | ||
|
||
module M3 : S3 = M1 | ||
(* CR aspsmith: This is somewhat unfortunate, if S3 and M1 are defined far away, but it's | ||
unclear how to squash the warning *) | ||
(* The actual kind here looks more like [value mod uncontended] *) | ||
let f1 (x : t @@ contended) = use_uncontended x | ||
let _ = use_as_value ({ contents = "foo" } : t) | ||
end | ||
[%%expect{| | ||
module type S3 = sig type t end | ||
Lines 2-3, characters 2-35: | ||
2 | ..type t : value | ||
3 | [@@unsafe_allow_any_kind_in_impl] | ||
Warning 212 [unnecessary-allow-any-kind]: [@@allow_any_kind_in_intf] and [@@allow_any_kind_in_impl] set on a | ||
type, but the kind matches. The attributes can be removed. | ||
|
||
module M3 : S3 | ||
module Weaker_layout_stronger_modes : sig type t : any mod uncontended end | ||
|}] |
Oops, something went wrong.