Skip to content

Commit

Permalink
Normalize before printing (#3612)
Browse files Browse the repository at this point in the history 
* Move normalize function (only)

* Fix compilation errors

* Normalize when printing without with-bounds

* Make arguments mandatory, not optional
  • Loading branch information
@goldfirere
goldfirere authored Feb 25, 2025
1 parent 5452641 commit 0fc831f
Show file tree
Hide file tree
Showing 21 changed files with 555 additions and 446 deletions.
28 changes: 14 additions & 14 deletions testsuite/tests/typing-jkind-bounds/annots.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,7 @@ Line 1, characters 21-23:
^^
Error: This alias is bound to type "int list"
but is used as an instance of type "('a : immediate)"
The kind of int list is immutable_data
The kind of int list is value
because it's a boxed variant type.
But the kind of int list must be a subkind of immediate
because of the annotation on the type variable 'a.
Expand All @@ -261,7 +261,7 @@ Line 1, characters 21-23:
^^
Error: This alias is bound to type "int list"
but is used as an instance of type "('a : value mod global)"
The kind of int list is immutable_data
The kind of int list is value
because it's a boxed variant type.
But the kind of int list must be a subkind of value mod global
because of the annotation on the type variable 'a.
Expand Down Expand Up @@ -1117,7 +1117,7 @@ type t : value mod global = { x : t_value }
Line 1, characters 0-43:
1 | type t : value mod global = { x : t_value }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 global
because of the annotation on the declaration of the type t.
Expand All @@ -1128,7 +1128,7 @@ type t : value mod aliased = { x : t_value }
Line 1, characters 0-44:
1 | type t : value mod aliased = { x : t_value }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 aliased
because of the annotation on the declaration of the type t.
Expand All @@ -1139,7 +1139,7 @@ type t : value mod many = { x : t_value }
Line 1, characters 0-41:
1 | type t : value mod many = { x : t_value }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 many
because of the annotation on the declaration of the type t.
Expand All @@ -1150,7 +1150,7 @@ type t : value mod portable = { x : t_value }
Line 1, characters 0-45:
1 | type t : value mod portable = { x : t_value }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 portable
because of the annotation on the declaration of the type t.
Expand All @@ -1161,7 +1161,7 @@ type t : value mod contended = { x : t_value }
Line 1, characters 0-46:
1 | type t : value mod contended = { x : t_value }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 contended
because of the annotation on the declaration of the type t.
Expand All @@ -1172,7 +1172,7 @@ type t : value mod external_ = { x : t_value }
Line 1, characters 0-46:
1 | type t : value mod external_ = { x : t_value }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 external_
because of the annotation on the declaration of the type t.
Expand Down Expand Up @@ -1256,7 +1256,7 @@ type t : value mod global = Foo of t_value
Line 1, characters 0-42:
1 | type t : value mod global = Foo of t_value
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
Error: The kind of type "t" is value
because it's a boxed variant type.
But the kind of type "t" must be a subkind of value mod global
because of the annotation on the declaration of the type t.
Expand All @@ -1267,7 +1267,7 @@ type t : value mod aliased = Foo of t_value
Line 1, characters 0-43:
1 | type t : value mod aliased = Foo of t_value
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
Error: The kind of type "t" is value
because it's a boxed variant type.
But the kind of type "t" must be a subkind of value mod aliased
because of the annotation on the declaration of the type t.
Expand All @@ -1278,7 +1278,7 @@ type t : value mod many = Foo of t_value
Line 1, characters 0-40:
1 | type t : value mod many = Foo of t_value
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
Error: The kind of type "t" is value
because it's a boxed variant type.
But the kind of type "t" must be a subkind of value mod many
because of the annotation on the declaration of the type t.
Expand All @@ -1289,7 +1289,7 @@ type t : value mod portable = Foo of t_value
Line 1, characters 0-44:
1 | type t : value mod portable = Foo of t_value
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
Error: The kind of type "t" is value
because it's a boxed variant type.
But the kind of type "t" must be a subkind of value mod portable
because of the annotation on the declaration of the type t.
Expand All @@ -1300,7 +1300,7 @@ type t : value mod contended = Foo of t_value
Line 1, characters 0-45:
1 | type t : value mod contended = Foo of t_value
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
Error: The kind of type "t" is value
because it's a boxed variant type.
But the kind of type "t" must be a subkind of value mod contended
because of the annotation on the declaration of the type t.
Expand All @@ -1311,7 +1311,7 @@ type t : value mod external_ = Foo of t_value
Line 1, characters 0-45:
1 | type t : value mod external_ = Foo of t_value
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
Error: The kind of type "t" is value
because it's a boxed variant type.
But the kind of type "t" must be a subkind of value mod external_
because of the annotation on the declaration of the type t.
Expand Down
20 changes: 10 additions & 10 deletions testsuite/tests/typing-jkind-bounds/basics.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,13 +9,13 @@
type 'a list : immutable_data with 'a

[%%expect{|
type 'a list : immutable_data
type 'a list : immutable_data with 'a
|}]

type ('a, 'b) either : immutable_data with 'a * 'b

[%%expect{|
type ('a, 'b) either : immutable_data
type ('a, 'b) either : immutable_data with 'a * 'b
|}]

type 'a gel : kind_of_ 'a mod global
Expand Down Expand Up @@ -762,7 +762,7 @@ type t : any mod many = { x : t_value }
Line 1, characters 0-39:
1 | type t : any mod many = { x : t_value }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 any mod many
because of the annotation on the declaration of the type t.
Expand All @@ -773,7 +773,7 @@ type t : any mod contended = { x : t_value }
Line 1, characters 0-44:
1 | type t : any mod contended = { x : t_value }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 any mod contended
because of the annotation on the declaration of the type t.
Expand All @@ -784,7 +784,7 @@ type t : any mod portable = { x : t_value }
Line 1, characters 0-43:
1 | type t : any mod portable = { x : t_value }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 any mod portable
because of the annotation on the declaration of the type t.
Expand All @@ -795,7 +795,7 @@ type t : any mod many contended portable global = { x : t_value }
Line 1, characters 0-65:
1 | type t : any mod many contended portable global = { x : t_value }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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
any mod global many contended portable
Expand Down Expand Up @@ -1234,7 +1234,7 @@ type 'a t : value mod aliased = { x : 'a @@ aliased }
Line 1, characters 0-53:
1 | type 'a t : value mod aliased = { x : 'a @@ aliased }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 aliased
because of the annotation on the declaration of the type t.
Expand All @@ -1245,7 +1245,7 @@ type 'a t : value mod global = { x : 'a @@ global }
Line 1, characters 0-51:
1 | type 'a t : value mod global = { x : 'a @@ global }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 global
because of the annotation on the declaration of the type t.
Expand Down Expand Up @@ -1547,7 +1547,7 @@ type 'a t : value mod global = { x : 'a }
Line 1, characters 0-41:
1 | type 'a t : value mod global = { x : 'a }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 global
because of the annotation on the declaration of the type t.
Expand All @@ -1558,7 +1558,7 @@ type 'a t : value mod many = { x : 'a }
Line 1, characters 0-39:
1 | type 'a t : value mod many = { x : 'a }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
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 many
because of the annotation on the declaration of the type t.
Expand Down
14 changes: 7 additions & 7 deletions testsuite/tests/typing-jkind-bounds/composite.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,7 @@ Line 1, characters 13-20:
1 | let foo (t : int ref t @@ contended) = use_uncontended t
^^^^^^^
Error: This type "int ref" should be an instance of type "('a : immutable_data)"
The kind of int ref is mutable_data.
The kind of int ref is value mod many unyielding.
But the kind of int ref must be a subkind of immutable_data
because of the definition of t at line 1, characters 0-46.
|}]
Expand Down Expand Up @@ -320,7 +320,7 @@ Line 1, characters 13-20:
1 | let foo (t : int ref t @@ contended) = use_uncontended t
^^^^^^^
Error: This type "int ref" should be an instance of type "('a : immutable_data)"
The kind of int ref is mutable_data.
The kind of int ref is value mod many unyielding.
But the kind of int ref must be a subkind of immutable_data
because of the definition of t at line 1, characters 0-73.
|}]
Expand Down Expand Up @@ -500,7 +500,7 @@ Line 1, characters 0-149:
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "int list list list list list list list list list list
list list list list list list list list list list
list list list list" is immutable_data
list list list list" is value
because it's a boxed variant type.
But the kind of type "int list list list list list list list list list
list list list list list list list list list list
Expand Down Expand Up @@ -568,7 +568,7 @@ type 'a t : immutable_data = Flat | Nested of 'a t t
Line 1, characters 0-52:
1 | type 'a t : immutable_data = Flat | Nested of 'a t t
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
Error: The kind of type "t" is value
because it's a boxed variant type.
But the kind of type "t" must be a subkind of immutable_data
because of the annotation on the declaration of the type t.
Expand Down Expand Up @@ -611,7 +611,7 @@ type ('a : immutable_data) t : immutable_data = Flat | Nested of 'a t t
Line 1, characters 0-71:
1 | type ('a : immutable_data) t : immutable_data = Flat | Nested of 'a t t
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The kind of type "t" is immutable_data
Error: The kind of type "t" is value
because it's a boxed variant type.
But the kind of type "t" must be a subkind of immutable_data
because of the annotation on the declaration of the type t.
Expand Down Expand Up @@ -647,7 +647,7 @@ Error: This value is "aliased" but expected to be "unique".
type 'a u : immutable_data with 'a
type t = { x : int u; y : string u }
[%%expect {|
type 'a u : immutable_data
type 'a u : immutable_data with 'a
type t = { x : int u; y : string u; }
|}]

Expand Down Expand Up @@ -688,7 +688,7 @@ type 'a t =
| None
| Some of ('a * 'a) t u
[%%expect {|
type 'a u : immutable_data
type 'a u : immutable_data with 'a
type 'a t = None | Some of ('a * 'a) t u
|}]

Expand Down
5 changes: 4 additions & 1 deletion testsuite/tests/typing-jkind-bounds/gadt.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,10 @@ type (_ : any, _ : any) eq = Refl : ('a : any). ('a, 'a) eq
val use_portable : 'a @ portable -> unit = <fun>
module F :
functor (X : S) ->
sig type t3 : value mod portable type t4 : value mod portable end
sig
type t3 : value mod portable with X.t1
type t4 : value mod portable with X.t2
end
module Arg1 : sig type t1 = int -> int type t2 = string end
module M1 : sig type t3 = F(Arg1).t3 type t4 = F(Arg1).t4 end
>> Fatal error: Abstract kind with [with]: value mod portable
Expand Down
20 changes: 12 additions & 8 deletions testsuite/tests/typing-jkind-bounds/no-infer-across-modules/test.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ Line 1, characters 20-31:
^^^^^^^^^^^
Error: This type "int Define_with_kinds.my_list" should be an instance of type
"('a : value mod portable)"
The kind of int Define_with_kinds.my_list is immutable_data.
The kind of int Define_with_kinds.my_list is value.
But the kind of int Define_with_kinds.my_list must be a subkind of
value mod portable
because of the definition of require_portable at line 12, characters 0-47.
Expand All @@ -63,7 +63,8 @@ Line 1, characters 20-35:
^^^^^^^^^^^^^^^
Error: This type "int ref Define_with_kinds.my_list"
should be an instance of type "('a : value mod portable)"
The kind of int ref Define_with_kinds.my_list is immutable_data.
The kind of int ref Define_with_kinds.my_list is
value mod many unyielding.
But the kind of int ref Define_with_kinds.my_list must be a subkind of
value mod portable
because of the definition of require_portable at line 12, characters 0-47.
Expand All @@ -76,7 +77,8 @@ Line 1, characters 20-40:
^^^^^^^^^^^^^^^^^^^^
Error: This type "(int -> int) Define_with_kinds.my_list"
should be an instance of type "('a : value mod portable)"
The kind of (int -> int) Define_with_kinds.my_list is immutable_data.
The kind of (int -> int) Define_with_kinds.my_list is
value mod contended.
But the kind of (int -> int) Define_with_kinds.my_list must be a subkind of
value mod portable
because of the definition of require_portable at line 12, characters 0-47.
Expand All @@ -89,7 +91,7 @@ Line 1, characters 14-25:
^^^^^^^^^^^
Error: This type "int Define_with_kinds.my_list" should be an instance of type
"('a : value mod global)"
The kind of int Define_with_kinds.my_list is immutable_data.
The kind of int Define_with_kinds.my_list is value.
But the kind of int Define_with_kinds.my_list must be a subkind of
value mod global
because of the definition of require_global at line 9, characters 0-43.
Expand All @@ -102,7 +104,8 @@ Line 1, characters 20-35:
^^^^^^^^^^^^^^^
Error: This type "int ref Define_with_kinds.my_list"
should be an instance of type "('a : value mod contended)"
The kind of int ref Define_with_kinds.my_list is immutable_data.
The kind of int ref Define_with_kinds.my_list is
value mod many unyielding.
But the kind of int ref Define_with_kinds.my_list must be a subkind of
value mod contended
because of the definition of require_contended at line 11, characters 0-49.
Expand All @@ -116,7 +119,7 @@ Line 1, characters 20-38:
Error: This type "int Define_with_kinds.my_ref Define_with_kinds.my_list"
should be an instance of type "('a : value mod contended)"
The kind of int Define_with_kinds.my_ref Define_with_kinds.my_list is
immutable_data.
value mod many unyielding.
But the kind of int Define_with_kinds.my_ref Define_with_kinds.my_list must be a subkind of
value mod contended
because of the definition of require_contended at line 11, characters 0-49.
Expand All @@ -134,7 +137,7 @@ Line 1, characters 20-38:
Error: This type "int Define_with_kinds.my_ref Define_with_kinds.my_list"
should be an instance of type "('a : value mod portable)"
The kind of int Define_with_kinds.my_ref Define_with_kinds.my_list is
immutable_data.
value mod many unyielding.
But the kind of int Define_with_kinds.my_ref Define_with_kinds.my_list must be a subkind of
value mod portable
because of the definition of require_portable at line 12, characters 0-47.
Expand Down Expand Up @@ -248,11 +251,12 @@ Error: This expression has type
"#((int -> int) * int) Define_with_kinds.unboxed_record"
but an expression was expected of type "('a : (value & value) & value)"
The kind of #((int -> int) * int) Define_with_kinds.unboxed_record is
(immutable_data & immutable_data) & immutable_data.
(value mod contended & value mod contended) & value mod contended.
But the kind of #((int -> int) * int) Define_with_kinds.unboxed_record must be a subkind of
(value & value) & value
because of the definition of use_portable_three_values at line 2, characters 84-95.
|}]
(* CR layouts v2.8: Lift bounds outside of products *)

(******)

Expand Down
Loading

0 comments on commit 0fc831f

Please sign in to comment.