1(* test generation of signature mismatch errors *)
2
3(* misc tests --- not exhaustive *)
4
5structure X = struct open General end: sig val + : (int * int) -> int end;
6structure X = struct val x = fn 1 => Div end : sig exception x of int end;
7structure X = struct val x = fn y => y end : sig prim_val  x : 'a ->'a = 1 "identity" end;
8exception e (* static *);
9structure X = struct exception e = e end : sig exception e (* dynamic *) end;
10structure X = struct val x = fn 1 => 1 end : sig val x : 'a -> 'a end;
11structure X = struct val x = fn 1 => Div end : sig exception x of int end;
12structure X = struct val x = fn y => y end : sig prim_val  x : 'a ->'a = 1 "identity" end;
13structure X = struct datatype t = C of int end : sig datatype t = C of bool end;
14
15signature S = sig type t end where type 'a t = int;
16signature S = sig structure X : sig type t end end where type 'a X.t = int;
17signature S = sig structure Y : sig structure X : sig type t end end end where type 'a Y.X.t = int;
18
19(* module mismatches *)
20structure X = struct end:functor(X:sig end)->sig end;
21functor X = (functor(X:sig end)=>struct end) : sig end;
22functor X = (functor(X:sig end)=>struct end): functor(X:sig end)->functor(X:sig end)->sig end;
23functor X = (functor(X:sig end)=>functor(X:sig end)=>struct end): functor(X:sig end)->sig end;
24functor X = (functor(X:functor(X:sig end)->sig end)=>struct end): functor(X:sig end)->sig end;
25functor X = (functor(X:sig end)=>struct end): functor(F:functor(X:sig end)->sig end)->sig end;
26
27
28(* systematic tests *)
29
30(* missing type declarations *)
31
32signature G = sig type t = unit end;
33signature L = sig end;
34
35functor L = functor (L:L)=>
36  L:G;
37functor LL = functor(LL:functor(L:L)->L)=>
38  LL:functor(L:L)->G;
39functor GL = functor(GL:functor(L:G)->L)=>
40  GL:functor(L:L)->L;
41functor YL = functor(YL:sig structure Y:L end)=>
42  YL:sig structure Y: G end;
43functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
44  L_YL:functor(L:L)->sig structure Y: G end;
45functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
46  YG_L:functor(YL:sig structure Y: L end)->L;
47functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
48  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
49functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
50  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
51
52(* missing value declarations *)
53
54signature G = sig val x: unit end;
55signature L = sig end;
56
57functor L = functor (L:L)=>
58  L:G;
59functor LL = functor(LL:functor(L:L)->L)=>
60  LL:functor(L:L)->G;
61functor GL = functor(GL:functor(L:G)->L)=>
62  GL:functor(L:L)->L;
63functor YL = functor(YL:sig structure Y:L end)=>
64  YL:sig structure Y: G end;
65functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
66  L_YL:functor(L:L)->sig structure Y: G end;
67functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
68  YG_L:functor(YL:sig structure Y: L end)->L;
69functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
70  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
71functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
72  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
73
74(* missing structure declarations *)
75
76signature G = sig structure X: sig end end;
77signature L = sig end;
78
79functor L = functor (L:L)=>
80  L:G;
81functor LL = functor(LL:functor(L:L)->L)=>
82  LL:functor(L:L)->G;
83functor GL = functor(GL:functor(L:G)->L)=>
84  GL:functor(L:L)->L;
85functor YL = functor(YL:sig structure Y:L end)=>
86  YL:sig structure Y: G end;
87functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
88  L_YL:functor(L:L)->sig structure Y: G end;
89functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
90  YG_L:functor(YL:sig structure Y: L end)->L;
91functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
92  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
93functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
94  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
95
96(* missing functor declarations *)
97
98signature G = sig functor F:functor(X:sig end)->sig end
99	      end;
100signature L = sig end;
101
102functor L = functor (L:L)=>
103  L:G;
104functor LL = functor(LL:functor(L:L)->L)=>
105  LL:functor(L:L)->G;
106functor GL = functor(GL:functor(L:G)->L)=>
107  GL:functor(L:L)->L;
108functor YL = functor(YL:sig structure Y:L end)=>
109  YL:sig structure Y: G end;
110functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
111  L_YL:functor(L:L)->sig structure Y: G end;
112functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
113  YG_L:functor(YL:sig structure Y: L end)->L;
114functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
115  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
116functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
117  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
118
119(* scheme mismatch *)
120
121signature G = sig val x : 'a -> 'a end;
122signature L = sig val x : int -> int end;
123
124functor L = functor (L:L)=>
125  L:G;
126functor LL = functor(LL:functor(L:L)->L)=>
127  LL:functor(L:L)->G;
128functor GL = functor(GL:functor(L:G)->L)=>
129  GL:functor(L:L)->L;
130functor YL = functor(YL:sig structure Y:L end)=>
131  YL:sig structure Y: G end;
132functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
133  L_YL:functor(L:L)->sig structure Y: G end;
134functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
135  YG_L:functor(YL:sig structure Y: L end)->L;
136functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
137  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
138functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
139  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
140
141(* scheme mismatch with free type parameter *)
142val 'b fail =
143let
144      signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end;
145      signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end;
146
147      functor L = functor (L:L)=>
148	  L:G;
149in unit
150end
151;
152val 'b fail =
153let
154      signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end;
155      signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end;
156      functor LL = functor(LL:functor(L:L)->L)=>
157	  LL:functor(L:L)->G;
158in unit
159end
160;
161val 'b fail =
162let
163      signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end;
164      signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end;
165      functor GL = functor(GL:functor(L:G)->L)=>
166	  GL:functor(L:L)->L;
167in unit
168end
169;
170val 'b fail =
171let
172      signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end;
173      signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end;
174      functor YL = functor(YL:sig structure Y:L end)=>
175	  YL:sig structure Y: G end;
176in unit
177end
178;
179val 'b fail =
180let
181      signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end;
182      signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end;
183      functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
184	  L_YL:functor(L:L)->sig structure Y: G end;
185in unit
186end
187;
188val 'b fail =
189let
190      signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end;
191      signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end;
192      functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
193	  YG_L:functor(YL:sig structure Y: L end)->L;
194in unit
195end
196;
197val 'b fail =
198let
199      signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end;
200      signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end;
201      functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
202	  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
203in unit
204end
205;
206val 'b fail =
207let
208      signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end;
209      signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end;
210      functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
211	  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
212in ()
213end;
214
215(* status mismatch *)
216
217signature G = sig exception x end;
218signature L = sig val x : exn end;
219
220functor L = functor (L:L)=>
221  L:G;
222functor LL = functor(LL:functor(L:L)->L)=>
223  LL:functor(L:L)->G;
224functor GL = functor(GL:functor(L:G)->L)=>
225  GL:functor(L:L)->L;
226functor YL = functor(YL:sig structure Y:L end)=>
227  YL:sig structure Y: G end;
228functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
229  L_YL:functor(L:L)->sig structure Y: G end;
230functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
231  YG_L:functor(YL:sig structure Y: L end)->L;
232functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
233  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
234functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
235  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
236
237(* conenv mismatch *)
238
239signature G = sig datatype t = C of int end;
240signature L = sig datatype t = D of int end;
241
242functor L = functor (L:L)=>
243  L:G;
244functor LL = functor(LL:functor(L:L)->L)=>
245  LL:functor(L:L)->G;
246functor GL = functor(GL:functor(L:G)->L)=>
247  GL:functor(L:L)->L;
248functor YL = functor(YL:sig structure Y:L end)=>
249  YL:sig structure Y: G end;
250functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
251  L_YL:functor(L:L)->sig structure Y: G end;
252functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
253  YG_L:functor(YL:sig structure Y: L end)->L;
254functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
255  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
256functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
257  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
258
259(* arity mismatch *)
260
261signature G = sig type t = unit end;
262signature L = sig type 'a t = unit end;
263
264functor L = functor (L:L)=>
265  L:G;
266functor LL = functor(LL:functor(L:L)->L)=>
267  LL:functor(L:L)->G;
268functor GL = functor(GL:functor(L:G)->L)=>
269  GL:functor(L:L)->L;
270functor YL = functor(YL:sig structure Y:L end)=>
271  YL:sig structure Y: G end;
272functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
273  L_YL:functor(L:L)->sig structure Y: G end;
274functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
275  YG_L:functor(YL:sig structure Y: L end)->L;
276functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
277  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
278functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
279  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
280
281(* ref equality mismatch *)
282
283signature G = sig datatype myref = datatype ref end;
284signature L = sig type 'a myref = 'a end;
285
286functor L = functor (L:L)=>
287  L:G;
288functor LL = functor(LL:functor(L:L)->L)=>
289  LL:functor(L:L)->G;
290functor GL = functor(GL:functor(L:G)->L)=>
291  GL:functor(L:L)->L;
292functor YL = functor(YL:sig structure Y:L end)=>
293  YL:sig structure Y: G end;
294functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
295  L_YL:functor(L:L)->sig structure Y: G end;
296functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
297  YG_L:functor(YL:sig structure Y: L end)->L;
298functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
299  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
300functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
301  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
302
303(* ref equality mismatch *)
304
305signature G = sig prim_EQtype t end;
306signature L = sig type t end;
307
308functor L = functor (L:L)=>
309  L:G;
310functor LL = functor(LL:functor(L:L)->L)=>
311  LL:functor(L:L)->G;
312functor GL = functor(GL:functor(L:G)->L)=>
313  GL:functor(L:L)->L;
314functor YL = functor(YL:sig structure Y:L end)=>
315  YL:sig structure Y: G end;
316functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
317  L_YL:functor(L:L)->sig structure Y: G end;
318functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
319  YG_L:functor(YL:sig structure Y: L end)->L;
320functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
321  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
322functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
323  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
324
325(* equality mismatch *)
326
327signature G = sig eqtype t end;
328signature L = sig type t = unit -> unit end;
329
330functor L = functor (L:L)=>
331  L:G;
332functor LL = functor(LL:functor(L:L)->L)=>
333  LL:functor(L:L)->G;
334functor GL = functor(GL:functor(L:G)->L)=>
335  GL:functor(L:L)->L;
336functor YL = functor(YL:sig structure Y:L end)=>
337  YL:sig structure Y: G end;
338functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
339  L_YL:functor(L:L)->sig structure Y: G end;
340functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
341  YG_L:functor(YL:sig structure Y: L end)->L;
342functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
343  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
344functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
345  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
346
347(* transparent mismatch *)
348
349signature G = sig type t = unit end;
350signature L = sig type t = unit -> unit end;
351
352functor L = functor (L:L)=>
353  L:G;
354functor LL = functor(LL:functor(L:L)->L)=>
355  LL:functor(L:L)->G;
356functor GL = functor(GL:functor(L:G)->L)=>
357  GL:functor(L:L)->L;
358functor YL = functor(YL:sig structure Y:L end)=>
359  YL:sig structure Y: G end;
360functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
361  L_YL:functor(L:L)->sig structure Y: G end;
362functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
363  YG_L:functor(YL:sig structure Y: L end)->L;
364functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
365  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
366functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
367  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
368
369(* datatype mismatch *)
370
371signature G = sig datatype t = C end;
372signature L = sig type t = unit end;
373
374functor L = functor (L:L)=>
375  L:G;
376functor LL = functor(LL:functor(L:L)->L)=>
377  LL:functor(L:L)->G;
378functor GL = functor(GL:functor(L:G)->L)=>
379  GL:functor(L:L)->L;
380functor YL = functor(YL:sig structure Y:L end)=>
381  YL:sig structure Y: G end;
382functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
383  L_YL:functor(L:L)->sig structure Y: G end;
384functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
385  YG_L:functor(YL:sig structure Y: L end)->L;
386functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
387  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
388functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
389  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
390
391(* scope violations *)
392
393signature G = functor X:sig type t end ->sig type u end;
394signature L = functor(X:sig type t end)->sig type u end;
395
396functor L = functor (L:L)=>
397  L:G;
398functor LL = functor(LL:functor(L:L)->L)=>
399  LL:functor(L:L)->G;
400functor GL = functor(GL:functor(L:G)->L)=>
401  GL:functor(L:L)->L;
402
403(* scope violations (cont.)
404   we need to embed the functors in structures for these tests *)
405
406signature G = sig functor F: functor  X:sig type t end ->sig type u end end;
407signature L = sig functor F: functor(X:sig type t end)->sig type u end end;
408
409functor YL = functor(YL:sig structure Y:L end)=>
410  YL:sig structure Y: G end;
411functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=>
412  L_YL:functor(L:L)->sig structure Y: G end;
413functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=>
414  YG_L:functor(YL:sig structure Y: L end)->L;
415functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=>
416  L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L;
417functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=>
418  FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end;
419
420
421
422
423
424
425
426
427
428