1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
|
(* TEST
expect;
*)
(* You may constrain abstract types in packages. *)
module type S = sig
type t
end
type m = (module S with type t = int);;
[%%expect{|
module type S = sig type t end
type m = (module S with type t = int)
|}];;
(* You may use variables in the current environment in the new definitions. *)
module type S = sig
type t
end
type 'a m = (module S with type t = 'a);;
[%%expect{|
module type S = sig type t end
type 'a m = (module S with type t = 'a)
|}];;
(* It works with non-trivial paths. *)
module type S = sig
module M : sig
type t
end
end
type m = (module S with type M.t = int)
[%%expect{|
module type S = sig module M : sig type t end end
type m = (module S with type M.t = int)
|}];;
(* It should respect immediacy - [m1] should typecheck but not [m2]. *)
module type S = sig
type t [@@immediate]
end
type m1 = (module S with type t = int)
type m2 = (module S with type t = string);;
[%%expect{|
module type S = sig type t [@@immediate] end
type m1 = (module S with type t = int)
Line 6, characters 18-40:
6 | type m2 = (module S with type t = string);;
^^^^^^^^^^^^^^^^^^^^^^
Error: In this "with" constraint, the new definition of "t"
does not match its original definition in the constrained signature:
Type declarations do not match:
type t = string
is not included in
type t [@@immediate]
The first is not an immediate type.
|}];;
(* You may not constrain types with a manifest in a package *)
module type S = sig
type t = int
end
type m = (module S with type t = string);;
[%%expect{|
module type S = sig type t = int end
Line 5, characters 17-39:
5 | type m = (module S with type t = string);;
^^^^^^^^^^^^^^^^^^^^^^
Error: In the constrained signature, type "t" is defined to be "int".
Package "with" constraints may only be used on abstract types.
|}];;
(* Even if your constraint would be satisfied. *)
(* It would be nice if this worked. *)
module type S = sig
type t = int
end
type m = (module S with type t = int);;
[%%expect{|
module type S = sig type t = int end
Line 5, characters 17-36:
5 | type m = (module S with type t = int);;
^^^^^^^^^^^^^^^^^^^
Error: In the constrained signature, type "t" is defined to be "int".
Package "with" constraints may only be used on abstract types.
|}];;
(* And even if the manifest is not obvious in the original definition. *)
module M = struct
type t
end
module type S = sig
module P = M
end
type m = (module S with type P.t = int);;
[%%expect{|
module M : sig type t end
module type S = sig module P = M end
Line 9, characters 17-38:
9 | type m = (module S with type P.t = int);;
^^^^^^^^^^^^^^^^^^^^^
Error: In the constrained signature, type "P.t" is defined to be "M.t".
Package "with" constraints may only be used on abstract types.
|}];;
(* If writing a package constraint in a mutually recursive group of type decls,
checking that the constraint's immediacy may not rely on the definitions of
other elements of the mutually recursive group. *)
(* It would be nice if this worked. *)
module type S = sig
type t [@@immediate]
end
type t1 = int
and t2 = (module S with type t = t1);;
[%%expect{|
module type S = sig type t [@@immediate] end
Line 6, characters 17-35:
6 | and t2 = (module S with type t = t1);;
^^^^^^^^^^^^^^^^^^
Error: In this "with" constraint, the new definition of "t"
does not match its original definition in the constrained signature:
Type declarations do not match:
type t = t1
is not included in
type t [@@immediate]
The first is not an immediate type.
|}];;
(* When using a package with constraint to give an abstract type a definition
that is immediate, that immediacy information should be usable after
unpacking. *)
module type S = sig
type t
end
type m = (module S with type t = int)
module F (X : sig val x : m end) = struct
module M = (val X.x)
type t = M.t [@@immediate]
end;;
[%%expect{|
module type S = sig type t end
type m = (module S with type t = int)
module F :
(X : sig val x : m end) ->
sig module M : sig type t = int end type t = M.t [@@immediate] end
|}];;
(* Checking such a constraint may require expanding definitions from the module
being updated. *)
module type S = sig
module type S1 = sig
type t
end
module M : S1
end
type t = (module S with type M.t = int)
[%%expect{|
module type S = sig module type S1 = sig type t end module M : S1 end
type t = (module S with type M.t = int)
|}];;
(* Ghosts haunted type definitions *)
module type Private_row = sig
type a
and t = private [< `A | `B ]
and b
and d = private [< `C ]
end
(* This is fine, the ghost type `t#row` is removed silently *)
module type Test = Private_row with type t = [ `A ]
(* This fails currently. If we ever allow it, make sure the ghost type is
removed as above. *)
type fail = (module Private_row with type t = [ `A ] )
[%%expect{|
module type Private_row =
sig type a and t = private [< `A | `B ] and b and d = private [< `C ] end
module type Test =
sig type a and t = [ `A ] and b and d = private [< `C ] end
Line 13, characters 20-52:
13 | type fail = (module Private_row with type t = [ `A ] )
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: In the constrained signature, type "t" is defined to be "[< `A | `B ]".
Package "with" constraints may only be used on abstract types.
|}]
(* More row type examples to consider, if we ever start allowing package type
constraints to replace compatible manifests. *)
module type Private_row = sig
type t = private [< `A ]
end
type t1 = (module Private_row with type t = [ `A ])
[%%expect{|
module type Private_row = sig type t = private [< `A ] end
Line 5, characters 18-50:
5 | type t1 = (module Private_row with type t = [ `A ])
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: In the constrained signature, type "t" is defined to be "[< `A ]".
Package "with" constraints may only be used on abstract types.
|}]
type t2 = (module Private_row with type t = [< `A ])
[%%expect{|
Line 1, characters 18-51:
1 | type t2 = (module Private_row with type t = [< `A ])
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: In the constrained signature, type "t" is defined to be "[< `A ]".
Package "with" constraints may only be used on abstract types.
|}]
type 'a t3 = (module Private_row with type t = [< `A ]) as 'a
[%%expect{|
Line 1, characters 21-54:
1 | type 'a t3 = (module Private_row with type t = [< `A ]) as 'a
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: In the constrained signature, type "t" is defined to be "[< `A ]".
Package "with" constraints may only be used on abstract types.
|}]
type 'a t4 = (module Private_row with type t = [< `A ] as 'a)
[%%expect{|
Line 1, characters 21-60:
1 | type 'a t4 = (module Private_row with type t = [< `A ] as 'a)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: In the constrained signature, type "t" is defined to be "[< `A ]".
Package "with" constraints may only be used on abstract types.
|}]
(** Issue 13778: constraining a type should count as using it *)
module X: sig
type t
end = struct
module type S = sig type s end
type t = (module S with type s = int)
end
[%%expect {|
module X : sig type t end
|}]
|
